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

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Thu Mar 18 18:22:59 2010 +0400

Completed the implementation of all_affine_ranking_functions_PR*().

---

src/termination.cc | 87 +++++++++++++++++++++++++++++++++++++- src/termination.defs.hh | 4 +- src/termination.templates.hh | 29 +++++++----- tests/Polyhedron/termination1.cc | 8 ++-- 4 files changed, 108 insertions(+), 20 deletions(-)

diff --git a/src/termination.cc b/src/termination.cc index 2fc0c58..5faf4eb 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -23,6 +23,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <ppl-config.h>

#include "termination.defs.hh" +#include "NNC_Polyhedron.defs.hh"

namespace Parma_Polyhedra_Library {

@@ -564,7 +565,7 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, // function computed in the feasible point is positive. finish: { - // We can impose that the le_ineq is >= 1 because every positive + // We can impose that le_ineq is >= 1 because every positive // multiple of the linear expression is acceptable. mip.add_constraint(le_ineq >= 1); Generator fp = mip.feasible_point(); @@ -615,7 +616,89 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, void all_affine_ranking_functions_PR(const Constraint_System& cs_before, const Constraint_System& cs_after, - C_Polyhedron& mu_space); + NNC_Polyhedron& mu_space) { + Constraint_System cs_eqs; + Linear_Expression le_ineq; + fill_constraint_system_PR(cs_before, cs_after, cs_eqs, le_ineq); + +#if PRINT_DEBUG_INFO + Variable::output_function_type* p_default_output_function + = Variable::get_output_function(); + Variable::set_output_function(output_function_PR); + + output_function_PR_r = distance(cs_before.begin(), cs_before.end()); + output_function_PR_s = distance(cs_after.begin(), cs_after.end()); + + std::cout << "*** cs_eqs ***" << std::endl; + using namespace IO_Operators; + std::cout << cs_eqs << std::endl; + std::cout << "*** le_ineq ***" << std::endl; + std::cout << le_ineq << std::endl; +#endif + + NNC_Polyhedron ph(cs_eqs); + ph.add_constraint(le_ineq > 0); + // u_3 corresponds to space dimensions 0, ..., s - 1. + const dimension_type s = distance(cs_after.begin(), cs_after.end()); + ph.remove_higher_space_dimensions(s); + +#if PRINT_DEBUG_INFO + std::cout << "*** ph ***" << std::endl; + std::cout << ph << std::endl; + + Variable::set_output_function(p_default_output_function); +#endif + + // FIXME: is this useful? + const dimension_type n = cs_before.space_dimension(); + + const Generator_System& gs_in = ph.generators(); + Generator_System gs_out; + for (Generator_System::const_iterator r = gs_in.begin(), + gs_in_end = gs_in.end(); r != gs_in_end; ++r) { + const Generator& g = *r; + Linear_Expression le; + // Set le to the multiplication of Linear_Expression(g) by E'_C. + dimension_type row_index = 0; + PPL_DIRTY_TEMP_COEFFICIENT(k); + for (Constraint_System::const_iterator i = cs_after.begin(), + cs_after_end = cs_after.end(); + i != cs_after_end; + ++i, ++row_index) { + Variable vi(row_index); + Coefficient_traits::const_reference g_i = g.coefficient(vi); + if (g_i != 0) { + const Constraint& c_i = *i; + for (dimension_type j = n; j-- > 0; ) { + Variable vj(j); + k = g_i*c_i.coefficient(vj); + le += k*vj; + } + } + } + + // Add to gs_out the transformed generator. + switch (g.type()) { + case Generator::LINE: + gs_out.insert(line(le)); + break; + case Generator::RAY: + if (!le.all_homogeneous_terms_are_zero()) + gs_out.insert(ray(le)); + break; + case Generator::POINT: + gs_out.insert(point(le, g.divisor())); + break; + case Generator::CLOSURE_POINT: + gs_out.insert(closure_point(le, g.divisor())); + break; + } + } + + mu_space = NNC_Polyhedron(gs_out); + // mu_0 is zero. + mu_space.add_space_dimensions_and_embed(1); +}

} // namespace Termination

