<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>PPL: General Information on the PPL</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.6.3 -->
<div class="navigation" id="top">
<div class="tabs">
<ul>
<li class="current"><a href="main.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
</ul>
</div>
</div>
<div class="contents">
<h1>General Information on the PPL </h1><h3 class="version">0.11.2 </h3><h2><a class="anchor" id="preamble">
The Main Features</a></h2>
<p>The Parma Polyhedra Library (PPL) is a modern C++ library for the manipulation of numerical information that can be represented by points in some <img class="formulaInl" alt="$n$" src="form_0.png"/>-dimensional vector space. For instance, one of the key domains the PPL supports is that of rational convex polyhedra (Section <a class="el" href="main.html#convex_polys">Convex Polyhedra</a>). 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.</p>
<p>The main features of the library are the following:</p>
<ul>
<li>it is user friendly: you write <code>x + 2*y + 5*z <= 7</code> when you mean it;</li>
<li>it is fully dynamic: available virtual memory is the only limitation to the dimension of anything;</li>
<li>it provides full support for the manipulation of convex polyhedra that are not topologically closed;</li>
<li>it is written in standard C++: meant to be portable;</li>
<li>it is exception-safe: never leaks resources or leaves invalid object fragments around;</li>
<li>it is rather efficient: and we hope to make it even more so;</li>
<li>it is thoroughly documented: perhaps not literate programming but close enough;</li>
<li>it has interfaces to other programming languages: including C, Java, OCaml and a number of Prolog systems;</li>
<li>it is free software: distributed under the terms of the GNU General Public License.</li>
</ul>
<p>In the following section we describe all the domains available to the PPL user. More detailed descriptions of these domains and the operations provided will be found in subsequent sections.</p>
<p>In the final section of this chapter (Section <a class="el" href="main.html#use_of_library">Using the Library</a>), we provide some additional advice on the use of the library.</p>
<h3><a class="anchor" id="Semantic_Geometric_Descriptors">
Semantic Geometric Descriptors</a></h3>
<p>A <em>semantic geometric descriptor</em> is a subset of <img class="formulaInl" alt="$ \Rset^n $" src="form_1.png"/>. The PPL provides several classes of semantic GDs. These are identified by their C++ class name, together with the class template parameters, if any. These classes include the <em>simple classes</em>:</p>
<ul>
<li><a class="el" href="classParma__Polyhedra__Library_1_1C__Polyhedron.html"><code>C_Polyhedron</code> </a>,</li>
<li><a class="el" href="classParma__Polyhedra__Library_1_1NNC__Polyhedron.html"><code>NNC_Polyhedron</code> </a>,</li>
<li><a class="el" href="classParma__Polyhedra__Library_1_1BD__Shape.html"><code>BD_Shape<T></code> </a>,</li>
<li><a class="el" href="classParma__Polyhedra__Library_1_1Octagonal__Shape.html"><code>Octagonal_Shape<T></code> </a>,</li>
<li><a class="el" href="classParma__Polyhedra__Library_1_1Box.html"><code>Box<ITV></code> </a>, and</li>
<li><a class="el" href="classParma__Polyhedra__Library_1_1Grid.html"><code>Grid</code> </a>,</li>
</ul>
<p>where:</p>
<ul>
<li><code>T</code> is a numeric type chosen among <code>mpz_class</code>, <code>mpq_class</code>, <code>signed char</code>, <code>short</code>, <code>int</code>, <code>long</code>, <code>long</code> long (or any of the C99 exact width integer equivalents <code>int8_t</code>, int16_t, and so forth); and</li>
<li><code>ITV</code> is an instance of the <a class="el" href="classParma__Polyhedra__Library_1_1Interval.html"><code>Interval</code> </a> template class.</li>
</ul>
<p>Other semantic GDs, the <em>compound classes</em>, can be constructed (also recursively) from all the GDs classes. These include:</p>
<ul>
<li><a class="el" href="classParma__Polyhedra__Library_1_1Pointset__Powerset.html"><code>Pointset_Powerset<PSET></code> </a>,</li>
<li><a class="el" href="classParma__Polyhedra__Library_1_1Partially__Reduced__Product.html"><code>Partially_Reduced_Product<D1, D2, R></code> </a>,</li>
</ul>
<p>where <code>PSET</code>, <code>D1</code> and <code>D2</code> can be any semantic GD classes and <code>R</code> is the reduction operation to be applied to the component domains of the product class.</p>
<p>A uniform set of operations is provided for creating, testing and maintaining each of the semantic GDs. However, as many of these depend on one or more syntactic GDs, we first describe the syntactic GDs.</p>
<h3><a class="anchor" id="Syntactic_Geometric_Descriptors">
Syntactic Geometric Descriptors</a></h3>
<p>A <em>syntactic geometric descriptor</em> is for defining, modifying and inspecting a semantic GD. There are three kinds of <em>syntactic GDs</em>: <em>basic GDs</em>, <em>constraint GDs</em> and <em>generator GDs</em>. Some of these are <em>generic</em> and some <em>specific</em>. A generic syntactic GD can be used (in the appropriate context) with any semantic GD; clearly, different semantic GDs will usually provide different levels of support for the different subclasses of generic GDs. In contrast, the use of a specific GD may be restricted to apply to a given subset of the semantic GDs (i.e., some semantic GDs provide no support at all for them).</p>
<h4><a class="anchor" id="Basic_Geometric_Descriptors">
Basic Geometric Descriptors</a></h4>
<p>The following basic GDs currently supported by the PPL are:</p>
<ul>
<li>space dimension;</li>
<li>variable and variable set;</li>
<li>coefficient;</li>
<li>linear expression;</li>
<li>relation symbol;</li>
<li>vector point.</li>
</ul>
<p>These classes, which are all generic syntactic GDs, are used to build the constraint and generator GDs as well as support many generic operations on the semantic GDs.</p>
<h4><a class="anchor" id="Constraint_Geometric_Descriptors">
Constraint Geometric Descriptors</a></h4>
<p>The PPL currently supports the following classes of <em>generic</em> constraint GDs:</p>
<ul>
<li>linear constraint;</li>
<li>linear congruence.</li>
</ul>
<p>Each linear constraint can be further classified to belong to one or more of the following syntactic subclasses:</p>
<ul>
<li>inconsistent constraints (e.g., <img class="formulaInl" alt="$0 \geq 2$" src="form_2.png"/>);</li>
<li>tautological constraints (e.g., <img class="formulaInl" alt="$0 \leq 2$" src="form_3.png"/>);</li>
<li>interval constraints (e.g., <img class="formulaInl" alt="$x \leq 2$" src="form_4.png"/>);</li>
<li>bounded-difference constraints (e.g., <img class="formulaInl" alt="$x - y \leq 2$" src="form_5.png"/>);</li>
<li>octagonal constraints (e.g., <img class="formulaInl" alt="$x + y \leq 2$" src="form_6.png"/>);</li>
<li>linear equality constraints (e.g., <img class="formulaInl" alt="$x = 2$" src="form_7.png"/>);</li>
<li>non-strict linear inequality constraints (e.g., <img class="formulaInl" alt="$x - 3y \leq 2$" src="form_8.png"/>);</li>
<li>strict linear inequality constraints (e.g., <img class="formulaInl" alt="$x - 3y < 2$" src="form_9.png"/>).</li>
</ul>
<p>Note that the subclasses are not disjoint.</p>
<p>Similarly, each linear congruence can be classified to belong to one or more of the following syntactic subclasses:</p>
<ul>
<li>inconsistent congruences (e.g., <img class="formulaInl" alt="$0 \equiv_2 1$" src="form_10.png"/>);</li>
<li>tautological congruences (e.g., <img class="formulaInl" alt="$0 \equiv_2 2$" src="form_11.png"/>);</li>
<li>linear equality, i.e., non-proper congruences (e.g., <img class="formulaInl" alt="$x + 3y \equiv_0 0$" src="form_12.png"/>);</li>
<li>proper congruences (e.g., <img class="formulaInl" alt="$x + 3y \equiv_5 0$" src="form_13.png"/>).</li>
</ul>
<p>The library also supports systems, i.e., finite collections, of either linear constraints or linear congruences (but see the note below).</p>
<p>Each semantic GD provides <em>optimal</em> support for some of the subclasses of generic syntactic GDs listed above: here, the word "optimal" means that the considered semantic GD computes the <em>best upward approximation</em> of the exact meaning of the linear constraint or congruence. When a semantic GD operation is applied to a syntactic GD that is not optimally supported, it will either indicate its unsuitability (e.g., by throwing an exception) or it will apply an upward approximation semantics (possibly not the best one).</p>
<p>For instance, the semantic GD of topologically closed convex polyhedra provides optimal support for non-strict linear inequality and equality constraints, but it does not provide optimal support for strict inequalities. Some of its operations (e.g., <code>add_constraint</code> and <code>add_congruence</code>) will throw an exception if supplied with a non-trivial strict inequality constraint or a proper congruence; some other operations (e.g., <code>refine_with_constraint</code> or <code>refine_with_congruence</code>) will compute an over-approximation.</p>
<p>Similarly, the semantic GD of rational boxes (i.e., multi-dimensional intervals) having integral values as interval boundaries provides optimal support for all interval constraints: even though the interval constraint <img class="formulaInl" alt="$2x \leq 5$" src="form_14.png"/> cannot be represented exactly, it will be optimally approximated by the constraint <img class="formulaInl" alt="$x \leq 3$" src="form_15.png"/>.</p>
<dl class="note"><dt><b>Note:</b></dt><dd>When providing an upward approximation for a constraint or congruence, we consider it in isolation: in particular, the approximation of each element of a system of GDs is independent from the other elements; also, the approximation is independent from the current value of the semantic GD.</dd></dl>
<h4><a class="anchor" id="Generator_Geometric_Descriptors">
Generator Geometric Descriptors</a></h4>
<p>The PPL currently supports two classes of generator GDs:</p>
<ul>
<li>polyhedra generator: these are polyhedra points, rays and lines;</li>
<li>grid generator: these are grid points, parameters and lines.</li>
</ul>
<p>Rays, lines and parameters are specific of the mentioned semantic GDs and, therefore, they cannot be used by other semantic GDs. In contrast, as already mentioned above, points are basic geometric descriptors since they are also used in <em>generic</em> PPL operations.</p>
<h3><a class="anchor" id="Generic_Operations_on_Semantic_Geometric_Descriptors">
Generic Operations on Semantic Geometric Descriptors</a></h3>
<ol>
<li>
Constructors of a universe or empty semantic GD with the given space dimension. </li>
<li>
Operations on a semantic GD that do not depend on the syntactic GDs. <ul>
<li>
<p class="startli"><code>is_empty()</code>, <code>is_universe()</code>, <code>is_topologically_closed()</code>, <code>is_discrete()</code>, <code>is_bounded()</code>, <code>contains_integer_point()</code></p>
<p class="endli">test for the named properties of the semantic GD. </p>
</li>
<li>
<p class="startli"><code>total_memory_in_bytes()</code>, <code>external_memory_in_bytes()</code></p>
<p class="endli">return the total and external memory size in bytes. </p>
</li>
<li>
<p class="startli"><code>OK()</code></p>
<p class="endli">checks that the semantic GD has a valid internal representation. (Some GDs provide this method with an optional Boolean argument that, when true, requires to also check for non-emptiness.) </p>
</li>
<li>
<p class="startli"><code>space_dimension()</code>, <code>affine_dimension()</code></p>
<p class="endli">return, respectively, the space and affine dimensions of the GD. </p>
</li>
<li>
<p class="startli"><code>add_space_dimensions_and_embed()</code>, <code>add_space_dimensions_and_project()</code>, <code>expand_space_dimension()</code>, <code>remove_space_dimensions()</code>, <code>fold_space_dimensions()</code>, <code>map_space_dimensions()</code></p>
<p class="endli">modify the space dimensions of the semantic GD; where, depending on the operation, the arguments can include the number of space dimensions to be added or removed a variable or set of variables denoting the actual dimensions to be used and a partial function defining a mapping between the dimensions. </p>
</li>
<li>
<p class="startli"><code>contains()</code>, <code>strictly_contains()</code>, <code>is_disjoint_from()</code></p>
<p class="endli">compare the semantic GD with an argument semantic GD of the same class. </p>
</li>
<li>
<p class="startli"><code>topological_closure_assign()</code>, <code>intersection_assign()</code>, <code>upper_bound_assign()</code>, <code>difference_assign()</code>, <code>time_elapse_assign()</code>, <code>widening_assign()</code>, <code>concatenate_assign()</code>, <code>swap()</code></p>
<p class="endli">modify the semantic GD, possibly with an argument semantic GD of the same class. </p>
</li>
<li>
<p class="startli"><code>constrains()</code>, <code>bounds_from_above()</code>, <code>bounds_from_below()</code>, <code>maximize()</code>, <code>minimize()</code>.</p>
<p class="endli">These find information about the bounds of the semantic GD where the argument variable or linear expression define the direction of the bound. </p>
</li>
<li>
<p class="startli"><code>affine_image()</code>, <code>affine_preimage()</code>, <code>generalized_affine_image()</code>, <code>generalized_affine_preimage()</code>, <code>bounded_affine_image()</code>, <code>bounded_affine_preimage()</code>.</p>
<p class="endli">These perform several variations of the affine image and preimage operations where, depending on the operation, the arguments can include a variable representing the space dimension to which the transformation will be applied and linear expressions with possibly a relation symbol and denominator value that define the exact form of the transformation. </p>
</li>
<li>
<p class="startli"><code>ascii_load()</code>, <code>ascii_dump()</code></p>
<p class="endli">are the ascii input and output operations. </p>
</li>
</ul>
</li>
<li>
Constructors of a semantic GD of one class from a semantic GD of any other class. These constructors obey an <em>upward approximation semantics</em>, meaning that the constructed semantic GD is guaranteed to contain all the points of the source semantic GD, but possibly more. Some of these constructors provide a complexity parameter with which the application can control the complexity/precision trade-off for the construction operation: by using the complexity parameter, it is possible to keep the construction operation in the polynomial or the simplex worst-case complexity class, possibly incurring into a further upward approximation if the precise constructor is based on an algorithm having exponential complexity. </li>
<li>
Constructors of a semantic GD from a constraint GD; either a linear constraint system or a linear congruence system. These constructors assume that the given semantic GD provides optimal support for the argument syntactic GD: if that is not the case, an invalid argument exception is thrown. </li>
<li>
Other interaction between the semantic GDs and constraint GDs. <ul>
<li>
<p class="startli"><code>add_constraint()</code>, <code>add_constraints()</code>, <code>add_recycled_constraints()</code>, <code>add_congruence()</code>, <code>add_congruences()</code>, <code>add_recycled_congruences()</code>.</p>
<p>These methods assume that the given semantic GD provides optimal support for the argument syntactic GD: if that is not the case, an invalid argument exception is thrown.</p>
<p class="endli">For <code>add_recycled_constraints()</code> and <code>add_recycled_congruences()</code>, the only assumption that can be made on the constraint GD after return (successful or exceptional) is that it can be safely destroyed. </p>
</li>
<li>
<p class="startli"><code>refine_with_constraint()</code>, <code>refine_with_constraints()</code>, <code>refine_with_congruence()</code>, <code>refine_with_congruences()</code>.</p>
<p class="endli">If the argument constraint GD is optimally supported by the semantic GD, the methods behave the same as the corresponding <code>add_*</code> methods listed above. Otherwise the constraint GD is used only to a limited extent to refine the semantic GD; possibly not at all. Notice that, while repeating an add operation is pointless, this is not true for the refine operations. For example, in those cases where </p>
<div class="fragment"><pre class="fragment"> Semantic_GD.add_constraint(c)
</pre></div><p> raises an exception, a fragment of the form </p>
<div class="fragment"><pre class="fragment"> Semantic_GD.refine_with_constraint(c)
<span class="comment">// Other add_constraint(s) or refine_with_constraint(s) operations</span>
<span class="comment">// on Semantic_GD.</span>
Semantic_GD.refine_with_constraint(c)
</pre></div><p> may give more precise results than a single </p>
<div class="fragment"><pre class="fragment"> Semantic_GD.refine_with_constraint(c).
<span class="comment">// Other add_constraint(s) or refine_with_constraint(s) operations</span>
<span class="comment">// on Semantic_GD.</span>
</pre></div> </li>
<li>
<p class="startli"><code>constraints()</code>, <code>minimized_constraints()</code>, <code>congruences()</code>, <code>minimized_congruences()</code>.</p>
<p class="endli">Returns the indicated system of constraint GDs satisfied by the semantic GD. </p>
</li>
<li>
<p class="startli"><code>can_recycle_constraint_systems()</code>, <code>can_recycle_congruence_systems()</code>.</p>
<p class="endli">Return true if and only if the semantic GD can recycle the indicated constraint GD. </p>
</li>
<li>
<p class="startli"><code>relation_with()</code>.</p>
<p class="endli">This takes a constraint GD as an argument and returns the relations holding between the semantic GD and the constraint GD. The possible relations are: <code>IS_INCLUDED()</code>, <code>SATURATES()</code>, <code>STRICTLY_INTERSECTS()</code>, <code>IS_DISJOINT()</code> and <code>NOTHING()</code>. This operator also can take a polyhedron generator GD as an argument and returns the relation <code>SUBSUMES()</code> or <code>NOTHING()</code> that holds between the generator GD and the semantic GD. </p>
</li>
</ul>
</li>
</ol>
<h2><a class="anchor" id="Upward_Approximation">
Upward Approximation</a></h2>
<p>The Parma Polyhedra Library, for those cases where an exact result cannot be computed within the specified complexity limits, computes an <em>upward approximation</em> of the exact result. For semantic GDs this means that the computed result is a possibly strict superset of the set of points of <img class="formulaInl" alt="$ \Rset^n $" src="form_1.png"/> that constitutes the exact result. Notice that the PPL does not provide direct support to compute <em>downward approximations</em> (i.e., possibly strict subsets of the exact results). While downward approximations can often be computed from upward ones, the required algorithms and the conditions upon which they are correct are outside the current scope of the PPL. Beware, in particular, of the following possible pitfall: the library provides methods to compute upward approximations of set-theoretic difference, which is antitone in its second argument. Applying a difference method to a second argument that is not an exact representation or a downward approximation of reality, would yield a result that, of course, is not an upward approximation of reality. It is the responsibility of the library user to provide the PPL's method with approximations of reality that are consistent with respect to the desired results.</p>
<h2><a class="anchor" id="Approximating_Integers">
Approximating Integers</a></h2>
<p>The Parma Polyhedra Library provides support for approximating integer computations using the geometric descriptors it provides. In this section we briefly explain these facilities.</p>
<h3><a class="anchor" id="Dropping_Non_Integer_Points">
Dropping Non-Integer Points</a></h3>
<p>When a geometric descriptor is used to approximate integer quantities, all the points with non-integral coordinates represent an imprecision of the description. Of course, removing all these points may be impossible (because of convexity) or too expensive. The PPL provides the operator <code>drop_some_non_integer_points</code> to possibly tighten a descriptor by dropping some points with non-integer coordinates, using algorithms whose complexity is bounded by a parameter. The set of dimensions that represent integer quantities can be optionally specified. It is worth to stress the role of <em>some</em> in the operator name: in general no optimality guarantee is provided.</p>
<h3><a class="anchor" id="Approximating_Bounded_Integers">
Approximating Bounded Integers</a></h3>
<p>The Parma Polyhedra Library provides services that allow to compute correct approximations of bounded arithmetic as available in widespread programming languages. Supported bit-widths are 8, 16, 32 and 64 bits, with some limited support for 128 bits. Supported representations are binary unsigned and two's complement signed. Supported overflow behaviors are: </p>
<dl>
<dt>Wrapping: </dt>
<dd>this means that, for a <img class="formulaInl" alt="$w\textrm{-bit}$" src="form_16.png"/> bounded integer, the computation happens modulo <img class="formulaInl" alt="$2^w$" src="form_17.png"/>. In turn, this signifies that the computation happens <em>as if</em> the unbounded arithmetic result was computed and then wrapped. For unsigned integers, the wrapping function is simply <img class="formulaInl" alt="$x \bmod 2^w$" src="form_18.png"/>, most conveniently defined as <p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathrm{wrap}^\mathrm{u}_w(x) \defeq x - 2^w \lfloor x/2^w \rfloor. \]" src="form_19.png"/>
</p>
For signed integers the wrapping function is, instead, <p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathrm{wrap}^\mathrm{s}_w(x) \defeq \begin{cases} \mathrm{wrap}^\mathrm{u}_w(x), &\text{if $\mathrm{wrap}^\mathrm{u}_w(x) < 2^{w-1}$;} \\ \mathrm{wrap}^\mathrm{u}_w(x) - 2^w, &\text{otherwise.} \end{cases} \]" src="form_20.png"/>
</p>
</dd>
<dt>Undefined: </dt>
<dd>this means that the result of the operation resulting in an overflow can take any value. This is useful to partially model systems where overflow has unspecified effects on the computed result. Even though something more serious can happen in the system being analyzed ---due to, e.g., C's undefined behavior---, here we are only concerned with the results of arithmetic operations. It is the responsibility of the analyzer to ensure that other manifestations of undefined behavior are conservatively approximated. </dd>
<dt>Impossible: </dt>
<dd>this is for the analysis of languages where overflow is trapped before it affects the state, for which, thus, any indication that an overflow may have affected the state is necessarily due to the imprecision of the analysis. </dd>
</dl>
<h4><a class="anchor" id="Wrapping_Operator">
Wrapping Operator</a></h4>
<p>One possibility for precisely approximating the semantics of programs that operate on bounded integer variables is to follow the approach described in <a class="el" href="main.html#SK07">[SK07]</a>. The idea is to associate space dimensions to the <em>unwrapped values</em> of bounded variables. Suppose <code>j</code> is a <img class="formulaInl" alt="$w\textrm{-bit}$" src="form_16.png"/>, unsigned program variable associated to a space dimension labeled by the variable <img class="formulaInl" alt="$x$" src="form_21.png"/>. If <img class="formulaInl" alt="$x$" src="form_21.png"/> is constrained by some numerical abstraction to take values in a set <img class="formulaInl" alt="$S \sseq \Rset$" src="form_22.png"/>, then the program variable <code>j</code> can only take values in <img class="formulaInl" alt="$\bigl\{\, \mathrm{wrap}^\mathrm{u}_w(z) \bigm| z \in S \,\bigr\}$" src="form_23.png"/>. There are two reasons why this is interesting: firstly, this allows for the retention of relational information by using a single numerical abstraction tracking multiple program variables. Secondly, the integers modulo <img class="formulaInl" alt="$2^w$" src="form_17.png"/> form a ring of equivalence classes on which addition and multiplication are well defined. This means, e.g., that assignments with affine right-hand sides and involving only variables with the same bit-width and representation can be safely modeled by affine images. While upper bounds and widening can be used without any precaution, anything that can be reconducted to intersection requires a preliminary <em>wrapping</em> phase, where the dimensions corresponding to bounded integer types are brought back to their natural domain. This necessity arises naturally for the analysis of conditionals and conversion operators, as well as in the realization of domain combinations.</p>
<p>The PPL provides a general wrapping operator that is parametric with respect to the set of space dimensions (variables) to be wrapped, the width, representation and overflow behavior of all these variables. An optional constraint system can, when given, improve the precision. This constraint system, which must only depend on variables with respect to which wrapping is performed, is assumed to represent the conditional or looping construct guard with respect to which wrapping is performed. Since wrapping requires the computation of upper bounds and due to non-distributivity of constraint refinement over upper bounds, passing a constraint system in this way can be more precise than refining the result of the wrapping operation afterwards. The general wrapping operator offered by the PPL also allows control of the complexity/precision ratio by means of two additional parameters: an unsigned integer encoding a complexity threshold, with higher values resulting in possibly improved precision; and a Boolean controlling whether space dimensions should be wrapped individually, something that results in much greater efficiency to the detriment of precision, or collectively.</p>
<p>Note that the PPL assumes that any space dimension subject to wrapping is being used to capture the value of bounded integer values. As a consequence the library is free to drop, from the involved numerical abstraction, any point having a non-integer coordinate that corresponds to a space dimension subject to wrapping. It must be stressed that freedom to drop such points does not constitute an obligation to remove all of them (especially because this would be extraordinarily expensive on some numerical abstractions). The PPL provides operators for the more systematic <a class="el" href="main.html#Dropping_Non_Integer_Points">removal of points with non-integral coordinates</a>.</p>
<p>The wrapping operator will only remove some of these points as a by-product of its main task and only when this comes at a negligible extra cost.</p>
<h2><a class="anchor" id="convex_polys">
Convex Polyhedra</a></h2>
<p>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 <a class="el" href="main.html#BRZH02b">[BRZH02b]</a>, <a class="el" href="main.html#Fuk98">[Fuk98]</a>, <a class="el" href="main.html#NW88">[NW88]</a>, and <a class="el" href="main.html#Wil93">[Wil93]</a>.</p>
<h3><a class="anchor" id="Vectors_Matrices_and_Scalar_Products">
Vectors, Matrices and Scalar Products</a></h3>
<p>We denote by <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> the <img class="formulaInl" alt="$n\textrm{-dimensional}$" src="form_25.png"/> vector space on the field of real numbers <img class="formulaInl" alt="$\Rset$" src="form_26.png"/>, endowed with the standard topology. The set of all non-negative reals is denoted by <img class="formulaInl" alt="$\nonnegRset$" src="form_27.png"/>. For each <img class="formulaInl" alt="$i \in \{0, \ldots, n-1\}$" src="form_28.png"/>, <img class="formulaInl" alt="$v_i$" src="form_29.png"/> denotes the <img class="formulaInl" alt="$i\textrm{-th}$" src="form_30.png"/> component of the (column) vector <img class="formulaInl" alt="$\vect{v} = (v_0, \ldots, v_{n-1})^\transpose \in \Rset^n$" src="form_31.png"/>. We denote by <img class="formulaInl" alt="$\vect{0}$" src="form_32.png"/> the vector of <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/>, called <em>the origin</em>, having all components equal to zero. A vector <img class="formulaInl" alt="$\vect{v} \in \Rset^n$" src="form_33.png"/> can be also interpreted as a matrix in <img class="formulaInl" alt="$\Rset^{n \times 1}$" src="form_34.png"/> and manipulated accordingly using the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, denoted by <img class="formulaInl" alt="$\vect{v}^\transpose$" src="form_35.png"/>.</p>
<p>The <em>scalar product</em> of <img class="formulaInl" alt="$\vect{v},\vect{w} \in \Rset^n$" src="form_36.png"/>, denoted <img class="formulaInl" alt="$\langle \vect{v}, \vect{w} \rangle$" src="form_37.png"/>, is the real number </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \vect{v}^\transpose \vect{w} = \sum_{i=0}^{n-1} v_i w_i. \]" src="form_38.png"/>
</p>
<p>For any <img class="formulaInl" alt="$S_1, S_2 \sseq \Rset^n$" src="form_39.png"/>, the <em>Minkowski's sum</em> of <img class="formulaInl" alt="$S_1$" src="form_40.png"/> and <img class="formulaInl" alt="$S_2$" src="form_41.png"/> is: <img class="formulaInl" alt="$S_1 + S_2 = \{\, \vect{v}_1 + \vect{v}_2 \mid \vect{v}_1 \in S_1, \vect{v}_2 \in S_2 \,\}.$" src="form_42.png"/></p>
<h3><a class="anchor" id="Affine_Hyperplanes_and_Half_spaces">
Affine Hyperplanes and Half-spaces</a></h3>
<p>For each vector <img class="formulaInl" alt="$\vect{a} \in \Rset^n$" src="form_43.png"/> and scalar <img class="formulaInl" alt="$b \in \Rset$" src="form_44.png"/>, where <img class="formulaInl" alt="$\vect{a} \neq \vect{0}$" src="form_45.png"/>, and for each relation symbol <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq, > \}$" src="form_46.png"/>, the linear constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \relsym b$" src="form_47.png"/> defines:</p>
<ul>
<li>an affine hyperplane if it is an equality constraint, i.e., if <img class="formulaInl" alt="$\mathord{\relsym} \in \{ = \}$" src="form_48.png"/>;</li>
<li>a topologically closed affine half-space if it is a non-strict inequality constraint, i.e., if <img class="formulaInl" alt="$\mathord{\relsym} \in \{ \geq \}$" src="form_49.png"/>;</li>
<li>a topologically open affine half-space if it is a strict inequality constraint, i.e., if <img class="formulaInl" alt="$\mathord{\relsym} \in \{ > \}$" src="form_50.png"/>.</li>
</ul>
<p>Note that each hyperplane <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle = b$" src="form_51.png"/> can be defined as the intersection of the two closed affine half-spaces <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \geq b$" src="form_52.png"/> and <img class="formulaInl" alt="$\langle -\vect{a}, \vect{x} \rangle \geq -b$" src="form_53.png"/>. Also note that, when <img class="formulaInl" alt="$\vect{a} = \vect{0}$" src="form_54.png"/>, the constraint <img class="formulaInl" alt="$\langle \vect{0}, \vect{x} \rangle \relsym b$" src="form_55.png"/> is either a tautology (i.e., always true) or inconsistent (i.e., always false), so that it defines either the whole vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> or the empty set <img class="formulaInl" alt="$\emptyset$" src="form_56.png"/>.</p>
<h3><a class="anchor" id="Convex_Polyhedra">
Convex Polyhedra</a></h3>
<p>The set <img class="formulaInl" alt="$\cP \sseq \Rset^n$" src="form_57.png"/> is a <em>not necessarily closed convex polyhedron</em> (<em>NNC polyhedron</em>, for short) if and only if either <img class="formulaInl" alt="$\cP$" src="form_58.png"/> can be expressed as the intersection of a finite number of (open or closed) affine half-spaces of <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> or <img class="formulaInl" alt="$n = 0$" src="form_59.png"/> and <img class="formulaInl" alt="$\cP = \emptyset$" src="form_60.png"/>. The set of all NNC polyhedra on the vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> is denoted <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/>.</p>
<p>The set <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is a <em>closed convex polyhedron</em> (<em>closed polyhedron</em>, for short) if and only if either <img class="formulaInl" alt="$\cP$" src="form_58.png"/> can be expressed as the intersection of a finite number of closed affine half-spaces of <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> or <img class="formulaInl" alt="$n = 0$" src="form_59.png"/> and <img class="formulaInl" alt="$\cP = \emptyset$" src="form_60.png"/>. The set of all closed polyhedra on the vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> is denoted <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/>.</p>
<p>When ordering NNC polyhedra by the set inclusion relation, the empty set <img class="formulaInl" alt="$\emptyset$" src="form_56.png"/> and the vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> are, respectively, the smallest and the biggest elements of both <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/> and <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/>. The vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> is also called the <em>universe</em> polyhedron.</p>
<p>In theoretical terms, <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/> is a <em>lattice</em> under set inclusion and <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/> is a <em>sub-lattice</em> of <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/>.</p>
<dl class="note"><dt><b>Note:</b></dt><dd>In the following, we will usually specify operators on the domain <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/> of NNC polyhedra. Unless an explicit distinction is made, these operators are provided with the same specification when applied to the domain <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/> of topologically closed polyhedra. The implementation maintains a clearer separation between the two domains of polyhedra (see <a class="el" href="main.html#Topologies_and_Topological_compatibility">Topologies and Topological-compatibility</a>): while computing polyhedra in <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/> may provide more precise results, polyhedra in <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/> can be represented and manipulated more efficiently. As a rule of thumb, if your application will only manipulate polyhedra that are topologically closed, then it should use the simpler domain <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/>. Using NNC polyhedra is only recommended if you are going to actually benefit from the increased accuracy.</dd></dl>
<h3><a class="anchor" id="Bounded_Polyhedra">
Bounded Polyhedra</a></h3>
<p>An NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is <em>bounded</em> if there exists a <img class="formulaInl" alt="$\lambda \in \nonnegRset$" src="form_64.png"/> such that: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cP \sseq \bigl\{\, \vect{x} \in \Rset^n \bigm| - \lambda \leq x_j \leq \lambda \text{ for } j = 0, \ldots, n-1 \,\bigr\}. \]" src="form_65.png"/>
</p>
<p> A bounded polyhedron is also called a <em>polytope</em>.</p>
<h2><a class="anchor" id="representation">
Representations of Convex Polyhedra</a></h2>
<p>NNC polyhedra can be specified by using two possible representations, the constraints (or implicit) representation and the generators (or parametric) representation.</p>
<h3><a class="anchor" id="Constraints_Representation">
Constraints Representation</a></h3>
<p>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 <em>constraint</em>.</p>
<p>By definition, each polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is the set of solutions to a <em>constraint system</em>, i.e., a finite number of constraints. By using matrix notation, we have </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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 \,\}, \]" src="form_66.png"/>
</p>
<p> where, for all <img class="formulaInl" alt="$i \in \{1, 2, 3\}$" src="form_67.png"/>, <img class="formulaInl" alt="$A_i \in \Rset^{m_i} \times \Rset^n$" src="form_68.png"/> and <img class="formulaInl" alt="$\vect{b}_i \in \Rset^{m_i}$" src="form_69.png"/>, and <img class="formulaInl" alt="$m_1, m_2, m_3 \in \Nset$" src="form_70.png"/> are the number of equalities, the number of non-strict inequalities, and the number of strict inequalities, respectively.</p>
<h3><a class="anchor" id="Combinations_and_Hulls">
Combinations and Hulls</a></h3>
<p>Let <img class="formulaInl" alt="$S = \{ \vect{x}_1, \ldots, \vect{x}_k \} \sseq \Rset^n$" src="form_71.png"/> be a finite set of vectors. For all scalars <img class="formulaInl" alt="$\lambda_1, \ldots, \lambda_k \in \Rset$" src="form_72.png"/>, the vector <img class="formulaInl" alt="$\vect{v} = \sum_{j=1}^k \lambda_j \vect{x}_j$" src="form_73.png"/> is said to be a <em>linear</em> combination of the vectors in <img class="formulaInl" alt="$S$" src="form_74.png"/>. Such a combination is said to be</p>
<ul>
<li>a <em>positive</em> (or <em>conic</em>) combination, if <img class="formulaInl" alt="$\forall j \in \{ 1, \ldots, k \} \itc \lambda_j \in \nonnegRset$" src="form_75.png"/>;</li>
<li>an <em>affine</em> combination, if <img class="formulaInl" alt="$\sum_{j = 1}^k \lambda_j = 1$" src="form_76.png"/>;</li>
<li>a <em>convex</em> combination, if it is both positive and affine.</li>
</ul>
<p>We denote by <img class="formulaInl" alt="$\linearhull(S)$" src="form_77.png"/> (resp., <img class="formulaInl" alt="$\conichull(S)$" src="form_78.png"/>, <img class="formulaInl" alt="$\affinehull(S)$" src="form_79.png"/>, <img class="formulaInl" alt="$\convexhull(S)$" src="form_80.png"/>) the set of all the linear (resp., positive, affine, convex) combinations of the vectors in <img class="formulaInl" alt="$S$" src="form_74.png"/>.</p>
<p>Let <img class="formulaInl" alt="$P, C \sseq \Rset^n$" src="form_81.png"/>, where <img class="formulaInl" alt="$P \union C = S$" src="form_82.png"/>. We denote by <img class="formulaInl" alt="$\NNChull(P, C)$" src="form_83.png"/> the set of all convex combinations of the vectors in <img class="formulaInl" alt="$S$" src="form_74.png"/> such that <img class="formulaInl" alt="$\lambda_j > 0$" src="form_84.png"/> for some <img class="formulaInl" alt="$\vect{x}_j \in P$" src="form_85.png"/> (informally, we say that there exists a vector of <img class="formulaInl" alt="$P$" src="form_86.png"/> that plays an active role in the convex combination). Note that <img class="formulaInl" alt="$\NNChull(P, C) = \NNChull(P, P \union C)$" src="form_87.png"/> so that, if <img class="formulaInl" alt="$C \sseq P$" src="form_88.png"/>, </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \convexhull(P) = \NNChull(P, \emptyset) = \NNChull(P, P) = \NNChull(P, C). \]" src="form_89.png"/>
</p>
<p> It can be observed that <img class="formulaInl" alt="$\linearhull(S)$" src="form_77.png"/> is an affine space, <img class="formulaInl" alt="$\conichull(S)$" src="form_78.png"/> is a topologically closed convex cone, <img class="formulaInl" alt="$\convexhull(S)$" src="form_80.png"/> is a topologically closed polytope, and <img class="formulaInl" alt="$\NNChull(P, C)$" src="form_83.png"/> is an NNC polytope.</p>
<h3><a class="anchor" id="Points_Closure_Points_Rays_and_Lines">
Points, Closure Points, Rays and Lines</a></h3>
<p>Let <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> be an NNC polyhedron. Then</p>
<ul>
<li>a vector <img class="formulaInl" alt="$\vect{p} \in \cP$" src="form_90.png"/> is called a <em>point</em> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>;</li>
<li>a vector <img class="formulaInl" alt="$\vect{c} \in \Rset^n$" src="form_91.png"/> is called a <em>closure point</em> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> if it is a point of the topological closure of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>;</li>
<li>a vector <img class="formulaInl" alt="$\vect{r} \in \Rset^n$" src="form_92.png"/>, where <img class="formulaInl" alt="$\vect{r} \neq \vect{0}$" src="form_93.png"/>, is called a <em>ray</em> (or direction of infinity) of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> if <img class="formulaInl" alt="$\cP \neq \emptyset$" src="form_94.png"/> and <img class="formulaInl" alt="$\vect{p} + \lambda \vect{r} \in \cP$" src="form_95.png"/>, for all points <img class="formulaInl" alt="$\vect{p} \in \cP$" src="form_90.png"/> and all <img class="formulaInl" alt="$\lambda \in \nonnegRset$" src="form_64.png"/>;</li>
<li>a vector <img class="formulaInl" alt="$\vect{l} \in \Rset^n$" src="form_96.png"/> is called a <em>line</em> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> if both <img class="formulaInl" alt="$\vect{l}$" src="form_97.png"/> and <img class="formulaInl" alt="$-\vect{l}$" src="form_98.png"/> are rays of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>.</li>
</ul>
<p>A point of an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is a <em>vertex</em> if and only if it cannot be expressed as a convex combination of any other pair of distinct points in <img class="formulaInl" alt="$\cP$" src="form_58.png"/>. A ray <img class="formulaInl" alt="$\vect{r}$" src="form_99.png"/> of a polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is an <em>extreme ray</em> if and only if it cannot be expressed as a positive combination of any other pair <img class="formulaInl" alt="$\vect{r}_1$" src="form_100.png"/> and <img class="formulaInl" alt="$\vect{r}_2$" src="form_101.png"/> of rays of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>, where <img class="formulaInl" alt="$\vect{r} \neq \lambda \vect{r}_1$" src="form_102.png"/>, <img class="formulaInl" alt="$\vect{r} \neq \lambda \vect{r}_2$" src="form_103.png"/> and <img class="formulaInl" alt="$\vect{r}_1 \neq \lambda \vect{r}_2$" src="form_104.png"/> for all <img class="formulaInl" alt="$\lambda \in \nonnegRset$" src="form_64.png"/> (i.e., rays differing by a positive scalar factor are considered to be the same ray).</p>
<h3><a class="anchor" id="Generators_Representation">
Generators Representation</a></h3>
<p>Each NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> can be represented by finite sets of lines <img class="formulaInl" alt="$L$" src="form_105.png"/>, rays <img class="formulaInl" alt="$R$" src="form_106.png"/>, points <img class="formulaInl" alt="$P$" src="form_86.png"/> and closure points <img class="formulaInl" alt="$C$" src="form_107.png"/> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>. The 4-tuple <img class="formulaInl" alt="$\cG = (L, R, P, C)$" src="form_108.png"/> is said to be a <em>generator system</em> for <img class="formulaInl" alt="$\cP$" src="form_58.png"/>, in the sense that </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cP = \linearhull(L) + \conichull(R) + \NNChull(P, C), \]" src="form_109.png"/>
</p>
<p> where the symbol '<img class="formulaInl" alt="$+$" src="form_110.png"/>' denotes the Minkowski's sum.</p>
<p>When <img class="formulaInl" alt="$\cP \in \CPset_n$" src="form_111.png"/> is a closed polyhedron, then it can be represented by finite sets of lines <img class="formulaInl" alt="$L$" src="form_105.png"/>, rays <img class="formulaInl" alt="$R$" src="form_106.png"/> and points <img class="formulaInl" alt="$P$" src="form_86.png"/> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>. In this case, the 3-tuple <img class="formulaInl" alt="$\cG = (L, R, P)$" src="form_112.png"/> is said to be a <em>generator system</em> for <img class="formulaInl" alt="$\cP$" src="form_58.png"/> since we have </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cP = \linearhull(L) + \conichull(R) + \convexhull(P). \]" src="form_113.png"/>
</p>
<p> Thus, in this case, every closure point of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is a point of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>.</p>
<p>For any <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> and generator system <img class="formulaInl" alt="$\cG = (L, R, P, C)$" src="form_108.png"/> for <img class="formulaInl" alt="$\cP$" src="form_58.png"/>, we have <img class="formulaInl" alt="$\cP = \emptyset$" src="form_60.png"/> if and only if <img class="formulaInl" alt="$P = \emptyset$" src="form_114.png"/>. Also <img class="formulaInl" alt="$P$" src="form_86.png"/> must contain all the vertices of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> although <img class="formulaInl" alt="$\cP$" src="form_58.png"/> can be non-empty and have no vertices. In this case, as <img class="formulaInl" alt="$P$" src="form_86.png"/> is necessarily non-empty, it must contain points of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> that are <em>not</em> vertices. For instance, the half-space of <img class="formulaInl" alt="$\Rset^2$" src="form_115.png"/> corresponding to the single constraint <img class="formulaInl" alt="$y \geq 0$" src="form_116.png"/> can be represented by the generator system <img class="formulaInl" alt="$\cG = (L, R, P, C)$" src="form_108.png"/> such that <img class="formulaInl" alt="$L = \bigl\{ (1, 0)^\transpose \bigr\}$" src="form_117.png"/>, <img class="formulaInl" alt="$R = \bigl\{ (0, 1)^\transpose \bigr\}$" src="form_118.png"/>, <img class="formulaInl" alt="$P = \bigl\{ (0, 0)^\transpose \bigr\}$" src="form_119.png"/>, and <img class="formulaInl" alt="$C = \emptyset$" src="form_120.png"/>. It is also worth noting that the only ray in <img class="formulaInl" alt="$R$" src="form_106.png"/> is <em>not</em> an extreme ray of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>.</p>
<h3><a class="anchor" id="Minimized_Representations">
Minimized Representations</a></h3>
<p>A constraints system <img class="formulaInl" alt="$\cC$" src="form_121.png"/> for an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is said to be <em>minimized</em> if no proper subset of <img class="formulaInl" alt="$\cC$" src="form_121.png"/> is a constraint system for <img class="formulaInl" alt="$\cP$" src="form_58.png"/>.</p>
<p>Similarly, a generator system <img class="formulaInl" alt="$\cG = (L, R, P, C)$" src="form_108.png"/> for an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is said to be <em>minimized</em> if there does not exist a generator system <img class="formulaInl" alt="$\cG' = (L', R', P', C') \neq \cG$" src="form_122.png"/> for <img class="formulaInl" alt="$\cP$" src="form_58.png"/> such that <img class="formulaInl" alt="$L' \sseq L$" src="form_123.png"/>, <img class="formulaInl" alt="$R' \sseq R$" src="form_124.png"/>, <img class="formulaInl" alt="$P' \sseq P$" src="form_125.png"/> and <img class="formulaInl" alt="$C' \sseq C$" src="form_126.png"/>.</p>
<h3><a class="anchor" id="Double_Description">
Double Description</a></h3>
<p>Any NNC polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> can be described by using a constraint system <img class="formulaInl" alt="$\cC$" src="form_121.png"/>, a generator system <img class="formulaInl" alt="$\cG$" src="form_127.png"/>, or both by means of the <em>double description pair (DD pair)</em> <img class="formulaInl" alt="$(\cC, \cG)$" src="form_128.png"/>. The <em>double description method</em> 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.</p>
<p>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.</p>
<h3><a class="anchor" id="Topologies_and_Topological_compatibility">
Topologies and Topological-compatibility</a></h3>
<p>As indicated above, when an NNC polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is necessarily closed, we can ignore the closure points contained in its generator system <img class="formulaInl" alt="$\cG = (L, R, P, C)$" src="form_108.png"/> (as every closure point is also a point) and represent <img class="formulaInl" alt="$\cP$" src="form_58.png"/> by the triple <img class="formulaInl" alt="$(L, R, P)$" src="form_129.png"/>. Similarly, <img class="formulaInl" alt="$\cP$" src="form_58.png"/> 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, <em>NNC</em> and <em>C</em>. We shall abuse terminology by referring to the topological kind of a polyhedron as its <em>topology</em>.</p>
<p>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.</p>
<p>Unless it is otherwise stated, all the polyhedra, constraints and/or generators in any library operation must obey the following <em>topological-compatibility</em> rules:</p>
<ul>
<li>polyhedra are topologically-compatible if and only if they have the same topology;</li>
<li>all constraints except for strict inequality constraints and all generators except for closure points are topologically-compatible with both C and NNC polyhedra;</li>
<li>strict inequality constraints and closure points are topologically-compatible with a polyhedron if and only if it is NNC.</li>
</ul>
<p>Wherever possible, the library provides methods that, starting from a polyhedron of a given topology, build the corresponding polyhedron having the other topology.</p>
<h3><a class="anchor" id="Space_Dimensions_and_Dimension_Compatibility">
Space Dimensions and Dimension Compatibility</a></h3>
<p>The <em>space dimension</em> of an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> (resp., a C polyhedron <img class="formulaInl" alt="$\cP \in \CPset_n$" src="form_111.png"/>) is the dimension <img class="formulaInl" alt="$n \in \Nset$" src="form_130.png"/> of the corresponding vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/>. The space dimension of constraints, generators and other objects of the library is defined similarly.</p>
<p>Unless it is otherwise stated, all the polyhedra, constraints and/or generators in any library operation must obey the following (space) <em>dimension-compatibility</em> rules:</p>
<ul>
<li>polyhedra are dimension-compatible if and only if they have the same space dimension;</li>
<li>the constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \relsym b$" src="form_47.png"/> where <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq, > \}$" src="form_46.png"/> and <img class="formulaInl" alt="$\vect{a}, \vect{x} \in \Rset^m$" src="form_131.png"/>, is dimension-compatible with a polyhedron having space dimension <img class="formulaInl" alt="$n$" src="form_0.png"/> if and only if <img class="formulaInl" alt="$m \leq n$" src="form_132.png"/>;</li>
<li>the generator <img class="formulaInl" alt="$\vect{x} \in \Rset^m$" src="form_133.png"/> is dimension-compatible with a polyhedron having space dimension <img class="formulaInl" alt="$n$" src="form_0.png"/> if and only if <img class="formulaInl" alt="$m \leq n$" src="form_132.png"/>;</li>
<li>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.</li>
</ul>
<p>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.</p>
<h3><a class="anchor" id="Affine_Independence_and_Affine_Dimension">
Affine Independence and Affine Dimension</a></h3>
<p>A finite set of points <img class="formulaInl" alt="$\{ \vect{x}_1, \ldots, \vect{x}_k \} \sseq \Rset^n$" src="form_134.png"/> is <em>affinely independent</em> if, for all <img class="formulaInl" alt="$\lambda_1, \ldots, \lambda_k \in \Rset$" src="form_72.png"/>, the system of equations </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \sum_{i = 1}^k \lambda_i \vect{x}_i = \vect{0}, \quad \sum_{i = 1}^k \lambda_i = 0 \]" src="form_135.png"/>
</p>
<p> implies that, for each <img class="formulaInl" alt="$i = 1, \ldots, k$" src="form_136.png"/>, <img class="formulaInl" alt="$\lambda_i = 0$" src="form_137.png"/>.</p>
<p>The maximum number of affinely independent points in <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> is <img class="formulaInl" alt="$n + 1$" src="form_138.png"/>.</p>
<p>A <em>non-empty</em> NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> has <em>affine dimension</em> <img class="formulaInl" alt="$k \in \Nset$" src="form_139.png"/>, denoted by <img class="formulaInl" alt="$\pdim(\cP) = k$" src="form_140.png"/>, if the maximum number of affinely independent points in <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is <img class="formulaInl" alt="$k + 1$" src="form_141.png"/>.</p>
<p>We remark that the above definition only applies to polyhedra that are not empty, so that <img class="formulaInl" alt="$0 \leq \pdim(\cP) \leq n$" src="form_142.png"/>. By convention, the affine dimension of an empty polyhedron is 0 (even though the ``natural'' generalization of the definition above would imply that the affine dimension of an empty polyhedron is <img class="formulaInl" alt="$-1$" src="form_143.png"/>).</p>
<dl class="note"><dt><b>Note:</b></dt><dd>The affine dimension <img class="formulaInl" alt="$k \leq n$" src="form_144.png"/> of an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> must not be confused with the space dimension <img class="formulaInl" alt="$n$" src="form_0.png"/> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>, which is the dimension of the enclosing vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/>. In particular, we can have <img class="formulaInl" alt="$\pdim(\cP) \neq \pdim(\cQ)$" src="form_145.png"/> even though <img class="formulaInl" alt="$\cP$" src="form_58.png"/> and <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> are dimension-compatible; and vice versa, <img class="formulaInl" alt="$\cP$" src="form_58.png"/> and <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> may be dimension-incompatible polyhedra even though <img class="formulaInl" alt="$\pdim(\cP) = \pdim(\cQ)$" src="form_147.png"/>.</dd></dl>
<h3><a class="anchor" id="Rational_Polyhedra">
Rational Polyhedra</a></h3>
<p>An NNC polyhedron is called <em>rational</em> 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.</p>
<p>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.</p>
<h2><a class="anchor" id="Operations_on_Convex_Polyhedra">
Operations on Convex Polyhedra</a></h2>
<p>In this section we briefly describe operations on NNC polyhedra that are provided by the library.</p>
<h3><a class="anchor" id="Intersection_and_Convex_Polyhedral_Hull">
Intersection and Convex Polyhedral Hull</a></h3>
<p>For any pair of NNC polyhedra <img class="formulaInl" alt="$\cP_1, \cP_2 \in \Pset_n$" src="form_148.png"/>, the <em>intersection</em> of <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> and <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>, defined as the set intersection <img class="formulaInl" alt="$\cP_1 \inters \cP_2$" src="form_151.png"/>, is the biggest NNC polyhedron included in both <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> and <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>; similarly, the <em>convex polyhedral hull</em> (or <em>poly-hull</em>) of <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> and <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>, denoted by <img class="formulaInl" alt="$\cP_1 \uplus \cP_2$" src="form_152.png"/>, is the smallest NNC polyhedron that includes both <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> and <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>. The intersection and poly-hull of any pair of closed polyhedra in <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/> is also closed.</p>
<p>In theoretical terms, the intersection and poly-hull operators defined above are the binary <em>meet</em> and the binary <em>join</em> operators on the lattices <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/> and <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/>.</p>
<h3><a class="anchor" id="Convex_Polyhedral_Difference">
Convex Polyhedral Difference</a></h3>
<p>For any pair of NNC polyhedra <img class="formulaInl" alt="$\cP_1, \cP_2 \in \Pset_n$" src="form_148.png"/>, the <em>convex polyhedral difference</em> (or <em>poly-difference</em>) of <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> and <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/> is defined as the smallest convex polyhedron containing the set-theoretic difference of <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> and <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>.</p>
<p>In general, even though <img class="formulaInl" alt="$\cP_1, \cP_2 \in \CPset_n$" src="form_153.png"/> 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.</p>
<h3><a class="anchor" id="Concatenating_Polyhedra">
Concatenating Polyhedra</a></h3>
<p>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 <em>concatenation</em> of the polyhedra <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> and <img class="formulaInl" alt="$\cQ \in \Pset_m$" src="form_154.png"/> (taken in this order) is the polyhedron <img class="formulaInl" alt="$\cR \in \Pset_{n+m}$" src="form_155.png"/> such that </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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\}. \]" src="form_156.png"/>
</p>
<p> Another way of seeing it is as follows: first embed polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> into a vector space of dimension <img class="formulaInl" alt="$n+m$" src="form_157.png"/> and then add a suitably renamed-apart version of the constraints defining <img class="formulaInl" alt="$\cQ$" src="form_146.png"/>.</p>
<h3><a class="anchor" id="Adding_New_Dimensions_to_the_Vector_Space">
Adding New Dimensions to the Vector Space</a></h3>
<p>The library provides two operators for adding a number <img class="formulaInl" alt="$i$" src="form_158.png"/> of space dimensions to an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/>, therefore transforming it into a new NNC polyhedron <img class="formulaInl" alt="$\cQ \in \Pset_{n+i}$" src="form_159.png"/>. In both cases, the added dimensions of the vector space are those having the highest indices.</p>
<p>The operator <code>add_space_dimensions_and_embed</code> <em>embeds</em> the polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> into the new vector space of dimension <img class="formulaInl" alt="$i+n$" src="form_160.png"/> and returns the polyhedron <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> defined by all and only the constraints defining <img class="formulaInl" alt="$\cP$" src="form_58.png"/> (the variables corresponding to the added dimensions are unconstrained). For instance, when starting from a polyhedron <img class="formulaInl" alt="$\cP \sseq \Rset^2$" src="form_161.png"/> and adding a third space dimension, the result will be the polyhedron </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cQ = \bigl\{\, (x_0, x_1, x_2)^\transpose \in \Rset^3 \bigm| (x_0, x_1)^\transpose \in \cP \,\bigr\}. \]" src="form_162.png"/>
</p>
<p>In contrast, the operator <code>add_space_dimensions_and_project</code> <em>projects</em> the polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> into the new vector space of dimension <img class="formulaInl" alt="$i+n$" src="form_160.png"/> and returns the polyhedron <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> whose constraint system, besides the constraints defining <img class="formulaInl" alt="$\cP$" src="form_58.png"/>, 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 <img class="formulaInl" alt="$\cP \sseq \Rset^2$" src="form_161.png"/> and adding a third space dimension, the result will be the polyhedron </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cQ = \bigl\{\, (x_0, x_1, 0)^\transpose \in \Rset^3 \bigm| (x_0, x_1)^\transpose \in \cP \,\bigr\}. \]" src="form_163.png"/>
</p>
<h3><a class="anchor" id="Removing_Dimensions_from_the_Vector_Space">
Removing Dimensions from the Vector Space</a></h3>
<p>The library provides two operators for removing space dimensions from an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/>, therefore transforming it into a new NNC polyhedron <img class="formulaInl" alt="$\cQ \in \Pset_m$" src="form_154.png"/> where <img class="formulaInl" alt="$m \leq n$" src="form_132.png"/>.</p>
<p>Given a set of variables, the operator <code>remove_space_dimensions</code> removes all the space dimensions specified by the variables in the set. For instance, letting <img class="formulaInl" alt="$\cP \in \Pset_4$" src="form_164.png"/> be the singleton set <img class="formulaInl" alt="$\bigl\{ (3, 1, 0, 2)^\transpose \bigr\} \sseq \Rset^4$" src="form_165.png"/>, then after invoking this operator with the set of variables <img class="formulaInl" alt="$\{x_1, x_2\}$" src="form_166.png"/> the resulting polyhedron is </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cQ = \bigl\{ (3, 2)^\transpose \bigr\} \sseq \Rset^2. \]" src="form_167.png"/>
</p>
<p>Given a space dimension <img class="formulaInl" alt="$m$" src="form_168.png"/> less than or equal to that of the polyhedron, the operator <code>remove_higher_space_dimensions</code> removes the space dimensions having indices greater than or equal to <img class="formulaInl" alt="$m$" src="form_168.png"/>. For instance, letting <img class="formulaInl" alt="$\cP \in \Pset_4$" src="form_164.png"/> defined as before, by invoking this operator with <img class="formulaInl" alt="$m = 2$" src="form_169.png"/> the resulting polyhedron will be </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cQ = \bigl\{ (3, 1)^\transpose \bigr\} \sseq \Rset^2. \]" src="form_170.png"/>
</p>
<h3><a class="anchor" id="Mapping_the_Dimensions_of_the_Vector_Space">
Mapping the Dimensions of the Vector Space</a></h3>
<p>The operator <code>map_space_dimensions</code> provided by the library maps the dimensions of the vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> according to a partial injective function <img class="formulaInl" alt="$\pard{\rho}{\{0, \ldots, n-1\}}{\Nset}$" src="form_171.png"/> such that <img class="formulaInl" alt="$\rho\bigl(\{0, \ldots, n-1\}\bigr) = \{0, \ldots, m-1\}$" src="form_172.png"/> with <img class="formulaInl" alt="$m \leq n$" src="form_132.png"/>. Dimensions corresponding to indices that are not mapped by <img class="formulaInl" alt="$\rho$" src="form_173.png"/> are removed.</p>
<p>If <img class="formulaInl" alt="$m = 0$" src="form_174.png"/>, i.e., if the function <img class="formulaInl" alt="$\rho$" src="form_173.png"/> is undefined everywhere, then the operator projects the argument polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> onto the zero-dimension space <img class="formulaInl" alt="$\Rset^0$" src="form_175.png"/>; otherwise the result is <img class="formulaInl" alt="$\cQ \in \Pset_m$" src="form_154.png"/> given by </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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\}. \]" src="form_176.png"/>
</p>
<p><a class="anchor" id="expand_space_dimension"></a> </p>
<h3><a class="anchor" id="Expanding_One_Dimension_of_the_Vector_Space_to_Multiple_Dimensions">
Expanding One Dimension of the Vector Space to Multiple Dimensions</a></h3>
<p>The operator <code>expand_space_dimension</code> provided by the library adds <img class="formulaInl" alt="$m$" src="form_168.png"/> new space dimensions to a polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/>, with <img class="formulaInl" alt="$n > 0$" src="form_177.png"/>, so that dimensions <img class="formulaInl" alt="$n$" src="form_0.png"/>, <img class="formulaInl" alt="$n+1$" src="form_178.png"/>, <img class="formulaInl" alt="$\ldots$" src="form_179.png"/>, <img class="formulaInl" alt="$n+m-1$" src="form_180.png"/> of the result <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> are exact copies of the <img class="formulaInl" alt="$i$" src="form_158.png"/>-th space dimension of <img class="formulaInl" alt="$\cP$" src="form_58.png"/>. More formally, </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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 }. \]" src="form_181.png"/>
</p>
<p> This operation has been proposed in <a class="el" href="main.html#GDDetal04">[GDDetal04]</a>.</p>
<p><a class="anchor" id="fold_space_dimensions"></a> </p>
<h3><a class="anchor" id="Folding_Multiple_Dimensions_of_the_Vector_Space_into_One_Dimension">
Folding Multiple Dimensions of the Vector Space into One Dimension</a></h3>
<p>The operator <code>fold_space_dimensions</code> provided by the library, given a polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/>, with <img class="formulaInl" alt="$n > 0$" src="form_177.png"/>, folds a set of space dimensions <img class="formulaInl" alt="$J = \{ j_0, \ldots, j_{m-1} \}$" src="form_182.png"/>, with <img class="formulaInl" alt="$m < n$" src="form_183.png"/> and <img class="formulaInl" alt="$j < n$" src="form_184.png"/> for each <img class="formulaInl" alt="$j \in J$" src="form_185.png"/>, into space dimension <img class="formulaInl" alt="$i < n$" src="form_186.png"/>, where <img class="formulaInl" alt="$i \notin J$" src="form_187.png"/>. The result is given by </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cQ \defeq \biguplus_{d = 0}^m \cQ_d \]" src="form_188.png"/>
</p>
<p> where </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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 } \]" src="form_189.png"/>
</p>
<p> and, for <img class="formulaInl" alt="$ d = 0 $" src="form_190.png"/>, <img class="formulaInl" alt="$ \ldots $" src="form_191.png"/>, <img class="formulaInl" alt="$ m-1 $" src="form_192.png"/>, </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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 }, \]" src="form_193.png"/>
</p>
<p> and, finally, for <img class="formulaInl" alt="$ k = 0 $" src="form_194.png"/>, <img class="formulaInl" alt="$ \ldots $" src="form_191.png"/>, <img class="formulaInl" alt="$ n-1 $" src="form_195.png"/>, </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ k' \defeq k - \card \{\, j \in J \mid k > j \,\}, \]" src="form_196.png"/>
</p>
<p> (<img class="formulaInl" alt="$\card S$" src="form_197.png"/> denotes the cardinality of the finite set <img class="formulaInl" alt="$S$" src="form_74.png"/>).</p>
<p>This operation has been proposed in <a class="el" href="main.html#GDDetal04">[GDDetal04]</a>.</p>
<p><a class="anchor" id="affine_relation"></a> </p>
<h3><a class="anchor" id="Images_and_Preimages_of_Affine_Transfer_Relations">
Images and Preimages of Affine Transfer Relations</a></h3>
<p>For each relation <img class="formulaInl" alt="$\reld{\phi}{\Rset^n}{\Rset^m}$" src="form_198.png"/>, we denote by <img class="formulaInl" alt="$\phi(S) \sseq \Rset^m$" src="form_199.png"/> the <em>image</em> under <img class="formulaInl" alt="$\phi$" src="form_200.png"/> of the set <img class="formulaInl" alt="$S \sseq \Rset^n$" src="form_201.png"/>; formally, </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \phi(S) \defeq \bigl\{\, \vect{w} \in \Rset^m \bigm| \exists \vect{v} \in S \st (\vect{v}, \vect{w}) \in \phi \,\bigr\}. \]" src="form_202.png"/>
</p>
<p> Similarly, we denote by <img class="formulaInl" alt="$\phi^{-1}(S') \sseq \Rset^n$" src="form_203.png"/> the <em>preimage</em> under <img class="formulaInl" alt="$\phi$" src="form_200.png"/> of <img class="formulaInl" alt="$S' \sseq \Rset^m$" src="form_204.png"/>, that is </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \phi^{-1}(S') \defeq \bigl\{\, \vect{v} \in \Rset^n \bigm| \exists \vect{w} \in S' \st (\vect{v}, \vect{w}) \in \phi \,\bigr\}. \]" src="form_205.png"/>
</p>
<p> If <img class="formulaInl" alt="$n = m$" src="form_206.png"/>, then the relation <img class="formulaInl" alt="$\phi$" src="form_200.png"/> is said to be <em>space dimension preserving</em>.</p>
<p>The relation <img class="formulaInl" alt="$\reld{\phi}{\Rset^n}{\Rset^m}$" src="form_198.png"/> is said to be an <em>affine relation</em> if there exists <img class="formulaInl" alt="$\ell \in \Nset$" src="form_207.png"/> such that </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^n, \vect{w} \in \Rset^m \itc (\vect{v}, \vect{w}) \in \phi \iff \bigland_{i=1}^{\ell} \bigl( \langle \vect{c}_i, \vect{w} \rangle \relsym_i \langle \vect{a}_i, \vect{v} \rangle + b_i \bigr), \]" src="form_208.png"/>
</p>
<p> where <img class="formulaInl" alt="$\vect{a}_i \in \Rset^n$" src="form_209.png"/>, <img class="formulaInl" alt="$\vect{c}_i \in \Rset^m$" src="form_210.png"/>, <img class="formulaInl" alt="$b_i \in \Rset$" src="form_211.png"/> and <img class="formulaInl" alt="$\mathord{\relsym}_i \in \{ <, \leq, =, \geq, > \}$" src="form_212.png"/>, for each <img class="formulaInl" alt="$i = 1, \ldots, \ell$" src="form_213.png"/>.</p>
<p>As a special case, the relation <img class="formulaInl" alt="$\reld{\phi}{\Rset^n}{\Rset^m}$" src="form_198.png"/> is an <em>affine function</em> if and only if there exist a matrix <img class="formulaInl" alt="$A \in \Rset^m \times \Rset^n$" src="form_214.png"/> and a vector <img class="formulaInl" alt="$\vect{b} \in \Rset^m$" src="form_215.png"/> such that, </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^n, \vect{w} \in \Rset^m \itc (\vect{v}, \vect{w}) \in \phi \iff \vect{w} = A\vect{v} + \vect{b}. \]" src="form_216.png"/>
</p>
<p>The set <img class="formulaInl" alt="$\Pset_n$" src="form_61.png"/> of NNC polyhedra is closed under the application of images and preimages of any space dimension preserving affine relation. The same property holds for the set <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/> of closed polyhedra, provided the affine relation makes no use of the strict relation symbols <img class="formulaInl" alt="$<$" src="form_217.png"/> and <img class="formulaInl" alt="$>$" src="form_218.png"/>. Images and preimages of affine relations can be used to model several kinds of transition relations, including deterministic assignments of affine expressions, (affinely constrained) nondeterministic assignments and affine conditional guards.</p>
<p>A space dimension preserving relation <img class="formulaInl" alt="$\reld{\phi}{\Rset^n}{\Rset^n}$" src="form_219.png"/> can be specified by means of a shorthand notation:</p>
<ul>
<li>the vector <img class="formulaInl" alt="$\vect{x} = (x_0, \ldots, x_{n-1})^\transpose$" src="form_220.png"/> of <em>unprimed</em> variables is used to represent the space dimensions of the domain of <img class="formulaInl" alt="$\phi$" src="form_200.png"/>;</li>
<li>the vector <img class="formulaInl" alt="$\vect{x}' = (x'_0, \ldots, x'_{n-1})^\transpose$" src="form_221.png"/> of <em>primed</em> variables is used to represent the space dimensions of the range of <img class="formulaInl" alt="$\phi$" src="form_200.png"/>;</li>
<li>any primed variable that ``does not occur'' in the shorthand specification is meant to be <em>unaffected</em> by the relation; namely, for each index <img class="formulaInl" alt="$i \in \{0, \ldots, n-1\}$" src="form_28.png"/>, if in the syntactic specification of the relation the primed variable <img class="formulaInl" alt="$x'_i$" src="form_222.png"/> only occurs (if ever) with coefficient 0, then it is assumed that the specification also contains the constraint <img class="formulaInl" alt="$x'_i = x_i$" src="form_223.png"/>.</li>
</ul>
<p>As an example, assuming <img class="formulaInl" alt="$\reld{\phi}{\Rset^3}{\Rset^3}$" src="form_224.png"/>, the notation <img class="formulaInl" alt="$x'_0 - x'_2 \geq 2 x_0 - x_1$" src="form_225.png"/>, where the primed variable <img class="formulaInl" alt="$x'_1$" src="form_226.png"/> does not occur, is meant to specify the affine relation defined by </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^3, \vect{w} \in \Rset^3 \itc (\vect{v}, \vect{w}) \in \phi \iff (w_0 - w_2 \geq 2 v_0 - v_1) \land (w_1 = v_1). \]" src="form_227.png"/>
</p>
<p> The same relation is specified by <img class="formulaInl" alt="$x'_0 + 0 \cdot x'_1 - x'_2 \geq 2 x_0 - x_1$" src="form_228.png"/>, since <img class="formulaInl" alt="$x'_1$" src="form_226.png"/> occurs with coefficient 0.</p>
<p>The library allows for the computation of images and preimages of polyhedra under restricted subclasses of space dimension preserving affine relations, as described in the following.</p>
<h3><a class="anchor" id="Single_Update_Affine_Functions">
Single-Update Affine Functions.</a></h3>
<p>Given a primed variable <img class="formulaInl" alt="$x'_k$" src="form_229.png"/> and an unprimed affine expression <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle + b$" src="form_230.png"/>, the <em>affine function</em> <img class="formulaInl" alt="$\fund{\phi = \bigl(x'_k = \langle \vect{a}, \vect{x} \rangle + b\bigr)} {\Rset^n}{\Rset^n}$" src="form_231.png"/> is defined by </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^n \itc \phi(\vect{v}) = A\vect{v} + \vect{b}, \]" src="form_232.png"/>
</p>
<p> where </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ 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} \]" src="form_233.png"/>
</p>
<p> and the <img class="formulaInl" alt="$a_i$" src="form_234.png"/> (resp., <img class="formulaInl" alt="$b$" src="form_235.png"/>) occur in the <img class="formulaInl" alt="$(k+1)$" src="form_236.png"/>st row in <img class="formulaInl" alt="$A$" src="form_237.png"/> (resp., position in <img class="formulaInl" alt="$\vect{b}$" src="form_238.png"/>). Thus function <img class="formulaInl" alt="$\phi$" src="form_200.png"/> maps any vector <img class="formulaInl" alt="$(v_0, \ldots, v_{n-1})^\transpose$" src="form_239.png"/> to </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \Bigl(v_0, \ldots, \bigl(\textstyle{\sum_{i=0}^{n-1}} a_i v_i + b\bigr), \ldots, v_{n-1}\Bigr)^\transpose. \]" src="form_240.png"/>
</p>
<p>The <em>affine image</em> operator computes the affine image of a polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> under <img class="formulaInl" alt="$x'_k = \langle \vect{a}, \vect{x} \rangle + b$" src="form_241.png"/>. For instance, suppose the polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> to be transformed is the square in <img class="formulaInl" alt="$\Rset^2$" src="form_115.png"/> generated by the set of points <img class="formulaInl" alt="$\bigl\{ (0, 0)^\transpose, (0, 3)^\transpose, (3, 0)^\transpose, (3, 3)^\transpose \bigr\}$" src="form_242.png"/>. Then, if the primed variable is <img class="formulaInl" alt="$x_0$" src="form_243.png"/> and the affine expression is <img class="formulaInl" alt="$x_0 + 2 x_1 + 4$" src="form_244.png"/> (so that <img class="formulaInl" alt="$k = 0$" src="form_245.png"/>, <img class="formulaInl" alt="$a_0 = 1, a_1 = 2, b = 4$" src="form_246.png"/>), the affine image operator will translate <img class="formulaInl" alt="$\cP$" src="form_58.png"/> to the parallelogram <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/> generated by the set of points <img class="formulaInl" alt="$\bigl\{ (4, 0)^\transpose, (10, 3)^\transpose, (7, 0)^\transpose, (13, 3)^\transpose \bigr\}$" src="form_247.png"/> with height equal to the side of the square and oblique sides parallel to the line <img class="formulaInl" alt="$x_0 - 2 x_1$" src="form_248.png"/>. If the primed variable is as before (i.e., <img class="formulaInl" alt="$k = 0$" src="form_245.png"/>) but the affine expression is <img class="formulaInl" alt="$x_1$" src="form_249.png"/> (so that <img class="formulaInl" alt="$a_0 = 0, a_1 = 1, b = 0$" src="form_250.png"/>), then the resulting polyhedron <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/> is the positive diagonal of the square.</p>
<p>The <em>affine preimage</em> operator computes the affine preimage of a polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> under <img class="formulaInl" alt="$x'_k = \langle \vect{a}, \vect{x} \rangle + b$" src="form_241.png"/>. For instance, suppose now that we apply the affine preimage operator as given in the first example using primed variable <img class="formulaInl" alt="$x_0$" src="form_243.png"/> and affine expression <img class="formulaInl" alt="$x_0 + 2 x_1 + 4$" src="form_244.png"/> to the parallelogram <img class="formulaInl" alt="$\cP_1$" src="form_149.png"/>; then we get the original square <img class="formulaInl" alt="$\cP$" src="form_58.png"/> back. If, on the other hand, we apply the affine preimage operator as given in the second example using primed variable <img class="formulaInl" alt="$x_0$" src="form_243.png"/> and affine expression <img class="formulaInl" alt="$x_1$" src="form_249.png"/> to <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>, then the resulting polyhedron is the stripe obtained by adding the line <img class="formulaInl" alt="$(1, 0)^\transpose$" src="form_251.png"/> to polyhedron <img class="formulaInl" alt="$\cP_2$" src="form_150.png"/>.</p>
<p>Observe that provided the coefficient <img class="formulaInl" alt="$a_k$" src="form_252.png"/> of the considered variable in the affine expression is non-zero, the affine function is invertible.</p>
<h3><a class="anchor" id="Single_Update_Bounded_Affine_Relations">
Single-Update Bounded Affine Relations.</a></h3>
<p>Given a primed variable <img class="formulaInl" alt="$x'_k$" src="form_229.png"/> and two unprimed affine expressions <img class="formulaInl" alt="$\mathrm{lb} = \langle \vect{a}, \vect{x} \rangle + b$" src="form_253.png"/> and <img class="formulaInl" alt="$\mathrm{ub} = \langle \vect{c}, \vect{x} \rangle + d$" src="form_254.png"/>, the <em>bounded affine relation</em> <img class="formulaInl" alt="$\phi = (\mathrm{lb} \leq x'_k \leq \mathrm{ub})$" src="form_255.png"/> is defined as </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^n, \vect{w} \in \Rset^n \itc (\vect{v}, \vect{w}) \in \phi \iff \bigl( \langle \vect{a}, \vect{v} \rangle + b \leq w_k \leq \langle \vect{c}, \vect{v} \rangle + d \bigr) \land \Bigl( \bigland_{0 \leq i < n, i \neq k} w_i = v_i \Bigr). \]" src="form_256.png"/>
</p>
<h3><a class="anchor" id="Generalized_Affine_Relations">
Generalized Affine Relations.</a></h3>
<p>Similarly, the <em>generalized affine relation</em> <img class="formulaInl" alt="$\phi = (\mathrm{lhs}' \relsym \mathrm{rhs})$" src="form_257.png"/>, where <img class="formulaInl" alt="$\mathrm{lhs} = \langle \vect{c}, \vect{x} \rangle + d$" src="form_258.png"/> and <img class="formulaInl" alt="$\mathrm{rhs} = \langle \vect{a}, \vect{x} \rangle + b$" src="form_259.png"/> are affine expressions and <img class="formulaInl" alt="$\mathord{\relsym} \in \{ <, \leq, =, \geq, > \}$" src="form_260.png"/> is a relation symbol, is defined as </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^n, \vect{w} \in \Rset^n \itc (\vect{v}, \vect{w}) \in \phi \iff \bigl( \langle \vect{c}, \vect{w} \rangle + d \relsym \langle \vect{a}, \vect{v} \rangle + b \bigr) \land \Bigl( \bigland_{0 \leq i < n, c_i = 0} w_i = v_i \Bigr). \]" src="form_261.png"/>
</p>
<p> When <img class="formulaInl" alt="$\mathrm{lhs} = x_k$" src="form_262.png"/> and <img class="formulaInl" alt="$\mathord{\relsym} \in \{ = \}$" src="form_48.png"/>, then the above affine relation becomes equivalent to the single-update affine function <img class="formulaInl" alt="$x'_k = \mathrm{rhs}$" src="form_263.png"/> (hence the name given to this operator). It is worth stressing that the notation is not symmetric, because the variables occurring in expression <img class="formulaInl" alt="$\mathrm{lhs}$" src="form_264.png"/> are interpreted as primed variables, whereas those occurring in <img class="formulaInl" alt="$\mathrm{rhs}$" src="form_265.png"/> are unprimed; for instance, the transfer relations <img class="formulaInl" alt="$\mathrm{lhs}' \leq \mathrm{rhs}$" src="form_266.png"/> and <img class="formulaInl" alt="$\mathrm{rhs}' \geq \mathrm{lhs}$" src="form_267.png"/> are not equivalent in general.</p>
<h3><a class="anchor" id="Cylindrification">
Cylindrification Operator</a></h3>
<p>The operator <code>unconstrain</code> computes the <em>cylindrification</em> <a class="el" href="main.html#HMT71">[HMT71]</a> of a polyhedron with respect to one of its variables. Formally, the cylindrification <img class="formulaInl" alt="$\cQ \in \Pset_n$" src="form_268.png"/> of an NNC polyhedron <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> with respect to variable index <img class="formulaInl" alt="$i \in \{ 0, \ldots, n-1 \}$" src="form_269.png"/> is defined as follows: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cQ = \bigl\{\, \vect{w} \in \Rset^n \bigm| \exists \vect{v} \in \cP \st \forall j \in \{0, \ldots, n-1\} \itc j \neq i \implies w_j = v_j \,\bigr\}. \]" src="form_270.png"/>
</p>
<p> Cylindrification is an idempotent operation; in particular, note that the computed result has the same space dimension of the original polyhedron. A variant of the operator above allows for the cylindrification of a polyhedron with respect to a finite set of variables.</p>
<h3><a class="anchor" id="Time_Elapse_Operator">
Time-Elapse Operator</a></h3>
<p>The <em>time-elapse</em> operator has been defined in <a class="el" href="main.html#HPR97">[HPR97]</a>. 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 <img class="formulaInl" alt="$\cP, \cQ \in \Pset_n$" src="form_271.png"/>, the time-elapse between <img class="formulaInl" alt="$\cP$" src="form_58.png"/> and <img class="formulaInl" alt="$\cQ$" src="form_146.png"/>, denoted <img class="formulaInl" alt="$ \cP \nearrow \cQ$" src="form_272.png"/>, is the smallest NNC polyhedron containing the set </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \bigl\{\, \vect{p} + \lambda \vect{q} \in \Rset^n \bigm| \vect{p} \in \cP, \vect{q} \in \cQ, \lambda \in \nonnegRset \,\bigr\}. \]" src="form_273.png"/>
</p>
<p> Note that, if <img class="formulaInl" alt="$\cP,\cQ \in \CPset_n$" src="form_274.png"/> are closed polyhedra, the above set is also a closed polyhedron. In contrast, when <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> is not topologically closed, the above set might not be an NNC polyhedron.</p>
<h3><a class="anchor" id="Meet_Preserving_Simplification">
Meet-Preserving Enlargement and Simplification</a></h3>
<p>Let <img class="formulaInl" alt="$\cP, \cQ, \cR \in \Pset_n$" src="form_275.png"/> be NNC polyhedra. Then:</p>
<ul>
<li><img class="formulaInl" alt="$\cR$" src="form_276.png"/> is <em>meet-preserving</em> with respect to <img class="formulaInl" alt="$\cP$" src="form_58.png"/> using context <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> if <img class="formulaInl" alt="$\cR \inters \cQ = \cP \inters \cQ$" src="form_277.png"/>;</li>
</ul>
<ul>
<li><img class="formulaInl" alt="$\cR$" src="form_276.png"/> is an <em>enlargement</em> of <img class="formulaInl" alt="$\cP$" src="form_58.png"/> if <img class="formulaInl" alt="$\cR \Sseq \cP$" src="form_278.png"/>.</li>
</ul>
<ul>
<li><img class="formulaInl" alt="$\cR$" src="form_276.png"/> is a <em>simplification</em> with respect to <img class="formulaInl" alt="$\cP$" src="form_58.png"/> if <img class="formulaInl" alt="$r \leq p$" src="form_279.png"/>, where <img class="formulaInl" alt="$r$" src="form_280.png"/> and <img class="formulaInl" alt="$p$" src="form_281.png"/> are the cardinalities of minimized constraint representations for <img class="formulaInl" alt="$\cR$" src="form_276.png"/> and <img class="formulaInl" alt="$\cP$" src="form_58.png"/>, respectively.</li>
</ul>
<p>Notice that an enlargement need not be a simplification, and vice versa; moreover, the identity function is (trivially) a meet-preserving enlargement and simplification.</p>
<p>The library provides a binary operator (<code>simplify_using_context</code>) for the domain of NNC polyhedra that returns a polyhedron which is a meet-preserving enlargement simplification of its first argument using the second argument as context.</p>
<p>The concept of meet-preserving enlargement and simplification also applies to the other basic domains (boxes, grids, BD and octagonal shapes). See below for a definition of the concept of <a class="el" href="main.html#Powerset_Meet_Preserving_Simplification">meet-preserving simplification for powerset domains</a>.</p>
<p><a class="anchor" id="relation_with"></a> </p>
<h3><a class="anchor" id="Relation_With_Operators">
Relation-With Operators</a></h3>
<p>The library provides operators for checking the relation holding between an NNC polyhedron and either a constraint or a generator.</p>
<p>Suppose <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is an NNC polyhedron and <img class="formulaInl" alt="$\cC$" src="form_121.png"/> an arbitrary constraint system representing <img class="formulaInl" alt="$\cP$" src="form_58.png"/>. Suppose also that <img class="formulaInl" alt="$ c = \bigl( \langle \vect{a}, \vect{x} \rangle \relsym b \bigr) $" src="form_282.png"/> is a constraint with <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq, > \}$" src="form_46.png"/> and <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> the set of points that satisfy <img class="formulaInl" alt="$c$" src="form_283.png"/>. The possible relations between <img class="formulaInl" alt="$\cP$" src="form_58.png"/> and <img class="formulaInl" alt="$c$" src="form_283.png"/> are as follows.</p>
<ul>
<li><img class="formulaInl" alt="$\cP$" src="form_58.png"/> <em>is disjoint</em> from <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cP \inters \cQ = \emptyset$" src="form_284.png"/>; that is, adding <img class="formulaInl" alt="$c$" src="form_283.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> gives us the empty polyhedron.</li>
<li><img class="formulaInl" alt="$\cP$" src="form_58.png"/> <em>strictly intersects</em> <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cP \inters \cQ \neq \emptyset$" src="form_285.png"/> and <img class="formulaInl" alt="$\cP \inters \cQ \subset \cP$" src="form_286.png"/>; that is, adding <img class="formulaInl" alt="$c$" src="form_283.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> gives us a non-empty polyhedron strictly smaller than <img class="formulaInl" alt="$\cP$" src="form_58.png"/>.</li>
<li><img class="formulaInl" alt="$\cP$" src="form_58.png"/> <em>is included</em> in <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cP \sseq \cQ$" src="form_287.png"/>; that is, adding <img class="formulaInl" alt="$c$" src="form_283.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> leaves <img class="formulaInl" alt="$\cP$" src="form_58.png"/> unchanged.</li>
<li><img class="formulaInl" alt="$\cP$" src="form_58.png"/> <em>saturates</em> <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cP \sseq \cH$" src="form_288.png"/>, where <img class="formulaInl" alt="$\cH$" src="form_289.png"/> is the hyperplane induced by constraint <img class="formulaInl" alt="$c$" src="form_283.png"/>, i.e., the set of points satisfying the equality constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle = b$" src="form_51.png"/>; that is, adding the constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle = b$" src="form_51.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> leaves <img class="formulaInl" alt="$\cP$" src="form_58.png"/> unchanged.</li>
</ul>
<p>The polyhedron <img class="formulaInl" alt="$\cP$" src="form_58.png"/> <em>subsumes</em> the generator <img class="formulaInl" alt="$g$" src="form_290.png"/> if adding <img class="formulaInl" alt="$g$" src="form_290.png"/> to any generator system representing <img class="formulaInl" alt="$\cP$" src="form_58.png"/> does not change <img class="formulaInl" alt="$\cP$" src="form_58.png"/>.</p>
<h3><a class="anchor" id="Widening_Operators">
Widening Operators</a></h3>
<p>The library provides two widening operators for the domain of polyhedra. <a class="anchor" id="H79_widening"></a> The first one, that we call <em>H79-widening</em>, mainly follows the specification provided in the PhD thesis of N. Halbwachs <a class="el" href="main.html#Hal79">[Hal79]</a>, also described in <a class="el" href="main.html#HPR97">[HPR97]</a>. Note that in the computation of the H79-widening <img class="formulaInl" alt="$\cP \widen \cQ$" src="form_291.png"/> of two polyhedra <img class="formulaInl" alt="$\cP, \cQ \in \CPset_n$" src="form_292.png"/> it is required as a precondition that <img class="formulaInl" alt="$\cP \sseq \cQ$" src="form_287.png"/> (the same assumption was implicitly present in the cited papers).</p>
<p><a class="anchor" id="BHRZ03_widening"></a> The second widening operator, that we call <em>BHRZ03-widening</em>, is an instance of the specification provided in <a class="el" href="main.html#BHRZ03a">[BHRZ03a]</a>. This operator also requires as a precondition that <img class="formulaInl" alt="$\cP \sseq \cQ$" src="form_287.png"/> and it is guaranteed to provide a result which is at least as precise as the H79-widening.</p>
<p>Both widening operators can be applied to NNC polyhedra. 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.</p>
<dl class="note"><dt><b>Note:</b></dt><dd>As is the case for the other operators on polyhedra, the implementation overwrites one of the two polyhedra arguments with the result of the widening application. To avoid trivial misunderstandings, it is worth stressing that if polyhedra <img class="formulaInl" alt="$\cP$" src="form_58.png"/> and <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> (where <img class="formulaInl" alt="$\cP \sseq \cQ$" src="form_287.png"/>) are identified by program variables <code>p</code> and <code>q</code>, respectively, then the call <code>q.H79_widening_assign(p)</code> will assign the polyhedron <img class="formulaInl" alt="$\cP \widen \cQ$" src="form_291.png"/> to variable <code>q</code>. Namely, it is the bigger polyhedron <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> which is overwritten by the result of the widening. The smaller polyhedron is not modified, so as to lead to an easier coding of the usual convergence test (<img class="formulaInl" alt="$\cP \Sseq \cP \widen \cQ$" src="form_293.png"/> can be coded as <code>p.contains(q)</code>). Note that, in the above context, a call such as <code>p.H79_widening_assign(q)</code> is likely to result in undefined behavior, since the precondition <img class="formulaInl" alt="$\cQ \sseq \cP$" src="form_294.png"/> will be missed (unless it happens that <img class="formulaInl" alt="$\cP = \cQ$" src="form_295.png"/>). The same observation holds for all flavors of widenings and extrapolation operators that are implemented in the library and for all the language interfaces.</dd></dl>
<h3><a class="anchor" id="Widening_with_Tokens">
Widening with Tokens</a></h3>
<p>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 <img class="formulaInl" alt="$k$" src="form_296.png"/> and only apply widenings starting from the <img class="formulaInl" alt="$k$" src="form_296.png"/>-th iteration.</p>
<p>The library also supports an improved widening delay strategy, that we call <em>widening with tokens</em> <a class="el" href="main.html#BHRZ03a">[BHRZ03a]</a>. A token is a sort of wild card 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 <em>potential</em> 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 <img class="formulaInl" alt="$k$" src="form_296.png"/> of tokens, which will be used if and when needed. When there are no tokens left, the widening is always applied.</p>
<h3><a class="anchor" id="Extrapolation_Operators">
Extrapolation Operators</a></h3>
<p>Besides the two widening operators, the library also implements several <em>extrapolation</em> operators, which differ from widenings in that their use along an upper iteration sequence does not ensure convergence in a finite number of steps.</p>
<p><a class="anchor" id="limited_extrapolation"></a> In particular, for each of the two widenings there is a corresponding <em>limited</em> extrapolation operator, which can be used to implement the <em>widening ``up to''</em> technique as described in <a class="el" href="main.html#HPR97">[HPR97]</a>. 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 <a class="el" href="main.html#HPR97">[HPR97]</a> this set is fixed once and for all before starting the computation of the upward iteration sequence.</p>
<p><a class="anchor" id="bounded_extrapolation"></a> The <em>bounded</em> extrapolation operators further enhance each one of the limited extrapolation operators described above by intersecting the result of the limited extrapolation operation with the box obtained as a result of applying the <a class="el" href="main.html#CC76_interval_widening">CC76-widening</a> to the smallest <a class="el" href="main.html#Intervals_and_Boxes">boxes</a> enclosing the two argument polyhedra.</p>
<h2><a class="anchor" id="Intervals_and_Boxes">
Intervals and Boxes</a></h2>
<p>The PPL provides support for computations on non-relational domains, called boxes, and also the interval domains used for their representation.</p>
<p><a class="anchor" id="intervals"></a> An <em>interval</em> in <img class="formulaInl" alt="$\Rset$" src="form_26.png"/> is a pair of <em>bounds</em>, called <em>lower</em> and <em>upper</em>. Each bound can be either (1) <em>closed and bounded</em>, (2) <em>open and bounded</em>, or (3) <em>open and unbounded</em>. If the bound is <em>bounded</em>, then it has a value in <img class="formulaInl" alt="$\Rset$" src="form_26.png"/>. For each vector <img class="formulaInl" alt="$\vect{a} \in \Rset^n$" src="form_43.png"/> and scalar <img class="formulaInl" alt="$b \in \Rset$" src="form_44.png"/>, and for each relation symbol <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq, >\}$" src="form_297.png"/>, the constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \relsym b$" src="form_47.png"/> is said to be a <em>interval constraint</em> if there exist an index <img class="formulaInl" alt="$i \in \{ 0, \ldots, n-1 \}$" src="form_269.png"/> such that, for all <img class="formulaInl" alt="$k \in \{ 0, \ldots, i-1, i+1, \ldots, n-1 \}$" src="form_298.png"/>, <img class="formulaInl" alt="$a_k = 0$" src="form_299.png"/>. Thus each interval constraint that is not a tautology or inconsistent has the form <img class="formulaInl" alt="$x = r$" src="form_300.png"/>, <img class="formulaInl" alt="$x \leq r$" src="form_301.png"/>, <img class="formulaInl" alt="$x \geq r$" src="form_302.png"/>, <img class="formulaInl" alt="$x < r$" src="form_303.png"/> or <img class="formulaInl" alt="$x > r$" src="form_304.png"/>, with <img class="formulaInl" alt="$r \in \Rset$" src="form_305.png"/>.</p>
<p>Letting <img class="formulaInl" alt="$\cB$" src="form_306.png"/> be a sequence of <img class="formulaInl" alt="$n$" src="form_0.png"/> intervals and <img class="formulaInl" alt="$\vect{e}_i = (0, \ldots, 1, \ldots, 0)^\transpose$" src="form_307.png"/> be the vector in <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> with 1 in the <img class="formulaInl" alt="$i$" src="form_158.png"/>'th position and zeroes in every other position; if the lower bound of the <img class="formulaInl" alt="$i$" src="form_158.png"/>'th interval in <img class="formulaInl" alt="$\cB$" src="form_306.png"/> is bounded, the corresponding interval constraint is defined as <img class="formulaInl" alt="$\langle \vect{e}_i, \vect{x} \rangle \relsym b$" src="form_308.png"/>, where <img class="formulaInl" alt="$b$" src="form_235.png"/> is the value of the bound and <img class="formulaInl" alt="$\mathord{\relsym}$" src="form_309.png"/> is <img class="formulaInl" alt="$\mathord{\geq}$" src="form_310.png"/> if it is a closed bound and <img class="formulaInl" alt="$\mathord{>}$" src="form_311.png"/> if it is an open bound. Similarly, if the upper bound of the <img class="formulaInl" alt="$i$" src="form_158.png"/>'th interval in <img class="formulaInl" alt="$\cB$" src="form_306.png"/> is bounded, the corresponding interval constraint is defined as <img class="formulaInl" alt="$\langle\vect{e}_i,\vect{x}\rangle \relsym b$" src="form_312.png"/>, where <img class="formulaInl" alt="$b$" src="form_235.png"/> is the value of the bound and <img class="formulaInl" alt="$\mathord{\relsym}$" src="form_309.png"/> is <img class="formulaInl" alt="$\mathord{\leq}$" src="form_313.png"/> if it is a closed bound and <img class="formulaInl" alt="$\mathord{<}$" src="form_314.png"/> if it is an open bound.</p>
<p>A convex polyhedron <img class="formulaInl" alt="$\cP \in \CPset_n$" src="form_111.png"/> is said to be a <em>box</em> if and only if either <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is the set of solutions to a finite set of interval constraints or <img class="formulaInl" alt="$n = 0$" src="form_59.png"/> and <img class="formulaInl" alt="$\cP = \emptyset$" src="form_60.png"/>. Therefore any <img class="formulaInl" alt="$n$" src="form_0.png"/>-dimensional <em>box</em> <img class="formulaInl" alt="$\cP$" src="form_58.png"/> in <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> where <img class="formulaInl" alt="$n > 0$" src="form_177.png"/> can be represented by a sequence of <img class="formulaInl" alt="$n$" src="form_0.png"/> intervals <img class="formulaInl" alt="$\cB$" src="form_306.png"/> in <img class="formulaInl" alt="$\Rset$" src="form_26.png"/> and <img class="formulaInl" alt="$\cP$" src="form_58.png"/> is a closed polyhedron if every bound in the intervals in <img class="formulaInl" alt="$\cB$" src="form_306.png"/> is either closed and bounded or open and unbounded.</p>
<p><a class="anchor" id="CC76_interval_widening"></a> </p>
<h3><a class="anchor" id="Widening_and_Extrapolation_Operators_on_Boxes">
Widening and Extrapolation Operators on Boxes</a></h3>
<p>The library provides a widening operator for boxes. Given two sequences of intervals defining two <img class="formulaInl" alt="$n$" src="form_0.png"/>-dimensional boxes, the <em>CC76-widening</em> applies, for each corresponding interval and bound, the interval constraint widening defined in <a class="el" href="main.html#CC76">[CC76]</a>. For extra precision, this incorporates the widening with thresholds as defined in <a class="el" href="main.html#BCCetal02">[BCCetal02]</a> with <img class="formulaInl" alt="$\{-2, -1, 0, 1, 2\}$" src="form_315.png"/> as the set of default threshold values.</p>
<h2><a class="anchor" id="Weakly_Relational_Shapes">
Weakly-Relational Shapes</a></h2>
<p>The PPL provides support for computations on numerical domains that, in selected contexts, can achieve a better precision/efficiency ratio with respect to the corresponding computations on a ``fully relational'' domain of convex polyhedra. This is achieved by restricting the syntactic form of the constraints that can be used to describe the domain elements.</p>
<h3><a class="anchor" id="Bounded_Difference_Shapes">
Bounded Difference Shapes</a></h3>
<p>For each vector <img class="formulaInl" alt="$\vect{a} \in \Rset^n$" src="form_43.png"/> and scalar <img class="formulaInl" alt="$b \in \Rset$" src="form_44.png"/>, and for each relation symbol <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq\}$" src="form_316.png"/>, the linear constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \relsym b$" src="form_47.png"/> is said to be a <em>bounded difference</em> if there exist two indices <img class="formulaInl" alt="$i, j \in \{ 0, \ldots, n-1 \}$" src="form_317.png"/> such that:</p>
<ul>
<li><img class="formulaInl" alt="$a_i, a_j \in \{ -1, 0, 1 \}$" src="form_318.png"/> and <img class="formulaInl" alt="$a_i \neq a_j$" src="form_319.png"/>;</li>
<li><img class="formulaInl" alt="$a_k = 0$" src="form_299.png"/>, for all <img class="formulaInl" alt="$k \notin \{ i, j \}$" src="form_320.png"/>.</li>
</ul>
<p>A convex polyhedron <img class="formulaInl" alt="$\cP \in \CPset_n$" src="form_111.png"/> is said to be a <em>bounded difference shape</em> (BDS, for short) if and only if either <img class="formulaInl" alt="$\cP$" src="form_58.png"/> can be expressed as the intersection of a finite number of bounded difference constraints or <img class="formulaInl" alt="$n = 0$" src="form_59.png"/> and <img class="formulaInl" alt="$\cP = \emptyset$" src="form_60.png"/>.</p>
<h3><a class="anchor" id="Octagonal_Shapes">
Octagonal Shapes</a></h3>
<p>For each vector <img class="formulaInl" alt="$\vect{a} \in \Rset^n$" src="form_43.png"/> and scalar <img class="formulaInl" alt="$b \in \Rset$" src="form_44.png"/>, and for each relation symbol <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq\}$" src="form_316.png"/>, the linear constraint <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \relsym b$" src="form_47.png"/> is said to be an <em>octagonal</em> if there exist two indices <img class="formulaInl" alt="$i, j \in \{ 0, \ldots, n-1 \}$" src="form_317.png"/> such that:</p>
<ul>
<li><img class="formulaInl" alt="$a_i, a_j \in \{ -1, 0, 1 \}$" src="form_318.png"/>;</li>
<li><img class="formulaInl" alt="$a_k = 0$" src="form_299.png"/>, for all <img class="formulaInl" alt="$k \notin \{ i, j \}$" src="form_320.png"/>.</li>
</ul>
<p>A convex polyhedron <img class="formulaInl" alt="$\cP \in \CPset_n$" src="form_111.png"/> is said to be an <em>octagonal shape</em> (OS, for short) if and only if either <img class="formulaInl" alt="$\cP$" src="form_58.png"/> can be expressed as the intersection of a finite number of octagonal constraints or <img class="formulaInl" alt="$n = 0$" src="form_59.png"/> and <img class="formulaInl" alt="$\cP = \emptyset$" src="form_60.png"/>.</p>
<p>Note that, since any bounded difference is also an octagonal constraint, any BDS is also an OS. The name ``octagonal'' comes from the fact that, in a vector space of dimension 2, a bounded OS can have eight sides at most.</p>
<h3><a class="anchor" id="Weakly_Relational_Shape_Interface">
Weakly-Relational Shapes Interface</a></h3>
<p>By construction, any BDS or OS is always topologically closed. Under the usual set inclusion ordering, the set of all BDSs (resp., OSs) on the vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> is a lattice having the empty set <img class="formulaInl" alt="$\emptyset$" src="form_56.png"/> and the universe <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> as the smallest and the biggest elements, respectively. In theoretical terms, it is a meet sub-lattice of <img class="formulaInl" alt="$\CPset_n$" src="form_63.png"/>; moreover, the lattice of BDSs is a meet sublattice of the lattice of OSs. The least upper bound of a finite set of BDSs (resp., OSs) is said to be their <em>bds-hull</em> (resp., <em>oct-hull</em>).</p>
<p>As far as the representation of the rational inhomogeneous term of each bounded difference or octagonal constraint is concerned, several <em>rounding-aware</em> implementation choices are available, including:</p>
<ul>
<li>bounded precision integer types;</li>
<li>bounded precision floating point types;</li>
<li>unbounded precision integer and rational types, as provided by GMP.</li>
</ul>
<p>The user interface for BDSs and OSs is meant to be as similar as possible to the one developed for the domain of closed polyhedra: in particular, all operators on polyhedra are also available for the domains of BDSs and OSs, even though they are typically characterized by a lower degree of precision. For instance, the <em>bds-difference</em> and <em>oct-difference</em> operators return (the smallest) over-approximations of the set-theoretical difference operator on the corresponding domains. In the case of (generalized) images and preimages of affine relations, suitable (possibly not-optimal) over-approximations are computed when the considered relations cannot be precisely modeled by only using bounded differences or octagonal constraints.</p>
<h3><a class="anchor" id="Widening_and_Extrapolation_Operators_on_WR_Shapes">
Widening and Extrapolation Operators on Weakly-Relational Shapes</a></h3>
<p><a class="anchor" id="BHMZ05_widening"></a> For the domains of BDSs and OSs, the library provides a variant of the widening operator for convex polyhedra defined in <a class="el" href="main.html#CH78">[CH78]</a>. The implementation follows the specification in <a class="el" href="main.html#BHMZ05a">[BHMZ05a,BHMZ05b]</a>, resulting in an operator which is well-defined on the corresponding domain (i.e., it does not depend on the internal representation of BDSs or OSs), while still ensuring convergence in a finite number of steps.</p>
<p><a class="anchor" id="CC76_extrapolation"></a> The library also implements an extension of the widening operator for intervals as defined in <a class="el" href="main.html#CC76">[CC76]</a>. The reader is warned that such an extension, even though being well-defined on the domain of BDSs and OSs, is not provided with a convergence guarantee and is therefore an extrapolation operator.</p>
<h2><a class="anchor" id="sect_rational_grids">
Rational Grids</a></h2>
<p>In this section we introduce rational grids as provided by the library. See also <a class="el" href="main.html#BDHetal05">[BDHetal05]</a> for a detailed description of this domain.</p>
<p>The library supports two representations for the grids domain; <em>congruence systems</em> and <em>grid generator systems</em>. We first describe <em>linear congruence relations</em> which form the elements of a congruence system.</p>
<h3><a class="anchor" id="Congruence_Relations">
Congruences and Congruence Relations</a></h3>
<p>For any <img class="formulaInl" alt="$a, b, f \in \Rset$" src="form_321.png"/>, <img class="formulaInl" alt="$a \equiv_f b$" src="form_322.png"/> denotes the <em>congruence</em> <img class="formulaInl" alt="$\exists \mu \in \Zset \st a - b = \mu f$" src="form_323.png"/>.</p>
<p>Let <img class="formulaInl" alt="$\Sset \in \{ \Qset, \Rset \}$" src="form_324.png"/>. For each vector <img class="formulaInl" alt="$\vect{a} \in \Sset^n \setdiff \{\vect{0}\}$" src="form_325.png"/> and scalars <img class="formulaInl" alt="$b, f \in \Sset$" src="form_326.png"/>, the notation <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \equiv_f b$" src="form_327.png"/> stands for the <em>linear congruence relation in <img class="formulaInl" alt="$\Sset^n$" src="form_328.png"/></em> defined by the set of vectors </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \bigl\{\, \vect{v} \in \Rset^n \bigm| \exists \mu \in \Zset \st \langle \vect{a}, \vect{v} \rangle = b + \mu f \,\bigr\}; \]" src="form_329.png"/>
</p>
<p> when <img class="formulaInl" alt="$f \neq 0$" src="form_330.png"/>, the relation is said to be <em>proper</em>; <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \equiv_0 b$" src="form_331.png"/> (i.e., when <img class="formulaInl" alt="$f = 0$" src="form_332.png"/>) denotes the equality <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle = b$" src="form_51.png"/>. <img class="formulaInl" alt="$f$" src="form_333.png"/> is called the <em>frequency</em> or <em>modulus</em> and <img class="formulaInl" alt="$b$" src="form_235.png"/> the <em>base value</em> of the relation. Thus, provided <img class="formulaInl" alt="$\vect{a} \neq \vect{0}$" src="form_45.png"/>, the relation <img class="formulaInl" alt="$\langle \vect{a}, \vect{x} \rangle \equiv_f b$" src="form_327.png"/> defines the set of affine hyperplanes </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \big\{\, \bigl(\langle \vect{a}, \vect{x} \rangle = b + \mu f\bigr) \bigm| \mu \in \Zset \,\bigr\}; \]" src="form_334.png"/>
</p>
<p> if <img class="formulaInl" alt="$b \equiv_f 0$" src="form_335.png"/>, <img class="formulaInl" alt="$\langle \vect{0}, \vect{x} \rangle \equiv_f b$" src="form_336.png"/> defines the universe <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> and the empty set, otherwise.</p>
<h3><a class="anchor" id="Rational_Grids">
Rational Grids</a></h3>
<p>The set <img class="formulaInl" alt="$\cL \sseq \Rset^n$" src="form_337.png"/> is a <em>rational grid</em> if and only if either <img class="formulaInl" alt="$\cL$" src="form_338.png"/> is the set of vectors in <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> that satisfy a finite system <img class="formulaInl" alt="$\cC$" src="form_121.png"/> of congruence relations in <img class="formulaInl" alt="$\Qset^n$" src="form_339.png"/> or <img class="formulaInl" alt="$n = 0$" src="form_59.png"/> and <img class="formulaInl" alt="$\cL = \emptyset$" src="form_340.png"/>.</p>
<p>We also say that <em><img class="formulaInl" alt="$\cL$" src="form_338.png"/> is described by <img class="formulaInl" alt="$\cC$" src="form_121.png"/></em> and that <em><img class="formulaInl" alt="$\cC$" src="form_121.png"/> is a congruence system for <img class="formulaInl" alt="$\cL$" src="form_338.png"/></em>.</p>
<p>The <em>grid domain</em> <img class="formulaInl" alt="$\Gset_{n}$" src="form_341.png"/> is the set of all rational grids described by finite sets of congruence relations in <img class="formulaInl" alt="$\Qset^n$" src="form_339.png"/>.</p>
<p>If the congruence system <img class="formulaInl" alt="$\cC$" src="form_121.png"/> describes the <img class="formulaInl" alt="$\emptyset$" src="form_56.png"/>, the <em>empty</em> grid, then we say that <img class="formulaInl" alt="$\cC$" src="form_121.png"/> is <em>inconsistent</em>. For example, the congruence systems <img class="formulaInl" alt="$\bigl\{\langle\vect{0}, \vect{x}\rangle \equiv_0 1\bigr\}$" src="form_342.png"/> meaning that <img class="formulaInl" alt="$0 = 1$" src="form_343.png"/> and <img class="formulaInl" alt="$\bigl\{\langle\vect{a}, \vect{x}\rangle \equiv_2 0, \langle\vect{a}, \vect{x}\rangle \equiv_2 1\bigr\}$" src="form_344.png"/>, for any <img class="formulaInl" alt="$\vect{a} \in \Rset^n$" src="form_43.png"/>, meaning that the value of an expression must be both even and odd are both inconsistent since both describe the empty grid.</p>
<p>When ordering grids by the set inclusion relation, the empty set <img class="formulaInl" alt="$\emptyset$" src="form_56.png"/> and the vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> (which is described by the empty set of congruence relations) are, respectively, the smallest and the biggest elements of <img class="formulaInl" alt="$\Gset_n$" src="form_345.png"/>. The vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/> is also called the <em>universe</em> grid.</p>
<p>In set theoretical terms, <img class="formulaInl" alt="$\Gset_n$" src="form_345.png"/> is a <em>lattice</em> under set inclusion.</p>
<h3><a class="anchor" id="Integer_Combinations">
Integer Combinations</a></h3>
<p>Let <img class="formulaInl" alt="$S = \{ \vect{x}_1, \ldots, \vect{x}_k \} \sseq \Rset^n$" src="form_71.png"/> be a finite set of vectors. For all scalars <img class="formulaInl" alt="$\mu_1, \ldots, \mu_k \in \Zset$" src="form_346.png"/>, the vector <img class="formulaInl" alt="$\vect{v} = \sum_{j=1}^k \mu_j \vect{x}_j$" src="form_347.png"/> is said to be a <em>integer</em> combination of the vectors in <img class="formulaInl" alt="$S$" src="form_74.png"/>.</p>
<p>We denote by <img class="formulaInl" alt="$\inthull(S)$" src="form_348.png"/> (resp., <img class="formulaInl" alt="$\intaffinehull(S)$" src="form_349.png"/>) the set of all the integer (resp., integer and affine) combinations of the vectors in <img class="formulaInl" alt="$S$" src="form_74.png"/>.</p>
<h3><a class="anchor" id="Points_Parameters_Lines">
Points, Parameters and Lines</a></h3>
<p>Let <img class="formulaInl" alt="$\cL$" src="form_338.png"/> be a grid. Then</p>
<ul>
<li>a vector <img class="formulaInl" alt="$\vect{p} \in \cL$" src="form_350.png"/> is called a <em>grid point</em> of <img class="formulaInl" alt="$\cL$" src="form_338.png"/>;</li>
<li>a vector <img class="formulaInl" alt="$\vect{q} \in \Rset^n$" src="form_351.png"/>, where <img class="formulaInl" alt="$\vect{q} \neq \vect{0}$" src="form_352.png"/>, is called a <em>parameter</em> of <img class="formulaInl" alt="$\cL$" src="form_338.png"/> if <img class="formulaInl" alt="$\cL \neq \emptyset$" src="form_353.png"/> and <img class="formulaInl" alt="$\vect{p} + \mu \vect{q} \in \cL$" src="form_354.png"/>, for all points <img class="formulaInl" alt="$\vect{p} \in \cL$" src="form_350.png"/> and all <img class="formulaInl" alt="$\mu \in \Zset$" src="form_355.png"/>;</li>
<li>a vector <img class="formulaInl" alt="$\vect{l} \in \Rset^n$" src="form_96.png"/> is called a <em>grid line</em> of <img class="formulaInl" alt="$\cL$" src="form_338.png"/> if <img class="formulaInl" alt="$\cL \neq \emptyset$" src="form_353.png"/> and <img class="formulaInl" alt="$\vect{p} + \lambda \vect{l} \in \cL$" src="form_356.png"/>, for all points <img class="formulaInl" alt="$\vect{p} \in \cL$" src="form_350.png"/> and all <img class="formulaInl" alt="$\lambda \in \Rset$" src="form_357.png"/>.</li>
</ul>
<h3><a class="anchor" id="Grid_Generator_Representation">
The Grid Generator Representation</a></h3>
<p>We can generate any rational grid in <img class="formulaInl" alt="$\Gset_n$" src="form_345.png"/> from a finite subset of its points, parameters and lines; each point in a grid is obtained by adding a linear combination of its generating lines to an integral combination of its parameters and an integral affine combination of its generating points.</p>
<p>If <img class="formulaInl" alt="$L, Q, P$" src="form_358.png"/> are each finite subsets of <img class="formulaInl" alt="$\Qset^n$" src="form_339.png"/> and </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \cL = \linearhull(L) + \inthull(Q) + \intaffinehull(P) \]" src="form_359.png"/>
</p>
<p> where the symbol '<img class="formulaInl" alt="$+$" src="form_110.png"/>' denotes the Minkowski's sum, then <img class="formulaInl" alt="$\cL \in \Gset_n$" src="form_360.png"/> is a rational grid (see Section 4.4 in <a class="el" href="main.html#Sch99">[Sch99]</a> and also Proposition 8 in <a class="el" href="main.html#BDHetal05">[BDHetal05]</a>). The 3-tuple <img class="formulaInl" alt="$(L, Q, P)$" src="form_361.png"/> is said to be a <em>grid generator system</em> for <img class="formulaInl" alt="$\cL$" src="form_338.png"/> and we write <img class="formulaInl" alt="$\cL = \ggen(L, Q, P)$" src="form_362.png"/>.</p>
<p>Note that the grid <img class="formulaInl" alt="$\cL = \ggen(L, Q, P) = \emptyset$" src="form_363.png"/> if and only if the set of grid points <img class="formulaInl" alt="$P = \emptyset$" src="form_114.png"/>. If <img class="formulaInl" alt="$P \neq \emptyset$" src="form_364.png"/>, then <img class="formulaInl" alt="$\cL = \ggen(L, \emptyset, Q_{\vect{p}} \union P)$" src="form_365.png"/> where, for some <img class="formulaInl" alt="$\vect{p} \in P$" src="form_366.png"/>, <img class="formulaInl" alt="$Q_{\vect{p}} = \{\, \vect{p} + \vect{q} \mid \vect{q} \in Q \,\}$" src="form_367.png"/>.</p>
<h3><a class="anchor" id="Grid_Minimized_Representations">
Minimized Grid Representations</a></h3>
<p>A <em>minimized</em> congruence system <img class="formulaInl" alt="$\cC$" src="form_121.png"/> for <img class="formulaInl" alt="$\cL$" src="form_338.png"/> is such that, if <img class="formulaInl" alt="$\cC'$" src="form_368.png"/> is another congruence system for <img class="formulaInl" alt="$\cL$" src="form_338.png"/>, then <img class="formulaInl" alt="$\card \cC \leq \card \cC'$" src="form_369.png"/>. Note that a minimized congruence system for a non-empty grid has at most <img class="formulaInl" alt="$n$" src="form_0.png"/> congruence relations.</p>
<p>Similarly, a <em>minimized</em> grid generator system <img class="formulaInl" alt="$\cG = (L, Q, P)$" src="form_370.png"/> for <img class="formulaInl" alt="$\cL$" src="form_338.png"/> is such that, if <img class="formulaInl" alt="$\cG' = (L', Q', P')$" src="form_371.png"/> is another grid generator system for <img class="formulaInl" alt="$\cL$" src="form_338.png"/>, then <img class="formulaInl" alt="$\card L \leq \card L'$" src="form_372.png"/> and <img class="formulaInl" alt="$\card Q + \card P \leq \card Q' + \card P'$" src="form_373.png"/>. Note that a minimized grid generator system for a grid has no more than a total of <img class="formulaInl" alt="$n+1$" src="form_178.png"/> grid lines, parameters and points.</p>
<h3><a class="anchor" id="Grids_Double_Description_Grids">
Double Description for Grids</a></h3>
<p>As for convex polyhedra, any grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> can be described by using a congruence system <img class="formulaInl" alt="$\cC$" src="form_121.png"/> for <img class="formulaInl" alt="$\cL$" src="form_338.png"/>, a grid generator system <img class="formulaInl" alt="$\cG$" src="form_127.png"/> for <img class="formulaInl" alt="$\cL$" src="form_338.png"/>, or both by means of the <em>double description pair (DD pair)</em> <img class="formulaInl" alt="$(\cC, \cG)$" src="form_128.png"/>. The <em>double description method</em> for grids is a collection of theoretical results very similar to those for convex polyhedra showing that, given one kind of representation, there are algorithms for computing a representation of the other kind and for minimizing both representations.</p>
<p>As for convex polyhedra, such changes of representation form a key step in the implementation of many operators on grids such as, for example, intersection and grid join.</p>
<h3><a class="anchor" id="Grid_Space_Dimensions">
Space Dimensions and Dimension-compatibility for Grids</a></h3>
<p>The <em>space dimension</em> of a grid <img class="formulaInl" alt="$\cL \in \Gset_n$" src="form_360.png"/> is the dimension <img class="formulaInl" alt="$n \in \Nset$" src="form_130.png"/> of the corresponding vector space <img class="formulaInl" alt="$\Rset^n$" src="form_24.png"/>. The space dimension of congruence relations, grid generators and other objects of the library is defined similarly.</p>
<h3><a class="anchor" id="Grid_Affine_Dimension">
Affine Independence and Affine Dimension for Grids</a></h3>
<p>A <em>non-empty</em> grid <img class="formulaInl" alt="$\cL \in \Gset_n$" src="form_360.png"/> has <em>affine dimension</em> <img class="formulaInl" alt="$k \in \Nset$" src="form_139.png"/>, denoted by <img class="formulaInl" alt="$\pdim(\cG) = k$" src="form_374.png"/>, if the maximum number of affinely independent points in <img class="formulaInl" alt="$\cG$" src="form_127.png"/> is <img class="formulaInl" alt="$k + 1$" src="form_141.png"/>. The affine dimension of an empty grid is defined to be 0. Thus we have <img class="formulaInl" alt="$0 \leq \pdim(\cG) \leq n$" src="form_375.png"/>.</p>
<h2><a class="anchor" id="rational_grid_operations">
Operations on Rational Grids</a></h2>
<p>In general, the operations on rational grids are the same as those for the other PPL domains and the definitions of these can be found in Section <a class="el" href="main.html#Operations_on_Convex_Polyhedra">Operations on Convex Polyhedra</a>. Below we just describe those operations that have features or behavior that is in some way special to the grid domain.</p>
<h3><a class="anchor" id="Grid_Affine_Transformation">
Affine Images and Preimages</a></h3>
<p>As for convex polyhedra (see <a class="el" href="main.html#Single_Update_Affine_Functions">Single-Update Affine Functions</a>), the library provides affine image and preimage operators for grids: given a variable <img class="formulaInl" alt="$x_k$" src="form_376.png"/> and linear expression <img class="formulaInl" alt="$\mathrm{expr} = \langle \vect{a}, \vect{x} \rangle + b$" src="form_377.png"/>, these determine the affine transformation <img class="formulaInl" alt="$\fund{\phi = \bigl(x'_k = \langle \vect{a}, \vect{x} \rangle + b\bigr)} {\Rset^n}{\Rset^n}$" src="form_231.png"/> that transforms any point <img class="formulaInl" alt="$(v_0, \ldots, v_{n-1})^\transpose$" src="form_239.png"/> in a grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> to </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \Bigl(v_0, \ldots, \bigl(\textstyle{\sum_{i=0}^{n-1}} a_i v_i + b\bigr), \ldots, v_{n-1}\Bigr)^\transpose. \]" src="form_240.png"/>
</p>
<p>The <em>affine image</em> operator computes the affine image of a grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> under <img class="formulaInl" alt="$x'_k = \langle \vect{a}, \vect{x} \rangle + b$" src="form_241.png"/>. For instance, suppose the grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> to be transformed is the non-relational grid in <img class="formulaInl" alt="$\Rset^2$" src="form_115.png"/> generated by the set of grid points <img class="formulaInl" alt="$\bigl\{ (0, 0)^\transpose, (0, 3)^\transpose, (3, 0)^\transpose \bigr\}$" src="form_378.png"/>. Then, if the considered variable is <img class="formulaInl" alt="$x_0$" src="form_243.png"/> and the linear expression is <img class="formulaInl" alt="$3x_0 + 2 x_1 + 1$" src="form_379.png"/> (so that <img class="formulaInl" alt="$k = 0$" src="form_245.png"/>, <img class="formulaInl" alt="$a_0 = 3, a_1 = 2, b = 1$" src="form_380.png"/>), the affine image operator will translate <img class="formulaInl" alt="$\cL$" src="form_338.png"/> to the grid <img class="formulaInl" alt="$\cL_1$" src="form_381.png"/> generated by the set of grid points <img class="formulaInl" alt="$\bigl\{ (1, 0)^\transpose, (7, 3)^\transpose, (10, 0)^\transpose \bigr\}$" src="form_382.png"/> which is the grid generated by the grid point <img class="formulaInl" alt="$(1, 0)$" src="form_383.png"/> and parameters <img class="formulaInl" alt="$(3, -3), (0, 9)$" src="form_384.png"/>; or, alternatively defined by the congruence system <img class="formulaInl" alt="$\{x \equiv_3 1, x + y \equiv_9 1\}$" src="form_385.png"/>. If the considered variable is as before (i.e., <img class="formulaInl" alt="$k = 0$" src="form_245.png"/>) but the linear expression is <img class="formulaInl" alt="$x_1$" src="form_249.png"/> (so that <img class="formulaInl" alt="$a_0 = 0, a_1 = 1, b = 0$" src="form_250.png"/>), then the resulting grid <img class="formulaInl" alt="$\cL_2$" src="form_386.png"/> is the grid containing all the points whose coordinates are integral multiples of 3 and lie on line <img class="formulaInl" alt="$x = y$" src="form_387.png"/>.</p>
<p>The affine preimage operator computes the affine preimage of a grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> under <img class="formulaInl" alt="$\phi$" src="form_200.png"/>. For instance, suppose now that we apply the affine preimage operator as given in the first example using variable <img class="formulaInl" alt="$x_0$" src="form_243.png"/> and linear expression <img class="formulaInl" alt="$3x_0 + 2 x_1 + 1$" src="form_379.png"/> to the grid <img class="formulaInl" alt="$\cL_1$" src="form_381.png"/>; then we get the original grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> back. If, on the other hand, we apply the affine preimage operator as given in the second example using variable <img class="formulaInl" alt="$x_0$" src="form_243.png"/> and linear expression <img class="formulaInl" alt="$x_1$" src="form_249.png"/> to <img class="formulaInl" alt="$\cL_2$" src="form_386.png"/>, then the resulting grid will consist of all the points in <img class="formulaInl" alt="$\Rset^2$" src="form_115.png"/> where the <img class="formulaInl" alt="$y$" src="form_388.png"/> coordinate is an integral multiple of 3.</p>
<p>Observe that provided the coefficient <img class="formulaInl" alt="$a_k$" src="form_252.png"/> of the considered variable in the linear expression is non-zero, the affine transformation is invertible.</p>
<h3><a class="anchor" id="Grid_Generalized_Image">
Generalized Affine Images</a></h3>
<p>Similarly to convex polyhedra (see <a class="el" href="main.html#Generalized_Affine_Relations">Generalized Affine Relations</a>), the library provides two other grid operators that are generalizations of the single update affine image and preimage operators for grids. The <em>generalized affine image</em> operator <img class="formulaInl" alt="$\fund{\phi = (\mathrm{lhs}', \mathrm{rhs}, f)}{\Rset^n}{\Rset^n}$" src="form_389.png"/>, where <img class="formulaInl" alt="$\mathrm{lhs} = \langle \vect{c}, \vect{x} \rangle + d$" src="form_258.png"/> and <img class="formulaInl" alt="$\mathrm{rhs} = \langle \vect{a}, \vect{x} \rangle + b$" src="form_259.png"/> are affine expressions and <img class="formulaInl" alt="$f \in \Qset$" src="form_390.png"/>, is defined as </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall \vect{v} \in \Rset^n, \vect{w} \in \Rset^n \itc (\vect{v}, \vect{w}) \in \phi \iff \bigl( \langle \vect{c}, \vect{w} \rangle + d \equiv_f \langle \vect{a}, \vect{v} \rangle + b \bigr) \land \Bigl( \bigland_{0 \leq i < n, c_i = 0} w_i = v_i \Bigr). \]" src="form_391.png"/>
</p>
<p> Note that, when <img class="formulaInl" alt="$\mathrm{lhs} = x_k$" src="form_262.png"/> and <img class="formulaInl" alt="$f = 0$" src="form_332.png"/>, so that the transfer function is an equality, then the above operator is equivalent to the application of the standard affine image of <img class="formulaInl" alt="$\cL$" src="form_338.png"/> with respect to the variable <img class="formulaInl" alt="$x_k$" src="form_376.png"/> and the affine expression <img class="formulaInl" alt="$\mathrm{rhs}$" src="form_265.png"/>.</p>
<h3><a class="anchor" id="Grid_Frequency">
Frequency Operator</a></h3>
<p>Let <img class="formulaInl" alt="$\cL \in \Gset_n$" src="form_360.png"/> be any non-empty grid and <img class="formulaInl" alt="$\mathrm{expr} = \bigl(\langle \vect{a}, \vect{x} \rangle + b\bigr)$" src="form_392.png"/> be a linear expression. Then if, for some <img class="formulaInl" alt="$c, f \in \Rset$" src="form_393.png"/>, all the points in <img class="formulaInl" alt="$\cL$" src="form_338.png"/> satisfy the congruence <img class="formulaInl" alt="$\cg = ( \mathrm{expr} \equiv_f c )$" src="form_394.png"/>, then the maximum <img class="formulaInl" alt="$f$" src="form_333.png"/> such that this holds is called the <em>frequency</em> of <img class="formulaInl" alt="$\cL$" src="form_338.png"/> with respect to <img class="formulaInl" alt="$\mathrm{expr}$" src="form_395.png"/>.</p>
<p>The frequency operator provided by the library returns both the frequency <img class="formulaInl" alt="$f$" src="form_333.png"/> and a value <img class="formulaInl" alt="$\mathrm{val} = \langle \vect{a}, \vect{w} \rangle + b$" src="form_396.png"/> where <img class="formulaInl" alt="$\vect{w} \in \cL$" src="form_397.png"/> and </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \lvert\mathrm{val}\rvert = \min\Bigl\{\, \bigl\lvert\langle \vect{a}, \vect{v} \rangle + b \bigr\rvert \Bigm| \vect{v} \in \cL \,\Bigr\}. \]" src="form_398.png"/>
</p>
<p>Observe that the above definition is also applied to other simple objects in the library like polyhedra, octagonal shapes, bd-shapes and boxes and in such cases the definition of frequency can be simplified. For instance, the frequency for an object <img class="formulaInl" alt="$\cP \in \Pset_n$" src="form_62.png"/> is defined if and only if there is a unique value <img class="formulaInl" alt="$c$" src="form_283.png"/> such that <img class="formulaInl" alt="$\cP$" src="form_58.png"/> saturates the equality <img class="formulaInl" alt="$( \mathrm{expr} = c )$" src="form_399.png"/>; in this case the frequency is <img class="formulaInl" alt="$0$" src="form_400.png"/> and the value returned is <img class="formulaInl" alt="$c$" src="form_283.png"/>.</p>
<h3><a class="anchor" id="Grid_Time_Elapse">
Time-Elapse Operator</a></h3>
<p>For any two grids <img class="formulaInl" alt="$\cL_1, \cL_2 \in \Gset_n$" src="form_401.png"/>, the <em>time-elapse</em> between <img class="formulaInl" alt="$\cL_1$" src="form_381.png"/> and <img class="formulaInl" alt="$\cL_2$" src="form_386.png"/>, denoted <img class="formulaInl" alt="$ \cL_1 \nearrow \cL_2$" src="form_402.png"/>, is the grid </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \bigl\{\, \vect{p} + \mu \vect{q} \in \Rset^n \bigm| \vect{p} \in \cL_1, \vect{q} \in \cL_2, \mu \in \Zset \,\bigr\}. \]" src="form_403.png"/>
</p>
<h3><a class="anchor" id="Grid_Relation_With">
Relation-with Operators</a></h3>
<p>The library provides operators for checking the relation holding between a grid and a congruence, a grid generator, a constraint or a (polyhedron) generator.</p>
<p>Suppose <img class="formulaInl" alt="$\cL$" src="form_338.png"/> is a grid and <img class="formulaInl" alt="$\cC$" src="form_121.png"/> an arbitrary congruence system representing <img class="formulaInl" alt="$\cL$" src="form_338.png"/>. Suppose also that <img class="formulaInl" alt="$ \cg = \bigl( \langle \vect{a}, \vect{x} \rangle \equiv_f b \bigr) $" src="form_404.png"/> is a congruence relation with <img class="formulaInl" alt="$\cL_{\cg} = \gcon\bigl(\{\cg\}\bigr)$" src="form_405.png"/>. The possible relations between <img class="formulaInl" alt="$\cL$" src="form_338.png"/> and <img class="formulaInl" alt="$\cg$" src="form_406.png"/> are as follows.</p>
<ul>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>is disjoint</em> from <img class="formulaInl" alt="$\cg$" src="form_406.png"/> if <img class="formulaInl" alt="$\cL \inters \cL_{\cg} = \emptyset$" src="form_407.png"/>; that is, adding <img class="formulaInl" alt="$\cg$" src="form_406.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> gives us the empty grid.</li>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>strictly intersects</em> <img class="formulaInl" alt="$\cg$" src="form_406.png"/> if <img class="formulaInl" alt="$\cL \inters \cL_{\cg} \neq \emptyset$" src="form_408.png"/> and <img class="formulaInl" alt="$\cL \inters \cL_{\cg} \subset \cL$" src="form_409.png"/>; that is, adding <img class="formulaInl" alt="$\cg$" src="form_406.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> gives us a non-empty grid strictly smaller than <img class="formulaInl" alt="$\cL$" src="form_338.png"/>.</li>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>is included</em> in <img class="formulaInl" alt="$\cg$" src="form_406.png"/> if <img class="formulaInl" alt="$\cL \sseq \cL_{\cg}$" src="form_410.png"/>; that is, adding <img class="formulaInl" alt="$\cg$" src="form_406.png"/> to <img class="formulaInl" alt="$\cC$" src="form_121.png"/> leaves <img class="formulaInl" alt="$\cL$" src="form_338.png"/> unchanged.</li>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>saturates</em> <img class="formulaInl" alt="$\cg$" src="form_406.png"/> if <img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>is included</em> in <img class="formulaInl" alt="$\cg$" src="form_406.png"/> and <img class="formulaInl" alt="$f = 0$" src="form_332.png"/>, i.e., <img class="formulaInl" alt="$\cg$" src="form_406.png"/> is an equality congruence.</li>
</ul>
<p>For the relation between <img class="formulaInl" alt="$\cL$" src="form_338.png"/> and a constraint, suppose that <img class="formulaInl" alt="$ c = \bigl( \langle \vect{a}, \vect{x} \rangle \relsym b \bigr) $" src="form_282.png"/> is a constraint with <img class="formulaInl" alt="$\mathord{\relsym} \in \{ =, \geq, > \}$" src="form_46.png"/> and <img class="formulaInl" alt="$\cQ$" src="form_146.png"/> the set of points that satisfy <img class="formulaInl" alt="$c$" src="form_283.png"/>. The possible relations between <img class="formulaInl" alt="$\cL$" src="form_338.png"/> and <img class="formulaInl" alt="$c$" src="form_283.png"/> are as follows.</p>
<ul>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>is disjoint</em> from <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cL \inters \cQ = \emptyset$" src="form_411.png"/>.</li>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>strictly intersects</em> <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cL \inters \cQ \neq \emptyset$" src="form_412.png"/> and <img class="formulaInl" alt="$\cL \inters \cQ \subset \cL$" src="form_413.png"/>.</li>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>is included</em> in <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cL \sseq \cQ$" src="form_414.png"/>.</li>
<li><img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>saturates</em> <img class="formulaInl" alt="$c$" src="form_283.png"/> if <img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>is included</em> in <img class="formulaInl" alt="$c$" src="form_283.png"/> and <img class="formulaInl" alt="$\mathord{\relsym}$" src="form_309.png"/> is <img class="formulaInl" alt="$=$" src="form_415.png"/>.</li>
</ul>
<p>A grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>subsumes</em> a grid generator <img class="formulaInl" alt="$g$" src="form_290.png"/> if adding <img class="formulaInl" alt="$g$" src="form_290.png"/> to any grid generator system representing <img class="formulaInl" alt="$\cL$" src="form_338.png"/> does not change <img class="formulaInl" alt="$\cL$" src="form_338.png"/>.</p>
<p>A grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>subsumes</em> a (polyhedron) point or closure point <img class="formulaInl" alt="$g$" src="form_290.png"/> if adding the corresponding grid point to any grid generator system representing <img class="formulaInl" alt="$\cL$" src="form_338.png"/> does not change <img class="formulaInl" alt="$\cL$" src="form_338.png"/>. A grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> <em>subsumes</em> a (polyhedron) ray or line <img class="formulaInl" alt="$g$" src="form_290.png"/> if adding the corresponding grid line to any grid generator system representing <img class="formulaInl" alt="$\cL$" src="form_338.png"/> does not change <img class="formulaInl" alt="$\cL$" src="form_338.png"/>.</p>
<h3><a class="anchor" id="Grid_Wrapping_Operator">
Wrapping Operator</a></h3>
<p>The operator <code>wrap_assign</code> provided by the library, allows for the <a class="el" href="main.html#Wrapping_Operator">wrapping</a> of a subset of the set of space dimensions so as to fit the given bounded integer type and have the specified overflow behavior. In order to maximize the precision of this operator for grids, the exact behavior differs in some respects from the other simple classes of geometric descriptors.</p>
<p>Suppose <img class="formulaInl" alt="$\cL \in \Gset_n$" src="form_360.png"/> is a grid and <img class="formulaInl" alt="$J$" src="form_416.png"/> a subset of the set of space dimensions <img class="formulaInl" alt="$\{0, \ldots, n-1\}$" src="form_417.png"/>. Suppose also that the width of the bounded integer type is <img class="formulaInl" alt="$w$" src="form_418.png"/> so that the range of values <img class="formulaInl" alt="$R = \{r \in \Rset \mid 0 \leq r < 2^w\}$" src="form_419.png"/> if the type is unsigned and <img class="formulaInl" alt="$R = \{r \in \Rset \mid -2^{w-1} \leq r < 2^{w-1}\}$" src="form_420.png"/> otherwise. Consider a space dimension <img class="formulaInl" alt="$j \in J$" src="form_185.png"/> and a variable <img class="formulaInl" alt="$v_j$" src="form_421.png"/> for dimension <img class="formulaInl" alt="$j$" src="form_422.png"/>.</p>
<p>If the value in <img class="formulaInl" alt="$\cL$" src="form_338.png"/> for the variable <img class="formulaInl" alt="$v_j$" src="form_421.png"/> is a constant in the range <img class="formulaInl" alt="$R$" src="form_106.png"/>, then it is unchanged. Otherwise the result <img class="formulaInl" alt="$\cL'$" src="form_423.png"/> of the operation on <img class="formulaInl" alt="$\cL$" src="form_338.png"/> will depend on the specified overflow behavior.</p>
<ul>
<li>Overflow impossible. In this case, it is known that no wrapping can occur. If the grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/> has no value for the variable <img class="formulaInl" alt="$v_j$" src="form_421.png"/> in the range <img class="formulaInl" alt="$R$" src="form_106.png"/>, then <img class="formulaInl" alt="$\cL$" src="form_338.png"/> is set empty. If <img class="formulaInl" alt="$v_j$" src="form_421.png"/> has exactly one value <img class="formulaInl" alt="$a \in R$" src="form_424.png"/> in <img class="formulaInl" alt="$\cL$" src="form_338.png"/>, then <img class="formulaInl" alt="$v_j$" src="form_421.png"/> is set equal to <img class="formulaInl" alt="$a$" src="form_425.png"/>. Otherwise, <img class="formulaInl" alt="$\cL' = \cL$" src="form_426.png"/>.</li>
</ul>
<ul>
<li>Overflow undefined. In this case, for each value <img class="formulaInl" alt="$a$" src="form_425.png"/> for <img class="formulaInl" alt="$v_j$" src="form_421.png"/> in the grid <img class="formulaInl" alt="$\cL$" src="form_338.png"/>, the wrapped value can be any value <img class="formulaInl" alt="$a + z \in R$" src="form_427.png"/> where <img class="formulaInl" alt="$z \in \Zset$" src="form_428.png"/>. Therefore <img class="formulaInl" alt="$\cL'$" src="form_423.png"/> is obtained by adding the parameter <img class="formulaInl" alt="$(0, \ldots, 0, v_j, 0, \ldots, 0)$" src="form_429.png"/>, where <img class="formulaInl" alt="$v_j = 1$" src="form_430.png"/>, to the generator system for <img class="formulaInl" alt="$\cL$" src="form_338.png"/>.</li>
</ul>
<ul>
<li>Overflow wraps. In this case, if <img class="formulaInl" alt="$\cL$" src="form_338.png"/> already satisfies the congruence <img class="formulaInl" alt="$v_j = a \mod 2^w$" src="form_431.png"/>, for some <img class="formulaInl" alt="$a \in \Rset$" src="form_432.png"/>, then <img class="formulaInl" alt="$v_j$" src="form_421.png"/> is set equal to <img class="formulaInl" alt="$a'$" src="form_433.png"/> where <img class="formulaInl" alt="$a' = a \mod 2^w$" src="form_434.png"/> and <img class="formulaInl" alt="$a'\in R$" src="form_435.png"/>. Otherwise, <img class="formulaInl" alt="$\cL'$" src="form_423.png"/> is obtained by adding the parameter <img class="formulaInl" alt="$(0, \ldots, 0, v_j, 0, \ldots, 0)$" src="form_429.png"/>, where <img class="formulaInl" alt="$v_j = 2^w$" src="form_436.png"/>, to the generator system for <img class="formulaInl" alt="$\cL$" src="form_338.png"/>.</li>
</ul>
<h3><a class="anchor" id="Grid_Widening">
Widening Operators</a></h3>
<p>The library provides <em>grid widening</em> operators for the domain of grids. The congruence widening and generator widening follow the specifications provided in <a class="el" href="main.html#BDHetal05">[BDHetal05]</a>. The third widening uses either the congruence or the generator widening, the exact rule governing this choice at the time of the call is left to the implementation. Note that, as for the widenings provided for convex polyhedra, all the operations provided by the library for computing a widening <img class="formulaInl" alt="$\cL_1 \widen \cL_2$" src="form_437.png"/> of grids <img class="formulaInl" alt="$\cL_1, \cL_2 \in \Gset_n$" src="form_401.png"/> require as a precondition that <img class="formulaInl" alt="$\cL_1 \sseq \cL_2$" src="form_438.png"/>.</p>
<dl class="note"><dt><b>Note:</b></dt><dd>As is the case for the other operators on grids, the implementation overwrites one of the two grid arguments with the result of the widening application. It is worth stressing that, in any widening operation that computes the widening <img class="formulaInl" alt="$\cL_1 \widen \cL_2$" src="form_437.png"/>, the resulting grid will be assigned to overwrite the store containing the bigger grid <img class="formulaInl" alt="$\cL_2$" src="form_386.png"/>. The smaller grid <img class="formulaInl" alt="$\cL_1$" src="form_381.png"/> is not modified. The same observation holds for all flavors of widenings and extrapolation operators that are implemented in the library and for all the language interfaces.</dd></dl>
<h3><a class="anchor" id="Grid_Widening_with_Tokens">
Widening with Tokens</a></h3>
<p>This is as for <a class="el" href="main.html#Widening_with_Tokens">widening with tokens</a> for convex polyhedra.</p>
<h3><a class="anchor" id="Grid_Extrapolation">
Extrapolation Operators</a></h3>
<p>Besides the widening operators, the library also implements several <em>extrapolation</em> operators, which differ from widenings in that their use along an upper iteration sequence does not ensure convergence in a finite number of steps.</p>
<p>In particular, for each grid widening that is provided, there is a corresponding <em>limited</em> extrapolation operator, which can be used to implement the <em>widening ``up to''</em> technique as described in <a class="el" href="main.html#HPR97">[HPR97]</a>. Each limited extrapolation operator takes a congruence system as an additional parameter and uses it to improve the approximation yielded by the corresponding widening operator. Note that, as in the case for convex polyhedra, a convergence guarantee can only be obtained by suitably restricting the set of congruence relations that can occur in this additional parameter.</p>
<h2><a class="anchor" id="powerset">
The Powerset Construction</a></h2>
<p>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 <em>finite</em> number of disjuncts). The construction follows the approach described in <a class="el" href="main.html#Bag98">[Bag98]</a>, also summarized in <a class="el" href="main.html#BHZ04">[BHZ04]</a> where there is an account of generic widenings for the powerset domain (some of which are supported in the pointset powerset domain instantiation of this construction described in Section <a class="el" href="main.html#pointset_powerset">The Pointset Powerset Domain</a>).</p>
<p><a class="anchor" id="powerset_domain"></a> </p>
<h3><a class="anchor" id="The_Powerset_Domain">
The Powerset Domain</a></h3>
<p>The domain is built from a pre-existing base-level domain <img class="formulaInl" alt="$D$" src="form_439.png"/> which must include an entailment relation `<img class="formulaInl" alt="$\mathord{\entails}$" src="form_440.png"/>', meet operation `<img class="formulaInl" alt="$\mathord{\meet}$" src="form_441.png"/>', a top element `<img class="formulaInl" alt="$\true$" src="form_442.png"/>' and bottom element `<img class="formulaInl" alt="$\false$" src="form_443.png"/>'.</p>
<p>A set <img class="formulaInl" alt="$\cS \in \wp(D)$" src="form_444.png"/> is called <em>non-redundant</em> with respect to `<img class="formulaInl" alt="$\mathord{\entails}$" src="form_440.png"/>' if and only if <img class="formulaInl" alt="$\false \notin \cS$" src="form_445.png"/> and <img class="formulaInl" alt="$\forall d_1, d_2 \in \cS \itc d_1 \entails d_2 \implies d_1 = d_2$" src="form_446.png"/>. The set of finite non-redundant subsets of <img class="formulaInl" alt="$D$" src="form_439.png"/> (with respect to `<img class="formulaInl" alt="$\mathord{\entails}$" src="form_440.png"/>') is denoted by <img class="formulaInl" alt="$\wpfn{D}{\entails}$" src="form_447.png"/>. The function <img class="formulaInl" alt="$\fund{\nonredmap}{\wpf(D)}{\wpfn{D}{\entails}}$" src="form_448.png"/>, called <em>Omega-reduction</em>, maps a finite set into its non-redundant counterpart; it is defined, for each <img class="formulaInl" alt="$\cS \in \wpf(D)$" src="form_449.png"/>, by </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \nonredmap(\cS) \defeq \cS \setdiff \{\, d \in \cS \mid d = \false \text{ or } \exists d' \in \cS \st d \sentails d' \,\}. \]" src="form_450.png"/>
</p>
<p> where <img class="formulaInl" alt="$d \sentails d'$" src="form_451.png"/> denotes <img class="formulaInl" alt="$d \entails d' \land d \ne d'$" src="form_452.png"/>.</p>
<p>As the intended semantics of a powerset domain element <img class="formulaInl" alt="$\cS \in \wpf(D)$" src="form_449.png"/> is that of disjunction of the semantics of <img class="formulaInl" alt="$D$" src="form_439.png"/>, the finite set <img class="formulaInl" alt="$\cS$" src="form_453.png"/> is semantically equivalent to the non-redundant set <img class="formulaInl" alt="$\nonredmap(\cS)$" src="form_454.png"/>; and elements of <img class="formulaInl" alt="$\cS$" src="form_453.png"/> will be called <em>disjuncts</em>. The restriction to the finite subsets reflects the fact that here disjunctions are implemented by explicit collections of disjuncts. As a consequence of this restriction, for any <img class="formulaInl" alt="$\cS \in \wpf(D)$" src="form_449.png"/> such that <img class="formulaInl" alt="$\cS \neq \{ \false \}$" src="form_455.png"/>, <img class="formulaInl" alt="$\nonredmap(\cS)$" src="form_454.png"/> is the (finite) set of the maximal elements of <img class="formulaInl" alt="$\cS$" src="form_453.png"/>.</p>
<p>The <em>finite powerset domain</em> over a domain <img class="formulaInl" alt="$D$" src="form_439.png"/> is the set of all finite non-redundant sets of <img class="formulaInl" alt="$D$" src="form_439.png"/> and denoted by <img class="formulaInl" alt="$D_{\smallP}$" src="form_456.png"/>. The domain includes an approximation ordering `<img class="formulaInl" alt="$\mathord{\entailsP}$" src="form_457.png"/>' defined so that, for any <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> and <img class="formulaInl" alt="$\cS_2 \in D_{\smallP}$" src="form_459.png"/>, <img class="formulaInl" alt="$\cS_1 \entailsP \cS_2$" src="form_460.png"/> if and only if </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \forall d_1 \in \cS_1 \itc \exists d_2 \in \cS_2 \st d_1 \entails d_2. \]" src="form_461.png"/>
</p>
<p> Therefore the top element is <img class="formulaInl" alt="$\{\true\}$" src="form_462.png"/> and the bottom element is the emptyset.</p>
<dl class="note"><dt><b>Note:</b></dt><dd>As far as Omega-reduction is concerned, the library adopts a <em>lazy</em> approach: an element of the powerset domain is represented by a potentially redundant sequence of disjuncts. Redundancies can be eliminated by explicitly invoking the operator <code>omega_reduce()</code>, e.g., before performing the output of a powerset element. Note that all the documented operators automatically perform Omega-reductions on their arguments, when needed or appropriate.</dd></dl>
<h2><a class="anchor" id="ps_operations">
Operations on the Powerset Construction</a></h2>
<p>In this section we briefly describe the generic operations on Powerset Domains that are provided by the library for any given base-level domain <img class="formulaInl" alt="$D$" src="form_439.png"/>.</p>
<p><a class="anchor" id="ps_meet_upper_bound"></a> </p>
<h3><a class="anchor" id="Meet_and_Upper_Bound">
Meet and Upper Bound</a></h3>
<p>Given the sets <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> and <img class="formulaInl" alt="$\cS_2 \in D_{\smallP}$" src="form_459.png"/>, the <em>meet</em> and <em>upper bound</em> operators provided by the library returns the set <img class="formulaInl" alt="$ \nonredmap \bigl( \{\, d_1 \meet d_2 \mid d_1 \in \cS_1, d_2 \in \cS_2 \,\} \bigr) $" src="form_463.png"/> and Omega-reduced set union <img class="formulaInl" alt="$\nonredmap(\cS_1 \union \cS_2)$" src="form_464.png"/> respectively.</p>
<p><a class="anchor" id="ps_add_disjunct"></a> </p>
<h3><a class="anchor" id="Adding_a_Disjunct">
Adding a Disjunct</a></h3>
<p>Given the powerset element <img class="formulaInl" alt="$\cS \in D_{\smallP}$" src="form_465.png"/> and the base-level element <img class="formulaInl" alt="$d \in D$" src="form_466.png"/>, the <em>add disjunct</em> operator provided by the library returns the powerset element <img class="formulaInl" alt="$\nonredmap\bigl(\cS \union \{d\}\bigr)$" src="form_467.png"/>.</p>
<p><a class="anchor" id="ps_collapse"></a> </p>
<h3><a class="anchor" id="Collapsing_a_Powerset_Element">
Collapsing a Powerset Element</a></h3>
<p>If the given powerset element is not empty, then the <em>collapse</em> operator returns the singleton powerset consisting of an upper-bound of all the disjuncts.</p>
<h2><a class="anchor" id="pointset_powerset">
The Pointset Powerset Domain</a></h2>
<p>The pointset powerset domain provided by the PPL is the finite powerset domain (defined in Section <a class="el" href="main.html#powerset">The Powerset Construction</a>) whose base-level domain <img class="formulaInl" alt="$D$" src="form_439.png"/> is one of the classes of semantic geometric descriptors listed in Section <a class="el" href="main.html#Semantic_Geometric_Descriptors">Semantic Geometric Descriptors</a>.</p>
<p>In addition to the operations described for the generic powerset domain in Section <a class="el" href="main.html#ps_operations">Operations on the Powerset Construction</a>, the PPL provides all the generic operations listed in <a class="el" href="main.html#Generic_Operations_on_Semantic_Geometric_Descriptors">Generic Operations on Semantic Geometric Descriptors</a>. Here we just describe those operations that are particular to the pointset powerset domain.</p>
<h3><a class="anchor" id="Powerset_Meet_Preserving_Simplification">
Meet-Preserving Simplification</a></h3>
<p>Let <img class="formulaInl" alt="$\cS_1 = \{ d_1, \ldots, d_m \}$" src="form_468.png"/>, <img class="formulaInl" alt="$\cS_2 = \{ c_1, \ldots, c_n \}$" src="form_469.png"/> and <img class="formulaInl" alt="$\cS = \{ s_1, \ldots, s_q \}$" src="form_470.png"/> be Omega-reduced elements of a pointset powerset domain over the same base-level domain. Then:</p>
<ul>
<li><img class="formulaInl" alt="$\cS$" src="form_453.png"/> is <em>powerset meet-preserving</em> with respect to <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> using context <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/> if the meet of <img class="formulaInl" alt="$\cS$" src="form_453.png"/> and <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/> is equal to the meet of <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> and <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/>;</li>
</ul>
<ul>
<li><img class="formulaInl" alt="$\cS$" src="form_453.png"/> is a <em>powerset simplification</em> with respect to <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> if <img class="formulaInl" alt="$q \leq m$" src="form_472.png"/>.</li>
</ul>
<ul>
<li><img class="formulaInl" alt="$\cS$" src="form_453.png"/> is a <em>disjunct meet-preserving simplification</em> with respect to <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> if, for each <img class="formulaInl" alt="$s_k \in \cS$" src="form_473.png"/>, there exists <img class="formulaInl" alt="$d_i \in \cS_1$" src="form_474.png"/> such that, for each <img class="formulaInl" alt="$c_j \in \cS_2$" src="form_475.png"/>, <img class="formulaInl" alt="$s_k$" src="form_476.png"/> is a meet-preserving enlargement and simplification of <img class="formulaInl" alt="$d_i$" src="form_477.png"/> using context <img class="formulaInl" alt="$c_j$" src="form_478.png"/>.</li>
</ul>
<p>The library provides a binary operator (<code>simplify_using_context</code>) for the pointset powerset domain that returns a powerset which is a powerset meet-preserving, powerset simplification and disjunct meet-preserving simplification of its first argument using the second argument as context.</p>
<p>Notice that, due to the powerset simplification property, in general a meet-preserving powerset simplification is <em>not</em> an enlargement with respect to the ordering defined on the powerset lattice. Because of this, the operator provided by the library is only well-defined when the base-level domain is not itself a powerset domain.</p>
<p><a class="anchor" id="pps_geometric"></a> </p>
<h3><a class="anchor" id="Geometric_Comparisons">
Geometric Comparisons</a></h3>
<p>Given the pointset powersets <img class="formulaInl" alt="$\cS_1, \cS_2$" src="form_479.png"/> over the same base-level domain and with the same space dimension, then we say that <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> <em>geometrically covers</em> <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/> if every point (in some disjunct) of <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/> is also a point in a disjunct of <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/>. If <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/> geometrically covers <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/> and <img class="formulaInl" alt="$\cS_2$" src="form_471.png"/> geometrically covers <img class="formulaInl" alt="$\cS_1$" src="form_458.png"/>, then we say that they are <em>geometrically equal</em>.</p>
<p><a class="anchor" id="pps_pairwise_merge"></a> </p>
<h3><a class="anchor" id="Pairwise_Merge">
Pairwise Merge</a></h3>
<p>Given the pointset powerset <img class="formulaInl" alt="$\cS$" src="form_453.png"/> over a base-level semantic GD domain <img class="formulaInl" alt="$D$" src="form_439.png"/>, then the <em>pairwise merge</em> operator takes pairs of distinct elements in <img class="formulaInl" alt="$\cS$" src="form_453.png"/> whose upper bound (denoted here by <img class="formulaInl" alt="$\uplus$" src="form_480.png"/>) in <img class="formulaInl" alt="$D$" src="form_439.png"/> (using the PPL operator <code>upper_bound_assign()</code> for <img class="formulaInl" alt="$D$" src="form_439.png"/>) is the same as their set-theoretical union and replaces them by their union. This replacement is done recursively so that, for each pair <img class="formulaInl" alt="$c, d$" src="form_481.png"/> of distinct disjuncts in the result set, we have <img class="formulaInl" alt="$c \uplus d \neq c \union d$" src="form_482.png"/>.</p>
<p><a class="anchor" id="pps_bgp99_extrapolation"></a> </p>
<h3><a class="anchor" id="Powerset_Extrapolation_Operators">
Powerset Extrapolation Operators</a></h3>
<p>The library implements a generalization of the extrapolation operator for powerset domains proposed in <a class="el" href="main.html#BGP99">[BGP99]</a>. The operator <code>BGP99_extrapolation_assign</code> is made parametric by allowing for the specification of any PPL extrapolation operator for the base-level domain. Note that, even when the extrapolation operator for the base-level domain <img class="formulaInl" alt="$D$" src="form_439.png"/> is known to be a widening on <img class="formulaInl" alt="$D$" src="form_439.png"/>, the <code>BGP99_extrapolation_assign</code> operator cannot guarantee the convergence of the iteration sequence in a finite number of steps (for a counter-example, see <a class="el" href="main.html#BHZ04">[BHZ04]</a>).</p>
<p><a class="anchor" id="pps_certificate_widening"></a> </p>
<h3><a class="anchor" id="Certificate_Based_Widenings">
Certificate-Based Widenings</a></h3>
<p>The PPL library provides support for the specification of proper widening operators on the pointset powerset domain. In particular, this version of the library implements an instance of the <em>certificate-based widening framework</em> proposed in <a class="el" href="main.html#BHZ03b">[BHZ03b]</a>.</p>
<p>A <em>finite convergence certificate</em> 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 <img class="formulaInl" alt="$D$" src="form_439.png"/>, together with the corresponding convergence certificate, the BHZ03 framework is able to lift this widening on <img class="formulaInl" alt="$D$" src="form_439.png"/> to a widening on the pointset powerset domain; ensuring convergence in a finite number of iterations.</p>
<p>Being highly parametric, the BHZ03 widening framework can be instantiated in many ways. The current implementation provides the templatic operator <code>BHZ03_widening_assign<Certificate, Widening></code> 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 upper bound operator for the base-level domain is tried; second, the <a class="el" href="main.html#pps_bgp99_extrapolation">BGP99 extrapolation operator</a> is tried, possibly applying <a class="el" href="main.html#pps_pairwise_merge">pairwise merging</a>. If both heuristics fail to converge according to the convergence certificate, then an attempt is made to apply the base-level widening to the upper bound of the two arguments, possibly improving the result obtained by means of the difference operator for the base-level domain. For more details and a justification of the overall approach, see <a class="el" href="main.html#BHZ03b">[BHZ03b]</a> and <a class="el" href="main.html#BHZ04">[BHZ04]</a>.</p>
<p>The library provides several convergence certificates. Note that, for the domain of Polyhedra, while <a class="el" href="classParma__Polyhedra__Library_1_1BHRZ03__Certificate.html">Parma_Polyhedra_Library::BHRZ03_Certificate</a> the "BHRZ03_Certificate" is compatible with both the BHRZ03 and the H79 widenings, <a class="el" href="classParma__Polyhedra__Library_1_1H79__Certificate.html">H79_Certificate</a> 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.</p>
<h2><a class="anchor" id="use_of_library">
Using the Library</a></h2>
<h3><a class="anchor" id="A_Note_on_the_Implementation_of_the_Operators">
A Note on the Implementation of the Operators</a></h3>
<p>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.</p>
<p>In earlier versions of the library, a number of operators were introduced in two flavors: a <em>lazy</em> version and an <em>eager</em> version, the latter having the operator name ending with <code>_and_minimize</code>. In principle, only the lazy versions should be used. The eager versions were added to help a knowledgeable 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.</p>
<p>One of the cases when an eager computation might still make sense is when the well-known <em>fail-first</em> 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 emptiness check. Note anyway that the same effect can be obtained by interleaving the calls of the lazy operator with explicit emptiness checks.</p>
<dl class="warning"><dt><b>Warning:</b></dt><dd>For the reasons mentioned above, starting from version 0.10 of the library, the usage of the eager versions (i.e., the ones having a name ending with <code>_and_minimize</code>) of these operators is <em>deprecated</em>; this is in preparation of their complete removal, which will occur starting from version 0.11.</dd></dl>
<h3><a class="anchor" id="On_Pointset_Powerset_and_Partially_Reduced_Product_Domains_A_Warning">
On Pointset_Powerset and Partially_Reduced_Product Domains: A Warning</a></h3>
<p>For future versions of the PPL library all practical instantiations for the disjuncts for a pointset_powerset and component domains for the partially_reduced_product domains will be fully supported. However, for version 0.10, these compound domains should not themselves occur as one of their argument domains. Therefore their use comes with the following warning.</p>
<dl class="warning"><dt><b>Warning:</b></dt><dd>The <code>Pointset_Powerset<PSET></code> and <code>Partially_Reduced_Product<D1, D2, R></code> should only be used with the following instantiations for the disjunct domain template <code>PSET</code> and component domain templates <code>D1</code> and <code>D2:</code> <code>C_Polyhedron</code>, <code>NNC_Polyhedron</code>, <code>Grid</code>, <code>Octagonal_Shape<T></code>, <code>BD_Shape<T></code>, <code>Box<T></code>.</dd></dl>
<h3><a class="anchor" id="On_Object_Orientation_and_Polymorphism_A_Disclaimer">
On Object-Orientation and Polymorphism: A Disclaimer</a></h3>
<p>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 <code>virtual</code>). In practice, this restriction means that the library types should not be used as <em>public base classes</em> to be derived from. A user willing to extend the library types, adding new functionalities, often can do so by using <em>containment</em> instead of inheritance; even when there is the need to override a <code>protected</code> method, non-public inheritance should suffice.</p>
<h3><a class="anchor" id="On_Const_Correctness_A_Warning_about_the_Use_of_References_and_Iterators">
On Const-Correctness: A Warning about the Use of References and Iterators</a></h3>
<p>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: </p>
<div class="fragment"><pre class="fragment"><span class="comment">// Find a reference to the first point of the non-empty polyhedron `ph'.</span>
<span class="keyword">const</span> Generator_System& gs = ph.generators();
Generator_System::const_iterator i = gs.begin();
<span class="keywordflow">for</span> (Generator_System::const_iterator gs_end = gs.end(); i != gs_end; ++i)
<span class="keywordflow">if</span> (i->is_point())
<span class="keywordflow">break</span>;
<span class="keyword">const</span> Generator& p = *i;
<span class="comment">// Get the constraints of `ph'.</span>
<span class="keyword">const</span> Constraint_System& cs = ph.constraints();
<span class="comment">// Both the const iterator `i' and the reference `p'</span>
<span class="comment">// are no longer valid at this point.</span>
cout << p.divisor() << endl; <span class="comment">// Undefined behavior!</span>
++i; <span class="comment">// Undefined behavior!</span>
</pre></div><p> 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 <code>i</code> and the reference <code>p</code>. 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: </p>
<div class="fragment"><pre class="fragment">Generator_System gs = ph.generators();
</pre></div><p> The same observations, modulo syntactic sugar, apply to the operators defined in the C interface of the library.</p>
<h2><a class="anchor" id="bibliography">
Bibliography</a></h2>
<dl>
<dt>[Anc91] </dt>
<dd><p class="startdd"><a class="anchor" id="Anc91"></a> C. Ancourt. <em>Génération automatique de codes de transfert pour multiprocesseurs à mémoires locales</em>. PhD thesis, Université de Paris VI, Paris, France, March 1991.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BA05] </dt>
<dd><p class="startdd"><a class="anchor" id="BA05"></a> J. M. Bjorndalen and O. Anshus. Lessons learned in benchmarking - Floating point benchmarks: Can you trust them? In <em>Proceedings of the <em>Norsk informatikkonferanse 2005</em> (NIK 2005)</em>, pages 89-100, Bergen, Norway, 2005. Tapir Akademisk Forlag.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Bag97] </dt>
<dd><p class="startdd"><a class="anchor" id="Bag97"></a> R. Bagnara. <em>Data-Flow Analysis for Constraint Logic-Based Languages</em>. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, March 1997. Printed as Report TD-1/97.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Bag98] </dt>
<dd><p class="startdd"><a class="anchor" id="Bag98"></a> R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. <em>Science of Computer Programming</em>, 30(1-2):119-155, 1998.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BCC<sup>+</sup>02] </dt>
<dd><p class="startdd"><a class="anchor" id="BCCetal02"></a> B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In T. Æ. Mogensen, D. A. Schmidt, and I. Hal Sudborough, editors, <em>The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday]</em>, volume 2566 of <em>Lecture Notes in Computer Science</em>, pages 85-108. Springer-Verlag, Berlin, 2002.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BDH<sup>+</sup>05] </dt>
<dd><p class="startdd"><a class="anchor" id="BDHetal05"></a> R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, and E. Zaffanella. A linear domain for analyzing the distribution of numerical values. Report 2005.06, School of Computing, University of Leeds, UK, 2005. Available at <a href="http://www.comp.leeds.ac.uk/research/pubs/reports.shtml">http://www.comp.leeds.ac.uk/research/pubs/reports.shtml</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BDH<sup>+</sup>06] </dt>
<dd><p class="startdd"><a class="anchor" id="BDHetal06"></a> R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, and E. Zaffanella. A practical tool for analyzing the distribution of numerical values, 2006. Available at <a href="http://www.comp.leeds.ac.uk/hill/Papers/papers.html">http://www.comp.leeds.ac.uk/hill/Papers/papers.html</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BDH<sup>+</sup>07] </dt>
<dd><p class="startdd"><a class="anchor" id="BDHetal07"></a> R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, and E. Zaffanella. Grids: A domain for analyzing the distribution of numerical values. In G. Puebla, editor, <em>Logic-based Program Synthesis and Transformation, 16th International Symposium</em>, volume 4407 of <em>Lecture Notes in Computer Science</em>, pages 219-235, Venice, Italy, 2007. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BFT00] </dt>
<dd><p class="startdd"><a class="anchor" id="BFT00"></a> A. Bemporad, K. Fukuda, and F. D. Torrisi. Convexity recognition of the union of polyhedra. Report AUT00-13, Automatic Control Laboratory, ETHZ, Zurich, Switzerland, 2000.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BFT01] </dt>
<dd><p class="startdd"><a class="anchor" id="BFT01"></a> A. Bemporad, K. Fukuda, and F. D. Torrisi. Convexity recognition of the union of polyhedra. <em>Computational Geometry: Theory and Applications</em>, 18(3):141-154, 2001.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BGP99] </dt>
<dd><p class="startdd"><a class="anchor" id="BGP99"></a> T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. <em>ACM Transactions on Programming Languages and Systems</em>, 21(4):747-789, 1999.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHMZ04] </dt>
<dd><p class="startdd"><a class="anchor" id="BHMZ04"></a> R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Widening operators for weakly-relational numeric abstractions. Report <code>arXiv:cs.PL/0412043</code>, 2004. Extended abstract. Contribution to the <em>International workshop on “Numerical & Symbolic Abstract Domains”</em> (NSAD'05, Paris, January 21, 2005). Available at <a href="http://arxiv.org/">http://arxiv.org/</a> and <a href="http://www.cs.unipr.it/ppl/">http://www.cs.unipr.it/ppl/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHMZ05a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHMZ05a"></a> R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Università di Parma, Italy, 2005. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHMZ05b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHMZ05b"></a> R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Widening operators for weakly-relational numeric abstractions. In C. Hankin and I. Siveroni, editors, <em>Static Analysis: Proceedings of the 12th International Symposium</em>, volume 3672 of <em>Lecture Notes in Computer Science</em>, pages 3-18, London, UK, 2005. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHRZ03a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHRZ03a"></a> R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, <em>Static Analysis: Proceedings of the 10th International Symposium</em>, volume 2694 of <em>Lecture Notes in Computer Science</em>, pages 337-354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHRZ03b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHRZ03b"></a> 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 <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHRZ05] </dt>
<dd><p class="startdd"><a class="anchor" id="BHRZ05"></a> R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. <em>Science of Computer Programming</em>, 58(1-2):28-56, 2005.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ02a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ02a"></a> 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 <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ02b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ02b"></a> 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, <em>Proceedings of the 1st CoLogNet Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems</em>, pages 147-153, Madrid, Spain, 2002. Published as TR Number CLIP4/02.0, Universidad Politécnica de Madrid, Facultad de Informática.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ03a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ03a"></a> 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, <em> Proceedings of the 3rd Workshop on Automated Verification of Critical Systems</em>, pages 161-176, Southampton, UK, 2003. Published as TR Number DSSE-TR-2003-2, University of Southampton.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ03b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ03b"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. In B. Steffen and G. Levi, editors, <em>Verification, Model Checking and Abstract Interpretation: Proceedings of the 5th International Conference (VMCAI 2004)</em>, volume 2937 of <em>Lecture Notes in Computer Science</em>, pages 135-148, Venice, Italy, 2003. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ04] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ04"></a> 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 <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ05] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ05"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Not necessarily closed convex polyhedra and the double description method. <em>Formal Aspects of Computing</em>, 17(2):222-257, 2005.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ06a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ06a"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Quaderno 457, Dipartimento di Matematica, Università di Parma, Italy, 2006. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. Also published as <code>arXiv:cs.MS/0612085</code>, available from <a href="http://arxiv.org/">http://arxiv.org/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ06b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ06b"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. <em>Software Tools for Technology Transfer</em>, 8(4/5):449-466, 2006. In the printed version of this article, all the figures have been improperly printed (rendering them useless). See <a class="el" href="main.html#BHZ07c">[BHZ07c]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ07a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ07a"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Applications of polyhedral computations to the analysis and verification of hardware and software systems. Quaderno 458, Dipartimento di Matematica, Università di Parma, Italy, 2007. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. Also published as <code>arXiv:cs.CG/0701122</code>, available from <a href="http://arxiv.org/">http://arxiv.org/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ07b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ07b"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. An improved tight closure algorithm for integer octagonal constraints. Quaderno 467, Dipartimento di Matematica, Università di Parma, Italy, 2007. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. Also published as <code>arXiv:0705.4618v2 [cs.DS]</code>, available from <a href="http://arxiv.org/">http://arxiv.org/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ07c] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ07c"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. <em>Software Tools for Technology Transfer</em>, 9(3/4):413-414, 2007. Erratum to <a class="el" href="main.html#BHZ06b">[BHZ06b]</a> containing all the figures properly printed.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ08a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ08a"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. An improved tight closure algorithm for integer octagonal constraints. In F. Logozzo, D. Peled, and L. Zuck, editors, <em>Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008)</em>, volume 4905 of <em>Lecture Notes in Computer Science</em>, pages 8-21, San Francisco, USA, 2008. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ08b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ08b"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. <em>Science of Computer Programming</em>, 72(1-2):3-21, 2008.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ09a] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ09a"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Applications of polyhedral computations to the analysis and verification of hardware and software systems. <em>Theoretical Computer Science</em>, 410(46):4672-4691, 2009.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ09b] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ09b"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Exact join detection for convex polyhedra and other numerical abstractions. Quaderno 492, Dipartimento di Matematica, Università di Parma, Italy, 2009. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. A corrected and improved version (corrected an error in the statement of condition (3) of Theorem 3.6, typos corrected in statement and proof of Theorem 6.8) has been published in <a class="el" href="main.html#BHZ09c">[BHZ09c]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ09c] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ09c"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Exact join detection for convex polyhedra and other numerical abstractions. Report <code>arXiv:cs.CG/0904.1783</code>, 2009. Available at <a href="http://arxiv.org/">http://arxiv.org/</a> and <a href="http://www.cs.unipr.it/ppl/">http://www.cs.unipr.it/ppl/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ09d] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ09d"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. <em>Formal Methods in System Design</em>, 35(3):279-323, 2009.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BHZ10] </dt>
<dd><p class="startdd"><a class="anchor" id="BHZ10"></a> R. Bagnara, P. M. Hill, and E. Zaffanella. Exact join detection for convex polyhedra and other numerical abstractions. <em>Computational Geometry: Theory and Applications</em>, 43(5):453-473, 2010. To appear in print. Available online at <a href="http://dx.doi.org/10.1016/j.comgeo.2009.09.002">http://dx.doi.org/10.1016/j.comgeo.2009.09.002</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BJT99] </dt>
<dd><p class="startdd"><a class="anchor" id="BJT99"></a> F. Besson, T. P. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In A. Cortesi and G. Filé, editors, <em>Static Analysis: Proceedings of the 6th International Symposium</em>, volume 1694 of <em>Lecture Notes in Computer Science</em>, pages 51-68, Venice, Italy, 1999. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BK89] </dt>
<dd><p class="startdd"><a class="anchor" id="BK89"></a> V. Balasundaram and K. Kennedy. A technique for summarizing data access and its use in parallelism enhancing transformations. In B. Knobe, editor, <em>Proceedings of the ACM SIGPLAN'89 Conference on Programming Language Design and Implementation (PLDI)</em>, volume 24(7) of <em>ACM SIGPLAN Notices</em>, pages 41-53, Portland, Oregon, USA, 1989. ACM Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BMPZ10] </dt>
<dd><p class="startdd"><a class="anchor" id="BMPZ10"></a> R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. The automatic synthesis of linear ranking functions: The complete unabridged version. Quaderno 498, Dipartimento di Matematica, Università di Parma, Italy, 2010. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. Also published as <code>arXiv:cs.PL/1004.0944</code>, available from <a href="http://arxiv.org/">http://arxiv.org/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BRZH02a] </dt>
<dd><p class="startdd"><a class="anchor" id="BRZH02a"></a> 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, <em>Static Analysis: Proceedings of the 9th International Symposium</em>, volume 2477 of <em>Lecture Notes in Computer Science</em>, pages 213-229, Madrid, Spain, 2002. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BRZH02b] </dt>
<dd><p class="startdd"><a class="anchor" id="BRZH02b"></a> 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 <a class="el" href="main.html#BRZH02c">[BRZH02c]</a>. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[BRZH02c] </dt>
<dd><p class="startdd"><a class="anchor" id="BRZH02c"></a> R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Errata for technical report “Quaderno 286”. Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>, 2002. See <a class="el" href="main.html#BRZH02b">[BRZH02b]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[CC76] </dt>
<dd><p class="startdd"><a class="anchor" id="CC76"></a> P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In B. Robinet, editor, <em>Proceedings of the Second International Symposium on Programming</em>, pages 106-130, Paris, France, 1976. Dunod, Paris, France.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[CC79] </dt>
<dd><p class="startdd"><a class="anchor" id="CC79"></a> P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In <em>Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages</em>, pages 269-282, New York, 1979. ACM Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[CC92] </dt>
<dd><p class="startdd"><a class="anchor" id="CC92"></a> P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, <em>Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming</em>, volume 631 of <em>Lecture Notes in Computer Science</em>, pages 269-295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[CH78] </dt>
<dd><p class="startdd"><a class="anchor" id="CH78"></a> P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In <em>Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages</em>, pages 84-96, Tucson, Arizona, 1978. ACM Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Che64] </dt>
<dd><p class="startdd"><a class="anchor" id="Che64"></a> N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear equations. <em>U.S.S.R. Computational Mathematics and Mathematical Physics</em>, 4(4):151-158, 1964.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Che65] </dt>
<dd><p class="startdd"><a class="anchor" id="Che65"></a> N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. <em>U.S.S.R. Computational Mathematics and Mathematical Physics</em>, 5(2):228-233, 1965.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Che68] </dt>
<dd><p class="startdd"><a class="anchor" id="Che68"></a> N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. <em>U.S.S.R. Computational Mathematics and Mathematical Physics</em>, 8(6):282-293, 1968.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Dan63] </dt>
<dd><p class="startdd"><a class="anchor" id="Dan63"></a> G. B. Dantzig. <em>Linear Programming and Extensions</em>. Princeton University Press, Princeton, NJ, 1963.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[FCB07] </dt>
<dd><p class="startdd"><a class="anchor" id="FCB07"></a> P. Feautrier, J.-F. Collard, and C. Bastoul. <em>PIP/PipLib: A Solver for Parametric Integer Programming Problems</em>, 5.0 edition, July 2007. Distributed with PIP/PipLib 1.4.0.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Fea88] </dt>
<dd><p class="startdd"><a class="anchor" id="Fea88"></a> P. Feautrier. Parametric integer programming. <em>RAIRO Recherche Opérationnelle</em>, 22(3):243-268, 1988.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[FP96] </dt>
<dd><p class="startdd"><a class="anchor" id="FP96"></a> K. Fukuda and A. Prodon. Double description method revisited. In M. Deza, R. Euler, and Y. Manoussakis, editors, <em>Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5, 1995, Selected Papers</em>, volume 1120 of <em>Lecture Notes in Computer Science</em>, pages 91-111. Springer-Verlag, Berlin, 1996.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Fuk98] </dt>
<dd><p class="startdd"><a class="anchor" id="Fuk98"></a> K. Fukuda. Polyhedral computation FAQ. Swiss Federal Institute of Technology, Lausanne and Zurich, Switzerland, available at <a href="http://www.ifor.math.ethz.ch/~fukuda/polyfaq/polyfaq.html">http://www.ifor.math.ethz.ch/~fukuda/polyfaq/polyfaq.html</a>, 1998.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[GDD<sup>+</sup>04] </dt>
<dd><p class="startdd"><a class="anchor" id="GDDetal04"></a> D. Gopan, F. DiMaio, N. Dor, T. W. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In K. Jensen and A. Podelski, editors, <em>Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004</em>, volume 2988 of <em>Lecture Notes in Computer Science</em>, pages 512-529, Barcelona, Spain, 2004. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[GJ00] </dt>
<dd><p class="startdd"><a class="anchor" id="GJ00"></a> E. Gawrilow and M. Joswig. <code>polymake</code>: A framework for analyzing convex polytopes. In G. Kalai and G. M. Ziegler, editors, <em>Polytopes - Combinatorics and Computation</em>, pages 43-74. Birkhäuser, 2000.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[GJ01] </dt>
<dd><p class="startdd"><a class="anchor" id="GJ01"></a> E. Gawrilow and M. Joswig. <code>polymake</code>: An approach to modular software design in computational geometry. In <em>Proceedings of the 17th Annual Symposium on Computational Geometry</em>, pages 222-231, Medford, MA, USA, 2001. ACM.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[GR77] </dt>
<dd><p class="startdd"><a class="anchor" id="GR77"></a> D. Goldfarb and J. K. Reid. A practical steepest-edge simplex algorithm. <em>Mathematical Proramming</em>, 12(1):361-371, 1977.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Gra91] </dt>
<dd><p class="startdd"><a class="anchor" id="Gra91"></a> P. Granger. Static analysis of linear congruence equalities among variables of a program. In S. Abramsky and T. S. E. Maibaum, editors, <em>TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91)</em>, volume 493 of <em>Lecture Notes in Computer Science</em>, pages 169-192, Brighton, UK, 1991. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Gra97] </dt>
<dd><p class="startdd"><a class="anchor" id="Gra97"></a> P. Granger. Static analyses of congruence properties on rational numbers (extended abstract). In P. Van Hentenryck, editor, <em>Static Analysis: Proceedings of the 4th International Symposium</em>, volume 1302 of <em>Lecture Notes in Computer Science</em>, pages 278-292, Paris, France, 1997. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Hal79] </dt>
<dd><p class="startdd"><a class="anchor" id="Hal79"></a> N. Halbwachs. <em>Détermination Automatique de Relations Linéaires Vérifiées par les Variables d'un Programme</em>. Thèse de 3ème cycle d'informatique, Université scientifique et médicale de Grenoble, Grenoble, France, March 1979.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Hal93] </dt>
<dd><p class="startdd"><a class="anchor" id="Hal93"></a> N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, <em>Computer Aided Verification: Proceedings of the 5th International Conference (CAV'93)</em>, volume 697 of <em> Lecture Notes in Computer Science</em>, pages 333-346, Elounda, Greece, 1993. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HH95] </dt>
<dd><p class="startdd"><a class="anchor" id="HH95"></a> 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, <em> Hybrid Systems II</em>, volume 999 of <em>Lecture Notes in Computer Science</em>, pages 252-264. Springer-Verlag, Berlin, 1995.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HHL90] </dt>
<dd><p class="startdd"><a class="anchor" id="HHL90"></a> L. Huelsbergen, D. Hahn, and J. Larus. Exact dependence analysis using data access descriptors. Technical Report 945, Department of Computer Science, University of Wisconsin, Madison, 1990.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HKP95] </dt>
<dd><p class="startdd"><a class="anchor" id="HKP95"></a> N. Halbwachs, A. Kerbrat, and Y.-E. Proy. <em>POLyhedra INtegrated Environment</em>. Verimag, France, version 1.0 of POLINE edition, September 1995. Documentation taken from source code.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HLW94] </dt>
<dd><p class="startdd"><a class="anchor" id="HLW94"></a> V. Van Dongen H. Le Verge and D. K. Wilde. Loop nest synthesis using the polyhedral library. <em>Publication interne</em> 830, IRISA, Campus de Beaulieu, Rennes, France, 1994.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HMT71] </dt>
<dd><p class="startdd"><a class="anchor" id="HMT71"></a> L. Henkin, J. D. Monk, and A. Tarski. <em>Cylindric Algebras: Part I</em>. North-Holland, Amsterdam, 1971.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HPR94] </dt>
<dd><p class="startdd"><a class="anchor" id="HPR94"></a> N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In B. Le Charlier, editor, <em>Static Analysis: Proceedings of the 1st International Symposium</em>, volume 864 of <em>Lecture Notes in Computer Science</em>, pages 223-237, Namur, Belgium, 1994. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HPR97] </dt>
<dd><p class="startdd"><a class="anchor" id="HPR97"></a> N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. <em>Formal Methods in System Design</em>, 11(2):157-185, 1997.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[HPWT01] </dt>
<dd><p class="startdd"><a class="anchor" id="HPWT01"></a> T. A. Henzinger, J. Preussig, and H. Wong-Toi. Some lessons from the hytech experience. In <em>Proceedings of the 40th Annual Conference on Decision and Control</em>, pages 2887-2892. IEEE Computer Society Press, 2001.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Jea02] </dt>
<dd><p class="startdd"><a class="anchor" id="Jea02"></a> B. Jeannet. <em>Convex Polyhedra Library</em>, release 1.1.3c edition, March 2002. Documentation of the “New Polka” library available at <a href="http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html">http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[JMSY94] </dt>
<dd><p class="startdd"><a class="anchor" id="JMSY94"></a> J. Jaffar, M. J. Maher, P. J. Stuckey, and R. H. C. Yap. Beyond finite domains. In A. Borning, editor, <em>Principles and Practice of Constraint Programming: Proceedings of the Second International Workshop</em>, volume 874 of <em>Lecture Notes in Computer Science</em>, pages 86-94, Rosario, Orcas Island, Washington, USA, 1994. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[KBB<sup>+</sup>06] </dt>
<dd><p class="startdd"><a class="anchor" id="KBBetal06"></a> L. Khachiyan, E. Boros, K. Borys, K. Elbassioni, and V. Gurvich. Generating all vertices of a polyhedron is hard. <em>Discrete and Computational Geometry</em>, 2006. Invited contribution. To appear.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Kuh56] </dt>
<dd><p class="startdd"><a class="anchor" id="Kuh56"></a> H. W. Kuhn. Solvability and consistency for linear equations and inequalities. <em>American Mathematical Monthly</em>, 63:217-232, 1956.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Le 92] </dt>
<dd><p class="startdd"><a class="anchor" id="Le"></a> 92 H. Le Verge. A note on Chernikova's algorithm. <em>Publication interne</em> 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Loe99] </dt>
<dd><p class="startdd"><a class="anchor" id="Loe99"></a> V. Loechner. <em>PolyLib</em>: A library for manipulating parameterized polyhedra. Available at <a href="http://icps.u-strasbg.fr/~loechner/polylib/">http://icps.u-strasbg.fr/~loechner/polylib/</a>, March 1999. Declares itself to be a continuation of <a class="el" href="main.html#Wil93">[Wil93]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[LW97] </dt>
<dd><p class="startdd"><a class="anchor" id="LW97"></a> V. Loechner and D. K. Wilde. Parameterized polyhedra and their vertices. <em>International Journal of Parallel Programming</em>, 25(6):525-549, 1997.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Mas92] </dt>
<dd><p class="startdd"><a class="anchor" id="Mas92"></a> F. Masdupuy. Array operations abstraction using semantic analysis of trapezoid congruences. In <em>Proceedings of the 6th ACM International Conference on Supercomputing</em>, pages 226-235, Washington, DC, USA, 1992. ACM Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Mas93] </dt>
<dd><p class="startdd"><a class="anchor" id="Mas93"></a> F. Masdupuy. <em>Array Indices Relational Semantic Analysis Using Rational Cosets and Trapezoids</em>. Thèse d'informatique, École Polytechnique, Palaiseau, France, December 1993.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Min01a] </dt>
<dd><p class="startdd"><a class="anchor" id="Min01a"></a> A. Miné. A new numerical abstract domain based on difference-bound matrices. In O. Danvy and A. Filinski, editors, <em>Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001)</em>, volume 2053 of <em> Lecture Notes in Computer Science</em>, pages 155-172, Aarhus, Denmark, 2001. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Min01b] </dt>
<dd><p class="startdd"><a class="anchor" id="Min01b"></a> A. Miné. The octagon abstract domain. In <em>Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01)</em>, pages 310-319, Stuttgart, Germany, 2001. IEEE Computer Society Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Min02] </dt>
<dd><p class="startdd"><a class="anchor" id="Min02"></a> A. Miné. A few graph-based relational numerical abstract domains. In M. V. Hermenegildo and G. Puebla, editors, <em>Static Analysis: Proceedings of the 9th International Symposium</em>, volume 2477 of <em>Lecture Notes in Computer Science</em>, pages 117-132, Madrid, Spain, 2002. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Min04] </dt>
<dd><p class="startdd"><a class="anchor" id="Min04"></a> A. Miné. Relational abstract domains for the detection of floating-point run-time errors. In D. Schmidt, editor, <em>Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming</em>, volume 2986 of <em>Lecture Notes in Computer Science</em>, pages 3-17, Barcelona, Spain, 2004. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Min05] </dt>
<dd><p class="startdd"><a class="anchor" id="Min05"></a> A. Miné. <em>Weakly Relational Numerical Abstract Domains</em>. PhD thesis, École Polytechnique, Paris, France, March 2005.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[MRTT53] </dt>
<dd><p class="startdd"><a class="anchor" id="MRTT53"></a> 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, <em>Contributions to the Theory of Games - Volume II</em>, number 28 in Annals of Mathematics Studies, pages 51-73. Princeton University Press, Princeton, New Jersey, 1953.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[NF01] </dt>
<dd><p class="startdd"><a class="anchor" id="NF01"></a> T. Nakanishi and A. Fukuda. Modulo interval arithmetic and its application to program analysis. <em>Transactions of Information Processing Society of Japan</em>, 42(4):829-837, 2001.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[NJPF99] </dt>
<dd><p class="startdd"><a class="anchor" id="NJPF99"></a> T. Nakanishi, K. Joe, C. D. Polychronopoulos, and A. Fukuda. The modulo interval: A simple and practical representation for program analysis. In <em>Proceedings of the 1999 International Conference on Parallel Architectures and Compilation Techniques</em>, pages 91-96, Newport Beach, California, USA, 1999. IEEE Computer Society.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[NO77] </dt>
<dd><p class="startdd"><a class="anchor" id="NO77"></a> G. Nelson and D. C. Oppen. Fast decision algorithms based on Union and Find. In <em>Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS'77)</em>, pages 114-119, Providence, RI, USA, 1977. IEEE Computer Society Press. The journal version of this paper is <a class="el" href="main.html#NO80">[NO80]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[NO80] </dt>
<dd><p class="startdd"><a class="anchor" id="NO80"></a> G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. <em>Journal of the ACM</em>, 27(2):356-364, 1980. An earlier version of this paper is <a class="el" href="main.html#NO77">[NO77]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[NR00] </dt>
<dd><p class="startdd"><a class="anchor" id="NR00"></a> S. P. K. Nookala and T. Risset. A library for Z-polyhedral operations. <em>Publication interne</em> 1330, IRISA, Campus de Beaulieu, Rennes, France, 2000.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[NW88] </dt>
<dd><p class="startdd"><a class="anchor" id="NW88"></a> G. L. Nemhauser and L. A. Wolsey. <em>Integer and Combinatorial Optimization</em>. Wiley Interscience Series in Discrete Mathematics and Optimization. John Wiley & Sons, 1988.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Pra77] </dt>
<dd><p class="startdd"><a class="anchor" id="Pra77"></a> V. R. Pratt. Two easy theories whose combination is hard. Memo sent to Nelson and Oppen concerning a preprint of their paper <a class="el" href="main.html#NO77">[NO77]</a>, September 1977.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[PS98] </dt>
<dd><p class="startdd"><a class="anchor" id="PS98"></a> C. H. Papadimitriou and K. Steiglitz. <em>Combinatorial Optimization: Algorithms and Complexity</em>. Dover Publications, second edition, 1998.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[QRR96] </dt>
<dd><p class="startdd"><a class="anchor" id="QRR96"></a> P. Quinton, S. Rajopadhye, and T. Risset. On manipulating Z-polyhedra. Technical Report 1016, IRISA, Campus Universitaire de Bealieu, Rennes, France, July 1996.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[QRR97] </dt>
<dd><p class="startdd"><a class="anchor" id="QRR97"></a> P. Quinton, S. Rajopadhye, and T. Risset. On manipulating Z-polyhedra using a canonic representation. <em>Parallel Processing Letters</em>, 7(2):181-194, 1997.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[QRW00] </dt>
<dd><p class="startdd"><a class="anchor" id="QRW00"></a> F. Quilleré, S. V. Rajopadhye, and D. Wilde. Generation of efficient nested loops from polyhedra. <em>International Journal of Parallel Programming</em>, 28(5):469-498, 2000.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[RBL06] </dt>
<dd><p class="startdd"><a class="anchor" id="RBL06"></a> T. W. Reps, G. Balakrishnan, and J. Lim. Intermediate-representation recovery from low-level code. In J. Hatcliff and F. Tip, editors, <em>Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation</em>, pages 100-111, Charleston, South Carolina, USA, 2006. ACM Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Ric02] </dt>
<dd><p class="startdd"><a class="anchor" id="Ric02"></a> E. Ricci. Rappresentazione e manipolazione di poliedri convessi per l'analisi e la verifica di programmi. Laurea dissertation, University of Parma, Parma, Italy, July 2002. In Italian.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Sch99] </dt>
<dd><p class="startdd"><a class="anchor" id="Sch99"></a> A. Schrijver. <em>Theory of Linear and Integer Programming</em>. Wiley Interscience Series in Discrete Mathematics and Optimization. John Wiley & Sons, 1999.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Sho81] </dt>
<dd><p class="startdd"><a class="anchor" id="Sho81"></a> R. E. Shostak. Deciding linear inequalities by computing loop residues. <em>Journal of the ACM</em>, 28(4):769-779, 1981.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[SK07] </dt>
<dd><p class="startdd"><a class="anchor" id="SK07"></a> A. Simon and A. King. Taming the wrapping of integer arithmetic. In H. Riis Nielson and G. Filé, editors, <em>Static Analysis: Proceedings of the 14th International Symposium</em>, volume 4634 of <em>Lecture Notes in Computer Science</em>, pages 121-136, Kongens Lyngby, Denmark, 2007. Springer-Verlag, Berlin.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Sri93] </dt>
<dd><p class="startdd"><a class="anchor" id="Sri93"></a> D. Srivastava. Subsumption and indexing in constraint query languages with linear arithmetic constraints. <em>Annals of Mathematics and Artificial Intelligence</em>, 8(3-4):315-343, 1993.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[SS07a] </dt>
<dd><p class="startdd"><a class="anchor" id="SS07a"></a> R. Sen and Y. N. Srikant. Executable analysis using abstract interpretation with circular linear progressions. In <em>Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007)</em>, pages 39-48, Nice, France, 2007. IEEE Computer Society Press.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[SS07b] </dt>
<dd><p class="startdd"><a class="anchor" id="SS07b"></a> R. Sen and Y. N. Srikant. Executable analysis with circular linear progressions. Technical Report IISc-CSA-TR-2007-3, Department of Computer Science and Automation, Indian Institute of Science, Bangalore, India, 2007.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[SW70] </dt>
<dd><p class="startdd"><a class="anchor" id="SW70"></a> J. Stoer and C. Witzgall. <em>Convexity and Optimization in Finite Dimensions I</em>. Springer-Verlag, Berlin, 1970.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[War03] </dt>
<dd><p class="startdd"><a class="anchor" id="War03"></a> H. S. Warren, Jr. <em>Hacker's Delight</em>. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Wey35] </dt>
<dd><p class="startdd"><a class="anchor" id="Wey35"></a> H. Weyl. Elementare theorie der konvexen polyeder. <em>Commentarii Mathematici Helvetici</em>, 7:290-306, 1935. English translation in <a class="el" href="main.html#Wey50">[Wey50]</a>.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Wey50] </dt>
<dd><p class="startdd"><a class="anchor" id="Wey50"></a> H. Weyl. The elementary theory of convex polyhedra. In H. W. Kuhn, editor, <em>Contributions to the Theory of Games - Volume I</em>, number 24 in Annals of Mathematics Studies, pages 3-18. Princeton University Press, Princeton, New Jersey, 1950. Translated from <a class="el" href="main.html#Wey35">[Wey35]</a> by H. W. Kuhn.</p>
<p></p>
<p class="enddd"></p>
</dd>
<dt>[Wil93] </dt>
<dd><p class="startdd"><a class="anchor" id="Wil93"></a> D. K. Wilde. A library for doing polyhedral operations. Master's thesis, Oregon State University, Corvallis, Oregon, December 1993. Also published as IRISA <em>Publication interne</em> 785, Rennes, France, 1993.</p>
<p class="enddd"></p>
</dd>
</dl>
</div>
<hr class="footer"/><address style="text-align: right;"><small>Generated on Sun Feb 27 10:10:57 2011 for PPL by
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.6.3 </small></address>
</body>
</html>
