Z3: преобразовать выражение Z3py в 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())

Вот пример (также доступен здесь)

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")

РЕДАКТИРОВАНИЕ Мы можем использовать следующий сценарий для отображения вывода в формате SMTLIB 1.x (также доступен в Интернете здесь). Обратите внимание, что 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")

ЗАВЕРШИТЬ РЕДАКТИРОВАНИЕ