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

【问题标题】：How to print out the whole symbolic expression in Z3?如何在 Z3 中打印出整个符号表达式？
【发布时间】：2023-03-31 10:34:01
【问题描述】：

我正在使用Z3Py 进行一些分析任务，并且多次想打印出符号表达式。例如，

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

但是，我发现一旦Z3 表达式变得相当大，它就无法完全打印出来。相反，“ellipsis”将经常用于简化表达式...

所以这是我的问题，我怎样才能完全打印出Z3 表达式？我可以利用任何特定的 API 吗？

【问题讨论】：

标签： z3 z3py

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

【讨论】：