Awesome E-Graphs

A curated list of resources related to e-graphs, equality saturation, and their applications. Contributions are welcome! Thanks to Yihong Zhang for the initial list which is complementary to this one and still updated.

Table of Contents

• Awesome E-Graphs
  • Table of Contents
  • Community
  • Implementations
  • General
  • Applications
    • Hardware
    • Program Synthesis
    • Program Optimization
    • Theorem Proving and Verification
    • Other
  • Blog Posts
  • Extraction
  • Scheduling
  • EGRAPHS Workshop
  • Rulesets

---

Community

• egraphs.org
• zulip
• Community Meetings youtube
• PLDI EGRAPHS Workshop

Implementations

• egg
• egglog
• egglog-python
• snake-egg
• Metatheory.jl Julia Library
• hegg Haskell library
• ego OCaml library
• quiche
• egraphs.cpp
• eqsat
• eggmt
• ekege
• Eqlog
• GATlab
• marktoberdorf-egglog
• egraph-sqlite
• egglog-speedrun
• zegg
• prolog egraph
• eggp
• microegg

General

• Fast Decision Procedures Based on Congruence Closure
• Proof-Producing Congruence Closure
• Efficient E-matching for SMT Solvers
• The Chase Revisited
• egg Fast and Extensible Equality Saturation
• egglog Better Together: Unifying Datalog and Equality Saturation
• Small Proofs from Congruence Closure
• Colored E-Graphs arxiv
• Slotted E-Graphs PLDI paper
• E-Graphs, VSAs, and Tree Automata: a Rosetta Stone
• An Evaluation Algorithm for Datalog with Equality
• Algebraic Semantics of Datalog with Equality
• Semantic foundations of equality saturation
• E-graphs Modulo Theories via Bottom-up E-matching
• Dis/Equality Graphs
• E-Graphs with Bindings
• Relational e-graph matching
• Contextual Equality Saturation
• Abstract Congruence Closure
• Congruence Closure Modulo Permutation Equations
• Shostak's congruence closure as completion
• Conditional Congruence Closure over Uninterpreted and Interpreted Symbols
• A Modular Associative Commutative (AC) Congruence Closure Algorithm

Applications

A reverse search on the egg paper on Google Scholar is a good way to stay up to date

Hardware

• ROVER: Combining Power and Arithmetic Optimization via Datapath Rewriting. ARITH 2024.

• Infinity Stream: Portable and Programmer-Friendly In-/Near-Memory Fusion. ASPLOS 2023.

• Lakeroad FPGA Technology Mapping Using Sketch-Guided Program Synthesis repo

• Multiplier Optimization via E-Graph Rewriting

• SEER Super-Optimization Explorer for High-Level Synthesis using E-graph Rewriting

• ESFO Equality Saturation for FIRRTL Optimization

• There and Back Again A Netlist's Tale with Much Egraphin'

• E-Syn Eqsat framework for technology-aware logic synthesis

• BoolE Exact Symbolic Reasoning via Boolean Equality Saturation

• E-morphic Scalable Equality Saturation for Structural Exploration in Logic Synthesis repo

• Equality Saturation for Circuit Synthesis and Verification Samuel Coward Thesis

• Yosys + egglog: Supercharge your passes with Equality Saturation

• EqMap FPGA LUT Remapping using E-Graphs

Program Synthesis

• Szalinski: Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations.
  PLDI 2020.

• Ruler: Rewrite Rule Inference Using Equality Saturation. OOPSLA 2021. Distinguished paper.

• CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. ICFP 2024.

• enumo: Equality Saturation Theory Exploration à la Carte. OOPSLA 2023.

• babble: Learning Better Abstractions with E-Graphs and Anti-unification. POPL 2023.

• MegaLibm: Implementation and Synthesis of Math Library Functions. POPL 2024. Distinguished paper.

• Isaria: Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors. ASPLOS 2024. Best paper.

• srtree A supporting library for tree-based symbolic regression

• TheSy: Theory Synthesizer - a theory exploration tool for inductive equational proofs. paper

Program Optimization

• Herbie: Automatically Improving Accuracy for Floating Point Expressions.
  PLDI 2015. Distinguished paper.

• Felix: Optimizing Tensor Programs with Gradient Descent. ASPLOS 2024.

• aegraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler https://vimeo.com/843540328

• Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations of Functional Programs

• peggy Equality Saturation: A New Approach to Optimization

• optir RVSDG optimizing intermediate representation

• eggcc

• Denali A practical algorithm for generating optimal code

• Glenside Pure Tensor Program Rewriting via Access Patterns

• Simplifying MBA Expression Using E-Graphs

• SPORES sum-product optimization via relational equality saturation for large scale linear algebra

• ∇SD: A Tensor Algebra Compiler for Sparse Differentiation. CGO 2024.

• TenSat: Equality Saturation for Tensor Graph Superoptimization. MLSys 2021.

• PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting. OOPSLA 2024.

• RisingLight: Write a SQL Optimizer using Egg. EGRAPHS 2023.

