Nelson–Oppen 理论组合

两个 theory solvers 不交换内部公式，只协商“这些共同对象是否相等”。Purification 把跨理论嵌套拆成命名接口；arrangement 则像一份双方必须接受的共享对象身份证明。若某一方推出新等式，另一方把它当输入继续检查，直至冲突或达到共同一致。

稳定无限不是技术装饰。局部 solver 可能各自有模型，却分别被迫使用不同有限论域大小，导致无法粘合；允许把可满足模型扩成无限论域，便消除了这种纯基数冲突。签名互不相交同样关键：若两个 solver 同时给同一函数符号不同解释，仅交换等式不足以协调它们。

组合 EUF 与线性实数算术，考察

算术部分由LRA theory solver公理库线性实数算术 SMT 的单纯形算法LRA SMT simplex algorithm · Simplex for linear real arithmetic · SMT simplex维护线性 tableau 与变量界以增量判定 LRA 文字合取可行性，并生成理论冲突解释。推出共享等式 $x=y$。把它交给 EUF 后，同余闭包公理库同余闭包算法Congruence closure algorithm · EUF congruence closure计算地面项等式生成的最小函数同余，并以此判定 EUF 等式与不等式合取是否一致。推出 $f(x)=f(y)$，与输入 disequality 冲突。两侧原本各自可满足：LRA 可取 $x=y=0$，EUF 在未获知 $x=y$ 时可把 $x,y$ 解释为不同元素；正是等式交换暴露了组合矛盾。

若组件理论是 convex 的，即

必然意味着其中某个单独等式已由 $T\cup \mathrm{\Gamma }$ 蕴涵，那么反复传播必然等式即可。非 convex 理论可能只推出一个等式析取，却不推出任何单项；此时必须让 Boolean 层 case split 或枚举 arrangements，不能任意挑一个等式传播。

定宽位向量理论只有有限论域，通常不满足稳定无限；含共享非逻辑函数的理论也违反 signature-disjoint 假设。许多实用求解器有专门组合、bit-blasting 或 delayed theory combination 来处理这些情形，但它们不是原始定理的无条件实例。多 sort 场景还要逐个共享 sort 核对稳定无限性，不能只说“理论总体无限”。

Nelson–Oppen 为模块化 SMT 提供清晰边界：EUF、LRA、数组等组件可各自维护高效专用状态，只需通过共享等式协调。DPLL(T) 可把 arrangement 分支与 equality propagation 交给 Boolean 层，并把局部 theory conflicts 学成子句；组合方法决定哪些交换足以保证全局模型存在。

复杂度可能由共享变量对数主导，因为完整 arrangement 数量呈指数增长。Convexity、equality propagation 和延迟分裂能减少枚举，却没有让任意组合自动高效。实现或教材在声称“可组合”时应同时列出签名、sort、稳定无限、convexity 与各组件判定完备性，而不是只列 solver 名称。