The Parma Polyhedra Library
User’s Manual
∗
(version 0.10.2)
Roberto Bagnara
†
Patricia M. Hill
‡
Enea Zaffanella
§
based on previous work also by
Elisa Ricci
and
Sara Bonini
Andrea Pescetti
Angela Stazzone
Tatiana Zolo
April 18, 2009
∗
This work has been partly supported by: University of Parma’s FIL scientific research project (ex 60%) “Pure and Applied Math-
ematics”; MURST project “Automatic Program Certification by Abstract Interpretation”; MURST project “Abstract Interpretation,
Type Systems and Control-Flow Analysis”; MURST project “Automatic Aggregate- and Number-Reasoning for Computing: from
Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps”; MURST project “Constraint Based Verification
of Reactive Systems”; MURST project “Abstract Interpretation: Design and Applications”; EPSRC project “Numerical Domains for
Software Analysis”; EPSRC project “Geometric Abstractions for Scalable Program Analyzers”.
†
bagnara@cs.unipr.it, Department of Mathematics, University of Parma, Italy.
‡
hill@comp.leeds.ac.uk, School of Computing, University of Leeds, U.K.
§
zaffanella@cs.unipr.it, Department of Mathematics, University of Parma, Italy.
CONTENTS i
Copyright © 2001–2009 Roberto Bagnara (bagnara@cs.unipr.it).
This document describes the Parma Polyhedra Library (PPL).
Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free
Documentation License, Version 1.2 or any later version published by the Free Software Foundation; with
no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included
in the section entitled “GNU Free Documentation License”.
The PPL is free software; you can redistribute it and/or modify it under the terms of the GNU General
Public License as published by the Free Software Foundation; either version 3 of the License, or (at your
option) any later version. A copy of the license is included in the section entitled “GNU GENERAL
PUBLIC LICENSE”.
The PPL is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even
the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
For the most up-to-date information see the Parma Polyhedra Library site:
http://www.cs.unipr.it/ppl/
Contents
1 General Information on the PPL 2
1.1 The Main Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Upward Approximation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.3 Convex Polyhedra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Representations of Convex Polyhedra . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.5 Operations on Convex Polyhedra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.6 Intervals and Boxes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.7 Weakly-Relational Shapes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.8 Rational Grids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
1.9 Operations on Rational Grids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.10 The Powerset Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1.11 Operations on the Powerset Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1.12 The Pointset Powerset Domain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1.13 Using the Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1.14 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2 GNU General Public License 39
3 GNU Free Documentation License 48
4 Deprecated List 53
5 Module Index 56
The Parma Polyhedra Library User’s Manual (version 0.10.2). See http://www.cs.unipr.it/ppl/ for more information.
CONTENTS ii
5.1 Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
6 Namespace Index 56
6.1 Namespace List . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
7 Class Index 56
7.1 Class Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
8 Class Index 58
8.1 Class List . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
9 Module Documentation 60
9.1 C++ Language Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
10 Namespace Documentation 69
10.1 Parma_Polyhedra_Library Namespace Reference . . . . . . . . . . . . . . . . . . . . . . 69
10.2 Parma_Polyhedra_Library::IO_Operators Namespace Reference . . . . . . . . . . . . . . 76
10.3 std Namespace Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
11 Class Documentation 78
11.1 Parma_Polyhedra_Library::BD_Shape< T > Class Template Reference . . . . . . . . . . 78
11.2 Parma_Polyhedra_Library::BHRZ03_Certificate Class Reference . . . . . . . . . . . . . 110
11.3 Parma_Polyhedra_Library::BHRZ03_Certificate::Compare Struct Reference . . . . . . . . 112
11.4 Parma_Polyhedra_Library::Box< ITV > Class Template Reference . . . . . . . . . . . . 112
11.5 Parma_Polyhedra_Library::C_Polyhedron Class Reference . . . . . . . . . . . . . . . . . 141
11.6 Parma_Polyhedra_Library::Checked_Number< T, Policy > Class Template Reference . . 146
11.7 Parma_Polyhedra_Library::Congruence Class Reference . . . . . . . . . . . . . . . . . . 161
11.8 Parma_Polyhedra_Library::Congruence_System Class Reference . . . . . . . . . . . . . . 168
11.9 Parma_Polyhedra_Library::Congruence_System::const_iterator Class Reference . . . . . 173
11.10Parma_Polyhedra_Library::Constraint Class Reference . . . . . . . . . . . . . . . . . . . 174
11.11Parma_Polyhedra_Library::Constraint_System Class Reference . . . . . . . . . . . . . . 183
11.12Parma_Polyhedra_Library::Constraint_System::const_iterator Class Reference . . . . . . 187
11.13Parma_Polyhedra_Library::Constraints_Reduction< D1, D2 > Class Template Reference 188
11.14Parma_Polyhedra_Library::Determinate< PS > Class Template Reference . . . . . . . . . 189
11.15Parma_Polyhedra_Library::Domain_Product< D1, D2 > Class Template Reference . . . . 192
11.16Parma_Polyhedra_Library::From_Covering_Box Struct Reference . . . . . . . . . . . . . 192
11.17Parma_Polyhedra_Library::Generator Class Reference . . . . . . . . . . . . . . . . . . . 192
11.18Parma_Polyhedra_Library::Generator_System Class Reference . . . . . . . . . . . . . . . 203
11.19Parma_Polyhedra_Library::Generator_System::const_iterator Class Reference . . . . . . . 207
The Parma Polyhedra Library User’s Manual (version 0.10.2). See http://www.cs.unipr.it/ppl/ for more information.
CONTENTS 1
11.20Parma_Polyhedra_Library::GMP_Integer Class Reference . . . . . . . . . . . . . . . . . 209
11.21Parma_Polyhedra_Library::Grid Class Reference . . . . . . . . . . . . . . . . . . . . . . 212
11.22Parma_Polyhedra_Library::Grid_Certificate Class Reference . . . . . . . . . . . . . . . . 249
11.23Parma_Polyhedra_Library::Grid_Certificate::Compare Struct Reference . . . . . . . . . . 250
11.24Parma_Polyhedra_Library::Grid_Generator Class Reference . . . . . . . . . . . . . . . . 251
11.25Parma_Polyhedra_Library::Grid_Generator_System Class Reference . . . . . . . . . . . . 258
11.26Parma_Polyhedra_Library::Grid_Generator_System::const_iterator Class Reference . . . 264
11.27Parma_Polyhedra_Library::H79_Certificate Class Reference . . . . . . . . . . . . . . . . 265
11.28Parma_Polyhedra_Library::H79_Certificate::Compare Struct Reference . . . . . . . . . . 266
11.29Parma_Polyhedra_Library::Interval< Boundary, Info > Class Template Reference . . . . 267
11.30Parma_Polyhedra_Library::Is_Checked< T > Struct Template Reference . . . . . . . . . 270
11.31Parma_Polyhedra_Library::Is_Checked< Checked_Number< T, P > > Struct Template
Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 270
11.32Parma_Polyhedra_Library::Is_Native_Or_Checked< T > Struct Template Reference . . . 271
11.33Parma_Polyhedra_Library::Linear_Expression Class Reference . . . . . . . . . . . . . . . 271
11.34Parma_Polyhedra_Library::MIP_Problem Class Reference . . . . . . . . . . . . . . . . . 279
11.35Parma_Polyhedra_Library::NNC_Polyhedron Class Reference . . . . . . . . . . . . . . . 287
11.36Parma_Polyhedra_Library::No_Reduction< D1, D2 > Class Template Reference . . . . . 292
11.37Parma_Polyhedra_Library::Octagonal_Shape< T > Class Template Reference . . . . . . 293
11.38Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R > Class Template
Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323
11.39Parma_Polyhedra_Library::Pointset_Powerset< PS > Class Template Reference . . . . . 350
11.40Parma_Polyhedra_Library::Poly_Con_Relation Class Reference . . . . . . . . . . . . . . 376
11.41Parma_Polyhedra_Library::Poly_Gen_Relation Class Reference . . . . . . . . . . . . . . 378
11.42Parma_Polyhedra_Library::Polyhedron Class Reference . . . . . . . . . . . . . . . . . . 380
11.43Parma_Polyhedra_Library::Powerset< D > Class Template Reference . . . . . . . . . . . 414
11.44Parma_Polyhedra_Library::Recycle_Input Struct Reference . . . . . . . . . . . . . . . . . 421
11.45Parma_Polyhedra_Library::Smash_Reduction< D1, D2 > Class Template Reference . . . 422
11.46Parma_Polyhedra_Library::Throwable Class Reference . . . . . . . . . . . . . . . . . . . 423
11.47Parma_Polyhedra_Library::Variable Class Reference . . . . . . . . . . . . . . . . . . . . 423
11.48Parma_Polyhedra_Library::Variable::Compare Struct Reference . . . . . . . . . . . . . . 425
11.49Parma_Polyhedra_Library::Variables_Set Class Reference . . . . . . . . . . . . . . . . . 426
The Parma Polyhedra Library User’s Manual (version 0.10.2). See http://www.cs.unipr.it/ppl/ for more information.
1 General Information on the PPL 2
1 General Information on the PPL
1.1 The Main Features
The Parma Polyhedra Library (PPL) is a modern C++ library for the manipulation of numerical information
that can be represented by points in some n-dimensional vector space. For instance, one of the key domains
the PPL supports is that of rational convex polyhedra (Section Convex Polyhedra). Such domains are
employed in several systems for the analysis and verification of hardware and software components, with
applications spanning imperative, functional and logic programming languages, synchronous languages
and synchronization protocols, real-time and hybrid systems. Even though the PPL library is not meant
to target a particular problem, the design of its interface has been largely influenced by the needs of the
above class of applications. That is the reason why the library implements a few operators that are more or
less specific to static analysis applications, while lacking some other operators that might be useful when
working, e.g., in the field of computational geometry.
The main features of the library are the following:
• it is user friendly: you write x + 2∗y + 5∗z <= 7 when you mean it;
• it is fully dynamic: available virtual memory is the only limitation to the dimension of anything;
• it provides full support for the manipulation of convex polyhedra that are not topologically closed;
• it is written in standard C++: meant to be portable;
• it is exception-safe: never leaks resources or leaves invalid object fragments around;
• it is rather efficient: and we hope to make it even more so;
• it is thoroughly documented: perhaps not literate programming but close enough;
• it has interfaces to other programming languages: including C, Java, OCaml and a number of Prolog
systems;
• it is free software: distributed under the terms of the GNU General Public License.
In the following section we describe all the domains available to the PPL user. More detailed descriptions
of these domains andthe operations provided will be found in subsequent sections.
In the final section of this chapter (Section Using the Library), we provide some additional advice on the
use of the library.
1.1.1 Semantic Geometric Descriptors
A semantic geometric descriptor is a subset of R
n
. 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 simple classes:
• C_Polyhedron ,
• NNC_Polyhedron ,
• BD_Shape<T> ,
• Octagonal_Shape<T> ,
• Box<ITV> , and
The Parma Polyhedra Library User’s Manual (version 0.10.2). See http://www.cs.unipr.it/ppl/ for more information.
