时间戳

首页 > 解决方案 > 如何解释 z3 API 求解器的 z3.solve() 函数的输出？

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

问题描述

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

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

标签： pythonsmtz3py

解决方案

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

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

推荐阅读