Classes |
class | Parma_Polyhedra_Library::Variable |
| A dimension of the vector space. More...
|
struct | Parma_Polyhedra_Library::Variable::Compare |
| Binary predicate defining the total ordering on variables. More...
|
class | Parma_Polyhedra_Library::Throwable |
| User objects the PPL can throw. More...
|
struct | Parma_Polyhedra_Library::Recycle_Input |
| A tag class. More...
|
class | Parma_Polyhedra_Library::Linear_Form< C > |
| A linear form with interval coefficients. More...
|
class | Parma_Polyhedra_Library::Checked_Number< T, Policy > |
| A wrapper for numeric types implementing a given policy. More...
|
class | Parma_Polyhedra_Library::Interval< Boundary, Info > |
| A generic, not necessarily closed, possibly restricted interval. More...
|
class | Parma_Polyhedra_Library::Linear_Expression |
| A linear expression. More...
|
class | Parma_Polyhedra_Library::Constraint |
| A linear equality or inequality. More...
|
class | Parma_Polyhedra_Library::Generator |
| A line, ray, point or closure point. More...
|
class | Parma_Polyhedra_Library::Grid_Generator |
| A grid line, parameter or grid point. More...
|
class | Parma_Polyhedra_Library::Congruence |
| A linear congruence. More...
|
class | Parma_Polyhedra_Library::Box< ITV > |
| A not necessarily closed, iso-oriented hyperrectangle. 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::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::Poly_Con_Relation |
| The relation between a polyhedron and a constraint. 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...
|
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::MIP_Problem |
| A Mixed Integer (linear) Programming problem. More...
|
class | Parma_Polyhedra_Library::Grid_Generator_System |
| A system of grid generators. More...
|
class | Parma_Polyhedra_Library::Grid |
| A grid. More...
|
class | Parma_Polyhedra_Library::BD_Shape< T > |
| A bounded difference shape. More...
|
class | Parma_Polyhedra_Library::C_Polyhedron |
| A closed convex polyhedron. More...
|
class | Parma_Polyhedra_Library::Octagonal_Shape< T > |
| An octagonal shape. More...
|
class | Parma_Polyhedra_Library::PIP_Problem |
| A Parametric Integer (linear) Programming problem. More...
|
class | Parma_Polyhedra_Library::BHRZ03_Certificate |
| The convergence certificate for the BHRZ03 widening operator. More...
|
class | Parma_Polyhedra_Library::H79_Certificate |
| A convergence certificate for the H79 widening operator. More...
|
class | Parma_Polyhedra_Library::Grid_Certificate |
| The convergence certificate for the Grid widening operator. More...
|
class | Parma_Polyhedra_Library::NNC_Polyhedron |
| A not necessarily closed convex polyhedron. 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::Determinate< PSET > |
| A wrapper for PPL pointsets, providing them with a determinate constraint system interface, as defined in [Bag98]. More...
|
class | Parma_Polyhedra_Library::Powerset< D > |
| The powerset construction on a base-level domain. More...
|
class | Parma_Polyhedra_Library::Pointset_Powerset< PSET > |
| The powerset construction instantiated on PPL pointset domains. More...
|
class | Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format > |
| A generic Cast Floating Point Expression. 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::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format > |
| A generic Variable Floating Point Expression. 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::Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > |
| A generic Difference Floating Point Expression. 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::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > |
| A generic Division Floating Point Expression. 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::GMP_Integer |
| Unbounded integers as provided by the GMP library. More...
|
Enumerations |
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_NOT_NEEDED
,
Parma_Polyhedra_Library::ROUND_STRICT_RELATION
} |
| Rounding directions for arithmetic computations. More...
|
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::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::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...
|
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].
|
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.
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:
go onto space dimensions .
|
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:
go onto space dimensions ,
go onto space dimensions ,
|
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
where
identify any point of the decreasing_mu_space
and bounded_mu_space
polyhedrons. The variables
correspond to the space dimensions
, 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.