Z3:将 Z3py 表达式从 Solver 对象转换为 SMT-LIB2

这个问题非常类似于:Z3: convert Z3py expression to SMT-LIB2?

是否可以从 Solver 对象生成 SMT-LIB2 输出？

最佳答案

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

编辑 我们可以使用以下脚本以 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")

结束编辑

关于Z3:将 Z3py 表达式从 Solver 对象转换为 SMT-LIB2，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/14775122/