La simplification d'une expression entraîne une temporisation

Question

Comment simplifier l'expression suivante à l'aide de Z3 Solver?

(declare-const c0 Int) 
(declare-const c1 Int) 
(declare-const c2 Int) 

(assert (let ((a!1 (to_real (+ (* (* 2 c0) c2) 
        (* (* 2 c0) c1) 
        (* 2 c1 c2) 
        (* c0 (- c0 1)) 
        (* c1 (- c1 1)))))) 
    (let ((a!2 (/ (to_real (* (* 2 c0) c2)) a!1))) 
    (and (or (and (<= c2 1) (>= c2 1) (<= c0 2) (>= c0 2) (<= c1 3) (>= c1 3)) 
      (and (<= c2 1) (>= c2 1) (<= c0 3) (>= c0 3) (<= c1 2) (>= c1 2))) 
    (= (/ 2.0 15.0) a!2)))) 
) 

(apply (then qe propagate-values (repeat (then ctx-solver-simplify propagate-ineqs) 10))) 

Lien: http://rise4fun.com/Z3/u7F7

J'ai essayé toutes les tactiques possibles que je connais et pourtant fini par causer le temps par le solveur. Y a-t-il un moyen d'éviter le temps mort? Est-il supposé retourner faux à Java API?

Answer 1

Il est difficile de dire ce qui se passe en regardant ce code. Mais je pense que to_real pourrait être la partie problématique, car la conversion entre les domaines a tendance à générer des contraintes non linéaires qui peuvent causer des problèmes de complexité.

Je donnerais un essai en utilisant purement Reals (à savoir, déclarer c0, c1 .. comme Real s;. Et de supprimer les appels à to_real)

Si vous avez besoin d'entiers/reals mixtes; assurez-vous que le mélange est fait au niveau des feuilles (c'est-à-dire aux constantes); ou tout en haut, autant que vous pouvez pousser les conversions autour; au lieu de aux valeurs intermédiaires.

Mais j'imagine que coller à Reals serait le moyen d'aller ici si l'espace de problème le permet.

Answer 2

L'exemple utilise une arithmétique entière non linéaire. Malheureusement, il est facile de produire des exemples dans ce domaine où Z3 ne se termine pas. La routine ctx-solver-simplify appelle le solveur SMT plusieurs fois et dans chaque invocation doit vérifier la satisfiabilité d'une combinaison des contraintes non-linéaires.