z3 - Z3 可以检查递归函数在有界数据结构上的可满足性吗？

Question

我知道Z3 cannot check the satisfiability of formulas that contain recursive functions .但是，我想知道是否 Z3可以在有界数据结构上处理此类公式。例如，我在 my Z3 program 中定义了一个长度最多为 2 的列表。和一个名为 last 的函数, 返回列表的最后一个元素。但是，当被要求检查包含 last 的公式的可满足性时，Z3 不会终止。 .

有没有办法在 Z3 中的有界列表上使用递归函数？

Answer 1

(请注意，这也与您的其他问题有关。)我们将此类案例视为 Leon verifier 的一部分。项目。我们在那里做的是避免使用量词，而是“展开”递归函数定义:如果我们在公式中看到术语长度(lst)，我们通过引入一个新的等式来使用长度的定义来扩展它:length( lst) = if(isNil(lst)) 0 else 1 + length(tail(lst))。您可以将此视为手动量词实例化过程。

如果您对长度最多为两个的列表感兴趣，则对所有术语进行手动实例化，然后对新列表术语再做一次就足够了，只要您添加术语:

isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst))))

对于每个列表。在实践中，您当然不想手动生成这些等式和含义；在我们的例子中，我们编写了一个程序，它本质上是一个围绕 Z3 的循环，在需要时添加更多这样的公理。

一个非常有趣的属性(与您的问题非常相关)是，对于某些函数(例如长度)，使用连续展开将为您提供完整的决策程序。 IE。即使您不限制数据结构的大小，您最终也将能够得出 SAT 或 UNSAT(对于无量词的情况)。

您可以在我们的论文 Satisfiability Modulo Recursive Programs 中找到更多详细信息，或者我很乐意在这里提供更多。