smt - Z3 可以检查包含递归函数的公式的可满足性吗？

Question

我正在尝试 a Z3 tutorial 的一些示例涉及递归函数。我已经尝试了以下示例。

Fibonacci (第 8.3 节)

IsNat (第 8.3 节)

Inductive (第 10.5 节)

Z3上述所有示例均超时。但是，教程似乎暗示只有 Inductive是非终止的。

Z3 是否可以检查包含递归函数的公式的可满足性或无法处理任何归纳事实？

Answer 1

Z3 教程中的这些示例用于说明 Z3 背后技术的局限性。

Z3 在这些示例中失败有两个原因:

Z3 生成的模型为每个未解释的函数符号指定了解释。这些模型可以被视为功能程序。当前版本不产生递归定义。第一个例子是可满足的，但 Z3 无法产生 fib 的解释，因为它不支持递归定义。
我们计划在这个方向上扩展 Z3。

Z3 不支持归纳证明。例 2 和例 3 是不可满足的，但 Z3 失败了，因为它不支持归纳证明。
我们还计划为此添加基本支持。

虽然这些项目在我的 TODO list 上，但我今年不会开始处理它们。