Z3py：打印具有 144 个变量的大型公式答案

【问题标题】：Z3py: print large formula with 144 variablesZ3py：打印具有 144 个变量的大型公式
【发布时间】：2013-10-24 14:57:21
【问题描述】：

我使用 Z3 定理证明器，并且我有一个大公式（114 个变量）。我可以打印一个包含所有子句的大公式吗？普通的print str(f) 会截断输出，最后只打印“...”，而不是所有子句。

我测试了print f.sexpr()，这总是会打印所有子句。但是仅在 sexpr 语法中。

我可以打印公式的所有子句但避免使用 s-expression 语法吗？

注意：为了说明问题，代码示例太小了，但发布一个大公式会占用太多空间。

from z3 import *


C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))



f = simplify(C)

#
# PRINTING
#

# for large a formula with 114 variables, the output of str(f) gets truncated
# only "..." is displayed at the end, not all the clauses are shown
# this is printed in the format I need:
print str(f) 

# this always prints all the clauses, even for very large formulae
# here all clauses are printed, but not the format I need:
print f.sexpr()

# if you try the above two commands with a very large formula you see the difference!

【问题讨论】：

可以打印SMT2格式的公式：stackoverflow.com/a/14629021/1841530

标签： python z3 z3py sat-solvers

【解决方案1】：

Z3Py 使用自己的漂亮打印机来打印表达式。它在文件src/api/python/z3printer.py 中定义。这台漂亮的打印机有几个配置参数。您可以使用以下命令设置它们：

set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)

这将防止输出因大型表达式而被截断。备注：Z3Py 漂亮的打印机比 Z3 库中可用的打印机效率低。如果性能有问题，您应该按照 Nuno Lopes 的建议使用 SMT2 格式打印机。

【讨论】：