给定代码场景下Z3为何MBQI可实例化nil-cons量词而e匹配无法生效？

触发逻辑的核心差异 #

• e匹配并不是“上下文存在可匹配项就自动执行”的无差别匹配机制，它是高度依赖求解器内部流程的惰性触发逻辑，运行行为受参数配置的严格控制。
• 你设置了auto-config false之后，Z3不会自动为e匹配引擎开启初始全量扫描流程。默认开启自动配置时，Z3会在预处理完所有初始断言后，主动遍历所有已存在的ground项，和已注册的量词模式做匹配；但关闭自动配置后，e匹配只会在核心推理流程推进的节点（比如等价类合并、冲突检测、子句传播）才会被动扫描当前项数据库里的活跃项。
• 对应到这个案例，求解器接收完所有初始断言后，没有检测到任何逻辑冲突，也没有需要分解传播的复杂约束，整个推理流程不会进入需要触发e匹配扫描的节点。尽管cons(global_x global_xs)在语法上完全匹配nil-cons的指定模式，但这个ground项从来没有被e匹配引擎遍历到，自然不会触发量词实例化，最终因为没有足够推理步骤推出矛盾，返回unknown。
• 可以通过简单操作验证这个逻辑：在现有代码的check-sat之前加一句断言(assert (= (cons global_x global_xs) (cons global_x global_xs)))，把cons构造的项作为独立的活跃项显式注册到求解器的项数据库中，此时就算保持auto-config false、关闭MBQI，e匹配也会正常触发实例化，最终返回unsat。

开启MBQI后正常求解的原因 #

• MBQI（基于模型的量词实例化）的工作逻辑和e匹配完全不同：它不会被动等待推理流程触发扫描，而是在每个求解阶段主动构建候选抽象模型，遍历模型中所有的ground项和量词做匹配。这个流程不受e匹配的惰性触发逻辑限制，因此不管自动配置开不开，都能主动识别到可匹配的cons项，实例化nil-cons公理后和末尾的等式断言产生直接矛盾，最终返回unsat。

常见认知误区 #

• 不少使用者会把e匹配的触发条件理解为“模式和ground项存在语法合一关系就一定触发”，但实际上Z3的e匹配带有非常细粒度的成本控制、触发时机控制，尤其是在关闭自动配置的场景下，很多默认的主动扫描、项索引优化逻辑都不会生效，运行行为和直观预期存在差异是很常见的情况。

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