PPL 1.0

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

- Namespace List
- Namespace Members

Namespaces | Classes | Typedefs | Enumerations | Functions | Variables
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

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.