August 2017 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(devel): Fixed typos in Prolog documentation for ppl_Pointset_Powerset predicates.
by Patricia Hill 22 Aug '17

22 Aug '17

Module: ppl/ppl Branch: devel Commit: f41d7c42ac9dadb807fb6a499d8d083125cbc345 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f41d7c42ac9d… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Tue Aug 8 20:06:17 2017 +0100 Fixed typos in Prolog documentation for ppl_Pointset_Powerset predicates. --- .../Prolog/Prolog_interface_sysindep_domains.dox | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/interfaces/Prolog/Prolog_interface_sysindep_domains.dox b/interfaces/Prolog/Prolog_interface_sysindep_domains.dox index d868ad3..9d4d273 100644 --- a/interfaces/Prolog/Prolog_interface_sysindep_domains.dox +++ b/interfaces/Prolog/Prolog_interface_sysindep_domains.dox @@ -812,15 +812,15 @@ on these iterators and disjuncts via the usual handles. \c Iterator_1 is equal to the iterator referenced by \c Iterator_2. -<CODE>ppl_Pointset_Powerset_C_Polyhedron_iterator_increment(+Iterator)</CODE> +<CODE>ppl_Pointset_Powerset_C_Polyhedron_increment_iterator(+Iterator)</CODE> Increments the iterator referenced by \c Iterator so that it "points" to the next disjunct. -<CODE>ppl_Pointset_Powerset_C_Polyhedron_iterator_decrement(+Iterator)</CODE> +<CODE>ppl_Pointset_Powerset_C_Polyhedron_decrement_iterator(+Iterator)</CODE> Decrements the iterator referenced by \c Iterator so that it "points" to the previous disjunct. -<CODE>ppl_Pointset_Powerset_C_Polyhedron_iterator_get_disjunct(+Iterator, -Handle)</CODE> +<CODE>ppl_Pointset_Powerset_C_Polyhedron_get_disjunct(+Iterator, -Handle)</CODE> Unifies with \c Handle a reference to the disjunct referred to by \c Iterator_1.

2 1

difference on pointset powerset
by j.c.vandepol＠utwente.nl 14 Aug '17

14 Aug '17

Dear developers of PPL, Is it possible to directly compute the set-difference of two pointset powersets? In particular, I’m interested in the precise complement; convex difference approximations are not sufficient for my case. Kind regards, Jaco van de Pol -- Prof. Jaco van de Pol University of Twente (NL) Formal Methods and Tools http://www.cs.utwente.nl/~vdpol

2 3

On using PPL (powersets) from SWI Prolog
by j.c.vandepol＠utwente.nl 07 Aug '17

07 Aug '17

