如何在 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 的源代码以确定哪些选项可以解决问题。

如何在 Z3 中打印出整个符号表达式？

How to print out the whole symbolic expression in Z3?

z3

z3py