Equality is just the beginning: optimizations for semantic-aware e-graphs.
E-graphs store bare equalities: they do not know why an equality holds, when it applies, or how it relates to facts derived elsewhere, so reasoning tools compensate with costly workarounds. Smart e-graphs move that semantic knowledge into the data structure itself: proving more, faster.
E-graphs compactly represent large spaces of equivalent terms, and they sit at the
core of automated theorem provers, SMT solvers, and optimizing compilers. The
classical data structure is built around one kind of fact: unconditional equality
between terms. For example, the e-graph below contains the atoms a and
b and the applications f(a) and f(b).
Rectangles are e-nodes, one per term; circles are e-classes, the
sets of e-nodes known to be equal; and each arrow connects an e-node to the e-class
of its argument. Initially every e-node sits in its own e-class (a). Asserting
a = b merges their e-classes (b), and by congruence the e-graph
discovers on its own that f(a) = f(b), merging those e-classes as
well (c).
Other aspects of the reasoning, such as terms being different, equalities holding under assumptions, or facts being discovered in separate contexts, are not part of the data structure itself. This semantic information is traditionally managed by the tools around the e-graph, for example by encoding it through equalities or by maintaining one e-graph per context.
Consider a verifier analyzing the following function, which adds the distances
f(dx) and f(dy) of two differences, doubling by a bit
shift when the operands are known to be equal. Each conditional splits the
reasoning into branches: the first branch assumes dx = dy, the others
assume dx ≠ dy together with da = db or
da ≠ db. The nested scopes form a tree of contexts, each carrying
its own set of facts.
A classical e-graph has no place for any of this. The disequality
dx ≠ dy cannot be stated, so it must be tracked outside the data
structure. Each branch needs its own equivalence relation, so tools maintain one
full e-graph per branch, even though the branches agree on most of what they know.
And once the branches have been explored, there is no operation to combine what they
learned. As programs and proofs branch further, the duplicated and replayed work
compounds.
Representing difference, assumptions, and contexts directly in the data structure removes these costs: facts can be shared across proof branches rather than replicated, knowledge from independently explored contexts can be composed, and proof exploration can be organized in parallel. The extensions below develop this idea step by step, each with formal correctness guarantees and measurable performance gains.
E-graphs that natively know when two terms must differ. Refutation becomes a first-class operation instead of an encoding trick, with a simpler metatheory and better performance than the embeddings used in SMT solvers. Dis/Equality Graphs, POPL 2025.
Equalities rarely hold unconditionally. Versioned e-graphs encode a whole family of equivalence relations at once, one per set of assumptions, so proof branches share the facts they agree on instead of replicating them. Versioned E-Graphs, PLDI 2026.
Equivalence relations form a lattice. Lazy meet and join operations compose the knowledge of independently explored contexts on demand, touching only the equalities a query actually needs. In progress.
The lattice structure exposes which reasoning tasks are independent. Scheduling proof exploration as parallel tasks over a lattice of e-graphs turns semantic awareness into raw speed. In progress.
Proc. ACM Program. Lang. 10, PLDI, Article 171, June 2026
E-graphs are an efficient encoding for discovering and maintaining sets of equalities. In several scenarios, equalities may hold only conditionally, i.e., under certain assumptions: in automated provers the proof is often split into multiple branches, each considering a different set of equalities. Traditional e-graphs can only encode a single set of equalities at a time, so conditional equalities are handled by maintaining multiple e-graphs, replicating the equalities shared among branches. Versioned e-graphs efficiently encode multiple equivalence sets at the same time, maximizing shared information among them. Compared to widely-adopted solutions that maintain multiple e-graphs, versioned e-graphs are up to 5–30% more memory efficient and up to 4× faster, especially when solution spaces are large both in explored program terms and number of branches.
Proc. ACM Program. Lang. 9, POPL, Article 77, January 2025
In many applications it is necessary to reason about disequality of terms as well as equality. While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory. This paper develops an implementation-independent framework to formally reason about e-graphs, proving for the first time the equivalence of e-graphs to the closure of the equivalence relation they encode. It presents the first formalization of an e-graph extension that directly supports disequalities, with an analytical result about their superior efficiency compared to common embedding techniques. The approach is implemented as an extension to egg and evaluated in an SMT solver and an automated theorem prover, where direct support for disequalities outperforms encodings based on equality embedding.