[PPL-devel] [GIT] ppl/ppl(termination): Temporarily implemented termination_test_PR() in terms of termination_test_PR_2().

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Wed Mar 17 15:11:07 2010 +0400

Temporarily implemented termination_test_PR() in terms of termination_test_PR_2().

---

 src/termination.templates.hh     |   37 ++++++++++++++++++++-----------------
 tests/Polyhedron/termination1.cc |   28 ++++++++++++++++++++++++----
 2 files changed, 44 insertions(+), 21 deletions(-)

diff --git a/src/termination.templates.hh b/src/termination.templates.hh
index b42cdc0..d59bcb6 100644
--- a/src/termination.templates.hh
+++ b/src/termination.templates.hh
@@ -28,7 +28,7 @@ site: http://www.cs.unipr.it/ppl/ . */
 #include "BD_Shape.defs.hh"
 #include "Octagonal_Shape.defs.hh"
 
-#define PRINT_DEBUG_INFO 1
+#define PRINT_DEBUG_INFO 0
 
 #if PRINT_DEBUG_INFO
 #include <iostream>
@@ -357,22 +357,6 @@ all_affine_ranking_functions_MS_2(const PSET& pset_before,
 
 template <typename PSET>
 bool
-termination_test_PR(const PSET& pset) {
-  const dimension_type space_dim = pset.space_dimension();
-  if (space_dim % 2 != 0) {
-    std::ostringstream s;
-    s << "PPL::termination_test_PR(pset):\n"
-         "pset.space_dimension() == " << space_dim
-      << " is odd.";
-    throw std::invalid_argument(s.str());
-  }
-
-  throw std::runtime_error("PPL::termination_test_PR()"
-			   " not yet implemented.");
-}
-
-template <typename PSET>
-bool
 termination_test_PR_2(const PSET& pset_before, const PSET& pset_after) {
   const dimension_type before_space_dim = pset_before.space_dimension();
   const dimension_type after_space_dim = pset_after.space_dimension();
@@ -395,6 +379,25 @@ termination_test_PR_2(const PSET& pset_before, const PSET& pset_after) {
 
 template <typename PSET>
 bool
+termination_test_PR(const PSET& pset_after) {
+  const dimension_type space_dim = pset_after.space_dimension();
+  if (space_dim % 2 != 0) {
+    std::ostringstream s;
+    s << "PPL::termination_test_PR(pset):\n"
+         "pset.space_dimension() == " << space_dim
+      << " is odd.";
+    throw std::invalid_argument(s.str());
+  }
+
+  // FIXME: this may be inefficient.
+  PSET pset_before(pset_after);
+  Variables_Set primed_variables(Variable(0), Variable(space_dim/2 - 1));
+  pset_before.remove_space_dimensions(primed_variables);
+  return termination_test_PR_2(pset_before, pset_after);
+}
+
+template <typename PSET>
+bool
 one_affine_ranking_function_PR(const PSET& pset, Generator& mu) {
   const dimension_type space_dim = pset.space_dimension();
   if (space_dim % 2 != 0) {
diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc
index b096391..f843ab6 100644
--- a/tests/Polyhedron/termination1.cc
+++ b/tests/Polyhedron/termination1.cc
@@ -300,7 +300,8 @@ test12() {
   {
     Variable x1(0);
     Variable x2(1);
-    // ph_before is universe.
+    ph_before.add_constraint(x1 >= 1);
+    ph_before.add_constraint(x2 <= 0);
   }
 
   C_Polyhedron ph_after(4);
@@ -312,9 +313,7 @@ test12() {
     Variable xp2(1);
 
     ph_after.add_constraint(xp2 == 1);
-    ph_after.add_constraint(x1 >= 1);
     ph_after.add_constraint(x1 - xp1 >= 1);
-    ph_after.add_constraint(x2 <= 0);
   }
 
   return termination_test_MS_2(ph_before, ph_after);
@@ -345,6 +344,26 @@ test13() {
   return termination_test_PR_2(ph_before, ph_after);
 }
 
+bool
+test14() {
+  C_Polyhedron ph(4);
+  {
+    Variable x1(2);
+    Variable x2(3);
+
+    Variable xp1(0);
+    Variable xp2(1);
+
+    ph.add_constraint(xp2 == 1);
+    ph.add_constraint(x1 >= 1);
+    ph.add_constraint(x1 - xp1 >= 1);
+    ph.add_constraint(x2 <= 0);
+  }
+
+  return termination_test_PR(ph);
+}
+
+
 } // namespace
 
 BEGIN_MAIN
@@ -356,9 +375,10 @@ BEGIN_MAIN
   DO_TEST(test06);
   //DO_TEST(test07);
   DO_TEST(test08);
-  DO_TEST_F(test09);
+  DO_TEST(test09);
   DO_TEST(test10);
   DO_TEST(test11);
   DO_TEST(test12);
   DO_TEST(test13);
+  DO_TEST(test14);
 END_MAIN