egg: Fast and Extensible Equality Saturation

1 INTRODUCTION

• Equality saturation repeatedly applies pattern-based rewrites to represent equivalent programs, then extracts a best program using a user-provided cost function.Rewrites add information rather than removing earlier expressions; saturation or timeout precedes extraction.Source: §1 · p. 1
• Conventional e-graphs can be expensive as they grow, while integrating analyses beyond syntactic rewrites has required ad hoc extensions and repeated reimplementation.The paper identifies both challenges as limiting equality saturation’s practicality.Source: §1 · p. 1
• Equality saturation’s workload separates matching rewrites from merging their equivalences and does not require backtracking.These phases enable invariant restoration to be deferred.Source: §1 · p. 2
• Rebuilding defers e-graph invariant maintenance to equality-saturation phase boundaries without compromising soundness.It exploits equality saturation’s workload and provides asymptotic speedups over conventional approaches empirically.Source: §1 · p. 2
• E-class analyses integrate domain-specific facts into e-classes and let rewrites use those facts to establish further facts.The invariant relates analysis facts to represented terms; examples include constant folding and free-variable analysis.Source: §1 · p. 2
• egg packages rebuilding and e-class analyses in an open-source, reusable library parameterized by user-defined languages, rewrites, and cost functions.Its case studies demonstrate use across diverse domains.Source: §1 · p. 2
• egg’s case studies are orders of magnitude faster than previous implementations where comparisons exist, while offering more features.The applications cover deductive synthesis and optimization in floating-point accuracy, linear algebra, and CAD.Source: §1 · p. 2

2.1 E-graphs

• An e-graph stores terms and their congruence relation, organizing equivalent e-nodes into e-classes whose children refer to other e-classes.Its representation uses union-find, an e-class map, and hashconsing.Source: §2.1 · p. 3, §2.1.1 · p. 3

2.1.1 Definitions.

• The e-graph definitions distinguish equivalence over IDs, nodes, and terms, and define congruence closure as the smallest congruence-closed superset of node equivalence.A singleton-e-node e-class makes the graph essentially a term graph with sharing.Source: §2.1.1 · p. 4

2.1.2 E-graph Invariants.

• The e-graph invariants require congruent e-nodes to share an e-class and canonical e-nodes to be mapped by hashconsing.These invariants support correct and efficient operations.Source: §2.1.2 · p. 4

2.1.3 Interface and Rewriting.

• The interface adds e-nodes, merges e-classes, finds canonical IDs, and matches patterns so rewrites can add and merge equivalent expressions.Rewriting is additive: it preserves the initial term, and repeated application can reach saturation.Source: §2.1.3 · p. 5

2.2 Equality Saturation

• Equality saturation addresses destructive rewrite ordering by representing alternatives together in an e-graph, rather than naively storing every expression separately.Traditional rewriting forgets the matched expression, creating a phase-ordering problem; equality saturation applies rewrites while retaining alternatives.Source: §2.2 · p. 5
• Equality saturation initializes an e-graph, applies rewrite rules until saturation or timeout, then extracts a term optimal under a cost function.A greedy bottom-up traversal suffices for simple cost functions; more complex costs have other extraction procedures.Source: §2.2 · p. 5

2.3 Equality Saturation and Theorem Proving

• Equality saturation specializes optimization by extracting a cost-optimal term, while theorem provers such as SMT solvers support broader interpreted reasoning.For one TASO verification task, egg took 1.56 seconds versus Z3’s 24.65 seconds, or 0.52 seconds with batched evaluation.Source: §2.3 · p. 6

3 REBUILDING: A NEW TAKE ON E-GRAPH INVARIANT MAINTENANCE

• Rebuilding separates merge from invariant restoration, allowing clients to choose when to pay the maintenance cost.The client must rebuild at a time that improves performance without limiting the application.Source: §3 · p. 6, §3.3 · p. 9

3.1 Upward Merging

• Traditional upward merging repairs congruence during merges, while rebuilding queues possibly affected e-classes and restores invariants later.Repair canonicalizes parent e-nodes and merges congruent parents; deduplicating the worklist coalesces overlapping work.Source: §3.2 · pp. 7–8, §3.1 · p. 7

3.2 Rebuilding in Detail

• Rebuilding processes a deduplicated worklist in chunks, so e-classes made equivalent during repair are deduplicated before later processing.Merge adds affected classes to the worklist rather than immediately starting upward merging.Source: §3.2 · p. 7

3.2.1 Examples of Rebuilding.

• Deferred rebuilding reduces illustrative workloads from O(n^2) to O(n) hashcons updates and from O(wd) to O(d) repair calls.The second example merges w nested terms of depth d before rebuilding, eliminating the width factor in repair calls.Source: §3.2.1 · pp. 8–9

