An implementation of congruence closure, CongruenceClosure
, which drives modifications to an arbitrary union-find ADT implementing the UnionFind
trait.
Based on Nieuwenhuis and Oliveras Proof-producing Congruence Closure, except without the proof production.
A minimal disjoint set forest implementation with dense usize
nodes, DisjointSetForest
, is also provided.