7. A Sixth Issue: Finite Union of Polyhedra

Arnauld LESERVOT, in his dissertation, has used the domain of lists of polyhedra [LES96]. Starting from the fact that all Presburger formulae can be represented in Disjunctive Normal Form (DNF) or Conjunctive Normal Form (CNF), an element of the domain can have two representations based on convex polyhedra.

The set of lists of polyhedra, with its operations like union, difference, inclusion, equality between two elements, emptiness test as well as conversion from one form to another, forms an abstract domain, which has been implemented in PIPS for the computation of Array Data Flow Graphs [LES96]. It is only used in PIPS for exact convex array region computation [CI96], and its operator signatures are unfortunately not compatible with polyhedral ones. For example, the satisfiability test does not use homogeneous names for functions: the disjunction of constraint systems has the function boolean dj_empty_p, whereas a constraint system has the function boolean sc_feasibility_p and boolean sc_empty_p has a different semantic .

As mentioned before, this interface is not taken into account for HQ. This abstract domain is less powerful than the Presburger formulae since it cannot manipulate infinite sets. Moreover, no experimental results comparing the performances between the Omega library and the implementation for lists of polyhedra are available.