Congruence closure

also: uninterpreted functions, euf

The decision procedure for equality over uninterpreted functions: union-find plus the rule that equal arguments give equal applications. Merging two classes can therefore force their parents to merge, so the closure is computed by re-examining parents until nothing changes.

Equality alone is a union-find. What makes it a theory is one extra rule, which says that a function applied to equal arguments produces equal results:

\frac{a _{1} = b _{1} \dots a _{n} = b _{n}}{f ( a _{1} , \dots , a _{n} ) = f ( b _{1} , \dots , b _{n} )}

So a merge is not local. Making $a$ and $b$ equal can make $f (a)$ and $f (b)$ equal, which can in turn make $g (f (a))$ and $g (f (b))$ equal, and so on. The closure is computed by re-examining the parents of every merged class until nothing changes.

f(a) and f(b) become equal only after a = b is asserted, with no rule mentioning f. Compiled with ocamlopt 4.14.1.

before: f(a) = f(b) ? false
assert a = b, then congruence
after:  f(a) = f(b) ? true

A disequality is a conflict exactly when its two sides end up with the same representative, and the explanation a DPLL(T) core wants is the set of asserted equalities along the path that merged them, which is why implementations keep a proof forest rather than a bare union-find.

Uninterpreted means the solver knows nothing about $f$ except that it is a function. That is weak on purpose: it is decidable in near-linear time, and it is the theory every other one is combined with.