PPL  1.0
Parma_Polyhedra_Library Namespace Reference

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

Namespaces

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

Classes

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  Variable
 A dimension of the vector space. More...
class  Throwable
 User objects the PPL can throw. More...
struct  Recycle_Input
 A tag class. More...
class  Linear_Form
 A linear form with interval coefficients. More...
class  Checked_Number
 A wrapper for numeric types implementing a given policy. More...
class  Interval
 A generic, not necessarily closed, possibly restricted interval. More...
class  Variables_Set
 An std::set of variables' indexes. More...
class  Linear_Expression
 A linear expression. More...
class  Constraint
 A linear equality or inequality. More...
class  Generator
 A line, ray, point or closure point. More...
class  Grid_Generator
 A grid line, parameter or grid point. More...
class  Congruence
 A linear congruence. More...
class  Box
 A not necessarily closed, iso-oriented hyperrectangle. More...
class  Constraint_System
 A system of constraints. More...
class  Constraint_System_const_iterator
 An iterator over a system of constraints. More...
class  Congruence_System
 A system of congruences. More...
class  Poly_Con_Relation
 The relation between a polyhedron and a constraint. More...
class  Generator_System
 A system of generators. More...
class  Generator_System_const_iterator
 An iterator over a system of generators. More...
class  Poly_Gen_Relation
 The relation between a polyhedron and a generator. More...
class  Polyhedron
 The base class for convex polyhedra. More...
class  MIP_Problem
 A Mixed Integer (linear) Programming problem. More...
class  Floating_Point_Expression
 A floating point expression on a given format. More...
class  Grid_Generator_System
 A system of grid generators. More...
class  Grid
 A grid. More...
class  BD_Shape
 A bounded difference shape. More...
class  C_Polyhedron
 A closed convex polyhedron. More...
class  Octagonal_Shape
 An octagonal shape. More...
class  Concrete_Expression_Type
 The type of a concrete expression. More...
class  Concrete_Expression_Common
 Base class for all concrete expressions. More...
class  Binary_Operator_Common
 Base class for binary operator applied to two concrete expressions. More...
class  Unary_Operator_Common
 Base class for unary operator applied to one concrete expression. More...
class  Cast_Operator_Common
 Base class for cast operator concrete expressions. More...
class  Integer_Constant_Common
 Base class for integer constant concrete expressions. More...
class  Floating_Point_Constant_Common
 Base class for floating-point constant concrete expression. More...
class  Approximable_Reference_Common
 Base class for references to some approximable. More...
class  PIP_Problem
 A Parametric Integer (linear) Programming problem. More...
class  PIP_Tree_Node
 A node of the PIP solution tree. More...
class  PIP_Solution_Node
 A tree node representing part of the space of solutions. More...
class  PIP_Decision_Node
 A tree node representing a decision in the space of solutions. More...
class  BHRZ03_Certificate
 The convergence certificate for the BHRZ03 widening operator. More...
class  H79_Certificate
 A convergence certificate for the H79 widening operator. More...
class  Grid_Certificate
 The convergence certificate for the Grid widening operator. More...
class  NNC_Polyhedron
 A not necessarily closed convex polyhedron. More...
class  Smash_Reduction
 This class provides the reduction method for the Smash_Product domain. More...
class  Constraints_Reduction
 This class provides the reduction method for the Constraints_Product domain. More...
class  Congruences_Reduction
 This class provides the reduction method for the Congruences_Product domain. More...
class  Shape_Preserving_Reduction
 This class provides the reduction method for the Shape_Preserving_Product domain. More...
class  No_Reduction
 This class provides the reduction method for the Direct_Product domain. More...
class  Partially_Reduced_Product
 The partially reduced product of two abstractions. More...
class  Domain_Product
 This class is temporary and will be removed when template typedefs will be supported in C++. More...
class  Determinate
 A wrapper for PPL pointsets, providing them with a determinate constraint system interface, as defined in [Bag98]. More...
class  Powerset
 The powerset construction on a base-level domain. More...
