November 2015 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(devel): Mention fixed bug.
by Enea Zaffanella 19 Nov '15

19 Nov '15

Module: ppl/ppl Branch: devel Commit: 673343a9e22e99f6ecb9e1bdb2c733369047d9fc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=673343a9e22e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:44:41 2015 +0100 Mention fixed bug. --- NEWS | 7 +++++++ 1 files changed, 7 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index ea2858f..e4f862f 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,13 @@ o TO BE WRITTEN Bugfixes ======== +o Fixed a bug in the implementation of methods + Pointset_Powerset<PSET>::relation_with(const Constraint&) const; + and + Pointset_Powerset<PSET>::relation_with(const Congruence&) const; + whereby the computed result for relations strictly_intersects() + and saturates() could have been wrong. + o Fixed a bug in the implementation of dense rows. o Portability improved.

1 0

[GIT] ppl/ppl(devel): Provide a common, correct implementation for the methods
by Enea Zaffanella 19 Nov '15

19 Nov '15

Module: ppl/ppl Branch: devel Commit: e7cc925274945a76599d9601a24e001adfc534a1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e7cc92527494… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:36:02 2015 +0100 Provide a common, correct implementation for the methods Pointset_Powerset<PSET>::relation_with() working on Constraint and Congruence objects. --- src/Pointset_Powerset_defs.hh | 7 ++++ src/Pointset_Powerset_inlines.hh | 12 ++++++++ src/Pointset_Powerset_templates.hh | 56 +---------------------------------- 3 files changed, 21 insertions(+), 54 deletions(-) diff --git a/src/Pointset_Powerset_defs.hh b/src/Pointset_Powerset_defs.hh index 32615fb..6d4e321 100644 --- a/src/Pointset_Powerset_defs.hh +++ b/src/Pointset_Powerset_defs.hh @@ -1294,6 +1294,13 @@ private: typename Cert::Compare>& y_cert_ms) const; + /*! \brief + Template helper: common implementation for constraints + and congruences. + */ + template <typename Cons_or_Congr> + Poly_Con_Relation relation_with_aux(const Cons_or_Congr& c) const; + // FIXME: here it should be enough to befriend the template constructor // template <typename QH> // Pointset_Powerset(const Pointset_Powerset<QH>&), diff --git a/src/Pointset_Powerset_inlines.hh b/src/Pointset_Powerset_inlines.hh index 460999e..54b03da 100644 --- a/src/Pointset_Powerset_inlines.hh +++ b/src/Pointset_Powerset_inlines.hh @@ -233,6 +233,18 @@ Pointset_Powerset<PSET>::time_elapse_assign(const Pointset_Powerset& y) { } template <typename PSET> +inline Poly_Con_Relation +Pointset_Powerset<PSET>::relation_with(const Constraint& c) const { + return relation_with_aux(c); +} + +template <typename PSET> +inline Poly_Con_Relation +Pointset_Powerset<PSET>::relation_with(const Congruence& cg) const { + return relation_with_aux(cg); +} + +template <typename PSET> inline bool Pointset_Powerset<PSET> ::geometrically_covers(const Pointset_Powerset& y) const { diff --git a/src/Pointset_Powerset_templates.hh b/src/Pointset_Powerset_templates.hh index f2858c1..0f160a3 100644 --- a/src/Pointset_Powerset_templates.hh +++ b/src/Pointset_Powerset_templates.hh @@ -829,61 +829,9 @@ Pointset_Powerset<PSET>::strictly_contains(const Pointset_Powerset& y) const { } template <typename PSET> +template <typename Cons_or_Congr> Poly_Con_Relation -Pointset_Powerset<PSET>::relation_with(const Congruence& cg) const { - const Pointset_Powerset& x = *this; - - /* *this is included in cg if every disjunct is included in cg */ - bool is_included = true; - /* *this is disjoint with cg if every disjunct is disjoint with cg */ - bool is_disjoint = true; - /* *this strictly_intersects with cg if some disjunct strictly - intersects with cg */ - bool is_strictly_intersecting = false; - /* *this saturates cg if some disjunct saturates cg and - every disjunct is either disjoint from cg or saturates cg */ - bool saturates_once = false; - bool may_saturate = true; - for (Sequence_const_iterator si = x.sequence.begin(), - s_end = x.sequence.end(); si != s_end; ++si) { - Poly_Con_Relation relation_i = si->pointset().relation_with(cg); - if (!relation_i.implies(Poly_Con_Relation::is_included())) { - is_included = false; - } - if (!relation_i.implies(Poly_Con_Relation::is_disjoint())) { - is_disjoint = false; - } - if (relation_i.implies(Poly_Con_Relation::strictly_intersects())) { - is_strictly_intersecting = true; - } - if (relation_i.implies(Poly_Con_Relation::saturates())) { - saturates_once = true; - } - else if (!relation_i.implies(Poly_Con_Relation::is_disjoint())) { - may_saturate = false; - } - } - - Poly_Con_Relation result = Poly_Con_Relation::nothing(); - if (is_included) { - result = result && Poly_Con_Relation::is_included(); - } - if (is_disjoint) { - result = result && Poly_Con_Relation::is_disjoint(); - } - if (is_strictly_intersecting) { - result = result && Poly_Con_Relation::strictly_intersects(); - } - if (saturates_once && may_saturate) { - result = result && Poly_Con_Relation::saturates(); - } - - return result; -} - -template <typename PSET> -Poly_Con_Relation -Pointset_Powerset<PSET>::relation_with(const Constraint& c) const { +Pointset_Powerset<PSET>::relation_with_aux(const Cons_or_Congr& c) const { const Pointset_Powerset& x = *this; /* *this is included in c if every disjunct is included in c */

