When we first reviewed the equality saturation paper, we thought there was one major pro, and one major con: [pro] phase-ordering invariant; [con] at the time there was no (believable) way to extract the transformed graph in a non-hand-wavy-way.
Personally, I think e-graphs should be combined with Massalin superoptimization — they're natural "duals" — and just turn the whole exercise into a hill-climbing process. You can tune the total effort by the set of passes used, the amount of time to drive the graph to saturation, and the method (and time) for graph extraction.
Speaking as an e-graph rookie - I believe so, with caveats.
You can certainly store the chosen extractions/optimizations and re-use any that don't change. For example, if a long chain of rewrites yields A ==> B ==> ... ==> Z, you could short-circuit that and assume that Z is still what you want to replace A with. Perhaps each time you compiled, you could only rewrite the 'changed' sections of the program, along with a randomly selected portion to explore for greater-optimization. (Although, you may just want to go all the way and write a tool that constantly adds to your equivalence DB in the background, with compilation just a matter of running your extraction heuristics.)
You probably wouldn't want to store every possible rewrite, though, as the space complexity or retrieval cost is likely a bigger deal than the time complexity (you wouldn't load 2+2=4 from a database, you'd just do the addition). But, if you restore only a subset of equivalencies that are known to be useful, there's not a simple way to keep the optimization from re-exploring the "rejected candidates" (without shutting off the eclass entirely) - and, it's even not clear to me that you'd want to, as changing program context may end up meaning that M becomes a better replacement candidate for A than Z.
(Boring prerequisites for this approach also include: consistent serialization of terms, avoiding storage of infinite equivalencies, like `A => A + 0 => A + 0 + 0 ==> ...` (and possibly of exponential equivalencies like the kind associativity rules can produce), and strong heuristics to capture "high-value" equivalencies that are both useful and cheaper to lookup than re-derive.)
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.
Personally, I think e-graphs should be combined with Massalin superoptimization — they're natural "duals" — and just turn the whole exercise into a hill-climbing process. You can tune the total effort by the set of passes used, the amount of time to drive the graph to saturation, and the method (and time) for graph extraction.