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