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.

Table of Contents

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

---

Community

• egraphs.org
• zulip
• Community Meetings
• 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

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
• 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

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

Program Synthesis

• 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

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

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)
• KestRel: Relational Verification Using E-Graphs for Program Alignment. EGRAPHS 2023.
• 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

Other

• YOGO Semantic Code Search via Equational Reasoning

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

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

• 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

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
• https://github.com/NationalSecurityAgency/ghidra/blob/2eff37f655159574593b15bc19273915fc780cf2/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
• https://github.com/halide/Halide/blob/2e36da4d7631464272640a2126854748da299d54/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

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

Rule Scheduling

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

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 2024

Accepted Papers

youtube

EGRAPHS 2023

Presentations

EGRAPHS 2022

Accepted papers

youtube

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