- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed the all_affine_ranking_functions_PR*() functions to correctly deal with the case where the system is unsatisfiable .
by Roberto Bagnara 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: b28f49a5038aaef781fb95b4e92631c041e59649 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b28f49a5038a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Mar 25 09:41:59 2010 +0400 Fixed the all_affine_ranking_functions_PR*() functions to correctly deal with the case where the system is unsatisfiable. --- src/termination.cc | 170 ++++++++++++++++++++++++++++------------------------ 1 files changed, 91 insertions(+), 79 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 3626b3a..6876232 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -803,51 +803,57 @@ all_affine_ranking_functions_PR(const Constraint_System& cs_before, 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; + Generator_System::const_iterator gs_in_it = gs_in.begin(); + Generator_System::const_iterator gs_in_end = gs_in.end(); + if (gs_in_it == gs_in_end) + // The system is unsatisfiable. + mu_space = NNC_Polyhedron(n + 1, EMPTY); + else { + for ( ; gs_in_it != gs_in_end; ++gs_in_it) { + const Generator& g = *gs_in_it; + 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: - if (!le.all_homogeneous_terms_are_zero()) - 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; + // Add to gs_out the transformed generator. + switch (g.type()) { + case Generator::LINE: + if (!le.all_homogeneous_terms_are_zero()) + 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); + mu_space = NNC_Polyhedron(gs_out); + // mu_0 is zero. + mu_space.add_space_dimensions_and_embed(1); + } } void @@ -877,50 +883,56 @@ all_affine_ranking_functions_PR_original(const Constraint_System& cs, 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.begin(), - cs_end = cs.end(); i != cs_end; ++i, ++row_index) { - Variable lambda_2(row_index); - Coefficient_traits::const_reference g_i = g.coefficient(lambda_2); - if (g_i != 0) { - const Constraint& c_i = *i; - for (dimension_type j = n; j-- > 0; ) { - Variable vj(j); - Coefficient_traits::const_reference Ap_j = c_i.coefficient(vj); - k = g_i * Ap_j; - le -= k * vj; + Generator_System::const_iterator gs_in_it = gs_in.begin(); + Generator_System::const_iterator gs_in_end = gs_in.end(); + if (gs_in_it == gs_in_end) + // The system is unsatisfiable. + mu_space = NNC_Polyhedron(n + 1, EMPTY); + else { + for ( ; gs_in_it != gs_in_end; ++gs_in_it) { + const Generator& g = *gs_in_it; + 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.begin(), + cs_end = cs.end(); i != cs_end; ++i, ++row_index) { + Variable lambda_2(row_index); + Coefficient_traits::const_reference g_i = g.coefficient(lambda_2); + if (g_i != 0) { + const Constraint& c_i = *i; + for (dimension_type j = n; j-- > 0; ) { + Variable vj(j); + Coefficient_traits::const_reference Ap_j = c_i.coefficient(vj); + k = g_i * Ap_j; + le -= k * vj; + } } } - } - // Add to gs_out the transformed generator. - switch (g.type()) { - case Generator::LINE: - if (!le.all_homogeneous_terms_are_zero()) - 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; + // Add to gs_out the transformed generator. + switch (g.type()) { + case Generator::LINE: + if (!le.all_homogeneous_terms_are_zero()) + 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); + mu_space = NNC_Polyhedron(gs_out); + // mu_0 is zero. + mu_space.add_space_dimensions_and_embed(1); + } } } // namespace Termination

1 0

[GIT] ppl/ppl(master): Implemented methods Pointset_Powerset:: drop_some_non_integer_points().
by Roberto Bagnara 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: b54b2fabc3bea07c599a68f6a8ba8db35476fe06 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b54b2fabc3be… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Mar 25 07:22:25 2010 +0400 Implemented methods Pointset_Powerset::drop_some_non_integer_points(). --- ...erface_generator_common_procedure_generators.m4 | 4 +- src/Pointset_Powerset.defs.hh | 33 ++++++++++++++++++++ src/Pointset_Powerset.templates.hh | 25 +++++++++++++++ 3 files changed, 60 insertions(+), 2 deletions(-) diff --git a/interfaces/ppl_interface_generator_common_procedure_generators.m4 b/interfaces/ppl_interface_generator_common_procedure_generators.m4 index 48cde25..e93d96b 100644 --- a/interfaces/ppl_interface_generator_common_procedure_generators.m4 +++ b/interfaces/ppl_interface_generator_common_procedure_generators.m4 @@ -90,8 +90,8 @@ ppl_@CLASS@_remove_higher_space_dimensions/2 *nofail +all, ppl_@CLASS@_expand_space_dimension/3 *nofail +all, ppl_@CLASS@_fold_space_dimensions/3 +all, ppl_@CLASS@_map_space_dimensions/2 +all, -ppl_@CLASS@_drop_some_non_integer_points/2 +simple -pointset_powerset, -ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple -pointset_powerset, +ppl_@CLASS@_drop_some_non_integer_points/2 +simple, +ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple, ppl_@CLASS@_ascii_dump/1 +all, ppl_@CLASS@_@MEMBYTES@/2 +all, dnl diff --git a/src/Pointset_Powerset.defs.hh b/src/Pointset_Powerset.defs.hh index 6e6e362..849e971 100644 --- a/src/Pointset_Powerset.defs.hh +++ b/src/Pointset_Powerset.defs.hh @@ -681,6 +681,39 @@ public: */ void unconstrain(const Variables_Set& vars); + /*! \brief + Possibly tightens \p *this by dropping some points with non-integer + coordinates. + + \param complexity + The maximal complexity of any algorithms used. + + \note + 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 + = ANY_COMPLEXITY); + + /*! \brief + Possibly tightens \p *this by dropping some points with non-integer + coordinates for the space dimensions corresponding to \p vars. + + \param vars + Points with non-integer coordinates for these variables/space-dimensions + can be discarded. + + \param complexity + The maximal complexity of any algorithms used. + + \note + Currently there is no optimality guarantee, not even if + \p complexity is <CODE>ANY_COMPLEXITY</CODE>. + */ + void drop_some_non_integer_points(const Variables_Set& vars, + Complexity_Class complexity + = ANY_COMPLEXITY); + //! Assigns to \p *this its topological closure. void topological_closure_assign(); diff --git a/src/Pointset_Powerset.templates.hh b/src/Pointset_Powerset.templates.hh index 8e53200..d759e7b 100644 --- a/src/Pointset_Powerset.templates.hh +++ b/src/Pointset_Powerset.templates.hh @@ -625,6 +625,31 @@ Pointset_Powerset<PSET>::is_disjoint_from(const Pointset_Powerset& y) const { template <typename PSET> void +Pointset_Powerset<PSET> +::drop_some_non_integer_points(const Variables_Set& vars, + Complexity_Class complexity) { + Pointset_Powerset& x = *this; + for (Sequence_iterator si = x.sequence.begin(), + s_end = x.sequence.end(); si != s_end; ++si) + si->pointset().drop_some_non_integer_points(vars, complexity); + x.reduced = false; + PPL_ASSERT_HEAVY(x.OK()); +} + +template <typename PSET> +void +Pointset_Powerset<PSET> +::drop_some_non_integer_points(Complexity_Class complexity) { + Pointset_Powerset& x = *this; + for (Sequence_iterator si = x.sequence.begin(), + s_end = x.sequence.end(); si != s_end; ++si) + si->pointset().drop_some_non_integer_points(complexity); + x.reduced = false; + PPL_ASSERT_HEAVY(x.OK()); +} + +template <typename PSET> +void Pointset_Powerset<PSET>::topological_closure_assign() { Pointset_Powerset& x = *this; for (Sequence_iterator si = x.sequence.begin(),

1 0

[GIT] ppl/ppl(master): Test Polyhedron::drop_some_non_integer_points().
by Roberto Bagnara 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: f34bcd0e0c7397ac91ba95d562446acd8f1efef7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f34bcd0e0c73… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Mar 25 07:07:04 2010 +0400 Test Polyhedron::drop_some_non_integer_points(). --- tests/Polyhedron/Makefile.am | 8 + tests/Polyhedron/dropsomenonintegerpoints1.cc | 174 +++++++++++++++++++++++++ tests/Polyhedron/dropsomenonintegerpoints2.cc | 160 +++++++++++++++++++++++ 3 files changed, 342 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/Makefile.am b/tests/Polyhedron/Makefile.am index 22cbec0..2096287 100644 --- a/tests/Polyhedron/Makefile.am +++ b/tests/Polyhedron/Makefile.am @@ -81,6 +81,7 @@ constraints1 \ contains1 contains2 \ containsintegerpoint1 \ disjoint1 disjoint2 \ +dropsomenonintegerpoints1 dropsomenonintegerpoints2 \ dualhypercubes \ empty1 \ equals1 \ @@ -169,6 +170,7 @@ nnc_constraints1 \ nnc_contains1 \ nnc_containsintegerpoint1 \ nnc_disjoint1 \ +nnc_dropsomenonintegerpoints1 \ nnc_empty1 \ nnc_equals1 \ nnc_exceptions1 nnc_exceptions3 \ @@ -288,6 +290,9 @@ containsintegerpoint1_SOURCES = containsintegerpoint1.cc disjoint1_SOURCES = disjoint1.cc disjoint2_SOURCES = disjoint2.cc +dropsomenonintegerpoints1_SOURCES = dropsomenonintegerpoints1.cc +dropsomenonintegerpoints2_SOURCES = dropsomenonintegerpoints2.cc + dualhypercubes_SOURCES = dualhypercubes.cc empty1_SOURCES = empty1.cc @@ -517,6 +522,9 @@ nnc_containsintegerpoint1_CXXFLAGS = $(DERIVED_CXXFLAGS) nnc_disjoint1_SOURCES = disjoint1.cc nnc_disjoint1_CXXFLAGS = $(DERIVED_CXXFLAGS) +nnc_dropsomenonintegerpoints1_SOURCES = dropsomenonintegerpoints1.cc +nnc_dropsomenonintegerpoints1_CXXFLAGS = $(DERIVED_CXXFLAGS) + nnc_empty1_SOURCES = empty1.cc nnc_empty1_CXXFLAGS = $(DERIVED_CXXFLAGS) diff --git a/tests/Polyhedron/dropsomenonintegerpoints1.cc b/tests/Polyhedron/dropsomenonintegerpoints1.cc new file mode 100644 index 0000000..c02efde --- /dev/null +++ b/tests/Polyhedron/dropsomenonintegerpoints1.cc @@ -0,0 +1,174 @@ +/* Test Polyhedron::drop_some_non_integer_points(). + Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +bool +test01() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.add_constraint(2*A >= 1); + ph.add_constraint(2*B >= -1); + ph.add_constraint(6*A - 3*B >= 7); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + C_Polyhedron known_result(2); + known_result.add_constraint(A >= 1); + known_result.add_constraint(B >= 0); + known_result.add_constraint(2*A - B >= 3); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test02() { + C_Polyhedron ph1; + C_Polyhedron ph2(2, EMPTY); + + print_constraints(ph1, "*** ph1 ***"); + print_constraints(ph2, "*** ph2 ***"); + + C_Polyhedron known_result1(0, EMPTY); + C_Polyhedron known_result2(ph2); + + ph1.drop_some_non_integer_points(); + ph2.drop_some_non_integer_points(); + + bool ok = (ph1 == known_result1 && ph2 == known_result2); + + print_constraints(ph1, "*** after ph1.drop_some_non_integer_points() ***"); + print_constraints(ph2, "*** after ph2.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test03() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.add_constraint(A - B == 0); + ph.add_constraint(A >= 0); + + C_Polyhedron known_result(ph); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test04() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.generators(); + ph.add_constraint(A >= 0); + ph.add_constraint(A == B); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + C_Polyhedron known_result(2); + known_result.add_constraint(A >= 0); + known_result.add_constraint(A == B); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test05() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2, EMPTY); + ph.add_generator(point(A+B, 2)); + ph.add_generator(line(B)); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + C_Polyhedron known_result(2, EMPTY); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test06() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.add_constraint(2*A <= 1); + ph.add_constraint(2*B <= -1); + ph.add_constraint(6*A - 3*B <= 7); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + bool ok = true; //(ph1 == ph2); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); +END_MAIN diff --git a/tests/Polyhedron/dropsomenonintegerpoints2.cc b/tests/Polyhedron/dropsomenonintegerpoints2.cc new file mode 100644 index 0000000..a3a6606 --- /dev/null +++ b/tests/Polyhedron/dropsomenonintegerpoints2.cc @@ -0,0 +1,160 @@ +/* Test Polyhedron::drop_some_non_integer_points(). + Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +bool +test01() { + Variable A(0); + Variable B(1); + + NNC_Polyhedron ph1(2); + ph1.add_constraint(A > 1); + ph1.add_constraint(A - B > 0); + Generator_System gs; + gs.insert(point(2*A)); + gs.insert(closure_point(A + B)); + gs.insert(ray(-B)); + gs.insert(ray(A + B)); + NNC_Polyhedron ph2(gs); + + print_constraints(ph1, "*** ph1 ***"); + print_generators(ph2, "*** ph2 ***"); + + ph1.drop_some_non_integer_points(); + ph2.drop_some_non_integer_points(); + + bool ok = (ph1 == ph2); + + print_constraints(ph1, "*** after ph1.drop_some_non_integer_points() ***"); + print_generators(ph2, "*** after ph2.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test02() { + NNC_Polyhedron ph1; + NNC_Polyhedron ph2(2, EMPTY); + + print_constraints(ph1, "*** ph1 ***"); + print_constraints(ph2, "*** ph2 ***"); + + NNC_Polyhedron known_result1(0, EMPTY); + NNC_Polyhedron known_result2(ph2); + + ph1.drop_some_non_integer_points(); + ph2.drop_some_non_integer_points(); + + bool ok = (ph1 == known_result1 && ph2 == known_result2); + + print_constraints(ph1, "*** after ph1.drop_some_non_integer_points() ***"); + print_constraints(ph2, "*** after ph2.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test03() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.add_constraint(A - B == 0); + ph.add_constraint(A >= 0); + + C_Polyhedron known_result(ph); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test04() { + Variable A(0); + Variable B(1); + + NNC_Polyhedron ph(2); + ph.generators(); + ph.add_constraint(A > 0); + ph.add_constraint(A == B); + + print_constraints(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + NNC_Polyhedron known_result(2); + known_result.add_constraint(A >= 1); + known_result.add_constraint(A == B); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +bool +test05() { + Variable A(0); + Variable B(1); + + NNC_Polyhedron ph(2, EMPTY); + ph.add_generator(point(A)); + ph.constraints(); + ph.add_generator(closure_point()); + ph.add_generator(ray(A)); + ph.add_generator(ray(B)); + + print_generators(ph, "*** ph ***"); + + ph.drop_some_non_integer_points(); + + NNC_Polyhedron known_result(2); + known_result.add_constraint(A >= 1); + known_result.add_constraint(B >= 0); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** after ph.drop_some_non_integer_points() ***"); + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); +END_MAIN

1 0

[GIT] ppl/ppl(master): Fixed a couple of bugs in drop_some_non_integer_points().
by Roberto Bagnara 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: 96e0624a5897a8c9ed7d4f9eb2f1f85d4132aef6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=96e0624a5897… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Mar 25 07:06:19 2010 +0400 Fixed a couple of bugs in drop_some_non_integer_points(). --- src/Polyhedron_nonpublic.cc | 30 +++++++++++++++++++----------- 1 files changed, 19 insertions(+), 11 deletions(-) diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index b48c610..20049a6 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -2087,8 +2087,10 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, // A zero-dimensional, universe polyhedron has, by convention, an // integer point. - if (space_dim == 0) + if (space_dim == 0) { set_empty(); + return; + } // The constraints (possibly with pending rows) are required. if (has_pending_generators()) { @@ -2105,8 +2107,17 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, else update_constraints(); } + // For NNC polyhedra we need to process any pending constraints. + if (!is_necessarily_closed() && has_pending_constraints()) { + if (complexity != ANY_COMPLEXITY) + return; + else if (!process_pending_constraints()) + // We just discovered the polyhedron is empty. + return; + } PPL_ASSERT(!has_pending_generators() && constraints_are_up_to_date()); + PPL_ASSERT(is_necessarily_closed() || !has_pending_constraints()); bool changed = false; const dimension_type eps_index = space_dim + 1; @@ -2126,9 +2137,12 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, if (!is_necessarily_closed()) { // Transform all strict inequalities into non-strict ones, // with the inhomogeneous term incremented by 1. - if (c[eps_index] < 0 && !c.is_tautological()) { + if (c[eps_index] < 0) { c[eps_index] = 0; --c[0]; + // Enforce normalization. + // FIXME: is this really necessary? + c.normalize(); changed = true; } } @@ -2146,18 +2160,18 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, } } // We reach this point only if all the coefficients were zero. - goto maybe_normalize; + goto next_constraint; compute_gcd: if (gcd == 1) - goto maybe_normalize; + goto next_constraint; while (i > 1) { const Coefficient& c_i = c[--i]; if (c_i != 0) { // See the comment in Row::normalize(). gcd_assign(gcd, c_i, gcd); if (gcd == 1) - goto maybe_normalize; + goto next_constraint; } } PPL_ASSERT(gcd != 1); @@ -2182,12 +2196,6 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, changed = true; } - maybe_normalize: - if (changed) - // Enforce normalization. - //c.normalize(); - ; - next_constraint: ; }

1 0

[GIT] ppl/ppl(master): Fixed a bug in drop_some_non_integer_points().
by Roberto Bagnara 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: master Commit: 42af7d51365d12593274c61ac4121f634cd803a3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=42af7d51365d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 24 22:07:29 2010 +0400 Fixed a bug in drop_some_non_integer_points(). --- src/Polyhedron_nonpublic.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index a54c639..b48c610 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -2128,7 +2128,7 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, // with the inhomogeneous term incremented by 1. if (c[eps_index] < 0 && !c.is_tautological()) { c[eps_index] = 0; - ++c[0]; + --c[0]; changed = true; } }

1 0

[GIT] ppl/ppl(master): Enable *drop_some_non_integer_points* for Polyhedron ; disable it for Pointset_Powerset.
by Roberto Bagnara 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: master Commit: b319599bb6747044e2555a9468f676f6e5aa50d5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b319599bb674… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 24 21:39:53 2010 +0400 Enable *drop_some_non_integer_points* for Polyhedron; disable it for Pointset_Powerset. --- ...erface_generator_common_procedure_generators.m4 | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/interfaces/ppl_interface_generator_common_procedure_generators.m4 b/interfaces/ppl_interface_generator_common_procedure_generators.m4 index 81fa8ad..48cde25 100644 --- a/interfaces/ppl_interface_generator_common_procedure_generators.m4 +++ b/interfaces/ppl_interface_generator_common_procedure_generators.m4 @@ -90,8 +90,8 @@ ppl_@CLASS@_remove_higher_space_dimensions/2 *nofail +all, ppl_@CLASS@_expand_space_dimension/3 *nofail +all, ppl_@CLASS@_fold_space_dimensions/3 +all, ppl_@CLASS@_map_space_dimensions/2 +all, -ppl_@CLASS@_drop_some_non_integer_points/2 +simple -polyhedron, -ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple -polyhedron, +ppl_@CLASS@_drop_some_non_integer_points/2 +simple -pointset_powerset, +ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple -pointset_powerset, ppl_@CLASS@_ascii_dump/1 +all, ppl_@CLASS@_@MEMBYTES@/2 +all, dnl

1 0

[GIT] ppl/ppl(master): Indentation corrected.
by Roberto Bagnara 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: master Commit: e1cb708053900953d6a0fea5890237f52321408f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e1cb70805390… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 24 21:38:59 2010 +0400 Indentation corrected. --- src/Octagonal_Shape.defs.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index e47383c..4f28fe1 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1491,7 +1491,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

1 0

[GIT] ppl/ppl(master): Drafted the implementation of methods drop_some_non_integer_points().
by Roberto Bagnara 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: master Commit: ce7681699c3e6056ce77eb9492ae8a051bb00dc3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ce7681699c3e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 24 21:37:52 2010 +0400 Drafted the implementation of methods drop_some_non_integer_points(). --- src/Polyhedron.defs.hh | 18 ++++++ src/Polyhedron.inlines.hh | 13 ++++ src/Polyhedron_nonpublic.cc | 135 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 166 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 3a1f563..0a3c86b 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2698,6 +2698,24 @@ protected: //@} // Exception Throwers #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + /*! \brief + Possibly tightens \p *this by dropping some points with non-integer + coordinates for the space dimensions corresponding to \p *pvars. + + \param pvars + When nonzero, points with non-integer coordinates for the + variables/space-dimensions contained in \p *pvars can be discarded. + + \param complexity + The maximal complexity of any algorithms used. + + \note + Currently there is no optimality guarantee, not even if + \p complexity is <CODE>ANY_COMPLEXITY</CODE>. + */ + void drop_some_non_integer_points(const Variables_Set* pvars, + Complexity_Class complexity); + //! Helper function that overapproximates an interval linear form. /*! \param lf diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh index 8f3aeef..2909057 100644 --- a/src/Polyhedron.inlines.hh +++ b/src/Polyhedron.inlines.hh @@ -431,6 +431,19 @@ Polyhedron::strictly_contains(const Polyhedron& y) const { return x.contains(y) && !y.contains(x); } +inline void +Polyhedron::drop_some_non_integer_points(Complexity_Class complexity) { + drop_some_non_integer_points(static_cast<const Variables_Set*>(0), + complexity); +} + +inline void +Polyhedron::drop_some_non_integer_points(const Variables_Set& vars, + Complexity_Class complexity) { + drop_some_non_integer_points(&vars, complexity); +} + + namespace Interfaces { inline bool diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 1cd9fb2..a54c639 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -2075,6 +2075,141 @@ PPL::Polyhedron::BFT00_poly_hull_assign_if_exact(const Polyhedron& y) { } void +PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, + Complexity_Class complexity) { + // There is nothing to do for an empty set of variables. + if (pvars != 0 && pvars->empty()) + return; + + // Any empty polyhedron does not contain integer points. + if (marked_empty()) + return; + + // A zero-dimensional, universe polyhedron has, by convention, an + // integer point. + if (space_dim == 0) + set_empty(); + + // The constraints (possibly with pending rows) are required. + if (has_pending_generators()) { + // Processing of pending generators is exponential in the worst case. + if (complexity != ANY_COMPLEXITY) + return; + else + process_pending_generators(); + } + if (!constraints_are_up_to_date()) { + // Constraints update is exponential in the worst case. + if (complexity != ANY_COMPLEXITY) + return; + else + update_constraints(); + } + + PPL_ASSERT(!has_pending_generators() && constraints_are_up_to_date()); + + bool changed = false; + const dimension_type eps_index = space_dim + 1; + PPL_DIRTY_TEMP_COEFFICIENT(gcd); + + for (dimension_type j = con_sys.num_rows(); j-- > 0; ) { + Constraint& c = con_sys[j]; + if (c.is_tautological()) + goto next_constraint; + + if (pvars != 0) { + for (dimension_type i = space_dim; i-- > 0; ) + if (c[i+1] != 0 && pvars->find(i) == pvars->end()) + goto next_constraint; + } + + if (!is_necessarily_closed()) { + // Transform all strict inequalities into non-strict ones, + // with the inhomogeneous term incremented by 1. + if (c[eps_index] < 0 && !c.is_tautological()) { + c[eps_index] = 0; + ++c[0]; + changed = true; + } + } + + { + // Compute the GCD of all the homogeneous terms. + dimension_type i = space_dim+1; + while (i > 1) { + const Coefficient& c_i = c[--i]; + if (const int c_i_sign = sgn(c_i)) { + gcd = c_i; + if (c_i_sign < 0) + neg_assign(gcd); + goto compute_gcd; + } + } + // We reach this point only if all the coefficients were zero. + goto maybe_normalize; + + compute_gcd: + if (gcd == 1) + goto maybe_normalize; + while (i > 1) { + const Coefficient& c_i = c[--i]; + if (c_i != 0) { + // See the comment in Row::normalize(). + gcd_assign(gcd, c_i, gcd); + if (gcd == 1) + goto maybe_normalize; + } + } + PPL_ASSERT(gcd != 1); + PPL_ASSERT(c[0] % gcd != 0); + + // If we have an equality, the polyhedron becomes empty. + if (c.is_equality()) { + set_empty(); + return; + } + + // Divide the inhomogeneous coefficients by the GCD. + for (dimension_type i = space_dim+1; --i > 0; ) { + Coefficient& c_i = c[i]; + exact_div_assign(c_i, c_i, gcd); + } + Coefficient& c_0 = c[0]; + const int c_0_sign = sgn(c_0); + c_0 /= gcd; + if (c_0_sign < 0) + --c_0; + changed = true; + } + + maybe_normalize: + if (changed) + // Enforce normalization. + //c.normalize(); + ; + + next_constraint: + ; + } + + if (changed) { + if (!is_necessarily_closed()) { + con_sys.insert(Constraint::epsilon_leq_one()); + // FIXME: make sure that the following line really can stay here + // and should not be moved below the brace. + con_sys.set_sorted(false); + } + + // After changing the system of constraints, the generators + // are no longer up-to-date and the constraints are no longer + // minimized. + clear_generators_up_to_date(); + clear_constraints_minimized(); + } + PPL_ASSERT_HEAVY(OK()); +} + +void PPL::Polyhedron::throw_runtime_error(const char* method) const { std::ostringstream s; s << "PPL::";

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Std_Vector_Backend: add and use sequential_search_treshold.
by Marco Poletti 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: f3957a85aeb8243fe82d015780a17d7601126865 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f3957a85aeb8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Mar 24 16:24:38 2010 +0100 Unlimited_Sparse_Row_Std_Vector_Backend: add and use sequential_search_treshold. --- ...Unlimited_Sparse_Row_Std_Vector_Backend.defs.hh | 5 +++++ ...imited_Sparse_Row_Std_Vector_Backend.inlines.hh | 18 ++++++++++++++++++ 2 files changed, 23 insertions(+), 0 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Std_Vector_Backend.defs.hh b/src/Unlimited_Sparse_Row_Std_Vector_Backend.defs.hh index a479672..370feba 100644 --- a/src/Unlimited_Sparse_Row_Std_Vector_Backend.defs.hh +++ b/src/Unlimited_Sparse_Row_Std_Vector_Backend.defs.hh @@ -57,6 +57,11 @@ private: Unlimited_Sparse_Row_Std_Vector_Backend::key_value_comparison<Compare> key_value_compare(const Compare& comp); + //! This is the number of sequential comparisons after which binary search + //! is performed. This affects performance, but not correctness. + //! Some methods do one more comparison. + static const dimension_type sequential_search_treshold = 3; + public: //! Needed to satisfy the backend requirements. //! This is not a typedef to allow overloading of methods with both types. diff --git a/src/Unlimited_Sparse_Row_Std_Vector_Backend.inlines.hh b/src/Unlimited_Sparse_Row_Std_Vector_Backend.inlines.hh index c7c8776..02f3696 100644 --- a/src/Unlimited_Sparse_Row_Std_Vector_Backend.inlines.hh +++ b/src/Unlimited_Sparse_Row_Std_Vector_Backend.inlines.hh @@ -143,6 +143,12 @@ inline Unlimited_Sparse_Row_Std_Vector_Backend::dangerous_iterator Unlimited_Sparse_Row_Std_Vector_Backend ::lower_bound_dangerous(const dimension_type k, dangerous_iterator itr) { PPL_ASSERT(itr == end_dangerous() || (*itr).first <= k); + for (dimension_type i = sequential_search_treshold; i-- > 0; ) { + if (itr == end_dangerous() || (*itr).first >= k) + return itr; + ++itr; + } + // Now perform binary search. return std::lower_bound(itr, end_dangerous(), k, value_key_compare(std::less<dimension_type>())); } @@ -162,6 +168,12 @@ inline Unlimited_Sparse_Row_Std_Vector_Backend::iterator Unlimited_Sparse_Row_Std_Vector_Backend ::lower_bound(const dimension_type k, iterator itr) { PPL_ASSERT(itr == end() || (*itr).first <= k); + for (dimension_type i = sequential_search_treshold; i-- > 0; ) { + if (itr == end() || (*itr).first >= k) + return itr; + ++itr; + } + // Now perform binary search. return std::lower_bound(itr, end(), k, value_key_compare(std::less<dimension_type>())); } @@ -181,6 +193,12 @@ inline Unlimited_Sparse_Row_Std_Vector_Backend::const_iterator Unlimited_Sparse_Row_Std_Vector_Backend ::lower_bound(const dimension_type k, const_iterator itr1) const { PPL_ASSERT(itr1 == end() || (*itr1).first <= k); + for (dimension_type i = sequential_search_treshold; i-- > 0; ) { + if (itr1 == end() || (*itr1).first >= k) + return itr1; + ++itr1; + } + // Now perform binary search. return std::lower_bound(itr1, end(), k, value_key_compare(std::less<dimension_type>())); }

1 0

[GIT] ppl/ppl(master): Enable the interfaces procedures for Grid:: drop_some_non_integer_points().
by Patricia Hill 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: master Commit: 44bb8667fb1c413b18a1a504425200b246254f00 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=44bb8667fb1c… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Wed Mar 24 14:31:43 2010 +0000 Enable the interfaces procedures for Grid::drop_some_non_integer_points(). --- ...erface_generator_common_procedure_generators.m4 | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/interfaces/ppl_interface_generator_common_procedure_generators.m4 b/interfaces/ppl_interface_generator_common_procedure_generators.m4 index f83a37d..81fa8ad 100644 --- a/interfaces/ppl_interface_generator_common_procedure_generators.m4 +++ b/interfaces/ppl_interface_generator_common_procedure_generators.m4 @@ -90,8 +90,8 @@ ppl_@CLASS@_remove_higher_space_dimensions/2 *nofail +all, ppl_@CLASS@_expand_space_dimension/3 *nofail +all, ppl_@CLASS@_fold_space_dimensions/3 +all, ppl_@CLASS@_map_space_dimensions/2 +all, -ppl_@CLASS@_drop_some_non_integer_points/2 +simple -polyhedron -grid, -ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple -polyhedron -grid, +ppl_@CLASS@_drop_some_non_integer_points/2 +simple -polyhedron, +ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple -polyhedron, ppl_@CLASS@_ascii_dump/1 +all, ppl_@CLASS@_@MEMBYTES@/2 +all, dnl

1 0