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

Question

给定 Z3py 中的表达式，我可以将其转换为 SMT-LIB2 语言吗？（所以我可以将此 SMT-LIB2 表达式提供给支持 SMT-LIB2 的其他 SMT 求解器）

如果可能，请举一个例子。

非常感谢。

Answer 1

我们可以使用 C API Z3_benchmark_to_smtlib_string。C 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")