3.2.2 Proof of Congruence.

• Theorem 3.1 establishes that rebuilding restores congruence and terminates.The proof tracks incongruent node pairs and the worklist, which decrease lexicographically until both are empty.Source: §3.2.2 · p. 9

3.3 Rebuilding and Equality Saturation

• egg separates each iteration into read and write phases, then rebuilds once at the end, making results invariant to rewrite-list order.In the traditional algorithm, later rules can see earlier results within the same iteration; deferring rebuilding there can miss matches.Source: §3.3 · p. 10

3.4 Evaluating Rebuilding

• 88× faster congruence maintenance and 21× faster equality saturation were achieved in aggregate with deferred rebuilding.Figure 7 also shows the multiplicative speedup increasing with problem size.Source: Figure 6 · p. 11, Figure 7 · p. 11, §3.4 · p. 12

4 EXTENDING E-GRAPHS WITH E-CLASS ANALYSES

• E-class analyses replace ad hoc e-graph extensions with a general mechanism that lets rewrites use analysis facts and compactly analyze many similar programs.Analysis facts can modify the graph, inform rewrite applications, or determine extraction costs.Source: §4 · pp. 12–13

4.1 E-class Analyses

• An e-class analysis associates each class with domain data, using make for new nodes, join for merges, and optionally modify to change a class.The analysis domain and join operation form a join-semilattice.Source: §4.1 · p. 13

4.1.1 Maintaining the Analysis Invariant.

• Rebuilding restores the analysis invariant alongside congruence by recomputing parent data after merges and applying the idempotent modify hook.The implementation assumes a semilattice domain and idempotent modify; without them, restoration may fail or not terminate.Source: §4.1.1 · pp. 13–14

4.1.2 Example: Constant Folding.

• Constant folding can be expressed as an e-class analysis, with make abstracting node values and modify adding a constant node when the class has a constant value.The join operation also checks that terms unified in one class have the same constant value.Source: §4.1.2 · pp. 14–15

4.2 Conditional and Dynamic Rewrites

• Conditional rewrites check analysis facts to determine validity, while dynamic rewrites use those facts to construct the right-hand side.The paper gives x/x → 1 as a conditional rewrite whose validity depends on x ≠ 0.Source: §4.2 · p. 15

4.3 Extraction

• For local cost functions, extraction can be an e-class analysis that stores each class’s cheapest e-node and cost.This also lets conditional and dynamic rewrites use the cheapest term in a class.Source: §4.3 · pp. 15–16

5 egg: EASY, EXTENSIBLE, AND EFFICIENT E-GRAPHS

• egg implements rebuilding and e-class analysis in a reusable e-graph library, with a lambda-calculus example demonstrating extensibility for binding.The example uses explicit substitution, which the authors describe as illustrative but costly; built-in support for binding remains future work.Source: §5 · p. 16, §5.1 · p. 16

5.1 Ease of Use

• Users define a language and rewrites, then use Runners and Extractors to manage saturation, limits, iteration metrics, and cost-based extraction.The define_language! macro supports language definitions; tests can check whether a rewritten pattern occurs in the initial expression’s e-class.Source: §5.1 · pp. 16, 18

5.2 Extensibility

• E-class analyses track facts such as constants and free variables, while conditional and dynamic rewrites use those facts to guide transformations.CaptureAvoid applies a capture-avoiding substitution only when free-variable information indicates it is needed; user-defined schedulers can also moderate expansive rules.Source: §5.2 · p. 18, Figure 11 · p. 19

5.3 Efficiency

• Rust specialization, cache-friendly flat buffers, and compiled patterns support egg’s efficiency, alongside rebuilding and other implementation optimizations.Phase-separated search can be parallelized; per-iteration rebuilding also permits search-phase invariants such as sorted e-nodes and a function-symbol cache.Source: §5.3 · p. 20
• Batch simplification and user hooks can improve performance when inputs are similar or a task-specific stopping condition is reached.Structural deduplication lets similar starting expressions share rewriting and analysis work.Source: §5.3 · p. 20

• All three projects had first developed their own e-graph implementations before incorporating egg.Source: §6 · p. 20
• Using egg let the projects delete code and gain performance; in some cases, they also broadened project scope.Source: §6 · p. 20
• The projects used egg’s extensibility features, including e-class analyses and dynamic or conditional rewrites.Source: §6 · p. 20

6.1 Herbie: Improving Floating Point Accuracy

• Herbie’s earlier Racket simplifier consumed most runtime, so its size and time limits could make simplification fail altogether.The slowdown also constrained features that would require additional simplification calls.Source: §6.1 · p. 21

6.1.1 Implementation.

• The Rust backend defines Herbie’s expression grammar and uses an e-class analysis to track exact values for constant folding.The implementation separates exact rational constants from inexact constants and evaluates operations when all arguments have exact values.Source: §6.1.1 · p. 21

