[PPL-devel] [GIT] ppl/ppl(master): Fixed a bug in Polyhedron:: simplify_using_context_assign().
Roberto Bagnara
roberto.bagnara at bugseng.com
Sat Sep 27 16:46:05 CEST 2014
Module: ppl/ppl
Branch: master
Commit: 0dc00fd021aa5e592ad9b00cb37b76a9b074580c
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0dc00fd021aa5e592ad9b00cb37b76a9b074580c
Author: Roberto Bagnara <roberto.bagnara at 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 at 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
More information about the PPL-devel
mailing list