An egraph is a data structure for storing many ground equalities at once in a highly shared way. Egg style equality saturation searches over this egraph for patterns and asserts nondestructive rewrites into the egraph. Once you’re sick of doing that, you can use extract a best term from the egraph. This may enable you to avoid valleys that greedy rewriting may stick you in and makes the system more robust to the order of rewrites.
