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

Namespaces
	Parma_Polyhedra_Library::IO_Operators
	All input/output operators are confined to this namespace.

	std
	The standard C++ namespace.

Classes
struct	Parma_Polyhedra_Library::Variable::Compare
	Binary predicate defining the total ordering on variables. More...

class	Parma_Polyhedra_Library::Variable
	A dimension of the vector space. 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::const_iterator

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::const_iterator
	An iterator over a system of congruences. More...

class	Parma_Polyhedra_Library::Congruence_System
	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::const_iterator
	A read-only iterator on the constraints defining the feasible region. More...

class	Parma_Polyhedra_Library::MIP_Problem
	A Mixed Integer (linear) Programming problem. More...

class	Parma_Polyhedra_Library::Grid_Generator_System::const_iterator
	An iterator over a system of grid generators. 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...

struct	Parma_Polyhedra_Library::BHRZ03_Certificate::Compare
	A total ordering on BHRZ03 certificates. More...

class	Parma_Polyhedra_Library::BHRZ03_Certificate
	The convergence certificate for the BHRZ03 widening operator. More...

struct	Parma_Polyhedra_Library::H79_Certificate::Compare
	A total ordering on H79 certificates. More...

class	Parma_Polyhedra_Library::H79_Certificate
	A convergence certificate for the H79 widening operator. More...

struct	Parma_Polyhedra_Library::Grid_Certificate::Compare
	A total ordering on Grid certificates. 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. More...

#define	PPL_VERSION_MINOR 2
	The minor number of the PPL version. More...

#define	PPL_VERSION_REVISION 0
	The revision number of the PPL version. More...

#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.2"
	A string containing the PPL version. More...

Typedefs
typedef size_t	Parma_Polyhedra_Library::dimension_type
	An unsigned integral type for representing space dimensions. More...

typedef size_t	Parma_Polyhedra_Library::memory_size_type
	An unsigned integral type for representing memory size in bytes. More...

typedef PPL_COEFFICIENT_TYPE	Parma_Polyhedra_Library::Coefficient
	An alias for easily naming the type of PPL coefficients. More...

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 }

enum	Parma_Polyhedra_Library::Bounded_Integer_Type_Representation { Parma_Polyhedra_Library::UNSIGNED, Parma_Polyhedra_Library::SIGNED_2_COMPLEMENT }

enum	Parma_Polyhedra_Library::Bounded_Integer_Type_Overflow { Parma_Polyhedra_Library::OVERFLOW_WRAPS, Parma_Polyhedra_Library::OVERFLOW_UNDEFINED, Parma_Polyhedra_Library::OVERFLOW_IMPOSSIBLE }

enum	Parma_Polyhedra_Library::Representation { Parma_Polyhedra_Library::DENSE, Parma_Polyhedra_Library::SPARSE }

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 }

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...

enum	Parma_Polyhedra_Library::Constraint::Type { Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY }
	The constraint type. More...

enum	Parma_Polyhedra_Library::Generator::Type { Parma_Polyhedra_Library::Generator::LINE, Parma_Polyhedra_Library::Generator::RAY, Parma_Polyhedra_Library::Generator::POINT, Parma_Polyhedra_Library::Generator::CLOSURE_POINT }
	The generator type. More...

enum	Parma_Polyhedra_Library::Grid_Generator::Kind
	The possible kinds of Grid_Generator objects.

enum	Parma_Polyhedra_Library::Grid_Generator::Type { Parma_Polyhedra_Library::Grid_Generator::LINE, Parma_Polyhedra_Library::Grid_Generator::PARAMETER, Parma_Polyhedra_Library::Grid_Generator::POINT }
	The generator type. More...

enum	Parma_Polyhedra_Library::MIP_Problem::Control_Parameter_Name { Parma_Polyhedra_Library::MIP_Problem::PRICING }
	Names of MIP problems' control parameters. More...

