egg: Fast and Extensible Equality Saturation

I was just skimming this to understand their relation to VSAs, but some more quick notes:

The paper summarizes e-graphs and their usage in equality-saturation. Then, they introduce "rebuilding", which is an optimization that defers e-graph invariant maintenance for better performance. They also introduce a generalized "e-class analysis" mechanism that makes working with e-graphs easier.

Equality-saturation: given an input program P, using rewrite rules to build an e-graph of many equivalent programs. Then, some heuristic is used to choose the best program from the set.

One thing that makes equality-saturation difficult is that even relatively simple transformations such as constant-folding or free-variable analysis can be difficult to implement over e-graphs.

The deferred invariant maintenance method was not useful previously because e-graphs were used in theorem provers where backtracking is used (how?). Equality saturation doesn't have backtracking so this optimization is very effective (dozens of times faster!). It seems like `egg`

wouldn't work for theorem provers unless you can just rebuild after every operation.