egg: Fast and Extensible Equality Saturation
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites.
This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation’s distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation.
We implemented these techniques in a new open-source library called
egg. Our case studies on three previously published applications of equality saturation highlight how
egg’s performance and flexibility enable state-of-the-art results across diverse domains.
Fri 22 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:00
|Cyclic Proofs, System T, and the Power of Contraction|
Denis Kuperberg LIP, ENS de Lyon, Laureline Pinault LIP, ENS de Lyon, Damien Pous CNRSLink to publication DOI
|egg: Fast and Extensible Equality SaturationDistinguished Paper|
Max Willsey University of Washington, USA, Chandrakana Nandi University of Washington, USA, Yisu Remy Wang University of Washington, Oliver Flatt University of Utah, Zachary Tatlock University of Washington, Seattle, Pavel Panchekha University of UtahLink to publication DOI Pre-print
|Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS|
David Zhao The University of Sydney, Pavle Subotic Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard Scholz University of Sydney, AustraliaLink to publication DOI