2

我使用 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!
4

1 回答 1

4

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 格式打印机。

于 2013-10-24T15:40:10.293 回答