Мне нужно распечатать всю проблему Z3, чтобы отладить ее, но когда я распечатываю ее, вывод обрезается.
from z3 import *
s = Solver()
... Add many assertions to s ...
print(s)
Как мне все отобразить?
Отключение усечения печати Z3py
Ответы (1)
Пытаться:
set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)
Возможно, вы захотите поиграть с реальными ценностями, чтобы придумать что-то, что соответствует вашим потребностям.
person
alias
schedule
25.05.2020
Спасибо. Почему не
s.set_option()? Повлияет ли это на другие программы, вызывающие z3?
- person HiDefender; 26.05.2020
Параметры применяются ко всем объектам z3py, а не только к
Solver. (Например, Expr, Int, ...) Итак, это имеет смысл, это не зависит от решателя. Не уверен, что вы имеете в виду, повлияет ли это на другие программы. Если вы имеете в виду, если они увидят, что их собственные структуры данных будут напечатаны по-другому: тогда ответ отрицательный. Если вы имеете в виду, что объекты z3py, которые они хранят, будут напечатаны по-другому, тогда ответ - да. Эти настройки применяются только к объектам z3py, независимо от того, кто за них владеет.
- person alias; 26.05.2020
