PPL
1.0
|
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. |
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. |
The entire library is confined to this namespace.
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.
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.
|
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.
|
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
.
std::invalid_argument | Thrown if p is greater than INT_MAX . |
|
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.
|
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.