5 releases (3 breaking)
| 0.4.0 | Jan 11, 2022 |
|---|---|
| 0.3.0 | Jan 5, 2022 |
| 0.2.0 | Jan 4, 2022 |
| 0.1.1 | Jan 3, 2022 |
| 0.1.0 | Jan 3, 2022 |
#2305 in Data structures
80KB
1.5K
SLoC
congruence
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.
lib.rs:
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.
Dependencies
~1MB
~17K SLoC