同余闭包算法

普通等式闭包只做自反、对称和传递；函数同余还要求“相等参数可代入同一函数”。若先知道 $a=b$，那么即便输入没有写 $f(a)=f(b)$，任何函数解释都必须让二者相等。参数类合并像改变了函数应用的地址：原本不同的两个 signature 可能突然重合，于是父节点也要合并，并继续向更外层传播。

函数是 uninterpreted，表示求解器不能使用单调性、线性或可逆性。它只保留所有函数都必须满足的确定性与同余性。这种克制使算法适用于程序中的抽象库调用，也明确标出它无法证明的领域性质。

考虑

前两个等式先得到类 $[a]=[b]=[c]$。因此

同余规则合并 $f(a),f(c)$；输入 $f(a)=d$ 又把 $d$ 并入该类，最终得到 $f(c)\equiv d$，与最后一个 disequality 冲突。一个可检查 explanation 恰可引用 $a=b,b=c,f(a)=d$ 与函数同余，说明不等式为何不可能成立。

边界也可在反方向看清。$f(a)=f(b)$ 不推出 $a=b$，因为未解释函数可以不是单射；没有写 $a\ne b$ 时，两个不同常元符号也允许解释成同一元素，EUF 没有默认 unique-name assumption。输入 $a\ne b$ 与 $f(a)=f(b)$ 完全可满足，例如取常值函数。量词公式、函数外延性或代数公理都超出纯地面 congruence closure。

并查集公理库并查集Disjoint-set union · Union-find维护不交集合划分并支持合并与代表元查询的数据结构。适合维护不断合并的等价类，但它本身不知道 term DAG 和函数 signature。把 DSU 的 $O(\alpha (n))$ 摊还界直接写成完整同余闭包复杂度会漏掉父应用重检、哈希表与 explanation 维护；精确界必须指定 Nelson–Oppen、Downey–Sethi–Tarjan 或后续哪一种实现。

判定的“没有冲突就可满足”也需要理由。可把最终等价类作为模型元素，对已出现的应用规定 $f([t_1],\dots ,[t_k])=[f(t_1,\dots ,t_k)]$。同签名项已被合并，所以这一定义不会对同一输入给出两个不同输出；没有出现的参数组合可任意补全。输入等式因此成立，而未被合并的不等式两端保持不同，这就构造出了模型；空输入可另取任意单元素模型。

在 SMT 中，当前 trail 新增等式会增量触发合并；新增 disequality 若落在同一类中就产生 theory conflict。若 Boolean 层已登记原子 $f(a)=f(b)$，参数类合并还可把它作为 theory propagation 返回。回溯要求撤销合并或使用分层持久状态，普通路径压缩 DSU 不能直接无日志回滚。

EUF 常用于把复杂函数暂时抽象为纯函数符号。若验证目标依赖库函数的单调性、内存副作用或异常行为，必须另加公理或更精确模型；否则 SAT 模型可能选择任意符合同余性的函数。Nelson–Oppen 组合可让 EUF 与算术 theory solver 通过共享等式协作，但组合正确性还需要签名互不相交和稳定无限等额外条件。