The entire library is confined to this namespace. More...

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

Classes
class	Approximable_Reference
	A concrete expression representing a reference to some approximable. More...

class	Approximable_Reference_Common
	Base class for references to some approximable. More...

class	BD_Shape
	A bounded difference shape. More...

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

class	Binary_Operator
	A binary operator applied to two concrete expressions. More...

class	Binary_Operator_Common
	Base class for binary operator applied to two concrete expressions. More...

class	Box
	A not necessarily closed, iso-oriented hyperrectangle. More...

class	C_Polyhedron
	A closed convex polyhedron. More...

class	Cast_Floating_Point_Expression
	A generic Cast Floating Point Expression. More...

class	Cast_Operator
	A cast operator converting one concrete expression to some type. More...

class	Cast_Operator_Common
	Base class for cast operator concrete expressions. More...

class	Checked_Number
	A wrapper for numeric types implementing a given policy. More...

class	Concrete_Expression
	The base class of all concrete expressions. More...

class	Concrete_Expression_Common
	Base class for all concrete expressions. More...

class	Concrete_Expression_Type
	The type of a concrete expression. More...

class	Congruence
	A linear congruence. More...

class	Congruence_System
	A system of congruences. More...

class	Congruences_Reduction
	This class provides the reduction method for the Congruences_Product domain. More...

class	Constant_Floating_Point_Expression
	A generic Constant Floating Point Expression. More...

class	Constraint
	A linear equality or inequality. More...

class	Constraint_System
	A system of constraints. More...

class	Constraint_System_const_iterator
	An iterator over a system of constraints. More...

class	Constraints_Reduction
	This class provides the reduction method for the Constraints_Product domain. More...

class	Determinate
	A wrapper for PPL pointsets, providing them with a determinate constraint system interface, as defined in [Bag98]. More...

class	Difference_Floating_Point_Expression
	A generic Difference Floating Point Expression. More...

class	Division_Floating_Point_Expression
	A generic Division Floating Point Expression. More...

class	Domain_Product
	This class is temporary and will be removed when template typedefs will be supported in C++. More...

class	Floating_Point_Constant
	A floating-point constant concrete expression. More...

class	Floating_Point_Constant_Common
	Base class for floating-point constant concrete expression. More...

class	Floating_Point_Expression

class	FP_Oracle
	An abstract class to be implemented by an external analyzer such as ECLAIR in order to provide to the PPL the necessary information for performing the analysis of floating point computations. More...

class	Generator
	A line, ray, point or closure point. More...

class	Generator_System
	A system of generators. More...

class	Generator_System_const_iterator
	An iterator over a system of generators. More...

class	GMP_Integer
	Unbounded integers as provided by the GMP library. More...

class	Grid
	A grid. More...

class	Grid_Certificate
	The convergence certificate for the Grid widening operator. More...

class	Grid_Generator
	A grid line, parameter or grid point. More...

class	Grid_Generator_System
	A system of grid generators. More...

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

class	Integer_Constant
	An integer constant concrete expression. More...

class	Integer_Constant_Common
	Base class for integer constant concrete expressions. More...

class	Interval
	A generic, not necessarily closed, possibly restricted interval. More...

class	Linear_Expression
	A linear expression. More...

class	Linear_Form
	A linear form with interval coefficients. More...

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

class	Multiplication_Floating_Point_Expression
	A generic Multiplication Floating Point Expression. More...

class	NNC_Polyhedron
	A not necessarily closed convex polyhedron. More...

class	No_Reduction
	This class provides the reduction method for the Direct_Product domain. More...

class	Octagonal_Shape
	An octagonal shape. More...

class	Opposite_Floating_Point_Expression
	A generic Opposite Floating Point Expression. More...

class	Partially_Reduced_Product
	The partially reduced product of two abstractions. More...

class	PIP_Decision_Node
	A tree node representing a decision in the space of solutions. More...

class	PIP_Problem
	A Parametric Integer (linear) Programming problem. More...

class	PIP_Solution_Node
	A tree node representing part of the space of solutions. More...

class	PIP_Tree_Node
	A node of the PIP solution tree. More...

class	Pointset_Powerset
	The powerset construction instantiated on PPL pointset domains. More...

