-dimensional vector space) that satisfies a finite number of linear inequalities having rational coefficients. The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components, with applications spanning imperative, functional and logic programming languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Even though the PPL library is not meant to target a particular problem, the design of its interface has been largely influenced by the needs of the above class of applications. That is the reason why the library implements a few operators that are more or less specific to static analysis applications, while lacking some other operators that might be useful when working, e.g., in the field of computational geometry.The main features of the library are the following:
x + 2*y + 5*z <= 7 when you mean it;In the following sections we describe the polyhedra and the different representations and operations supported by the PPL in more detail. For more information about the definitions and results stated here see [BRZH02b], [Fuk98], [NW88], and [Wil93].
Vectors, Matrices and Scalar Products
We denote by
the
-dimensional vector space on the field of real numbers
, endowed with the standard topology. The set of all non-negative reals is denoted by
. For each
,
denotes the
-th component of the (column) vector
. We denote by
the vector of
, called the origin, having all components equal to zero. A vector
can be also interpreted as a matrix in
and manipulated accordingly using the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, denoted by
.
The scalar product of
, denoted
, is the real number
For any
, the Minkowski's sum of
and
is: 
Affine Hyperplanes and Half-spaces
For each vector
and scalar
, where
, and for each relation symbol
, the linear constraint
defines:
;
;
.
Note that each hyperplane
can be defined as the intersection of the two closed affine half-spaces
and
. Also note that, when
, the constraint
is either a tautology (i.e., always true) or inconsistent (i.e., always false), so that it defines either the whole vector space
or the empty set
.
Convex Polyhedra
The set
is a not necessarily closed convex polyhedron (NNC polyhedron, for short) if and only if either
can be expressed as the intersection of a finite number of (open or closed) affine half-spaces of
or
and
. The set of all NNC polyhedra on the vector space
is denoted
.
The set
is a closed convex polyhedron (closed polyhedron, for short) if and only if either
can be expressed as the intersection of a finite number of closed affine half-spaces of
or
and
. The set of all closed polyhedra on the vector space
is denoted
.
When ordering NNC polyhedra by the set inclusion relation, the empty set
and the vector space
are, respectively, the smallest and the biggest elements of both
and
. The vector space
is also called the universe polyhedron.
In theoretical terms,
is a lattice under set inclusion and
is a sub-lattice of
.
Bounded Polyhedra
An NNC polyhedron
is bounded if there exists a
such that
A bounded polyhedron is also called a polytope.
Constraints representation
In the sequel, we will simply write ``equality'' and ``inequality'' to mean ``linear equality'' and ``linear inequality'', respectively; also, we will refer to either an equality or an inequality as a constraint.
By definition, each polyhedron
is the set of solutions to a constraint system, i.e., a finite number of constraints. By using matrix notation, we have
where, for all
,
and
, and
are the number of equalities, the number of non-strict inequalities, and the number of strict inequalities, respectively.
Combinations and Hulls
Let
be a finite set of vectors. For all scalars
, the vector
is said to be a linear combination of the vectors in
. Such a combination is said to be
;
;
We denote by
(resp.,
,
,
) the set of all the linear (resp., positive, affine, convex) combinations of the vectors in
.
Let
, where
. We denote by
the set of all convex combinations of the vectors in
such that
for some
(informally, we say that there exists a vector of
that plays an active role in the convex combination). Note that
so that, if
,
It can be observed that
is an affine space,
is a topologically closed convex cone,
is a topologically closed polytope, and
is an NNC polytope.
Points, Closure Points, Rays and Lines
Let
be an NNC polyhedron. Then
is called a point of
;
is called a closure point of
if it is a point of the topological closure of
;
, where
, is called a ray (or direction of infinity) of
if
and
, for all points
and all
;
is called a line of
if both
and
are rays of
.
A point of an NNC polyhedron
is a vertex if and only if it cannot be expressed as a convex combination of any other pair of distinct points in
. A ray
of a polyhedron
is an extreme ray if and only if it cannot be expressed as a positive combination of any other pair
and
of rays of
, where
,
and
for all
(i.e., rays differing by a positive scalar factor are considered to be the same ray).
Generators Representation
Each NNC polyhedron
can be represented by finite sets of lines
, rays
, points
and closure points
of
. The 4-tuple
is said to be a generator system for
, in the sense that
where the symbol '
' denotes the Minkowski's sum.
When
is a closed polyhedron, then it can be represented by finite sets of lines
, rays
and points
of
. In this case, the 3-tuple
is said to be a generator system for
since we have
Thus, in this case, every closure point of
is a point of
.
For any
and generator system
for
, we have
if and only if
. Also
must contain all the vertices of
although
can be non-empty and have no vertices. In this case, as
is necessarily non-empty, it must contain points of
that are not vertices. For instance, the half-space of
corresponding to the single constraint
can be represented by the generator system
such that
,
,
, and
. It is also worth noting that the only ray in
is not an extreme ray of
.
Minimized Representations
A constraints system
for an NNC polyhedron
is said to be minimized if no proper subset of
is a constraint system for
.
Similarly, a generator system
for an NNC polyhedron
is said to be minimized if there does not exist a generator system
for
such that
,
,
and
.
Double Description
Any NNC polyhedron
can be described by using a constraint system
, a generator system
, or both by means of the double description pair (DD pair)
. The double description method is a collection of well-known as well as novel theoretical results showing that, given one kind of representation, there are algorithms for computing a representation of the other kind and for minimizing both representations by removing redundant constraints/generators.
Such changes of representation form a key step in the implementation of many operators on NNC polyhedra: this is because some operators, such as intersections and poly-hulls, are provided with a natural and efficient implementation when using one of the representations in a DD pair, while being rather cumbersome when using the other.
Topologies and Topological-compatibility
As indicated above, when an NNC polyhedron
is necessarily closed, we can ignore the closure points contained in its generator system
(as every closure point is also a point) and represent
by the triple
. Similarly,
can be represented by a constraint system that has no strict inequalities. Thus a necessarily closed polyhedron can have a smaller representation than one that is not necessarily closed. Moreover, operators restricted to work on closed polyhedra only can be implemented more efficiently. For this reason the library provides two alternative ``topological kinds'' for a polyhedron, NNC and C. We shall abuse terminology by referring to the topologcal kind of a polyhedron as its topology.
In the library, the topology of each polyhedron object is fixed once for all at the time of its creation and must be respected when performing operations on the polyhedron.
Unless it is otherwise stated, all the polyhedra, constraints and/or generators in any library operation must obey the following topological-compatibility rules:
Wherever possible, the library provides methods that, starting from a polyhedron of a given topology, build the corresponding polyhedron having the other topology.
Space Dimensions and Dimension-compatibility
The space dimension of an NNC polyhedron
(resp., a C polyhedron
) is the dimension
of the corresponding vector space
. The space dimension of constraints, generators and other objects of the library is defined similarly.
Unless it is otherwise stated, all the polyhedra, constraints and/or generators in any library operation must obey the following space dimension-compatibility rules:
where
and
, is dimension-compatible with a polyhedron having space dimension
if and only if
;
is dimension-compatible with a polyhedron having space dimension
if and only if
;While the space dimension of a constraint, a generator or a system thereof is automatically adjusted when needed, the space dimension of a polyhedron can only be changed by explicit calls to operators provided for that purpose.
Rational Polyhedra
An NNC polyhedron is called rational if it can be represented by a constraint system where all the constraints have rational coefficients. It has been shown that an NNC polyhedron is rational if and only if it can be represented by a generator system where all the generators have rational coefficients.
The library only supports rational polyhedra. The restriction to rational numbers applies not only to polyhedra, but also to the other numeric arguments that may be required by the operators considered, such as the coefficients defining (rational) affine transformations and (rational) bounding boxes.
Intersection and Convex Polyhedral Hull
For any pair of NNC polyhedra
, the intersection of
and
, defined as the set intersection
, is the biggest NNC polyhedron included in both
and
; similarly, the convex polyhedral hull (or poly-hull) of
and
, denoted by
, is the smallest NNC polyhedron that includes both
and
. The intersection and poly-hull of any pair of closed polyhedra in
is also closed.
In theoretical terms, the intersection and poly-hull operators defined above are the binary meet and the binary join operators on the lattices
and
.
For any pair of NNC polyhedra
, the convex polyhedral difference (or poly-difference) of
and
is defined as the smallest convex polyhedron containing the set-theoretic difference of
and
.
In general, even though
are topologically closed polyhedra, their poly-difference may be a convex polyhedron that is not topologically closed. For this reason, when computing the poly-difference of two C polyhedra, the library will enforce the topological closure of the result.
Viewing a polyhedron as a set of tuples (its points), it is sometimes useful to consider the set of tuples obtained by concatenating an ordered pair of polyhedra. Formally, the concatenation of the polyhedra
and
(taken in this order) is the polyhedron
such that
Another way of seeing it is as follows: first embed polyhedron
into a vector space of dimension
and then add a suitably renamed-apart version of the constraints defining
.
Adding New Dimensions to the Vector Space
The library provides two operators for adding a number
of space dimensions to an NNC polyhedron
, therefore transforming it into a new NNC polyhedron
. In both cases, the added dimensions of the vector space are those having the highest indices.
The operator add_dimensions_and_embed embeds the polyhedron
into the new vector space of dimension
and returns the polyhedron
defined by all and only the constraints defining
(the variables corresponding to the added dimensions are unconstrained). For instance, when starting from a polyhedron
and adding a third dimension, the result will be the polyhedron
In contrast, the operator add_dimensions_and_project projects the polyhedron
into the new vector space of dimension
and returns the polyhedron
whose constraint system, besides the constraints defining
, will include additional constraints on the added dimensions. Namely, the corresponding variables are all constrained to be equal to 0. For instance, when starting from a polyhedron
and adding a third dimension, the result will be the polyhedron
Removing Dimensions from the Vector Space
The library provides two operators for removing space dimensions from an NNC polyhedron
, therefore transforming it into a new NNC polyhedron
where
.
Given a set of variables, the operator remove_dimensions removes all the space dimensions specified by the variables in the set. For instance, letting
be the singleton set
, then after invoking this operator with the set of variables
the resulting polyhedron is
Given a space dimension
less than or equal to that of the polyhedron, the operator remove_higher_dimensions removes the dimensions having indices greater than or equal to
. For instance, letting
defined as before, by invoking this operator with
the resulting polyhedron will be
Mapping the Dimensions of the Vector Space
The operator map_dimensions provided by the library maps the dimensions of the vector space
according to a partial injective function
such that
with
. Dimensions corresponding to indices that are not mapped by
are removed.
If
, i.e., if the function
is undefined everywhere, then the operator projects the argument polyhedron
onto the zero-dimension space
; otherwise the result is
given by
Expanding One Dimension of the Vector Space to Multiple Dimensions
The operator expand_dimension provided by the library adds
new dimensions to a polyhedron
, with
, so that dimensions
,
,
,
of the result
are exact copies of the
-th dimension of
. More formally,
This operation has been proposed in [GDMDRS04].
Folding Multiple Dimensions of the Vector Space into One Dimension
The operator fold_dimensions provided by the library, given a polyhedron
, with
, folds a set of dimensions
, with
and
for each
, into dimension
, where
. The result is given by
where
and, for
,
,
,
and, finally, for
,
,
,
(
denotes the cardinality of the finite set
).
This operation has been proposed in [GDMDRS04].
For each function mapping
, we denote by
the image under
of the set
; formally,
Similarly, we denote by
the preimage under
of
, that is the largest set
such that
; formally,
The function mapping
is an affine transformation if there exist a matrix
and a vector
such that, for all
, we have
. If
, then the function
is said to be space-dimension preserving.
Both
and
are closed under the application of any space-dimension preserving affine image and preimage operators.
The library provides two operators, one computes an affine image and the other an affine preimage of a polyhedron
for a given variable
and linear expression
. This variable and expression determine the affine transformation
that is to be used by the operator. That is,
is the transformation defined by the matrix and vector
where the
(resp.,
) occurs in the
st row in
(resp., position in
). Thus
transforms any point
in the polyhedron
to
The affine image operator computes the affine image of
under
. For instance, suppose the polyhedron
to be transformed is the square in
generated by the set of points
. Then, for example if the considered variable is
and the linear expression
(so that
,
), the affine image operator will translate
to the parallelogram
generated by the set of points
with height equal to the side of the square and oblique sides parallel to the line
. If the considered variable is as before (i.e.,
) but the linear expression is
(so that
), then the resulting polyhedron
is the positive diagonal of the square.
The affine preimage operator computes the affine preimage of
under
. For instance, suppose now that we apply the affine preimage operator as given in the first example using variable
and linear expression
to the parallelogram
; then we get the original square
back. If, on the other hand, we apply the affine preimage operator as given in the second example using variable
and linear expression
to
, then the resulting polyhedron is a line that corresponds to the
axes.
Observe that provided the coefficient
of the considered variable in the linear expression is non-zero, the affine transformation is invertible.
The library provides another operator which is a generalization of the affine image operator. Given a polyhedron
, an affine expression
, a relation symbol
, and an affine expression
, the image of
with respect to the transfer function
is defined as
Note that, when
and
, then the above operator is equivalent to the application of the standard affine image of
with respect to the variable
and the affine expression
(hence the name given to this operator).
The time-elapse operator has been defined in [HPR97]. Actually, the time-elapse operator provided by the library is a slight generalization of that one, since it also works on NNC polyhedra. For any two NNC polyhedra
, the time-elapse between
and
, denoted
, is the smallest NNC polyhedron containing the set
Note that, if
are closed polyhedra, the above set is also a closed polyhedron. In contrast, when
is not topologically closed, the above set might not be an NNC polyhedron.
The library provides operators for checking the relation holding between an NNC polyhedron and either a constraint or a generator.
Suppose
is an NNC polyhedron and
an arbitrary constraint system representing
. Suppose also that
is a constraint with
and
the set of points that satisfy
. The possible relations between
and
are as follows.
is disjoint from
if
; that is, adding
to
gives us the empty polyhedron.
strictly intersects
if
and
; that is, adding
to
gives us a non-empty polyhedron strictly smaller than
.
is included in
if
; that is, adding
to
leaves
unchanged.
saturates
if
, where
is the hyperplane induced by constraint
, i.e., the set of points satisfying the equality constraint
; that is, adding the constraint
to
leaves
unchanged.
The polyhedron
subsumes the generator
if adding
to any generator system representing
does not change
.
Intervals, boxes and bounding boxes
An interval in
is a pair of bounds, called lower and upper. Each bound can be either (1) closed and bounded, (2) open and bounded, or (3) open and unbounded. If the bound is bounded, then it has a value in
. An
-dimensional box
in
is a sequence of
intervals in
.
The polyhedron
represents a box
in
if
is described by a constraint system in
that consists of one constraint for each bounded bound (lower and upper) in an interval in
: Letting
be the vector in
with 1 in the
'th position and zeroes in every other position; if the lower bound of the
'th interval in
is bounded, the corresponding constraint is defined as
, where
is the value of the bound and
is
if it is a closed bound and
if it is an open bound. Similarly, if the upper bound of the
'th interval in
is bounded, the corresponding constraint is defined as
, where
is the value of the bound and
is
if it is a closed bound and
if it is an open bound.
If every bound in the intervals defining a box
is either closed and bounded or open and unbounded, then
represents a closed polyhedron.
The bounding box of an NNC polyhedron
is the smallest
-dimensional box containing
.
The library provides operations for computing the bounding box of an NNC polyhedron and conversely, for obtaining the NNC polyhedron representing a given bounding box.
The library provides two widening operators for the domain of NNC polyhedra. The first one, that we call H79-widening, mainly follows the specification provided in the PhD thesis of N. Halbwachs [Hal79], also described in [HPR97]. There are a few differences between the H79-widening and the widening described in the cited paper. In particular, the H79-widening of an NNC polyhedron
using the NNC polyhedron
:
and
(the original definition is restricted to inequalities);
.
The second widening operator, that we call BHRZ03-widening, is an instance of the specification provided in [BHRZ03a]. This operator also requires as a precondition that
and it is guaranteed to provide a result which is at least as precise as the H79-widening.
Both widening operators can be applied to polyhedra that are not topologically closed. The user is warned that, in such a case, the results may not closely match the geometric intuition which is at the base of the specification of the two widenings. The reason is that, in the current implementation, the widenings are not directly applied to the NNC polyhedra, but rather to their internal representations. Implementation work is in progress and future versions of the library may provide an even better integration of the two widenings with the domain of NNC polyhedra.
When approximating a fixpoint computation using widening operators, a common tactic to improve the precision of the final result is to delay the application of widening operators. The usual approach is to fix a parameter
and only apply widenings starting from the
-th iteration.
The library also supports an improved widening delay strategy, that we call widening with tokens [BHRZ03a]. A token is a sort of wildcard allowing for the replacement of the widening application by the exact upper bound computation: the token is used (and thus consumed) only when the widening would have resulted in an actual precision loss (as opposed to the potential precision loss of the classical delay strategy). Thus, all widening operators can be supplied with an optional argument, recording the number of available tokens, which is decremented when tokens are used. The approximated fixpoint computation will start with a fixed number
of tokens, which will be used if and when needed. When there are no tokens left, the widening is always applied.
Besides the two widening operators, the library also implements several extrapolation operators, which differ from widenings in that their use along an upper iteration sequence does not ensure convergence in a finite number of steps.
In particular, for each of the two widenings there is a corresponding limited extrapolation operator, which can be used to implement the widening ``up to'' technique as described in [HPR97]. Each limited extrapolation operator takes a constraint system as an additional parameter and uses it to improve the approximation yielded by the corresponding widening operator. Note that a convergence guarantee can only be obtained by suitably restricting the set of constraints that can occur in this additional parameter. For instance, in [HPR97] this set is fixed once and for all before starting the computation of the upward iteration sequence.
The bounded extrapolation operators further enhance each one of the limited extrapolation operators described above, by ensuring that their results cannot be worse than the smallest bounding box enclosing the two argument polyhedra.
A Note on the Implementation of the Operators
When adopting the double description method, the implementation of the above operators on polyhedra may require an explicit conversion from one of the two representations into the other one, leading to algorithms having a worst-case exponential complexity. However, thanks to the adoption of lazy and incremental computation techniques, the library turns out to be rather efficient in many practical cases.
In earlier versions of the library, a number of operators were introduced in two flavors: a lazy version and an eager version, the latter having the operator name ending with _and_minimize. In principle, only the lazy versions should be used. The eager versions were added to help a knowledgeble user obtain better performance in particular cases. Basically, by invoking the eager version of an operator, the user is trading laziness to better exploit the incrementality of the inner library computations. Starting from version 0.5, the lazy and incremental computation techniques have been refined to achieve a better integration: as a consequence, the lazy versions of the operators are now almost always more efficient than the eager versions.
The only case when an eager computation still makes sense is when the well-known fail-first principle comes into play. For instance, if you have to compute the intersection of several polyhedra and you strongly suspect that the result will become empty after a few of these intersections, then you may obtain a better performance by calling the eager version of the intersection operator, since the minimization process also enforces an emptyness check. Note anyway that the same effect can be obtained by interleaving the calls of the lazy operator with explicit emptyness checks.
On Const-Correctness: A Warning about the Use of References and Iterators
Most operators of the library depend on one or more parameters that are declared ``const'', meaning that they will not be changed by the application of the considered operator. Due to the adoption of lazy computation techniques, in many cases such a const-correctness guarantee only holds at the semantic level, whereas it does not necessarily hold at the implementation level. For a typical example, consider the extraction from a polyhedron of its constraint system representation. While this operation is not going to change the polyhedron, it might actually invoke the internal conversion algorithm and modify the generators representation of the polyhedron object, e.g., by reordering the generators and removing those that are detected as redundant. Thus, any previously computed reference to the generators of the polyhedron (be it a direct reference object or an indirect one, such as an iterator) will no longer be valid. For this reason, code fragments such as the following should be avoided, as they may result in undefined behavior:
// Find a reference to the first point of the non-empty polyhedron `ph'. const GenSys& gs = ph.generators(); GenSys::const_iterator i = gs.begin(); for (GenSys::const_iterator gs_end = gs.end(); i != gs_end; ++i) if (i->is_point()) break; const Generator& p = *i; // Get the constraints of `ph'. const ConSys& cs = ph.constraints(); // Both the const iterator `i' and the reference `p' // are no longer valid at this point. cout << p.divisor() << endl; // Undefinded behavior! ++i; // Undefinded behavior!
i and the reference p. Anyway, if really needed, it is always possible to take a copy of, instead of a reference to, the parts of interest of the polyhedron; in the case above, one may have taken a copy of the generator system by replacing the second line of code with the following: GenSys gs = ph.generators();
polymake: a framework for analyzing convex polytopes. In G. Kalai and G. M. Ziegler, editors, Polytopes - Combinatorics and Computation, pages 43-74. Birkhäuser, 2000.
polymake: an approach to modular software design in computational geometry. In Proceedings of the 17th Annual Symposium on Computational Geometry, pages 222-231, Medford, MA, USA, 2001. ACM.
1.3.8-20040812