我正在研究决策过程，另一方面，我也在研究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
与任何一款大型软件一样，z3是多年来实现的一系列算法的集合。因此，很难确定具体实现了什么算法以及它们是如何交互的；特别是考虑到它也在积极开发中。因此，要想以任何权威人士的身份回答您的问题，您必须询问实际的开发人员。https://github.com/Z3Prover/z3/discussions是最好的论坛；堆栈溢出不太可能为您提供满意的答案。
要做的另一件事是查看源代码本身。由于它是开源的，您可以亲眼看到它是如何构建的。虽然这不适合普通的最终用户，但听起来你的兴趣更深了；所以你不妨更熟悉整个东西是如何构建的。
我个人的观点是，它和其他软件项目一样。重点是正确性，目标(但必须是目标(是完整性。处理好业内人士遇到的实际问题比实施一个在绩效方面表现不佳的理论决策程序更重要。(因此，这就是启发式发挥作用的地方。识别和重写模式，希望达到unsat的结果。比特向量理论就是一个很好的例子：只需比特爆炸并将其扔给SAT求解器很容易，但z3非常努力地重写并做其他"魔术"，这样计算复杂性就可以得到控制，并取得不同程度的成功。(。)但所有这些都是"；厨房；事情的一面。要获得准确的答案，请尝试z3讨论论坛，希望其中一位真正的开发人员能给你一个更准确的答案。