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	Parma_Polyhedra_Library::Checked
	Types and functions implementing checked numbers.
namespace	Parma_Polyhedra_Library::Implementation
	Implementation related data and functions.
namespace	std
	The standard C++ namespace.

Classes
class	Parma_Polyhedra_Library::Affine_Space
	An affine space. More...
class	Parma_Polyhedra_Library::Any_Pointset
	Any PPL pointset. More...
class	Parma_Polyhedra_Library::Ask_Tell_Pair< D >
	A pair of ask and tell descriptions. More...
class	Parma_Polyhedra_Library::BD_Shape< T >
	A bounded difference shape. More...
class	Parma_Polyhedra_Library::BD_Shape< T >::Status
	A conjunctive assertion about a BD_Shape<T> object. More...
class	Parma_Polyhedra_Library::BHRZ03_Certificate
	The convergence certificate for the BHRZ03 widening operator. More...
struct	Parma_Polyhedra_Library::BHRZ03_Certificate::Compare
	A total ordering on BHRZ03 certificates. More...
class	Parma_Polyhedra_Library::Bit_Matrix
	A matrix of bits. More...
struct	Parma_Polyhedra_Library::Bit_Matrix::Bit_Row_Less_Than
	Ordering predicate (used when implementing the sort algorithm). More...
class	Parma_Polyhedra_Library::Bit_Row
	A row in a matrix of bits. More...
class	Parma_Polyhedra_Library::Box< ITV >
	A not necessarily closed, iso-oriented hyperrectangle. More...
class	Parma_Polyhedra_Library::C_Polyhedron
	A closed convex polyhedron. More...
class	Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >
	A generic Cast Floating Point Expression. More...
struct	Parma_Polyhedra_Library::Checked_Number_Transparent_Policy< T >
struct	Parma_Polyhedra_Library::Extended_Number_Policy
struct	Parma_Polyhedra_Library::Check_Overflow_Policy< T >
	A policy checking for overflows. More...
struct	Parma_Polyhedra_Library::Native_Checked_From_Wrapper< T, typename Enable_If< Is_Native< T >::value >::type >
struct	Parma_Polyhedra_Library::Native_Checked_From_Wrapper< Checked_Number< T, P > >
struct	Parma_Polyhedra_Library::Native_Checked_To_Wrapper< T, typename Enable_If< Is_Native< T >::value >::type >
struct	Parma_Polyhedra_Library::Native_Checked_To_Wrapper< Checked_Number< T, P > >
struct	Parma_Polyhedra_Library::Is_Checked< T >
struct	Parma_Polyhedra_Library::Is_Checked< Checked_Number< T, P > >
struct	Parma_Polyhedra_Library::Is_Native_Or_Checked< T >
class	Parma_Polyhedra_Library::Checked_Number< T, Policy >
	A wrapper for numeric types implementing a given policy. More...
struct	Parma_Polyhedra_Library::Slow_Copy< Checked_Number< T, P > >
class	Parma_Polyhedra_Library::CO_Tree
	A cache-oblivious binary search tree of pairs. More...
struct	Parma_Polyhedra_Library::Coefficient_traits_template< Coefficient >
	Coefficient traits. More...
class	Parma_Polyhedra_Library::Congruence
	A linear congruence. 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::Constant_Floating_Point_Expression< FP_Interval_Type, FP_Format >
	A generic Constant Floating Point Expression. More...
class	Parma_Polyhedra_Library::Constraint
	A linear equality or inequality. 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::DB_Matrix< T >
	The base class for the square matrices. More...
class	Parma_Polyhedra_Library::DB_Row_Impl_Handler< T >
	The handler of the actual DB_Row implementation. More...
class	Parma_Polyhedra_Library::DB_Row< T >
	The base class for the single rows of matrices. More...
class	Parma_Polyhedra_Library::DB_Row_Impl_Handler< T >::Impl
	The real implementation of a DB_Row object. More...
class	Parma_Polyhedra_Library::Dense_Row
	A finite sequence of coefficients. 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::Determinate< PSET >::Binary_Operator_Assign_Lifter< Binary_Operator_Assign >
	A function adapter for the Determinate class. More...
class	Parma_Polyhedra_Library::Determinate< PSET >::Rep
	The possibly shared representation of a Determinate object. 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::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >
	A generic Division Floating Point Expression. More...
struct	Parma_Polyhedra_Library::float_ieee754_half
struct	Parma_Polyhedra_Library::float_ieee754_single
struct	Parma_Polyhedra_Library::float_ieee754_double
struct	Parma_Polyhedra_Library::float_ibm_single
struct	Parma_Polyhedra_Library::float_ibm_double
struct	Parma_Polyhedra_Library::float_intel_double_extended
struct	Parma_Polyhedra_Library::float_ieee754_quad
class	Parma_Polyhedra_Library::Float< T >
class	Parma_Polyhedra_Library::Generator
	A line, ray, point or closure point. 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...
struct	Parma_Polyhedra_Library::Weightwatch_Traits
	Traits class for the deterministic timeout mechanism. More...
