pith. sign in

arxiv: 2511.20782 · v4 · submitted 2025-11-25 · 💻 cs.PL

Optimism in Equality Saturation

Russel Arbore , Alvin Cheung , Max Willsey This is my paper

Pith reviewed 2026-05-17 04:28 UTC · model grok-4.3

classification 💻 cs.PL
keywords equality saturatione-graphsabstract interpretationprogram optimizationSSA programsoptimistic analysiscyclic programsnon-destructive rewriting
0
0 comments X

The pith

A new abstract interpretation algorithm performs sound optimistic analysis of e-graphs during equality saturation and unifies it with non-destructive rewriting.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Equality saturation optimizes programs through repeated non-destructive rewrites stored in e-graphs. Existing e-class analyses stay pessimistic to remain safe and therefore lose precision on cyclic programs such as those in SSA form. A direct attempt to make the analysis optimistic turns out to be unsound because of how e-graphs encode program structure. The paper supplies a revised abstract-interpretation procedure that respects this structure, yielding sound optimism. The result is a single algorithm that interleaves optimistic analysis with rewriting and delivers higher precision on cyclic examples while keeping performance comparable to prior methods.

Core claim

The paper establishes that an abstract interpretation algorithm can analyze e-graphs optimistically during equality saturation without introducing unsoundness. It does so by correctly handling the representation of programs inside e-graphs, in particular the encoding of cyclic SSA programs. The same procedure simultaneously performs non-destructive rewriting, producing a unified optimization engine that improves precision over both pure abstract interpretation and pessimistic e-class analysis.

What carries the argument

The optimistic e-class analysis algorithm that respects e-graph representation of programs and runs together with non-destructive rewriting.

If this is right

  • Optimizations of cyclic programs achieve higher precision than either standalone abstract interpretation or pessimistic e-class analysis.
  • A single procedure now handles both optimistic analysis and non-destructive rewriting.
  • The implementation shows precision gains on example SSA programs while matching the speed of existing analysis techniques.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same representation-aware optimism could be applied to other graph-based program representations beyond e-graphs.
  • Compilers that already use equality saturation might obtain more aggressive transformations on looped code by adopting this analysis.
  • The work highlights that soundness in optimistic settings depends on precise modeling of how equalities are stored rather than on the optimism itself.

Load-bearing premise

The new algorithm correctly accounts for the specific way e-graphs represent cyclic programs so that optimistic conclusions remain sound.

What would settle it

A cyclic SSA program on which the straightforward optimistic analysis produces an incorrect program property while the proposed algorithm produces only sound properties.

Figures

Figures reproduced from arXiv: 2511.20782 by Alvin Cheung, Max Willsey, Russel Arbore.

