我知道Z3无法检查包含递归函数的公式的可满足性.但是,我想知道Z3是否可以在有界数据结构上处理这样的公式.例如,我在我的Z3程序中定义了一个长度最多为2的列表,并且调用了一个函数last来返回列表的最后一个元素.但是,当要求检查包含的公式的可满足性时,Z3不会终止last.
有没有办法在Z3中使用有界列表上的递归函数？
（请注意，这也与您的其他问题有关。）我们将此类案例作为Leon 验证程序项目的一部分进行了研究。我们正在做的是避免使用量词，而是“展开”递归函数定义：如果我们在公式中看到术语 length(lst)，我们会通过引入新的等式，使用长度的定义来扩展它： length( lst) = if(isNil(lst)) 0 else 1 + 长度(tail(lst))。您可以将此视为手动量词实例化过程。
如果您对长度最多为两个的列表感兴趣，请对所有术语进行手动实例化，然后对新列表术语再次进行操作就足够了，只要添加术语即可：
isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst))))
对于每个列表。在实践中，您当然不想手动生成这些等式和含义；在我们的例子中，我们编写了一个程序，该程序本质上是围绕 Z3 的循环，并在需要时添加更多此类公理。
一个非常有趣的属性（与您的问题非常相关）是，事实证明，对于某些函数（例如长度），使用连续展开将为您提供完整的决策过程。IE。即使您不限制数据结构的大小，您最终也将能够得出 SAT 或 UNSAT 的结论（对于无量词的情况）。
您可以在我们的论文可满足性模递归程序中找到更多详细信息，或者我很乐意在这里提供更多信息。