Reference. 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.
Cite
Cited by (2)
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale bolan-2025-the
We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.
Vectorization for digital signal processors via equality saturation vanhattum-2021-vectorization
Cites 32 works (0 here)
External (32)
- Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations (2020)
- Semantic Code Search via Equational Reasoning (2020)
- SPORES: Sum-Product Optimization via Relational Equality Saturation for Large Scale Linear Algebra (2020)
- Apache SystemML (2019)
- TASO: optimizing deep learning computation with automatic generation of graph substitutions (2019)
- Learning to Infer and Execute 3D Shape Programs (2019)
- InverseCSG: automatic conversion of 3D models to CSG trees (2018)
- Learning to Infer Graphics Programs from Hand-Drawn Images (2018)
- Functional Programming for Compiling and Decompiling Computer-aided Design (2018)
- CSGNet: Neural Shape Parser for Constructive Solid Geometry (2017)
- Automatically Improving Accuracy for Floating Point Expressions (2015)
- Equality-Based Translation Validator for LLVM (2011)
- Equality Saturation: A New Approach to Optimization (2009)
- Z3: An Efficient SMT Solver (2008)
- Efficient E-Matching for SMT Solvers (2007)
- Simplify: A Theorem Prover for Program Checking (2005)
- Proof-Producing Congruence Closure (2005)
- Denali: A Goal-directed Superoptimizer (2002)
- Compiling language definitions: the ASF+SDF compiler (2002)
- Graph Transformation for Specification and Programming (1999)
- Building Program Optimizers with Rewriting Strategies (1998)
- The TAMPR Program Transformation System: Simplifying the Development of Numerical Software (1996)
- A taste of rewrite systems (1993)
- Rewrite Systems (1990)
- Superoptimizer: A Look at the Smallest Program (1987)
- Variations on the Common Subexpression Problem (1980)
- Techniques for Program Verification (1980)
- Fast Decision Procedures Based on Congruence Closure (1980)
- Complexity of Finitely Presented Algebras (1977)
- Efficiency of a Good But Not Linear Set Union Algorithm (1975)
- A Computing Procedure for Quantification Theory (1960)
- Rust programming language