class	Poly_Con_Relation
	The relation between a polyhedron and a constraint. More...

class	Poly_Gen_Relation
	The relation between a polyhedron and a generator. More...

class	Polyhedron
	The base class for convex polyhedra. More...

class	Powerset
	The powerset construction on a base-level domain. More...

struct	Recycle_Input
	A tag class. More...

struct	Select_Temp_Boundary_Type
	Helper class to select the appropriate numerical type to perform boundary computations so as to reduce the chances of overflow without incurring too much overhead. More...

class	Shape_Preserving_Reduction
	This class provides the reduction method for the Shape_Preserving_Product domain. More...

class	Smash_Reduction
	This class provides the reduction method for the Smash_Product domain. More...

class	Sum_Floating_Point_Expression
	A generic Sum Floating Point Expression. More...

class	Threshold_Watcher
	A class of watchdogs controlling the exceeding of a threshold. More...

class	Throwable
	User objects the PPL can throw. More...

class	Unary_Operator
	A unary operator applied to one concrete expression. More...

class	Unary_Operator_Common
	Base class for unary operator applied to one concrete expression. More...

class	Variable
	A dimension of the vector space. More...

class	Variable_Floating_Point_Expression
	A generic Variable Floating Point Expression. More...

class	Variables_Set
	An std::set of variables' indexes. More...

class	Watchdog
	A watchdog timer. More...

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

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

typedef int	Concrete_Expression_Kind
	Encodes the kind of concrete expression. More...

typedef int	Concrete_Expression_BOP
	Encodes a binary operator of concrete expressions. More...

typedef int	Concrete_Expression_UOP
	Encodes a unary operator of concrete expressions. More...

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

Enumerations
enum	Result_Class { VC_NORMAL, VC_MINUS_INFINITY, VC_PLUS_INFINITY, VC_NAN }

enum	Result_Relation { VR_EMPTY, VR_EQ, VR_LT, VR_GT, VR_NE, VR_LE, VR_GE, VR_LGE }

enum	Result { V_EMPTY, V_EQ, V_LT, V_GT, V_NE, V_LE, V_GE, V_LGE, V_OVERFLOW, V_LT_INF, V_GT_SUP, V_LT_PLUS_INFINITY, V_GT_MINUS_INFINITY, V_EQ_MINUS_INFINITY, V_EQ_PLUS_INFINITY, V_NAN, V_CVT_STR_UNK, V_DIV_ZERO, V_INF_ADD_INF, V_INF_DIV_INF, V_INF_MOD, V_INF_MUL_ZERO, V_INF_SUB_INF, V_MOD_ZERO, V_SQRT_NEG, V_UNKNOWN_NEG_OVERFLOW, V_UNKNOWN_POS_OVERFLOW, V_UNREPRESENTABLE }
	Possible outcomes of a checked arithmetic computation. More...

enum	Rounding_Dir { ROUND_DOWN, ROUND_UP, ROUND_IGNORE , ROUND_NOT_NEEDED , ROUND_STRICT_RELATION }
	Rounding directions for arithmetic computations. More...

enum	Degenerate_Element { UNIVERSE, EMPTY }
	Kinds of degenerate abstract elements. More...

enum	Relation_Symbol { EQUAL, LESS_THAN, LESS_OR_EQUAL, GREATER_THAN, GREATER_OR_EQUAL, NOT_EQUAL }
	Relation symbols. More...

enum	Complexity_Class { POLYNOMIAL_COMPLEXITY, SIMPLEX_COMPLEXITY, ANY_COMPLEXITY }
	Complexity pseudo-classes. More...

enum	Optimization_Mode { MINIMIZATION, MAXIMIZATION }
	Possible optimization modes. More...

enum	Bounded_Integer_Type_Width { BITS_8, BITS_16, BITS_32, BITS_64, BITS_128 }

enum	Bounded_Integer_Type_Representation { UNSIGNED, SIGNED_2_COMPLEMENT }

enum	Bounded_Integer_Type_Overflow { OVERFLOW_WRAPS, OVERFLOW_UNDEFINED, OVERFLOW_IMPOSSIBLE }

enum	Representation { DENSE, SPARSE }

