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

Question

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

1. 斐波那契（第 8.3 节）
2. IsNat（第 8.3 节）
3. 感应式（第 10.5 节）

Z3在上述所有示例中都超时。但是，本教程似乎暗示只有归纳是非终止的。

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

Answer 1

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

Z3 在这些示例上失败的原因有两个：

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

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

虽然这些项目都在我的 TODO 清单上，但我今年不会开始研究它们。