class  Pointset_Powerset
 The powerset construction instantiated on PPL pointset domains. More...
class  Cast_Floating_Point_Expression
 A generic Cast Floating Point Expression. More...
class  Constant_Floating_Point_Expression
 A generic Constant Floating Point Expression. More...
class  Variable_Floating_Point_Expression
 A generic Variable Floating Point Expression. More...
class  Sum_Floating_Point_Expression
 A generic Sum Floating Point Expression. More...
class  Difference_Floating_Point_Expression
 A generic Difference Floating Point Expression. More...
class  Multiplication_Floating_Point_Expression
 A generic Multiplication Floating Point Expression. More...
class  Division_Floating_Point_Expression
 A generic Division Floating Point Expression. More...
class  Opposite_Floating_Point_Expression
 A generic Opposite Floating Point Expression. More...
class  Watchdog
 A watchdog timer. More...
class  Threshold_Watcher
 A class of watchdogs controlling the exceeding of a threshold. More...
class  Concrete_Expression
 The base class of all concrete expressions. More...
class  Binary_Operator
 A binary operator applied to two concrete expressions. More...
class  Unary_Operator
 A unary operator applied to one concrete expression. More...
class  Cast_Operator
 A cast operator converting one concrete expression to some type. More...
class  Integer_Constant
 An integer constant concrete expression. More...
class  Floating_Point_Constant
 A floating-point constant concrete expression. More...
class  Approximable_Reference
 A concrete expression representing a reference to some approximable. More...
class  GMP_Integer
 Unbounded integers as provided by the GMP library. More...

Typedefs

typedef size_t dimension_type
 An unsigned integral type for representing space dimensions.
typedef size_t memory_size_type
 An unsigned integral type for representing memory size in bytes.
typedef int Concrete_Expression_Kind
 Encodes the kind of concrete expression.
typedef int Concrete_Expression_BOP
 Encodes a binary operator of concrete expressions.
typedef int Concrete_Expression_UOP
 Encodes a unary operator of concrete expressions.
typedef PPL_COEFFICIENT_TYPE Coefficient
 An alias for easily naming the type of PPL coefficients.

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
}
 Widths of bounded integer types. More...
enum  Bounded_Integer_Type_Representation { UNSIGNED, SIGNED_2_COMPLEMENT }
 Representation of bounded integer types. More...
enum  Bounded_Integer_Type_Overflow { OVERFLOW_WRAPS, OVERFLOW_UNDEFINED, OVERFLOW_IMPOSSIBLE }
 Overflow behavior of bounded integer types. More...
enum  Representation { DENSE, SPARSE }
 Possible representations of coefficient sequences (i.e. linear expressions and more complex objects containing linear expressions, e.g. Constraints, Generators, etc.). More...
enum  Floating_Point_Format {
  IEEE754_HALF, IEEE754_SINGLE, IEEE754_DOUBLE, IEEE754_QUAD,
  INTEL_DOUBLE_EXTENDED, IBM_SINGLE, IBM_DOUBLE
}
 Floating point formats known to the library. More...
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.
void set_rounding_for_PPL ()
 Sets the FPU rounding mode so that the PPL abstractions based on floating point numbers work correctly.
void restore_pre_PPL_rounding ()
 Sets the FPU rounding mode as it was before initialization of the PPL.
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.
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)
 Extracts the value class part of r (representable number, unrepresentable minus/plus infinity or nan).
Result_Relation result_relation (Result r)
 Extracts the relation part of 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.
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)
 Returns the inverse rounding mode of dir, ROUND_IGNORE being the inverse of itself.
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)
 Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
template<typename PSET >
bool 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 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 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 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 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 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 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 termination_test_PR (const PSET &pset)
 Like termination_test_MS() but using the method by Podelski and Rybalchenko [BMPZ10].
template<typename PSET >
bool 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 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 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 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 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].

Variables

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

Detailed Description

The entire library is confined to this namespace.


Typedef Documentation

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

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.

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

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.

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