Pith. sign in

REVIEW 5 major objections 6 minor 2 cited by

E-Graphs as a Persistent Compiler Abstraction

T0 review · 5 major / 6 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read This paper argues that an e-graph — the data structure that records all equivalent expressions found by equality saturation — can be embedded directly into a compiler's intermediate representation and persist across the whole compilation fl

desk verdict The eqsat dialect is a genuinely new design for embedding e-graphs in MLIR, but the paper's central persistence claim is not demonstrated; the evaluation is a single isolated saturation pass, and the abstract promises results the full text never reports. read the letter →

arxiv 2602.16707 v2 pith:EBVB2T2Z submitted 2026-02-18 cs.PL

Jules Merckx , Alexandre Lopoukhine , Samuel Coward , Jianyi Cheng , Bjorn De Sutter , Tobias Grosser This is my paper
classification cs.PL MSC 68N20
keywords equalitysaturatione-graphcompilerintermediaterepresentationSSApatternrewritingphase-orderingprobleme-classanalysisfloating-pointaccuracy
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Equality saturation usually lives outside the compiler: a tool builds an e-graph, rewrites it, extracts one best expression, and hands back a single answer, discarding all other equivalences. The paper tries to change that by encoding the e-graph itself as operations in the compiler's intermediate representation, introducing a small dialect — e-graph wrapper, e-class, constant e-class, and yield — so the e-graph persists across passes. If this works, compiler developers can interleave equality saturation with other transformations such as lowering, inlining, and constant folding, mitigating the phase-ordering problem because alternatives are never lost. The authors support the idea by reimplementing the equality-saturation stage of a floating-point accuracy tool, matching the original's accuracy on most benchmarks and showing that combined pattern matching gives speedups over per-pattern matching.

What carries the argument

The load-bearing machinery is the eqsat dialect built on SSA: eqsat.egraph wraps a region in a graph region (allowing cyclic use-def edges, which appear when rewriting x+0 to x folds into a cycle); eqsat.eclass groups one or more equivalent values into an e-class; eqsat.const_eclass wraps constants so existing constant folding works; eqsat.yield exposes chosen e-classes to surrounding code. Rewriting is done by a reinterpreted pattern-language interpreter: it backtracks over e-class members, reorders semantic checks to avoid exponential backtracking blowup, inserts a choose operation to isolate backtracking between different patterns, and converts destructive replace into constructive 'add t

What would settle it

Run the proposed pipeline on a loop-carried computation, with equality saturation before and after a loop transformation such as unrolling: if the second saturation phase cannot see (or reconstruct) the equalities created in the first, because the intervening transformation destroyed the e-class structure, then the e-graph did not actually persist across the compilation flow.

Watch

Extended reading notes

Core claim

The central claim is that an e-graph need not be a separate data structure that the compiler talks to; it can be the IR itself. The paper's eqsat dialect represents each equivalence class as an operation, ordinary compute operations point at e-class results, and a graph-region wrapper permits cycles, so the full equality-saturation machinery — matching, congruence rebuilding, extraction — operates directly on the program. Because the e-graph is made of ordinary IR operations, existing analyses and passes can see it, and extraction can be partial: a cost model can select the best member of some e-classes now and others later. The case study demonstrates the approach can reproduce the core of

Load-bearing premise

The whole approach is only implemented and tested for pure, straight-line functions; the paper explicitly leaves loops, branches, and control-flow rewrites for future work, so the broader claim that the e-graph persists across abstraction levels rests on the assumption that real pipelines can be handled without these.

Editorial extensions

