模型和递归函数

Question

由于previously asked Z3不能提供递归函数的模型。然而，是否有可能告诉Z3（最好通过Java API）没有定义递归函数的模型是足够的（或者确实选择我感兴趣的函数，本质上我不需要非常量函数的模型） ？显然，这可能会导致查询返回，尽管某些函数没有模型。基本上，用户然后必须确保这些功能确实有一些模型。然而，我认为Z3或SMT解算器的工作方式并不是真正可以实现的，也就是说，我假设Z3需要递归函数的（部分）模型来评估表达式。

Answer 1

量词的MBQI实现并不能很好地处理递归函数。 有一件事可能会为你带来诀窍：用有界递归函数替换递归函数定义。您添加一个额外的参数来计算您愿意探索该函数的展开次数。每当您在输入的其余部分应用递归函数时，请设置深度参数。您可以使用代数数据类型的Peano数字或整数。例如，符号自动机工具包使用这种方法。

Answer 2

我发现了一篇论文，探讨了Nikolaj Bjorner的答案：Amin，Leino和Rompf（2014）的“用SMT解算器进行计算”。此外，我发现Suter，Köksal和Kuncak（2011）的“可满足模递归程序”，其中调用连续递归函数，直到可以决定可满足性为止。