class	Parma_Polyhedra_Library::Throwable
	User objects the PPL can throw. More...
struct	Parma_Polyhedra_Library::Recycle_Input
	A tag class. More...
struct	Parma_Polyhedra_Library::Coefficient_traits_template< GMP_Integer >
	Coefficient traits specialization for unbounded integers. More...
class	Parma_Polyhedra_Library::Grid
	A grid. More...
class	Parma_Polyhedra_Library::Grid_Certificate
	The convergence certificate for the Grid widening operator. More...
class	Parma_Polyhedra_Library::Grid_Generator
	A grid line, parameter or grid point. More...
class	Parma_Polyhedra_Library::Grid_Generator_System
	A system of grid generators. More...
class	Parma_Polyhedra_Library::H79_Certificate
	A convergence certificate for the H79 widening operator. More...
struct	Parma_Polyhedra_Library::Has_Assign_Or_Swap< T, Enable >
struct	Parma_Polyhedra_Library::Has_Assign_Or_Swap< T, typename Enable_If_Is< void(T::*)(T &x),&T::assign_or_swap >::type >
class	Parma_Polyhedra_Library::Init
	Class for initialization and finalization. More...
class	Parma_Polyhedra_Library::Interval< Boundary, Info >
	A generic, not necessarily closed, possibly restricted interval. More...
class	Parma_Polyhedra_Library::iterator_to_const< Container >
	An iterator on a sequence of read-only objects. More...
class	Parma_Polyhedra_Library::const_iterator_to_const< Container >
	A const_iterator on a sequence of read-only objects. More...
class	Parma_Polyhedra_Library::Linear_Expression
	A linear expression. More...
class	Parma_Polyhedra_Library::Linear_Expression_Impl< Row >
	A linear expression. More...
class	Parma_Polyhedra_Library::Linear_Expression_Interface
	A linear expression. More...
class	Parma_Polyhedra_Library::Linear_Form< C >
	A linear form with interval coefficients. More...
class	Parma_Polyhedra_Library::Linear_System< Row >
	The base class for systems of constraints and generators. More...
struct	Parma_Polyhedra_Library::Linear_System< Row >::With_Pending
	A tag class. More...
struct	Parma_Polyhedra_Library::Compile_Time_Check< true >
	A class that is only defined if `b` evaluates to `true`. More...
struct	Parma_Polyhedra_Library::Bool< b >
	A class holding a constant called `value` that evaluates to `b`. More...
struct	Parma_Polyhedra_Library::True
	A class holding a constant called `value` that evaluates to `true`. More...
struct	Parma_Polyhedra_Library::False
	A class holding a constant called `value` that evaluates to `false`. More...
struct	Parma_Polyhedra_Library::Is_Same< T1, T2 >
	A class holding a constant called `value` that evaluates to `true` if and only if `T1` is the same type as `T2`. More...
struct	Parma_Polyhedra_Library::Is_Same< T, T >
	A class holding a constant called `value` that evaluates to `true` if and only if `T1` is the same type as `T2`. More...
struct	Parma_Polyhedra_Library::Is_Same_Or_Derived< Base, Derived >
	A class holding a constant called `value` that evaluates to `true` if and only if `Base` is the same type as `Derived` or `Derived` is a class derived from `Base`. More...
struct	Parma_Polyhedra_Library::Enable_If< b, T >
	A class that provides a type member called `type` equivalent to `T` if and only if `b` is `true`. More...
struct	Parma_Polyhedra_Library::Enable_If< true, T >
	A class that provides a type member called `type` equivalent to `T` if and only if `b` is `true`. More...
class	Parma_Polyhedra_Library::MIP_Problem
	A Mixed Integer (linear) Programming problem. 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::NNC_Polyhedron
	A not necessarily closed convex polyhedron. More...
class	Parma_Polyhedra_Library::Octagonal_Shape< T >
	An octagonal shape. 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::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::PIP_Problem
	A Parametric Integer (linear) Programming problem. More...
class	Parma_Polyhedra_Library::Pointset_Ask_Tell< PSET >
	The ask-and-tell construction instantiated on PPL polyhedra. More...
class	Parma_Polyhedra_Library::Pointset_Powerset< PSET >
	The powerset construction instantiated on PPL pointset domains. More...
class	Parma_Polyhedra_Library::Poly_Con_Relation
	The relation between a polyhedron and a constraint. 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::Powerset< D >
	The powerset construction on a base-level domain. More...
class	Parma_Polyhedra_Library::Scalar_Products
	A class implementing various scalar product functions. More...
class	Parma_Polyhedra_Library::Topology_Adjusted_Scalar_Product_Sign
	Scalar product sign function object depending on topology. More...
struct	Parma_Polyhedra_Library::Slow_Copy< T >
struct	Parma_Polyhedra_Library::Slow_Copy< mpz_class >
struct	Parma_Polyhedra_Library::Slow_Copy< mpq_class >
class	Parma_Polyhedra_Library::Sparse_Row
	A finite sparse sequence of coefficients. 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::Variable
	A dimension of the vector space. 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::Widening_Function< PSET >
	Wraps a widening method into a function object. More...
