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

【问题标题】：Z3: convert Z3py expression to SMT-LIB2?Z3：将 Z3py 表达式转换为 SMT-LIB2？
【发布时间】：2013-01-15 16:50:31
【问题描述】：

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

如果可以，请举个例子。

非常感谢。

【问题讨论】：

标签： z3

【解决方案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())

这是一个使用它的小例子（也可以在线获得here）

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

【讨论】：

你能告诉我一个类似的 Java API 来转换为 SMTLIB2 吗？谢谢。
“v = (Ast * 0)()”是什么意思？
太棒了！我现在得到一个 Z3 python 段错误我不知道如何调试。这应该很有帮助。