The entire library is confined to this namespace. More...
Namespaces | |
namespace | IO_Operators |
All input/output operators are confined to this namespace. | |
Classes | |
class | Throwable |
User objects the PPL can throw. More... | |
struct | Recycle_Input |
A tag class. More... | |
struct | Is_Checked |
struct | Is_Checked< Checked_Number< T, P > > |
struct | Is_Native_Or_Checked |
class | Checked_Number |
A wrapper for numeric types implementing a given policy. More... | |
class | Variable |
A dimension of the vector space. More... | |
class | Linear_Expression |
A linear expression. More... | |
class | Constraint_System |
A system of constraints. More... | |
class | Constraint |
A linear equality or inequality. More... | |
class | Poly_Con_Relation |
The relation between a polyhedron and a constraint. More... | |
class | Generator_System |
A system of generators. More... | |
class | Generator |
A line, ray, point or closure point. More... | |
class | Congruence_System |
A system of congruences. More... | |
class | Congruence |
A linear congruence. More... | |
class | Grid_Generator_System |
A system of grid generators. More... | |
class | Grid_Generator |
A grid line, parameter or grid point. More... | |
class | Variables_Set |
An std::set of variables' indexes. 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 | 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 | Interval |
A generic, not necessarily closed, possibly restricted interval. More... | |
class | Grid_Certificate |
The convergence certificate for the Grid widening operator. More... | |
class | C_Polyhedron |
A closed convex polyhedron. More... | |
class | NNC_Polyhedron |
A not necessarily closed convex polyhedron. More... | |
class | Grid |
A grid. More... | |
class | Box |
A not necessarily closed, iso-oriented hyperrectangle. More... | |
class | BD_Shape |
A bounded difference shape. More... | |
class | Octagonal_Shape |
An octagonal shape. 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 | 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 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 | 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 | Rounding_Dir { ROUND_DOWN, ROUND_UP, ROUND_IGNORE , ROUND_NOT_NEEDED , ROUND_STRICT_RELATION } |
Rounding directions for arithmetic computations. 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... | |
enum | I_Result { I_EMPTY = 1, I_SINGLETON = 2, I_SOME = 4, I_UNIVERSE = 8, I_NOT_EMPTY = I_SINGLETON | I_SOME | I_UNIVERSE, I_ANY = I_EMPTY | I_NOT_EMPTY, I_NOT_UNIVERSE = I_EMPTY | I_SINGLETON | I_SOME, I_NOT_DEGENERATE = I_SINGLETON | I_SOME, I_EXACT = 16, I_INEXACT = 32, I_CHANGED = 64, I_UNCHANGED = 128, I_SINGULARITIES = 256 } |
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. | |
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 | 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. | |
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 . | |
dimension_type | not_a_dimension () |
Returns a value that does not designate a valid dimension. | |
Rounding_Dir | inverse (Rounding_Dir dir) |
Returns the inverse rounding mode of dir , ROUND_IGNORE being the inverse of itself. | |
void | initialize () |
Initializes the library. | |
void | finalize () |
Finalizes the library. | |
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. | |
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. | |
unsigned long | isqrt (unsigned long x) |
Returns the integer square root of x . | |
dimension_type | max_space_dimension () |
Returns the maximum space dimension this library can handle. | |
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]. | |
Memory Size Inspection Functions | |
template<typename T > | |
Enable_If< Is_Native< T > ::value, memory_size_type > ::type | total_memory_in_bytes (const T &) |
template<typename T > | |
Enable_If< Is_Native< T > ::value, memory_size_type > ::type | external_memory_in_bytes (const T &) |
memory_size_type | total_memory_in_bytes (const mpz_class &x) |
memory_size_type | external_memory_in_bytes (const mpz_class &x) |
memory_size_type | total_memory_in_bytes (const mpq_class &x) |
memory_size_type | external_memory_in_bytes (const mpq_class &x) |
Relational Operators and Comparison Functions | |
template<typename T1 , typename T2 > | |
Enable_If < Is_Native_Or_Checked< T1 > ::value &&Is_Native_Or_Checked < T2 >::value, bool >::type | equal (const T1 &x, const T2 &y) |
template<typename T1 , typename T2 > | |
Enable_If < Is_Native_Or_Checked< T1 > ::value &&Is_Native_Or_Checked < T2 >::value, bool >::type | not_equal (const T1 &x, const T2 &y) |
template<typename T1 , typename T2 > | |
Enable_If < Is_Native_Or_Checked< T1 > ::value &&Is_Native_Or_Checked < T2 >::value, bool >::type | greater_or_equal (const T1 &x, const T2 &y) |
template<typename T1 , typename T2 > | |
Enable_If < Is_Native_Or_Checked< T1 > ::value &&Is_Native_Or_Checked < T2 >::value, bool >::type | greater_than (const T1 &x, const T2 &y) |
template<typename T1 , typename T2 > | |
Enable_If < Is_Native_Or_Checked< T1 > ::value &&Is_Native_Or_Checked < T2 >::value, bool >::type | less_or_equal (const T1 &x, const T2 &y) |
template<typename T1 , typename T2 > | |
Enable_If < Is_Native_Or_Checked< T1 > ::value &&Is_Native_Or_Checked < T2 >::value, bool >::type | less_than (const T1 &x, const T2 &y) |
Input-Output Operators | |
template<typename T > | |
Enable_If < Is_Native_Or_Checked< T > ::value, void >::type | ascii_dump (std::ostream &s, const T &t) |
Ascii dump for native or checked. | |
template<typename T > | |
Enable_If < Is_Native_Or_Checked< T > ::value, bool >::type | ascii_load (std::ostream &s, T &t) |
Ascii load for native or checked. | |
Variables | |
const Throwable *volatile | abandon_expensive_computations |
A pointer to an exception object. |
The entire library is confined to this namespace.
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.
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.
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.
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
.
std::invalid_argument | Thrown if p is greater than INT_MAX . |
bool Parma_Polyhedra_Library::termination_test_MS | ( | const PSET & | pset | ) | [inline] |
Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows:
where 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. |
true
if any loop approximated by pset
definitely terminates; false
if the test is inconclusive. However, if pset
precisely characterizes the effect of the loop body onto the loop-relevant program variables, then true
is returned if and only if the loop terminates. bool Parma_Polyhedra_Library::termination_test_MS_2 | ( | const PSET & | pset_before, | |
const PSET & | pset_after | |||
) | [inline] |
Termination test using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
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:
| |
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:
|
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
.
true
if any loop approximated by pset
definitely terminates; false
if 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 true
is returned if and only if the loop terminates. bool Parma_Polyhedra_Library::one_affine_ranking_function_MS | ( | const PSET & | pset, | |
Generator & | mu | |||
) | [inline] |
Termination test with witness ranking function using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows:
where 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. | |
mu | When true is returned, this is assigned a point of space dimension ![]() ![]() ![]() mu corresponding to the space dimensions ![]() |
true
if any loop approximated by pset
definitely terminates; false
if the test is inconclusive. However, if pset
precisely characterizes the effect of the loop body onto the loop-relevant program variables, then true
is returned if and only if the loop terminates. bool Parma_Polyhedra_Library::one_affine_ranking_function_MS_2 | ( | const PSET & | pset_before, | |
const PSET & | pset_after, | |||
Generator & | mu | |||
) | [inline] |
Termination test with witness ranking function using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
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:
| |
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:
|
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
.
mu | When true is returned, this is assigned a point of space dimension ![]() ![]() ![]() mu corresponding to the space dimensions ![]() |
true
if any loop approximated by pset
definitely terminates; false
if 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 true
is returned if and only if the loop terminates. void Parma_Polyhedra_Library::all_affine_ranking_functions_MS | ( | const PSET & | pset, | |
C_Polyhedron & | mu_space | |||
) | [inline] |
Termination test with ranking function space using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows:
where 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. | |
mu_space | This is assigned a closed polyhedron of space dimension ![]() pset . These ranking functions are of the form ![]() ![]() mu_space polyhedron. The variables ![]() mu_space ![]() mu_space is empty, it means that the test is inconclusive. However, if pset precisely characterizes the effect of the loop body onto the loop-relevant program variables, then mu_space is empty if and only if the loop does not terminate. |
void Parma_Polyhedra_Library::all_affine_ranking_functions_MS_2 | ( | const PSET & | pset_before, | |
const PSET & | pset_after, | |||
C_Polyhedron & | mu_space | |||
) | [inline] |
Termination test with ranking function space using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
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:
| |
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:
|
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
.
mu_space | This is assigned a closed polyhedron of space dimension ![]() pset . These ranking functions are of the form ![]() ![]() mu_space polyhedron. The variables ![]() mu_space ![]() 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 mu_space is empty if and only if the loop does not terminate. |
void Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS | ( | const PSET & | pset, | |
C_Polyhedron & | decreasing_mu_space, | |||
C_Polyhedron & | bounded_mu_space | |||
) | [inline] |
Computes the spaces of affine quasi ranking functions using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
pset | A pointset approximating the behavior of a loop whose termination is being analyzed. The variables indices are allocated as follows:
where 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. | |
decreasing_mu_space | This is assigned a closed polyhedron of space dimension ![]() pset . | |
bounded_mu_space | This is assigned a closed polyhedron of space dimension ![]() pset . |
These quasi-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
precisely characterizes 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.
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 | |||
) | [inline] |
Computes the spaces of affine quasi ranking functions using an improvement of the method by Mesnard and Serebrenik [BMPZ10].
PSET | Any pointset supported by the PPL that provides the minimized_constraints() method. |
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:
| |
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:
|
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
.
decreasing_mu_space | This is assigned a closed polyhedron of space dimension ![]() pset . | |
bounded_mu_space | This is assigned a closed polyhedron of space dimension ![]() 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.