[PPL-devel] [GIT] ppl/ppl(termination): Completed the implementation of all_affine_ranking_functions_PR*().
Roberto Bagnara
bagnara at cs.unipr.it
Thu Mar 18 15:26:42 CET 2010
Module: ppl/ppl
Branch: termination
Commit: dab9262cbdb9166cd4a77a2ec9110c3295b3c773
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dab9262cbdb9166cd4a77a2ec9110c3295b3c773
Author: Roberto Bagnara <bagnara at 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);
More information about the PPL-devel
mailing list