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使用自己漂亮的打印機來表達。它在文件src/api/python/z3printer.py中定義。這臺漂亮的打印機有幾個配置參數。 您可以使用以下命令來設置它們：

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

這將防止輸出被截斷大型表達式。 備註：Z3Py漂亮打印機效率低於Z3庫中的可用打印機效率。如果性能出現問題，您應該使用Nuno Lopes建議的SMT2格式打印機。