[GIT] ppl/ppl(master): Minor improvements to documentation.

15 Apr 2010

Module: ppl/ppl
Branch: master
Commit: bcc4ff72caf513a585ec003e5adaff6aec2fb05b
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bcc4ff72caf51...
Author: Enea Zaffanella zaffanella@cs.unipr.it
Date:   Thu Apr 15 15:06:28 2010 +0200
Minor improvements to documentation.
Deal with the special cse of an empty input pointset for methods all_affine_*.
Adapted and improved test10 in termination2.cc.
---
src/termination.defs.hh          |   29 ++++++++++++++-----------
 src/termination.templates.hh     |   39 ++++++++++++++++++++++++++++++++-
 tests/Polyhedron/termination2.cc |   43 +++++++++++++++++++++++--------------
 3 files changed, 80 insertions(+), 31 deletions(-)

diff --git a/src/termination.defs.hh b/src/termination.defs.hh
index 8ccfc41..c64ed58 100644
--- a/src/termination.defs.hh
+++ b/src/termination.defs.hh
@@ -23,8 +23,9 @@ site: http://www.cs.unipr.it/ppl/ . */
 #ifndef PPL_termination_defs_hh
 #define PPL_termination_defs_hh 1
-#include "Generator.defs.hh"
-#include "C_Polyhedron.defs.hh"
+#include "Generator.types.hh"
+#include "C_Polyhedron.types.hh"
+#include "NNC_Polyhedron.types.hh"
namespace Parma_Polyhedra_Library {
@@ -408,15 +409,15 @@ all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before,
                                         C_Polyhedron& bounded_mu_space);
/*! \brief
-  Like termination_test_MS() but using an improvement
-  of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]".
+  Like termination_test_MS() but using the method by Podelski and
+  Rybalchenko \ref BMPZ10 "[BMPZ10]".
 */
 template <typename PSET>
 bool
 termination_test_PR(const PSET& pset);
/*! \brief
-  Like termination_test_MS_2() but using an improvement
+  Like termination_test_MS_2() but using an alternative formalization
   of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]".
 */
 template <typename PSET>
@@ -424,16 +425,17 @@ bool
 termination_test_PR_2(const PSET& pset_before, const PSET& pset_after);
/*! \brief
-  Like one_affine_ranking_function_MS() but using an improvement
-  of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]".
+  Like one_affine_ranking_function_MS() but using the method by Podelski
+  and Rybalchenko \ref BMPZ10 "[BMPZ10]".
 */
 template <typename PSET>
 bool
 one_affine_ranking_function_PR(const PSET& pset, Generator& mu);
/*! \brief
-  Like one_affine_ranking_function_MS_2() but using an improvement
-  of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]".
+  Like one_affine_ranking_function_MS_2() but using an alternative
+  formalization of the method by Podelski and Rybalchenko
+  \ref BMPZ10 "[BMPZ10]".
 */
 template <typename PSET>
 bool
@@ -442,16 +444,17 @@ one_affine_ranking_function_PR_2(const PSET& pset_before,
    			 Generator& mu);
/*! \brief
-  Like all_affine_ranking_functions_MS() but using an improvement
-  of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]".
+  Like all_affine_ranking_functions_MS() but using the method by Podelski
+  and Rybalchenko \ref BMPZ10 "[BMPZ10]".
 */
 template <typename PSET>
 void
 all_affine_ranking_functions_PR(const PSET& pset, NNC_Polyhedron& mu_space);
/*! \brief
-  Like all_affine_ranking_functions_MS_2() but using an improvement
-  of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]".
+  Like all_affine_ranking_functions_MS_2() but using an alternative
+  formalization of the method by Podelski and Rybalchenko
+  \ref BMPZ10 "[BMPZ10]".
 */
 template <typename PSET>
 void
diff --git a/src/termination.templates.hh b/src/termination.templates.hh
index f60573c..8582e22 100644
--- a/src/termination.templates.hh
+++ b/src/termination.templates.hh
@@ -23,10 +23,13 @@ site: http://www.cs.unipr.it/ppl/ . */
 #ifndef PPL_termination_templates_hh
 #define PPL_termination_templates_hh 1
+#include "globals.defs.hh"
+#include "Variable.defs.hh"
+#include "Generator.defs.hh"
 #include "Constraint_System.defs.hh"
 #include "C_Polyhedron.defs.hh"
-#include "BD_Shape.defs.hh"
-#include "Octagonal_Shape.defs.hh"
+
+#include <stdexcept>
#define PRINT_DEBUG_INFO 0
@@ -301,6 +304,11 @@ all_affine_ranking_functions_MS(const PSET& pset, C_Polyhedron& mu_space) {
     throw std::invalid_argument(s.str());
   }
+  if (pset.is_empty()) {
+    mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE);
+    return;
+  }
+
   using namespace Implementation::Termination;
   Constraint_System cs;
   assign_all_inequalities_approximation(pset, cs);
@@ -324,6 +332,11 @@ all_affine_ranking_functions_MS_2(const PSET& pset_before,
     throw std::invalid_argument(s.str());
   }
