我知道Z3 无法检查包含递归函数的公式的可满足性。但是，我想知道Z3是否可以在有界数据结构上处理此类公式。例如，我在Z3 程序中定义了一个长度最多为 2 的列表和一个名为 的函数，last用于返回列表的最后一个元素。但是，当要求检查包含 的公式的可满足性时，Z3 不会终止last。
有没有办法在 Z3 的有界列表上使用递归函数？
问问题
1351 次
2 回答
3
（请注意，这也与您的其他问题有关。）我们将此类案例视为Leon 验证程序项目的一部分。我们在那里所做的是避免使用量词，而是“展开”递归函数定义：如果我们在公式中看到术语长度（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中找到更多详细信息，或者我很乐意在这里提供更多信息。
于 2011-08-16T11:27:42.060 回答
2
您可能对 Erik Reeber 在 SULFA 上的工作感兴趣，“ACL2 中不可滚动列表公式的子类”。他在博士论文中展示了如何通过展开函数定义和应用来证明一大类面向列表的公式基于SAT的方法。他使用这些方法证明了 SULFA 类的可判定性。
于 2011-08-20T01:17:24.563 回答