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

Question

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

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

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

Answer 1

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

• 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，这个 API 是用 Haskell 编写的。

这绝不是一个详尽的列表。我敢肯定还有其他的，使用不同的宿主语言，具有不同程度的成熟度。您应该选择哪一个取决于您的宿主语言偏好以及每个系统提供的功能；这可能会有很大差异。