enum	Floating_Point_Format { IEEE754_HALF, IEEE754_SINGLE, IEEE754_DOUBLE, IEEE754_QUAD, INTEL_DOUBLE_EXTENDED, IBM_SINGLE, IBM_DOUBLE }

enum	PIP_Problem_Status { UNFEASIBLE_PIP_PROBLEM, OPTIMIZED_PIP_PROBLEM }
	Possible outcomes of the PIP_Problem solver. More...

enum	MIP_Problem_Status { UNFEASIBLE_MIP_PROBLEM, UNBOUNDED_MIP_PROBLEM, OPTIMIZED_MIP_PROBLEM }
	Possible outcomes of the MIP_Problem solver. More...

Functions
dimension_type	not_a_dimension ()
	Returns a value that does not designate a valid dimension.

unsigned	irrational_precision ()
	Returns the precision parameter used for irrational calculations.

void	set_irrational_precision (const unsigned p)
	Sets the precision parameter used for irrational calculations. More...

void	set_rounding_for_PPL ()
	Sets the FPU rounding mode so that the PPL abstractions based on floating point numbers work correctly. More...

void	restore_pre_PPL_rounding ()
	Sets the FPU rounding mode as it was before initialization of the PPL. More...

void	initialize ()
	Initializes the library.

void	finalize ()
	Finalizes the library.

Coefficient_traits::const_reference	Coefficient_zero ()
	Returns a const reference to a Coefficient with value 0.

Coefficient_traits::const_reference	Coefficient_one ()
	Returns a const reference to a Coefficient with value 1.

dimension_type	max_space_dimension ()
	Returns the maximum space dimension this library can handle.

Library Version Control Functions
unsigned	version_major ()
	Returns the major number of the PPL version.

unsigned	version_minor ()
	Returns the minor number of the PPL version.

unsigned	version_revision ()
	Returns the revision number of the PPL version.

unsigned	version_beta ()
	Returns the beta number of the PPL version.

const char *	version ()
	Returns a character string containing the PPL version.

const char *	banner ()
	Returns a character string containing the PPL banner. More...

Functions Inspecting and/or Combining Result Values
Result	operator& (Result x, Result y)

Result	operator\| (Result x, Result y)

Result	operator- (Result x, Result y)

Result_Class	result_class (Result r)

Result_Relation	result_relation (Result r)

Result	result_relation_class (Result r)

Functions Controlling Floating Point Unit
void	fpu_initialize_control_functions ()
	Initializes the FPU control functions.

fpu_rounding_direction_type	fpu_get_rounding_direction ()
	Returns the current FPU rounding direction.

void	fpu_set_rounding_direction (fpu_rounding_direction_type dir)
	Sets the FPU rounding direction to `dir`.

fpu_rounding_control_word_type	fpu_save_rounding_direction (fpu_rounding_direction_type dir)
	Sets the FPU rounding direction to `dir` and returns the rounding control word previously in use.

fpu_rounding_control_word_type	fpu_save_rounding_direction_reset_inexact (fpu_rounding_direction_type dir)
	Sets the FPU rounding direction to `dir`, clears the inexact computation status, and returns the rounding control word previously in use.

void	fpu_restore_rounding_direction (fpu_rounding_control_word_type w)
	Restores the FPU rounding rounding control word to `cw`.

void	fpu_reset_inexact ()
	Clears the inexact computation status.

int	fpu_check_inexact ()
	Queries the inexact computation status. More...

Functions Inspecting and/or Combining Rounding_Dir Values
Rounding_Dir	operator& (Rounding_Dir x, Rounding_Dir y)

Rounding_Dir	operator\| (Rounding_Dir x, Rounding_Dir y)

Rounding_Dir	inverse (Rounding_Dir dir)

Rounding_Dir	round_dir (Rounding_Dir dir)

bool	round_down (Rounding_Dir dir)

bool	round_up (Rounding_Dir dir)

bool	round_ignore (Rounding_Dir dir)

bool	round_not_needed (Rounding_Dir dir)

bool	round_not_requested (Rounding_Dir dir)

bool	round_direct (Rounding_Dir dir)

bool	round_inverse (Rounding_Dir dir)

bool	round_strict_relation (Rounding_Dir dir)

fpu_rounding_direction_type	round_fpu_dir (Rounding_Dir dir)