If this is right

  • E-classes remain in the IR after equality saturation ends, so a later pass can exploit equalities that an earlier extraction ignored.
  • The same declarative rewrite patterns used for ordinary lowering work for equality saturation, with no separate ruleset or translation layer.
  • Existing dataflow analyses become e-class analyses by defining e-class as the meet of its members, so interval analysis and friends run on e-graphs without new infrastructure.
  • Extraction is composable: greedy or integer-linear-programming selection can be run now, and a different cost model can finish the job later, enabling trade-offs such as performance versus floating-point accuracy.
  • Combining all patterns into a single matching routine is measurably faster than applying them one at a time — the paper measures 2.34× on a small ported test suite and 2.57× on the floating-point case study's saturation phase.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If region-level rewrites are enabled (the paper names this as future work), equality saturation could restructure loops and conditionals themselves, not just straight-line bodies — that would be a genuinely new capability for compiler IRs.
  • A persistent e-graph opens the door to multi-stage, multi-cost extraction: a high-level pass could pick a numerically stable form, lower it, and a later pass with the same e-graph could revisit the choice when actual hardware costs are known.
  • The large slowdown measured against the specialized reference implementation stems largely from the Python prototype and 1024-bit high-precision evaluation; a compiled implementation along the lines the paper sketches would likely bring the persistent-e-graph approach into practical range.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 6 minor

Summary. This paper proposes representing e-graphs directly in the compiler IR by introducing an `eqsat` dialect in MLIR/xDSL, with operations `eqsat.egraph`, `eqsat.eclass`, `eqsat.const_eclass`, and `eqsat.yield`. The authors reinterpret PDL-based pattern matching as e-matching, add a `choose` operation and eager semantic checks to avoid backtracking blowup, implement rebuilding and extraction as compiler passes, and lift existing dataflow analyses to e-class analyses. As the main evaluation, they replicate Herbie's equality saturation phase on 31 FPBench benchmarks, reporting accuracy close to Herbie on most benchmarks, a 2.57x speedup from combined matching, and a 401x overall slowdown relative to Herbie. The paper claims that this design enables persistent e-graphs across compilation phases and abstraction levels, helping mitigate the phase-ordering problem.

Significance. If the central claim holds, the paper makes a useful systems contribution: embedding e-graphs in an extensible SSA-based IR and reusing existing rewrite infrastructure (PDL) and dataflow analyses is a promising way to lower the barrier to equality saturation in real compilers. The Herbie replication is a nontrivial feasibility demonstration, and the careful description of the matcher reordering and the `choose` extension shows real engineering insight. I also see no circularity in reusing Herbie's rules and benchmarks; that is a legitimate replication test. However, the paper's headline claim — that the e-graph persists across phases and abstraction levels, interleaved with other compiler transformations — is not actually demonstrated by the included experiments. The abstract also promises software and hardware speedups that do not appear in the full text. The significance is therefore conditional on either adding the missing experiments or substantially narrowing the claims.

major comments (5)
  1. [Abstract, §1, §5] The abstract claims a software case study improving performance by 1.18x on average and a hardware case study reducing circuit delay by up to 11% over standard equality saturation. Neither experiment appears anywhere in the full text. Section 5 contains only the Herbie accuracy/runtime study. These are not presentation details: the claimed speedups are the concrete evidence for the persistence/interleaving benefit. The authors must either include the missing experiments or remove/qualify these claims in the abstract and introduction.
  2. [§5, Figure 6] The case study does not exercise persistence across compilation phases or abstraction levels. The flow in Figure 6 creates one eqsat.egraph from FPCore input, runs equality saturation to a 4000 e-node limit, extracts, and stops. No unrelated MLIR pass (e.g., inlining, CSE, or a lowering pass) is interleaved with a live e-graph, and all rewrites occur at essentially one level of abstraction. The §2 motivating example combines lowering and optimization rules inside a single saturation loop, but simultaneous multi-abstraction rewriting is not the same as persistence across pipeline phases. Since the central claim is that the e-graph persists and is interleavable with other transformations, this is a load-bearing gap that needs a direct experiment.
  3. [§4.1, §8] The implementation is explicitly restricted to pure, straight-line functions; the authors state that rewriting processes and extraction are not yet aware of scopes, and §8 says the pdl dialect cannot currently match regions or rewrite control-flow operations. This is an acknowledged limitation, but it directly narrows the paper's headline generality. Real MLIR pipelines routinely contain loops, branches, and nested regions, so the abstraction's persistence across a realistic compilation flow remains unsubstantiated. The paper should either demonstrate a control-flow-containing example or clearly reposition the contribution as a straight-line subset.
  4. [§5, Figure 7] The accuracy comparison appears to be a single run per benchmark, with no confidence intervals, repeated trials, or error bars. The paper itself notes nondeterminism introduced by the e-node limit and possible ordering effects: 'It is possible that a different ordering of rewrites would lead to other rules being applied, leading to a more accurate result by chance.' With such nondeterminism, the claim that the implementation 'matches Herbie's accuracy on most benchmarks' needs statistical support, or at the very least a discussion of run-to-run variance.
  5. [§5, Figure 8] The 401x geometric-mean slowdown is explained by Python/xDSL overhead and the fixed 1024-bit MPFR evaluation, with only 18.6% of runtime spent in equality saturation. This is acceptable as a feasibility demonstration, and the 2.57x speedup from combined matching is a meaningful micro-result. However, the large slowdown means the practical benefits of the persistent-e-graph approach remain speculative until an optimized implementation exists. The paper should make this caveat more prominent in the abstract and conclusion, not only in the runtime paragraph.
