Этот вопрос очень похож на: Z3: convert Z3py expression to SMT-LIB2?Z3: преобразовать выражение Z3py в SMT-Lib2 от объекта Solver
Можно ли генерировать вывод SMT-Lib2 от объекта Solver?
Этот вопрос очень похож на: Z3: convert Z3py expression to SMT-LIB2?Z3: преобразовать выражение Z3py в SMT-Lib2 от объекта Solver
Можно ли генерировать вывод SMT-Lib2 от объекта Solver?
Класс Solver
имеет метод, называемый assertions()
. Он возвращает все формулы, утверждаемые в заданный решатель. После извлечения утверждений мы можем использовать тот же подход, который использовался в предыдущем вопросе. Вот быстрый и грязный модификация
def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
if isinstance(f, Solver):
a = f.assertions()
if len(a) == 0:
f = BoolVal(True)
else:
f = And(*a)
return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())
Вот пример (also available online at here)
s = Solver()
print toSMT2Benchmark(s, logic="QF_LIA")
a, b = Ints('a b')
s.add(a > 1)
s.add(Or(a < 1, b < 2))
print toSMT2Benchmark(s, logic="QF_LIA")
EDIT Мы можем использовать следующий скрипт для вывода в формате SMTLIB 1.x (также доступно онлайн here). Обратите внимание, что SMTLIB 1.x очень ограничен, и некоторые функции не поддерживаются. Мы также настоятельно рекомендуем всем пользователям перейти на SMTLIB 2.x.
def toSMTBenchmark(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
if isinstance(f, Solver):
a = f.assertions()
if len(a) == 0:
f = BoolVal(True)
else:
f = And(*a)
Z3_set_ast_print_mode(f.ctx_ref(), Z3_PRINT_SMTLIB_COMPLIANT) # Set SMTLIB 1.x pretty print mode
r = Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())
Z3_set_ast_print_mode(f.ctx_ref(), Z3_PRINT_SMTLIB2_COMPLIANT) # Restore SMTLIB 2.x pretty print mode
return r
s = Solver()
print toSMTBenchmark(s, logic="QF_LIA")
a, b = Ints('a b')
s.add(a > 1)
s.add(Or(a < 1, b < 2))
print toSMTBenchmark(s, logic="QF_LIA")
END EDIT
Можно ли заставить z3 вернуть SMT-LIB 1.2 совместимую кодировку? – user1217406
Я обновил сообщение. –