python - Z3py:打印包含 144 个变量的大公式

Question

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

我测试了 print f.sexpr() 并且它总是打印所有的子句。但是仅在 sexpr 语法中。

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

注意:代码示例太小无法显示问题，但发布大公式会占用太多空间。

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!

Answer 1

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

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

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