Z3 可以检查包含递归函数的公式的可满足性吗? [英] Can Z3 check the satisfiability of formulas that contain recursive functions?

问题描述

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

I'm trying out some of the examples of a Z3 tutorial that involve recursive functions. I've tried out the following example.

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

1. Fibonacci (Section 8.3)
2. IsNat (Section 8.3)
3. Inductive (Section 10.5)

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

Z3 times out on all of the above examples. But, the tutorial seems to imply that only Inductive is non-terminating.

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

Can Z3 check the satisfiability of formulas that contain recursive functions or it cannot handle any inductive facts?

推荐答案

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

These examples from the Z3 tutorial are there to illustrate limitations of the technology behind Z3.

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

Z3 fails on these examples for two reasons:

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

1. The models produced by Z3 assign an interpretation for each uninterpreted function symbol. The models can be viewed as functional programs. The current version does not produce recursive definitions. The first example is satisfiable, but Z3 fails to produce an interpretation for fib because it does not support recursive definitions. We have plans to extend Z3 in this direction.

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

Z3 does not support proofs by induction. Examples 2 and 3 are unsatisfiable, but Z3 fails because it does not support proof by induction. We also have plans to add basic support for that.

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

Although these items are on my TODO list, I will not start working on them this year.

这篇关于Z3 可以检查包含递归函数的公式的可满足性吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！