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. Если производительность является проблемой, вы должны использовать принтер формата SMT2 в соответствии с рекомендациями Nuno Lopes.