This is a Massalin superoptimizer.
https://en.wikipedia.org/wiki/E-graph
Google fodder:
"Equality Saturation: A New Approach to Optimization"
"Denali: A Goal-directed Superoptimizer"
"Z3: An Efficient SMT Solver"
"Efficient E-matching for SMT Solvers"
"egg: Fast and Extensible Equality Saturation"
"Rewrite Rule Inference Using Equality Saturation"
Still a nice result. It looks like a dynamic programming solution to code generation.
Next to the game boy. ;-)