Automating Mathematical Program Transformations

Program transformations are often not automated because their definitions do not specify the many details needed to implement them correctly in code. We define two, the conversion of Boolean expressions into integer inequalities and the con- vex hull transformation of disjunctive constraints, using a novel style based on set theory. This treats constraints as syntactic objects, allowing mappings between con- straint spaces to be defined in a precise way. As a result, our definitions are directly amenable to a computer implementation. Examples of our software's input and output are provided.