我知道Z3 cannot check the satisfiability of formulas that contain recursive functions。但是，我想知道Z3 是否可以在有界数据结构上处理此类公式。例如，我在my Z3 program 中定义了一个长度最多为2 的列表，以及一个名为last 的函数，用于返回列表的最后一个元素。但是，当要求检查包含 last 的公式的可满足性时，Z3 不会终止。
有没有办法在 Z3 的有界列表上使用递归函数？
【问题讨论】：
标签： z3
（请注意，这也与您的其他问题有关。）我们将此类案例视为Leon verifier 项目的一部分。我们在那里所做的是避免使用量词，而是“展开”递归函数定义：如果我们在公式中看到术语长度（lst），我们通过引入一个新的等式来使用长度的定义来扩展它：长度（ lst) = if(isNil(lst)) 0 否则 1 + 长度(tail(lst))。您可以将其视为手动量词实例化过程。
如果您对最多两个长度的列表感兴趣，则对所有术语进行手动实例化，然后为新的列表术语再做一次就足够了，只要您添加术语：
isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst)))))
对于每个列表。在实践中，您当然不想手动生成这些等式和含义；在我们的例子中，我们编写了一个程序，它本质上是一个围绕 Z3 的循环，在需要时添加更多这样的公理。
一个非常有趣的属性（与您的问题非常相关）是事实证明，对于某些函数（例如长度），使用连续展开将为您提供完整的决策过程。 IE。即使您不限制数据结构的大小，您最终也可以得出 SAT 或 UNSAT（对于无量词的情况）。
您可以在我们的论文Satisfiability Modulo Recursive Programs 中找到更多详细信息，或者我很乐意在这里提供更多信息。
【讨论】：
define-fun 宏工具定义 last。 Z3 会自动展开宏。以下链接包含有关如何执行此操作的示例：rise4fun.com/Z3/9xVs
您可能对 Erik Reeber 在 SULFA 上的工作感兴趣，“ACL2 中不可滚动列表公式的子类”。他在博士论文中展示了如何通过展开函数证明一大类面向列表的公式定义和应用基于 SAT 的方法。他使用这些方法证明了 SULFA 类的可判定性。
【讨论】：