- PPL-devel - BUGSENG Mailman

[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

[GIT] ppl/ppl(master): New commits
by Roberto Bagnara 21 Aug '14

21 Aug '14

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dbc2d08da5e9… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jul 28 21:45:24 2014 +0200 Use a monotonic indentation style. Fixes violations detected by ECLAIR checker B.MONOINDENT. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=270d1d0c5e09… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Jul 27 09:29:04 2014 +0200 Comments should never be used for "commenting out" code. Fixes violations of rule EP1.17 detected by ECLAIR. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b1f5eb2caa2b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Jul 2 16:58:24 2014 +0200 Keep source lines to a length of 120 characters or less. Fixes violations of rule LP1.41 detected by ECLAIR. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=10368f7e6fda… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jun 30 18:00:31 2014 +0200 Avoid tabs. Fixes violations of rule UCRP1.RS1 detected by ECLAIR. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7a2ba6b6089a… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jun 30 14:33:02 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-4-1 detected by ECLAIR. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fe5b8f435d43… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Mon Jun 30 12:00:03 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-4-1 detected by ECLAIR. Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=36d6c9817821… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Mon Jun 30 02:32:03 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-3-1 detected by ECLAIR. Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a4125de9f40f… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Wed Jun 25 09:15:41 2014 +0200 Fixed permissions. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cf56af994e36… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Sat Jun 21 18:44:47 2014 +0200 Fixed brace position. Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d652b0b9d20… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Jun 24 12:53:52 2014 +0200 Deleted trailing whitespace. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d2c305abdf9b… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Tue Jun 24 08:48:41 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-4-1 detected by ECLAIR. Signed-off-by: Roberto Bagnara <bagnara(a)cs.unipr.it> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bd70cc6e44ca… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Sat Jun 21 12:17:47 2014 +0200 Brace position fixed. Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2c040ae00435… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 20 11:27:20 2014 +0200 Typo fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=178fed3200d9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 20 11:18:25 2014 +0200 Permissions fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b8be0e6326fe… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 20 11:15:47 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-4-1 detected by ECLAIR. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=15c8505625e4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 20 11:10:24 2014 +0200 Deleted trailing whitespace. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a62a3aa3cec4… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Thu Jun 19 18:33:33 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-4-1 detected by ECLAIR. Signed-off-by: Roberto Bagnara <bagnara(a)cs.unipr.it> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b66d45423488… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Wed Jun 18 21:56:56 2014 +0200 Deleted trailing whitespace. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=00014551b6ab… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Mon Jun 16 09:02:53 2014 +0200 Readded newlines erased by mistake. Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8d637a0f6e96… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jun 14 06:02:43 2014 +0200 Removed trailing whitespace. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5d0fb6173407… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Sat Jun 14 02:24:01 2014 +0200 Added missing braces. Fixes violations of rule MP1.6-3-1 detected by ECLAIR. Signed-off-by: Roberto Bagnara <bagnara(a)cs.unipr.it> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1e46c22014f2… Merge: a483b63739b1dd78bda63892043873e0205c2ab3 fe759bb940ffa3083ec6eca0c8221d388bd2bb64 Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Jun 14 05:57:00 2014 +0200 Merge branch 'master' into compliance. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a483b63739b1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 12 13:49:18 2014 +0200 Missing brace added. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2ea46ae16ed0… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Thu Jun 12 12:57:37 2014 +0200 Added missing braces. Fixes violations of rules MP1.6-3-1 and MP1.6-4-1 detected by ECLAIR. Signed-off-by: Roberto Bagnara <bagnara(a)cs.unipr.it> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5992421fdd82… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Mon Jun 9 15:44:24 2014 +0200 Do not declare more than one variable per declaration. Fixes violations of rule CP1.DCL04 detected by ECLAIR. Signed-off-by: Roberto Bagnara <bagnara(a)cs.unipr.it> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=333a57b84a18… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Mon Jun 9 12:00:23 2014 +0200 Previous commit fixed. Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com> URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f3dc0ba64a44… Author: Patrik Pomelli <patrik.pomelli(a)bugseng.com> Date: Mon Jun 9 10:25:27 2014 +0200 Added missing braces. Fixes violations of rules MP1.6-3-1 and MP1.6-4-1 detected by ECLAIR Signed-off-by: Roberto Bagnara <roberto.bagnara(a)bugseng.com>

1 0

Failure building ppl under Cygwin 64 with a mingw target.
by Keith Clifford 01 Aug '14

01 Aug '14

Hi, I'm building a set of cross compilers to run under mingw and I got the error below. The set of packages and their versions to do the build are: Build machine: CYGWIN_NT-6.1 1.7.31(0.272/5/3) 2014-07-21 18:40 x86_64 Cygwin Components: gmp-6.0.0a mpfr-3.1.2 mpc-1.0.2 isl-0.12.2 cloog-0.18.1 ppl-1.1 binutils-2.24 gcc-4.9.1 newlib-2.1.0 gdb-7.7 I've attached the script, mkx, that I use for building the cross compilers, the test-suit log, and the make and check logs. The individual test logs are empty. I'm set up to run so if you'd like me to try anything, let me know and I can give it a go. When the build failed it said let you know and I'm going to continue investigating. I'll let you know if I find anything. Regards, Keith Keith Clifford Cell: 250 888-4558 Tranaptic Signature

2 6

Custom Number Types
by Stefan Schupp 29 Jul '14

29 Jul '14

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 Hi, another (maybe silly) question: How exactly to I extend the PPL (if possible) to my own number types? Is it sufficient to implement the checked_number policies? How do I add my type to the PPL afterwards? Best regards, 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 Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/ iQEcBAEBCgAGBQJT0RDDAAoJEFPSi5GyofDjH4sH/1gwYU2SQqVcV71bfcPYbFgl Y0HVGEqOB4rRu6UqYq2g9K/fVx/JFEyw+fo2qbJUKCdexvz8DyHje9NNtABdRZev 7a6EnUQtHbN97VPQPnTtujuslb925FVnzbt1rZoWTYJAPHlJfy71yC7wbNrg6I4V O3TFLz3T6ETH3Oi2NPx2efcZhRC1VXkc85FIFpKQ3gzjGeHiwymiddQICuX/Ufg0 hrHK/20/K1iqXJ4HuzWBTy43ZebtYWRSjOAAt7o78KOUBIz/StNHSXh0UFRkbu7y zX7ZF9wPbePd91DR6JrJR5SZbqYOx3+90IfZw0quB/5CtWe3OfuYng/mvHcWfuI= =lfHt -----END PGP SIGNATURE-----

2 4

[GIT] ppl/ppl(compliance): Use a monotonic indentation style.
by Roberto Bagnara 28 Jul '14

28 Jul '14

Module: ppl/ppl Branch: compliance Commit: dbc2d08da5e9062670d62e7ff37aff35e7cec601 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dbc2d08da5e9… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jul 28 21:45:24 2014 +0200 Use a monotonic indentation style. Fixes violations detected by ECLAIR checker B.MONOINDENT. --- src/Pending_List_templates.hh | 2 +- src/Polyhedron_minimize_templates.hh | 2 +- src/Polyhedron_simplify_templates.hh | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Pending_List_templates.hh b/src/Pending_List_templates.hh index 54f04f1..440b17e 100644 --- a/src/Pending_List_templates.hh +++ b/src/Pending_List_templates.hh @@ -42,7 +42,7 @@ Pending_List<Traits>::insert(const typename Traits::Threshold& deadline, position != active_list_end && Traits::less_than(position->deadline(), deadline); ++position) { - } + } iterator pending_element_p; // Only allocate a new element if the free list is empty. if (free_list.empty()) { diff --git a/src/Polyhedron_minimize_templates.hh b/src/Polyhedron_minimize_templates.hh index 40d1d53..d9e4e78 100644 --- a/src/Polyhedron_minimize_templates.hh +++ b/src/Polyhedron_minimize_templates.hh @@ -414,7 +414,7 @@ Polyhedron::add_and_minimize(const bool con_to_gen, if (dest[first_point].expr.get(Variable(dest.space_dimension())) > 0) { break; } - } + } } if (first_point == dest_num_rows) { diff --git a/src/Polyhedron_simplify_templates.hh b/src/Polyhedron_simplify_templates.hh index c2da7bc..71d4ffb 100644 --- a/src/Polyhedron_simplify_templates.hh +++ b/src/Polyhedron_simplify_templates.hh @@ -290,8 +290,8 @@ Polyhedron::simplify(Linear_System1& sys, Bit_Matrix& sat) { swap(sat[j], sat[num_rows]); swap(num_saturators[j], num_saturators[num_rows]); } - } - else { + } + else { // If we reach this point then we know that `sat[i]' does // not contain (and is different from) `sat[j]', so that // `sys[i]' is not made redundant by inequality `sys[j]'.

