The Straight-Line Automatic Programming Problem

superoptimization, code generation, straight-line automatic programming problem The paper presents a design for the Denali-2 super-optimizer, which will generate minimum-instruction-length machine code for realistic machine architectures using automatic theorem-proving technology: specifically, using E-graph matching (a technique for pattern matching in the presence of equality information) and boolean satisfiability solving. The paper presents a precise definition of the underlying automatic programming problem solved by the Denali-2 super-optimizer. It sketches the E-graph matching phase and presents a detailed exposition and proof of correctness of the reduction of the automatic programming problem to the boolean satisfiability problem