PPL 1.0

- Main Page
- Related Pages
- Modules
- Namespaces
- Classes

Namespaces | Classes | Macros | Typedefs | Enumerations | Variables
C++ Language Interface

The core implementation of the Parma Polyhedra Library is written in C++. More...

## Namespaces
namespace | Parma_Polyhedra_Library::IO_Operators
| All input/output operators are confined to this namespace.
namespace | std
| The standard C++ namespace.

## Classes
class | Parma_Polyhedra_Library::Variable
| A dimension of the vector space. More...
struct | Parma_Polyhedra_Library::Variable::Compare
| Binary predicate defining the total ordering on variables. More...
class | Parma_Polyhedra_Library::Throwable
| User objects the PPL can throw. More...
struct | Parma_Polyhedra_Library::Recycle_Input
| A tag class. More...
class | Parma_Polyhedra_Library::Linear_Form< C >
| A linear form with interval coefficients. More...
class | Parma_Polyhedra_Library::Checked_Number< T, Policy >
| A wrapper for numeric types implementing a given policy. More...
class | Parma_Polyhedra_Library::Interval< Boundary, Info >
| A generic, not necessarily closed, possibly restricted interval. More...
class | Parma_Polyhedra_Library::Linear_Expression
| A linear expression. More...
class | Parma_Polyhedra_Library::Constraint
| A linear equality or inequality. More...
class | Parma_Polyhedra_Library::Generator
| A line, ray, point or closure point. More...
class | Parma_Polyhedra_Library::Grid_Generator
| A grid line, parameter or grid point. More...
class | Parma_Polyhedra_Library::Congruence
| A linear congruence. More...
class | Parma_Polyhedra_Library::Box< ITV >
| A not necessarily closed, iso-oriented hyperrectangle. More...
class | Parma_Polyhedra_Library::Constraint_System
| A system of constraints. More...
class | Parma_Polyhedra_Library::Constraint_System_const_iterator
| An iterator over a system of constraints. More...
class | Parma_Polyhedra_Library::Congruence_System
| A system of congruences. More...
class | Parma_Polyhedra_Library::Congruence_System::const_iterator
| An iterator over a system of congruences. More...
class | Parma_Polyhedra_Library::Poly_Con_Relation
| The relation between a polyhedron and a constraint. More...
class | Parma_Polyhedra_Library::Generator_System
| A system of generators. More...
class | Parma_Polyhedra_Library::Generator_System_const_iterator
| An iterator over a system of generators. More...
class | Parma_Polyhedra_Library::Poly_Gen_Relation
| The relation between a polyhedron and a generator. More...
class | Parma_Polyhedra_Library::Polyhedron
| The base class for convex polyhedra. More...
class | Parma_Polyhedra_Library::MIP_Problem
| A Mixed Integer (linear) Programming problem. More...
class | Parma_Polyhedra_Library::Grid_Generator_System
| A system of grid generators. More...
class | Parma_Polyhedra_Library::Grid
| A grid. More...
class | Parma_Polyhedra_Library::BD_Shape< T >
| A bounded difference shape. More...
class | Parma_Polyhedra_Library::C_Polyhedron
| A closed convex polyhedron. More...
class | Parma_Polyhedra_Library::Octagonal_Shape< T >
| An octagonal shape. More...
class | Parma_Polyhedra_Library::PIP_Problem
| A Parametric Integer (linear) Programming problem. More...
class | Parma_Polyhedra_Library::BHRZ03_Certificate
| The convergence certificate for the BHRZ03 widening operator. More...
class | Parma_Polyhedra_Library::H79_Certificate
| A convergence certificate for the H79 widening operator. More...
class | Parma_Polyhedra_Library::Grid_Certificate
| The convergence certificate for the Grid widening operator. More...
class | Parma_Polyhedra_Library::NNC_Polyhedron
| A not necessarily closed convex polyhedron. More...
class | Parma_Polyhedra_Library::Smash_Reduction< D1, D2 >
| This class provides the reduction method for the Smash_Product domain. More...
class | Parma_Polyhedra_Library::Constraints_Reduction< D1, D2 >
| This class provides the reduction method for the Constraints_Product domain. More...
class | Parma_Polyhedra_Library::Congruences_Reduction< D1, D2 >
| This class provides the reduction method for the Congruences_Product domain. More...
class | Parma_Polyhedra_Library::Shape_Preserving_Reduction< D1, D2 >
| This class provides the reduction method for the Shape_Preserving_Product domain. More...
class | Parma_Polyhedra_Library::No_Reduction< D1, D2 >
| This class provides the reduction method for the Direct_Product domain. More...
class | Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >
| The partially reduced product of two abstractions. More...
class | Parma_Polyhedra_Library::Determinate< PSET >
| A wrapper for PPL pointsets, providing them with a determinate constraint system interface, as defined in [Bag98]. More...
class | Parma_Polyhedra_Library::Powerset< D >
| The powerset construction on a base-level domain. More...
class | Parma_Polyhedra_Library::Pointset_Powerset< PSET >
| The powerset construction instantiated on PPL pointset domains. More...
class | Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Cast Floating Point Expression. More...
class | Parma_Polyhedra_Library::Constant_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Constant Floating Point Expression. More...
class | Parma_Polyhedra_Library::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Variable Floating Point Expression. More...
class | Parma_Polyhedra_Library::Sum_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Sum Floating Point Expression. More...
class | Parma_Polyhedra_Library::Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Difference Floating Point Expression. More...
class | Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Multiplication Floating Point Expression. More...
class | Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Division Floating Point Expression. More...
class | Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >
| A generic Opposite Floating Point Expression. More...
class | Parma_Polyhedra_Library::GMP_Integer
| Unbounded integers as provided by the GMP library. More...