minor comments (6)
  1. [§1] 'expressability' should be 'expressibility'.
  2. [§5 Runtime] 'perfomance' is a typo for 'performance'.
  3. [§4.1] 'Alleqsat.eclass operations' should be 'All eqsat.eclass operations'.
  4. [§4.2.1] The semantics of eqsat_pdl_interp.choose are described only schematically; a small concrete example showing how the choose operation interacts with the existing pdl_interp backtracking stack would make the presentation much clearer.
  5. [§5, Figures 7-9] The benchmark names on the x-axes are small and may be unreadable after typesetting; a table with the exact NMSE values and timings would improve reproducibility.
  6. [§5] The paper says all benchmarks hit the 4000 e-node limit and thus saturation is never reached. This should be stated more prominently, since it means the comparison is against Herbie with a resource-limited run, not a saturating equality saturation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the eqsat representation is not derived from its evaluation, and the Herbie replication is a benchmark comparison, not a fitted prediction.

full rationale

The paper's central contribution is a representation (eqsat embedded in MLIR IR) plus an implementation/replication study, not a derivation whose output is loaded into its own premise. The load-bearing claims are about expressivity and persistence, and they are not established by circular reasoning: the eqsat dialect is defined in terms of IR constructs (eclass, const_eclass, egraph, yield), not in terms of the accuracy results; no parameter is fitted to Herbie's outputs and then renamed as a prediction. Reusing Herbie's rewrite rules and the FPBench contributed benchmarks to show parity is a standard replication test: the paper does not claim to predict Herbie's accuracy from Herbie's rules as a novel result, but rather to demonstrate that the same rules can be executed inside their dialect. Self-citations are present but not load-bearing: xDSL [12] is cited as the prototyping substrate, and [15]/[18] appear only as future-work pointers; none is invoked as an external uniqueness theorem or as the justification for the central persistence claim. The manuscript itself flags the main limitations: Section 4.1 says 'In our implementation of e-class insertion, we focus on pure, straight-line functions' and Section 8 says 'we do not explore applying equality saturation code with structured control flow.' These are genuine support gaps for the broad persistence/interleaving claim, as is the absence in the full text of the abstract's promised 1.18x software speedup and 11% hardware delay reduction. But unsupported or under-evaluated claims are not circularity. No specific reduction from claim to input, no self-definitional equation, and no fitted-input-called-prediction step could be identified, so the appropriate score is 0.

Assumptions & free parameters 3 free parameters · 4 assumptions · 2 invented entities

The central claim is a systems/engineering contribution rather than a fitted model. The genuinely ad hoc numbers are resource limits and precision choices in the evaluation, not parameters fit to make a derivation work. The rewrite rules and MLIR graph-region semantics are inherited from prior work. The eqsat dialect and its choose extension are new entities whose only evidence in this paper is the descriptive case study, since no artifact is shipped.

free parameters (3)
  • E-node limit = 4000 e-nodes
    Herbie comparison caps e-graph growth at 4000 e-nodes; the authors state all benchmarks hit this cap, so accuracy results and nondeterminism depend on this hand-chosen limit.
  • MPFR precision = 1024 bits
    Ground-truth evaluation uses a fixed 1024-bit MPFR precision; this affects runtime and the accuracy of ground-truth comparisons.
  • Maximum iterations in matcher benchmark = 5 iterations
    The small egg-test-suite comparison runs equality saturation for at most 5 iterations or until saturation; the reported 2.34× speedup depends on this cap.
