Pith. sign in

REVIEW 3 cited by

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2504.14340 v1 pith:EGZEZEKN submitted 2025-04-19 cs.PL

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

Philip Zucker This is my paper
classification cs.PL
keywords e-graphsgenerictheoriesbottom-upe-graphe-matchingmoduloquestion
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Rewrite System Showdown: Stochastic Search vs. EqSat

    cs.PL 2026-05 unverdicted novelty 7.0

    The paper benchmarks equality saturation against stochastic search on five program optimization tasks to evaluate the effectiveness of e-graphs.

  2. Optimism in Equality Saturation

    cs.PL 2025-11 unverdicted novelty 7.0

    A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.

  3. Rewrite System Showdown: Stochastic Search vs. EqSat

    cs.PL 2026-05 unverdicted novelty 6.0

    Empirical comparison of equality saturation versus stochastic search on five benchmarks to evaluate if e-graphs are superior for rewrite-based optimization.