Implied Constraints for the Unison Presolver

Abstract: Unison is a compiler back-end that differs from traditional compiler approaches in that the compilation is carried out using constraint programming rather than greedy algorithms. The compilation problem is translated to a constraint model and then solved using a constraint solver, yielding an approach that has the potential of producing optimal code. Presolving is the process of strengthening a constraint model before solving, and has previously been shown to be effective in terms of the robustness and the quality of the generated code. This thesis presents an evaluation of different presolving techniques used in Unison’s presolver for deducing implied constraints. Such constraints are logical consequences of other constraints in the model and must therefore be fulfilled in any valid solution of the model. Two of the most important techniques for generating these constraints are reimplemented, aiming to reduce Unison’s dependencies on systems that are not free software. The reimplementation is shown to be successful with respect to both correctness and performance. In fact, while producing the same output a substantial performance increase can be measured indicating a mean speedup of 2.25 times compared to the previous implementation.