assumptions (4)
  • domain assumption MLIR graph regions can represent cyclic use-def chains and hence cyclic e-graphs.
    Section 3.1 and Section 4.1 rely on this standard MLIR property; no proof is given, but it is built into the framework used.
  • domain assumption The Herbie/egglog rewrite rules preserve real-arithmetic equivalence when their interval-analysis preconditions hold.
    Section 5 imports the egglog ruleset as the rewrite set; the paper does not re-prove soundness of these rules.
  • ad hoc to paper PDL pattern matching can be faithfully reinterpreted as e-matching by handling eqsat.eclass indirection and backtracking.
    Section 4.2.1 describes the reinterpretation and optimizations, but no formal correctness argument is given that the modified interpreter exactly implements e-matching.
  • ad hoc to paper Pure, straight-line functions are sufficiently expressive to validate the persistent-equality-saturation claim.
    Section 4.1 explicitly restricts the implementation to pure straight-line functions and states control flow is unexplored; the broader claim depends on this restriction being unproblematic.
invented entities (2)
  • eqsat dialect operations (eqsat.egraph, eqsat.eclass, eqsat.const_eclass, eqsat.yield)
    purpose: Represent e-graphs natively in MLIR/xDSL IR so they can persist and be rewritten constructively.
    No public artifact or formal semantics is provided; evidence is the descriptive case study in this paper. Independent reimplementation is possible but not yet demonstrated.
  • eqsat_pdl_interp.choose
    purpose: Isolate backtracking points from different patterns to avoid exponential e-matching blowup.
    Introduced as an extension to pdl_interp; performance evidence is the small benchmark and the 2.57× speedup in Section 5, but no standalone artifact or formal model accompanies it.

how reviews work

0 comments
Cite this review

Pith. "Pith review of E-Graphs as a Persistent Compiler Abstraction." pith.science (2026). https://pith.science/paper/EBVB2T2Z

@misc{pith2026260216707,
  author       = {Pith},
  title        = {Pith review of: E-Graphs as a Persistent Compiler Abstraction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EBVB2T2Z}},
  note         = {Machine review of arXiv:2602.16707}
}
abstract

Recent algorithmic advances have made equality saturation an appealing technique for program optimization, avoiding the phase-ordering problem by separating the discovery of equivalent expressions from optimal expression selection. Existing work leveraging equality saturation in compilers uses either external equality saturation libraries or custom implementations that are coupled to the specific application. These approaches are inherently limited, as the first discards semantic equivalences when translating back from the external library, while the second restricts equality saturation to a single level of abstraction. We propose an alternative approach that represents an e-graph natively in code, facilitating the application of constructive compiler passes that maintain the e-graph state throughout the compilation flow. We present Tamagoyaki, an implementation of this approach in MLIR and demonstrate its versatility through partial re-implementations of two equality saturation applications. Our software case study improves performance by 1.18$\times$ on average, whilst our hardware case study reduces circuit delay by up to 11% over standard equality saturation. Building on reusable compiler infrastructure, our work expands the scope of equality saturation, making it persistent across and interleavable with other analyses and transformations.

Figures

Figures reproduced from arXiv: 2602.16707 by the authors.

