Equivalence graphs, commonly called e-graphs, provide a dense representation of equivalence classes (e-classes) of expressions [1]}. Often found in theorem provers, this data structure enables a graph optimization technique called equality saturation [2]}, [3]}, [4]}. The e-graph represents expressions, where the nodes, known as e-nodes, represent functions (including variables and constants, as 0-arity functions) and are partitioned into a set of e-classes. The intuition is that e-classes can be used to compactly represent equivalent expressions, whose evaluation always leads to the same result. Edges represent function inputs and are from e-nodes to e-classes; see Figure REF , where dashed lines represent e-class boundaries, solid ellipses are e-nodes and arrows are edges. We define \(\mathcal {C}\)  to be the set of e-classes, \(\mathcal {N}\)  the set of e-nodes and \(E \subseteq \mathcal {N} \times \mathcal {C}\)  the set of edges. We also introduce \(\mathcal {N}_c\)  to denote the set of e-nodes in a given e-class \(c\) .