• Hydro: Optimizing Stateful Dataflow with Local Rewrites. EGRAPHS 2023.

• SpEQ: Translation of Sparse Codes using Equivalences

• ACC Saturator : Automatic Kernel Optimization for Directive-Based GPU Code

• High-performance symbolic-numerics via multiple dispatch

• Q-gym: An Equality Saturation Framework for DNN Inference Exploiting Weight Repetition

• Diospyros: Vectorization for Digital Signal Processors via Equality Saturation. ASPLOS 2021.

• Chassis : Target-Aware Implementation of Real Expressions

• Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search

• Latent Idiom Recognition for a Minimalist Functional Array Language Using Equality Saturation

• Optimizing Regular Expressions via Rewrite-Guided Synthesis

• MLIR egglog

• DialEgg Dialect-Agnostic MLIR Optimizer using Equality Saturation with Egglog video

• Zob Zig optimizing backend

• Database Theory in Action: Search-Based Program Optimization

• cgen compiler backend written in OCaml

• Equality Saturation for Optimizing High-Level Julia IR

• eqsat: An Equality Saturation Dialect for Non-destructive Rewriting

• Target-Aware Implementation of Real Expressions

• MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable Semantics-Driven Optimizations

• Numba v2 Compiler Design

• ACT: Automatically Generating Compiler Backends from Tensor Accelerator ISA Descriptions

• Optimism in Equality Saturation

• Pushing Tensor Accelerators beyond MatMul in a User-Schedulable Language

• E-Graphs as a Persistent Compiler Abstraction

Theorem Proving and Verification

• Most SMT solvers have an e-matching egraph implementation in them
• lean-egg: An Equality Saturation Tactic for Lean. Thesis 2023. (repo) paper
• KestRel: Relational Verification Using E-Graphs for Program Alignment. EGRAPHS 2023. OOPSLA
• cyclegg
• coq congruence
• Fast Approximations of Quantifier Elimination
• Congruence Closure in Intensional Type Theory
• Congruence Closure in Cubical Type Theory
• ZOMBIE: Programming up to Congruence
• GATlab: Modeling and Programming with Generalized Algebraic Theories
• Transforming Optimization Problems into Disciplined Convex Programming Form
• Coquetier a simplification tactic for our Coq toolbox
• Juniper Lean + egg CAS
• Proving properties of functional programs by equality saturation

Other

• YOGO Semantic Code Search via Equational Reasoning

• VyZX: Formal Verification of a Graphical Quantum Language with automated structural rewrites.
  Thesis 2023.

• Maletskyi and Shymanskyi: Genome Compression Using Program Synthesis.
  IDDM 2023.

• Cornelius: Equivalent and redundant mutant detection with e-graphs!!!

• MetaEmu: An Architecture Agnostic Rehosting Framework for Automotive Firmware.
  CCS 2022.

• wasm-evasion: WebAssembly diversification for malware evasion.
  COSE 2023.

• Guided Equality Saturation: Improve performance/capabilities by using guides in a semi-automatic equality saturation process. POPL 2024.

• Novel Algorithms for Computing Correlation Functions of Nuclei

• rEGGression: an Interactive and Agnostic Tool for the Exploration of Symbolic Regression Models

• eggshell Wrapper around egg with various TRS implementations for ML

• egg-bench Benchmark problems for egraphs

• Metamorphic Testing for Infrastructure-as-Code Engines

Extraction

• extraction-gym
• E-Graphs as Circuits, and Optimal Extraction via Treewidth
• Notes on the scheduling and extraction problems of EqSat
• Answer Set Programming for E-Graph DAG extraction
• Fast and Optimal Extraction for Sparse Equality Graphs
• SmoothE Differentiable E-Graph Extraction
• e-boost e-boost: Boosted E-Graph Extraction with Adaptive Heuristics and Exact Solving
• ESACO Fast E-Graph Extraction via Orchestrated Simulated Annealing-based Local Search and Ant Colony Optimization-based Global Search

Scheduling

• Learned Graph Rewriting with Equality Saturation: A New Paradigm in Relational Query Rewrite and Beyond

Blog Posts

• The e-graph data structure: A gradual introduction
• The Theoretical Aspect of Equality Saturation
• Acyclic Egraphs and Smart Constructors
• Gauss and Groebner Egraphs: Intrinsic Linear and Polynomial Equations
• What's in an e-graph?
• Improving MBA Deobfuscation using Equality Saturation
• Automating Transport with Univalent E-Graphs
• Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas
• Binding in E-graphs
• Specializing Python with E-graphs
• Efficient E-Matching for Super Optimizers
• The Promise of P-Graphs Polynomials + e-graphs
• Solving Cryptic Crosswords with Egraphs
• Monus, Factor, and Thinning Union Finds
• Weighted Union Find and Ground Knuth Bendix Completion
• An Inequality Union Find Inspired by Atomic Asymmetric Completion
• Verified Code Optimization in Lean 4: How Equality Saturation Generates Proven-Correct C Code with AMO-LEAN
• The acyclic e-graph: Cranelift's mid-end optimizer

