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

Author: Roberto Bagnara bagnara@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