Equality Saturation: Optimizing Code With E-Graphs

The phase-ordering problem it solves

Classical optimizers are pipelines of destructive rewrites. Constant folding, common-subexpression elimination, strength reduction, inlining, loop-invariant code motion — each pass reads the program, decides on a change, and overwrites the old form with the new one. The trouble is that these passes interact. Inlining can expose a constant that folding could have used, but only if folding runs afterward; strength-reducing x*2 to x<<1 may hide the fact that a later distributivity rule wanted the multiply. This is the phase-ordering problem: there is no single order of passes that is best for all programs, choosing an order is effectively intractable, and real compilers such as LLVM and GCC ship a hand-tuned, sometimes-repeated pipeline that is known to be suboptimal.

Greedy rewriting has a second, deeper flaw: a rewrite that looks locally profitable can be globally harmful. Because each step commits and discards the previous form, the search can walk into a local optimum it can never leave. Equality saturation removes both problems by refusing to ever throw a form away.

The e-graph: storing every equivalent program at once

The core data structure is the e-graph (equivalence graph), invented by Greg Nelson and Derek Oppen in 1980 for congruence closure inside automated theorem provers and later repurposed for optimization. An e-graph is built from two kinds of node:

• An e-node is an operator applied to children — but the children are not other e-nodes, they are e-classes. So (+ a b) is an e-node whose symbol is + and whose two children are the e-class of a and the e-class of b.
• An e-class is a set of e-nodes that have been proven equivalent. Every term the e-graph currently believes are equal to each other live in one e-class.

This one level of indirection is what makes the structure so compact. If an e-class contains ten equivalent forms of a subexpression, and it is the child of an operator that also has ten forms, the parent already denotes 100 distinct programs while storing only twenty e-nodes. Sharing multiplies: a modest e-graph routinely represents exponentially many programs, and because e-classes may reference themselves through cycles, it can represent infinitely many.

Two invariants keep the structure honest. A hashcons (memo table) maps each e-node to its e-class so identical e-nodes are never duplicated. The congruence invariant says that if two e-nodes have the same operator and their children are pairwise in the same e-classes, they must be in the same e-class — i.e. equal inputs to the same function give equal outputs. Maintaining equivalence between e-classes is done with a union-find (disjoint-set) structure, so merging two e-classes costs near-constant amortized time, O(α(n)) with the inverse-Ackermann function α.

The saturation loop: read, write, rebuild

Optimization proceeds by repeatedly applying a set of rewrite rules — bidirectional equalities such as x*2 = x<<1, (a+b)*c = a*c + b*c, x+0 = x, or (a*b)*c = a*(b*c). Crucially the application is non-destructive: when a rule fires, the compiler adds the right-hand side to the e-graph and unions its e-class with the matched left-hand side. The original form stays. Every ordering of rewrites is therefore explored at the same time, because no ordering ever deletes an opportunity.

Each iteration has three phases, as formalized by the egg library (Willsey, Nandi, Wang, Flatt, Tatlock, Panchekha, POPL 2021):

• Read (e-matching): search the e-graph for every place a rule's left-hand pattern matches. E-matching over e-classes is the performance bottleneck and is worst-case exponential; egglog reformulates it as a relational join solved with worst-case-optimal join algorithms.
• Write: for each match, add the right-hand e-node and record a pending union. egg defers these unions rather than repairing invariants immediately.
• Rebuild: restore the hashcons and congruence invariants in one batched pass. egg's key insight was that deferring and de-duplicating this repair work — instead of restoring congruence after every single merge — makes saturation asymptotically faster, with reported speedups of roughly one-to-two orders of magnitude on real workloads.

The loop runs until saturation: a fixpoint where no rule can add a new e-node or a new equality. Because rules like associativity and commutativity can grow the graph without bound, true saturation may be unreachable, so implementations impose limits on iterations, node count, or wall-clock time and stop early.

Extraction: pulling the cheapest program back out

