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.
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00
|(PLDI 2021) DreamCoder: Bootstrapping inductive program synthesis with wake-sleep library learning
Kevin Ellis Cornell University, Lionel Wong Massachusetts Institute of Technology, Maxwell Nye Massachusetts Institute of Technology, Mathias Sablé-Meyer PSL University; Collège de France; NeuroSpin, Lucas Morales Massachusetts Institute of Technology, Luke Hewitt Massachusetts Institute of Technology, Luc Cary Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Joshua B. Tenenbaum MIT
|(POPL 2021) egg: Fast and Extensible Equality Saturation
|(POPL 2022) Relational E-Matching
|(OOPSLA 2020) Just-in-Time Learning for Bottom-up Enumerative Synthesis