Z3py: вывести большую формулу с 144 переменными
Я использую доказательство теоремы 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!
1 ответ
Z3Py использует собственный симпатичный принтер для выражений. Определяется в файле src/api/python/z3printer.py
, Этот симпатичный принтер имеет несколько параметров конфигурации. Вы можете установить их, используя следующую команду:
set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)
Это предотвратит усечение вывода для больших выражений. Примечание: симпатичный принтер Z3Py менее эффективен, чем тот, который доступен в библиотеке Z3. Если производительность является проблемой, вы должны использовать принтер формата SMT2 в соответствии с рекомендациями Nuno Lopes.