如何在Z3中打印出整個符號表達式？

Question

我正在使用Z3Py進行一些分析任務，並且很多時候，我想打印出符號表達式。例如，

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

然而，我發現，一旦Z3表達變得相當大，它只是不能完全打印出來。相反，「省略號」將經常因此，這裏是我的問題用於簡化表達......

，我怎麼能完全打印出Z3體現在哪裏？有什麼特定的API可以利用嗎？

Answer 1

最具擴展性的方法是使用SMT-LIB打印機。 例如：

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

print x.sexpr() 

會打印：

(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)))))) 

您可以通過使用該功能「set_pp_option」漂亮的打印機使用的格式化控制參數。你將不得不查看z3printer.py的源代碼來確定哪些選項可以做到這一點。