Z3处理带量词公理的流程及相关技术疑问与代码阅读求助

我阅读了相关书籍和Z3官方教程的部分内容，希望了解Z3处理带量词公式的具体方式。目前已知相关资料均提到：带量词公式中（一阶逻辑内有值的）项会被映射到*E-graph（等价类）*中的现有项来完成实例化。

我有两个核心疑问：

• 若E-graph为空（即所有公式均为带量词公式），该如何处理？
• 一阶公式集的可满足性需要尝试所有可能的模型，而这类模型实际上是无限的，Z3如何应对这一问题？

我自己梳理了一套逻辑，不确定是否正确、是否是Z3的实际实现方式：

核心处理步骤 #

1. 对所有函数执行斯科伦化，消除现有量词，将所有带量词公式转换为$\forall x_1,...,x_n \phi(x_1,...,x_n)$的形式
2. 将公式中所有非量化变量视为新的常量符号；若不存在此类变量，则实例化1个新的常量符号
3. 应用匹配过程将变量与这些新常量符号匹配，更新E-graph，并持续实例化直至发现冲突或确定可满足性

可满足性判定结论 #

若确定公式集可满足：

• 所有变量均由常量符号实例化，因此采用与常量符号对应的模型即可
• 通过斯科伦化步骤和E-graph，可构建出满足公式的有限模型，由此判定公式集可满足

冲突出现时的结论 #

若实例化过程中出现冲突：

• 由于实例化对应常量扩展符号，所有用常量符号替换的操作均可通过一阶定理中的全局特化公理证明，因此冲突真实存在
• 结合上述步骤与哥德尔完备性定理，可判定该公式集无法被任何模型满足

我注意到Z3在处理需要无限常量实例化的公式（比如皮亚诺算术公理）时会进入循环，这似乎能印证上述逻辑，但仍不确定正确性。另外，Z3的代码阅读难度极高，我找不到处理逻辑的线索，希望能获得Z3代码阅读的相关帮助。

内容的提问来源于stack exchange，提问作者Shore