Hi Roberto, other developers, Thanks for the package PPL! I'm just going to use it for the first time, and I have read some documentation, but it looks really great. I had some issues when installing and using the Parma Polyhedra Library for the first time. Everything seems to be working now, so I hope you can use my experience to improve the documentation a bit (which is already quite extensive!). What I need are disjunctions of conjunctions of inequations, so I decided to go for the pointset powerset domain. I was already using CLP, so I decided to go for the SWI Prolog bindings. (Probably not directly the easiest path into using PPL) At the end, some suggestion how a “more Prolog-like” interface could look like. I really hope this helps you and future users. Kind regards, Jaco van de Pol I am using PPL version 1.2, on a Mac Notebook with MacOS Sierra 10.12.6, with SWI Prolog version 7.2.3. I was using the following documentation: - http://bugseng.com/products/ppl/documentation//user/ppl-user-prolog-interfa… Here are some issues: 1. "brew install ppl" nicely installs PPL, but it doesn't provide the SWI bindings / library, so I decided to install it myself from the source code. 2. The documentation suggests that SWI bindings should be generated automatically if swipl is on the path. This was not true: I had to explicitly add: --enable-interfaces=SWI_PROLOG (and this was not documented a.f.a.i.k.) 3. The library is called "*.so", where swipl expects it to be called "*.dylib". I found a comment on the web about it, but the documentation didn't mention it. It requires either making a ln -s link manually, or loading the library with :- load_foreign_library('<prefix>/lib/ppl/libppl_swiprolog.so'). 4. I found it hard to understand how variables are handled. Apparently I need something like '$Var'(VarId). It appears in the grammar ("predicate specifications") but it is not explained what this is supposed to mean and what the rules are. 5. I found it hard to get started with disjunctions (Pointset_Powerset). The documentation seems incomplete, and it was not clear what the various +Iterators and +Handles are referring to exactly. 6. The feature I was lacking most was how to create an initial Pointset_Powerset. I found out that the following was working, but this function seems to be missing entirely from the documentation. I understand that this follows a general pattern, but it makes it hard to get started with powerset domains: ppl_new_Pointset_Powerset_C_Polyhedron_from_space_dimension(0,empty,R), 7. The documentation says: ppl_Pointset_Powerset_C_Polyhedron_iterator_get_disjunct(+Iterator, -Handle) Unifies with Handle a reference to the disjunct referred to by Iterator_1. However, the real name appears to be: ppl_Pointset_Powerset_C_Polyhedron_get_disjunct 8. The documentation says: ppl_Pointset_Powerset_C_Polyhedron_iterator_increment(+Iterator) Increments the iterator referenced by Iterator so that it "points" to the next disjunct. However, the real name appears to be: ppl_Pointset_Powerset_C_Polyhedron_increment_iterator 8b. (probably similar with decrement; I didn't check it) 9. It would help to add some code examples, if only in the test scripts for PPL, but preferably to the documentation. It seems that example code (with prolog) is missing throughout the documentation. Here is my first example, maybe you can use it. (In particular: nice to see how the two boxes are glued together in a single box!) load_foreign_library('/Users/vdpol/lib/ppl/libppl_swiprolog.so'). X='$VAR'(0), Y='$VAR'(1), ppl_new_C_Polyhedron_from_constraints([X>=2, Y>=1, 5-X >= Y],P), ppl_new_C_Polyhedron_from_constraints([X=<4, Y=<3, Y >= 5-X],Q), ppl_Polyhedron_get_constraints(P,LP), ppl_Polyhedron_get_constraints(Q,LQ), ppl_new_Pointset_Powerset_C_Polyhedron_from_space_dimension(2,empty,R), ppl_Pointset_Powerset_C_Polyhedron_add_disjunct(R,P), ppl_Pointset_Powerset_C_Polyhedron_add_disjunct(R,Q), ppl_Pointset_Powerset_C_Polyhedron_pairwise_reduce(R), ppl_Pointset_Powerset_C_Polyhedron_begin_iterator(R,I), ppl_Pointset_Powerset_C_Polyhedron_get_disjunct(I,P1), ppl_Polyhedron_get_constraints(P1,L1). 9. Handling handles and iterators is quite error-prone (in particular handling their side effects, and the implicit typing rules). This can even lead to segfaults, consider the following (wrong) attempt (there is no second disjunct after pairwise_reduce): load_foreign_library('/Users/vdpol/lib/ppl/libppl_swiprolog.so'). X='$VAR'(0), Y='$VAR'(1), ppl_new_C_Polyhedron_from_constraints([X>=2, Y>=1, 5-X >= Y],P), ppl_new_C_Polyhedron_from_constraints([X=<4, Y=<3, Y >= 5-X],Q), ppl_new_Pointset_Powerset_C_Polyhedron_from_space_dimension(2,empty,R), ppl_Pointset_Powerset_C_Polyhedron_add_disjunct(R,P), ppl_Pointset_Powerset_C_Polyhedron_add_disjunct(R,P), ppl_Pointset_Powerset_C_Polyhedron_pairwise_reduce(R), ppl_Pointset_Powerset_C_Polyhedron_begin_iterator(R,I), ppl_Pointset_Powerset_C_Polyhedron_increment_iterator(I), ppl_Pointset_Powerset_C_Polyhedron_get_disjunct(I,P2), ppl_Polyhedron_get_constraints(P2,L). (I ran into quite some more segfaults from SWI-Prolog (!)) 10. Handling handles and iterators is quite un-Prolog-like (side effects). To me, it seems more natural to provide a Prolog-interface at the level of "conjunctions from lists of constraints" and "disjunctions from lists of conjunctions". With some simple auxiliary functions I can write code like: X='$VAR'(0), Y='$VAR'(1), conjunction([X>=2, Y>=1, 5-X >= Y],P), conjunction([X=<4, Y=<3, Y >= 5-X],Q), disjunction([P,Q],2,R), get_disjuncts(R,D). The code to get the disjuncts reads as follows. (Maybe I shouldn't have called ppl_Polyhedron_get_constraints in this code; I'm not yet sure if I want to encapsulate the handles, or keep them in my prolog program) get_all_disjuncts(_,Begin,End,[]) :- ppl_Pointset_Powerset_C_Polyhedron_iterator_equals_iterator(Begin,End), !, ppl_delete_Pointset_Powerset_C_Polyhedron_iterator(Begin), ppl_delete_Pointset_Powerset_C_Polyhedron_iterator(End). get_all_disjuncts(D,Begin,End,[Cs|L]) :- ppl_Pointset_Powerset_C_Polyhedron_get_disjunct(Begin,C), ppl_Polyhedron_get_constraints(C,Cs), ppl_Pointset_Powerset_C_Polyhedron_increment_iterator(Begin), get_all_disjuncts(D,Begin,End,L). get_disjuncts(D,L) :- ppl_Pointset_Powerset_C_Polyhedron_begin_iterator(D,B), ppl_Pointset_Powerset_C_Polyhedron_end_iterator(D,E), get_all_disjuncts(D,B,E,L). -- Prof. Jaco van de Pol University of Twente (NL) Formal Methods and Tools http://www.cs.utwente.nl/~vdpol