+  if (pset_before.is_empty()) {
+    mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE);
+    return;
+  }
+
   using namespace Implementation::Termination;
   Constraint_System cs;
   assign_all_inequalities_approximation(pset_before, pset_after, cs);
@@ -345,6 +358,12 @@ all_affine_quasi_ranking_functions_MS(const PSET& pset,
     throw std::invalid_argument(s.str());
   }
+  if (pset.is_empty()) {
+    decreasing_mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE);
+    bounded_mu_space = decreasing_mu_space;
+    return;
+  }
+
   using namespace Implementation::Termination;
   Constraint_System cs;
   assign_all_inequalities_approximation(pset, cs);
@@ -371,6 +390,12 @@ all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before,
     throw std::invalid_argument(s.str());
   }
+  if (pset_before.is_empty()) {
+    decreasing_mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE);
+    bounded_mu_space = decreasing_mu_space;
+    return;
+  }
+
   using namespace Implementation::Termination;
   Constraint_System cs;
   assign_all_inequalities_approximation(pset_before, pset_after, cs);
@@ -479,6 +504,11 @@ all_affine_ranking_functions_PR_2(const PSET& pset_before,
     throw std::invalid_argument(s.str());
   }
+  if (pset_before.is_empty()) {
+    mu_space = NNC_Polyhedron(1 + before_space_dim);
+    return;
+  }
+
   using namespace Implementation::Termination;
   Constraint_System cs_before;
   Constraint_System cs_after;
@@ -500,6 +530,11 @@ all_affine_ranking_functions_PR(const PSET& pset_after,
     throw std::invalid_argument(s.str());
   }
+  if (pset_after.is_empty()) {
+    mu_space = NNC_Polyhedron(1 + space_dim/2);
+    return;
+  }
+
   using namespace Implementation::Termination;
   Constraint_System cs;
   assign_all_inequalities_approximation(pset_after, cs);
diff --git a/tests/Polyhedron/termination2.cc b/tests/Polyhedron/termination2.cc
index 43fcceb..496a476 100644
--- a/tests/Polyhedron/termination2.cc
+++ b/tests/Polyhedron/termination2.cc
@@ -128,26 +128,37 @@ test09() {
bool
 test10() {
-  C_Polyhedron ph1(2, EMPTY);
-  C_Polyhedron ph2(4, EMPTY);
+  C_Polyhedron ph_before(2, EMPTY);
+  C_Polyhedron ph_after(4, EMPTY);
   C_Polyhedron c_mu_space;
   NNC_Polyhedron nnc_mu_space;
-  all_affine_ranking_functions_MS(ph1, c_mu_space);
-  all_affine_ranking_functions_MS_2(ph1, ph2, c_mu_space);
-  all_affine_ranking_functions_PR(ph1, nnc_mu_space);
-  all_affine_ranking_functions_PR_2(ph1, ph2, nnc_mu_space);
+  C_Polyhedron c_known_result(3, UNIVERSE);
+  NNC_Polyhedron nnc_known_result(3, UNIVERSE);
+  bool ok = true;
-  C_Polyhedron c_known_result(2, EMPTY);
-  c_known_result.add_generator(point());
-  NNC_Polyhedron nnc_known_result(3, EMPTY);
-  nnc_known_result.add_generator(point());
+  all_affine_ranking_functions_MS(ph_after, c_mu_space);
+  ok &= (c_mu_space == c_known_result);
-  print_constraints(ph1, "*** ph ***");
-  print_constraints(c_mu_space, "*** c_mu_space ***");
-  print_constraints(nnc_known_result, "*** nnc_known_result ***");
-  print_constraints(nnc_mu_space, "*** nnc_mu_space ***");
+  all_affine_ranking_functions_MS_2(ph_before, ph_after, c_mu_space);
+  ok &= (c_mu_space == c_known_result);
-  return ph1.OK() && (nnc_mu_space == nnc_known_result);
+//   all_affine_ranking_functions_PR(ph_after, nnc_mu_space);
+//   ok &= (nnc_mu_space == nnc_known_result);
+
+  all_affine_ranking_functions_PR_2(ph_before, ph_after, nnc_mu_space);
+  ok &= (nnc_mu_space == nnc_known_result);
+
+  print_constraints(ph_after, "*** ph_after ***");
+
+  print_generators(c_known_result.minimized_generators(),
+                   "*** c_known_result ***");
+  print_generators(nnc_known_result.minimized_generators(),
+                   "*** nnc_known_result ***");
+
+  print_generators(c_mu_space.minimized_generators(), "*** c_mu_space ***");
+  print_generators(nnc_mu_space.minimized_generators(), "*** nnc_mu_space ***");
+
+  return ok;
 }
} // namespace
@@ -162,5 +173,5 @@ BEGIN_MAIN
   DO_TEST(test07);
   DO_TEST(test08);
   DO_TEST(test09);
-  DO_TEST_F(test10);
+  DO_TEST(test10);
 END_MAIN

    

Enea Zaffanella

tags (0)

participants (1)