After saturation the e-graph holds a whole space of equivalent programs; the compiler still needs one concrete program to emit. That final step is extraction: choose one e-node from each reachable e-class so that the resulting term minimizes a cost model (instruction count, latency, floating-point error, estimated cycles).

The simple method is greedy bottom-up extraction: assign each e-class the minimum cost over its e-nodes, where an e-node's cost is its own cost plus the costs of its children's e-classes, and iterate to a fixpoint (this also naturally avoids cyclic terms, whose cost never converges downward). This is fast and near-linear but assumes costs add up along a tree — it does not account for shared subexpressions, where reusing a value already computed should be free.

Once you want the true optimum under a DAG cost model with sharing, extraction becomes NP-hard. The standard exact formulation is an integer linear program (ILP): a 0/1 variable per e-node, constraints that a selected node's children must also be selected and that the selection is acyclic, minimizing total cost. ILP gives the global optimum but can be slow, so production systems typically ship greedy extraction and reserve ILP for cases where the extra quality pays off.

Why the guarantees hold, and what they cost

The correctness argument is clean: every e-node ever added is equal to what it was rewritten from (because rules are sound equalities), and the congruence invariant only ever merges classes that are provably equal. So any term extracted from the e-graph is semantically equivalent to the input program by construction — extraction cannot produce a wrong answer, only a suboptimal one. This is why equality saturation is used for verified and safety-critical rewriting.

The optimality argument is relative, not absolute. Equality saturation finds the cheapest program in the space it managed to discover before hitting its resource limit. Given the same rule set and unlimited resources it would find the true optimum reachable by those rules — strictly dominating any single greedy ordering, which can only explore one path. The costs are memory and matching time: the e-graph can blow up, e-matching is the dominant expense, and adversarial rule sets (deep associativity/commutativity, ring axioms) can make the graph grow faster than any budget. Choosing rules and resource limits is the real engineering, much as choosing a pass pipeline is in a classical compiler — but the ordering problem itself is gone.

Where it runs in real systems

Equality saturation was named and popularized by Ross Tate, Michael Stepp, Zachary Tatlock and Sorin Lerner in their POPL 2009 paper, but it became practical with egg ("e-graphs good"), a fast, extensible Rust library whose deferred-rebuilding trick made saturation cheap enough for real tools. Its successor egglog (Zhang et al., PLDI 2023) fuses e-graphs with Datalog, letting analyses and rewrites be written as declarative rules over a database and evaluated with worst-case-optimal joins.

• Herbie improves the accuracy of floating-point expressions, using e-graphs to explore algebraically equivalent rearrangements that reduce rounding error; it is used by numerical-software developers and won a PLDI 2015 distinguished paper.
• Cranelift, the WebAssembly and Rust code generator, builds its mid-end optimizer on ægraphs (acyclic e-graphs) — Chris Fallin's design that fuses e-graph rewriting with the SSA IR to do global value numbering, constant folding and code motion in one pass.
• Tensat and related work apply equality saturation to tensor-graph superoptimization for machine-learning compilers, searching equivalent operator graphs for faster execution plans.

The technique also appears in hardware datapath synthesis, SQL query optimization research, and theorem-prover simplification — anywhere a rich set of equivalences meets a cost model.

Equality saturation versus other rewriting strategies

Strategy	How it explores	Phase-ordering sensitivity	Result quality
Greedy / destructive rewriting	Applies one rule, replaces the term in place	High — a chosen rewrite can block a later one	Local optimum; order-dependent
Pass-based optimizer (LLVM-style)	Fixed pipeline of passes, each destructive	High — pipeline order is hand-tuned	Good, but no order is universally best
Equality saturation	Adds every rewritten form non-destructively to an e-graph, to a fixpoint	None — all orders explored simultaneously	Global optimum over the discovered space
Superoptimization (SMT / search)	Searches instruction sequences directly	N/A	Optimal for a tiny window, extremely slow