## Macros
#define | PPL_VERSION_MAJOR 1
| The major number of the PPL version.
#define | PPL_VERSION_MINOR 0
| The minor number of the PPL version.
#define | PPL_VERSION_REVISION 0
| The revision number of the PPL version.
#define | PPL_VERSION_BETA 0
| The beta number of the PPL version. This is zero for official releases and nonzero for development snapshots.
#define | PPL_VERSION "1.0"
| A string containing the PPL version.

## Typedefs
typedef size_t | Parma_Polyhedra_Library::dimension_type
| An unsigned integral type for representing space dimensions.
typedef size_t | Parma_Polyhedra_Library::memory_size_type
| An unsigned integral type for representing memory size in bytes.
typedef PPL_COEFFICIENT_TYPE | Parma_Polyhedra_Library::Coefficient
| An alias for easily naming the type of PPL coefficients.

## Enumerations
enum | Parma_Polyhedra_Library::Result { Parma_Polyhedra_Library::V_EMPTY, Parma_Polyhedra_Library::V_EQ, Parma_Polyhedra_Library::V_LT, Parma_Polyhedra_Library::V_GT, Parma_Polyhedra_Library::V_NE, Parma_Polyhedra_Library::V_LE, Parma_Polyhedra_Library::V_GE, Parma_Polyhedra_Library::V_LGE, Parma_Polyhedra_Library::V_OVERFLOW, Parma_Polyhedra_Library::V_LT_INF, Parma_Polyhedra_Library::V_GT_SUP, Parma_Polyhedra_Library::V_LT_PLUS_INFINITY, Parma_Polyhedra_Library::V_GT_MINUS_INFINITY, Parma_Polyhedra_Library::V_EQ_MINUS_INFINITY, Parma_Polyhedra_Library::V_EQ_PLUS_INFINITY, Parma_Polyhedra_Library::V_NAN, Parma_Polyhedra_Library::V_CVT_STR_UNK, Parma_Polyhedra_Library::V_DIV_ZERO, Parma_Polyhedra_Library::V_INF_ADD_INF, Parma_Polyhedra_Library::V_INF_DIV_INF, Parma_Polyhedra_Library::V_INF_MOD, Parma_Polyhedra_Library::V_INF_MUL_ZERO, Parma_Polyhedra_Library::V_INF_SUB_INF, Parma_Polyhedra_Library::V_MOD_ZERO, Parma_Polyhedra_Library::V_SQRT_NEG, Parma_Polyhedra_Library::V_UNKNOWN_NEG_OVERFLOW, Parma_Polyhedra_Library::V_UNKNOWN_POS_OVERFLOW, Parma_Polyhedra_Library::V_UNREPRESENTABLE }
| Possible outcomes of a checked arithmetic computation. More...
enum | Parma_Polyhedra_Library::Rounding_Dir { Parma_Polyhedra_Library::ROUND_DOWN, Parma_Polyhedra_Library::ROUND_UP, Parma_Polyhedra_Library::ROUND_IGNORE , Parma_Polyhedra_Library::ROUND_NOT_NEEDED , Parma_Polyhedra_Library::ROUND_STRICT_RELATION }
| Rounding directions for arithmetic computations. More...
enum | Parma_Polyhedra_Library::Degenerate_Element { Parma_Polyhedra_Library::UNIVERSE, Parma_Polyhedra_Library::EMPTY }
| Kinds of degenerate abstract elements. More...
enum | Parma_Polyhedra_Library::Relation_Symbol { Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::LESS_THAN, Parma_Polyhedra_Library::LESS_OR_EQUAL, Parma_Polyhedra_Library::GREATER_THAN, Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::NOT_EQUAL }
| Relation symbols. More...
enum | Parma_Polyhedra_Library::Complexity_Class { Parma_Polyhedra_Library::POLYNOMIAL_COMPLEXITY, Parma_Polyhedra_Library::SIMPLEX_COMPLEXITY, Parma_Polyhedra_Library::ANY_COMPLEXITY }
| Complexity pseudo-classes. More...
enum | Parma_Polyhedra_Library::Optimization_Mode { Parma_Polyhedra_Library::MINIMIZATION, Parma_Polyhedra_Library::MAXIMIZATION }
| Possible optimization modes. More...
enum | Parma_Polyhedra_Library::Bounded_Integer_Type_Width { Parma_Polyhedra_Library::BITS_8, Parma_Polyhedra_Library::BITS_16, Parma_Polyhedra_Library::BITS_32, Parma_Polyhedra_Library::BITS_64, Parma_Polyhedra_Library::BITS_128 }
| Widths of bounded integer types. More...
enum | Parma_Polyhedra_Library::Bounded_Integer_Type_Representation { Parma_Polyhedra_Library::UNSIGNED, Parma_Polyhedra_Library::SIGNED_2_COMPLEMENT }
| Representation of bounded integer types. More...
enum | Parma_Polyhedra_Library::Bounded_Integer_Type_Overflow { Parma_Polyhedra_Library::OVERFLOW_WRAPS, Parma_Polyhedra_Library::OVERFLOW_UNDEFINED, Parma_Polyhedra_Library::OVERFLOW_IMPOSSIBLE }
| Overflow behavior of bounded integer types. More...
enum | Parma_Polyhedra_Library::Representation { Parma_Polyhedra_Library::DENSE, Parma_Polyhedra_Library::SPARSE }
| Possible representations of coefficient sequences (i.e. linear expressions and more complex objects containing linear expressions, e.g. Constraints, Generators, etc.). More...
enum | Parma_Polyhedra_Library::Floating_Point_Format { Parma_Polyhedra_Library::IEEE754_HALF, Parma_Polyhedra_Library::IEEE754_SINGLE, Parma_Polyhedra_Library::IEEE754_DOUBLE, Parma_Polyhedra_Library::IEEE754_QUAD, Parma_Polyhedra_Library::INTEL_DOUBLE_EXTENDED, Parma_Polyhedra_Library::IBM_SINGLE, Parma_Polyhedra_Library::IBM_DOUBLE }
| Floating point formats known to the library. More...
enum | Parma_Polyhedra_Library::PIP_Problem_Status { Parma_Polyhedra_Library::UNFEASIBLE_PIP_PROBLEM, Parma_Polyhedra_Library::OPTIMIZED_PIP_PROBLEM }
| Possible outcomes of the PIP_Problem solver. More...
enum | Parma_Polyhedra_Library::MIP_Problem_Status { Parma_Polyhedra_Library::UNFEASIBLE_MIP_PROBLEM, Parma_Polyhedra_Library::UNBOUNDED_MIP_PROBLEM, Parma_Polyhedra_Library::OPTIMIZED_MIP_PROBLEM }
| Possible outcomes of the MIP_Problem solver. More...

