eqsat: An Equality Saturation Dialect for Non-destructive Rewriting
summary
An MLIR-based e-graph representation called eqsat dialect encodes e-classes and e-nodes as MLIR ops and uses MLIR graph regions to express cycles so equality information stays inside the compiler IR. Pattern rewrites use the MLIR PDL rewriter to insert enodes, unioning relies on existing passes such as CSE rather than egg’s unionfind, and extraction is currently naive extraction that scans enodes for a best result. The prototype runs but lacks region-aware matching and valueless-op handling.
AI-written summary · about
chapters (8)
- 0:00eqsat introduction
- 1:37Compiler integration challenges
- 3:14MIR for egraphs
- 4:39Egraphs in MIR
- 7:51Union and rebuilding
- 9:19Rewrite rules in MIR
- 11:45Open questions
- 13:54Q&A
related talks
20mEquality Saturation and Joins
30megg: Fast and Extensible Equality Saturation
19mTowards Relational Contextual Equality Saturation
17mBetter Together: Unifying Datalog and Equality Saturation
21mImproving Equality Saturation for EDA via Semantic E-Graphs
24mOptimism in Equality Saturation
15mEquality Saturation Theory Exploration à la Carte
23mPerformant Dynamically Typed E-Graphs in Pure Julia