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

Question

我正在使用Z3 Python接口为我的实验创建公式。然后我将这个公式发送给Z3解算器。如果我是正确的Z3使用它自己的求解器！

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

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

Answer 1

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

Z3py是一个特定于Z3的API（如名称所示），它不提供使用其他SMT求解器的方法。

Answer 2

听起来像你应该真的使用解算器不可知的SMT接口，而不是Z3py。已经有一些尝试创建这样的接口，有不同程度的支持多种解算器：

• https://github.com/pysmt/pysmt是求解不可知的Python API来SMT求解。我自己并没有使用它，但它确实听起来很有希望，特别是如果你想Python作为你的顶级API。

• https://github.com/sosy-lab/java-smt是一个类似的项目，它使用Java作为主机语言。

• http://leventerkok.github.io/sbv/是我自己尝试为使用SMT解算器提供解算器不可知的API，这是用Haskell编写的。

绝不意味着这是一份详尽的清单。我敢肯定，还有其他的语言，不同程度的成熟度。您应该选择哪一个取决于您的主机语言偏好以及每个系统提供的功能;这可能差别很大。