Destructive E-Graph Rewrites
summary
Implements destructive rewrites in egg by e‑matching each rule left hand side and deleting matching right hand side enodes rather than adding them, requiring rules that forbid removing the last enode of an eclass and preserving at least one grounded eclass. Disables explanations and pruning for fair comparison. Benchmarks on the math test suite show up to 3x speedups and one case with orders of magnitude improvement, solves workloads that previously hit the e‑node limit, but accuracy varies and results are mixed when compared to pruning.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:24Exploding egraphs problem
- 3:31Limiting egraph size strategies
- 5:57Destructive rewrites concept
- 7:41Rules and limitations
- 9:27Experimental results
- 10:54Next steps and challenges
- 12:54Herby project application
- 13:41Future work and explanation
- 14:06Q&A
related talks
22mFrom Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs
30megg: Fast and Extensible Equality Saturation
23mVersioned E-Graphs
25mEGSTRA: E-Graph-Based Strategy for Test Suite Reduction and Abstraction
38mE-graphs and Automated Reasoning: Looking back to look forward
25mDisequalities in E-Graphs: An Experiment
23mSlotted E-Graphs
14mRewrite Rule Inference Using Equality Saturation