如何解释 z3 API 求解器中 z3.solve() 函数的输出？

如何解决如何解释 z3 API 求解器中 z3.solve() 函数的输出？

我是 z3 smt 求解器的新手。我正在使用 python API z3py。

我有一个关于 z3.solve() 函数输出的快速问题。当我在某些约束上调用 z3.solve() 并得到 [] 作为输出时，这意味着什么？ 也可以有人给我推荐一个好的文档

解决方法

您确实需要提供导致这种情况的输入，因为这实际上取决于您的约束。但这是说明这种行为的最简单方法：

from z3 import *

z3.solve([])

当我运行这个时，我得到：

[]

我想这就是你所看到的。这实质上意味着您的系统对于所有变量都是可满足的；即，要么您没有约束，要么它们不以任何特定方式约束模型。在上面，没有约束，所以我们有“平凡”模型。如果你做一些更有趣的事情，说：

from z3 import *

a,b = Ints('a b')
z3.solve([a > b,b > 3])

然后你会看到一个更有趣的模型：

[b = 4,a = 5]

总体上有大量关于 z3、z3py 和 SMTLib 的文档（描述了所有 SMT 求解器使用的底层语言）：

• 对于 z3，以 https://rise4fun.com/z3/tutorial 开头
• 对于 z3 python 绑定，使用：https://ericpony.github.io/z3py-tutorial/guide-examples.htm
• 一般 SMTLib 信息：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

请注意，z3 也可以从许多其他语言编写脚本，包括 C、C++、Java、Scala 和 Haskell 等等。通常，使用高级语言比直接使用 SMTLib 或基本的 C 绑定要容易得多。 Python 和 Haskell（在我看来）提供了最高级别的抽象来简化 z3 编程，但是您应该选择哪种环境实际上取决于您的总体目标是什么。 （虽然大多数绑定支持通用约束编程，但它们具有不同级别的自动化和对不同 z3 设施的访问。）