Z3:将Z3py表达式转换为SMT-LIB2？

Question

给定Z3py中的表达式,我可以将其转换为SMT-LIB2语言吗？(所以我可以将这个SMT-LIB2表达式提供给支持SMT-LIB2的其他SMT求解器)

如果可以,请举一个例子.

非常感谢.

Answer 1

我们可以使用C API Z3_benchmark_to_smtlib_string.Z API中的每个函数都可以在Z3Py中使用.此函数最初用于转储SMT 1.0格式的基准测试,并且它早于SMT 2.0.这就是为什么它有一些看似不必要的参数.现在,默认情况下,它将以SMT 2.0格式显示基准.输出并不意味着人类可读.我们可以编写以下Python函数以使其更方便使用:

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

这是一个使用它的小例子(也可在这里在线获得)

a = Int('a')
b = Int('b')
f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0)
print toSMT2Benchmark(f, logic="QF_LIA")