cr1901: equivalence graph, they are a classic data structure in smt solvers that allows reasoning about things like functions and arrays. smt can broadly be thought of as two layers (particularly if we ignore quantifiers), there is a set of theories (e.g. bitvectors, linear arithmetic, etc). relations between terms then become atoms (of type Bool), which are related in either propositional logic for quantifier free fragments or first order if you add quantifiers
e.g in some vague pseudocode
```
// Introduce two terms a and b in the theory of ints
int a
int b
// introduce an atom that is true if a is less than b
atom a_lt_b = a < b
// introduce a similar atom for b less than a
atom b_lt_a = b < a

// Add something we want to make true in any satisfying assignment
atom a_lt_b_and_b_lt_a = a_lt_b && b_lt_a
assert a_lt_b_and_b_lt_a

// This will return unsat as there is no model for a and b that makes both those atoms true
checksat
```

The e-graph allows reasoning about equivalences over terms without ever looking inside the terms, e.g. if we have `a == b` and `f(a) == 10` we can deduce `f(b) == 10` without ever looking at f