A semi-persistent equality saturation engine in Rust, with O(1) snapshots and O(k) restore across all core data structures.
Three contributions:
-
Pervasive semi-persistence — every data structure is built from a single semi-persistent vector primitive with a diff-log protocol. Mark/restore composes automatically across the union-find, node stores, hash-cons caches, and registries. Enables embedding equality saturation inside backtracking search (SAT, SMT, constraint propagation).
-
Native A/AC/ACI theories with leapfrog matching — associative, commutative, and idempotent operators are handled structurally through canonical representations (sorted multisets for AC, sorted sets for ACI, sequences for A), not rewrite rules. Pattern matching extends leapfrog triejoin with maximum partition semantics: branching is over distinct elements, not multiplicities, avoiding exponential blowup.
-
Proof logging with compile-time opt-out — a dual-parent-pointer union-find with copy-on-first-re-canonization preserves original node structure for proof reconstruction. Euler-tour LCA enables O(n) preprocessing, O(1)-per-query batch extraction. A
const PROOFS: boolgeneric eliminates all proof machinery at compile time when not needed.
Both semi-persistence (const TRACK: bool) and proof logging (const PROOFS: bool) are compile-time opt-out with zero residual overhead when disabled.
| Crate | Description |
|---|---|
semi-persistent |
CLI front-end and integration surface for the engine. |
containers |
Semi-persistent core data structures: Vec, Map, BPlusTreeSet, SparseSet, ListArena, bitsets, dense-id utilities. All support O(1) snapshots and O(k) restore. (design docs) |
egraph |
Equality saturation engine: e-graphs, e-matching, rewrite scheduling, term extraction, proofs. (design docs) |
traversals |
Arena-based recursion schemes. Stack-safe folds, unfolds, transforms, zippers. Includes traversals-derive proc-macro. (tutorial) |
abstract-domains |
Verified bitvector abstract domains (Tnums, Anums, Unums, Intervals, reduced products). 754 Verus proofs, 0 admits. Built separately from the default workflow. |
# Build all crates (except abstract-domains)
cargo build
# Run all tests (except abstract-domains)
cargo test --workspace --exclude semi-persistent-abstract-domains
# abstract-domains is verified with Verus and built separately
cd abstract-domains && cargo verus verify- Correctness first: proofs and tests before optimization.
- Zero-overhead abstractions: pool indices, not heap allocations, on hot paths.
CopyoverClonefor all pool-index and bitfield types. - Semi-persistence as the unifying mechanism: the same generational protocol that yields O(1) snapshots also supplies stratum boundaries for stratified negation and rollback for exploratory search.
See CONTRIBUTING for more information.
This project is licensed under the Apache-2.0 License.