6.1.2 Results.

• Deferring rebuilding gave Herbie’s Racket e-graph implementation a further 2.2× speedup, with better scaling as search size grows.Batch simplification also speeds work on similar expressions through structural sharing.Source: §6.1.2 · p. 22

6.2.1 Implementation.

• Spores uses relational-algebra identities and fused-operator identities to expose fine-grained equivalences and avoid intermediate matrices.For example, a squared residual expression can be replaced with a streaming sqloss operator.Source: §6.2 · p. 22, §6.2.1 · p. 23
• Spores represents relations as functions from tuples to real numbers and optimizes in relational algebra between linear-algebra input and output translations.Relational algebra uses join, union, and aggregate; join multiplies associated values, union adds them, and aggregate sums along a dimension.Source: §6.2.1 · pp. 22–23
• An e-class analysis tracks expression schemas, conservatively estimates costs, and performs constant folding during optimization.When equivalent expressions have different cost estimates, merges retain the lower estimate.Source: §6.2.1 · p. 23

6.2.2 Results.

• 1.2× to 5× end-to-end speedups came from novel rewrites discovered by Spores in its Apache SystemML prototype.All compilations completed within a second with greedy extraction.Source: §6.2.2 · p. 23
• The SystemML prototype derived all 84 hand-written rules and heuristics for sum-product optimization.This result demonstrates that Spores can recover the existing rule set while also discovering novel rewrites.Source: §6.2.2 · p. 23

6.3 Szalinski: Decompiling CAD into Structured Programs

• Szalinski extracts maps and folds from flat CSG outputs, producing structured programs that are easier to customize through small, mostly local edits.The illustrated customized model is a 3D-printed hex wrench holder with altered hole sizes.Source: §6.3 · p. 24, Figure 14 · p. 24
• Loop-rerolling rules infer Fold, Map2, Repeat, and Tabulate patterns, while CAD identities equate differently expressed terms.Szalinski also uses external solvers to propose potentially profitable expressions when list elements are ordered or grouped unintuitively.Source: §6.3 · p. 24

6.3.1 Implementation.

• For repetitive lists, an e-class analysis tracks accumulated vectors and a solver-backed dynamic rewrite converts them into a Tabulate expression.Subsequent syntactic rewrites can hoist the Tabulate, including when CAD identities affect the input.Source: §6.3.1 · pp. 24–25, Figure 15 · p. 25
• Inverse transformations let solvers reorder or regroup lists speculatively without asserting those non-equivalent reorderings as e-graph equivalences.The solver records the permutation or grouping, and later syntactic rewrites remove inverse transformations when possible.Source: §6.3.1 · p. 25

6.3.2 Results.

• About 1000× faster performance after switching to egg enabled Szalinski to move from small hand-picked examples to evaluation on over 2000 real-world models.The authors also report that the switch removed most custom e-graph code and eliminated bugs.Source: §6.3.2 · p. 25

Term Rewriting.

• Term rewriting applies semantics-preserving symbolic rules but can create a phase-ordering problem by replacing an expression and losing access to the old one.The approach has been used in program optimization, theorem proving, and program transformation.Source: §7 · p. 25

E-graphs and E-matching.

• Egg’s rebuilding maintains e-graph invariants only at critical points, specializing invariant restoration to equality saturation rather than conventional per-operation maintenance.Egg also provides e-class analyses for semantic reasoning, and its design is compatible with several theorem-prover matching optimizations not yet explored in egg.Source: §7 · p. 26

Congruence Closure.

• Rebuilding adapts congruence closure to online equality saturation, where rewrites inspect current equalities and assert new ones, and it also propagates analysis facts.The paper gives no theoretical analysis of rebuilding in the online setting, whose performance is likely workload dependent.Source: §7 · p. 26

Superoptimization and Equality Saturation.

• Denali used e-graphs and SAT solving for near-optimal assembly generation but targeted straight-line code, limiting applicability to large real programs.Later equality-saturation work handled constructs such as loops and conditionals with PEGs, which egg can support as a user-defined language.Source: §7 · p. 26

8 CONCLUSION

• Rebuilding amortizes e-graph invariant maintenance and specializes its restoration to the equality-saturation workload.The paper presents it as one of two techniques for making equality saturation fast and extensible.Source: §8 · p. 26
• E-class analysis provides a general framework for interpreted reasoning beyond purely syntactic rewrites.Source: §8 · p. 27
• Egg combines the techniques in a reusable, efficient, extensible library generic over user-defined languages, avoiding ad hoc e-graph implementations and manipulations.The case studies show equality saturation scaling further and being used more flexibly, with new functionality and large speedups.Source: §8 · p. 27