Efficient E-Matching for Super Optimizers

Summary

IntroductionModern theorem provers and optimizing compilers are built on an interesting concept: the ability to recognize when two things are equal, even if they look completely different. It’s not enough to just match the syntax - we need to match the semantics as well. That’s where E-Matching comes in.E-Matching is a pattern matching technique that considers syntactic structures and established equalities. Suppose you’re trying to apply the axiom:The solver must find terms in its database that match f(x). These need to match syntactically, and up to equality. The “E” in E-matching refers to equality reasoning, usually captured using “E-Graphs” or congruence closures.E-matching comes from the world of SMT Solvers, where it’s used to instantiate quantified axioms during the proof search. The general setup is: the solver knows a bunch of constraints and terms, and it’s trying to apply some universal quantified formulas, such as ∀x. f(x) = x. To do this effectively, it needs to search for instances of f(x) inside a big heap of terms - but doing so modulo equality.In solvers like Z3, E-matching is key to making quantifiers tractable. Without it, you’d have to blindly try substitutions or generate ground instances randomly - both of which scale terribly, for the obvious reasons. E-matching provides a middle ground: a way to find promising instantiations by searching through terms that already exist in the solver’s database.Understanding E-Graphs is important to grasping the application of E-Matching in Superoptimization and understanding the next sections. I recommend reading this blog on the subject.The basic idea is quite simple, we have 3 important things to understand.E-Nodes - These represent individual expressions or operations, such as addition or multiplication, within the graph. They sometimes have operands, such as the left and right-hand sides of an addition, and it results in some value or “dependency”.E-Class - E-Classes group the aforementioned E-Nodes tha...