1 0

[GIT] ppl/ppl(compliance): Comments should never be used for " commenting out" code.
by Roberto Bagnara 27 Jul '14

27 Jul '14

Module: ppl/ppl Branch: compliance Commit: 270d1d0c5e09996d077b52a21a85bd6c7ca09a07 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=270d1d0c5e09… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Jul 27 09:29:04 2014 +0200 Comments should never be used for "commenting out" code. Fixes violations of rule EP1.17 detected by ECLAIR. --- src/Bit_Row.cc | 18 ++++++++++-------- src/CO_Tree_inlines.hh | 14 ++++++++------ src/PIP_Tree.cc | 8 +++++--- src/Polyhedron_nonpublic.cc | 2 -- src/iterator_to_const_defs.hh | 1 - 5 files changed, 23 insertions(+), 20 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index c8e5e87..e17d475 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -47,14 +47,16 @@ unsigned long PPL::Bit_Row::next(unsigned long position) const { ++position; - // The alternative implementation using the mpz_scan1() function - // of GMP was measured to be slower that ours. Here it is, in - // case mpz_scan1() is improved. - // - // <CODE> - // unsigned long r = mpz_scan1(vec, position); - // return (r == C_Integer<unsigned long>::max) ? -1 : r; - // </CODE> + /* + The alternative implementation using the mpz_scan1() function + of GMP was measured to be slower that ours. Here it is, in + case mpz_scan1() is improved: + + <CODE> + unsigned long r = mpz_scan1(vec, position); + return (r == C_Integer<unsigned long>::max) ? -1 : r; + </CODE> + */ const unsigned long uli = position / PPL_BITS_PER_GMP_LIMB; mp_size_t li = static_cast<mp_size_t>(uli); diff --git a/src/CO_Tree_inlines.hh b/src/CO_Tree_inlines.hh index f94f81e..1209bf5 100644 --- a/src/CO_Tree_inlines.hh +++ b/src/CO_Tree_inlines.hh @@ -343,12 +343,14 @@ CO_Tree::refresh_cached_iterators() { inline void CO_Tree::move_data_element(data_type& to, data_type& from) { - // The following code is equivalent (but slower): - // - // <CODE> - // new (&to) data_type(from); - // from.~data_type(); - // </CODE> + /* + The following code is equivalent (but slower): + + <CODE> + new (&to) data_type(from); + from.~data_type(); + </CODE> + */ std::memcpy(&to, &from, sizeof(data_type)); } diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index dae15f1..fe2318b 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -28,9 +28,11 @@ site: http://bugseng.com/products/ppl/ . */ #include <memory> #include <map> -// #define NOISY_PIP_TREE_STRUCTURE 1 -// #define NOISY_PIP 1 -// #define VERY_NOISY_PIP 1 +#if 0 +#define NOISY_PIP_TREE_STRUCTURE 1 +#define NOISY_PIP 1 +#define VERY_NOISY_PIP 1 +#endif namespace Parma_Polyhedra_Library { diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 4743e3c..70addd4 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -2453,8 +2453,6 @@ PPL::Polyhedron::positive_time_elapse_assign_impl(const Polyhedron& y) { } PPL_ASSERT(gs->OK()); - //gs->ascii_dump(std::cout); - //IO_Operators::operator<<(std::cout, *gs); const dimension_type gs_num_rows = gs->num_rows(); diff --git a/src/iterator_to_const_defs.hh b/src/iterator_to_const_defs.hh index 9a6c29e..0e011fc 100644 --- a/src/iterator_to_const_defs.hh +++ b/src/iterator_to_const_defs.hh @@ -26,7 +26,6 @@ site: http://bugseng.com/products/ppl/ . */ #include "iterator_to_const_types.hh" #include "Powerset_types.hh" -//#include "Ask_Tell_types.hh" #include <iterator> #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

1 0