class	Parma_Polyhedra_Library::Limited_Widening_Function< PSET, CSYS >
	Wraps a limited widening method into a function object. More...
struct	Parma_Polyhedra_Library::WRD_Extended_Number_Policy
	The production policy for checked numbers used in weakly-relational domains. More...
struct	Parma_Polyhedra_Library::Debug_WRD_Extended_Number_Policy
	The debugging policy for checked numbers used in weakly-relational domains. 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.
#define	const_bool_nodef(name, value) enum const_bool_value_ ## name { PPL_U(name) = (value) }
	Declares a per-class constant of type `bool`, called `name` and with value `value`.
#define	const_int_nodef(name, value) enum anonymous_enum_ ## name { PPL_U(name) = (value) }
	Declares a per-class constant of type `int`, called `name` and with value `value`.
#define	const_value_nodef(type, name, value)
	Declares a per-class constant of type `type`, called `name` and with value `value`. The value of the constant is accessible by means of the syntax `name()`.
#define	const_ref_nodef(type, name, value)
	Declares a per-class constant of type `type`, called `name` and with value `value`. A constant reference to the constant is accessible by means of the syntax `name()`.
#define	PPL_COMPILE_TIME_CHECK(e, msg) PPL_COMPILE_TIME_CHECK_AUX(e, __LINE__)
	Produces a compilation error if the compile-time constant `e` does not evaluate to `true`

Typedefs
typedef PPL_COEFFICIENT_TYPE	Parma_Polyhedra_Library::Coefficient
	An alias for easily naming the type of PPL coefficients.
typedef Coefficient_traits_template < Coefficient >	Parma_Polyhedra_Library::Coefficient_traits
	An alias for easily naming the coefficient traits.
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.

Enumerations
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::I_Result { Parma_Polyhedra_Library::I_EMPTY, Parma_Polyhedra_Library::I_SINGLETON, Parma_Polyhedra_Library::I_SOME, Parma_Polyhedra_Library::I_UNIVERSE, Parma_Polyhedra_Library::I_NOT_EMPTY, Parma_Polyhedra_Library::I_ANY, Parma_Polyhedra_Library::I_NOT_UNIVERSE, Parma_Polyhedra_Library::I_NOT_DEGENERATE, Parma_Polyhedra_Library::I_EXACT, Parma_Polyhedra_Library::I_INEXACT, Parma_Polyhedra_Library::I_CHANGED, Parma_Polyhedra_Library::I_UNCHANGED, Parma_Polyhedra_Library::I_SINGULARITIES }
	The result of an operation on intervals. 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::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::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_NATIVE = ROUND_IGNORE, Parma_Polyhedra_Library::ROUND_NOT_NEEDED, Parma_Polyhedra_Library::ROUND_DIRECT = ROUND_UP, Parma_Polyhedra_Library::ROUND_INVERSE = ROUND_DOWN, Parma_Polyhedra_Library::ROUND_DIR_MASK = 7U, Parma_Polyhedra_Library::ROUND_STRICT_RELATION, Parma_Polyhedra_Library::ROUND_CHECK = ROUND_DIRECT \| ROUND_STRICT_RELATION }
	Rounding directions for arithmetic computations. More...
enum	Parma_Polyhedra_Library::Topology { Parma_Polyhedra_Library::NECESSARILY_CLOSED = 0, Parma_Polyhedra_Library::NOT_NECESSARILY_CLOSED = 1 }
	Kinds of polyhedra domains. More...

Functions
template<typename T >
Enable_If< Has_Assign_Or_Swap < T >::value, void >::type	Parma_Polyhedra_Library::assign_or_swap (T &to, T &from)

Variables
const Throwable *volatile	Parma_Polyhedra_Library::abandon_expensive_computations = 0
	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 const_bool_nodef	(	name,
		value
	)	enum const_bool_value_ ## name { PPL_U(name) = (value) }

Declares a per-class constant of type bool, called name and with value value.

Differently from static constants, name needs not (and cannot) be defined (for static constants, the need for a further definition is mandated by Section 9.4.2/4 of the C++ standard).

Definition at line 42 of file meta_programming.hh.

#define const_int_nodef	(	name,
		value
	)	enum anonymous_enum_ ## name { PPL_U(name) = (value) }

Declares a per-class constant of type int, called name and with value value.

Differently from static constants, name needs not (and cannot) be defined (for static constants, the need for a further definition is mandated by Section 9.4.2/4 of the C++ standard).

Definition at line 56 of file meta_programming.hh.

#define const_ref_nodef	(	type,
		name,
		value
	)

Value:

static const type& PPL_U(name)() {                                    \
    static type PPL_U(name) = (value);                                       \
    return (name);                                                      \
  }

Declares a per-class constant of type type, called name and with value value. A constant reference to the constant is accessible by means of the syntax name().

Differently from static constants, name needs not (and cannot) be defined (for static constants, the need for a further definition is mandated by Section 9.4.2/4 of the C++ standard).

Definition at line 88 of file meta_programming.hh.

#define const_value_nodef	(	type,
		name,
		value
	)

Value:

