Omelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
summary
Claims that bottom-up e-matching plus semantic eids lets e-graphs incorporate domain theories by canonicalizing terms before matching, avoiding combinatorial explosion from AC or linear arithmetic; implementation builds substitutions by enumerating variable bindings from the term bank, canonizing (e.g., row‑echelon for linear, Groebner for polynomials, group-labeled unions for offsets, SMT sweeping for hard equalities) and then checking membership; prototype knuckle dragger exists and demonstrates feasibility, with tradeoffs (exponential cost in number of pattern variables vs. infinite theory factors for top‑down) but no full benchmarking yet.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 2:25E-graphs modulo theories
- 7:18Term banks and smart constructors
- 11:48Bottom-up e-matching
- 18:48Structured eids for canonization
- 29:22Advanced structured eids and related work
- 33:36Future directions
related talks
18mAssociativity and Commutativity in Equality Saturation
23mE-graphs modulo theories
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
25mLifting E-Graphs: A Function Isn’t a Constant
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
20mEquality Saturation and Joins
37mEquivalence Hypergraphs: E-Graphs for Monoidal Theories
15mEquality Saturation Theory Exploration à la Carte