Z3py:打印包含 144 个变量的大型公式 [英] Z3py: print large formula with 144 variables

问题描述

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

I use the Z3 theorem prover and I have a large formula (114 variables). Can I print a large formula with all clauses? A normal print str(f) truncates the output, and only "..." is printed at the end, not all the clauses.

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

I tested print f.sexpr() and this always prints all the clauses. However only in the sexpr syntax.

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

Can I print all the clauses of a formula but avoid the s-expression syntax?

注意:代码示例很少能说明问题，但发布一个大公式会占用太多空间.

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!

推荐答案

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

Z3Py uses its own pretty printer for expressions. It is defined in the file src/api/python/z3printer.py. This pretty printer has several configuration parameters. You can set them using the following command:

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

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

This will prevent the output to be truncated for large expressions. Remark: the Z3Py pretty printer is less efficient than the one available in the Z3 library. If performance is an issue, you should use the SMT2 format printer as suggested by Nuno Lopes.

这篇关于Z3py:打印包含 144 个变量的大型公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！