Compiler: Yihong Zhang, with many crowdsourced ideas!

Systems for Equality Saturation

This list is opinionated in that it only includes systems that I know are ready to use. If you know other mature systems, let me know! For a more comprehensive list, check out Phil Zucker’s list.

Systems

Projects that use equality saturation

This page keeps track of research and industry projects that use equality saturation (EqSat), especially those that are based on a modern EqSat library (e.g., egg, Metatheory.jl, egglog).

# projects in each field

Projects that use modern EqSat libraries

Toolbox for Equality Saturation

Variations of the E-graph data structure and Equality Saturation

• ae-graph: adapting E-graph to real-world compilers
  • Cranelift: Using E-Graphs for Verified, Cooperating Middle-End Optimizations
• Colored E-graph: Reasoning with multiple equality relations
  • Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions by Singher and Itzhaky at FMCAD 2024
• Disequality graph: Reasoning with disequality
  • Dis/Equality Graphs by Zakhour, Weisenburger, and Salvaneschi at POPL 2024
• Slotted E-graphs
  • Slotted E-graphs by Schneider, Koehler, and Steuwer at EGRAPHS 2024
• Tree Automata Completion
  • Termination criteria for tree automata completion by Genet
  • Completeness of Tree Automata Completion by Genet
  • Ensuring the termination of equality saturation for terminating term rewriting systems by Zhang and Flatt

Extraction

• extraction-gym: a benchmark for e-graph extraction
• Solver based extraction
  • Many project take this approach. See this paper for an exmaple: Equality Saturation for Tensor Graph Superoptimization by Yang et al.
  • An improvement by He et al: Improving Term Extraction with Acyclic Constraints at EGRAPHS 2023