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.