September 2014 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed.
by Roberto Bagnara 27 Sep '14

27 Sep '14

Module: ppl/ppl Branch: master Commit: 0b93034882241b67a9074014ead300ecd49b5f26 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0b9303488224… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Sep 27 17:04:09 2014 +0200 Fixed. --- doc/Makefile.am | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/Makefile.am b/doc/Makefile.am index 5ae0ff5..73a745d 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -747,7 +747,7 @@ uninstall-txt if BUILD_DOCUMENTATION -CONTINUE_IF_NO_DOC = true +CONTINUE_IF_NO_DOC = false else !BUILD_DOCUMENTATION

1 0

[GIT] ppl/ppl(master): Fixed a bug in Polyhedron:: simplify_using_context_assign().
by Roberto Bagnara 27 Sep '14

27 Sep '14

Module: ppl/ppl Branch: master Commit: 0dc00fd021aa5e592ad9b00cb37b76a9b074580c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0dc00fd021aa… Author: Roberto Bagnara <roberto.bagnara(a)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(a)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

1 0

PPL for linear expression comparison and constraint derivation
by Aleksandra Jovanovic 22 Sep '14

22 Sep '14

Dear Sir/Madam, I am interested in starting to use Parma Polyhedra library for my research. I do have a specific problem and I would like to check whether PPL could be used for solving. I need to compare two linear expression and derive the necessary constraints on the variables such that one of them is minimum/maximum. For example, what should be the relation between x, a and b such that 3x+a+5b is smaller than x+5a+3b (just an example I haven’t paid attention to the actually numbers). Are there functions in PPL that I could use to solve this? Thank you in advance for your time, Aleksandra Jovanovic Aleksandra Jovanovic Research Assistant Department of Computer Science University of Oxford Wolfson Building, Parks Road Oxford, OX1 3QD

2 2

Convex Hull
by Stefan Schupp 19 Sep '14

19 Sep '14

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 Hello, a short question: What is the method to use when computing the convex hull of a C_Polyhedron? Currently I try minimized_generators. Best regard, Stefan - -- Stefan Schupp M.Sc. RWTH Aachen University Computer Science Department, Informatik 2 D-52056 Aachen, Germany http://www-i2.informatik.rwth-aachen.de/i2/schupp/ Tel.: +49 241 80 21243 -----BEGIN PGP SIGNATURE----- Version: GnuPG/MacGPG2 v2.0.22 (Darwin) Comment: GPGTools - https://gpgtools.org iQEcBAEBCgAGBQJUGvyCAAoJEFPSi5GyofDjhm8H/1hs1zqXzBnKohwlnwhM3ErV I17/lrNrkYAcvPUvXHMR1DdVYmN/80vad1nuwJkzNQe/luB7iO4jh0HsXSPPjh4j CDYSkzoP6P0Iu/13BSu3VLu8tnENoETN/yDsrIVNdKhk9JWCyu6mruUVP9Io7g8K PA3aqlXFikPX2Bekm4PX2Kaz49ojr7zQc+BNCDGijFK/r85PX1zeBflotk4xQ3Zp rQU5T1g0V1W7cquCW4r+dgar74YRf2zULywUN9NtSk0G2pfM3wOuOaQP9f6TyJJ8 jrxAooPGfLYdkCzN49DZU6Z7k3stP1I7vaPyeIi/SVRUKII+6mNn0mfM7+zeAPA= =8b3u -----END PGP SIGNATURE-----

2 3

phaver-ppl issue
by Vikas Jaiman 13 Sep '14

13 Sep '14

Hello, I was trying to compile phaver source code but I am getting following error after compilation. Can you help me out from this. convex_clock_val_set.cpp: In member function ‘void convex_clock_val_set::swap(convex_clock_val_set&)’: convex_clock_val_set.cpp:365:3: error: ‘m_swap’ is not a member of ‘Parma_Polyhedra_Library:: Polyhedron’ convex_clock_val_set.cpp: In member function ‘void convex_clock_val_set::minimize_memory()’: convex_clock_val_set.cpp:1185:4: error: ‘m_swap’ is not a member of ‘Parma_Polyhedra_Library::NNC_Polyhedron’ make: *** [convex_clock_val_set.o] Error 1 Thanks, Vikas ======================================================== Vikas Jaiman Research Scholar, Laboratoire VERIMAG, Centre Equation | 2, Avenue de Vignate | 38610 GIERES, Grenoble, FRANCE. Tel. +33 7 54 04 60 93 | Fax. +33 4 56 52 03 44 ========================================================

2 1

Re: [PPL-devel] phaver PPL library issue
by Roberto Bagnara 11 Sep '14

11 Sep '14

On 11/09/2014 13:57, Vikas Jaiman wrote: > Dear Prof. Roberto, > > I am a PhD student at Verimag. I was trying to compile phaver source code but I am getting following error after compilation. Can you help me out from this. > > convex_clock_val_set.cpp: In member function ‘void convex_clock_val_set::swap(convex_clock_val_set&)’: > convex_clock_val_set.cpp:365:3: error: ‘m_swap’ is not a member of ‘Parma_Polyhedra_Library::Polyhedron’ > convex_clock_val_set.cpp: In member function ‘void convex_clock_val_set::minimize_memory()’: > convex_clock_val_set.cpp:1185:4: error: ‘m_swap’ is not a member of ‘Parma_Polyhedra_Library::NNC_Polyhedron’ > make: *** [convex_clock_val_set.o] Error 1 > > Thanks, > Vikas > ======================================================== > Vikas Jaiman > Research Scholar, > Laboratoire VERIMAG, > Centre Equation | 2, Avenue de Vignate | 38610 GIERES, > Grenoble, FRANCE. > Tel. +33 7 54 04 60 93 | Fax. +33 4 56 52 03 44 > ======================================================== Dear Vikas, this is actually an issue with Phaver, not the PPL. It was already discussed on the PPL mailing list recently. Please consult the archives of the list and write to ppl-devel(a)cs.unipr.it if you have further doubts. Kind regards, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com

2 1