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

Question

我正在尝试一些涉及递归函数的Z3教程的例子.我试过以下例子.

1. 斐波纳契(第8.3节)
2. IsNat(第8.3节)
3. 归纳法(第10.5节)

Z3超过了上述所有示例.但是,该教程似乎意味着只有Inductive是非终结的.

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

Answer 1

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

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

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

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

虽然这些项目在我的TODO列表中,但我今年不会开始研究这些项目.