1 0

[GIT] ppl/ppl(devel): Modified the comparison function for generators.
by Enea Zaffanella 03 Aug '17

03 Aug '17

Module: ppl/ppl Branch: devel Commit: 2415b288480b08b85692cff798a3ca823d307d79 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2415b288480b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Aug 3 18:19:45 2017 +0200 Modified the comparison function for generators. The epsilon coefficient is checked last, after the divisor. This fixes the bug identified in test07() of nncminimize1.cc. --- src/Expression_Hide_Last_defs.hh | 8 +++++ src/Expression_Hide_Last_inlines.hh | 52 +++++++++++++++++++++++++++++++ src/Generator.cc | 43 ++++++++++++++++++++++--- src/Linear_Expression_Impl_defs.hh | 3 ++ src/Linear_Expression_Impl_templates.hh | 6 +++ src/Linear_Expression_Interface_defs.hh | 3 ++ src/Linear_Expression_defs.hh | 3 ++ src/Linear_Expression_inlines.hh | 7 ++++ 8 files changed, 119 insertions(+), 6 deletions(-) diff --git a/src/Expression_Hide_Last_defs.hh b/src/Expression_Hide_Last_defs.hh index d57005c..392a25e 100644 --- a/src/Expression_Hide_Last_defs.hh +++ b/src/Expression_Hide_Last_defs.hh @@ -160,6 +160,14 @@ private: const bool hide_last_; }; +namespace Parma_Polyhedra_Library { + +template <typename T> +int compare(const Expression_Hide_Last<T>& x, + const Expression_Hide_Last<T>& y); + +} // namespace Parma_Polyhedra_Library + #include "Expression_Hide_Last_inlines.hh" #endif // !defined(PPL_Expression_Hide_Last_defs_hh) diff --git a/src/Expression_Hide_Last_inlines.hh b/src/Expression_Hide_Last_inlines.hh index 17306dd..58bc72b 100644 --- a/src/Expression_Hide_Last_inlines.hh +++ b/src/Expression_Hide_Last_inlines.hh @@ -239,6 +239,58 @@ Expression_Hide_Last<T> return this->inner().have_a_common_variable(y, first, last); } +template <typename T> +inline int +compare(const Expression_Hide_Last<T>& x, const Expression_Hide_Last<T>& y) { + typedef typename Expression_Hide_Last<T>::const_iterator CIter; + CIter i = x.begin(); + CIter i_end = x.end(); + CIter j = y.begin(); + CIter j_end = y.end(); + while (i != i_end && j != j_end) { + if (i.index() < j.index()) { + const int s = sgn(*i); + if (s != 0) { + return 2*s; + } + ++i; + continue; + } + if (i.index() > j.index()) { + const int s = sgn(*j); + if (s != 0) { + return -2*s; + } + ++j; + continue; + } + PPL_ASSERT(i.index() == j.index()); + const int s = cmp(*i, *j); + if (s < 0) { + return -2; + } + if (s > 0) { + return 2; + } + PPL_ASSERT(s == 0); + ++i; + ++j; + } + for ( ; i != i_end; ++i) { + const int s = sgn(*i); + if (s != 0) { + return 2*s; + } + } + for ( ; j != j_end; ++j) { + const int s = sgn(*j); + if (s != 0) { + return -2*s; + } + } + return 0; +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Expression_Hide_Last_inlines_hh) diff --git a/src/Generator.cc b/src/Generator.cc index 8958163..4ee294d 100644 --- a/src/Generator.cc +++ b/src/Generator.cc @@ -212,14 +212,45 @@ PPL::Generator::linear_combine(const Generator& y, const dimension_type i) { /*! \relates Parma_Polyhedra_Library::Generator */ int PPL::compare(const Generator& x, const Generator& y) { - const bool x_is_line_or_equality = x.is_line_or_equality(); - const bool y_is_line_or_equality = y.is_line_or_equality(); - if (x_is_line_or_equality != y_is_line_or_equality) { - // Equalities (lines) precede inequalities (ray/point). - return y_is_line_or_equality ? 2 : -2; + const bool x_is_line = x.is_line(); + const bool y_is_line = y.is_line(); + if (x_is_line != y_is_line) { + // Lines precede rays and (closure) points. + return y_is_line ? 2 : -2; + } + if (x.is_necessarily_closed() && y.is_necessarily_closed()) { + return compare(x.expr, y.expr); } - return compare(x.expr, y.expr); + // Epsilon coefficient should be checked last: + // to this end, we use the adapted expression(). + int comp = compare(x.expression(), y.expression()); + if (comp != 0) { + return comp; + } + // Same homogeneous terms (disregarding epsilon). + if (x_is_line) { + PPL_ASSERT(y_is_line); + // Same line. + return 0; + } + if (x.is_ray()) { + return y.is_ray() ? 0 : -1; + } + if (y.is_ray()) { + return 1; + } + // Compare divisors. + comp = cmp(x.divisor(), y.divisor()); + if (comp > 0) { + return 1; + } + if (comp < 0) { + return -1; + } + PPL_ASSERT(comp == 0); + // `x' and `y' may only differ on their epsilon coefficient. + return cmp(x.epsilon_coefficient(), y.epsilon_coefficient()); } bool diff --git a/src/Linear_Expression_Impl_defs.hh b/src/Linear_Expression_Impl_defs.hh index f6e41e8..51094af 100644 --- a/src/Linear_Expression_Impl_defs.hh +++ b/src/Linear_Expression_Impl_defs.hh @@ -172,6 +172,9 @@ public: */ virtual Variable variable() const; + //! Returns the index of the coefficient pointed to by \c *this. + virtual dimension_type index() const; + //! Compares \p *this with x . /*! \param x diff --git a/src/Linear_Expression_Impl_templates.hh b/src/Linear_Expression_Impl_templates.hh index f388a97..fd0d86f 100644 --- a/src/Linear_Expression_Impl_templates.hh +++ b/src/Linear_Expression_Impl_templates.hh @@ -1327,6 +1327,12 @@ Linear_Expression_Impl<Row>::const_iterator } template <typename Row> +dimension_type +Linear_Expression_Impl<Row>::const_iterator::index() const { + return itr.index(); +} + +template <typename Row> bool Linear_Expression_Impl<Row>::const_iterator ::operator==(const const_iterator_interface& x) const { diff --git a/src/Linear_Expression_Interface_defs.hh b/src/Linear_Expression_Interface_defs.hh index 3e973e9..e616a1b 100644 --- a/src/Linear_Expression_Interface_defs.hh +++ b/src/Linear_Expression_Interface_defs.hh @@ -96,6 +96,9 @@ public: */ virtual Variable variable() const = 0; + //! Returns the index of the coefficient pointed to by \c *this. + virtual dimension_type index() const = 0; + //! Compares \p *this with x . /*! \param x diff --git a/src/Linear_Expression_defs.hh b/src/Linear_Expression_defs.hh index b6e72d3..db10bcb 100644 --- a/src/Linear_Expression_defs.hh +++ b/src/Linear_Expression_defs.hh @@ -459,6 +459,9 @@ public: */ Variable variable() const; + //! Returns the index of the coefficient pointed to by \c *this. + dimension_type index() const; + //! Compares \p *this with \p i. /*! \param i diff --git a/src/Linear_Expression_inlines.hh b/src/Linear_Expression_inlines.hh index 202bb21..b5b532a 100644 --- a/src/Linear_Expression_inlines.hh +++ b/src/Linear_Expression_inlines.hh @@ -682,6 +682,13 @@ Linear_Expression::const_iterator return itr->variable(); } +inline dimension_type +Linear_Expression::const_iterator +::index() const { + PPL_ASSERT(itr != NULL); + return itr->index(); +} + inline bool Linear_Expression::const_iterator ::operator==(const const_iterator& i) const {

