A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching.
summary
Describes an equality saturation engine built on a single vector primitive with O(1) snapshots and O(k) restore enabling backtracking inside search, native AC/A/ACI support via canonized representations and an extension of leapfrog triejoin to multiset matching using maximum partition semantics, proof logging by copy-on-first-re-canonization plus Euler-tour LCA for batch O(1) extractions, implemented in Rust with Verus verification of low-level structures, open-sourced, and an initial claim of ~30% faster pattern matching than egglog.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:19Semi-persistence foundation
- 6:49Native AC support
- 11:00Variadic AC nodes
- 12:27Leapfrog AC matching
- 17:25AC matching in VM
- 19:12Batch proof extraction
- 20:36Conclusion
- 22:02Q&A
related talks
30megg: Fast and Extensible Equality Saturation
20mEquality Saturation and Joins
23mVersioned E-Graphs
24mIncremental Equality Saturation
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
22mOatlog: A performant ahead-of-time compiled e-graph engine
17mBetter Together: Unifying Datalog and Equality Saturation
19mTowards Relational Contextual Equality Saturation