[PPL-devel] [GIT] ppl/ppl(termination): Fixed one_affine_ranking_function_PR().

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Thu Mar 18 11:13:02 2010 +0400

Fixed  one_affine_ranking_function_PR().

---

 src/termination.cc               |   18 ++++++++++--------
 tests/Polyhedron/termination1.cc |    2 +-
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/termination.cc b/src/termination.cc
index 2a8f96e..2fc0c58 100644
--- a/src/termination.cc
+++ b/src/termination.cc
@@ -564,29 +564,31 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before,
     // function computed in the feasible point is positive.
   finish:
     {
-      // We can impose that the linear expression is >= 1 because
-      // every positive multiple of the linear expression is
-      // acceptable.
+      // We can impose that the le_ineq is >= 1 because every positive
+      // multiple of the linear expression is acceptable.
       mip.add_constraint(le_ineq >= 1);
       Generator fp = mip.feasible_point();
       PPL_ASSERT(fp.is_point());
-      // u3 corresponds to space dimensions 0, ..., s - 1.
-      //const dimension_type s = distance(cs_after.begin(), cs_after.end());
+
+      // u_3 corresponds to space dimensions 0, ..., s - 1.
       const dimension_type n = cs_before.space_dimension();
       Linear_Expression le;
-      // mu0 is zero: do this first to avoid reallocations.
+      // mu_0 is zero: do this first to avoid reallocations.
       le += 0*Variable(n);
-      // Multiply u3 by E'_C.
+      // Multiply u_3 by E'_C to obtain mu_1, ..., mu_n.
       dimension_type row_index = 0;
+      PPL_DIRTY_TEMP_COEFFICIENT(k);
       for (Constraint_System::const_iterator i = cs_after.begin(),
 	     cs_after_end = cs_after.end();
 	   i != cs_after_end;
 	   ++i, ++row_index) {
 	Variable vi(row_index);
+	Coefficient_traits::const_reference fp_i = fp.coefficient(vi);
 	const Constraint& c_i = *i;
 	for (dimension_type j = n; j-- > 0; ) {
 	  Variable vj(j);
-	  le += vj*(fp.coefficient(vi)*c_i.coefficient(vi)) ;
+	  k = fp_i*c_i.coefficient(vj);
+	  le += k*vj;
 	}
       }
       // Note that we can neglect the divisor of `fp' since it is positive.
diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc
index 92a902b..a24b067 100644
--- a/tests/Polyhedron/termination1.cc
+++ b/tests/Polyhedron/termination1.cc
@@ -155,7 +155,7 @@ test05() {
   Variable mu1(0);
   Variable mu2(1);
   Variable mu0(2);
-  Generator known_result(point(0*mu0 + 1*mu1 + 0*mu2));
+  Generator known_result(point(0*mu0 + 2*mu1 + 0*mu2));
 
   print_generator(known_result, "*** known_result ***");