Figure 1
Figure 1. Figure 1: An example e-graph during equality saturation. Symbols are e-nodes, solid edges connect e-nodes [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A program in pseudo-code and its compilation into a SSA program. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Flow insensitive dataflow analysis (with the [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A trace of the dataflow algorithm performing a flow insensitive interval analysis on the running [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The interval (I) and offset (O) abstractions. Both abstractions are fairly standard, except that the concretization functions return functions that take and ignore a control flow walk argument. 1 fn example1 ( y ) { 2 let x = -6; 3 let z = 42; 4 while y < 10 { 5 y = y + 1; 6 x = x + 8; 7 let lhs = (( x + y ) + z ) * y ; 8 let rhs = 2 * y + ( y * y + z * y ) ; 9 if lhs ! = rhs { 10 z = 24; 11 } 12 x = x - 8… view at source ↗
Figure 7
Figure 7. Figure 7: Second example program to an￾alyze and rewrite. The goal is to show that the returned value is 0, which requires rewriting and an optimistic equivalence analysis. 7.2 Example Programs The first program example is shown in [PITH_FULL_IMAGE:figures/full_fig_p018_7.png] view at source ↗
read the original abstract

Equality saturation is a program optimization technique based on non-destructive rewriting and a form of abstract interpretation called e-class analysis. Existing e-class analyses are pessimistic and therefore typically imprecise when analyzing cyclic programs, such as those in SSA form. We show that a straightforward optimistic variant of e-class analysis can result in unsoundness, due to a subtlety in how e-graphs represent programs. We propose an abstract interpretation algorithm that circumvents this issue and can optimistically analyze e-graphs during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We implement a prototype abstract interpreter and equality saturation tool for SSA programs. Our tool exhibits precision improvements over pure abstract interpretation (without rewriting) and pessimistic e-class analysis on example programs. Additionally, its performance is comparable to existing abstract interpretation and e-class analysis techniques.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that a naive optimistic variant of e-class analysis in equality saturation is unsound due to subtleties in how e-graphs encode program structure (shared e-nodes and cycles from SSA phi-nodes). It proposes a new abstract interpretation algorithm that circumvents the issue while unifying optimistic analysis with non-destructive rewriting. A prototype for SSA programs is implemented and evaluated, showing precision improvements over pure abstract interpretation and pessimistic e-class analysis with comparable performance.

Significance. If the soundness argument holds, the result is significant for program optimization: it enables optimistic (more precise) analysis of cyclic programs inside equality saturation without the typical imprecision of pessimistic e-class analyses. The unification of analysis and rewriting is a practical contribution, and the prototype provides concrete evidence of precision gains on example programs. This addresses a known limitation in e-graph techniques for SSA and loop-heavy code.

major comments (2)
  1. [§4.2] §4.2 (unified algorithm description): The circumvention of the unsoundness shown in §3 relies on an informal argument about handling e-class merges and phi-node cycles; without a formal invariant or exhaustive case analysis on cyclic SSA fragments, it is unclear whether residual cases of incorrect optimistic propagation are fully eliminated.
  2. [§5] §5 (evaluation): The reported precision improvements are demonstrated only on example programs without quantitative metrics (e.g., number of optimized instructions or comparison to state-of-the-art SSA optimizers), which weakens the claim that the unified algorithm delivers practically meaningful gains over pessimistic e-class analysis.
minor comments (2)
  1. [Preliminaries] Preliminaries section: Notation for e-nodes, e-classes, and the distinction between pessimistic vs. optimistic analysis could be introduced with a small running example to improve readability for readers new to e-graphs.
  2. [Figure 3] Figure 3: The diagram illustrating the unified algorithm would benefit from explicit labels on the dataflow between the analysis and rewriting components.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive review. The comments highlight important areas for strengthening the soundness presentation and empirical claims. We address each point below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [§4.2] §4.2 (unified algorithm description): The circumvention of the unsoundness shown in §3 relies on an informal argument about handling e-class merges and phi-node cycles; without a formal invariant or exhaustive case analysis on cyclic SSA fragments, it is unclear whether residual cases of incorrect optimistic propagation are fully eliminated.

    Authors: We agree that the current presentation in §4.2 relies on an informal argument. The algorithm avoids unsound propagation by deferring optimistic updates until e-class merges stabilize and by processing phi-node cycles in a dependency-respecting order that mirrors the SSA dominance relation. In the revision we will add an explicit invariant (that the abstract state at each e-class is a sound over-approximation of all concrete values reachable under the current e-graph) together with a short case analysis on the possible merge patterns for a single cyclic fragment. This will make the elimination of residual unsound cases explicit without requiring a full mechanized proof. revision: yes

  2. Referee: [§5] §5 (evaluation): The reported precision improvements are demonstrated only on example programs without quantitative metrics (e.g., number of optimized instructions or comparison to state-of-the-art SSA optimizers), which weakens the claim that the unified algorithm delivers practically meaningful gains over pessimistic e-class analysis.

    Authors: The evaluation intentionally uses small, hand-crafted examples to isolate the effect of optimistic analysis on cyclic SSA fragments. We acknowledge that this leaves the practical magnitude of the gains less quantified. In the revised manuscript we will augment §5 with concrete counts of additional optimizations enabled (e.g., number of instructions removed or strength-reduced) and a direct comparison against a standard pessimistic e-class analysis baseline as well as a simple LLVM-style SSA optimizer on the same examples. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the proposed optimistic e-class analysis

full rationale

The paper first exhibits unsoundness of a naive optimistic e-class analysis due to e-graph representation details (shared e-nodes and SSA-induced cycles). It then directly presents a new abstract-interpretation algorithm that avoids those cases while unifying analysis with non-destructive rewriting. The derivation consists of a standard soundness argument for the new transfer functions and fixpoint computation; it does not reduce any central claim to a fitted parameter, a self-definition, or a load-bearing self-citation whose validity is presupposed. The algorithm is self-contained against the identified subtlety and does not rename or smuggle prior results by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard assumptions from abstract interpretation and e-graph theory rather than new free parameters or invented entities. No explicit fitted values or ad-hoc axioms are mentioned in the abstract.

axioms (2)
  • domain assumption E-graphs represent programs such that a straightforward optimistic e-class analysis leads to unsoundness on cyclic structures.
    Invoked to motivate the need for the new algorithm; appears in the discussion of the subtlety in e-graph representation.
  • domain assumption Abstract interpretation can be combined with non-destructive rewriting in a unified sound algorithm.
    Core premise of the proposed approach for SSA programs.

pith-pipeline@v0.9.0 · 5428 in / 1356 out tokens · 68970 ms · 2026-05-17T04:28:36.232685+00:00 · methodology

discussion (0)

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

Forward citations

Cited by 2 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. 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.

Reference graph

Works this paper leans on

59 extracted references · 59 canonical work pages · cited by 1 Pith paper

  1. [1]

    Aho, Monica S

    Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006.Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., USA

    work page 2006

  2. [2]

    Alpern, M

    B. Alpern, M. N. Wegman, and F. K. Zadeck. 1988. Detecting equality of variables in programs. InProceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(San Diego, California, USA)(POPL ’88). Association for Computing Machinery, New York, NY, USA, 1–11. doi:10.1145/73560.73561

    work page doi:10.1145/73560.73561 1988

  3. [3]

    François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. InFormal Methods in Programming and Their Applications, Dines Bjørner, Manfred Broy, and Igor V. Pottosin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 128–141

    work page 1993

  4. [4]

    Yaohui Cai, Kaixin Yang, Chenhui Deng, Cunxi Yu, and Zhiru Zhang. 2025. SmoothE: Differentiable E-Graph Extraction. InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1(Rotterdam, Netherlands)(ASPLOS ’25). Association for Computing Machinery, New York, NY, USA, 1020–1034....

    work page doi:10.1145/3669940.3707262 2025

  5. [5]

    Rustan M

    Bor-Yuh Evan Chang and K. Rustan M. Leino. 2005. Abstract Interpretation with Alien Expressions and Heap Structures. InVerification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 147–163

    work page 2005

  6. [6]

    Cliff Click and Keith D. Cooper. 1995. Combining analyses, combining optimizations.ACM Trans. Program. Lang. Syst. 17, 2 (March 1995), 181–196. doi:10.1145/201059.201061

    work page doi:10.1145/201059.201061 1995

  7. [7]

    Cliff Click and Michael Paleczny. 1995. A simple graph-based intermediate representation. InPapers from the 1995 ACM SIGPLAN Workshop on Intermediate Representations(San Francisco, California, USA)(IR ’95). Association for Computing Machinery, New York, NY, USA, 35–49. doi:10.1145/202529.202534

    work page doi:10.1145/202529.202534 1995

  8. [8]

    Agostino Cortesi, Giulia Costantini, and Pietro Ferrara. 2013. A Survey on Product Operators in Abstract Interpretation. Electronic Proceedings in Theoretical Computer Science129 (09 2013). doi:10.4204/EPTCS.129.19

    work page doi:10.4204/eptcs.129.19 2013

  9. [9]

    Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles 22 Arbore et al. of Programming Languages(Los Angeles, California)(POPL ’77). Association for Computing Machinery, New Yo...

    work page doi:10.1145/512950.512973 1977

  10. [10]

    Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. InProceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages(San Antonio, Texas)(POPL ’79). Association for Computing Machinery, New York, NY, USA, 269–282. doi:10.1145/567752.567778

    work page doi:10.1145/567752.567778 1979

  11. [11]

    Patrick Cousot and Radhia Cousot. 2002. Systematic design of program transformation frameworks by abstract interpretation.SIGPLAN Not.37, 1 (Jan. 2002), 178–190. doi:10.1145/565816.503290

    work page doi:10.1145/565816.503290 2002

  12. [12]

    Constantinides, and Theo Drane

    Samuel Coward, George A. Constantinides, and Theo Drane. 2023. Combining E-Graphs with Abstract Interpretation. InProceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis(Orlando, FL, USA)(SOAP 2023). Association for Computing Machinery, New York, NY, USA, 1–7. doi:10.1145/3589250.3596144

    work page doi:10.1145/3589250.3596144 2023

  13. [13]

    Constantinides

    Samuel Coward, Theo Drane, and George A. Constantinides. 2024. ROVER: RTL Optimization via Verified E-Graph Rewriting.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems(2024), 1–1. doi:10.1109/ TCAD.2024.3410154

    work page arXiv 2024

  14. [14]

    Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. InProceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(Budapest, Hungary)(TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340

    work page 2008

  15. [15]

    Delphine Demange, Yon Fernández de Retana, and David Pichardie. 2018. Semantic reasoning about the sea of nodes. InProceedings of the 27th International Conference on Compiler Construction(Vienna, Austria)(CC ’18). Association for Computing Machinery, New York, NY, USA, 163–173. doi:10.1145/3178372.3179503

    work page doi:10.1145/3178372.3179503 2018

  16. [16]

    Alexandre Drewery, Thomas Jensen, and David Pichardie. 2025. Contextual Equality Saturation. InSAS 2025 - 32nd Static Analysis Symposium. Singapore, Singapore, 1–26. https://inria.hal.science/hal-05226543

    work page 2025

  17. [17]

    Chris Fallin. 2023. ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler. https://pldi23.sigplan.org/details/egraphs-2023-papers/2/-graphs-Acyclic-E-graphs-for-Efficient-Optimization-in- a-Production-Compiler

    work page 2023

  18. [18]

    H. Gericke. 1957. Tarski Alfred. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of mathematics , Bd. 5 (1955), S. 285–309.Journal of Symbolic Logic22 (1957), 370 – 370. https://api.semanticscholar.org/CorpusID: 119521721

    work page 1957

  19. [19]

    Amir Kafshdar Goharshady, Chun Kit Lam, and Lionel Parreaux. 2024. Fast and Optimal Extraction for Sparse Equality Graphs.Proc. ACM Program. Lang.8, OOPSLA2, Article 361 (Oct. 2024), 27 pages. doi:10.1145/3689801

    work page doi:10.1145/3689801 2024

  20. [20]

    Hellerstein

    Tyler Hou, Shadaj Laddad, and Joseph M. Hellerstein. 2025. Towards Relational Contextual Equality Saturation. arXiv:2507.11897 [cs.PL] https://arxiv.org/abs/2507.11897

    work page arXiv 2025

  21. [21]

    Monotone data flow analysis fr ameworks,

    John B. Kam and Jeffrey D. Ullman. 1977. Monotone data flow analysis frameworks.Acta Inf.7, 3 (Sept. 1977), 305–317. doi:10.1007/BF00290339

    work page doi:10.1007/bf00290339 1977

  22. [22]

    Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transfor- mation. InProceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization(Palo Alto, California)(CGO ’04). IEEE Computer Society, USA, 75

    work page 2004

  23. [23]

    Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. 2021. MLIR: scaling compiler infrastructure for domain specific computation. InProceedings of the 2021 IEEE/ACM International Symposium on Code Generation and Optimization (Virtual Event, Republ...

    work page doi:10.1109/cgo51591.2021.9370308 2021

  24. [24]

    Matthieu Lemerre. 2023. SSA Translation Is an Abstract Interpretation.Proc. ACM Program. Lang.7, POPL, Article 65 (Jan. 2023), 30 pages. doi:10.1145/3571258

    work page doi:10.1145/3571258 2023

  25. [25]

    Sorin Lerner, David Grove, and Craig Chambers. 2002. Composing dataflow analyses and transformations. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Portland, Oregon) (POPL ’02). Association for Computing Machinery, New York, NY, USA, 270–282. doi:10.1145/503272.503298

    work page doi:10.1145/503272.503298 2002

  26. [26]

    Dorian Lesbre and Matthieu Lemerre. 2024. Compiling with Abstract Interpretation.Proc. ACM Program. Lang.8, PLDI, Article 162 (June 2024), 26 pages. doi:10.1145/3656392

    work page doi:10.1145/3656392 2024

  27. [27]

    Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait-El-Hara, and François Bobot. 2025. Relational Abstractions Based on Labeled Union-Find.Proc. ACM Program. Lang.9, PLDI, Article 195 (June 2025), 26 pages. doi:10.1145/3729298

    work page doi:10.1145/3729298 2025

  28. [28]

    Francesco Logozzo and Manuel Fähndrich. 2008. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. InProceedings of the 2008 ACM Symposium on Applied Computing(Fortaleza, Ceara, Brazil) (SAC ’08). Association for Computing Machinery, New York, NY, USA, 184–188. doi:10.1145/1363686.1363736

    work page doi:10.1145/1363686.1363736 2008

  29. [29]

    Antoine Miné. 2001. A New Numerical Abstract Domain Based on Difference-Bound Matrices. InProceedings of the Second Symposium on Programs as Data Objects (PADO ’01). Springer-Verlag, Berlin, Heidelberg, 155–172

    work page 2001

  30. [30]

    Antoine Miné. 2002. A Few Graph-Based Relational Numerical Abstract Domains. InProceedings of the 9th International Symposium on Static Analysis (SAS ’02). Springer-Verlag, Berlin, Heidelberg, 117–132. Optimism in Equality Saturation 23

    work page 2002

  31. [31]

    Antoine Miné. 2006. The octagon abstract domain.Higher Order Symbol. Comput.19, 1 (March 2006), 31–100. doi:10.1007/s10990-006-8609-1

    work page doi:10.1007/s10990-006-8609-1 2006

  32. [32]

    Leonardo Moura and Nikolaj Bjørner. 2007. Efficient E-Matching for SMT Solvers. InProceedings of the 21st International Conference on Automated Deduction: Automated Deduction(Bremen, Germany)(CADE-21). Springer-Verlag, Berlin, Heidelberg, 183–198. doi:10.1007/978-3-540-73595-3_13

    work page doi:10.1007/978-3-540-73595-3_13 2007

  33. [33]

    Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock

    Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock. 2020. Synthesizing structured CAD models with equality saturation and inverse transformations. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK)(PLDI 2020). Association for Computing ...

    work page doi:10.1145/3385412.3386012 2020

  34. [34]

    1980.Techniques for program verification

    Charles Gregory Nelson. 1980.Techniques for program verification. Ph. D. Dissertation. Stanford, CA, USA. AAI8011683

    work page 1980

  35. [35]

    Greg Nelson and Derek C. Oppen. 1979. Simplification by Cooperating Decision Procedures.ACM Trans. Program. Lang. Syst.1, 2 (Oct. 1979), 245–257. doi:10.1145/357073.357079

    work page doi:10.1145/357073.357079 1979

  36. [36]

    Michael Paleczny, Christopher Vick, and Cliff Click. 2001. The java hotspotTM server compiler. InProceedings of the 2001 Symposium on JavaTM Virtual Machine Research and Technology Symposium - Volume 1(Monterey, California) (JVM’01). USENIX Association, USA, 1

    work page 2001

  37. [37]

    Wilcox, and Zachary Tatlock

    Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock. 2015. Automatically improving accuracy for floating point expressions. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation(Portland, OR, USA)(PLDI ’15). Association for Computing Machinery, New York, NY, USA, 1–11. doi:10.1145/2737924.2737959

    work page doi:10.1145/2737924.2737959 2015

  38. [38]

    2016.SSA-based Compiler Design(1st ed.)

    Fabrice Rastello. 2016.SSA-based Compiler Design(1st ed.). Springer Publishing Company, Incorporated

    work page 2016

  39. [39]

    Amit Sabne. 2020. XLA : Compiling Machine Learning for Peak Performance

    work page 2020

  40. [40]

    Axel Simon and Andy King. 2010. The two variable per inequality abstract domain.Higher Order Symbol. Comput.23, 1 (March 2010), 87–143. doi:10.1007/s10990-010-9062-8

    work page doi:10.1007/s10990-010-9062-8 2010

  41. [41]

    Taylor Simpson, Keith Cooper, and L. Simpson. 1997. SCC-based value numbering. (02 1997)

    work page 1997

  42. [42]

    Gagandeep Singh, Markus Püschel, and Martin Vechev. 2015. Making numerical program analysis fast. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation(Portland, OR, USA)(PLDI ’15). Association for Computing Machinery, New York, NY, USA, 303–313. doi:10.1145/2737924.2738000

    work page doi:10.1145/2737924.2738000 2015

  43. [43]

    Eytan Singher and Shachar Itzhaky. 2023. Colored E-Graph: Equality Reasoning with Conditions. arXiv:2305.19203 [cs.PL] https://arxiv.org/abs/2305.19203

    work page arXiv 2023

  44. [44]

    Eytan Singher and Shachar Itzhaky. 2024. Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assump- tions. In2024 Formal Methods in Computer-Aided Design (FMCAD). 70–83. doi:10.34727/2024/isbn.978-3-85448-065-5_13

    work page doi:10.34727/2024/isbn.978-3-85448-065-5_13 2024

  45. [45]

    Michael Stepp, Ross Tate, and Sorin Lerner. 2011. Equality-based translation validator for LLVM. InProceedings of the 23rd International Conference on Computer Aided Verification(Snowbird, UT)(CA V’11). Springer-Verlag, Berlin, Heidelberg, 737–742

    work page 2011

  46. [46]

    Dan Suciu, Yisu Remy Wang, and Yihong Zhang. 2025. Semantic Foundations of Equality Saturation. In28th In- ternational Conference on Database Theory (ICDT 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 328), Sudeepa Roy and Ahmet Kara (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 11:1–11:18. doi:10.4...

    work page doi:10.4230/lipics.icdt.2025.11 2025

  47. [47]

    Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality saturation: a new approach to optimization. SIGPLAN Not.44, 1 (Jan. 2009), 264–276. doi:10.1145/1594834.1480915

    work page doi:10.1145/1594834.1480915 2009

  48. [48]

    Todd Veldhuizen and Jeremy Siek. 2003. On Combining Program Improvers. (04 2003)

    work page 2003

  49. [49]

    Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2022. Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers. In2022 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). 254–265. doi:10.1109/CGO53902.2022.9741267

    work page doi:10.1109/cgo53902.2022.9741267 2022

  50. [50]

    Yisu Remy Wang, Shana Hutchison, Jonathan Leang, Bill Howe, and Dan Suciu. 2020. SPORES: sum-product optimiza- tion via relational equality saturation for large scale linear algebra.Proc. VLDB Endow.13, 12 (July 2020), 1919–1932. doi:10.14778/3407790.3407799

    work page doi:10.14778/3407790.3407799 2020

  51. [51]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and extensible equality saturation.Proc. ACM Program. Lang.5, POPL, Article 23 (Jan. 2021), 29 pages. doi:10.1145/3434304

    work page doi:10.1145/3434304 2021

  52. [52]

    Yichen Yang, Phitchaya Mangpo Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy, and Jacques Pienaar

    work page

  53. [53]

    InProceedings of Machine Learning and Systems

    Equality Saturation for Tensor Graph Superoptimization. InProceedings of Machine Learning and Systems. arXiv:2101.01332

    work page arXiv

  54. [54]

    Jiaqi Yin, Zhan Song, Chen Chen, Yaohui Cai, Zhiru Zhang, and Cunxi Yu. 2025. e-boost: Boosted E-Graph Extraction with Adaptive Heuristics and Exact Solving.arXiv preprint arXiv:2508.13020(2025)

    work page arXiv 2025

  55. [55]

    Yihong Zhang. 2022. PLDI: U: Towards a Relational E-graph. https://api.semanticscholar.org/CorpusID:250122313 24 Arbore et al

    work page 2022

  56. [56]

    Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation.Proc. ACM Program. Lang.7, PLDI, Article 125 (June 2023), 25 pages. doi:10.1145/3591239

    work page doi:10.1145/3591239 2023

  57. [57]

    Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock. 2022. Relational e-matching.Proc. ACM Program. Lang.6, POPL, Article 35 (Jan. 2022), 22 pages. doi:10.1145/3498696

    work page doi:10.1145/3498696 2022

  58. [58]

    Philip Zucker. 2024. Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas. https://www.philipzucker.com/ coegraph/

    work page 2024

  59. [59]

    Philip Zucker. 2025. Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching. arXiv:2504.14340 [cs.PL] https://arxiv.org/abs/2504.14340

    work page arXiv 2025