Z3 (和其他求解者)总是在可能的情况下使用终止决策过程吗？

Question

我正在学习决策程序，另一方面，我也在学习Z3。具体来说，我正在研究一阶阵列理论中不同的可判定碎片.

例如，第1篇文章给出了一个数组的∃∗∀∗片段，我们可以证明它的属性:例如，∀i . 0 ≤ i < n → a[i+1] = a[i]−1。然而，通过定义一种新的带计数器的Büchi自动机类，他们按照自动机理论方法建立了这种逻辑的可判定性。对于我来说，这听起来远不是我所理解的SMT求解器作为可判定理论与量词的决策过程所实现的经典量词消除。

因此，我的问题是:如果一个理论可以像第1篇那样被证明是可判定的，那么Z3 (和其他求解者)是否实现了这些决策过程？换句话说，∀i . 0 ≤ i < n → a[i+1] = a[i]−1查询是用Z3中的终止决策过程来决定的，还是使用了更高效、但却是半可判定的启发式方法？如果他们使用终止过程，Z3 (和其他部分)如何识别可判定的片段？也许用正式语法来识别语言？

1关于整数数组还有什么可判定的？https://hal.archives-ouvertes.fr/hal-01418914/document

Answer 1

与任何大型软件一样，z3是多年来实现的一系列算法的集合。因此，很难确定具体实现了哪些算法以及它们是如何交互的；特别是考虑到它也在积极地开发。所以，要用任何权威来回答你的问题，你必须问实际的开发人员。https://github.com/Z3Prover/z3/discussions是这方面的最佳论坛；堆栈溢出不太可能给您带来满意的答案。

另一件事是查看源代码本身。因为它是开源的，所以您可以自己看看它是如何构造的。虽然这不适合随意的终端用户，但听起来您的兴趣更深了；所以您最好更熟悉整个过程是如何构建的。

我个人的看法是，它和其他软件项目一样。强调的是正确性，其目标(但必须是目标)的完整性。在工业中遇到的实际问题上做好工作，比执行一个在绩效方面表现糟糕的理论决策过程更重要。(因此，这就是启发发挥作用的地方。识别和重写模式，希望能够达到unsat结果。位向量理论就是一个很好的例子:简单地将比特爆炸并将其抛给SAT求解器，但是z3真的非常努力地重写和执行其他“魔术”，以便能够驯服计算复杂性；取得不同程度的成功。)但所有这一切都是“厨房”的一面。要获得精确的答案，请尝试Z3-讨论论坛，希望实际的开发人员能给您一个更准确的答案。