## Variables
const Throwable *volatile | Parma_Polyhedra_Library::abandon_expensive_computations
| A pointer to an exception object.

## Functions Inspecting and/or Combining Result Values
Result | Parma_Polyhedra_Library::operator& (Result x, Result y)
Result | Parma_Polyhedra_Library::operator| (Result x, Result y)
Result | Parma_Polyhedra_Library::operator- (Result x, Result y)
Result_Class | Parma_Polyhedra_Library::result_class (Result r)
| Extracts the value class part of `r` (representable number, unrepresentable minus/plus infinity or nan).
Result_Relation | Parma_Polyhedra_Library::result_relation (Result r)
| Extracts the relation part of `r`.
Result | Parma_Polyhedra_Library::result_relation_class (Result r)

## Functions Inspecting and/or Combining Rounding_Dir Values
Rounding_Dir | Parma_Polyhedra_Library::operator& (Rounding_Dir x, Rounding_Dir y)
Rounding_Dir | Parma_Polyhedra_Library::operator| (Rounding_Dir x, Rounding_Dir y)
Rounding_Dir | Parma_Polyhedra_Library::inverse (Rounding_Dir dir)
| Returns the inverse rounding mode of `dir`, `ROUND_IGNORE` being the inverse of itself.
Rounding_Dir | Parma_Polyhedra_Library::round_dir (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_down (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_up (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_ignore (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_not_needed (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_not_requested (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_direct (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_inverse (Rounding_Dir dir)
bool | Parma_Polyhedra_Library::round_strict_relation (Rounding_Dir dir)
fpu_rounding_direction_type | Parma_Polyhedra_Library::round_fpu_dir (Rounding_Dir dir)

## Functions for the Synthesis of Linear Rankings
template<typename PSET >
bool | Parma_Polyhedra_Library::termination_test_MS (const PSET &pset)
| Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::termination_test_MS_2 (const PSET &pset_before, const PSET &pset_after)
| Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::one_affine_ranking_function_MS (const PSET &pset, Generator &mu)
| Termination test with witness ranking function using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::one_affine_ranking_function_MS_2 (const PSET &pset_before, const PSET &pset_after, Generator &mu)
| Termination test with witness ranking function using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
void | Parma_Polyhedra_Library::all_affine_ranking_functions_MS (const PSET &pset, C_Polyhedron &mu_space)
| Termination test with ranking function space using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
void | Parma_Polyhedra_Library::all_affine_ranking_functions_MS_2 (const PSET &pset_before, const PSET &pset_after, C_Polyhedron &mu_space)
| Termination test with ranking function space using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
void | Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS (const PSET &pset, C_Polyhedron &decreasing_mu_space, C_Polyhedron &bounded_mu_space)
| Computes the spaces of affine quasi ranking functions using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
void | Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS_2 (const PSET &pset_before, const PSET &pset_after, C_Polyhedron &decreasing_mu_space, C_Polyhedron &bounded_mu_space)
| Computes the spaces of affine quasi ranking functions using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::termination_test_PR (const PSET &pset)
| Like termination_test_MS() but using the method by Podelski and Rybalchenko [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::termination_test_PR_2 (const PSET &pset_before, const PSET &pset_after)
| Like termination_test_MS_2() but using an alternative formalization of the method by Podelski and Rybalchenko [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::one_affine_ranking_function_PR (const PSET &pset, Generator &mu)
| Like one_affine_ranking_function_MS() but using the method by Podelski and Rybalchenko [BMPZ10].
template<typename PSET >
bool | Parma_Polyhedra_Library::one_affine_ranking_function_PR_2 (const PSET &pset_before, const PSET &pset_after, Generator &mu)
| Like one_affine_ranking_function_MS_2() but using an alternative formalization of the method by Podelski and Rybalchenko [BMPZ10].
template<typename PSET >
void | Parma_Polyhedra_Library::all_affine_ranking_functions_PR (const PSET &pset, NNC_Polyhedron &mu_space)
| Like all_affine_ranking_functions_MS() but using the method by Podelski and Rybalchenko [BMPZ10].
template<typename PSET >
void | Parma_Polyhedra_Library::all_affine_ranking_functions_PR_2 (const PSET &pset_before, const PSET &pset_after, NNC_Polyhedron &mu_space)
| Like all_affine_ranking_functions_MS_2() but using an alternative formalization of the method by Podelski and Rybalchenko [BMPZ10].

## Detailed Description

The core implementation of the Parma Polyhedra Library is written in C++.

See Namespace, Hierarchical and Compound indexes for additional information about each single data type.

## Macro Definition Documentation

#define PPL_VERSION_MAJOR 1

The major number of the PPL version.

#define PPL_VERSION_MINOR 0

The minor number of the PPL version.

#define PPL_VERSION_REVISION 0

The revision number of the PPL version.

#define PPL_VERSION "1.0"

A string containing the PPL version.

Let `M` and `m` denote the numbers associated to PPL_VERSION_MAJOR and PPL_VERSION_MINOR, respectively. The format of PPL_VERSION is `M "." m` if both PPL_VERSION_REVISION (`r`) and PPL_VERSION_BETA (`b`)are zero, `M "." m "pre" b` if PPL_VERSION_REVISION is zero and PPL_VERSION_BETA is not zero, `M "." m "." r` if PPL_VERSION_REVISION is not zero and PPL_VERSION_BETA is zero, `M "." m "." r "pre" b` if neither PPL_VERSION_REVISION nor PPL_VERSION_BETA are zero.

## Typedef Documentation

typedef size_t Parma_Polyhedra_Library::dimension_type

An unsigned integral type for representing space dimensions.

typedef size_t Parma_Polyhedra_Library::memory_size_type

An unsigned integral type for representing memory size in bytes.

typedef PPL_COEFFICIENT_TYPE Parma_Polyhedra_Library::Coefficient

An alias for easily naming the type of PPL coefficients.

Objects of type Coefficient are used to implement the integral valued coefficients occurring in linear expressions, constraints, generators, intervals, bounding boxes and so on. Depending on the chosen configuration options (see file `README.configure`), a Coefficient may actually be:

- The GMP_Integer type, which in turn is an alias for the `mpz_class` type implemented by the C++ interface of the GMP library (this is the default configuration).
- An instance of the Checked_Number class template: with the policy Bounded_Integer_Coefficient_Policy, this implements overflow detection on top of a native integral type (available template instances include checked integers having 8, 16, 32 or 64 bits); with the Checked_Number_Transparent_Policy, this is a wrapper for native integral types with no overflow detection (available template instances are as above).

## Enumeration Type Documentation

enum Parma_Polyhedra_Library::Result

Possible outcomes of a checked arithmetic computation.

Enumerator:

  V_EMPTY | The exact result is not comparable.
  V_EQ | The computed result is exact.
  V_LT | The computed result is inexact and rounded up.
  V_GT | The computed result is inexact and rounded down.
  V_NE | The computed result is inexact.
  V_LE | The computed result may be inexact and rounded up.
  V_GE | The computed result may be inexact and rounded down.
  V_LGE | The computed result may be inexact.
  V_OVERFLOW | The exact result is a number out of finite bounds.
  V_LT_INF | A negative integer overflow occurred (rounding up).
  V_GT_SUP | A positive integer overflow occurred (rounding down).
  V_LT_PLUS_INFINITY | A positive integer overflow occurred (rounding up).
  V_GT_MINUS_INFINITY | A negative integer overflow occurred (rounding down).
  V_EQ_MINUS_INFINITY | Negative infinity result.
  V_EQ_PLUS_INFINITY | Positive infinity result.
  V_NAN | Not a number result.
  V_CVT_STR_UNK | Converting from unknown string.
  V_DIV_ZERO | Dividing by zero.
  V_INF_ADD_INF | Adding two infinities having opposite signs.
  V_INF_DIV_INF | Dividing two infinities.
  V_INF_MOD | Taking the modulus of an infinity.
  V_INF_MUL_ZERO | Multiplying an infinity by zero.
  V_INF_SUB_INF | Subtracting two infinities having the same sign.
  V_MOD_ZERO | Computing a remainder modulo zero.
  V_SQRT_NEG | Taking the square root of a negative number.
  V_UNKNOWN_NEG_OVERFLOW | Unknown result due to intermediate negative overflow.
  V_UNKNOWN_POS_OVERFLOW | Unknown result due to intermediate positive overflow.
  V_UNREPRESENTABLE | The computed result is not representable.

enum Parma_Polyhedra_Library::Rounding_Dir

Rounding directions for arithmetic computations.

Enumerator:

  ROUND_DOWN | Round toward .
  ROUND_UP | Round toward .
  ROUND_IGNORE | Rounding is delegated to lower level. Result info is evaluated lazily.
  ROUND_NOT_NEEDED | Rounding is not needed: client code must ensure that the operation result is exact and representable in the destination type. Result info is evaluated lazily.
  ROUND_STRICT_RELATION | The client code is willing to pay an extra price to know the exact relation between the exact result and the computed one.

enum Parma_Polyhedra_Library::Degenerate_Element

Kinds of degenerate abstract elements.

Enumerator:

  UNIVERSE | The universe element, i.e., the whole vector space.
  EMPTY | The empty element, i.e., the empty set.

enum Parma_Polyhedra_Library::Relation_Symbol

Relation symbols.

Enumerator:

  EQUAL | Equal to.
  LESS_THAN | Less than.
  LESS_OR_EQUAL | Less than or equal to.
  GREATER_THAN | Greater than.
  GREATER_OR_EQUAL | Greater than or equal to.
  NOT_EQUAL | Not equal to.

enum Parma_Polyhedra_Library::Complexity_Class

Complexity pseudo-classes.

Enumerator:

  POLYNOMIAL_COMPLEXITY | Worst-case polynomial complexity.
  SIMPLEX_COMPLEXITY | Worst-case exponential complexity but typically polynomial behavior.
  ANY_COMPLEXITY | Any complexity.

enum Parma_Polyhedra_Library::Optimization_Mode

Possible optimization modes.

Enumerator:

  MINIMIZATION | Minimization is requested.
  MAXIMIZATION | Maximization is requested.

enum Parma_Polyhedra_Library::Bounded_Integer_Type_Width

Widths of bounded integer types.

See the section on approximating bounded integers.

Enumerator:

  BITS_8 | 8 bits.
  BITS_16 | 16 bits.
  BITS_32 | 32 bits.
  BITS_64 | 64 bits.
  BITS_128 | 128 bits.

enum Parma_Polyhedra_Library::Bounded_Integer_Type_Representation

Representation of bounded integer types.

See the section on approximating bounded integers.

Enumerator:

  UNSIGNED | Unsigned binary.
  SIGNED_2_COMPLEMENT | Signed binary where negative values are represented by the two's complement of the absolute value.

enum Parma_Polyhedra_Library::Bounded_Integer_Type_Overflow

Overflow behavior of bounded integer types.

See the section on approximating bounded integers.

Enumerator:

  OVERFLOW_WRAPS | On overflow, wrapping takes place. This means that, for a -bit bounded integer, the computation happens modulo .
  OVERFLOW_UNDEFINED | On overflow, the result is undefined. This simply means that the result of the operation resulting in an overflow can take any value. Note: 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.
  OVERFLOW_IMPOSSIBLE | Overflow is impossible. 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.

enum Parma_Polyhedra_Library::Representation

Possible representations of coefficient sequences (i.e. linear expressions and more complex objects containing linear expressions, e.g. Constraints, Generators, etc.).

Enumerator:

  DENSE | Dense representation: the coefficient sequence is represented as a vector of coefficients, including the zero coefficients. If there are only a few nonzero coefficients, this representation is faster and also uses a bit less memory.
  SPARSE | Sparse representation: only the nonzero coefficient are stored. If there are many nonzero coefficients, this improves memory consumption and run time (both because there is less data to process in O(n) operations and because finding zeroes/nonzeroes is much faster since zeroes are not stored at all, so any stored coefficient is nonzero).

enum Parma_Polyhedra_Library::Floating_Point_Format

Floating point formats known to the library.

The parameters of each format are defined by a specific struct in file Float.defs.hh. See the section on Analysis of floating point computations for more information.

Enumerator:

  IEEE754_HALF | IEEE 754 half precision, 16 bits (5 exponent, 10 mantissa).
  IEEE754_SINGLE | IEEE 754 single precision, 32 bits (8 exponent, 23 mantissa).
  IEEE754_DOUBLE | IEEE 754 double precision, 64 bits (11 exponent, 52 mantissa).
  IEEE754_QUAD | IEEE 754 quad precision, 128 bits (15 exponent, 112 mantissa).
  INTEL_DOUBLE_EXTENDED | Intel double extended precision, 80 bits (15 exponent, 64 mantissa)
  IBM_SINGLE | IBM single precision, 32 bits (7 exponent, 24 mantissa).
  IBM_DOUBLE | IBM double precision, 64 bits (7 exponent, 56 mantissa).

enum Parma_Polyhedra_Library::PIP_Problem_Status

Possible outcomes of the PIP_Problem solver.

Enumerator:

  UNFEASIBLE_PIP_PROBLEM | The problem is unfeasible.
  OPTIMIZED_PIP_PROBLEM | The problem has an optimal solution.

enum Parma_Polyhedra_Library::MIP_Problem_Status

Possible outcomes of the MIP_Problem solver.

Enumerator:

  UNFEASIBLE_MIP_PROBLEM | The problem is unfeasible.
  UNBOUNDED_MIP_PROBLEM | The problem is unbounded.
  OPTIMIZED_MIP_PROBLEM | The problem has an optimal solution.

## Function Documentation

Result Parma_Polyhedra_Library::operator& | ( | Result | x,
|  | Result | y
| ) |  |
| inline

Result Parma_Polyhedra_Library::operator| | ( | Result | x,
|  | Result | y
| ) |  |
| inline

Result Parma_Polyhedra_Library::operator- | ( | Result | x,
|  | Result | y
| ) |  |
| inline

Result_Class Parma_Polyhedra_Library::result_class | ( | Result | r | ) |
| inline

Extracts the value class part of `r` (representable number, unrepresentable minus/plus infinity or nan).

Result_Relation Parma_Polyhedra_Library::result_relation | ( | Result | r | ) |
| inline

Extracts the relation part of `r`.

Result Parma_Polyhedra_Library::result_relation_class | ( | Result | r | ) |
| inline

Rounding_Dir Parma_Polyhedra_Library::operator& | ( | Rounding_Dir | x,
|  | Rounding_Dir | y
| ) |  |
| inline

Rounding_Dir Parma_Polyhedra_Library::operator| | ( | Rounding_Dir | x,
|  | Rounding_Dir | y
| ) |  |
| inline

Rounding_Dir Parma_Polyhedra_Library::inverse | ( | Rounding_Dir | dir | ) |
| inline

Returns the inverse rounding mode of `dir`, `ROUND_IGNORE` being the inverse of itself.

Rounding_Dir Parma_Polyhedra_Library::round_dir | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_down | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_up | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_ignore | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_not_needed | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_not_requested | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_direct | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_inverse | ( | Rounding_Dir | dir | ) |
| inline

bool Parma_Polyhedra_Library::round_strict_relation | ( | Rounding_Dir | dir | ) |
| inline

fpu_rounding_direction_type Parma_Polyhedra_Library::round_fpu_dir | ( | Rounding_Dir | dir | ) |
| inline

template<typename PSET >

bool Parma_Polyhedra_Library::termination_test_MS | ( | const PSET & | pset | ) |

Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions , where unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update.

Returns:
  `true` if any loop approximated by `pset` definitely terminates; `false` if the test is inconclusive. However, if `pset` precisely characterizes the effect of the loop body onto the loop-relevant program variables, then `true` is returned if and only if the loop terminates.

template<typename PSET >

bool Parma_Polyhedra_Library::termination_test_MS_2 | ( | const PSET & | pset_before,
|  | const PSET & | pset_after
| ) |  |

Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset_before | A pointset approximating the values of loop-relevant variables before the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions .
  pset_after | A pointset approximating the values of loop-relevant variables after the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions ,

Note that unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update. Note also that unprimed variables are assigned to different space dimensions in `pset_before` and `pset_after`.

Returns:
  `true` if any loop approximated by `pset` definitely terminates; `false` if the test is inconclusive. However, if `pset_before` and `pset_after` precisely characterize the effect of the loop body onto the loop-relevant program variables, then `true` is returned if and only if the loop terminates.

template<typename PSET >

bool Parma_Polyhedra_Library::one_affine_ranking_function_MS | ( | const PSET & | pset,
|  | Generator & | mu
| ) |  |

Termination test with witness ranking function using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions , where unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update.
  mu | When `true` is returned, this is assigned a point of space dimension encoding one (not further specified) affine ranking function for the loop being analyzed. The ranking function is of the form where are the coefficients of `mu` corresponding to the space dimensions , respectively.

Returns:
  `true` if any loop approximated by `pset` definitely terminates; `false` if the test is inconclusive. However, if `pset` precisely characterizes the effect of the loop body onto the loop-relevant program variables, then `true` is returned if and only if the loop terminates.

template<typename PSET >

bool Parma_Polyhedra_Library::one_affine_ranking_function_MS_2 | ( | const PSET & | pset_before,
|  | const PSET & | pset_after,
|  | Generator & | mu
| ) |  |

Termination test with witness ranking function using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset_before | A pointset approximating the values of loop-relevant variables before the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions .
  pset_after | A pointset approximating the values of loop-relevant variables after the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions ,

Note that unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update. Note also that unprimed variables are assigned to different space dimensions in `pset_before` and `pset_after`.

Parameters:

  mu | When `true` is returned, this is assigned a point of space dimension encoding one (not further specified) affine ranking function for the loop being analyzed. The ranking function is of the form where are the coefficients of `mu` corresponding to the space dimensions , respectively.

Returns:
  `true` if any loop approximated by `pset` definitely terminates; `false` if the test is inconclusive. However, if `pset_before` and `pset_after` precisely characterize the effect of the loop body onto the loop-relevant program variables, then `true` is returned if and only if the loop terminates.

template<typename PSET >

void Parma_Polyhedra_Library::all_affine_ranking_functions_MS | ( | const PSET & | pset,
|  | C_Polyhedron & | mu_space
| ) |  |

Termination test with ranking function space using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions , where unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update.
  mu_space | This is assigned a closed polyhedron of space dimension representing the space of all the affine ranking functions for the loops that are precisely characterized by `pset`. These ranking functions are of the form where identify any point of the `mu_space` polyhedron. The variables correspond to the space dimensions of `mu_space` , respectively. When `mu_space` is empty, it means that the test is inconclusive. However, if `pset` precisely characterizes the effect of the loop body onto the loop-relevant program variables, then `mu_space` is empty if and only if the loop does not terminate.

template<typename PSET >

void Parma_Polyhedra_Library::all_affine_ranking_functions_MS_2 | ( | const PSET & | pset_before,
|  | const PSET & | pset_after,
|  | C_Polyhedron & | mu_space
| ) |  |

Termination test with ranking function space using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset_before | A pointset approximating the values of loop-relevant variables before the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions .
  pset_after | A pointset approximating the values of loop-relevant variables after the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions ,

Note that unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update. Note also that unprimed variables are assigned to different space dimensions in `pset_before` and `pset_after`.

Parameters:

  mu_space | This is assigned a closed polyhedron of space dimension representing the space of all the affine ranking functions for the loops that are precisely characterized by `pset`. These ranking functions are of the form where identify any point of the `mu_space` polyhedron. The variables correspond to the space dimensions of `mu_space` , respectively. When `mu_space` is empty, it means that the test is inconclusive. However, if `pset_before` and `pset_after` precisely characterize the effect of the loop body onto the loop-relevant program variables, then `mu_space` is empty if and only if the loop does not terminate.

template<typename PSET >

void Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS | ( | const PSET & | pset,
|  | C_Polyhedron & | decreasing_mu_space,
|  | C_Polyhedron & | bounded_mu_space
| ) |  |

Computes the spaces of affine quasi ranking functions using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions , where unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update.
  decreasing_mu_space | This is assigned a closed polyhedron of space dimension representing the space of all the decreasing affine functions for the loops that are precisely characterized by `pset`.
  bounded_mu_space | This is assigned a closed polyhedron of space dimension representing the space of all the lower bounded affine functions for the loops that are precisely characterized by `pset`.

These quasi-ranking functions are of the form where identify any point of the `decreasing_mu_space` and `bounded_mu_space` polyhedrons. The variables correspond to the space dimensions , respectively. When `decreasing_mu_space` (resp., `bounded_mu_space`) is empty, it means that the test is inconclusive. However, if `pset` precisely characterizes the effect of the loop body onto the loop-relevant program variables, then `decreasing_mu_space` (resp., `bounded_mu_space`) will be empty if and only if there is no decreasing (resp., lower bounded) affine function, so that the loop does not terminate.

template<typename PSET >

void Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS_2 | ( | const PSET & | pset_before,
|  | const PSET & | pset_after,
|  | C_Polyhedron & | decreasing_mu_space,
|  | C_Polyhedron & | bounded_mu_space
| ) |  |

Computes the spaces of affine quasi ranking functions using an improvement of the method by Mesnard and Serebrenik [BMPZ10].

Template Parameters:

  PSET | Any pointset supported by the PPL that provides the `minimized_constraints()` method.

Parameters:

  pset_before | A pointset approximating the values of loop-relevant variables before the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions .
  pset_after | A pointset approximating the values of loop-relevant variables after the update performed in the loop body that is being analyzed. The variables indices are allocated as follows: go onto space dimensions , go onto space dimensions ,

Note that unprimed variables represent the values of the loop-relevant program variables before the update performed in the loop body, and primed variables represent the values of those program variables after the update. Note also that unprimed variables are assigned to different space dimensions in `pset_before` and `pset_after`.

Parameters:

  decreasing_mu_space | This is assigned a closed polyhedron of space dimension representing the space of all the decreasing affine functions for the loops that are precisely characterized by `pset`.
  bounded_mu_space | This is assigned a closed polyhedron of space dimension representing the space of all the lower bounded affine functions for the loops that are precisely characterized by `pset`.

These ranking functions are of the form where identify any point of the `decreasing_mu_space` and `bounded_mu_space` polyhedrons. The variables correspond to the space dimensions , respectively. When `decreasing_mu_space` (resp., `bounded_mu_space`) is empty, it means that the test is inconclusive. However, if `pset_before` and `pset_after` precisely characterize the effect of the loop body onto the loop-relevant program variables, then `decreasing_mu_space` (resp., `bounded_mu_space`) will be empty if and only if there is no decreasing (resp., lower bounded) affine function, so that the loop does not terminate.

## Variable Documentation

const Throwable* volatile Parma_Polyhedra_Library::abandon_expensive_computations

A pointer to an exception object.

This pointer, which is initialized to zero, is repeatedly checked along any super-linear (i.e., computationally expensive) computation path in the library. When it is found nonzero the exception it points to is thrown. In other words, making this pointer point to an exception (and leaving it in this state) ensures that the library will return control to the client application, possibly by throwing the given exception, within a time that is a linear function of the size of the representation of the biggest object (powerset of polyhedra, polyhedron, system of constraints or generators) on which the library is operating upon.

Note:
  The only sensible way to assign to this pointer is from within a signal handler or from a parallel thread. For this reason, the library, apart from ensuring that the pointer is initially set to zero, never assigns to it. In particular, it does not zero it again when the exception is thrown: it is the client's responsibility to do so.