Talks

• egg: Fast and Extensible Equality Saturation
• Better Together: Unifying Datalog and Equality Saturation (PLDI 2023)
• egglog Tutorial (EGRAPHS 2023) | Next Generation Egraphs
• egglog: E-Graphs in Python
• ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler
• E-Graphs and Automated Reasoning: Looking Back to Look Forward

EGRAPHS Workshop

EGRAPHS 2025

Accepted Papers

EGRAPHS 2024

Accepted Papers

youtube

EGRAPHS 2023

Presentations

EGRAPHS 2022

Accepted papers

youtube

Rulesets

Pointers to the actual files are preferred. Human readable tables and imperative implementations are ok. It is all on a spectrum. A goal is to move these rules into more declarative and machine executable forms. Often files are in benchmarks or test directories

See Where are all the rewrite rules?

Human Readable

• https://personal.math.ubc.ca/~cbm/aands/ Abramowitz and Stegun: Handbook of Mathematical Functions
• https://en.wikipedia.org/wiki/Summation#Identities
• https://en.wikipedia.org/wiki/List_of_trigonometric_identities
• https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
• https://gappa.gitlabpages.inria.fr/gappa/theorems.html Gappa floating point rules

Imperative

• https://github.com/Boolector/boolector/blob/master/src/btorrewrite.c Boolector rewrites
• https://github.com/YosysHQ/yosys/tree/main/passes/opt Yosys opt
• https://github.com/llvm/llvm-project/tree/main/llvm/lib/Transforms/InstCombine LLVM InstCombine peephole optimizations
• 2eff37f655/Ghidra/Features/Decompiler/src/decompile/cpp/rulecompile.cc Ghidra rewrites

Declarative

• https://github.com/egraphs-good/egg/tree/main/tests egg test files
• https://github.com/egraphs-good/egglog/tree/main/tests Egglog test files
• https://github.com/uwplse/ruler/tree/main/tests Ruler
• https://github.com/herbie-fp/herbie/blob/main/src/core/rules.rkt Herbie floating point rules
• https://rulebasedintegration.org/ Rubi rule based integration
• https://fungrim.org/ The Mathematical Functions Grimoire
• https://www.philipzucker.com/rust-category/ Category theory
• https://github.com/mgree/katbury Kleene Algebra
• https://github.com/philzook58/Catlab.jl/blob/master/src/theories/Monoidal.jl Catlab.jl category theory
• https://gitlab.com/haroldaptroot/haroldbot/-/blob/main/prooffinder.js?ref_type=heads Bitvector rewrites
• https://github.com/TermCOMP/TPDB The termination competition
• https://sourcesup.renater.fr/scm/viewvc.php/rec/2019-CONVECS/ Rewrite engine competition
• https://github.com/bytekid/mkbtt/tree/master/input mkbtt Knuth Bendix completion solver tests
• https://www.tptp.org/ TPTP UEQ. How to collect these up?
• https://github.com/nick8325/twee/tree/master/tests Twee Tests
• https://github.com/ndmitchell/hlint/blob/master/data/hlint.yaml HLint
• https://github.com/golang/go/tree/master/src/cmd/compile/internal/ssa/_gen Go compiler
• https://github.com/bytecodealliance/wasmtime/blob/main/cranelift/codegen/src/isa/riscv64/inst.isle Cranelift Riscv64 isle
• https://github.com/cvc5/cvc5/blob/main/src/theory/bv/rewrites CVC5 RARE files
• https://github.com/gcc-mirror/gcc/blob/master/gcc/match.pd GCC rewrites
• https://github.com/llvm/llvm-project/blob/main/mlir/lib/Dialect/Arith/IR/ArithCanonicalization.td MLIR Canonicalizer files
• https://github.com/cucapra/diospyros/blob/master/src/dios-egraphs/src/rules.rs Diospyros
• 2e36da4d76/src/Simplify_Sub.cpp Halide Simplify_* files
• https://github.com/Bastacyclop/egg-sketches/blob/main/examples/bench_tiling.rs
• https://github.com/rise-lang/shine/blob/main/src/main/scala/rise/eqsat/rules.scala RiSE scheduling
• https://github.com/uwplse/tensat/blob/master/src/rewrites.rs Tensat
• https://github.com/yihozhang/szalinski-egglog/tree/main/egglog_src/rules Szalinski egglog
• https://github.com/caviar-trs/caviar/tree/main/src/rules Caviar rules
• https://github.com/mrocklin/matrix-algebra Matrix algebra in Maude
• https://github.com/risinglightdb/risinglight/blob/main/src/planner/rules/plan.rs RisingLight DB
• https://gist.github.com/manasij7479/2ad0f7f058503ae60de30e4bfb30c917 Hydra peephole rules
• https://github.com/ADAPT-uiuc/TensorRight/tree/master/rules TensorRight
• https://github.com/gussmith23/glenside/blob/main/src/language/rewrites.rs Glenside