# More Details on the PPL

The Parma Polyhedra Library provides a number of abstract domains and abstract domain constructors. Currently these are:

- the domain of topologically closed, rational convex polyhedra (C polyhedra);
- the domain of rational convex polyhedra that are not necessarily closed (NNC polyhedra);
- the domain of octagonal shapes;
- the domain of bounded-difference shapes;
- the domain of boxes;
- the domain of grids;
- the powerset domain construction;
- the pointset powerset domain construction, that can be instantiated for any pointset;
- the partially reduced product domain construction, which is parametric on the domains of its components and also on the reduction operator.

## Implementation of C and NNC Polyhedra in the PPL

The implementation of the domain of
C polyhedra uses the *double description* representation.
This representation was introduced by T. S. Motzkin et al.
MRTT53 :
the description based on the intersection of hyperspaces
is complemented by its description as a set of all points
constructed from several finite sets of vectors
(representing, for instance, points and rays) following
certain rules for their combination.
In other words, in the first representation, a polyhedron is
captured by a finite set (or system) of *constraints*
while, in the second representation,
it is characterized by a finite set (or system)
of *generators*.

Some operations on convex polyhedra are more conveniently performed using the first representation. Intersection of two polyhedra, for instance, can be characterized by the union of the respective constraint systems. The convex polyhedral hull of two polyhedra, instead, can be easily seen as the union of the respective systems of generators.

The library converts, *automatically*
and *lazily*, from one representation to the other.
Automatically means that the user does not need to worry about
when the conversion should take place.
Lazily means that the library tries hard to minimize the number of
conversions it will perform and exploit, as far as possible, the
conversions that are performed.

To perform the conversion, the library uses an algorithm that was originally proposed by T. S. Motzkin et al. MRTT53 , then rediscovered by N. V. Chernikova Che65 , improved by H. Le Verge Ver92 , further improved by D. K. Wilde Wil93 , K. Fukuda and A. Prodon FP96 , N. Halbwachs, Y.-E. Proy and P. Roumanoff HPR97 , and B. Jeannet (author of the New Polka library).

The double description method assumes the constraints are either
equalities or non-strict inequalities and only applies to closed polyhedra.
To allow for strict inequalities and hence
polyhedra that are *not necessarily closed* (NNC),
the library adopts the approach described by
N. Halbwachs, Y.-E. Proy, and P. Raymond in
HPR94 .
Here, the addition of an extra dimension to the vector space of the polyhedron
is used to encode the closedness of each of its defining hyperspaces.

The generator system that the library uses to describe an NNC polyhedron
has, in addition to the finite sets of vectors representing
points and rays, a set of vectors representing a subset of its
*closure points*.
These are points in the topological closure of the polyhedron
but not necessarily in the polyhedron itself.
See
BRZH02a
for more details about this representation.

The library includes widening algorithms for the domains of C and NNC polyhedra that are based on the widening introduced by N. Halbwachs in Hal79 . This widening is also described in HPR97 .