An integer set library for program analysis
Sven Verdoolaege · Lirias · 2009
Many program analysis techniques are based on manipulations of sets of integers bounded by linear constraints. These integers typically represent iterations of a loop nest or elements of an array. Double description based libraries have little or no explicit support for parameters and existentially quantified variables, which are essential for some program analysis tasks, and focus on rationals instead of integers. Furthermore, in our applications, the number of constraints describing a set is usually fairly small, while a vertex based description could be very large. We present a new library exclusively based on constraints and geared towards the manipulation of integer sets. The library supports some operations not typically available in other libraries, such as parametric integer linear programming (through PIP) and the computation of the integer affine hull, and produces significantly improved results in some applications. Operations such as the convex hull are more easily implemented using a double description. Both Fourier-Motzkin elimination and "wrapping" have been used to compute the convex hull using only constraints. The first is slow, while the second could only be used on bounded polyhedra. We present an extension of the "wrapping" method to unbounded polyhedra.