enum	Parma_Polyhedra_Library::MIP_Problem::Control_Parameter_Value { Parma_Polyhedra_Library::MIP_Problem::PRICING_STEEPEST_EDGE_FLOAT, Parma_Polyhedra_Library::MIP_Problem::PRICING_STEEPEST_EDGE_EXACT, Parma_Polyhedra_Library::MIP_Problem::PRICING_TEXTBOOK }
	Possible values for MIP problem's control parameters. More...

enum	Parma_Polyhedra_Library::PIP_Problem::Control_Parameter_Name { Parma_Polyhedra_Library::PIP_Problem::CUTTING_STRATEGY, Parma_Polyhedra_Library::PIP_Problem::PIVOT_ROW_STRATEGY }
	Possible names for PIP_Problem control parameters. More...

enum	Parma_Polyhedra_Library::PIP_Problem::Control_Parameter_Value { Parma_Polyhedra_Library::PIP_Problem::CUTTING_STRATEGY_FIRST, Parma_Polyhedra_Library::PIP_Problem::CUTTING_STRATEGY_DEEPEST, Parma_Polyhedra_Library::PIP_Problem::CUTTING_STRATEGY_ALL, Parma_Polyhedra_Library::PIP_Problem::PIVOT_ROW_STRATEGY_FIRST, Parma_Polyhedra_Library::PIP_Problem::PIVOT_ROW_STRATEGY_MAX_COLUMN }
	Possible values for PIP_Problem control parameters. More...

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

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)

Result_Relation	Parma_Polyhedra_Library::result_relation (Result 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)

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)

template<typename PSET >
bool	Parma_Polyhedra_Library::termination_test_MS_2 (const PSET &pset_before, const PSET &pset_after)

template<typename PSET >
bool	Parma_Polyhedra_Library::one_affine_ranking_function_MS (const PSET &pset, Generator &mu)

template<typename PSET >
bool	Parma_Polyhedra_Library::one_affine_ranking_function_MS_2 (const PSET &pset_before, const PSET &pset_after, Generator &mu)

template<typename PSET >
void	Parma_Polyhedra_Library::all_affine_ranking_functions_MS (const PSET &pset, C_Polyhedron &mu_space)

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)

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)

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)

template<typename PSET >
bool	Parma_Polyhedra_Library::termination_test_PR (const PSET &pset)

template<typename PSET >
bool	Parma_Polyhedra_Library::termination_test_PR_2 (const PSET &pset_before, const PSET &pset_after)

template<typename PSET >
bool	Parma_Polyhedra_Library::one_affine_ranking_function_PR (const PSET &pset, Generator &mu)

template<typename PSET >
bool	Parma_Polyhedra_Library::one_affine_ranking_function_PR_2 (const PSET &pset_before, const PSET &pset_after, Generator &mu)

template<typename PSET >
void	Parma_Polyhedra_Library::all_affine_ranking_functions_PR (const PSET &pset, NNC_Polyhedron &mu_space)

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)

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 2

The minor number of the PPL version.

#define PPL_VERSION_REVISION 0

The revision number of the PPL version.

#define PPL_VERSION "1.2"

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 $-\infty$ .
ROUND_UP	Round toward $+\infty$ .
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 $w$ -bit bounded integer, the computation happens modulo $2^w$ .

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.

enum Parma_Polyhedra_Library::Constraint::Type

The constraint type.

Enumerator
EQUALITY	The constraint is an equality.
NONSTRICT_INEQUALITY	The constraint is a non-strict inequality.
STRICT_INEQUALITY	The constraint is a strict inequality.

enum Parma_Polyhedra_Library::Generator::Type

The generator type.

Enumerator
LINE	The generator is a line.
RAY	The generator is a ray.
POINT	The generator is a point.
CLOSURE_POINT	The generator is a closure point.

enum Parma_Polyhedra_Library::Grid_Generator::Type

The generator type.

Enumerator
LINE	The generator is a grid line.
PARAMETER	The generator is a parameter.
POINT	The generator is a grid point.

enum Parma_Polyhedra_Library::MIP_Problem::Control_Parameter_Name

Names of MIP problems' control parameters.

Enumerator
PRICING	The pricing rule.

