z3: вывести очень длинное утверждение

Question

Возьмем для примера следующее:

trues = [True] * 1000
a = z3.And(trues)

Итак, a - это соединение 1000 True s. Обратите внимание, что это не практический пример, поскольку a логически эквивалентен True.

Если мы print(a), полное утверждение не отображается. Вместо этого результат заканчивается на ...).

Чтобы напечатать полное утверждение, я нашел одно решение - напечатать s-выражение из a. То есть print(a.sexpr()). Таким образом, отображаются все 1000 True.

Итак, мой вопрос: есть ли лучший способ распечатать очень длинное утверждение, например a?

Answer 1

Конечно. Попробуйте:

import z3

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

trues = [True] * 1000
a = z3.And(trues)

print(a)

Вы можете поиграть с числами до set_option, чтобы получить что-то более разумное для вашего варианта использования.