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 学成子句；组合方法决定哪些交换足以保证全局模型存在。

在单一共享 sort、共有 $n$ 个变量的最坏情形中，完整 arrangement 对应它们的集合划分，数量是 Bell 数；其最坏增长为 $2^{\mathrm{\Theta }(n\log n)}$。上界可把每个变量映到至多 $n$ 个块标号来估计；下界仅数偶数个变量的两两配对划分，就已有 $n!/(2^{n/2}(n/2)!)$ 种。逐对记录等式的接口虽只有 $O(n^2)$ 对，枚举全部相容划分仍可能成为主要开销。固定多 sort 时只枚举各 sort 内的划分，数量为对应 Bell 数的乘积，不超过同规模单 sort 的界。Convexity、equality propagation 和延迟分裂能减少枚举，却没有让任意组合自动高效。实现或教材在声称“可组合”时应同时列出签名、sort、稳定无限、convexity 与各组件判定完备性，而不是只列 solver 名称。