Z3 可以检查有界数据结构上的递归函数的可满足性吗？
我知道Z3无法检查包含递归函数的公式的可满足性。但是，我想知道 Z3 是否可以处理这样的公式有界数据结构。例如，我在 我的 Z3 程序 和一个函数中定义了一个长度最多为 2 的列表，称为last，返回列表的最后一个元素。但是，当要求检查包含 last 的公式的可满足性时，Z3 不会终止。
有没有办法在 Z3 中使用有界列表上的递归函数？
I know that Z3 cannot check the satisfiability of formulas that contain recursive functions. But, I wonder if Z3 can handle such formulas over bounded data structures. For example, I've defined a list of length at most two in my Z3 program and a function, called last, to return the last element of the list. However, Z3 does not terminate when asked to check the satisfiability of a formula that contains last.
Is there a way to use recursive functions over bounded lists in Z3?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
（请注意，这也与您的其他问题相关。）我们将此类案例作为 Leon 验证程序项目。我们正在做的是避免使用量词，而是“展开”递归函数定义：如果我们在公式中看到术语 length(lst)，我们通过引入新的等式，使用长度的定义来扩展它： length( lst) = if(isNil(lst)) 0 else 1 + 长度(tail(lst))。您可以将此视为手动量词实例化过程。
如果您对长度最多为两个的列表感兴趣，请对所有术语进行手动实例化，然后对新列表术语再次执行一次就足够了，只要添加术语：
isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst))))
对于每个列表。在实践中，您当然不想手动生成这些等式和含义；在我们的例子中，我们编写一个程序本质上是围绕 Z3 的循环，在需要时添加更多这样的公理。
一个非常有趣的属性（与您的问题非常相关）是，事实证明，对于某些函数（例如长度），使用连续展开将为您提供完整的结果。决定即，即使您不限制数据结构的大小，您最终也可以得出 SAT 或 UNSAT 的结论（对于无量词的情况），
您可以在我们的论文 可满足性模递归程序，或者我很乐意在这里提供更多。
(Note that this related to your other question as well.) We looked at such cases as part of the Leon verifier project. What we are doing there is avoiding the use of quantifiers and instead "unrolling" the recursive function definitions: if we see the term length(lst) in the formula, we expand it using the definition of length by introducing a new equality: length(lst) = if(isNil(lst)) 0 else 1 + length(tail(lst)). You can view this as a manual quantifier instantiation procedure.
If you're interested in lists of length at most two, doing the manual instantiation for all terms, then doing it once more for the new list terms should be enough, as long as you add the term:
isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst))))
for each list. In practice you of course don't want to generate these equalities and implications manually; in our case, we wrote a program that is essentially a loop around Z3 adding more such axioms when needed.
A very interesting property (very related to your question) is that it turns out that for some functions (such as length), using successive unrollings will give you a complete decision procedure. Ie. even if you don't constrain the size of the datastructures, you will eventually be able to conclude SAT or UNSAT (for the quantifier-free case).
You can find more details in our paper Satisfiability Modulo Recursive Programs, or I'm happy to give more here.
您可能对 Erik Reeber 在 SULFA 上的工作感兴趣，SULFA 是“ACL2 中可展开列表公式的子类”。他在他的博士论文中展示了如何通过展开函数定义并应用来证明一大类面向列表的公式基于 SAT 的方法。他使用这些方法证明了 SULFA 类的可判定性。
参见，例如，http://www.cs.utexas.edu/~reeber /IJCAR-2006.pdf 。
You may be interested in the work of Erik Reeber on SULFA, the ``Subclass of Unrollable List Formulas in ACL2.'' He showed in his PhD thesis how a large class of list-oriented formulas can be proven by unrolling function definitions and applying SAT-based methods. He proved decidability for the SULFA class using these methods.
See, e.g., http://www.cs.utexas.edu/~reeber/IJCAR-2006.pdf .