使用 Z3 计算递归函数

Question

我想写一个函数来“计算”一个列表的长度。 http://rise4fun.com/Z3/Irsl1，基于list concat in z3 和Proving inductive facts in Z3。

我似乎无法让它工作，它因超时而失败。在 Z3 中可以表达这样的功能吗？

更大的背景是我正在尝试建模和解决诸如“有多少偶正整数小于 9？”或“有 5 个偶正整数小于 x，x 是多少？”之类的问题。

Answer 1

更大的背景是我正在尝试建模和解决诸如“有多少偶正整数小于 9？”或“有 5 个偶正整数小于 x，x 是多少？”之类的问题。

如果这是您真正想要解决的问题，那么我建议不要直接创建列表或推导式，而是仅使用算术对问题进行编码。 例如，你可以通过乘以 2 获得偶数，并表示 使用量词的整数区间的属性。

对于序列操作，有一些新兴选项。 例如，部分处理序列和长度：http://rise4fun.com/z3/tutorial/sequences。比较简单的属性 使用内置程序排出序列和长度。 如果您像上面暗示的那样开始编码属性，则不太可能 做得很好，因为主要支持是围绕地面（无量词）属性。