1 0

[GIT] ppl/ppl(devel): Corrected expected result for test02().
by Enea Zaffanella 19 Nov '15

19 Nov '15

Module: ppl/ppl Branch: devel Commit: bbf24268be1c2af275ee76f9eb790feb2a63cbc2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bbf24268be1c… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:34:48 2015 +0100 Corrected expected result for test02(). The test shows a bug in current implementation of method Pointset_Powerset<PSET>::relation_with(const Congruence& c) const --- tests/Powerset/relationwith1.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Powerset/relationwith1.cc b/tests/Powerset/relationwith1.cc index a76856c..0a730be 100644 --- a/tests/Powerset/relationwith1.cc +++ b/tests/Powerset/relationwith1.cc @@ -54,15 +54,15 @@ test02() { C_Polyhedron ph2(1); ph2.add_constraint(x == 2); - Pointset_Powerset<C_Polyhedron> ps(1, EMPTY); + Pointset_Powerset<C_Polyhedron> ps(1, EMPTY); ps.add_disjunct(ph1); ps.add_disjunct(ph2); Congruence cg((x %= 1) / 0); Poly_Con_Relation rel = ps.relation_with(cg); - Poly_Con_Relation known_rel = Poly_Con_Relation::saturates(); + Poly_Con_Relation known_rel = Poly_Con_Relation::strictly_intersects(); bool ok = (rel == known_rel);

1 0

[GIT] ppl/ppl(devel): Fixed bug in Pointset_Powerset::relation_with( const Constraint&) const.
by Enea Zaffanella 19 Nov '15

19 Nov '15

Module: ppl/ppl Branch: devel Commit: 93b1fe4d63f7ea0cb9d515f5beeea595ca4d96d6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=93b1fe4d63f7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:08:43 2015 +0100 Fixed bug in Pointset_Powerset::relation_with(const Constraint&) const. The bug was causing wrong results for relations strictly_intersects() and saturates() on some inputs. --- src/Pointset_Powerset_templates.hh | 37 +++++++++++++++++++++-------------- 1 files changed, 22 insertions(+), 15 deletions(-) diff --git a/src/Pointset_Powerset_templates.hh b/src/Pointset_Powerset_templates.hh index 393b96b..f2858c1 100644 --- a/src/Pointset_Powerset_templates.hh +++ b/src/Pointset_Powerset_templates.hh @@ -890,30 +890,37 @@ Pointset_Powerset<PSET>::relation_with(const Constraint& c) const { bool is_included = true; /* *this is disjoint with c if every disjunct is disjoint with c */ bool is_disjoint = true; - /* *this strictly_intersects with c if some disjunct strictly - intersects with c */ + /* *this strictly_intersects with c if: + - some disjunct strictly intersects with c + or + - there exists two disjoints d1 and d2 + such that d1 is included in c and d2 is disjoint with c + */ bool is_strictly_intersecting = false; - /* *this saturates c if some disjunct saturates c and - every disjunct is either disjoint from c or saturates c */ - bool saturates_once = false; - bool may_saturate = true; + bool included_once = false; + bool disjoint_once = false; + /* *this saturates c if all disjuncts saturate c */ + bool saturates = true; for (Sequence_const_iterator si = x.sequence.begin(), s_end = x.sequence.end(); si != s_end; ++si) { Poly_Con_Relation relation_i = si->pointset().relation_with(c); - if (!relation_i.implies(Poly_Con_Relation::is_included())) { + if (relation_i.implies(Poly_Con_Relation::is_included())) { + included_once = true; + } + else { is_included = false; } - if (!relation_i.implies(Poly_Con_Relation::is_disjoint())) { + if (relation_i.implies(Poly_Con_Relation::is_disjoint())) { + disjoint_once = true; + } + else { is_disjoint = false; } if (relation_i.implies(Poly_Con_Relation::strictly_intersects())) { is_strictly_intersecting = true; } - if (relation_i.implies(Poly_Con_Relation::saturates())) { - saturates_once = true; - } - else if (!relation_i.implies(Poly_Con_Relation::is_disjoint())) { - may_saturate = false; + if (!relation_i.implies(Poly_Con_Relation::saturates())) { + saturates = false; } } @@ -924,10 +931,10 @@ Pointset_Powerset<PSET>::relation_with(const Constraint& c) const { if (is_disjoint) { result = result && Poly_Con_Relation::is_disjoint(); } - if (is_strictly_intersecting) { + if (is_strictly_intersecting || (included_once && disjoint_once)) { result = result && Poly_Con_Relation::strictly_intersects(); } - if (saturates_once && may_saturate) { + if (saturates) { result = result && Poly_Con_Relation::saturates(); } return result;

1 0

[GIT] ppl/ppl(devel): Corrected expected result for test06().
by Enea Zaffanella 19 Nov '15

19 Nov '15

Module: ppl/ppl Branch: devel Commit: fd92d113b4b3a646573fbaa26d35f62701e3ac12 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fd92d113b4b3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 11:57:02 2015 +0100 Corrected expected result for test06(). Added a new testcase as test11(). The two tests show a bug in current implementation of method Pointset_Powerset<PSET>::relation_with(const Constraint& c) const --- tests/Powerset/relationwith1.cc | 29 +++++++++++++++++++++++++++-- 1 files changed, 27 insertions(+), 2 deletions(-) diff --git a/tests/Powerset/relationwith1.cc b/tests/Powerset/relationwith1.cc index bff7e5b..a76856c 100644 --- a/tests/Powerset/relationwith1.cc +++ b/tests/Powerset/relationwith1.cc @@ -147,15 +147,15 @@ test06() { C_Polyhedron ph2(1); ph2.add_constraint(x == 2); - Pointset_Powerset<C_Polyhedron> ps(1, EMPTY); + Pointset_Powerset<C_Polyhedron> ps(1, EMPTY); ps.add_disjunct(ph1); ps.add_disjunct(ph2); Constraint c(x == 1); Poly_Con_Relation rel = ps.relation_with(c); - Poly_Con_Relation known_rel = Poly_Con_Relation::saturates(); + Poly_Con_Relation known_rel = Poly_Con_Relation::strictly_intersects(); bool ok = (rel == known_rel); @@ -262,6 +262,30 @@ test10() { return ok && ps.OK(); } +bool +test11() { + Variable x(0); + + C_Polyhedron ph1(1); + ph1.add_constraint(x <= 0); + + C_Polyhedron ph2(1); + ph2.add_constraint(x >= 2); + + Pointset_Powerset<C_Polyhedron> ps(1, EMPTY); + ps.add_disjunct(ph1); + ps.add_disjunct(ph2); + + Constraint c(x >= 2); + Poly_Con_Relation rel = ps.relation_with(c); + + Poly_Con_Relation known_rel = Poly_Con_Relation::strictly_intersects(); + + bool ok = (rel == known_rel); + + return ok && ps.OK(); +} + } // namespace BEGIN_MAIN @@ -275,4 +299,5 @@ BEGIN_MAIN DO_TEST(test08); DO_TEST(test09); DO_TEST(test10); + DO_TEST(test11); END_MAIN

1 0

[GIT] ppl/ppl(devel): Updated.
by Roberto Bagnara 18 Nov '15

18 Nov '15

Module: ppl/ppl Branch: devel Commit: 3d7c1e0242c21b9e8242527097270258f14a4cfe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d7c1e0242c2… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Tue Jun 30 19:10:15 2015 +0200 Updated. --- CREDITS | 50 ++++++++++++++++++++++++++------------------------ 1 files changed, 26 insertions(+), 24 deletions(-) diff --git a/CREDITS b/CREDITS index a0947c9..7310fc5 100644 --- a/CREDITS +++ b/CREDITS @@ -12,8 +12,8 @@ Core Development Team: Roberto Bagnara [1] (BUGSENG srl and University of Parma) Patricia M. Hill [2] (BUGSENG srl and University of Leeds) - Enea Zaffanella [3] (BUGSENG srl and University of Parma) Abramo Bagnara (BUGSENG srl) + Enea Zaffanella [3] (University of Parma) Former Members of the Core Development Team: @@ -29,29 +29,6 @@ Former Members of the Core Development Team: Current Contributors: --------------------- - Massimo Benerecetti (University of Naples) is working on additional - operators on polyhedra. - - Andrea Cimino (former student of the University of Parma) - wrote most of the mixed integer programming - solver, and also most of the Java and OCaml - interfaces. He keeps helping us, especially - with the web site. - - Marco Faella (University of Naples) is working on additional - operators on polyhedra. - - Stefano Minopoli (University of Naples) is working on additional - operators on polyhedra. - - Marco Poletti (student of the University of Bologna) - implemented the sparse matrices that are used - in the MIP and PIP solvers of the PPL; he also - did experiments on the parallelization of the - sparse matrices' computations; he is now working - on improving the PPL's memory footprint and - on other improvements to the library. - Alessandro Zaccagnini [4] (University of Parma) has helped with the efficient implementation of GCD and LCM for checked numbers. He is now working on the @@ -59,6 +36,9 @@ Current Contributors: Alessandro is always a very valuable source of mathematical advice. + Paulo Cesar Pereira de Andrade + Helps with Fedora packaging. + Past Contributors: ------------------ @@ -73,6 +53,9 @@ Past Contributors: whether or not the set-union of two polyhedra is the same as their poly-hull. + Massimo Benerecetti (University of Naples) worked on the positive + time-elapse operator on polyhedra. + Fabio Biselli (student of the University of Parma) did some work on the PPL support for the approximation of floating point computations. @@ -93,11 +76,19 @@ Past Contributors: one of the four students with which the PPL project started. + Andrea Cimino (former student of the University of Parma) + wrote most of the mixed integer programming + solver, and also most of the Java and OCaml + interfaces. He helped us a lot with the web site. + Katy Dobson (former student of the University of Leeds) worked on the formalization and definition of algorithms for rational grids and products of grids and polyhedra. + Marco Faella (University of Naples) worked on the positive + time-elapse operator on polyhedra. + Giordano Fracasso (former student of the University of Parma) wrote the initial version of the support for native and checked integer coefficients. @@ -121,6 +112,9 @@ Past Contributors: with the generation of the library's documentation using Doxygen. + Stefano Minopoli (University of Naples) worked on the positive + time-elapse operator on polyhedra. + Matthew Mundell [6] (formerly at the University of Leeds) worked on the implementation of rational grids. He has also helped on other implementation issues. @@ -130,6 +124,14 @@ Past Contributors: project started. Later, he helped a little with the library's documentation. + Marco Poletti (former student of the University of Bologna) + implemented the sparse matrices that are used + in the MIP and PIP solvers of the PPL; he also + did experiments on the parallelization of the + sparse matrices' computations; he also worked + on improving the PPL's memory footprint and + on other improvements to the library. + Barbara Quartieri (former student of the University of Parma) worked on our implementation of bounded differences and octagons.

1 0