Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching

TL;DR

Addresses how to fuse generic e-graph rewriting with specialized theories (e.g., AC, sets, multisets, polynomials) in an EMT setting. Proposes bottom-up e-matching coupled with semantic e-ids and a theory-aware union-find canonizer, enabling grounding and efficient equality reasoning. Demonstrates theory coverage via atomic ground equations, linear systems, Gröbner-basis style polynomial domains, and multiset semantics, plus discussion of abstraction via a minimal interface for canonizers. Shows that this approach preserves e-graph infrastructure while enabling theory specialization, suggesting practical EMT with broad applicability across formal reasoning and optimization tasks.

Abstract

E-graphs are a data structure for equational reasoning and optimization over ground terms. One of the benefits of e-graph rewriting is that it can declaratively handle useful but difficult to orient identities like associativity and commutativity (AC) in a generic way. However, using these generic mechanisms is more computationally expensive than using bespoke routines on terms containing sets, multi-sets, linear expressions, polynomials, and binders. A natural question arises: How can one combine the generic capabilities of e-graph rewriting with these specialized theories. This paper discusses a pragmatic approach to this e-graphs modulo theories (EMT) question using two key ideas: bottom-up e-matching and semantic e-ids.