static type PPL_U(name)() {                   \
    return (value);                             \
  }

Declares a per-class constant of type type, called name and with value value. The value of the constant is accessible by means of the syntax name().

Differently from static constants, name needs not (and cannot) be defined (for static constants, the need for a further definition is mandated by Section 9.4.2/4 of the C++ standard).

Definition at line 71 of file meta_programming.hh.

#define PPL_COMPILE_TIME_CHECK	(	e,
		msg
	)	PPL_COMPILE_TIME_CHECK_AUX(e, __LINE__)

Produces a compilation error if the compile-time constant e does not evaluate to true

Definition at line 133 of file meta_programming.hh.

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

Definition at line 59 of file version.hh.

#define PPL_VERSION_BETA 0

The beta number of the PPL version. This is zero for official releases and nonzero for development snapshots.

Definition at line 45 of file version.hh.

Referenced by Parma_Polyhedra_Library::version_beta().

#define PPL_VERSION_MAJOR 1

The major number of the PPL version.

Definition at line 30 of file version.hh.

Referenced by Parma_Polyhedra_Library::version_major().

#define PPL_VERSION_MINOR 0

The minor number of the PPL version.

Definition at line 34 of file version.hh.

Referenced by Parma_Polyhedra_Library::version_minor().

#define PPL_VERSION_REVISION 0

The revision number of the PPL version.

Definition at line 38 of file version.hh.

Referenced by Parma_Polyhedra_Library::version_revision().

Typedef Documentation

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

Definition at line 172 of file Coefficient.types.hh.

typedef Coefficient_traits_template<Coefficient> Parma_Polyhedra_Library::Coefficient_traits

An alias for easily naming the coefficient traits.

Definition at line 178 of file Coefficient.types.hh.

typedef size_t Parma_Polyhedra_Library::dimension_type

An unsigned integral type for representing space dimensions.

Definition at line 22 of file globals.types.hh.

typedef size_t Parma_Polyhedra_Library::memory_size_type

An unsigned integral type for representing memory size in bytes.

Definition at line 26 of file globals.types.hh.

Enumeration Type Documentation

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.

Definition at line 121 of file globals.types.hh.

                                   {
  OVERFLOW_WRAPS,
  OVERFLOW_UNDEFINED,
  OVERFLOW_IMPOSSIBLE
};

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.

Definition at line 104 of file globals.types.hh.

                                         {
  UNSIGNED,
  SIGNED_2_COMPLEMENT
};

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.

Definition at line 81 of file globals.types.hh.

                                {
  BITS_8 = 8,
  BITS_16 = 16,
  BITS_32 = 32,
  BITS_64 = 64,
  BITS_128 = 128
};

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.

Definition at line 57 of file globals.types.hh.

                      {
  POLYNOMIAL_COMPLEXITY,
  SIMPLEX_COMPLEXITY,
  ANY_COMPLEXITY
};

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.

Definition at line 30 of file globals.types.hh.

                        {
  UNIVERSE,
  EMPTY
};

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

Definition at line 187 of file globals.types.hh.

                           {
  IEEE754_HALF,
  IEEE754_SINGLE,
  IEEE754_DOUBLE,
  IEEE754_QUAD,
  INTEL_DOUBLE_EXTENDED,
  IBM_SINGLE,
  IBM_DOUBLE
};

enum Parma_Polyhedra_Library::I_Result

The result of an operation on intervals.

Enumerator:

I_EMPTY	Result may be empty.
I_SINGLETON	Result may have only one value.
I_SOME	Result may have more than one value, but it is not the domain universe.
I_UNIVERSE	Result may be the domain universe.
I_NOT_EMPTY	Result is not empty.
I_ANY	Result may be empty or not empty.
I_NOT_UNIVERSE	Result may be empty or not empty.
I_NOT_DEGENERATE	Result is neither empty nor the domain universe.
I_EXACT	Result is definitely exact.
I_INEXACT	Result is definitely inexact.
I_CHANGED	Operation has definitely changed the set.
I_UNCHANGED	Operation has left the set definitely unchanged.
I_SINGULARITIES	Operation is undefined for some combination of values.

Definition at line 38 of file intervals.defs.hh.

              {
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_EMPTY = 1U,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_SINGLETON = 2U,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_SOME = 4U,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_UNIVERSE = 8U,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_NOT_EMPTY = I_SINGLETON | I_SOME | I_UNIVERSE,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_ANY = I_EMPTY | I_NOT_EMPTY,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_NOT_UNIVERSE = I_EMPTY | I_SINGLETON | I_SOME,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_NOT_DEGENERATE = I_SINGLETON | I_SOME,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_EXACT = 16,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_INEXACT = 32,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_CHANGED = 64,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_UNCHANGED = 128,
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  I_SINGULARITIES = 256
};

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.

Definition at line 20 of file MIP_Problem.types.hh.

                        {
  UNFEASIBLE_MIP_PROBLEM,
  UNBOUNDED_MIP_PROBLEM,
  OPTIMIZED_MIP_PROBLEM
};

enum Parma_Polyhedra_Library::Optimization_Mode