Figure 1
Figure 1. Existing work targets a single abstraction, either: (b) orchestrating external equality saturation libraries, [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. An IR that incorporates user-extensibility as a [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. (left) In MLIR’s default, destructive pattern rewriting framework, the [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: A comparison between pdl_interp matching code without and with eager semantic checks. The interpreter inserts backtracking points (•) at each pdl_interp.get_defining_op. By carrying out semantic checks as soon as possible, an exponential blowup in the number of backtra…
Figure 5
Figure 5. Figure 5: By introducing a choose operation in the matching code, backtracking points from different patterns can be separated, avoiding exponential growth. Optimizing matchers. While semantically correct, simply reusing the lowering pass that converts declarative pdl patterns i…
Figure 6
Figure 6. Figure 6: Using a combination of existing and new compiler transformations, and analyses, we replicate a single [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]
Figure 7
Figure 7. Figure 7: We are able to match the accuracy of Herbie on most benchmarks. Differences in accuracy are due to [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: Our implementation is significantly slower than Herbie. This is largely due to performance optimiza [PITH_FULL_IMAGE:figures/full_fig_p017_8.png]
Figure 9
Figure 9. Figure 9: Running equality saturation with all pdl patterns combined into a single pdl_interp leads to signifi￾cant speedups compared to matching each pattern individually. workflow, the developer must initially identify potentially unstable mathematical expressions in their cod…

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

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

  1. LLM-Guided Strategy Synthesis for Scalable Equality Saturation

    cs.AI 2026-04 unverdicted novelty 6.0 of 10

    EggMind automates EqSat strategy synthesis via LLMs and EqSatL, cutting final cost 45.1% and peak RAM 69.1% versus full equality saturation on vectorization benchmarks while transferring to tensor compilers.

  2. Reading AI Model Compilation in MLIR Through the Lens of Formal Theories

    cs.PL 2026-06 unverdicted novelty 3.0 of 10

    MLIR concepts such as match-and-rewrite and staged lowering correspond to established formal theories, providing a basis for more principled abstraction design in compiler infrastructure.

Reference graph

Works this paper leans on

31 extracted references · 3 canonical work pages · cited by 2 Pith papers

  1. [1]

    GCC, the GNU Compiler Collection - GNU Project

    2024. GCC, the GNU Compiler Collection - GNU Project. https://gcc.gnu.org/

    2024

  2. [2]

    Aho, Monica S

    Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (second ed.). Addison-Wesley

    2006

  3. [3]

    Bytecode Alliance. 2024. Cranelift. https://cranelift.dev

    2024

  4. [4]

    Apple Inc. 2024. The Swift Programming Language . https://docs.swift.org/swift-book/documentation/the-swift- programming-language/ Version 6.1

    2024

  5. [5]

    Aart Bik, Penporn Koanantakool, Tatiana Shpeisman, Nicolas Vasilache, Bixia Zheng, and Fredrik Kjolstad. 2022. Compiler support for sparse tensor computations in MLIR. ACM Transactions on Architecture and Code Optimization (TACO) 19, 4 (2022), 1–25

    2022

  6. [7]

    Jianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho, and Theo Drane. 2024. SEER: Super-Optimization Explorer for HLS using E-graph Rewriting with MLIR. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems . Association for Computing Machinery, La Jolla, CA, 1029–1044. do...

    arXiv 2024

  7. [8]

    Constantinides, and Theo Drane

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

    arXiv 2023

  8. [9]

    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 43 (2024), 4687–4700. doi:10.1109/TCAD.2024.3410154

    arXiv 2024

Show all 31 references
  1. [10]

    Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, and Zachary Tatlock

  2. [11]

    Leonardo De Moura and Nikolaj Bjørner. 2007. Efficient E-matching for SMT solvers. In Proceedings of the 21st International Conference on Automated Deduction: Automated Deduction , Vol. 4603 LNAI. Springer-Verlag, Bremen, 183–198. doi:10.1007/978-3-540-73595-3{_}13

    2007 doi

  3. [13]

    Laurent Fousse, Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. 2007. MPFR: A multiple- precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33, 2 (June 2007), 13–es. doi:10.1145/1236463.1236468

    2007

  4. [14]

    Amir Kafshdar Goharshady, Chun Kit Lam, and Lionel Parreaux. 2024. Fast and Optimal Extraction for Sparse Equality Graphs. In Proceedings of the ACM on Programming Languages . Association for Computing Machinery, 2551–2577. doi:10.1145/3689801

    2024 doi

  5. [15]

    Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, and Michel Steuwer. 2024. Guided Equality Saturation. Proceedings of the ACM on Programming Languages 8, POPL (1 2024), 1727–1758. doi:10.1145/3632900

    2024 doi

  6. [16]

    Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, CGO . IEEE, 75–86. doi:10.1109/CGO.2004.1281665

    2004 arXiv

  7. [17]

    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. In 2021 IEEE/ACM International Sympos...

    2021

  8. [18]

    Alexandre Lopoukhine, Federico Ficarelli, Christos Vasiladiotis, Anton Lydike, Josse Van Delm, Alban Dutilleul, Luca Benini, Marian Verhelst, and Tobias Grosser. 2025. A Multi-level Compiler Backend for Accelerated Micro-kernels Targeting RISC-V ISA Extensions. In Proceedings ...

    2025

  9. [19]

    Charles Gregory Nelson. 1980. Techniques for program verification. Ph. D. Dissertation. Stanford University

    1980

  10. [20]

    Rachit Nigam, Samuel Thomas, Zhijing Li, and Adrian Sampson. 2021. A compiler infrastructure for accelerator generators. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (Virtual, USA) (ASPLOS ’21)...

    2021

  11. [21]

    Pavel Panchekha, Alex Sanchez-Stern, James R Wilcox, and Zachary Tatlock. 2015. Automatically improving accuracy for floating point expressions. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Vol. 50. Association for Comput...

    2015

  12. [22]

    Rui Pereira, Marco Couto, Francisco Ribeiro, Rui Rua, Jácome Cunha, João Paulo Fernandes, and João Saraiva. 2021. Ranking programming languages by energy efficiency. Science of Computer Programming 205 (2021), 102609. doi:10. 1016/j.scico.2021.102609

    2021

  13. [23]

    Brett Saiki, Jackson Brough, Jonas Regehr, Jesus Ponce, Varun Pradeep, Aditya Akhileshwaran, Zachary Tatlock, and Pavel Panchekha. 2025. Target-Aware Implementation of Real Expressions. In Proceedings of the 30th ACM International Conference on Architectural Support for Progra...

    2025

  14. [24]

    Glenn Sun, Yihong Zhang, and Haobin Ni. 2024. E-Graphs as Circuits, and Optimal Extraction via Treewidth. https://arxiv.org/abs/2408.17042

    2024 arXiv

  15. [25]

    Robert Endre Tarjan. 1975. Efficiency of a Good But Not Linear Set Union Algorithm. Journal of the ACM (JACM) 22, 2 (1975). doi:10.1145/321879.321884

    1975

  16. [26]

    Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality saturation: A new approach to optimization. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , Vol. 44. Association for Computing Machinery, 264–276...

    2009

  17. [27]

    Nicolas Vasilache, Oleksandr Zinenko, Aart JC Bik, Mahesh Ravishankar, Thomas Raoux, Alexander Belyaev, Matthias Springer, Tobias Gysi, Diego Caballero, Stephan Herhut, et al. 2022. Composable and modular code generation in MLIR: A structured and retargetable approach to tenso...

    2022 arXiv

  18. [28]

    Yisu Remy Wang, Shana Hutchison, Jonathan Leang, Bill Howe, and Dan Suciu. 2020. SPORES: Sum-product optimization via relational equality saturation for large scale linear algebra. Proceedings of the VLDB Endowment 13, 11 (2020), 1919–1932. doi:10.14778/3407790.3407799

    2020

  19. [29]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. Egg: Fast and extensible equality saturation. In Proceedings of the ACM on Principles of Programming Languages , Vol. 5. Association for Computing Machinery. doi:10.1145/3434304

    2021 doi

  20. [30]

    Abd-El-Aziz Zayed and Christophe Dubach. 2025. DialEgg: Dialect-Agnostic MLIR Optimizer using Equality Saturation with Egglog. In Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization (Las Vegas, NV, USA)(CGO ’25). Association for Computi...

    2025 doi

  21. [31]

    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. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 468–492. doi:10.1145/3591239

    2023 doi

  22. [32]

    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

    2022 doi

  23. [2017]

    In Numerical Software Verification, Vol

    Toward a standard benchmark format and suite for floating-point analysis. In Numerical Software Verification, Vol. 10152 LNCS. Springer, 63–77. doi:10.1007/978-3-319-54292-8{_}6

    doi

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.