Rewrite Rule Inference Using Equality Saturation
summary
Describes a system called Ruler that uses equality saturation over e-graphs to infer rewrite rules automatically, implemented in Rust on the egg library. Claims Ruler synthesizes 5.8× smaller rulesets and runs 25× faster than a CVC4-based tool, with 0.98 derivability (98% of CVC4’s 1,782 rules derivable from Ruler’s 188). Shows Ruler finds missing Herbie rational rules, integrates with Herbie without losing accuracy, and exposes unsound rules via e-graph merges.
AI-written summary · about
chapters (16)
- 0:00Rewrite Rule Inference Using Equality Saturation
- 0:49A 3-Step Approach for Inferring Rewrite Rules
- 2:16What is Equality Saturation?
- 3:16Equality Saturation Mitigates Phase Ordering!
- 3:38How Does Equality Saturation Work?
- 4:25Equality Saturation for Inferring Rewrite Rules
- 4:54Enumeration Modulo Equality Saturation
- 6:23Candidate Generation by Characteristic Vector Matching
- 7:37Rule Selection with Equality Saturation
- 9:10Ruler
- 10:26Implementation
- 10:45Comparison with CVC4
- 12:02Comparison with Human-written Rules
- 13:14End-to-End: Rational Herbie
- 13:35Rational Herbie: Comparing Accuracy
- 13:48Rational Herbie: Comparing AST Size
related talks
27mAugmenting Rewrite Rule Sets via Knuth-Bendix Completion
28mCERES: Making Equality Saturation Memory-Scalable
30megg: Fast and Extensible Equality Saturation
17mBetter Together: Unifying Datalog and Equality Saturation
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
26mEquality Saturation Guided by Large Language Models
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
19mDestructive E-Graph Rewrites