Possible optimization modes.

Enumerator:

MINIMIZATION	Minimization is requested.
MAXIMIZATION	Maximization is requested.

Definition at line 68 of file globals.types.hh.

                       {
  MINIMIZATION,
  MAXIMIZATION
};

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.

Definition at line 20 of file PIP_Problem.types.hh.

                        {
  UNFEASIBLE_PIP_PROBLEM,
  OPTIMIZED_PIP_PROBLEM
};

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.

Definition at line 40 of file globals.types.hh.

                     {
  EQUAL = 1U,
  LESS_THAN = 2U,
  LESS_OR_EQUAL = LESS_THAN | EQUAL,
  GREATER_THAN = 4U,
  GREATER_OR_EQUAL = GREATER_THAN | EQUAL,
  NOT_EQUAL = LESS_THAN | GREATER_THAN
};

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

Definition at line 161 of file globals.types.hh.

                    {
  DENSE,
  SPARSE
};

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.

Definition at line 76 of file Result.defs.hh.

            {
  V_EMPTY = VR_EMPTY,
  V_EQ = static_cast<unsigned>(VR_EQ),
  V_LT = static_cast<unsigned>(VR_LT),
  V_GT = static_cast<unsigned>(VR_GT),
  V_NE = VR_NE,
  V_LE = VR_LE,
  V_GE = VR_GE,
  V_LGE = VR_LGE,
  V_OVERFLOW = 1U << 6,
  V_LT_INF = V_LT | V_OVERFLOW,
  V_GT_SUP = V_GT | V_OVERFLOW,
  V_LT_PLUS_INFINITY = V_LT | static_cast<unsigned>(VC_PLUS_INFINITY),
  V_GT_MINUS_INFINITY = V_GT | static_cast<unsigned>(VC_MINUS_INFINITY),
  V_EQ_MINUS_INFINITY = V_EQ | static_cast<unsigned>(VC_MINUS_INFINITY),
  V_EQ_PLUS_INFINITY = V_EQ | static_cast<unsigned>(VC_PLUS_INFINITY),
  V_NAN = static_cast<unsigned>(VC_NAN),
  V_CVT_STR_UNK = V_NAN | (1U << 8),
  V_DIV_ZERO = V_NAN | (2U << 8),
  V_INF_ADD_INF = V_NAN | (3U << 8),
  V_INF_DIV_INF = V_NAN | (4U << 8),
  V_INF_MOD = V_NAN | (5U << 8),
  V_INF_MUL_ZERO = V_NAN | (6U << 8),
  V_INF_SUB_INF = V_NAN | (7U << 8),
  V_MOD_ZERO = V_NAN | (8U << 8),
  V_SQRT_NEG = V_NAN | (9U << 8),
  V_UNKNOWN_NEG_OVERFLOW = V_NAN | (10U << 8),
  V_UNKNOWN_POS_OVERFLOW = V_NAN | (11U << 8),
  V_UNREPRESENTABLE = 1U << 7
};

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_NATIVE
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_DIRECT
ROUND_INVERSE
ROUND_DIR_MASK
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.
ROUND_CHECK

Definition at line 34 of file Rounding_Dir.defs.hh.

                  {
  ROUND_DOWN = 0U,
  ROUND_UP = 1U,
  ROUND_IGNORE = 6U,
  ROUND_NATIVE = ROUND_IGNORE,
  ROUND_NOT_NEEDED = 7U,
  ROUND_DIRECT = ROUND_UP,
  ROUND_INVERSE = ROUND_DOWN,
  ROUND_DIR_MASK = 7U,
  ROUND_STRICT_RELATION = 8U,
  ROUND_CHECK = ROUND_DIRECT | ROUND_STRICT_RELATION
};

enum Parma_Polyhedra_Library::Topology

Kinds of polyhedra domains.

Enumerator:

NECESSARILY_CLOSED
NOT_NECESSARILY_CLOSED

Definition at line 22 of file Topology.types.hh.

              {
  NECESSARILY_CLOSED = 0,
  NOT_NECESSARILY_CLOSED = 1
};

Function Documentation

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.

Definition at line 353 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::all_affine_quasi_ranking_functions_MS(), Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::UNIVERSE.

                                                                      {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::all_affine_quasi_ranking_functions_MS"
      << "(pset, decr_space, bounded_space):\n"
      << "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  if (pset.is_empty()) {
    decreasing_mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE);
    bounded_mu_space = decreasing_mu_space;
    return;
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  all_affine_quasi_ranking_functions_MS(cs,
                                        decreasing_mu_space,
                                        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
	)

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.

Definition at line 382 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::all_affine_quasi_ranking_functions_MS(), Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::UNIVERSE.

                                                                        {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::all_affine_quasi_ranking_functions_MS_2"
      << "(pset_before, pset_after, decr_space, bounded_space):\n"
      << "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  if (pset_before.is_empty()) {
    decreasing_mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE);
    bounded_mu_space = decreasing_mu_space;
    return;
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  Termination_Helpers
    ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
  all_affine_quasi_ranking_functions_MS(cs,
                                        decreasing_mu_space,
                                        bounded_mu_space);
}

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.

