Can you explain what you mean by residuation here? But anyway, what you describe is maybe not entirely unlike equality saturation: https://www.cs.cornell.edu/~

Can you explain what you mean by residuation here? But anyway, what you describe is maybe not entirely unlike equality saturation: https://www.cs.cornell.edu/~ross/publications/eqsat/ https://www.cs.cornell.edu/~ross/publications/eqsat/ The idea is to apply a whole bunch of optimizations in parallel, but in a non-destructive fashion. So instead of changing "x * 5" to "x << 2 + x" or whatever, you just note that both are equivalent ways of expressing the same. Then you go on applying optimizations to both variants. At some point you stop and end up with a soup that contains many many different computations that all do the same thing. Then you apply a solver once to pick out an optimal variant. The trick is to make this scale.