// Copyright (C) 2001-2004 Roberto Bagnara // // This document describes the Parma Polyhedra Library (PPL). // // Permission is granted to copy, distribute and/or modify this document // under the terms of the GNU Free Documentation License, Version 1.1 or // any later version published by the Free Software Foundation; with no // Invariant Sections, with no Front-Cover Texts, and with no Back-Cover // Texts. // // The PPL is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by the // Free Software Foundation; either version 2 // of the License, or (at your option) any later version. // // The PPL is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or // FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License // for more details. // // For the most up-to-date information see the Parma Polyhedra Library // site: http://www.cs.unipr.it/ppl/ /*! \defgroup PPL_Library The Library The core implementation of the Parma Polyhedra Library is written in C++. See Namespace, Hierarchical and Compound indexes for additional information about each single data type. */ /*! \mainpage General Information on the PPL \section preamble The Main Features The Parma Polyhedra Library (PPL) is a modern C++ library for the manipulation of numerical information that can be represented by points in some \f$n\f$-dimensional vector space. For instance, one of the key domains the PPL supports is that of rational convex polyhedra (Section \ref convex_polys). Such domains are 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: - it is user friendly: you write x + 2*y + 5*z \<= 7 when you mean it; - it is fully dynamic: available virtual memory is the only limitation to the dimension of anything; - it provides full support for the manipulation of convex polyhedra that are not topologically closed; - it is written in standard C++: meant to be portable; - it is exception-safe: never leaks resources or leaves invalid object fragments around; - it is rather efficient: and we hope to make it even more so; - it is thoroughly documented: perhaps not literate programming but close enough; - it has interfaces to other programming languages: including C and a number of Prolog systems; - it is free software: distributed under the terms of the GNU General Public License. In addition to the basic domains, we also provide generic support for constructing new domains from pre-existing domains. The following domains and domain constructors are provided by the PPL: - the domain of topologically closed, rational convex polyhedra; - the domain of rational convex polyhedra that are not necessarily closed; - the powerset construction; - the powerset construction, instantiated for rational convex polyhedra. In the following sections we describe these domains and domain constructors together with their representations and operations that are available to the PPL user. In the final section of this chapter (Section \ref use_of_library), we provide some additional advice on the use of the library. \section convex_polys Convex Polyhedra In this section we introduce convex polyhedra, as considered by the library, in more detail. For more information about the definitions and results stated here see \ref BRZH02b "[BRZH02b]", \ref Fuk98 "[Fuk98]", \ref NW88 "[NW88]", and \ref Wil93 "[Wil93]". Vectors, Matrices and Scalar Products We denote by \f$\Rset^n\f$ the \f$n\f$-dimensional vector space on the field of real numbers \f$\Rset\f$, endowed with the standard topology. The set of all non-negative reals is denoted by \f$\nonnegRset\f$. For each \f$i \in \{0, \ldots, n-1\}\f$, \f$v_i\f$ denotes the \f$i\f$-th component of the (column) vector \f$\vect{v} = (v_0, \ldots, v_{n-1})^\transpose \in \Rset^n\f$. We denote by \f$\vect{0}\f$ the vector of \f$\Rset^n\f$, called the origin, having all components equal to zero. A vector \f$\vect{v} \in \Rset^n\f$ can be also interpreted as a matrix in \f$\Rset^{n \times 1}\f$ and manipulated accordingly using the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, denoted by \f$\vect{v}^\transpose\f$. The scalar product of \f$\vect{v},\vect{w} \in \Rset^n\f$, denoted \f$\langle \vect{v}, \vect{w} \rangle\f$, is the real number \f[ \vect{v}^\transpose \vect{w} = \sum_{i=0}^{n-1} v_i w_i. \f] For any \f$S_1, S_2 \sseq \Rset^n\f$, the Minkowski's sum of \f$S_1\f$ and \f$S_2\f$ is: \f$S_1 + S_2 = \{\, \vect{v}_1 + \vect{v}_2 \mid \vect{v}_1 \in S_1, \vect{v}_2 \in S_2 \,\}.\f$ Affine Hyperplanes and Half-spaces For each vector \f$\vect{a} \in \Rset^n\f$ and scalar \f$b \in \Rset\f$, where \f$\vect{a} \neq \vect{0}\f$, and for each relation symbol \f$\mathord{\relsym} \in \{ =, \geq, > \}\f$, the linear constraint \f$\langle \vect{a}, \vect{x} \rangle \relsym b\f$ defines: - an affine hyperplane if it is an equality constraint, i.e., if \f$\mathord{\relsym} \in \{ = \}\f$; - a topologically closed affine half-space if it is a non-strict inequality constraint, i.e., if \f$\mathord{\relsym} \in \{ \geq \}\f$; - a topologically open affine half-space if it is a strict inequality constraint, i.e., if \f$\mathord{\relsym} \in \{ > \}\f$. Note that each hyperplane \f$\langle \vect{a}, \vect{x} \rangle = b\f$ can be defined as the intersection of the two closed affine half-spaces \f$\langle \vect{a}, \vect{x} \rangle \geq b\f$ and \f$\langle -\vect{a}, \vect{x} \rangle \geq -b\f$. Also note that, when \f$\vect{a} = \vect{0}\f$, the constraint \f$\langle \vect{0}, \vect{x} \rangle \relsym b\f$ is either a tautology (i.e., always true) or inconsistent (i.e., always false), so that it defines either the whole vector space \f$\Rset^n\f$ or the empty set \f$\emptyset\f$. Convex Polyhedra The set \f$\cP \sseq \Rset^n\f$ is a not necessarily closed convex polyhedron (NNC polyhedron, for short) if and only if either \f$\cP\f$ can be expressed as the intersection of a finite number of (open or closed) affine half-spaces of \f$\Rset^n\f$ or \f$n = 0\f$ and \f$\cP = \emptyset\f$. The set of all NNC polyhedra on the vector space \f$\Rset^n\f$ is denoted \f$\Pset_n\f$. The set \f$\cP \in \Pset_n\f$ is a closed convex polyhedron (closed polyhedron, for short) if and only if either \f$\cP\f$ can be expressed as the intersection of a finite number of closed affine half-spaces of \f$\Rset^n\f$ or \f$n = 0\f$ and \f$\cP = \emptyset\f$. The set of all closed polyhedra on the vector space \f$\Rset^n\f$ is denoted \f$\CPset_n\f$. When ordering NNC polyhedra by the set inclusion relation, the empty set \f$\emptyset\f$ and the vector space \f$\Rset^n\f$ are, respectively, the smallest and the biggest elements of both \f$\Pset_n\f$ and \f$\CPset_n\f$. The vector space \f$\Rset^n\f$ is also called the universe polyhedron. In theoretical terms, \f$\Pset_n\f$ is a lattice under set inclusion and \f$\CPset_n\f$ is a sub-lattice of \f$\Pset_n\f$. Bounded Polyhedra An NNC polyhedron \f$\cP \in \Pset_n\f$ is bounded if there exists a \f$\lambda \in \nonnegRset\f$ such that \f[ \cP \sseq \bigl\{\, \vect{x} \in \Rset^n \bigm| - \lambda \leq x_j \leq \lambda \text{ for } j = 0, \ldots, n-1 \,\bigr\}. \f] A bounded polyhedron is also called a polytope. \section representation Representations of Convex Polyhedra NNC polyhedra can be specified by using two possible representations, the constraints (or implicit) representation and the generators (or parametric) representation. 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 \f$\cP \in \Pset_n\f$ is the set of solutions to a constraint system, i.e., a finite number of constraints. By using matrix notation, we have \f[ \cP \defeq \{\, \vect{x} \in \Rset^n \mid A_1 \vect{x} = \vect{b}_1, A_2 \vect{x} \geq \vect{b}_2, A_3 \vect{x} > \vect{b}_3 \,\}, \f] where, for all \f$i \in \{1, 2, 3\}\f$, \f$A_i \in \Rset^{m_i} \times \Rset^n\f$ and \f$\vect{b}_i \in \Rset^{m_i}\f$, and \f$m_1, m_2, m_3 \in \Nset\f$ are the number of equalities, the number of non-strict inequalities, and the number of strict inequalities, respectively. Combinations and Hulls Let \f$S = \{ \vect{x}_1, \ldots, \vect{x}_k \} \sseq \Rset^n\f$ be a finite set of vectors. For all scalars \f$\lambda_1, \ldots, \lambda_k \in \Rset\f$, the vector \f$\vect{v} = \sum_{j=1}^k \lambda_j \vect{x}_j\f$ is said to be a linear combination of the vectors in \f$S\f$. Such a combination is said to be - a positive (or conic) combination, if \f$\forall j \in \{ 1, \ldots, k \} \itc \lambda_j \in \nonnegRset\f$; - an affine combination, if \f$\sum_{j = 1}^k \lambda_j = 1\f$; - a convex combination, if it is both positive and affine. We denote by \f$\linearhull(S)\f$ (resp., \f$\conichull(S)\f$, \f$\affinehull(S)\f$, \f$\convexhull(S)\f$) the set of all the linear (resp., positive, affine, convex) combinations of the vectors in \f$S\f$. Let \f$P, C \sseq \Rset^n\f$, where \f$P \union C = S\f$. We denote by \f$\NNChull(P, C)\f$ the set of all convex combinations of the vectors in \f$S\f$ such that \f$\lambda_j > 0\f$ for some \f$\vect{x}_j \in P\f$ (informally, we say that there exists a vector of \f$P\f$ that plays an active role in the convex combination). Note that \f$\NNChull(P, C) = \NNChull(P, P \union C)\f$ so that, if \f$C \sseq P\f$, \f[ \convexhull(P) = \NNChull(P, \emptyset) = \NNChull(P, P) = \NNChull(P, C). \f] It can be observed that \f$\linearhull(S)\f$ is an affine space, \f$\conichull(S)\f$ is a topologically closed convex cone, \f$\convexhull(S)\f$ is a topologically closed polytope, and \f$\NNChull(P, C)\f$ is an NNC polytope. Points, Closure Points, Rays and Lines Let \f$\cP \in \Pset_n\f$ be an NNC polyhedron. Then - a vector \f$\vect{p} \in \cP\f$ is called a point of \f$\cP\f$; - a vector \f$\vect{c} \in \Rset^n\f$ is called a closure point of \f$\cP\f$ if it is a point of the topological closure of \f$\cP\f$; - a vector \f$\vect{r} \in \Rset^n\f$, where \f$\vect{r} \neq \vect{0}\f$, is called a ray (or direction of infinity) of \f$\cP\f$ if \f$\cP \neq \emptyset\f$ and \f$\vect{p} + \lambda \vect{r} \in \cP\f$, for all points \f$\vect{p} \in \cP\f$ and all \f$\lambda \in \nonnegRset\f$; - a vector \f$\vect{l} \in \Rset^n\f$ is called a line of \f$\cP\f$ if both \f$\vect{l}\f$ and \f$-\vect{l}\f$ are rays of \f$\cP\f$. A point of an NNC polyhedron \f$\cP \in \Pset_n\f$ is a vertex if and only if it cannot be expressed as a convex combination of any other pair of distinct points in \f$\cP\f$. A ray \f$\vect{r}\f$ of a polyhedron \f$\cP\f$ is an extreme ray if and only if it cannot be expressed as a positive combination of any other pair \f$\vect{r}_1\f$ and \f$\vect{r}_2\f$ of rays of \f$\cP\f$, where \f$\vect{r} \neq \lambda \vect{r}_1\f$, \f$\vect{r} \neq \lambda \vect{r}_2\f$ and \f$\vect{r}_1 \neq \lambda \vect{r}_2\f$ for all \f$\lambda \in \nonnegRset\f$ (i.e., rays differing by a positive scalar factor are considered to be the same ray). Generators Representation Each NNC polyhedron \f$\cP \in \Pset_n\f$ can be represented by finite sets of lines \f$L\f$, rays \f$R\f$, points \f$P\f$ and closure points \f$C\f$ of \f$\cP\f$. The 4-tuple \f$\cG = (L, R, P, C)\f$ is said to be a generator system for \f$\cP\f$, in the sense that \f[ \cP = \linearhull(L) + \conichull(R) + \NNChull(P, C), \f] where the symbol '\f$+\f$' denotes the Minkowski's sum. When \f$\cP \in \CPset_n\f$ is a closed polyhedron, then it can be represented by finite sets of lines \f$L\f$, rays \f$R\f$ and points \f$P\f$ of \f$\cP\f$. In this case, the 3-tuple \f$\cG = (L, R, P)\f$ is said to be a generator system for \f$\cP\f$ since we have \f[ \cP = \linearhull(L) + \conichull(R) + \convexhull(P). \f] Thus, in this case, every closure point of \f$\cP\f$ is a point of \f$\cP\f$. For any \f$\cP \in \Pset_n\f$ and generator system \f$\cG = (L, R, P, C)\f$ for \f$\cP\f$, we have \f$\cP = \emptyset\f$ if and only if \f$P = \emptyset\f$. Also \f$P\f$ must contain all the vertices of \f$\cP\f$ although \f$\cP\f$ can be non-empty and have no vertices. In this case, as \f$P\f$ is necessarily non-empty, it must contain points of \f$\cP\f$ that are not vertices. For instance, the half-space of \f$\Rset^2\f$ corresponding to the single constraint \f$y \geq 0\f$ can be represented by the generator system \f$\cG = (L, R, P, C)\f$ such that \f$L = \bigl\{ (1, 0)^\transpose \bigr\}\f$, \f$R = \bigl\{ (0, 1)^\transpose \bigr\}\f$, \f$P = \bigl\{ (0, 0)^\transpose \bigr\}\f$, and \f$C = \emptyset\f$. It is also worth noting that the only ray in \f$R\f$ is not an extreme ray of \f$\cP\f$. Minimized Representations A constraints system \f$\cC\f$ for an NNC polyhedron \f$\cP \in \Pset_n\f$ is said to be minimized if no proper subset of \f$\cC\f$ is a constraint system for \f$\cP\f$. Similarly, a generator system \f$\cG = (L, R, P, C)\f$ for an NNC polyhedron \f$\cP \in \Pset_n\f$ is said to be minimized if there does not exist a generator system \f$\cG' = (L', R', P', C') \neq \cG\f$ for \f$\cP\f$ such that \f$L' \sseq L\f$, \f$R' \sseq R\f$, \f$P' \sseq P\f$ and \f$C' \sseq C\f$. Double Description Any NNC polyhedron \f$\cP\f$ can be described by using a constraint system \f$\cC\f$, a generator system \f$\cG\f$, or both by means of the double description pair (DD pair) \f$(\cC, \cG)\f$. 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 \f$\cP\f$ is necessarily closed, we can ignore the closure points contained in its generator system \f$\cG = (L, R, P, C)\f$ (as every closure point is also a point) and represent \f$\cP\f$ by the triple \f$(L, R, P)\f$. Similarly, \f$\cP\f$ 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: - polyhedra are topologically-compatible if and only if they have the same topology; - all constraints except for strict inequality constraints and all generators except for closure points are topologically-compatible with both C and NNC polyhedra; - strict inequality constraints and closure points are topologically-compatible with a polyhedron if and only if it is NNC. 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 \f$\cP \in \Pset_n\f$ (resp., a C polyhedron \f$\cP \in \CPset_n\f$) is the dimension \f$n \in \Nset\f$ of the corresponding vector space \f$\Rset^n\f$. 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: - polyhedra are dimension-compatible if and only if they have the same space dimension; - the constraint \f$\langle \vect{a}, \vect{x} \rangle \relsym b\f$ where \f$\mathord{\relsym} \in \{ =, \geq, > \}\f$ and \f$\vect{a}, \vect{x} \in \Rset^m\f$, is dimension-compatible with a polyhedron having space dimension \f$n\f$ if and only if \f$m \leq n\f$; - the generator \f$\vect{x} \in \Rset^m\f$ is dimension-compatible with a polyhedron having space dimension \f$n\f$ if and only if \f$m \leq n\f$; - a system of constraints (resp., generators) is dimension-compatible with a polyhedron if and only if all the constraints (resp., generators) in the system are dimension-compatible with the polyhedron. 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. \section operations Operations on Convex Polyhedra In this section we briefly describe operations on NNC polyhedra that are provided by the library. Intersection and Convex Polyhedral Hull For any pair of NNC polyhedra \f$\cP_1, \cP_2 \in \Pset_n\f$, the intersection of \f$\cP_1\f$ and \f$\cP_2\f$, defined as the set intersection \f$\cP_1 \inters \cP_2\f$, is the biggest NNC polyhedron included in both \f$\cP_1\f$ and \f$\cP_2\f$; similarly, the convex polyhedral hull (or poly-hull) of \f$\cP_1\f$ and \f$\cP_2\f$, denoted by \f$\cP_1 \uplus \cP_2\f$, is the smallest NNC polyhedron that includes both \f$\cP_1\f$ and \f$\cP_2\f$. The intersection and poly-hull of any pair of closed polyhedra in \f$\CPset_n\f$ 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 \f$\Pset_n\f$ and \f$\CPset_n\f$. \anchor poly_difference Convex Polyhedral Difference For any pair of NNC polyhedra \f$\cP_1, \cP_2 \in \Pset_n\f$, the convex polyhedral difference (or poly-difference) of \f$\cP_1\f$ and \f$\cP_2\f$ is defined as the smallest convex polyhedron containing the set-theoretic difference of \f$\cP_1\f$ and \f$\cP_2\f$. In general, even though \f$\cP_1, \cP_2 \in \CPset_n\f$ 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. \anchor concatenate Concatenating Polyhedra 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 \f$\cP \in \Pset_n\f$ and \f$\cQ \in \Pset_m\f$ (taken in this order) is the polyhedron \f$\cR \in \Pset_{n+m}\f$ such that \f[ \cR \defeq \Bigl\{\, (x_0, \ldots, x_{n-1}, y_0, \ldots, y_{m-1})^\transpose \in \Rset^{n+m} \Bigm| (x_0, \ldots, x_{n-1})^\transpose \in \cP, (y_0, \ldots, y_{m-1})^\transpose \in \cQ \,\Bigl\}. \f] Another way of seeing it is as follows: first embed polyhedron \f$\cP\f$ into a vector space of dimension \f$n+m\f$ and then add a suitably renamed-apart version of the constraints defining \f$\cQ\f$. \anchor add_dimensions Adding New Dimensions to the Vector Space The library provides two operators for adding a number \f$i\f$ of space dimensions to an NNC polyhedron \f$\cP \in \Pset_n\f$, therefore transforming it into a new NNC polyhedron \f$\cQ \in \Pset_{n+i}\f$. In both cases, the added dimensions of the vector space are those having the highest indices. The operator add_dimensions_and_embed \e embeds the polyhedron \f$\cP\f$ into the new vector space of dimension \f$i+n\f$ and returns the polyhedron \f$\cQ\f$ defined by all and only the constraints defining \f$\cP\f$ (the variables corresponding to the added dimensions are unconstrained). For instance, when starting from a polyhedron \f$\cP \sseq \Rset^2\f$ and adding a third dimension, the result will be the polyhedron \f[ \cQ = \bigl\{\, (x_0, x_1, x_2)^\transpose \in \Rset^3 \bigm| (x_0, x_1)^\transpose \in \cP \,\bigr\}. \f] In contrast, the operator add_dimensions_and_project \e projects the polyhedron \f$\cP\f$ into the new vector space of dimension \f$i+n\f$ and returns the polyhedron \f$\cQ\f$ whose constraint system, besides the constraints defining \f$\cP\f$, 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 \f$\cP \sseq \Rset^2\f$ and adding a third dimension, the result will be the polyhedron \f[ \cQ = \bigl\{\, (x_0, x_1, 0)^\transpose \in \Rset^3 \bigm| (x_0, x_1)^\transpose \in \cP \,\bigr\}. \f] \anchor remove_dimensions Removing Dimensions from the Vector Space The library provides two operators for removing space dimensions from an NNC polyhedron \f$\cP \in \Pset_n\f$, therefore transforming it into a new NNC polyhedron \f$\cQ \in \Pset_m\f$ where \f$m \leq n\f$. Given a set of variables, the operator remove_dimensions removes all the space dimensions specified by the variables in the set. For instance, letting \f$\cP \in \Pset_4\f$ be the singleton set \f$\bigl\{ (3, 1, 0, 2)^\transpose \bigr\} \sseq \Rset^4\f$, then after invoking this operator with the set of variables \f$\{x_1, x_2\}\f$ the resulting polyhedron is \f[ \cQ = \bigl\{ (3, 2)^\transpose \bigr\} \sseq \Rset^2. \f] Given a space dimension \f$m\f$ less than or equal to that of the polyhedron, the operator remove_higher_dimensions removes the dimensions having indices greater than or equal to \f$m\f$. For instance, letting \f$\cP \in \Pset_4\f$ defined as before, by invoking this operator with \f$m = 2\f$ the resulting polyhedron will be \f[ \cQ = \bigl\{ (3, 1)^\transpose \bigr\} \sseq \Rset^2. \f] \anchor map_dimensions Mapping the Dimensions of the Vector Space The operator map_dimensions provided by the library maps the dimensions of the vector space \f$\Rset^n\f$ according to a partial injective function \f$\pard{\rho}{\{0, \ldots, n-1\}}{\Nset}\f$ such that \f$\rho\bigl(\{0, \ldots, n-1\}\bigr) = \{0, \ldots, m-1\}\f$ with \f$m \leq n\f$. Dimensions corresponding to indices that are not mapped by \f$\rho\f$ are removed. If \f$m = 0\f$, i.e., if the function \f$\rho\f$ is undefined everywhere, then the operator projects the argument polyhedron \f$\cP \in \Pset_n\f$ onto the zero-dimension space \f$\Rset^0\f$; otherwise the result is \f$\cQ \in \Pset_m\f$ given by \f[ \cQ \defeq \Bigl\{\, \bigl(v_{\rho^{-1}(0)}, \ldots, v_{\rho^{-1}(m-1)}\bigr)^\transpose \Bigm| (v_0, \ldots, v_{n-1})^\transpose \in \cP \,\Bigr\}. \f] \anchor expand_dimension Expanding One Dimension of the Vector Space to Multiple Dimensions The operator expand_dimension provided by the library adds \f$m\f$ new dimensions to a polyhedron \f$\cP \in \Pset_n\f$, with \f$n > 0\f$, so that dimensions \f$n\f$, \f$n+1\f$, \f$\ldots\f$, \f$n+m-1\f$ of the result \f$\cQ\f$ are exact copies of the \f$i\f$-th dimension of \f$\cP\f$. More formally, \f[ \cQ \defeq \sset{ \vect{u} \in \Rset^{n+m} }{ \exists \vect{v}, \vect{w} \in \cP \st u_i = v_i \\ \qquad \mathord{} \land \forall j = n, n+1, \ldots, n+m-1 \itc u_j = w_i \\ \qquad \mathord{} \land \forall k = 0, \ldots, n-1 \itc k \neq i \implies u_k = v_k = w_k }. \f] This operation has been proposed in \ref GDMDRS04 "[GDMDRS04]". \anchor fold_dimensions Folding Multiple Dimensions of the Vector Space into One Dimension The operator fold_dimensions provided by the library, given a polyhedron \f$\cP \in \Pset_n\f$, with \f$n > 0\f$, folds a set of dimensions \f$J = \{ j_0, \ldots, j_{m-1} \}\f$, with \f$m < n\f$ and \f$j < n\f$ for each \f$j \in J\f$, into dimension \f$i < n\f$, where \f$i \notin J\f$. The result is given by \f[ \cQ \defeq \biguplus_{d = 0}^m \cQ_d \f] where \f[ \cQ_m \defeq \sset{ \vect{u} \in \Rset^{n-m} }{ \exists \vect{v} \in \cP \st u_{i'} = v_i \\ \qquad \mathord{} \land \forall k = 0, \ldots, n-1 \itc k \neq i \implies u_{k'} = v_k } \f] and, for \f$ d = 0 \f$, \f$ \ldots \f$, \f$ m-1 \f$, \f[ \cQ_d \defeq \sset{ \vect{u} \in \Rset^{n-m} }{ \exists \vect{v} \in \cP \st u_{i'} = v_{j_d} \\ \qquad \mathord{} \land \forall k = 0, \ldots, n-1 \itc k \neq i \implies u_{k'} = v_k }, \f] and, finally, for \f$ k = 0 \f$, \f$ \ldots \f$, \f$ n-1 \f$, \f[ k' \defeq k - \card \{\, j \in J \mid k > j \,\}, \f] (\f$\card S\f$ denotes the cardinality of the finite set \f$S\f$). This operation has been proposed in \ref GDMDRS04 "[GDMDRS04]". \anchor affine_transformation Affine Images and Preimages For each function mapping \f$\fund{\phi}{\Rset^n}{\Rset^m}\f$, we denote by \f$\phi(S) \sseq \Rset^m\f$ the image under \f$\phi\f$ of the set \f$S \sseq \Rset^n\f$; formally, \f[ \phi(S) \defeq \bigl\{\, \phi(\vect{v}) \in \Rset^m \bigm| \vect{v} \in S \,\bigr\}. \f] Similarly, we denote by \f$\phi^{-1}(S') \sseq \Rset^n\f$ the preimage under \f$\phi\f$ of \f$S' \sseq \Rset^m\f$, that is the largest set \f$S \sseq \Rset^n\f$ such that \f$\phi(S) \sseq S'\f$; formally, \f[ \phi^{-1}(S') \defeq \bigl\{\, \vect{v} \in \Rset^n \bigm| \phi(\vect{v}) \in S' \,\bigr\}. \f] The function mapping \f$\fund{\phi}{\Rset^n}{\Rset^m}\f$ is an affine transformation if there exist a matrix \f$A \in \Rset^m \times \Rset^n\f$ and a vector \f$\vect{b} \in \Rset^m\f$ such that, for all \f$\vect{x} \in \Rset^n\f$, we have \f$\phi(\vect{x}) = A\vect{x} + \vect{b}\f$. If \f$n = m\f$, then the function \f$\phi\f$ is said to be space-dimension preserving. Both \f$\Pset_n\f$ and \f$\CPset_n\f$ 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 \f$\cP \in \Pset_n\f$ for a given variable \f$x_k\f$ and linear expression \f$\mathrm{expr} = \sum_{i=0}^{n-1} a_i x_i + b\f$. This variable and expression determine the affine transformation \f$\phi\f$ that is to be used by the operator. That is, \f$\phi\f$ is the transformation defined by the matrix and vector \f[ A = \begin{pmatrix} 1 & & 0 & 0 & \cdots & \cdots & 0 \\ & \ddots & & \vdots & & & \vdots \\ 0 & & 1 & 0 & \cdots & \cdots & 0 \\ a_0 & \cdots & a_{k-1} & a_k & a_{k+1} & \cdots & a_{n-1} \\ 0 & \cdots & \cdots & 0 & 1 & & 0 \\ \vdots & & & \vdots & & \ddots & \\ 0 & \cdots & \cdots & 0 & 0 & & 1 \end{pmatrix}, \qquad \vect{b} = \begin{pmatrix} 0 \\ \vdots \\ 0 \\ b \\ 0 \\ \vdots \\ 0 \end{pmatrix} \f] where the \f$a_i\f$ (resp., \f$b\f$) occurs in the \f$(k+1)\f$st row in \f$A\f$ (resp., position in \f$\vect{b}\f$). Thus \f$\phi\f$ transforms any point \f$(x_0, \ldots, x_{n-1})^\transpose\f$ in the polyhedron \f$\cP\f$ to \f[ \Bigl(x_0, \ldots, \bigl(\textstyle{\sum_{i=0}^{n-1}} a_i x_i + b\bigr), \ldots, x_{n-1}\Bigr)^\transpose. \f] The affine image operator computes the affine image of \f$\cP\f$ under \f$\phi\f$. For instance, suppose the polyhedron \f$\cP\f$ to be transformed is the square in \f$\Rset^2\f$ generated by the set of points \f$\bigl\{ (0, 0)^\transpose, (0, 3)^\transpose, (3, 0)^\transpose, (3, 3)^\transpose \bigr\}\f$. Then, for example if the considered variable is \f$x_0\f$ and the linear expression \f$x_0 + 2 x_1 + 4\f$ (so that \f$k = 0\f$, \f$a_0 = 1, a_1 = 2, b = 4\f$), the affine image operator will translate \f$\cP\f$ to the parallelogram \f$\cP_1\f$ generated by the set of points \f$\bigl\{ (4, 0)^\transpose, (10, 3)^\transpose, (7, 0)^\transpose, (13, 3)^\transpose \bigr\}\f$ with height equal to the side of the square and oblique sides parallel to the line \f$x_0 - 2 x_1\f$. If the considered variable is as before (i.e., \f$k = 0\f$) but the linear expression is \f$x_1\f$ (so that \f$a_0 = 0, a_1 = 1, b = 0\f$), then the resulting polyhedron \f$\cP_2\f$ is the positive diagonal of the square. The affine preimage operator computes the affine preimage of \f$\cP\f$ under \f$\phi\f$. For instance, suppose now that we apply the affine preimage operator as given in the first example using variable \f$x_0\f$ and linear expression \f$x_0 + 2 x_1 + 4\f$ to the parallelogram \f$\cP_1\f$; then we get the original square \f$\cP\f$ back. If, on the other hand, we apply the affine preimage operator as given in the second example using variable \f$x_0\f$ and linear expression \f$x_1\f$ to \f$\cP_2\f$, then the resulting polyhedron is a line that corresponds to the \f$x_1\f$ axes. Observe that provided the coefficient \f$a_k\f$ of the considered variable in the linear expression is non-zero, the affine transformation is invertible. \anchor generalized_image Generalized Affine Images The library provides another operator which is a generalization of the affine image operator. Given a polyhedron \f$\cP \in \Pset_n\f$, an affine expression \f$\mathrm{lhs} = \sum_{i=0}^{n-1} a'_i x_i + b'\f$, a relation symbol \f$\mathord{\relsym} \in \{ <, \leq, =, \geq, > \}\f$, and an affine expression \f$\mathrm{rhs} = \sum_{i=0}^{n-1} a_i x_i + b\f$, the image of \f$\cP\f$ with respect to the transfer function \f$\mathrm{lhs} \relsym \mathrm{rhs}\f$ is defined as \f[ \sset{ (w_0, \ldots, w_{n-1})^\transpose \in \Rset^n }{ (v_0, \ldots, v_{n-1})^\transpose \in \cP, \\ \bigl( i \in \{0, \ldots, n-1\} \land a'_i = 0 \implies w_i = v_i \bigr), \\ \sum_{i=0}^{n-1} a'_i w_i + b' \relsym \sum_{i=0}^{n-1} a_i v_i + b }. \f] Note that, when \f$\mathrm{lhs} = x_k\f$ and \f$\mathord{\relsym} \in \{ = \}\f$, then the above operator is equivalent to the application of the standard affine image of \f$\cP\f$ with respect to the variable \f$x_k\f$ and the affine expression \f$\mathrm{rhs}\f$ (hence the name given to this operator). \anchor time_elapse Time-Elapse Operator The time-elapse operator has been defined in \ref HPR97 "[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 \f$\cP, \cQ \in \Pset_n\f$, the time-elapse between \f$\cP\f$ and \f$\cQ\f$, denoted \f$ \cP \nearrow \cQ\f$, is the smallest NNC polyhedron containing the set \f[ \bigl\{\, \vect{p} + \lambda \vect{q} \in \Rset^n \bigm| \vect{p} \in \cP, \vect{q} \in \cQ, \lambda \in \nonnegRset \,\bigr\}. \f] Note that, if \f$\cP,\cQ \in \CPset_n\f$ are closed polyhedra, the above set is also a closed polyhedron. In contrast, when \f$\cQ\f$ is not topologically closed, the above set might not be an NNC polyhedron. \anchor relation_with Relation-with Operators The library provides operators for checking the relation holding between an NNC polyhedron and either a constraint or a generator. Suppose \f$\cP\f$ is an NNC polyhedron and \f$\cC\f$ an arbitrary constraint system representing \f$\cP\f$. Suppose also that \f$ c = \bigl( \langle \vect{a}, \vect{x} \rangle \relsym b \bigr) \f$ is a constraint with \f$\mathord{\relsym} \in \{ =, \geq, > \}\f$ and \f$\cQ\f$ the set of points that satisfy \f$c\f$. The possible relations between \f$\cP\f$ and \f$c\f$ are as follows. - \f$\cP\f$ is disjoint from \f$c\f$ if \f$\cP \inters \cQ = \emptyset\f$; that is, adding \f$c\f$ to \f$\cC\f$ gives us the empty polyhedron. - \f$\cP\f$ strictly intersects \f$c\f$ if \f$\cP \inters \cQ \neq \emptyset\f$ and \f$\cP \inters \cQ \subset \cP\f$; that is, adding \f$c\f$ to \f$\cC\f$ gives us a non-empty polyhedron strictly smaller than \f$\cP\f$. - \f$\cP\f$ is included in \f$c\f$ if \f$\cP \sseq \cQ\f$; that is, adding \f$c\f$ to \f$\cC\f$ leaves \f$\cP\f$ unchanged. - \f$\cP\f$ saturates \f$c\f$ if \f$\cP \sseq \cH\f$, where \f$\cH\f$ is the hyperplane induced by constraint \f$c\f$, i.e., the set of points satisfying the equality constraint \f$\langle \vect{a}, \vect{x} \rangle = b\f$; that is, adding the constraint \f$\langle \vect{a}, \vect{x} \rangle = b\f$ to \f$\cC\f$ leaves \f$\cP\f$ unchanged. The polyhedron \f$\cP\f$ subsumes the generator \f$g\f$ if adding \f$g\f$ to any generator system representing \f$\cP\f$ does not change \f$\cP\f$. \anchor bounding_boxes Intervals, boxes and bounding boxes An interval in \f$\Rset\f$ 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 \f$\Rset\f$. An \f$n\f$-dimensional box \f$\cB\f$ in \f$\Rset^n\f$ is a sequence of \f$n\f$ intervals in \f$\Rset\f$. The polyhedron \f$\cP\f$ represents a box \f$\cB\f$ in \f$\Rset^n\f$ if \f$\cP\f$ is described by a constraint system in \f$\Rset^n\f$ that consists of one constraint for each bounded bound (lower and upper) in an interval in \f$\cB\f$: Letting \f$\vect{e}_i = (0, \ldots, 1, \ldots, 0)^\transpose\f$ be the vector in \f$\Rset^n\f$ with 1 in the \f$i\f$'th position and zeroes in every other position; if the lower bound of the \f$i\f$'th interval in \f$\cB\f$ is bounded, the corresponding constraint is defined as \f$\langle \vect{e}_i, \vect{x} \rangle \relsym b\f$, where \f$b\f$ is the value of the bound and \f$\mathord{\relsym}\f$ is \f$\mathord{\geq}\f$ if it is a closed bound and \f$\mathord{>}\f$ if it is an open bound. Similarly, if the upper bound of the \f$i\f$'th interval in \f$\cB\f$ is bounded, the corresponding constraint is defined as \f$\langle\vect{e}_i,\vect{x}\rangle \relsym b\f$, where \f$b\f$ is the value of the bound and \f$\mathord{\relsym}\f$ is \f$\mathord{\leq}\f$ if it is a closed bound and \f$\mathord{<}\f$ if it is an open bound. If every bound in the intervals defining a box \f$\cB\f$ is either closed and bounded or open and unbounded, then \f$\cB\f$ represents a closed polyhedron. The bounding box of an NNC polyhedron \f$\cP\f$ is the smallest \f$n\f$-dimensional box containing \f$\cP\f$. 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. \anchor H79_widening Widening Operators 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 \ref Hal79 "[Hal79]", also described in \ref HPR97 "[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 \f$\cP \in \Pset_n\f$ using the NNC polyhedron \f$\cQ \in \Pset_n\f$: - allows for equalities in \f$\cP\f$ and \f$\cQ\f$ (the original definition is restricted to inequalities); - requires as a precondition that \f$\cQ \sseq \cP\f$. \anchor BHRZ03_widening The second widening operator, that we call BHRZ03-widening, is an instance of the specification provided in \ref BHRZ03a "[BHRZ03a]". This operator also requires as a precondition that \f$\cQ \sseq \cP\f$ 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. \anchor widening_with_tokens Widening with Tokens 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 \f$k\f$ and only apply widenings starting from the \f$k\f$-th iteration. The library also supports an improved widening delay strategy, that we call widening with tokens \ref BHRZ03a "[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 \f$k\f$ of tokens, which will be used if and when needed. When there are no tokens left, the widening is always applied. \anchor extrapolation Extrapolation Operators 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 \ref HPR97 "[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 \ref HPR97 "[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 \ref bounding_boxes "bounding box" enclosing the two argument polyhedra. \section powerset The Powerset Construction The PPL provides the finite powerset construction; this takes a pre-existing domain and upgrades it to one that can represent disjunctive information (by using a finite number of disjucts). The construction follows the approach described in \ref Bag98 "[Bag98]", also summarised in \ref BHZ04 "[BHZ04]" where there is an account of generic widenings for the powerset domain (some of which are supported in the instantiation of this construction by the domain of convex polyhedra and described in Section \ref poly_powerset). \anchor powerset_domain The Powerset Domain The domain is built from a pre-existing base-level domain \f$D\f$ which must include an entailment relation `\f$\mathord{\entails}\f$', a meet operation `\f$\mathord{\meet}\f$', a top element `\f$\true\f$' and bottom element `\f$\false\f$'. As the intended semantics of an element of the powerset of the base-level domain is that of disjunction, elements of the powerset are always reduced to semantically-equivalent non-redundant elements. A set \f$\cS \in \wp(D)\f$ is called non-redundant with respect to `\f$\mathord{\entails}\f$' if and only if \f$\false \notin \cS\f$ and \f$\forall d_1, d_2 \in \cS \itc d_1 \entails d_2 \implies d_1 = d_2\f$. The set of finite non-redundant subsets of \f$D\f$ (with respect to `\f$\mathord{\entails}\f$') is denoted by \f$\wpfn{D}{\entails}\f$. The reduction function \f$\fund{\nonredmap}{\wpf(D)}{\wpfn{D}{\entails}}\f$ mapping a finite set into its non-redundant counterpart is defined, for each \f$\cS \in \wpf(D)\f$, by \f[ \nonredmap(\cS) \defeq \cS \setdiff \{\, d \in \cS \mid d = \false \text{ or } \exists d' \in \cS \st d \sentails d' \,\}. \f] The restriction to the finite subsets reflects the fact that here disjunctions are implemented by explicit collections of elements of the base-level abstract domain. As a consequence of this restriction, for any \f$\cS \in \wpf(D)\f$ such that \f$\cS \neq \{ \false \}\f$, \f$\nonredmap(\cS)\f$ is the (finite) set of the maximal elements of \f$\cS\f$. The finite powerset domain over a domain \f$D\f$ is the set of all finite reduced sets of \f$D\f$ and denoted by \f$D_{\smallP}\f$. The domain includes an approximation ordering `\f$\mathord{\entailsP}\f$' defined so that \f$\cS_1 \entailsP \cS_2\f$ if and only if \f[ \forall d_1 \in \cS_1 \itc \exists d_2 \in \cS_2 \st d_1 \entails d_2. \f] Therefore the top element is \f$\{\true\}\f$ and the bottom element is the emptyset. \section ps_operations Operations on the Powerset Construction In this section we briefly describe the generic operations on Powerset Domains that are provided by the library for any given base-level domain \f$D\f$. \anchor ps_meet_upper_bound Meet and Upper Bound Given the sets \f$\cS_1\f$ and \f$\cS_2 \in D_{\smallP}\f$, the meet and upper bound operators provided by the library returns the set \f$\nonredmap\bigl(\{d_1 \meet d_2 \,|\, d_1 \in \cS_1, d_2 \in \cS_2\}\bigr)\f$ and reduced set union \f$\nonredmap(\cS_1 \union \cS_2)\f$ respectively. \anchor ps_add_disjunct Adding a Disjunct Given the powerset element \f$\cS \in D_{\smallP}\f$ and the base-level element \f$d \in D\f$, the add_disjunct operator provided by the library returns the powerset element \f$\nonredmap\bigl(\cS \union \{d\}\bigr)\f$. \anchor ps_collapse Collapsing a Powerset Element If the given powerset element is not empty, then the collapse operator returns the singleton powerset consisting of an upper-bound of all the disjuncts. \section poly_powerset The Polyhedra Powerset Domain The Polyhedra powerset domain \f$(\Pset_n)_{\smallP}\f$ provided by the PPL is the finite powerset domain (defined in Section \ref powerset) over the domain of NNC polyhedra \f$\Pset_n\f$. In addition to the operations described for the generic powerset domain in Section \ref ps_operations, we provide some operations that are specific to this instantiation. Of these, most correspond to the application of the equivalent operation on each of the NNC polyhedron that are in the given set. Here we just describe those operations that are particular to the polyhedra powerset domain. \anchor pps_geometric Geometric Comparisons Given the sets \f$\cS_1, \cS_2 \in (\Pset_n)_{\smallP}\f$, then we say that \f$\cS_1\f$ geometrically_covers \f$\cS_2\f$ if every point (in some element) in a polyhedron in \f$\cS_2\f$ is also a point in a polyhedron in \f$\cS_1\f$. If \f$\cS_1\f$ geometrically_covers \f$\cS_2\f$ and \f$\cS_2\f$ geometrically_covers \f$\cS_1\f$, then we say that they are geometrically_equal. \anchor pps_pairwise_merge Pairwise Merge Given the powerset \f$\cS \in (\Pset_n)_{\smallP}\f$, then the pairwise_merge operator takes pairs of distinct elements in \f$\cS\f$ whose poly-hull is the same as their set-theoretical union and replaces them by their union. This replacement is done recursively so that, for each pair \f$\cP, \cQ\f$ of distinct polyhedra in the result set, we have \f$\cP \uplus \cQ \neq \cP \union \cQ\f$. \anchor pps_bgp99_extrapolation Extrapolation Operators The library implements a generalization of the extrapolation operator for powerset domains proposed in \ref BGP99 "[BGP99]". The operator BGP99_extrapolation_assign is made parametric by allowing for the specification of a base-level extrapolation operator different from the H79 widening (e.g., the BHRZ03 widening can be used). Note that, in the general case, this operator cannot guarantee the convergence of the iteration sequence in a finite number of steps (for a counter-example, see \ref BHZ04 "[BHZ04]"). \anchor pps_certificate_widening Certificate-Based Widenings The PPL library provides support for the specification of proper widening operators on the powerset domain of convex polyhedra. In particular, this version of the library implements an instance of the certificate-based widening framework proposed in \ref BHZ03b "[BHZ03b]". A finite convergence certificate for an extrapolation operator is a formal way of ensuring that such an operator is indeed a widening on the considered domain. Given a widening operator on the base-level domain, together with the corresponding convergence certificate, the BHZ03 framework shows how it is possible to lift this widening so as to work on the finite powerset domain, while still ensuring convergence in a finite number of iterations. Being highly parametric, the BHZ03 widening framework can be instantiated in many ways. The current implementation provides the templatic operator BHZ03_widening_assign\ which only exploits a fraction of this generality, by allowing the user to specify the base-level widening function and the corresponding certificate. The widening strategy is fixed and uses two extrapolation heuristics: first, the least upper bound is tried; second, the \ref pps_bgp99_extrapolation "BGP99 extrapolation operator" is tried, possibly applying \ref pps_pairwise_merge "pairwise merging". If both heuristics fail to converge according to the convergence certificate, then an attempt is made to apply the base-level widening to the poly-hulls of the two arguments, possibly improving the result obtained by means of the \ref poly_difference "poly-difference" operator. For more details and a justification of the overall approach, see \ref BHZ03b "[BHZ03b]" and \ref BHZ04 "[BHZ04]". The library provides two convergence certificates: while \ref Parma_Polyhedra_Library::BHRZ03_Certificate "BHRZ03_Certificate" is compatible with both the BHRZ03 and the H79 widenings, \ref Parma_Polyhedra_Library::H79_Certificate "H79_Certificate" is only compatible with the latter. Note that using different certificates will change the results obtained, even when using the same base-level widening operator. It is also worth stressing that it is up to the user to see that the widening operator is actually compatible with a given convergence certificate. If such a requirement is not met, then an extrapolation operator will be obtained. \section use_of_library Using the Library A Note on the Implementation of the Operators When adopting the double description method for the representation of convex polyhedra, the implementation of most of the operators 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. One of the cases 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 Object-Orientation and Polymorphism: A Disclaimer The PPL library is mainly a collection of so-called ``concrete data types'': while providing the user with a clean and friendly interface, these types are not meant to --- i.e., they should not --- be used polymorphically (since, e.g., most of the destructors are not declared virtual). In practice, this restriction means that the library types should not be used as public base classes to be derived from. A user willing to extend the library types, adding new functionalities, often can do so by using containment instead of inheritance; even when there is the need to override a protected method, non-public inheritance should suffice. 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: \code // 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! \endcode As a rule of thumb, if a polyhedron plays any role in a computation (even as a const parameter), then any previously computed reference to parts of the polyhedron may have been invalidated. Note that, in the example above, the computation of the constraint system could have been placed after the uses of the iterator 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: \code GenSys gs = ph.generators(); \endcode The same observations, modulo syntactic sugar, apply to the operators defined in the C interface of the library. \section bibliography Bibliography
[Bag98]
\anchor Bag98 R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Science of Computer Programming, 30(1-2):119-155, 1998.
[BGP99]
\anchor BGP99 T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747-789, 1999.
[BHRZ03a]
\anchor BHRZ03a R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337-354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.
[BHRZ03b]
\anchor BHRZ03b R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Quaderno 312, Dipartimento di Matematica, Università di Parma, Italy, 2003. Available at http://www.cs.unipr.it/Publications/.
[BHZ02a]
\anchor BHZ02a R. Bagnara, P. M. Hill, and E. Zaffanella. A new encoding and implementation of not necessarily closed convex polyhedra. Quaderno 305, Dipartimento di Matematica, Università di Parma, Italy, 2002. Available at http://www.cs.unipr.it/Publications/.
[BHZ02b]
\anchor BHZ02b R. Bagnara, P. M. Hill, and E. Zaffanella. A new encoding of not necessarily closed convex polyhedra. In M. Carro, C. Vacheret, and K.-K. Lau, editors, Proceedings of the 1st CoLogNet Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems, pages 147-153, Madrid, Spain, 2002. Published as TR Number CLIP4/02.0, Universidad Politécnica de Madrid, Facultad de Informática.
[BHZ03a]
\anchor BHZ03a R. Bagnara, P. M. Hill, and E. Zaffanella. A new encoding and implementation of not necessarily closed convex polyhedra. In M. Leuschel, S. Gruner, and S. Lo Presti, editors, Proceedings of the 3rd Workshop on Automated Verification of Critical Systems, pages 161-176, Southampton, UK, 2003. Published as TR Number DSSE-TR-2003-2, University of Southampton.
[BHZ03b]
\anchor BHZ03b R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. In B. Steffen and G. Levi, editors, Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004), volume 2937 of Lecture Notes in Computer Science, pages 135-148, Venice, Italy, 2003. Springer-Verlag, Berlin.
[BHZ04]
\anchor BHZ04 R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. Quaderno 349, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.
[BJT99]
\anchor BJT99 F. Besson, T. P. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In A. Cortesi and G. Filé, editors, Static Analysis: Proceedings of the 6th International Symposium, volume 1694 of Lecture Notes in Computer Science, pages 51-68, Venice, Italy, 1999. Springer-Verlag, Berlin.
[BRZH02a]
\anchor BRZH02a R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 213-229, Madrid, Spain, 2002. Springer-Verlag, Berlin.
[BRZH02b]
\anchor BRZH02b R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286, Dipartimento di Matematica, Università di Parma, Italy, 2002. See also \ref BRZH02c "[BRZH02c]". Available at http://www.cs.unipr.it/Publications/.
[BRZH02c]
\anchor BRZH02c R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Errata for technical report ``Quaderno 286''. Available at http://www.cs.unipr.it/Publications/, 2002. See \ref BRZH02b "[BRZH02b]".
[CC92]
\anchor CC92 P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269-295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.
[CH78]
\anchor CH78 P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84-96, Tucson, Arizona, 1978. ACM Press.
[Che64]
\anchor Che64 N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear equations. U.S.S.R. Computational Mathematics and Mathematical Physics, 4(4):151-158, 1964.
[Che65]
\anchor Che65 N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. U.S.S.R. Computational Mathematics and Mathematical Physics, 5(2):228-233, 1965.
[Che68]
\anchor Che68 N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics, 8(6):282-293, 1968.
[Dan63]
\anchor Dan63 G. B. Dantzig. Linear Programming and Extensions. Princeton University Press, Princeton, NJ, 1963.
[FP96]
\anchor FP96 K. Fukuda and A. Prodon. Double description method revisited. In M. Deza, R. Euler, and Y. Manoussakis, editors, Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5, 1995, Selected Papers, volume 1120 of Lecture Notes in Computer Science, pages 91-111. Springer-Verlag, Berlin, 1996.
[Fuk98]
\anchor Fuk98 K. Fukuda. Polyhedral computation FAQ. Swiss Federal Institute of Technology, Lausanne and Zurich, Switzerland, available at http://www.ifor.math.ethz.ch/~fukuda/fukuda.html, 1998.
[GDD+04]
\anchor GDMDRS04 D. Gopan, F. DiMaio, N. Dor, T. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, volume 2988 of Lecture Notes in Computer Science, pages 512-529. Springer-Verlag, Berlin, 2004.
[GJ00]
\anchor GJ00 E. Gawrilow and M. Joswig. 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.
[GJ01]
\anchor GJ01 E. Gawrilow and M. Joswig. 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.
[Hal79]
\anchor Hal79 N. Halbwachs. Détermination Automatique de Relations Linéaires Vérifiées par les Variables d'un Programme. Thèse de 3ème cycle d'informatique, Université scientifique et médicale de Grenoble, Grenoble, France, March 1979.
[Hal93]
\anchor Hal93 N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, Computer Aided Verification: Proceedings of the 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 333-346, Elounda, Greece, 1993. Springer-Verlag, Berlin.
[HH95]
\anchor HH95 T. A. Henzinger and P.-H. Ho. A note on abstract interpretation strategies for hybrid automata. In P. J. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 252-264. Springer-Verlag, Berlin, 1995.
[HKP95]
\anchor HKP95 N. Halbwachs, A. Kerbrat, and Y.-E. Proy. POLyhedra INtegrated Environment. Verimag, France, version 1.0 of POLINE edition, September 1995. Documentation taken from source code.
[HLW94]
\anchor HLW94 V. Van Dongen H. Le Verge and D. K. Wilde. Loop nest synthesis using the polyhedral library. Publication interne 830, IRISA, Campus de Beaulieu, Rennes, France, 1994.
[HPR94]
\anchor HPR94 N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In B. Le Charlier, editor, Static Analysis: Proceedings of the 1st International Symposium, volume 864 of Lecture Notes in Computer Science, pages 223-237, Namur, Belgium, 1994. Springer-Verlag, Berlin.
[HPR97]
\anchor HPR97 N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157-185, 1997.
[HPWT01]
\anchor HPWT01 T. A. Henzinger, J. Preussig, and H. Wong-Toi. Some lessons from the hytech experience. In Proceedings of the 40th Annual Conference on Decision and Control, pages 2887-2892. IEEE Computer Society Press, 2001.
[Jea02]
\anchor Jea02 B. Jeannet. Convex Polyhedra Library, release 1.1.3c edition, March 2002. Documentation of the ``New Polka'' library available at http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html.
[Kuh56]
\anchor Kuh56 H. W. Kuhn. Solvability and consistency for linear equations and inequalities. American Mathematical Monthly, 63:217-232, 1956.
[Le 92]
\anchor Le 92 H. Le Verge. A note on Chernikova's algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.
[Loe99]
\anchor Loe99 V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Available at http://icps.u-strasbg.fr/~loechner/polylib/, March 1999. Declares itself to be a continuation of \ref Wil93 "[Wil93]".
[LW97]
\anchor LW97 V. Loechner and D. K. Wilde. Parameterized polyhedra and their vertices. International Journal of Parallel Programming, 25(6):525-549, 1997.
[Mas92]
\anchor Mas92 F. Masdupuy. Array operations abstraction using semantic analysis of trapezoid congruences. In Proceedings of the 6th ACM International Conference on Supercomputing, pages 226-235, Washington, DC, USA, 1992. ACM Press.
[Mas93]
\anchor Mas93 F. Masdupuy. Array Indices Relational Semantic Analysis Using Rational Cosets and Trapezoids. Thèse d'informatique, École Polytechnique, Palaiseau, France, December 1993.
[MRTT53]
\anchor MRTT53 T. S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall. The double description method. In H. W. Kuhn and A. W. Tucker, editors, Contributions to the Theory of Games - Volume II, number 28 in Annals of Mathematics Studies, pages 51-73. Princeton University Press, Princeton, New Jersey, 1953.
[NR00]
\anchor NR00 S. P. K. Nookala and T. Risset. A library for Z-polyhedral operations. Publication interne 1330, IRISA, Campus de Beaulieu, Rennes, France, 2000.
[NW88]
\anchor NW88 G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. Wiley Interscience Series in Discrete Mathematics and Optimization. John Wiley & Sons, 1988.
[Sch99]
\anchor Sch99 A. Schrijver. Theory of Linear and Integer Programming. Wiley Interscience Series in Discrete Mathematics and Optimization. John Wiley & Sons, 1999.
[Sri93]
\anchor Sri93 D. Srivastava. Subsumption and indexing in constraint query languages with linear arithmetic constraints. Annals of Mathematics and Artificial Intelligence, 8(3-4):315-343, 1993.
[SW70]
\anchor SW70 J. Stoer and C. Witzgall. Convexity and Optimization in Finite Dimensions I. Springer-Verlag, Berlin, 1970.
[Wey35]
\anchor Wey35 H. Weyl. Elementare theorie der konvexen polyeder. Commentarii Mathematici Helvetici, 7:290-306, 1935. English translation in \ref Wey50 "[Wey50]".
[Wey50]
\anchor Wey50 H. Weyl. The elementary theory of convex polyhedra. In H. W. Kuhn, editor, Contributions to the Theory of Games - Volume I, number 24 in Annals of Mathematics Studies, pages 3-18. Princeton University Press, Princeton, New Jersey, 1950. Translated from \ref Wey35 "[Wey35]" by H. W. Kuhn.
[Wil93]
\anchor Wil93 D. K. Wilde. A library for doing polyhedral operations. Master's thesis, Oregon State University, Corvallis, Oregon, December 1993. Also published as IRISA Publication interne 785, Rennes, France, 1993.
\if Include_Implementation_Details \section prelims Further notation and terminology Proposition A polyhedron is a convex set. Minkowski's theorem Let \f$P = \{\, \vect{x} \in \Rset^n \mid A\vect{x} \geq \vect{b} \,\}\f$ be a non-empty polyhedron where \f$\prank(A) = n\f$. Let \f$V\f$ be the set of vertices and \f$R\f$ the set of extreme rays of \f$P\f$. Let also \f$\mathcal{V}\f$ be the set of convex combinations of \f$V\f$ and \f$\mathcal{R}\f$ the set of positive combinations of \f$R\f$. Then \f[ P = \mathcal{V} + \mathcal{R}. \f] Informally, this theorem states that, whenever a polyhedron \f$P\f$ has a vertex, there exists a decomposition such that - \f$V\f$ is the set of all vertices of \f$P\f$; - \f$R\f$ is the set of all extreme rays of \f$P\f$; and - \f$L = \emptyset\f$. The conditions that \f$P\f$ is not empty and \f$\prank(A) = n\f$ are equivalent to the condition that \f$P\f$ has a vertex. (See also Nemhauser and Wolsey - Integer and Combinatorial Optimization - propositions 4.1 and 4.2 on pages 92 and 93). Proposition Under the same hypotheses of Minkowsky's theorem, if \f$P\f$ is a rational polyhedron then all the vertices in \f$V\f$ have rational coefficients and we can consider a set \f$R\f$ of extreme rays having rational coefficients only. The second theorem, called Weil's theorem, states that any system of generators having rational coefficients defines a rational polyhedron: Weil's theorem If \f$A\f$ is a rational \f$m \times n\f$ matrix, \f$B\f$ is a rational \f$m' \times n\f$ matrix and \f[ Q = \sset{ \vect{x} \in \Rset^n }{ \vect{x}^\transpose = \vect{y}^\transpose A + \vect{z}^\transpose B, \\ \vect{y} = (y_0, \ldots, y_{m-1})^\transpose \in \Rset_+^{m}, \sum_{k=0}^{m-1} y_k = 1, \\ \vect{z} \in \Rset_+^{m'} }, \f] then \f$Q\f$ is a rational polyhedron. In fact, since \f$Q\f$ consists of the sum of convex combinations of the rows of \f$A\f$ with positive combinations of the rows of \f$B\f$, we can think of \f$A\f$ as the matrix of vertices and \f$B\f$ as the matrix of rays. Polyhedron dimension A non-empty polyhedron \f$P \sseq \Rset^n\f$ is of dimension \f$k\f$, denoted by \f$\pdim(P) = k\f$, if the maximum number of affinely independent points in \f$P\f$ is \f$k + 1\f$. \note What is the dimension of the empty polyhedron? If the above definition is applied to an empty polyhedron, then the answer would be \f$-1\f$. The dimension \f$k \leq n\f$ of an NNC polyhedron \f$P \in \Pset_n\f$ must not be confused with the space dimension \f$n\f$ of \f$P\f$, which is the dimension of the enclosing vector space. In particular, we can have \f$\pdim(P) \neq \pdim(Q)\f$ even though \f$P\f$ and \f$Q\f$ are dimension-compatible; and vice versa, \f$P\f$ and \f$Q\f$ may be dimension-incompatible polyhedra even though \f$\pdim(P) = \pdim(Q)\f$. Cone A set \f$C \sseq \Rset^n\f$ is a cone if \f[ \vect{x} \in C \Rightarrow \lambda \vect{x} \in C \text{ for all } \lambda \in \Rset, \lambda \geq 0. \f] Polyhedral cone The polyhedron \f$P = \{\,\vect{x} \in \Rset^n \mid A\vect{x} \geq \vect{0}\,\}\f$ is a convex cone and is called polyhedral cone. A polyhedral cone is either pointed, having the origin as its only vertex, or has no vertices at all. Lineality space Given a polyhedron \f$P = \{\,\vect{x} \in \Rset^n \mid A\vect{x} \geq \vect{b}\,\}\f$, the lineality space of \f$P\f$ is the set \f[ \{\, \vect{x} \in P \mid A\vect{x} = \vect{0} \,\} \f] and it is denoted by \f$\linspace(P)\f$. Linear independence A finite set of points \f$\{ \vect{x}_1, \ldots, \vect{x}_k \} \sseq \Rset^n\f$ is linearly independent if, for all \f$\lambda_1, \ldots, \lambda_k \in \Rset\f$, the set of equations \f[ \sum_{i = 1}^k \lambda_i \vect{x}_i = \vect{0} \f] implies that, for each \f$i = 1\f$, \f$\ldots\f$, \f$k\f$, \f$\lambda_i = 0\f$. Note that the maximum number of linearly independent points in \f$\Rset^n\f$ is \f$n\f$. Proposition If \f$A\f$ is an \f$m \times n\f$ matrix, the maximum number of linearly independent rows of \f$A\f$, viewed as vectors of \f$\Rset^n\f$, equals the maximum number of linearly independent columns of \f$A\f$, viewed as vectors of \f$\Rset^m\f$. Rank The maximum number of linearly independent rows (columns) of a matrix \f$A\f$ is the rank of \f$A\f$ and is denoted by \f$\prank(A)\f$. Affine independence A finite set of points \f$\{ \vect{x}_1, \ldots, \vect{x}_k \} \sseq \Rset^n\f$ is affinely independent if, for all \f$\lambda_1, \ldots, \lambda_k \in \Rset\f$, the set of equations \f[ \sum_{i = 1}^k \lambda_i \vect{x}_i = \vect{0}, \quad \sum_{i = 1}^k \lambda_i = 0 \f] implies that, for each \f$i = 1, \ldots, k\f$, \f$\lambda_i = 0\f$. Note that linear independence implies affine independence, but the converse is not true. Moreover the maximum number of affinely independent points in \f$\Rset^n\f$ is \f$n + 1\f$ (e.g., \f$n\f$ linearly independent points and the origin \f$\vect{0}\f$). \section homogeneous Homogeneous Systems To simplify the operations on polyhedra, each polyhedron is first transformed to a homogeneous cone in which the original polyhedron is embedded. Corresponding Polyhedral Cone The transformation changes the inhomogeneous system of constraints in \f$n\f$ variables, representing a polyhedron \f$P \in \Rset^n\f$, into a homogeneous system in \f$n + 1\f$ variables, representing a polyhedral cone \f$C \in \Rset^{n + 1}\f$, so that each point \f$\vect{x} \in P\f$ corresponds to a point \f$\vect{x}' = (\xi \vect{x}^\transpose, \xi)^\transpose \in C\f$ where \f$\xi \geq 0\f$. That is, \f[ P = \{\,\vect{x} \mid A\vect{x} \geq \vect{b}\,\} = \{\,\vect{x} \mid A\vect{x} - \vect{b} \geq \vect{0}\,\} \f] \f[ C = \{\, (\xi \vect{x}^\transpose, \xi)^\transpose \mid \xi A\vect{x} - \xi \vect{b} \geq \vect{0}, \xi \geq 0 \,\} = \{\,\vect{x}' \mid A'\vect{x}' \geq \vect{0}\,\} \f] where: \f$\vect{x}' = (\xi \vect{x}^\transpose, \xi)^\transpose \in \Rset^{n + 1}\f$; \f$A'\f$ is the \f$(m+1) \times (n+1)\f$ matrix having, for its first \f$m\f$ rows, the submatrix \f$(A, -\vect{b}) \in \Rset^m \times \Rset^{n + 1}\f$; and, for the (\f$m + 1\f$)'st row, \f$(\vect{0}^\transpose, 1)\f$ where \f$\vect{0} \in \Rset^n\f$. We call \f$C\f$ the corresponding polyhedral cone for \f$P\f$. The (\f$m+1\f$)'st row \f$(\vect{0}^\transpose, 1)\f$ represents the positivity constraint \f$1 \geq 0\f$. Note that \f$P\f$ is contained in \f$C\f$ since the intersection of \f$C\f$ with the hyperplane defined by the equality \f$\xi = 1\f$ is \f$P\f$. Therefore, it is always possible to transform a polyhedron \f$P\f$ to its corresponding polyhedral cone \f$C\f$ and then recover \f$P\f$ by means of this intersection. As \f$C\f$ always includes the origin and, hence, is non-empty, by Minkowski's theorem, it can also be represented by a system of generators. The systems of generators for \f$P\f$ and \f$C\f$ are such that: - Each vertex \f$\vect{v}\f$ in \f$P\f$ corresponds to a ray \f$(\vect{v}^\transpose, d)^\transpose\f$ with \f$d \neq 0\f$, in \f$C\f$. - Each ray \f$\vect{r}\f$ in \f$P\f$ corresponds to the ray \f$(\vect{r}^\transpose, 0)^\transpose\f$ in \f$C\f$. - Every ray in \f$C\f$ corresponds to a vertex or ray in \f$P\f$. - The origin in \f$\Rset^{n+1}\f$ is a point in \f$C\f$. Thus, in the cone \f$C\f$, a ray derived from a vertex in \f$P\f$ differs from a ray derived from a ray in \f$P\f$ only in that, for a vertex, the (\f$n+1\f$)'st term is different from zero and, for a ray, it is zero. Double Description Let \f$P \in \Rset^n \f$ be a polyhedron and \f$C \in \Rset^{n+1} \f$ the corresponding polyhedral cone. Then the dual representations, the systems of constraints and generators representing \f$C\f$, form the double description for \f$P\f$. Note that, in a double description for a non-empty polyhedron, the system of constraints subsumes the positivity constraint \f$1 \geq 0\f$ while the system of generators (which has only rays and lines corresponding to the vertices, rays and lines for \f$P\f$) implicitly assumes the origin in \f$\Rset^{n+1} \f$ as a point so that the cone \f$C\f$ represented by the generators is non-empty. PPL Polyhedron Representation In the PPL, a polyhedron is represented by one or both of the representations in its double description. Thus, in the sequel, by PPL representation of a polyhedra, we are referring to the corresponding representation of its corresponding polyhedral cone. Valid linear inequalities Let \f$P\f$ be a convex polyhedron (or polytope) in \f$\Rset^n\f$. For a real \f$n\f$-vector \f$\vect{c}\f$ and a real number \f$b\f$, a linear inequality \f$\langle \vect{c}, \vect{x} \rangle \geq b\f$ (briefly denoted by \f$(\vect{c},b)\f$) is called valid for \f$P\f$ if it is satisfied by all points \f$\vect{x} \in P\f$. Redundancy -# In a system of equalities, if an equality is a linear combination of the others, it is said to be dependent upon them; the dependent equality is called redundant. A system containing no redundant equality is called independent. -# In a system of inequalities, an inequality is said to be redundant if it can be eliminated from the system obtaining a system equivalent to the previous one, i.e., having the same solutions. Given a polyhedron \f$P\f$ generated by \f$V\f$ vertices, \f$R\f$ rays and \f$L\f$ lines, we say that: -# \f$L\f$ is irredundant if \f$L\f$ is a set of linearly independent lines; and -# a ray \f$\vect{r}_1\in R\f$ is redundant if there exists another ray \f$\vect{r}_2 \in R\f$ and there exists \f$\lambda \in \Rset, \lambda > 0\f$ such that \f$\vect{r}_1 = \lambda \vect{r}_2\f$. Note that, in the PPL representation of a polyhedron \f$P\f$, vertices are represented as rays so that this concept of a redundant ray also applies to the vertices of \f$P\f$. Face If \f$(\vect{c},b)\f$ is a valid inequality for \f$P\f$, and \f$F = \{\,\vect{x} \in P \mid \langle \vect{c}, \vect{x} \rangle = b\,\}\f$, \f$F\f$ is called a face of \f$P\f$ and we say that the inequality represents \f$F\f$. A face \f$F\f$ is said to be proper if \f$F \neq \emptyset\f$ and \f$F \neq P\f$. When \f$F\f$ is non-empty, we say that \f$(\vect{c},b)\f$ supports \f$P\f$. The empty polyhedron and the universe polyhedron both have no proper faces, because the only face of an empty polyhedron is itself, while the faces of the universe polyhedron are itself and the emptyset. Let \f$P\f$ be a non-empty polyhedron. The set \f[ F = \{ \vect{p} \} + \linspace (P), \f] where \f$\vect{p}\f$ is a point of \f$P\f$ and the symbol '\f$+\f$' denotes the Minkowski's sum, is a minimal proper face of the polyhedron if \f$F\f$ is a proper face of \f$P\f$. Facet A proper face \f$F\f$ of \f$P\f$ is a facet (or maximal proper face) of \f$P\f$ if it is not strictly included into any other proper face of \f$P\f$. The dimension of a facet is equal to \f$\pdim(P) - 1\f$. Proposition Let \f$P\f$ a polyhedron in \f$\Rset^n\f$. The set of all faces is a lattice under inclusion: the minimal face is the emptyset, while the maximal face is the polyhedron. Proposition Let \f$P \neq \emptyset\f$ be a polyhedron in \f$\Rset^n\f$ and \f$C\f$ be the polyhedral cone in \f$\Rset^{n+1}\f$ obtaining by \f$P\f$ with the homogenization, then: -# the only minimal proper face of \f$C\f$ is \f$\linspace(C)\f$; -# let \f$\vect{y} \in C\f$ be different from \f$\vect{0}\f$ and \f$\cone\{\vect{y}\}\f$ be defined as \f$\{ \lambda \vect{y} \mid \lambda \geq 0 \}\f$. If the set \f$F = \cone\{\vect{y}\} + \linspace(C)\f$ is a proper face of \f$C,\f$ then \f$\vect{y}\f$ is an extremal ray of \f$C.\f$ Ray space Given the decomposition \f$\mathcal{V} + \mathcal{R} + \mathcal{L}\f$ of a polyhedron \f$P\f$ the set \f$\mathcal{V} + \mathcal{R}\f$ is called the ray space of \f$P\f$ and denoted by \f$\mathop{\mathrm{ray space}}(P)\f$. Thus a polyhedron \f$P\f$ can be always decomposed in its \f$\linspace\f$ and its \f$\mathop{\mathrm{ray space}}\f$. Note that, since \f$\linspace(P)\f$ and \f$\mathop{\mathrm{ray space}}(P)\f$ are special polyhedra, their dimension can be computed using the definition of dimension given for polyhedra. The spaces defined are connected by some consistency rules shown below. Dimensionality rules In \f$\Rset^n\f$ - The dimension of the \f$\linspace\f$ is the rank of any set of lines that span the space. - The dimension of the polyhedron is the dimension of the \f$\mathop{\mathrm{ray space}}\f$ plus the dimension of the \f$\linspace\f$. - The dimension of the \f$\mathop{\mathrm{ray space}}\f$ is \f$n\f$ minus the number of irredundant lines minus the number of irredundant equalities. The proofs of these properties can be obtained considering the definitions of dimension and the decomposition of a polyhedron. Saturation Let us consider a ray \f$\vect{r} \in \Rset^n\f$ and an inequality \f$(\vect{a}, 0)\f$ where \f$\vect{a} \in \Rset^n\f$. Then we say that: - \f$r\f$ saturates the inequality if \f$\langle \vect{a}, \vect{r} \rangle = 0\f$; - \f$r\f$ verifies the inequality if \f$\langle \vect{a}, \vect{r} \rangle > 0\f$; - \f$r\f$ violates the inequality if \f$\langle \vect{a}, \vect{r} \rangle < 0\f$. Similarly, considering an equality \f$\langle \vect{a}, \vect{x} \rangle = 0\f$: - \f$\vect{r}\f$ saturates the equality if \f$\langle \vect{a}, \vect{r} \rangle = 0\f$; - \f$\vect{r}\f$ does not verify the equality if \f$\langle \vect{a}, \vect{r} \rangle \neq 0\f$. A constraint (i.e., an equality or an inequality) is satisfied by a ray if the ray saturates or verifies the constraint. Proposition Let \f$C \sseq \Rset^n\f$ be a polyhedral cone and \f$\vect{y}_1, \vect{y}_2 \in C\f$. If the sets \f$F_i = \cone\{\vect{y}_i\} + \linspace(C)\f$ with \f$i = 1, 2\f$ are proper faces of \f$C\f$, \f$F_1\f$ is equal to \f$F_2\f$ if and only if the set of constraints that are saturated by \f$\vect{y}_1\f$ is equal to the set of constraints that are saturated by \f$\vect{y}_2\f$. Saturation matrix A saturation matrix is a Boolean matrix that represent the connection between constraints and generators of a polyhedron. There are two kinds of saturation matrix one having rows indexed by constraints and columns indexed by generators (sat_g), and one (that is the transposed version of the previous one) having rows indexed by generators and columns indexed by constraints (sat_c). For instance, in the saturation matrix sat_g, the elements are defined as follows: \f[ s_{ij} = \begin{cases} 0, \text{if the constraint indexed by } i \text{ is saturated by the generator indexed by } j;\\ 1, \text{if the constraint indexed by } i \text{ is only verified by the generator indexed by } j. \end{cases} \f] For efficiency reasons, the PPL uses both the sat_g and sat_c matrices. Saturation rule In an \f$n\f$-dimensional \f$\mathop{\mathrm{ray space}}\f$, -# Every inequality must be saturated by at least \f$n\f$ vertices/rays. -# Every vertex must saturate at least \f$n\f$ inequalities and a ray must saturate at least \f$n - 1\f$ inequalities plus the positivity constraint. -# Every equality must be saturated by all lines and vertices/rays. -# Every line must saturate all equalities and inequalities. These rules are a consequence of the saturation concept. Proposition Let \f$C = \{\vect{x} \mid A\vect{x} \geq \vect{0}\}\f$ be a polyhedral cone. Then the minimal proper face of \f$C\f$ in an \f$n\f$-dimensional space can also be represented as \f$ F = \{\,\vect{x} \mid A\vect{x} = \vect{0}\,\}. \f$ To see this, note that the minimal proper face of a polyhedral cone is equal to its lineality space. This for definition is composed by all \f$\vect{y}\f$ of \f$C\f$ that satisfies \f$A \vect{x} = \vect{0}.\f$ Adjacent rays Let \f$A\f$ be representing matrix of constraints of a cone \f$C\f$ and \f$Q\f$ the set of rays that generate \f$C\f$. Then two rays \f$\vect{r}_1\f$ and \f$\vect{r}_2\f$ are adjacent rays if -# there exist at least one row of \f$A\f$ (i.e., a constraint) that is saturated by both \f$\vect{r}_1\f$ and \f$\vect{r}_2\f$ -# and none of the rays of \f$Q\f$, except \f$\vect{r}_1\f$ and \f$\vect{r}_2\f$, saturates all the constraints saturated by both \f$\vect{r}_1\f$ and \f$\vect{r}_2\f$. Independence rule -# No inequality is a positive combination of any other two inequalities or equalities. -# No ray is a linear combination of any other two rays or lines. -# The set of equalities must be linearly independent. -# The set of lines must be linearly independent. To remove redundant constraints/generators we will use the following characterization: Redundancy rules - An inequality is not redundant if it satisfies both point (1) of the saturation rule and point (1) of the independence rule. - A vertex/ray is irredundant if it satisfies both point (2) of the saturation rule and point (2) of the independence rule. It is useful to note that: - All rays saturate the positivity constraint and no vertex saturates the positivity constraint; in fact in the homogeneous form the positivity constraint is represented by the vector \f$\vect{a}^\transpose = (0, \ldots, 0, 1)\f$, rays are of the form \f$\vect{r} = (r_0, \ldots, r_{n-1}, 0)^\transpose\f$ and vertices \f$\vect{v} = (v_0, \ldots, v_{n-1}, d)^\transpose\f$ with \f$d \neq 0\f$, thus \f$\langle \vect{a}, \vect{r} \rangle = 0\f$ for each ray \f$\vect{r}\f$ and \f$\langle \vect{a}, \vect{v} \rangle \neq 0\f$ for each vertex \f$\vect{v}\f$. - The positivity constraint will be irredundant if and only if the size of the set of rays is \f$\geq n\f$, where \f$n\f$ is the dimension of the ray space, and the rank of the ray set is \f$n\f$; in fact a constraint is irredundant if it is saturated by at least \f$n\f$ vertices/rays (see above), but since only rays saturate the positivity constraint, then in a system with \f$n\f$ vertices/rays the positivity constraint is irredundant. \endif */