verhindern, dass die Lösung vereinfacht wird

Question

Ich möchte die Lösung von z3 ohne Vereinfachung mit let Anweisungen zurück.

Zum Beispiel, wenn ich geben Sie den folgenden:

(declare-const x Int) 
    (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
      (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
             (and (<= (- 4 x.1) 0) 
              (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0)))) 

ich als zurück, um die Lösung zu bekommen:

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= x 13))) 
       (<= x 11)))) 
    (or (and (<= x 4) (>= x 4) (<= x 11)) a!1)) 

Gibt es eine Möglichkeit Z3 zu sagen, nicht einige komplexe Ausdrücke in eine let-Anweisung zu extrahieren ? Es wird für mich leichter sein, das Ergebnis zu parsen, wenn ich die Antwort ohne Angabe von letter flat bekomme.

Answer 1

Wir können die folgenden Optionen setzen die Z3 ziemlich Drucker verwenden let s

(set-option :pp-min-alias-size 1000000) 
(set-option :pp-max-depth  1000000) 

jede große Zahl wird der Trick zu verhindern.

Wir müssen daran denken, dass es möglicherweise nicht machbar ist, einige Formeln anzuzeigen, die viele gemeinsame Unterausdrücke enthalten, wenn wir die let s vermeiden. Intern speichert Z3 die Formeln als DAGs anstelle von Bäumen. Wenn wir die let s nicht verwenden, kann der Pretty-Print solcher Formeln exponentiell größer sein als ihre interne Darstellung. Also sollten wir die oben genannten Optionen nicht missbrauchen.

Answer 2

Ich benutze z3-4.5.0 und sieht aus wie die Optionen Namen ein wenig geändert haben. Wenn pp-max-depth nicht für Sie funktioniert, versuchen Sie pp.max_depth und pp.min_alias_size.

Ich bin mit dem Java-API und die folgenden mit mir gearbeitet

com.microsoft.z3.Global.setParameter("pp.min_alias_size", "1000000"); 
com.microsoft.z3.Global.setParameter("pp.max_depth", "1000000");