[PPL-devel] [GIT] ppl/ppl(master): Minor improvements to documentation.
Enea Zaffanella
zaffanella at cs.unipr.it
Thu Apr 15 15:08:28 CEST 2010
Module: ppl/ppl
Branch: master
Commit: bcc4ff72caf513a585ec003e5adaff6aec2fb05b
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bcc4ff72caf513a585ec003e5adaff6aec2fb05b
Author: Enea Zaffanella <zaffanella at 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
More information about the PPL-devel
mailing list