在Z3中使用不同的后端解算器

Question

我正在使用Z3 Python接口为我的实验创建公式。然后，我将该公式发送到Z3求解器。如果我没记错的话，Z3使用了自己的求解器！

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

我在CBMC (C bounded Checker)中使用的方法是:运行程序并生成一个中间DIMAC表示(在一个文件中)，然后使用该文件作为其他SAT求解器的输入。我可以在Z3中做类似的事情吗？谢谢。

Answer 1

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

• https://github.com/pysmt/pysmt是一种与求解器无关的Python API。我自己还没有用过它，但它听起来确实很有前途，特别是如果你想要Python作为你的顶层API.
• https://github.com/sosy-lab/java-smt是一个类似的项目，它使用Java作为主机language.
• http://leventerkok.github.io/sbv/是我自己的尝试，它提供了一个使用language.
• http://leventerkok.github.io/sbv/求解器的求解器不可知的API，这是用Haskell编写的。

这绝对不是一个详尽的列表。我相信，在不同的宿主语言中，也有其他语言，具有不同程度的成熟度。您应该选择哪种语言，这实际上取决于您的宿主语言偏好，以及每个系统提供的功能；这可能会有很大的差异。

Answer 2

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

Z3py是一个特定于Z3的API (顾名思义)，它不提供使用其他SMT解算器的方法。