Definition at line 301 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_MS(), Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::UNIVERSE.

                                                                          {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::all_affine_ranking_functions_MS(pset, mu_space):\n"
         "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  if (pset.is_empty()) {
    mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE);
    return;
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  all_affine_ranking_functions_MS(cs, 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
	)

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.

Definition at line 324 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_MS(), Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::UNIVERSE.

                                                          {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::all_affine_ranking_functions_MS_2"
      << "(pset_before, pset_after, mu_space):\n"
      << "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  if (pset_before.is_empty()) {
    mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE);
    return;
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  Termination_Helpers
    ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
  all_affine_ranking_functions_MS(cs, mu_space);
}

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

Definition at line 528 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_PR_original(), and Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation().

                                                          {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::all_affine_ranking_functions_PR(pset, mu_space):\n"
      << "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  if (pset.is_empty()) {
    mu_space = NNC_Polyhedron(1 + space_dim/2);
    return;
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  all_affine_ranking_functions_PR_original(cs, 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
	)

Like all_affine_ranking_functions_MS_2() but using an alternative formalization of the method by Podelski and Rybalchenko [BMPZ10].

Definition at line 498 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_PR(), and Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation().

                                                            {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::all_affine_ranking_functions_MS_2"
      << "(pset_before, pset_after, mu_space):\n"
      << "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  if (pset_before.is_empty()) {
    mu_space = NNC_Polyhedron(1 + before_space_dim);
    return;
  }
  using namespace Implementation::Termination;
  Constraint_System cs_before;
  Constraint_System cs_after;
  assign_all_inequalities_approximation(pset_before, cs_before);
  assign_all_inequalities_approximation(pset_after, cs_after);
  all_affine_ranking_functions_PR(cs_before, cs_after, mu_space);
}

template<typename T >

Enable_If<!Has_Assign_Or_Swap< T >::value &&Slow_Copy< T >::value, void >::type Parma_Polyhedra_Library::assign_or_swap	(	T &	to,
		T &	from
	)

inline

If there is an assign_or_swap() method, use it.

If there is no assign_or_swap() method but copies are not slow, copy.

If there is no assign_or_swap() and copies are slow, delegate to swap().

Definition at line 40 of file assign_or_swap.hh.

                               {
  to.assign_or_swap(from);
}

Rounding_Dir Parma_Polyhedra_Library::inverse ( Rounding_Dir dir )

inline

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

Definition at line 125 of file Rounding_Dir.inlines.hh.

References PPL_UNREACHABLE, Parma_Polyhedra_Library::round_dir(), Parma_Polyhedra_Library::ROUND_DOWN, Parma_Polyhedra_Library::ROUND_IGNORE, Parma_Polyhedra_Library::ROUND_STRICT_RELATION, and Parma_Polyhedra_Library::ROUND_UP.

                          {
  switch (round_dir(dir)) {
  case ROUND_UP:
    return ROUND_DOWN | (dir & ROUND_STRICT_RELATION);
  case ROUND_DOWN:
    return ROUND_UP | (dir & ROUND_STRICT_RELATION);
  case ROUND_IGNORE:
    return dir;
  default:
    PPL_UNREACHABLE;
    return dir;
  }
}

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.

Definition at line 260 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::one_affine_ranking_function_MS().

                                                                {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::one_affine_ranking_function_MS(pset, mu):\n"
         "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  return one_affine_ranking_function_MS(cs, mu);
}

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.

Definition at line 278 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::one_affine_ranking_function_MS().

                                                {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::one_affine_ranking_function_MS_2(pset_before, pset_after, mu):\n"
         "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  Termination_Helpers
    ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
  return one_affine_ranking_function_MS(cs, mu);
}

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

Definition at line 480 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::one_affine_ranking_function_PR_original().

                                                                {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::one_affine_ranking_function_PR(pset, mu):\n"
      << "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  return one_affine_ranking_function_PR_original(cs, mu);
}

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

Definition at line 455 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::one_affine_ranking_function_PR().

                                                {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::one_affine_ranking_function_PR_2"
      << "(pset_before, pset_after, mu):\n"
      << "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs_before;
  Constraint_System cs_after;
  assign_all_inequalities_approximation(pset_before, cs_before);
  assign_all_inequalities_approximation(pset_after, cs_after);
  return one_affine_ranking_function_PR(cs_before, cs_after, mu);
}

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

inline

Definition at line 33 of file Rounding_Dir.inlines.hh.

                                          {
  unsigned res = static_cast<unsigned>(x) & static_cast<unsigned>(y);
  return static_cast<Rounding_Dir>(res);
}

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

inline

Definition at line 33 of file Result.inlines.hh.

                              {
  unsigned res = static_cast<unsigned>(x) & static_cast<unsigned>(y);
  return static_cast<Result>(res);
}

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

inline

Definition at line 47 of file Result.inlines.hh.

                              {
  Result y_neg = static_cast<Result>(~static_cast<unsigned>(y));
  return x & y_neg;
}

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

inline

