March 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Added to Prolog interface the predicates for quasi-ranking functions.
by Enea Zaffanella 29 Mar '10

29 Mar '10

Module: ppl/ppl Branch: master Commit: f7c33880fca5903781922d35eb284d4e8e44c623 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f7c33880fca5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Mar 29 10:08:20 2010 +0200 Added to Prolog interface the predicates for quasi-ranking functions. --- .../ppl_interface_generator_prolog_cc_code.m4 | 124 ++++++++++++++++---- .../ppl_interface_generator_prolog_hh_code.m4 | 19 +++ ...erface_generator_prolog_procedure_generators.m4 | 2 + 3 files changed, 121 insertions(+), 24 deletions(-) diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 index 39dcd33..de6a103 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 @@ -1243,7 +1243,7 @@ m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', @TOPOLOGY@@CPP_CLASS@* pset = term_to_handle<@TOPOLOGY@@CPP_CLASS@ >(t_pset, where); PPL_CHECK(pset); if (Parma_Polyhedra_Library::termination_test_@TERMINATION_ID@(*pset)) - return PROLOG_SUCCESS; + return PROLOG_SUCCESS; } CATCH_ALL; } @@ -1265,7 +1265,7 @@ m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', PPL_CHECK(pset_after); if (Parma_Polyhedra_Library ::termination_test_@TERMINATION_ID@_2(*pset_before, *pset_after)) - return PROLOG_SUCCESS; + return PROLOG_SUCCESS; } CATCH_ALL; } @@ -1285,8 +1285,8 @@ m4_define(`ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_co PPL_CHECK(pset); if (Parma_Polyhedra_Library ::one_affine_ranking_function_@TERMINATION_ID@(*pset, gg) - && Prolog_unify(t_g, generator_term(gg))) - return PROLOG_SUCCESS; + && Prolog_unify(t_g, generator_term(gg))) + return PROLOG_SUCCESS; } CATCH_ALL; } @@ -1310,16 +1310,17 @@ m4_define(`ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_ PPL_CHECK(pset_before); PPL_CHECK(pset_after); if (Parma_Polyhedra_Library - ::one_affine_ranking_function_@TERMINATION_ID@_2(*pset_before, - *pset_after, - gg) + ::one_affine_ranking_function_@TERMINATION_ID@_2(*pset_before, + *pset_after, + gg) && Prolog_unify(t_g, generator_term(gg))) - return PROLOG_SUCCESS; + return PROLOG_SUCCESS; } CATCH_ALL; } ') + m4_define(`ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', `extern "C" Prolog_foreign_return_type ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ @@ -1333,15 +1334,14 @@ m4_define(`ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_c @A_TERMINATION_ID@Polyhedron* ph = new @A_TERMINATION_ID@Polyhedron(); Parma_Polyhedra_Library ::all_affine_ranking_functions_@TERMINATION_ID@(*pset, *ph); - Prolog_term_ref tmp = Prolog_new_term_ref(); - Prolog_put_address(tmp, ph); - if (Prolog_unify(t_ph, tmp)) { - PPL_REGISTER(ph); - return PROLOG_SUCCESS; - } - else + Prolog_term_ref tmp = Prolog_new_term_ref(); + Prolog_put_address(tmp, ph); + if (Prolog_unify(t_ph, tmp)) { + PPL_REGISTER(ph); + return PROLOG_SUCCESS; + } + else delete ph; - return PROLOG_SUCCESS; } CATCH_ALL; } @@ -1368,15 +1368,91 @@ m4_define(`ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2 ::all_affine_ranking_functions_@TERMINATION_ID@_2(*pset_before, *pset_after, *ph); - Prolog_term_ref tmp = Prolog_new_term_ref(); - Prolog_put_address(tmp, ph); - if (Prolog_unify(t_ph, tmp)) { - PPL_REGISTER(ph); - return PROLOG_SUCCESS; - } - else + Prolog_term_ref tmp = Prolog_new_term_ref(); + Prolog_put_address(tmp, ph); + if (Prolog_unify(t_ph, tmp)) { + PPL_REGISTER(ph); + return PROLOG_SUCCESS; + } + else delete ph; - return PROLOG_SUCCESS; + } + CATCH_ALL; +} + +') + +m4_define(`ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_code', + `extern "C" Prolog_foreign_return_type + ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@ + (Prolog_term_ref t_pset, + Prolog_term_ref t_ph_decreasing, + Prolog_term_ref t_ph_bounded) { + static const char* where = + "ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@/3"; + try { + @TOPOLOGY@@CPP_CLASS@* pset = term_to_handle<@TOPOLOGY@@CPP_CLASS@ >(t_pset, where); + PPL_CHECK(pset); + C_Polyhedron* ph_decreasing = new C_Polyhedron(); + C_Polyhedron* ph_bounded = new C_Polyhedron(); + Parma_Polyhedra_Library + ::all_affine_quasi_ranking_functions_MS(*pset, + *ph_decreasing, *ph_bounded); + Prolog_term_ref tmp_decreasing = Prolog_new_term_ref(); + Prolog_put_address(tmp_decreasing, ph_decreasing); + Prolog_term_ref tmp_bounded = Prolog_new_term_ref(); + Prolog_put_address(tmp_bounded, ph_bounded); + if (Prolog_unify(t_ph_decreasing, tmp_decreasing) + && Prolog_unify(t_ph_bounded, tmp_bounded)) { + PPL_REGISTER(ph_decreasing); + PPL_REGISTER(ph_bounded); + return PROLOG_SUCCESS; + } + else { + delete ph_decreasing; + delete ph_bounded; + } + } + CATCH_ALL; +} + +') + +m4_define(`ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2_code', + `extern "C" Prolog_foreign_return_type + ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2 + (Prolog_term_ref t_pset_before, + Prolog_term_ref t_pset_after, + Prolog_term_ref t_ph_decreasing, + Prolog_term_ref t_ph_bounded) { + static const char* where = + "ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2/4"; + try { + @TOPOLOGY@@CPP_CLASS@* pset_before + = term_to_handle<@TOPOLOGY@@CPP_CLASS@ >(t_pset_before, where); + @TOPOLOGY@@CPP_CLASS@* pset_after + = term_to_handle<@TOPOLOGY@@CPP_CLASS@ >(t_pset_after, where); + PPL_CHECK(pset_before); + PPL_CHECK(pset_after); + C_Polyhedron* ph_decreasing = new C_Polyhedron(); + C_Polyhedron* ph_bounded = new C_Polyhedron(); + Parma_Polyhedra_Library + ::all_affine_quasi_ranking_functions_MS_2(*pset_before, *pset_after, + *ph_decreasing, *ph_bounded); + Prolog_term_ref tmp_decreasing = Prolog_new_term_ref(); + Prolog_put_address(tmp_decreasing, ph_decreasing); + Prolog_term_ref tmp_bounded = Prolog_new_term_ref(); + Prolog_put_address(tmp_bounded, ph_bounded); + if (Prolog_unify(t_ph_decreasing, tmp_decreasing) + && Prolog_unify(t_ph_bounded, tmp_bounded)) { + PPL_REGISTER(ph_decreasing); + PPL_REGISTER(ph_bounded); + return PROLOG_SUCCESS; + } + else { + delete ph_decreasing; + delete ph_bounded; + } } CATCH_ALL; } diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 index 846fe05..2ffaf4b 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 @@ -573,6 +573,25 @@ m4_define(`ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2 ') +m4_define(`ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_code', + `extern "C" Prolog_foreign_return_type + ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@ + (Prolog_term_ref t_pset, + Prolog_term_ref t_ph_decreasing, + Prolog_term_ref t_ph_bounded); + +') + +m4_define(`ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2_code', + `extern "C" Prolog_foreign_return_type + ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2 + (Prolog_term_ref t_pset_before, + Prolog_term_ref t_pset_after, + Prolog_term_ref t_ph_decreasing, + Prolog_term_ref t_ph_bounded); + +') + m4_define(`ppl_@CLASS@_wrap_assign_code', `extern "C" Prolog_foreign_return_type ppl_@CLASS@_wrap_assign diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 index 685844f..e8b76b7 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 @@ -90,8 +90,10 @@ m4_define(`m4_procedure_list', ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@/1 +simple, ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@/2 +simple, ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@/2 +simple, +ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@/3 +simple, ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2/2 +simple, ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2/3 +simple, ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2/3 +simple, +ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2/4 +simple, ) ')

1 0

[GIT] ppl/ppl(master): Added procedures computing all the affine quasi-ranking functions.
by Enea Zaffanella 29 Mar '10

29 Mar '10

Module: ppl/ppl Branch: master Commit: 5707e3d66eca4be05ef4891081217c1cac5fb96e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5707e3d66eca… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Mar 29 09:17:19 2010 +0200 Added procedures computing all the affine quasi-ranking functions. Corrected a few glitches in the documentation and in exception messages. --- src/termination.cc | 38 ++++++++++++ src/termination.defs.hh | 134 ++++++++++++++++++++++++++++++++++++++---- src/termination.templates.hh | 87 ++++++++++++++++++++++----- 3 files changed, 233 insertions(+), 26 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5707e3d6…

1 0

[GIT] ppl/ppl(master): Factored away common code in the MS-based termination procedures.
by Enea Zaffanella 27 Mar '10

27 Mar '10

Module: ppl/ppl Branch: master Commit: d05d653edab6827589a3138989fac44bd2f9db49 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d05d653edab6… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 27 15:55:01 2010 +0100 Factored away common code in the MS-based termination procedures. Improved PR-based termination procedures relying on MIP_Problem by mapping optimizations to satisfiability testing. --- src/termination.cc | 388 +++++++++++++++--------------------------- src/termination.templates.hh | 13 -- 2 files changed, 136 insertions(+), 265 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=d05d653e…

1 0

[GIT] ppl/ppl(master): Avoid a few annoying warnings for unused parameters.
by Enea Zaffanella 27 Mar '10

27 Mar '10

Module: ppl/ppl Branch: master Commit: 5f9556efda1f122c17b38d10cf08e66c07cd2df9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5f9556efda1f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 27 15:19:14 2010 +0100 Avoid a few annoying warnings for unused parameters. Indentation fixed. Avoid using "return;" at the end of function body. --- src/BD_Shape.templates.hh | 4 ++-- src/Box.templates.hh | 4 ++-- src/Grid_public.cc | 25 ++++++------------------- src/Octagonal_Shape.templates.hh | 4 ++-- src/Polyhedron.defs.hh | 2 +- src/Polyhedron.inlines.hh | 4 ++-- 6 files changed, 15 insertions(+), 28 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 663ff36..e580ec8 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -6344,7 +6344,7 @@ BD_Shape<T>::fold_space_dimensions(const Variables_Set& vars, template <typename T> void -BD_Shape<T>::drop_some_non_integer_points(Complexity_Class complexity) { +BD_Shape<T>::drop_some_non_integer_points(Complexity_Class) { if (std::numeric_limits<T>::is_integer) return; @@ -6354,7 +6354,7 @@ BD_Shape<T>::drop_some_non_integer_points(Complexity_Class complexity) { template <typename T> void BD_Shape<T>::drop_some_non_integer_points(const Variables_Set& vars, - Complexity_Class complexity) { + Complexity_Class) { // Dimension-compatibility check. const dimension_type min_space_dim = vars.space_dimension(); if (space_dimension() < min_space_dim) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 674fd44..524a4f5 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1669,7 +1669,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, template <typename ITV> void -Box<ITV>::drop_some_non_integer_points(Complexity_Class complexity) { +Box<ITV>::drop_some_non_integer_points(Complexity_Class) { if (std::numeric_limits<typename ITV::boundary_type>::is_integer && !ITV::info_type::store_open) return; @@ -1680,7 +1680,7 @@ Box<ITV>::drop_some_non_integer_points(Complexity_Class complexity) { template <typename ITV> void Box<ITV>::drop_some_non_integer_points(const Variables_Set& vars, - Complexity_Class complexity) { + Complexity_Class) { // Dimension-compatibility check. const dimension_type min_space_dim = vars.space_dimension(); if (space_dimension() < min_space_dim) diff --git a/src/Grid_public.cc b/src/Grid_public.cc index ad89369..6d17f57 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2851,7 +2851,6 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, } } } - return; } // FIXME(0.11): Check if this is the correct interpretation of the @@ -2861,20 +2860,14 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // coordinates. All points in \p *this with non-integral coordinates are // removed. void - PPL::Grid::drop_some_non_integer_points(Complexity_Class) { - - if (marked_empty()) - return; - - // Space dimension = 0: then return - if (space_dim == 0) +PPL::Grid::drop_some_non_integer_points(Complexity_Class) { + if (marked_empty() || space_dim == 0) return; for (dimension_type i = space_dim; i-- > 0; ) add_congruence(Variable(i) %= 0); PPL_ASSERT(OK()); - return; } // FIXME(0.11): Check if this is the correct interpretation of the @@ -2885,28 +2878,22 @@ void // dimensions in vars. All points in \p *this with non-integral coordinates // for the dimensions in vars are removed. void - PPL::Grid::drop_some_non_integer_points(const Variables_Set& vars, - Complexity_Class) { +PPL::Grid::drop_some_non_integer_points(const Variables_Set& vars, + Complexity_Class) { // Dimension-compatibility check. const dimension_type min_space_dim = vars.space_dimension(); if (space_dimension() < min_space_dim) throw_dimension_incompatible("drop_some_non_integer_points(vs, cmpl)", min_space_dim); - - if (marked_empty()) - return; - - // If vars space dimension is 0: then return - if (min_space_dim == 0) + if (marked_empty() || min_space_dim == 0) return; for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) add_congruence(Variable(*i) %= 0); - PPL_ASSERT(OK()); - return; + PPL_ASSERT(OK()); } diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index d0034a7..94dab08 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -7560,7 +7560,7 @@ Octagonal_Shape<T> template <typename T> void Octagonal_Shape<T> -::drop_some_non_integer_points(Complexity_Class complexity) { +::drop_some_non_integer_points(Complexity_Class) { if (std::numeric_limits<T>::is_integer) return; @@ -7571,7 +7571,7 @@ template <typename T> void Octagonal_Shape<T> ::drop_some_non_integer_points(const Variables_Set& vars, - Complexity_Class complexity) { + Complexity_Class) { // Dimension-compatibility check. const dimension_type min_space_dim = vars.space_dimension(); if (space_dimension() < min_space_dim) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 0a3c86b..a0426f5 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1621,7 +1621,7 @@ public: Currently there is no optimality guarantee, not even if \p complexity is <CODE>ANY_COMPLEXITY</CODE>. */ - void drop_some_non_integer_points(Complexity_Class complexity + void drop_some_non_integer_points(Complexity_Class complexity = ANY_COMPLEXITY); /*! \brief diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh index 2909057..92b0b1d 100644 --- a/src/Polyhedron.inlines.hh +++ b/src/Polyhedron.inlines.hh @@ -433,8 +433,8 @@ Polyhedron::strictly_contains(const Polyhedron& y) const { inline void Polyhedron::drop_some_non_integer_points(Complexity_Class complexity) { - drop_some_non_integer_points(static_cast<const Variables_Set*>(0), - complexity); + const Variables_Set* p_vs = 0; + drop_some_non_integer_points(p_vs, complexity); } inline void

1 0

[GIT] ppl/ppl(master): Comma changed into full-stop.
by Roberto Bagnara 27 Mar '10

27 Mar '10

Module: ppl/ppl Branch: master Commit: 2ec4a13defe7fdee4b182c55859ff926b0f21f4b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2ec4a13defe7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Mar 27 16:07:36 2010 +0400 Comma changed into full-stop. --- src/termination.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 01ab60a..a86126d 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -85,7 +85,7 @@ shift_unprimed_variables(Constraint_System& cs) { - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions \f$ 0, \ldots, n-1 \f$, - \f$ x_1, \ldots, x_n \f$ go onto space dimensions - \f$ n, \ldots, 2n-1 \f$, + \f$ n, \ldots, 2n-1 \f$. . The system does not contain any equality.

1 0

[GIT] ppl/ppl(master): Other minor improvements in assign_all_inequalities_approximation().
by Enea Zaffanella 27 Mar '10

27 Mar '10

Module: ppl/ppl Branch: master Commit: 2fd3833a17b3c175fca9517ce2e5740686f37aee URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fd3833a17b3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 27 11:04:12 2010 +0100 Other minor improvements in assign_all_inequalities_approximation(). --- src/termination.cc | 20 +++++++++++--------- src/termination.templates.hh | 29 ++++++++++++++++------------- 2 files changed, 27 insertions(+), 22 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 8645b4b..01ab60a 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -35,23 +35,25 @@ template <> void assign_all_inequalities_approximation(const C_Polyhedron& ph, Constraint_System& cs) { - cs = ph.minimized_constraints(); - if (cs.has_equalities() > 0) { - Constraint_System tmp_cs; - for (Constraint_System::const_iterator i = cs.begin(), - cs_end = cs.end(); i != cs_end; ++i) { + const Constraint_System& ph_cs = ph.minimized_constraints(); + if (ph_cs.has_equalities()) { + // Translate equalities into inequalities. + for (Constraint_System::const_iterator i = ph_cs.begin(), + i_end = ph_cs.end(); i != i_end; ++i) { const Constraint& c = *i; if (c.is_equality()) { // Insert the two corresponding opposing inequalities. - tmp_cs.insert(Linear_Expression(c) >= 0); - tmp_cs.insert(Linear_Expression(c) <= 0); + cs.insert(Linear_Expression(c) >= 0); + cs.insert(Linear_Expression(c) <= 0); } else // Insert as is. - tmp_cs.insert(c); + cs.insert(c); } - cs = tmp_cs; } + else + // No equality constraints (and no strict inequalities). + cs = ph_cs; } void diff --git a/src/termination.templates.hh b/src/termination.templates.hh index bf754d3..f5dc925 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -149,26 +149,29 @@ template <typename PSET> void assign_all_inequalities_approximation(const PSET& pset, Constraint_System& cs) { - cs = pset.minimized_constraints(); - if (cs.has_strict_inequalities() || cs.has_equalities() > 0) { - Constraint_System tmp_cs; - for (Constraint_System::const_iterator i = cs.begin(), - cs_end = cs.end(); i != cs_end; ++i) { + const Constraint_System& pset_cs = pset.minimized_constraints(); + if (pset_cs.has_strict_inequalities() || pset_cs.has_equalities()) { + // Here we have some strict inequality and/or equality constraints: + // translate them into non-strict inequality constraints. + for (Constraint_System::const_iterator i = pset_cs.begin(), + i_end = pset_cs.end(); i != i_end; ++i) { const Constraint& c = *i; if (c.is_equality()) { - // Insert the two corresponding opposing inequalities. - tmp_cs.insert(Linear_Expression(c) >= 0); - tmp_cs.insert(Linear_Expression(c) <= 0); + // Insert the two corresponding opposing inequalities. + cs.insert(Linear_Expression(c) >= 0); + cs.insert(Linear_Expression(c) <= 0); } else if (c.is_strict_inequality()) - // Insert the non-strict approximation. - tmp_cs.insert(Linear_Expression(c) >= 0); + // Insert the non-strict approximation. + cs.insert(Linear_Expression(c) >= 0); else - // Insert as is. - tmp_cs.insert(c); + // Insert as is. + cs.insert(c); } - cs = tmp_cs; } + else + // No strict inequality and no equality constraints. + cs = pset_cs; } template <>

1 0

[GIT] ppl/ppl(master): Apply more memory allocation improvements.
by Enea Zaffanella 27 Mar '10

27 Mar '10

Module: ppl/ppl Branch: master Commit: 3bda0d459fde855a46cc93aba619f5d422484376 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3bda0d459fde… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 27 09:13:40 2010 +0100 Apply more memory allocation improvements. --- src/termination.cc | 82 +++++++++++++++++++++++++++++++++------------------ 1 files changed, 53 insertions(+), 29 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index a85962f..8645b4b 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -83,7 +83,8 @@ shift_unprimed_variables(Constraint_System& cs) { - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions \f$ 0, \ldots, n-1 \f$, - \f$ x_1, \ldots, x_n \f$ go onto space dimensions - \f$ n, \ldots, 2n-1 \f$. + \f$ n, \ldots, 2n-1 \f$, + . The system does not contain any equality. \param n @@ -124,11 +125,13 @@ fill_constraint_systems_MS(const Constraint_System& cs, Constraint_System& cs_out2) { dimension_type y_begin = n+1; dimension_type z_begin = (&cs_out1 == &cs_out2) ? y_begin + m : y_begin; + // Make sure linear expressions are not reallocated multiple times. Linear_Expression y_le(0*Variable(y_begin + m - 1)); Linear_Expression z_le(0*Variable(z_begin + m + 2 - 1)); - std::vector<Linear_Expression> y_les(2*n); - std::vector<Linear_Expression> z_les(2*n + 1); + std::vector<Linear_Expression> y_les(2*n, y_le); + std::vector<Linear_Expression> z_les(2*n + 1, z_le); + dimension_type y = y_begin; dimension_type z = z_begin; for (Constraint_System::const_iterator i = cs.begin(), @@ -294,7 +297,9 @@ fill_constraint_system_PR(const Constraint_System& cs_before, const dimension_type s = distance(cs_after.begin(), cs_after.end()); const dimension_type m = r + s; - std::vector<Linear_Expression> les_eq(2*n); + // Make sure linear expressions are not reallocated multiple times. + le_out = 0 * Variable(m + r - 1); + std::vector<Linear_Expression> les_eq(2*n, le_out); dimension_type row_index = 0; for (Constraint_System::const_iterator i = cs_before.begin(), @@ -306,14 +311,18 @@ fill_constraint_system_PR(const Constraint_System& cs_before, const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { Coefficient_traits::const_reference A_ij_B = c_i.coefficient(Variable(j)); - // (u1 - u2) A_B, in the context of j-th constraint. - add_mul_assign(les_eq[j], A_ij_B, u1_i); - sub_mul_assign(les_eq[j], A_ij_B, u2_i); - // u2 A_B, in the context of (j+n)-th constraint. - add_mul_assign(les_eq[j + n], A_ij_B, u2_i); + if (A_ij_B != 0) { + // (u1 - u2) A_B, in the context of j-th constraint. + add_mul_assign(les_eq[j], A_ij_B, u1_i); + sub_mul_assign(les_eq[j], A_ij_B, u2_i); + // u2 A_B, in the context of (j+n)-th constraint. + add_mul_assign(les_eq[j + n], A_ij_B, u2_i); + } } - // u2 b_B, in the context of the strict inequality constraint. - add_mul_assign(le_out, c_i.inhomogeneous_term(), u2_i); + Coefficient_traits::const_reference b_B = c_i.inhomogeneous_term(); + if (b_B != 0) + // u2 b_B, in the context of the strict inequality constraint. + add_mul_assign(le_out, b_B, u2_i); } row_index = 0; @@ -326,16 +335,22 @@ fill_constraint_system_PR(const Constraint_System& cs_before, for (dimension_type j = n; j-- > 0; ) { Coefficient_traits::const_reference A_ij_C = c_i.coefficient(Variable(j + n)); + if (A_ij_C != 0) { + // - u3 A_C, in the context of the j-th constraint. + sub_mul_assign(les_eq[j], A_ij_C, u3_i); + // u3 A_C, in the context of the (j+n)-th constraint. + add_mul_assign(les_eq[j+n], A_ij_C, u3_i); + } Coefficient_traits::const_reference Ap_ij_C = c_i.coefficient(Variable(j)); - // - u3 A_C, in the context of the j-th constraint. - sub_mul_assign(les_eq[j], A_ij_C, u3_i); - // u3 (A_C + Ap_C), in the context of the (j+n)-th constraint. - add_mul_assign(les_eq[j+n], A_ij_C, u3_i); - add_mul_assign(les_eq[j+n], Ap_ij_C, u3_i); + if (Ap_ij_C != 0) + // u3 Ap_C, in the context of the (j+n)-th constraint. + add_mul_assign(les_eq[j+n], Ap_ij_C, u3_i); } - // u3 b_C, in the context of the strict inequality constraint. - add_mul_assign(le_out, c_i.inhomogeneous_term(), u3_i); + Coefficient_traits::const_reference b_C = c_i.inhomogeneous_term(); + if (b_C != 0) + // u3 b_C, in the context of the strict inequality constraint. + add_mul_assign(le_out, b_C, u3_i); } // Add the nonnegativity constraints for u_1, u_2 and u_3. @@ -355,7 +370,9 @@ fill_constraint_system_PR_original(const Constraint_System& cs, const dimension_type n = cs.space_dimension() / 2; const dimension_type m = distance(cs.begin(), cs.end()); - std::vector<Linear_Expression> les_eq(3*n); + // Make sure linear expressions are not reallocated multiple times. + le_out = 0 * Variable(2*m - 1); + std::vector<Linear_Expression> les_eq(3*n, le_out); dimension_type row_index = 0; for (Constraint_System::const_iterator i = cs.begin(), @@ -365,18 +382,25 @@ fill_constraint_system_PR_original(const Constraint_System& cs, const Variable lambda2_i(m + row_index); for (dimension_type j = n; j-- > 0; ) { Coefficient_traits::const_reference Ap_ij = c_i.coefficient(Variable(j)); + if (Ap_ij != 0) { + // lambda_1 A' + add_mul_assign(les_eq[j], Ap_ij, lambda1_i); + // lambda_2 A' + add_mul_assign(les_eq[j+n+n], Ap_ij, lambda2_i); + } Coefficient_traits::const_reference A_ij = c_i.coefficient(Variable(j+n)); - // lambda_1 A' - add_mul_assign(les_eq[j], Ap_ij, lambda1_i); - // (lambda_1 - lambda_2) A - add_mul_assign(les_eq[j+n], A_ij, lambda1_i); - sub_mul_assign(les_eq[j+n], A_ij, lambda2_i); - // lambda_2 (A + A') - add_mul_assign(les_eq[j+n+n], A_ij, lambda2_i); - add_mul_assign(les_eq[j+n+n], Ap_ij, lambda2_i); + if (A_ij != 0) { + // (lambda_1 - lambda_2) A + add_mul_assign(les_eq[j+n], A_ij, lambda1_i); + sub_mul_assign(les_eq[j+n], A_ij, lambda2_i); + // lambda_2 A + add_mul_assign(les_eq[j+n+n], A_ij, lambda2_i); + } } - // lambda2 b - add_mul_assign(le_out, c_i.inhomogeneous_term(), lambda2_i); + Coefficient_traits::const_reference b = c_i.inhomogeneous_term(); + if (b != 0) + // lambda2 b + add_mul_assign(le_out, b, lambda2_i); } // Add the non-negativity constraints for lambda_1 and lambda_2.

1 0

[GIT] ppl/ppl(master): A few optimizations applied to fill_constraint_systems_MS().
by Enea Zaffanella 26 Mar '10

26 Mar '10

Module: ppl/ppl Branch: master Commit: 4df3615f9dbfe73d368d219f98c8a8fa65dfe061 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4df3615f9dbf… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Mar 26 16:54:00 2010 +0100 A few optimizations applied to fill_constraint_systems_MS(). --- src/termination.cc | 30 +++++++++++++++++------------- 1 files changed, 17 insertions(+), 13 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 93aaa88..a85962f 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -83,8 +83,7 @@ shift_unprimed_variables(Constraint_System& cs) { - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions \f$ 0, \ldots, n-1 \f$, - \f$ x_1, \ldots, x_n \f$ go onto space dimensions - \f$ n, \ldots, 2n-1 \f$, - . + \f$ n, \ldots, 2n-1 \f$. The system does not contain any equality. \param n @@ -134,22 +133,27 @@ fill_constraint_systems_MS(const Constraint_System& cs, dimension_type z = z_begin; for (Constraint_System::const_iterator i = cs.begin(), cs_end = cs.end(); i != cs_end; ++i) { + Variable vy(y); + Variable vz(z); + ++y; + ++z; + cs_out1.insert(vy >= 0); + cs_out2.insert(vz >= 0); const Constraint& c_i = *i; Coefficient_traits::const_reference b_i = c_i.inhomogeneous_term(); - // Note that b_i is to the left ot the relation sign, hence here - // we have -= and not += just to avoid negating b_i. - sub_mul_assign(y_le, b_i, Variable(y)); - cs_out1.insert(Variable(y) >= 0); - // We have -= and not += for the same reason mentioned above. - sub_mul_assign(z_le, b_i, Variable(z)); - cs_out2.insert(Variable(z) >= 0); + if (b_i != 0) { + // Note that b_i is to the left ot the relation sign, hence here + // we have -= and not += just to avoid negating b_i. + sub_mul_assign(y_le, b_i, vy); + sub_mul_assign(z_le, b_i, vz); + } for (dimension_type j = 2*n; j-- > 0; ) { Coefficient_traits::const_reference a_i_j = c_i.coefficient(Variable(j)); - add_mul_assign(y_les[j], a_i_j, Variable(y)); - add_mul_assign(z_les[j], a_i_j, Variable(z)); + if (a_i_j != 0) { + add_mul_assign(y_les[j], a_i_j, vy); + add_mul_assign(z_les[j], a_i_j, vz); + } } - ++y; - ++z; } z_le += Variable(z); z_les[2*n] += Variable(z);

1 0

[GIT] ppl/ppl(master): Rename Termination.cc in ppl_java_Termination. cc in Java interface.
by Enea Zaffanella 26 Mar '10

26 Mar '10

Module: ppl/ppl Branch: master Commit: 366effb5cb03447652ec899c4c18c88bfdc0ab70 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=366effb5cb03… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Mar 26 07:55:33 2010 +0100 Rename Termination.cc in ppl_java_Termination.cc in Java interface. Add the generated file to CLEANFILES. --- interfaces/Java/jni/Makefile.am | 1 + ...ppl_interface_generator_java_classes_cc_code.m4 | 14 +++++++------- ...pl_interface_generator_java_classes_cc_files.m4 | 2 +- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/interfaces/Java/jni/Makefile.am b/interfaces/Java/jni/Makefile.am index 497728f..79d7919 100644 --- a/interfaces/Java/jni/Makefile.am +++ b/interfaces/Java/jni/Makefile.am @@ -199,6 +199,7 @@ ppl_java_implementation_domains.cc.stamp: $(interface_generator_dependencies) CLEANFILES = \ @required_instantiations_java_cxx_sources@ \ +ppl_java_Termination.cc \ ppl_java_implementation_domains.cc.stamp $(top_builddir)/interfaces/ppl_interface_instantiations.m4: diff --git a/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4 b/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4 index cfa8de9..0fb2a58 100644 --- a/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4 +++ b/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4 @@ -1381,7 +1381,7 @@ Java_parma_1polyhedra_1library_@1CLASS@_approximate_1@PARTITION@ m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_termination_1test_1MS_1@TOPOLOGY@1@CLASS@ @@ -1399,7 +1399,7 @@ Java_parma_1polyhedra_1library_termination_1test_1MS_1@TOPOLOGY@1@CLASS@ m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_termination_1test_1@TERMINATION_ID@_1@TOPOLOGY@1@CLASS@ @@ -1418,7 +1418,7 @@ Java_parma_1polyhedra_1library_termination_1test_1@TERMINATION_ID@_1@TOPOLOGY@1@ m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_termination_1test_1@TERMINATION_ID@_1@TOPOLOGY@1@CLASS@_12 @@ -1439,7 +1439,7 @@ Java_parma_1polyhedra_1library_termination_1test_1@TERMINATION_ID@_1@TOPOLOGY@1@ m4_define(`ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_one_1affine_1ranking_1function_1@TERMINATION_ID@_1@TOPOLOGY@1@CLASS@ @@ -1464,7 +1464,7 @@ Java_parma_1polyhedra_1library_one_1affine_1ranking_1function_1@TERMINATION_ID@_ m4_define(`ppl_one_affine_ranking_function_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_one_1affine_1ranking_1function_1@TERMINATION_ID@_1@TOPOLOGY@1@CLASS@_12 @@ -1491,7 +1491,7 @@ Java_parma_1polyhedra_1library_one_1affine_1ranking_1function_1@TERMINATION_ID@_ m4_define(`ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_all_1affine_1ranking_1functions_1@TERMINATION_ID@_1@TOPOLOGY@1@CLASS@ @@ -1513,7 +1513,7 @@ Java_parma_1polyhedra_1library_all_1affine_1ranking_1functions_1@TERMINATION_ID@ m4_define(`ppl_all_affine_ranking_functions_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', `dnl ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_all_1affine_1ranking_1functions_1@TERMINATION_ID@_1@TOPOLOGY@1@CLASS@_12 diff --git a/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_files.m4 b/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_files.m4 index 6ec6688..f69b156 100644 --- a/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_files.m4 +++ b/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_files.m4 @@ -43,7 +43,7 @@ dnl in the code file outputs a warning message. m4_define(`m4_default_code', `m4_dumpdef($1`'_code)') m4_divert ___END_OF_FILE___ -___BEGIN_OF_FILE___ Termination.cc << ___END_OF_FILE___ +___BEGIN_OF_FILE___ ppl_java_Termination.cc << ___END_OF_FILE___ /* Java Termination interface code. m4_include(`ppl_interface_generator_copyright')`'dnl */

1 0

Re: [PPL-devel] unable to clone ppl git repository
by Roberto Bagnara 26 Mar '10

26 Mar '10

On 03/24/2010 10:31 PM, Bryan Hundven wrote: > $ git clone git://git.cs.unipr.it/ppl/ppl.git > Initialized empty Git repository in /home/bryan/gccfun/src/ppl/.git/ > fatal: read error: Connection reset by peer > > I have been able to clone from other git repositories in just the last > few minutes, but this server always gives me a Connection reset by > peer. Hi Bryan, you must be behind a firewall that is blocking you. We tried using the same command from different locations, and it works: $ git clone git://git.cs.unipr.it/ppl/ppl.git Initialized empty Git repository in /tmp/ppl/.git/ remote: Counting objects: 89722, done. remote: Compressing objects: 100% (26481/26481), done. remote: Total 89722 (delta 71980), reused 79288 (delta 63172) Receiving objects: 100% (89722/89722), 29.70 MiB | 814 KiB/s, done. Resolving deltas: 100% (71980/71980), done. All the best, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 2