[PPL-devel] [GIT] ppl/ppl(termination): Kludge to allow the proof-of-concept implementation of the PR functions to compile .

[Roberto Bagnara]

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

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

Kludge to allow the proof-of-concept implementation of the PR functions to compile.

---

 src/Polyhedron.defs.hh           |   15 +++++++++++
 src/termination.templates.hh     |   51 ++++++++++++++++++++------------------
 tests/Polyhedron/termination1.cc |    2 +-
 3 files changed, 43 insertions(+), 25 deletions(-)

diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index 8981831..0568c2a 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -52,6 +52,10 @@ site: http://www.cs.unipr.it/ppl/ . */
 #include <vector>
 #include <iosfwd>
 
+// FIXME: this is only needed to access the copy constructor of
+// class Polyhedron from the termination utility functions.
+#include "C_Polyhedron.types.hh"
+
 namespace Parma_Polyhedra_Library {
 
 namespace IO_Operators {
@@ -2568,6 +2572,17 @@ private:
   friend class Parma_Polyhedra_Library::BHRZ03_Certificate;
   friend class Parma_Polyhedra_Library::H79_Certificate;
 
+  // FIXME: these are only needed to access the copy constructor of
+  // class Polyhedron.
+  template <typename PSET>
+  friend bool termination_test_PR(const PSET& pset);
+  template <typename PSET>
+  friend bool one_affine_ranking_function_PR(const PSET& pset,
+					     Generator& mu);
+  template <typename PSET>
+  friend void all_affine_ranking_functions_PR(const PSET& pset,
+					      C_Polyhedron& mu_space);
+
 protected:
 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
   /*! \brief
diff --git a/src/termination.templates.hh b/src/termination.templates.hh
index d59bcb6..247a587 100644
--- a/src/termination.templates.hh
+++ b/src/termination.templates.hh
@@ -398,23 +398,6 @@ termination_test_PR(const PSET& 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) {
-    std::ostringstream s;
-    s << "PPL::one_affine_ranking_function_PR(pset):\n"
-         "pset.space_dimension() == " << space_dim
-      << " is odd.";
-    throw std::invalid_argument(s.str());
-  }
-
-  used(mu);
-  throw std::runtime_error("PPL::one_affine_ranking_function_PR()"
-			   " not yet implemented.");
-}
-
-template <typename PSET>
-bool
 one_affine_ranking_function_PR_2(const PSET& pset_before,
 				 const PSET& pset_after,
 				 Generator& mu) {
@@ -438,20 +421,23 @@ one_affine_ranking_function_PR_2(const PSET& pset_before,
 }
 
 template <typename PSET>
-void
-all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) {
-  const dimension_type space_dim = pset.space_dimension();
+bool
+one_affine_ranking_function_PR(const PSET& pset_after, Generator& mu) {
+  const dimension_type space_dim = pset_after.space_dimension();
   if (space_dim % 2 != 0) {
     std::ostringstream s;
-    s << "PPL::all_affine_ranking_functions_PR(pset):\n"
+    s << "PPL::one_affine_ranking_function_PR(pset):\n"
          "pset.space_dimension() == " << space_dim
       << " is odd.";
     throw std::invalid_argument(s.str());
   }
 
-  used(mu_space);
-  throw std::runtime_error("PPL::all_affine_ranking_functions_PR()"
-			   " not yet implemented.");
+  // 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 one_affine_ranking_function_PR_2(pset_before, pset_after, mu);
+
 }
 
 template <typename PSET>
@@ -475,6 +461,23 @@ all_affine_ranking_functions_PR_2(const PSET& pset_before,
 			   " not yet implemented.");
 }
 
+template <typename PSET>
+void
+all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) {
+  const dimension_type space_dim = pset.space_dimension();
+  if (space_dim % 2 != 0) {
+    std::ostringstream s;
+    s << "PPL::all_affine_ranking_functions_PR(pset):\n"
+         "pset.space_dimension() == " << space_dim
+      << " is odd.";
+    throw std::invalid_argument(s.str());
+  }
+
+  used(mu_space);
+  throw std::runtime_error("PPL::all_affine_ranking_functions_PR()"
+			   " not yet implemented.");
+}
+
 } // namespace Parma_Polyhedra_Library
 
 #endif // !defined(PPL_termination_templates_hh)
diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc
index f843ab6..e169729 100644
--- a/tests/Polyhedron/termination1.cc
+++ b/tests/Polyhedron/termination1.cc
@@ -371,7 +371,7 @@ BEGIN_MAIN
   DO_TEST(test02);
   DO_TEST(test03);
   //DO_TEST(test04);
-  //DO_TEST(test05);
+  DO_TEST(test05);
   DO_TEST(test06);
   //DO_TEST(test07);
   DO_TEST(test08);