You don't have to actually saturate the egraph, or compute a globally optimal extraction. There are schemes that drive the rewrite exploration by "expected valu

You don't have to actually saturate the egraph, or compute a globally optimal extraction. There are schemes that drive the rewrite exploration by "expected value" of the rewrite, for example, to avoid bloating the egraph with identities that are probably useless - I'd be surprised if that is much heavier than normal graph rewriting optimizers.