I always thought that it'd be nice to build an expository version of eq-sat that just operated on straight-line code, and didn't try to use the complicated e-gr

I always thought that it'd be nice to build an expository version of eq-sat that just operated on straight-line code, and didn't try to use the complicated e-graph structure (does it still use pi-nodes? I've not looked at the paper in a decade). The major complexity of eq-sat is in the novel extraction heuristics, and the complicated data-structures only mask that. EDIT: Right. Blech. Theta & Phi nodes.