z3 - 在 Z3 中使用不同的后端求解器

Question

我正在使用 Z3 Python 界面为我的实验创建公式。然后我将该公式发送到 Z3 求解器。如果我是正确的 Z3 使用它自己的求解器！

如何在 Z3py 中使用不同的 SAT/SMT 求解器？

我在 CBMC（C 有界模型检查器）中使用的方法：运行程序并吐出中间 DIMAC 表示（在文件中），然后将该文件用作其他 SAT 求解器的输入。我可以在 Z3 中做类似的事情吗？谢谢你。

score 4 · Accepted Answer

听起来你真的应该使用与求解器无关的 SMT 接口而不是 Z3py。已经多次尝试创建这样的接口，对多个求解器提供不同程度的支持：

https://github.com/pysmt/pysmt是 SMT 求解器的求解器无关 Python API。我自己没有使用过它，但它听起来很有希望，特别是如果您希望 Python 作为您的顶级 API。
https://github.com/sosy-lab/java-smt是一个类似的项目，它使用 Java 作为宿主语言。
http://leventerkok.github.io/sbv/是我自己尝试为使用 SMT 求解器提供与求解器无关的 API，这是用 Haskell 编写的。

这绝不是一份详尽的清单。我敢肯定还有其他语言，使用不同的宿主语言，成熟度不同。你应该选择哪一个取决于你的宿主语言偏好，以及每个系统提供的功能；这可能变化很大。

score 2 · Accepted Answer

所有 SMT 求解器都支持 SMT2 输入格式，因此您可以对 Z3 和其他 SMT 求解器执行相同操作。Z3py 可以将 Solver 和 Goal 对象转换为符合 SMT2 的字符串（一些复杂的变量声明，例如某些数据类型可能会丢失）。

Z3py 是 Z3 特定的 API（顾名思义），它不提供使用其他 SMT 求解器的方法。

2 回答 2