[PPL-devel] [GIT] ppl/ppl(termination): Function renamed. Unwanted stuff removed from comment.

Roberto Bagnara bagnara at cs.unipr.it
Tue Mar 9 11:31:31 CET 2010


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

Author: Roberto Bagnara <bagnara at 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);
 }




More information about the PPL-devel mailing list