Module: ppl/ppl Branch: termination Commit: df002a70c37365fc661bb7674ba60baf71898ccb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=df002a70c3736...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Tue Mar 9 14:31:09 2010 +0400

Function renamed. Unwanted stuff removed from comment.

---

src/termination.cc | 24 +++++++----------------- src/termination.templates.hh | 14 +++++++------- 2 files changed, 14 insertions(+), 24 deletions(-)

diff --git a/src/termination.cc b/src/termination.cc index 31b257a..cd1d168 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -176,13 +176,9 @@ fill_constraint_systems_MS(const Constraint_System& cs, \param cs_out The output constraint system, where variables indices are allocated as follows: - - \f$ \mu_1, \ldots, \mu_n \f$ go onto space dimensions - \f$ 0, \ldots, n-1 \f$; - - \f$ \mu_0\f$ goes onto space dimension \f$ n \f$; - - \f$ y_1, \ldots, y_m \f$ go onto space dimensions - \f$ n+1, \ldots, n+m \f$; - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions - \f$ n+m+1, ..., n+2*m+2 \f$. + - \f$ u_3 \f$ goes onto space dimensions \f$ 0, \ldots, s-1 \f$; + - \f$ u_2 \f$ goes onto space dimensions \f$ s, \ldots, s+r-1 \f$; + - \f$ u_1 \f$ goes onto space dimensions \f$ s+r, \ldots, s+2r-1 \f$.

The improved Podelski-Rybalchenko method described in the paper is based on a loop encoding of the form @@ -259,18 +255,12 @@ fill_constraint_systems_MS(const Constraint_System& cs, \f$ \vect{u}_3 \in \Qset_-^s \f$. The space of ranking functions is then spanned by \f$ \vect{u}_3^\transpose E_C' \vect x \f$. - - The allocation of variable indices in the output constraint - system \p cs_out is as follows: - - \f$ u_3 \f$ goes onto space dimensions \f$ 0, \ldots, s-1 \f$; - - \f$ u_2 \f$ goes onto space dimensions \f$ s, \ldots, s+r-1 \f$; - - \f$ u_1 \f$ goes onto space dimensions \f$ s+r, \ldots, s+2r-1 \f$. */ void -fill_constraint_systems_PR(const Constraint_System& cs, - const dimension_type n, - const dimension_type m, - Constraint_System& cs_out) { +fill_constraint_system_PR(const Constraint_System& cs, + const dimension_type n, + const dimension_type m, + Constraint_System& cs_out) { // Determine the partitioning of the m rows into the r rows // of E_B and the s rows of E'_C|E_C. std::deque<bool> in_A_B(m, true); diff --git a/src/termination.templates.hh b/src/termination.templates.hh index 84b56c3..0b28c19 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -119,10 +119,10 @@ fill_constraint_systems_MS(const Constraint_System& cs, Constraint_System& cs_out2);

void -fill_constraint_systems_PR(const Constraint_System& cs, - const dimension_type n, - const dimension_type m, - Constraint_System& cs_out); +fill_constraint_system_PR(const Constraint_System& cs, + const dimension_type n, + const dimension_type m, + Constraint_System& cs_out);

template <typename PSET> void @@ -344,7 +344,7 @@ termination_test_PR(const PSET& pset) { prepare_input_MS_PR(pset, cs, n, m, "termination_test_PR");

Constraint_System cs_mip; - fill_constraint_systems_PR(cs, n, m, cs_mip); + fill_constraint_system_PR(cs, n, m, cs_mip);

MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip);

@@ -361,7 +361,7 @@ one_affine_ranking_function_PR(const PSET& pset, Generator& mu) { prepare_input_MS_PR(pset, cs, n, m, "one_affine_ranking_function_PR");

Constraint_System cs_mip; - fill_constraint_systems_PR(cs, n, m, cs_mip); + fill_constraint_system_PR(cs, n, m, cs_mip);

MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip);

@@ -386,7 +386,7 @@ all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) { prepare_input_MS_PR(pset, cs, n, m, "all_affine_ranking_functions_PR");

Constraint_System cs_out; - fill_constraint_systems_PR(cs, n, m, cs_out); + fill_constraint_system_PR(cs, n, m, cs_out);

mu_space = C_Polyhedron(n+1, EMPTY); }