An e-graph, short for “equality graph,” is a data structure that maintains a congruence relation on expression trees: an equivalence relation stable under forming new expressions. First devised by Nelson and Oppen in 1980 (Nelson 1980; Nelson and Oppen 1980), e-graphs received a surge of new attention when Willsey et al demonstrated, via their software package egg, that e-graphs combined with equality saturation can be a fast, powerful, and adaptable tool for equational reasoning (Willsey...