Functions for the Synthesis of Linear Rankings
template<typename PSET >
bool	termination_test_MS (const PSET &pset)

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

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

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

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

template<typename PSET >
void	all_affine_ranking_functions_MS_2 (const PSET &pset_before, const PSET &pset_after, C_Polyhedron &mu_space)

template<typename PSET >
void	all_affine_quasi_ranking_functions_MS (const PSET &pset, C_Polyhedron &decreasing_mu_space, C_Polyhedron &bounded_mu_space)

template<typename PSET >
void	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	termination_test_PR (const PSET &pset)

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

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

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

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

template<typename PSET >
void	all_affine_ranking_functions_PR_2 (const PSET &pset_before, const PSET &pset_after, NNC_Polyhedron &mu_space)

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

Detailed Description

The entire library is confined to this namespace.

Typedef Documentation

typedef int Parma_Polyhedra_Library::Concrete_Expression_Kind

Encodes the kind of concrete expression.

The values should be defined by the particular instance and uniquely identify one of: Binary_Operator, Unary_Operator, Cast_Operator, Integer_Constant, Floating_Point_Constant, or Approximable_Reference. For example, the Binary_Operator kind integer constant should be defined by an instance as the member Binary_Operator<T>::KIND.

typedef int Parma_Polyhedra_Library::Concrete_Expression_BOP

Encodes a binary operator of concrete expressions.

The values should be uniquely defined by the particular instance and named: ADD, SUB, MUL, DIV, REM, BAND, BOR, BXOR, LSHIFT, RSHIFT.

typedef int Parma_Polyhedra_Library::Concrete_Expression_UOP

Encodes a unary operator of concrete expressions.

The values should be uniquely defined by the particular instance and named: PLUS, MINUS, BNOT.

Enumeration Type Documentation

enum Parma_Polyhedra_Library::Result_Class

Enumerator
VC_NORMAL	Representable number result class.
VC_MINUS_INFINITY	Negative infinity result class.
VC_PLUS_INFINITY	Positive infinity result class.
VC_NAN	Not a number result class.

enum Parma_Polyhedra_Library::Result_Relation

Enumerator
VR_EMPTY	No values satisfies the relation.
VR_EQ	Equal. This need to be accompanied by a value.
VR_LT	Less than. This need to be accompanied by a value.
VR_GT	Greater than. This need to be accompanied by a value.
VR_NE	Not equal. This need to be accompanied by a value.
VR_LE	Less or equal. This need to be accompanied by a value.
VR_GE	Greater or equal. This need to be accompanied by a value.
VR_LGE	All values satisfy the relation.

Function Documentation

const char* Parma_Polyhedra_Library::banner ( )

Returns a character string containing the PPL banner.

The banner provides information about the PPL version, the licensing, the lack of any warranty whatsoever, the C++ compiler used to build the library, where to report bugs and where to look for further information.

int Parma_Polyhedra_Library::fpu_check_inexact ( )

inline

Queries the inexact computation status.

Returns 0 if the computation was definitely exact, 1 if it was definitely inexact, -1 if definite exactness information is unavailable.

void Parma_Polyhedra_Library::set_irrational_precision ( const unsigned p )

inline

Sets the precision parameter used for irrational calculations.

The lesser between numerator and denominator is limited to 2**p.

If p is less than or equal to INT_MAX, sets the precision parameter used for irrational calculations to p.

Exceptions

std::invalid_argument Thrown if p is greater than INT_MAX.

void Parma_Polyhedra_Library::set_rounding_for_PPL ( )

inline

Sets the FPU rounding mode so that the PPL abstractions based on floating point numbers work correctly.

This is performed automatically at initialization-time. Calling this function is needed only if restore_pre_PPL_rounding() has been previously called.

void Parma_Polyhedra_Library::restore_pre_PPL_rounding ( )

inline

Sets the FPU rounding mode as it was before initialization of the PPL.

This is important if the application uses floating-point computations outside the PPL. It is crucial when the application uses functions from a mathematical library that are not guaranteed to work correctly under all rounding modes.

After calling this function it is absolutely necessary to call set_rounding_for_PPL() before using any PPL abstractions based on floating point numbers. This is performed automatically at finalization-time.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Detailed Description

Typedef Documentation

Enumeration Type Documentation

Function Documentation