Module: ppl/ppl Branch: master Commit: 0dc00fd021aa5e592ad9b00cb37b76a9b074580c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0dc00fd021aa5... Author: Roberto Bagnara <roberto.bagnara@bugseng.com> Date: Sat Sep 27 16:43:39 2014 +0200 Fixed a bug in Polyhedron::simplify_using_context_assign(). (Thanks to Didier Lime for the bug report.) --- src/Polyhedron_public.cc | 60 ++++++++++++++++++++++++----- tests/Polyhedron/Makefile.am | 4 +- tests/Polyhedron/simplifyusingcontext2.cc | 59 ++++++++++++++++++++++++++++ 3 files changed, 112 insertions(+), 11 deletions(-) diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index 21f88ec..ba604d8 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -2255,9 +2255,9 @@ PPL::Polyhedron::simplify_using_context_assign(const Polyhedron& y) { z.add_recycled_constraints(tmp_cs); } if (!z.minimize()) { - // The objective function is the default, zero. - // We do not care about minimization or maximization, since - // we are only interested in satisfiability. + // For necessarily closed polyhedra, the objective function is + // the default, zero. Moreover, the default maximization mode is + // OK, since we are only interested in satisfiability. MIP_Problem lp; if (x.is_necessarily_closed()) { lp.add_space_dimensions_and_embed(x.space_dim); @@ -2278,6 +2278,11 @@ PPL::Polyhedron::simplify_using_context_assign(const Polyhedron& y) { const_cast<Constraint_System&>(y_cs).mark_as_not_necessarily_closed(); throw; } + // For not necessarily closed polyhedra, we maximize the + // epsilon dimension as we want to rule out the possibility + // that all solutions have epsilon = 0. We are in this case + // if and only if the maximal value for epsilon is 0. + lp.set_objective_function(Variable(x.space_dim)); } // We apply the following heuristics here: constraints of `x' that // are not made redundant by `y' are added to `lp' depending on @@ -2387,15 +2392,50 @@ PPL::Polyhedron::simplify_using_context_assign(const Polyhedron& y) { ++j) { const Constraint& c = x_cs[j->constraint_index]; result_cs.insert(c); - lp.add_constraint(c); + if (x.is_necessarily_closed()) { + lp.add_constraint(c); + } + else { + // KLUDGE: temporarily mark `c' as if it was necessarily + // closed, so that we can interpret the epsilon dimension as a + // standard dimension. Be careful to reset the topology of `c' + // also on exceptional execution paths. + const_cast<Constraint&>(c).mark_as_necessarily_closed(); + try { + lp.add_constraint(c); + const_cast<Constraint&>(c).mark_as_not_necessarily_closed(); + } + catch (...) { + const_cast<Constraint&>(c).mark_as_not_necessarily_closed(); + throw; + } + } const MIP_Problem_Status status = lp.solve(); - if (status == UNFEASIBLE_MIP_PROBLEM) { - Polyhedron result_ph(x.topology(), x.space_dim, UNIVERSE); - result_ph.add_constraints(result_cs); - swap(x, result_ph); - PPL_ASSERT_HEAVY(x.OK()); - return false; + switch (status) { + case UNFEASIBLE_MIP_PROBLEM: + break; + case OPTIMIZED_MIP_PROBLEM: + if (x.is_necessarily_closed()) { + continue; + } + else { + Coefficient num; + Coefficient den; + lp.optimal_value(num, den); + if (num != 0) { + continue; + } + } + break; + default: + PPL_UNREACHABLE; + break; } + Polyhedron result_ph(x.topology(), x.space_dim, UNIVERSE); + result_ph.add_constraints(result_cs); + swap(x, result_ph); + PPL_ASSERT_HEAVY(x.OK()); + return false; } // Cannot exit from here. PPL_UNREACHABLE; diff --git a/tests/Polyhedron/Makefile.am b/tests/Polyhedron/Makefile.am index 828b2e5..63bc462 100644 --- a/tests/Polyhedron/Makefile.am +++ b/tests/Polyhedron/Makefile.am @@ -129,7 +129,7 @@ refinewithconstraint1 \ refinewithconstraints1 \ relations1 relations2 relations3 \ removespacedims1 removespacedims2 \ -simplifyusingcontext1 \ +simplifyusingcontext1 simplifyusingcontext2 \ smm1 \ sparserow1 \ termination1 termination2 \ @@ -341,6 +341,8 @@ intersection1_SOURCES = intersection1.cc simplifyusingcontext1_SOURCES = simplifyusingcontext1.cc +simplifyusingcontext2_SOURCES = simplifyusingcontext2.cc + limitedbhrz03extrapolation1_SOURCES = limitedbhrz03extrapolation1.cc limitedh79extrapolation1_SOURCES = limitedh79extrapolation1.cc diff --git a/tests/Polyhedron/simplifyusingcontext2.cc b/tests/Polyhedron/simplifyusingcontext2.cc new file mode 100644 index 0000000..98ac4dc --- /dev/null +++ b/tests/Polyhedron/simplifyusingcontext2.cc @@ -0,0 +1,59 @@ +/* Test Polyhedron::simplify_using_context_assign() with NNC polyhedra. + Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> + Copyright (C) 2010-2014 BUGSENG srl (http://bugseng.com) + +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://bugseng.com/products/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +bool +test01() { + Variable A(0); + + NNC_Polyhedron ph1(1); + ph1.add_constraint(0 < A); + + NNC_Polyhedron ph2(1); + ph2.add_constraint(A <= 0); + + NNC_Polyhedron computed_result = ph1; + computed_result.simplify_using_context_assign(ph2); + + NNC_Polyhedron known_result(1); + known_result.add_constraint(0 < A); + + bool ok = (computed_result == known_result); + + print_constraints(ph1, "*** ph1 ***"); + print_constraints(ph2, "*** ph2 ***"); + print_constraints(computed_result, + "*** ph1.simplify_using_context_assign(ph2) ***"); + print_constraints(known_result, "*** known_result ***"); + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); +END_MAIN