enum Parma_Polyhedra_Library::MIP_Problem::Control_Parameter_Value

Possible values for MIP problem's control parameters.

Enumerator
PRICING_STEEPEST_EDGE_FLOAT	Steepest edge pricing method, using floating points (default).
PRICING_STEEPEST_EDGE_EXACT	Steepest edge pricing method, using Coefficient.
PRICING_TEXTBOOK	Textbook pricing method.

enum Parma_Polyhedra_Library::PIP_Problem::Control_Parameter_Name

Possible names for PIP_Problem control parameters.

Enumerator
CUTTING_STRATEGY	Cutting strategy.
PIVOT_ROW_STRATEGY	Pivot row strategy.

enum Parma_Polyhedra_Library::PIP_Problem::Control_Parameter_Value

Possible values for PIP_Problem control parameters.

Enumerator
CUTTING_STRATEGY_FIRST	Choose the first non-integer row.
CUTTING_STRATEGY_DEEPEST	Choose row which generates the deepest cut.
CUTTING_STRATEGY_ALL	Always generate all possible cuts.
PIVOT_ROW_STRATEGY_FIRST	Choose the first row with negative parameter sign.
PIVOT_ROW_STRATEGY_MAX_COLUMN	Choose a row that generates a lexicographically maximal pivot column.

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:

$x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ ,
$x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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: $x_1, \ldots, x_n$ go onto space dimensions $0, \ldots, n-1$ .
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: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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:

$x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ ,
$x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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 $\mu_0 + \sum_{i=1}^n \mu_i x_i$ where $\mu_0, \mu_1, \ldots, \mu_n$ are the coefficients of mu corresponding to the space dimensions $n, 0, \ldots, n-1$ , 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: $x_1, \ldots, x_n$ go onto space dimensions $0, \ldots, n-1$ .
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: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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 $\mu_0 + \sum_{i=1}^n \mu_i x_i$ where $\mu_0, \mu_1, \ldots, \mu_n$ are the coefficients of mu corresponding to the space dimensions $n, 0, \ldots, n-1$ , 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:

$x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ ,
$x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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 $\mu_0 + \sum_{i=1}^n \mu_i x_i$ where $\mu_0, \mu_1, \ldots, \mu_n$ identify any point of the mu_space polyhedron. The variables $\mu_0, \mu_1, \ldots, \mu_n$ correspond to the space dimensions of mu_space $n, 0, \ldots, n-1$ , 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: $x_1, \ldots, x_n$ go onto space dimensions $0, \ldots, n-1$ .
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: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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 $\mu_0 + \sum_{i=1}^n \mu_i x_i$ where $\mu_0, \mu_1, \ldots, \mu_n$ identify any point of the mu_space polyhedron. The variables $\mu_0, \mu_1, \ldots, \mu_n$ correspond to the space dimensions of mu_space $n, 0, \ldots, n-1$ , 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: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ , 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 $\mu_0 + \sum_{i=1}^n \mu_i x_i$ where $\mu_0, \mu_1, \ldots, \mu_n$ identify any point of the decreasing_mu_space and bounded_mu_space polyhedrons. The variables $\mu_0, \mu_1, \ldots, \mu_n$ correspond to the space dimensions $n, 0, \ldots, n-1$ , 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: $x_1, \ldots, x_n$ go onto space dimensions $0, \ldots, n-1$ .
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: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ ,

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 $\mu_0 + \sum_{i=1}^n \mu_i x_i$ where $\mu_0, \mu_1, \ldots, \mu_n$ identify any point of the decreasing_mu_space and bounded_mu_space polyhedrons. The variables $\mu_0, \mu_1, \ldots, \mu_n$ correspond to the space dimensions $n, 0, \ldots, n-1$ , 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.

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].

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.

Namespaces

Classes

Macros

Typedefs

Enumerations

Variables

Functions Inspecting and/or Combining Result Values

Functions Inspecting and/or Combining Rounding_Dir Values

Functions for the Synthesis of Linear Rankings

Detailed Description

Macro Definition Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation

Variable Documentation