1 0

[GIT] ppl/ppl(devel): New test07() shows a bug in the filtering of minimized NNC generators.
by Enea Zaffanella 03 Aug '17

03 Aug '17

Module: ppl/ppl Branch: devel Commit: 0ea33aae911bf0fe56896b6579cd30118459e686 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0ea33aae911b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Aug 3 14:44:46 2017 +0200 New test07() shows a bug in the filtering of minimized NNC generators. The bug should only affect output operations; it is not going to affect the result of methods such as NNC_Polyhedron::is_topologically_closed(). The bug has been discovered while working on an alternative representation and implementation for NNC polyhedra, requiring no epsilon dimension. The conversion algorithm for this new representation will be described in the undergraduate thesis of Anna Becchi (work in progress). --- tests/Polyhedron/nncminimize1.cc | 28 ++++++++++++++++++++++++++++ 1 files changed, 28 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/nncminimize1.cc b/tests/Polyhedron/nncminimize1.cc index 7f22ed3..a8325b6 100644 --- a/tests/Polyhedron/nncminimize1.cc +++ b/tests/Polyhedron/nncminimize1.cc @@ -368,6 +368,33 @@ test06() { return ok; } +bool +test07() { + Variable A(0); + Variable B(1); + + Generator_System gs; + gs.insert(closure_point(A + 2*B)); + gs.insert(closure_point(A + 2*B, 2)); + gs.insert(point(A + 2*B)); + gs.insert(point(A + 2*B, 2)); + + NNC_Polyhedron ph(gs); + + nout << endl << "Before NNC minimization:" << endl; + print_constraints(ph.constraints(), "*** ph constraints ***"); + print_generators(ph.generators(), "*** ph generators ***"); + + const Generator_System& min_gs = ph.minimized_generators(); + bool ok = (2 == std::distance(min_gs.begin(), min_gs.end())); + + nout << endl << "After NNC minimization:" << endl; + print_constraints(ph.constraints(), "*** ph constraints ***"); + print_generators(ph.generators(), "*** ph generators ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -377,4 +404,5 @@ BEGIN_MAIN DO_TEST_F8(test04); DO_TEST(test05); DO_TEST(test06); + DO_TEST(test07); END_MAIN

1 0

[GIT] ppl/ppl(devel): Do not include config.h in header files.
by Enea Zaffanella 03 Aug '17

03 Aug '17

Module: ppl/ppl Branch: devel Commit: 401c35278d369a90e41965b70a43e3b21bdb6ebf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=401c35278d36… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Nov 15 10:31:49 2016 +0100 Do not include config.h in header files. --- src/thread_safe.hh | 2 -- 1 files changed, 0 insertions(+), 2 deletions(-) diff --git a/src/thread_safe.hh b/src/thread_safe.hh index 0edc50c..8b1746b 100644 --- a/src/thread_safe.hh +++ b/src/thread_safe.hh @@ -24,8 +24,6 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_thread_safe_hh #define PPL_thread_safe_hh 1 -#include <config.h> - #ifdef PPL_THREAD_SAFE #define PPL_TLS thread_local #else

1 0