Wie wird der gesamte symbolische Ausdruck in Z3 ausgedruckt?

Question

Ich verwende Z3Py für einige Analyseaufgabe, und für viele Male möchte ich den symbolischen Ausdruck ausdrucken. Zum Beispiel

a = BitVecVal("test", 32) + 13 
print a 

Allerdings finde ich, dass, sobald der Z3 Ausdruck ziemlich groß wird, kann es voll wird einfach nicht ausdrucken. Stattdessen wird der „Auslassungs“ recht häufig verwendet werden, um den Ausdruck zu vereinfachen ...

So, hier ist meine Frage, wie kann ich voll einen Z3 Ausdruck ausdrucken? Gibt es eine bestimmte API, die ich nutzen könnte?

Answer 1

Die am besten skalierbare Möglichkeit ist die Verwendung des SMT-LIB-Druckers. Zum Beispiel:

x = Int('x') 
for i in range(12): 
    x = x + x 

print x.sexpr() 

druckt:

(let ((a!1 (+ (+ (+ x x) (+ x x)) (+ (+ x x) (+ x x))))) 
(let ((a!2 (+ (+ (+ a!1 a!1) (+ a!1 a!1)) (+ (+ a!1 a!1) (+ a!1 a!1))))) 
(let ((a!3 (+ (+ (+ a!2 a!2) (+ a!2 a!2)) (+ (+ a!2 a!2) (+ a!2 a!2))))) 
    (+ (+ (+ a!3 a!3) (+ a!3 a!3)) (+ (+ a!3 a!3) (+ a!3 a!3)))))) 

Sie Parameter auf der Formatierungs durch den ziemlich Drucker mit der Funktion ‚set_pp_option‘ verwendet steuern kann. Sie müssten im Quellcode von z3printer.py nachsehen, welche Optionen den Zweck erfüllen.