Definition at line 40 of file Rounding_Dir.inlines.hh.

                                          {
  unsigned res = static_cast<unsigned>(x) | static_cast<unsigned>(y);
  return static_cast<Rounding_Dir>(res);
}

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

inline

Definition at line 40 of file Result.inlines.hh.

                              {
  unsigned res = static_cast<unsigned>(x) | static_cast<unsigned>(y);
  return static_cast<Result>(res);
}

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

Definition at line 54 of file Result.inlines.hh.

References Parma_Polyhedra_Library::VC_MASK.

Referenced by Parma_Polyhedra_Library::Extended_Number_Policy::handle_result(), Parma_Polyhedra_Library::WRD_Extended_Number_Policy::handle_result(), Parma_Polyhedra_Library::Debug_WRD_Extended_Number_Policy::handle_result(), Parma_Polyhedra_Library::Checked::idiv_float(), Parma_Polyhedra_Library::Checked::input_mpq(), and Parma_Polyhedra_Library::result_overflow().

                       {
  Result rc = r & static_cast<Result>(VC_MASK);
  return static_cast<Result_Class>(rc);
}

Result_Relation Parma_Polyhedra_Library::result_relation ( Result r )

inline

Extracts the relation part of r.

Definition at line 61 of file Result.inlines.hh.

References Parma_Polyhedra_Library::VR_MASK.

Referenced by Parma_Polyhedra_Library::DB_Matrix< T >::ascii_load(), Parma_Polyhedra_Library::OR_Matrix< T >::ascii_load(), Parma_Polyhedra_Library::check_result(), Parma_Polyhedra_Library::Boundary_NS::set_minus_infinity(), Parma_Polyhedra_Library::Boundary_NS::set_plus_infinity(), and Parma_Polyhedra_Library::Boundary_NS::set_unbounded().

                          {
  Result rc = r & static_cast<Result>(VR_MASK);
  return static_cast<Result_Relation>(rc);
}

Result Parma_Polyhedra_Library::result_relation_class ( Result r )

inline

Definition at line 68 of file Result.inlines.hh.

References Parma_Polyhedra_Library::VC_MASK, and Parma_Polyhedra_Library::VR_MASK.

Referenced by Parma_Polyhedra_Library::Boundary_NS::adjust_boundary(), Parma_Polyhedra_Library::I_Constraint_Common< I_Constraint< T, Val_Or_Ref_Criteria, extended > >::convert_integer(), Parma_Polyhedra_Library::I_Constraint_Common< I_Constraint< T, Val_Or_Ref_Criteria, extended > >::convert_real(), Parma_Polyhedra_Library::I_Constraint_Rel::I_Constraint_Rel(), Parma_Polyhedra_Library::Interval< Boundary, Info >::Interval(), Parma_Polyhedra_Library::operator>>(), and Parma_Polyhedra_Library::Implementation::Boxes::propagate_constraint_check_result().

                                {
  return r & (static_cast<Result>(VR_MASK) | static_cast<Result>(VC_MASK));
}

Rounding_Dir Parma_Polyhedra_Library::round_dir ( Rounding_Dir dir )

inline

Definition at line 47 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::ROUND_DIR_MASK.

                            {
  return dir & ROUND_DIR_MASK;
}

bool Parma_Polyhedra_Library::round_direct ( Rounding_Dir dir )

inline

Definition at line 83 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), and Parma_Polyhedra_Library::ROUND_DIRECT.

Referenced by Parma_Polyhedra_Library::Checked::assign_int_float(), Parma_Polyhedra_Library::Checked::assign_mpz_float(), and Parma_Polyhedra_Library::Checked::fpu_direct_rounding().

                               {
  return round_dir(dir) == ROUND_DIRECT;
}

bool Parma_Polyhedra_Library::round_down ( Rounding_Dir dir )

inline

Definition at line 53 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), and Parma_Polyhedra_Library::ROUND_DOWN.

Referenced by Parma_Polyhedra_Library::Checked::assign_mpz_mpq(), Parma_Polyhedra_Library::Checked::assign_special_int(), Parma_Polyhedra_Library::Checked::div_2exp_mpz(), Parma_Polyhedra_Library::Checked::div_mpz(), Parma_Polyhedra_Library::Checked::round_lt_float(), Parma_Polyhedra_Library::Checked::round_lt_int(), Parma_Polyhedra_Library::Checked::round_lt_int_no_overflow(), Parma_Polyhedra_Library::Checked::round_lt_mpz(), and Parma_Polyhedra_Library::Checked::set_pos_overflow_int().

                             {
  return round_dir(dir) == ROUND_DOWN;
}

fpu_rounding_direction_type Parma_Polyhedra_Library::round_fpu_dir ( Rounding_Dir dir )

bool Parma_Polyhedra_Library::round_ignore ( Rounding_Dir dir )

inline

Definition at line 65 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), and Parma_Polyhedra_Library::ROUND_IGNORE.

Referenced by Parma_Polyhedra_Library::Checked::assign_mpz_mpq(), and Parma_Polyhedra_Library::Checked::div_mpz().

                               {
  return round_dir(dir) == ROUND_IGNORE;
}