diff --git a/src/termination.defs.hh b/src/termination.defs.hh index 1f6f18a..c63e877 100644 --- a/src/termination.defs.hh +++ b/src/termination.defs.hh @@ -333,7 +333,7 @@ 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); +all_affine_ranking_functions_PR(const PSET& pset, NNC_Polyhedron& mu_space);

/*! \brief Like all_affine_ranking_functions_MS_2() but using an improvement @@ -343,7 +343,7 @@ template <typename PSET> void all_affine_ranking_functions_PR_2(const PSET& pset_before, const PSET& pset_after, - C_Polyhedron& mu_space); + NNC_Polyhedron& mu_space);

} // namespace Parma_Polyhedra_Library

diff --git a/src/termination.templates.hh b/src/termination.templates.hh index 247a587..ce365c9 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 0 +#define PRINT_DEBUG_INFO 1

#if PRINT_DEBUG_INFO #include <iostream> @@ -231,7 +231,7 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, void all_affine_ranking_functions_PR(const Constraint_System& cs_before, const Constraint_System& cs_after, - C_Polyhedron& mu_space); + NNC_Polyhedron& mu_space);

} // namespace Termination

@@ -437,14 +437,13 @@ one_affine_ranking_function_PR(const PSET& pset_after, Generator& mu) { 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> void all_affine_ranking_functions_PR_2(const PSET& pset_before, const PSET& pset_after, - C_Polyhedron& mu_space) { + NNC_Polyhedron& mu_space) { const dimension_type before_space_dim = pset_before.space_dimension(); const dimension_type after_space_dim = pset_after.space_dimension(); if (after_space_dim != 2*before_space_dim) { @@ -456,15 +455,19 @@ all_affine_ranking_functions_PR_2(const PSET& pset_before, throw std::invalid_argument(s.str()); }

- used(mu_space); - throw std::runtime_error("PPL::all_affine_ranking_functions_PR_2()" - " not yet implemented."); + using namespace Implementation::Termination; + Constraint_System cs_before; + Constraint_System cs_after; + assign_all_inequalities_approximation(pset_before, cs_before); + assign_all_inequalities_approximation(pset_after, cs_after); + all_affine_ranking_functions_PR(cs_before, cs_after, mu_space); }

template <typename PSET> void -all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) { - const dimension_type space_dim = pset.space_dimension(); +all_affine_ranking_functions_PR(const PSET& pset_after, + NNC_Polyhedron& mu_space) { + 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" @@ -473,9 +476,11 @@ all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) { 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); + all_affine_ranking_functions_PR_2(pset_before, pset_after, mu_space); }

} // namespace Parma_Polyhedra_Library diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index 6ef7e39..90ca22b 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -112,7 +112,7 @@ test04() { ph.add_constraint(xp2 == x2 + 1); ph.add_constraint(xp2 >= 1);

- C_Polyhedron mu_space; + NNC_Polyhedron mu_space; all_affine_ranking_functions_PR(ph, mu_space);

print_constraints(mu_space, "*** mu_space ***"); @@ -120,10 +120,10 @@ test04() { Variable mu1(0); Variable mu2(1); Variable mu0(2); - C_Polyhedron known_result(3); + NNC_Polyhedron known_result(3); known_result.add_constraint(mu1 - mu2 >= 1); + known_result.add_constraint(mu0 + 2*mu1 >= 0); known_result.add_constraint(mu2 >= 0); - known_result.add_constraint(2*mu0 + mu1 + 2*mu2 >= 0);

print_constraints(known_result, "*** known_result ***");

@@ -436,7 +436,7 @@ BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); - //DO_TEST(test04); + DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); DO_TEST(test07);