Z3可以检查包含递归函数的公式的可满足性吗？
我正在尝试 Z3 教程 中涉及递归函数的一些示例。我已经尝试过以下示例。
Z3 在上述所有示例中都会超时。但是，该教程似乎暗示只有 归纳 是非终止的。
Z3 可以检查包含递归函数的公式的可满足性吗？或者它不能处理任何归纳事实？
I'm trying out some of the examples of a Z3 tutorial that involve recursive functions. I've tried out the following example.
Z3 times out on all of the above examples. But, the tutorial seems to imply that only Inductive is non-terminating.
Can Z3 check the satisfiability of formulas that contain recursive functions or it cannot handle any inductive facts?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
Z3 教程中的这些示例旨在说明 Z3 背后的技术的局限性。
Z3 在这些示例中失败的原因有两个：
Z3 生成的模型为每个未解释的函数符号分配了解释。这些模型可以被视为功能程序。当前版本不产生递归定义。第一个示例是可满足的，但 Z3 无法生成 fib 的解释，因为它不支持递归定义。
我们计划朝这个方向扩展Z3。
Z3不支持归纳证明。例2和例3是不可满足的，但Z3失败了，因为它不支持归纳证明。
我们还计划为此添加基本支持。
虽然这些项目都在我的待办事项清单上，但我今年不会开始处理它们。
These examples from the Z3 tutorial are there to illustrate limitations of the technology behind Z3.
Z3 fails on these examples for two reasons:
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 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.
Although these items are on my TODO list, I will not start working on them this year.