bool Parma_Polyhedra_Library::round_inverse ( Rounding_Dir dir )

inline

Definition at line 89 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), and Parma_Polyhedra_Library::ROUND_INVERSE.

Referenced by Parma_Polyhedra_Library::Checked::fpu_inverse_rounding().

                                {
  return round_dir(dir) == ROUND_INVERSE;
}

bool Parma_Polyhedra_Library::round_not_needed ( Rounding_Dir dir )

inline

Definition at line 71 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), and Parma_Polyhedra_Library::ROUND_NOT_NEEDED.

Referenced by Parma_Polyhedra_Library::Checked::assign_mpz_mpq(), Parma_Polyhedra_Library::Checked::div_mpz(), Parma_Polyhedra_Library::Checked::prepare_inexact(), and Parma_Polyhedra_Library::Checked::result_relation().

                                   {
  return round_dir(dir) == ROUND_NOT_NEEDED;
}

bool Parma_Polyhedra_Library::round_not_requested ( Rounding_Dir dir )

inline

Definition at line 77 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), Parma_Polyhedra_Library::ROUND_IGNORE, and Parma_Polyhedra_Library::ROUND_NOT_NEEDED.

                                      {
  return round_dir(dir) == ROUND_IGNORE || round_dir(dir) == ROUND_NOT_NEEDED;
}

bool Parma_Polyhedra_Library::round_strict_relation ( Rounding_Dir dir )

inline

Definition at line 95 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::ROUND_STRICT_RELATION.

Referenced by Parma_Polyhedra_Library::Checked::assign_mpz_mpq(), Parma_Polyhedra_Library::Checked::div_2exp_mpz(), Parma_Polyhedra_Library::Checked::div_mpz(), Parma_Polyhedra_Library::Checked::prepare_inexact(), and Parma_Polyhedra_Library::Checked::result_relation().

                                        {
  return (dir & ROUND_STRICT_RELATION) == ROUND_STRICT_RELATION;
}

bool Parma_Polyhedra_Library::round_up ( Rounding_Dir dir )

inline

Definition at line 59 of file Rounding_Dir.inlines.hh.

References Parma_Polyhedra_Library::round_dir(), and Parma_Polyhedra_Library::ROUND_UP.

Referenced by Parma_Polyhedra_Library::Checked::assign_mpz_mpq(), Parma_Polyhedra_Library::Checked::assign_special_int(), Parma_Polyhedra_Library::Checked::div_2exp_mpz(), Parma_Polyhedra_Library::Checked::div_mpz(), Parma_Polyhedra_Library::Checked::round_gt_float(), Parma_Polyhedra_Library::Checked::round_gt_int(), Parma_Polyhedra_Library::Checked::round_gt_int_no_overflow(), Parma_Polyhedra_Library::Checked::round_gt_mpz(), and Parma_Polyhedra_Library::Checked::set_neg_overflow_int().

                           {
  return round_dir(dir) == ROUND_UP;
}

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.

Definition at line 221 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::termination_test_MS().

                                      {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::termination_test_MS(pset):\n"
         "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  return termination_test_MS(cs);
}

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.

Definition at line 239 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::termination_test_MS().

                                                                       {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::termination_test_MS_2(pset_before, pset_after):\n"
         "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  Termination_Helpers
    ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
  return termination_test_MS(cs);
}

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

Definition at line 437 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::termination_test_PR_original().

                                      {
  const dimension_type space_dim = pset.space_dimension();
  if (space_dim % 2 != 0) {
    std::ostringstream s;
    s << "PPL::termination_test_PR(pset):\n"
      << "pset.space_dimension() == " << space_dim
      << " is odd.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs;
  assign_all_inequalities_approximation(pset, cs);
  return termination_test_PR_original(cs);
}

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

Definition at line 415 of file termination.templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), and Parma_Polyhedra_Library::Implementation::Termination::termination_test_PR().

                                                                       {
  const dimension_type before_space_dim = pset_before.space_dimension();
  const dimension_type after_space_dim = pset_after.space_dimension();
  if (after_space_dim != 2*before_space_dim) {
    std::ostringstream s;
    s << "PPL::termination_test_PR_2(pset_before, pset_after):\n"
      << "pset_before.space_dimension() == " << before_space_dim
      << ", pset_after.space_dimension() == " << after_space_dim
      << ";\nthe latter should be twice the former.";
    throw std::invalid_argument(s.str());
  }
  using namespace Implementation::Termination;
  Constraint_System cs_before;
  Constraint_System cs_after;
  assign_all_inequalities_approximation(pset_before, cs_before);
  assign_all_inequalities_approximation(pset_after, cs_after);
  return termination_test_PR(cs_before, cs_after);
}

Variable Documentation

const Throwable *volatile Parma_Polyhedra_Library::abandon_expensive_computations = 0

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.

Definition at line 31 of file globals.cc.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::concatenate_assign(), Parma_Polyhedra_Library::maybe_abandon(), and Parma_Polyhedra_Library::Powerset< D >::omega_reduce().

Namespaces

Classes

Macros

Typedefs

Enumerations

Functions

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