egg: Easy, Efficient, and Extensible E-graphs

Preprint, April 2020
BibTeX
 @misc{2020-egg,
    title={egg: Easy, Efficient, and Extensible E-graphs},
    author={Max Willsey and Yisu Remy Wang and Oliver Flatt and Chandrakana Nandi and Pavel Panchekha and Zachary Tatlock},
    year={2020},
    eprint={2004.03082},
    archivePrefix={arXiv},
    primaryClass={cs.PL}
}
 
egg logo

egg is available on GitHub, crates.io, and docs.rs.

Abstract

An E-graph is a data structure that can efficiently encode the congruence closure of an equivalence relation over many expressions. E-graphs are used in theorem provers for communicating equalities among theories. Another strand of work proposed their use for rewrite-driven program optimization with a technique called equality saturation.

In this work, we expand on the idea of equality saturation and re-propose E-graphs as a solution to a diverse set of optimization problems, addressing issues identified by past work. We introduce rebuilding, a new, simpler means of maintaining congruence closure that is much faster than current techniques. We propose metadata, a mechanism that enables integration of semantic analyses to the E-graph in addition to syntactic rewrites. We realize these techniques in egg, an easy, efficient, and extensible E-graph library. We highlight published works that use egg across a wide range of optimization-oriented applications.