April 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Size has to be specified in bits.
by Abramo Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: f4152242e68e80d38a8ed790fdfd23116c79b1f3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f4152242e68e… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Mon Apr 20 15:21:57 2009 +0200 Size has to be specified in bits. --- src/Bit_Row.inlines.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Bit_Row.inlines.hh b/src/Bit_Row.inlines.hh index 5321f41..0803ffe 100644 --- a/src/Bit_Row.inlines.hh +++ b/src/Bit_Row.inlines.hh @@ -50,11 +50,11 @@ Bit_Row::Bit_Row(const Bit_Row& y, const Bit_Row& z) { const mp_size_t y_size = y.vec->_mp_size; const mp_size_t z_size = z.vec->_mp_size; if (y_size < z_size) { - mpz_init2(vec, z_size); + mpz_init2(vec, z_size * sizeof(mp_limb_t) * 8); union_helper(y, z); } else { - mpz_init2(vec, y_size); + mpz_init2(vec, y_size * sizeof(mp_limb_t) * 8); union_helper(z, y); } }

1 0

[GIT] ppl/ppl(master): New constructor Bit_Row::Bit_Row(const Bit_Row& y, const Bit_Row& z).
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: 03552e3fe4336c7c194c8b8decd092794e0977c8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=03552e3fe433… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 14:43:58 2009 +0200 New constructor Bit_Row::Bit_Row(const Bit_Row& y, const Bit_Row& z). Constructs an object containing the set-union of y and z. --- src/Bit_Row.cc | 26 ++++++++++++++++++++++++++ src/Bit_Row.defs.hh | 13 +++++++++++++ src/Bit_Row.inlines.hh | 14 ++++++++++++++ 3 files changed, 53 insertions(+), 0 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index eee1cbf..e1d2e0f 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -376,3 +376,29 @@ PPL::Bit_Row::OK() const { && vec_alloc >= vec_size && (vec_size == 0 || mpz_getlimbn(vec, vec_size-1) != 0); } + +void +PPL::Bit_Row::union_helper(const Bit_Row& y, const Bit_Row& z) { + mp_size_t y_size = y.vec->_mp_size; + mp_size_t z_size = z.vec->_mp_size; + assert(y_size <= z.size); + assert(vec->_mp_alloc >= z.size); + vec->_mp_size = z_size; + mp_srcptr yp = y.vec->_mp_d; + mp_srcptr zp = z.vec->_mp_d; + mp_ptr p = vec->_mp_d; + z_size -= y_size; + while (y_size > 0) { + *p = *yp | * zp; + ++yp; + ++zp; + ++p; + --y_size; + } + while (z_size > 0) { + *p = *zp; + ++zp; + ++p; + --z_size; + } +} diff --git a/src/Bit_Row.defs.hh b/src/Bit_Row.defs.hh index 613046e..ce278c9 100644 --- a/src/Bit_Row.defs.hh +++ b/src/Bit_Row.defs.hh @@ -116,6 +116,12 @@ public: //! Copy-constructor. Bit_Row(const Bit_Row& y); + //! Set-union constructor. + /*! + Constructs an object containing the set-union of \p y and \p z. + */ + Bit_Row(const Bit_Row& y, const Bit_Row& z); + //! Destructor. ~Bit_Row(); @@ -191,6 +197,13 @@ private: //! Bit-vector representing the row. mpz_t vec; + //! Assigns to \p *this the union of \p y and \p z. + /*! + The size of \p y must be be less than or equal to the size of \p z. + Upon entry, \p vec must have allocated enough space to contain the result. + */ + void union_helper(const Bit_Row& x, const Bit_Row& y); + //! Assuming \p w is nonzero, returns the index of the first set bit in \p w. static unsigned int first_one(mp_limb_t w); diff --git a/src/Bit_Row.inlines.hh b/src/Bit_Row.inlines.hh index 6fc36f7..5321f41 100644 --- a/src/Bit_Row.inlines.hh +++ b/src/Bit_Row.inlines.hh @@ -46,6 +46,20 @@ Bit_Row::Bit_Row(const Bit_Row& y) { } inline +Bit_Row::Bit_Row(const Bit_Row& y, const Bit_Row& z) { + const mp_size_t y_size = y.vec->_mp_size; + const mp_size_t z_size = z.vec->_mp_size; + if (y_size < z_size) { + mpz_init2(vec, z_size); + union_helper(y, z); + } + else { + mpz_init2(vec, y_size); + union_helper(z, y); + } +} + +inline Bit_Row::~Bit_Row() { mpz_clear(vec); }

1 0

[GIT] ppl/ppl(master): Further improved subset_or_equal(const Bit_Row&, const Bit_Row&, bool&).
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: ead61e70bbce24c517afc3f79d2285b8abcfdb4c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ead61e70bbce… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 13:50:09 2009 +0200 Further improved subset_or_equal(const Bit_Row&, const Bit_Row&, bool&). --- src/Bit_Row.cc | 51 ++++++++++++++++++++++++++------------------------- 1 files changed, 26 insertions(+), 25 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index 688fff8..eee1cbf 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -282,33 +282,34 @@ PPL::subset_or_equal(const Bit_Row& x, const Bit_Row& y, mp_srcptr xp = x.vec->_mp_d; mp_srcptr yp = y.vec->_mp_d; strict_subset = (x_size < y_size); - if (strict_subset) - goto strict_subset_loop; - - while (x_size > 0) { - const mp_limb_t xl = *xp; - const mp_limb_t yl = *yp; - if (xl & ~yl) - return false; - ++xp; - ++yp; - --x_size; - if (xl != yl) { - strict_subset = true; - goto strict_subset_loop; + mp_limb_t xl; + mp_limb_t yl; + if (strict_subset) { + while (x_size > 0) { + xl = *xp; + yl = *yp; + if (xl & ~yl) + return false; + strict_subset_next: + ++xp; + ++yp; + --x_size; } } - return true; - - strict_subset_loop: - while (x_size > 0) { - const mp_limb_t xl = *xp; - const mp_limb_t yl = *yp; - if (xl & ~yl) - return false; - ++xp; - ++yp; - --x_size; + else { + while (x_size > 0) { + xl = *xp; + yl = *yp; + if (xl != yl) { + if (xl & ~yl) + return false; + strict_subset = true; + goto strict_subset_next; + } + ++xp; + ++yp; + --x_size; + } } return true; }

1 0

[GIT] ppl/ppl(master): Avoid useless allocations by only adding recycled rows to Bit_Matrix.
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: 73047e08667ebca99b0262dd03c07f100f3c2925 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=73047e08667e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 12:18:05 2009 +0200 Avoid useless allocations by only adding recycled rows to Bit_Matrix. --- src/Bit_Matrix.cc | 9 +++++---- src/Bit_Matrix.defs.hh | 8 +++++++- src/conversion.cc | 4 ++-- 3 files changed, 14 insertions(+), 7 deletions(-) diff --git a/src/Bit_Matrix.cc b/src/Bit_Matrix.cc index ac126c5..dbce634 100644 --- a/src/Bit_Matrix.cc +++ b/src/Bit_Matrix.cc @@ -55,7 +55,7 @@ PPL::Bit_Matrix::sort_rows() { } void -PPL::Bit_Matrix::add_row(const Bit_Row& row) { +PPL::Bit_Matrix::add_recycled_row(Bit_Row& row) { const dimension_type new_rows_size = rows.size() + 1; if (rows.capacity() < new_rows_size) { // Reallocation will take place. @@ -64,7 +64,7 @@ PPL::Bit_Matrix::add_row(const Bit_Row& row) { new_rows.insert(new_rows.end(), new_rows_size, Bit_Row()); // Put the new row in place. dimension_type i = new_rows_size-1; - new_rows[i] = row; + new_rows[i].swap(row); // Steal the old rows. while (i-- > 0) new_rows[i].swap(rows[i]); @@ -72,8 +72,9 @@ PPL::Bit_Matrix::add_row(const Bit_Row& row) { std::swap(rows, new_rows); } else - // Reallocation will NOT take place: append a new empty row. - rows.push_back(row); + // Reallocation will NOT take place: append an empty row + // and swap it with the new row. + rows.insert(rows.end(), Bit_Row())->swap(row); assert(OK()); } diff --git a/src/Bit_Matrix.defs.hh b/src/Bit_Matrix.defs.hh index 82f4b4f..c460924 100644 --- a/src/Bit_Matrix.defs.hh +++ b/src/Bit_Matrix.defs.hh @@ -94,7 +94,13 @@ public: bool sorted_contains(const Bit_Row& row) const; //! Adds \p row to \p *this. - void add_row(const Bit_Row& row); + /*! + \param row + The row whose implementation will be recycled. + + The only thing that can be done with \p row upon return is destruction. + */ + void add_recycled_row(Bit_Row& row); //! Erases the rows from the \p first_to_erase -th to the last one. void rows_erase_to_end(dimension_type first_to_erase); diff --git a/src/conversion.cc b/src/conversion.cc index ec581f7..7c0b04b 100644 --- a/src/conversion.cc +++ b/src/conversion.cc @@ -721,10 +721,10 @@ PPL::Polyhedron::conversion(Linear_System& source, // Make room for one more row. dest.add_pending_row(Linear_Row::Flags(dest.topology(), Linear_Row::RAY_OR_POINT_OR_INEQUALITY)); - sat.add_row(new_satrow); + sat.add_recycled_row(new_satrow); } else - sat[dest_num_rows] = new_satrow; + sat[dest_num_rows].swap(new_satrow); Linear_Row& new_row = dest[dest_num_rows]; // The following fragment optimizes the computation of

1 0

[GIT] ppl/ppl(master): Significantly speeded up the construction of `new_satrow'.
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: 5959eedc504b636abadb642035680a78627b21a0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5959eedc504b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 10:49:44 2009 +0200 Significantly speeded up the construction of `new_satrow'. --- src/conversion.cc | 8 +++++--- 1 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/conversion.cc b/src/conversion.cc index 3fd1757..ec581f7 100644 --- a/src/conversion.cc +++ b/src/conversion.cc @@ -670,15 +670,16 @@ PPL::Polyhedron::conversion(Linear_System& source, // If there exist another generator that saturates // all the constraints saturated by both `dest[i]' and // `dest[j]', then they are NOT adjacent. - Bit_Row new_satrow; assert(sat[i].last() == ULONG_MAX || sat[i].last() < k); assert(sat[j].last() == ULONG_MAX || sat[j].last() < k); + // Being the union of `sat[i]' and `sat[j]', // `new_satrow' corresponds to a ray that saturates all the // constraints saturated by both `dest[i]' and `dest[j]'. - set_union(sat[i], sat[j], new_satrow); + Bit_Row new_satrow(sat[i]); + set_union(new_satrow, sat[j], new_satrow); - // Computing the number of common saturators. + // Compute the number of common saturators. // NOTE: this number has to be less than `k' because // we are treating the `k'-th constraint. const dimension_type @@ -724,6 +725,7 @@ PPL::Polyhedron::conversion(Linear_System& source, } else sat[dest_num_rows] = new_satrow; + Linear_Row& new_row = dest[dest_num_rows]; // The following fragment optimizes the computation of //

1 0

[GIT] ppl/ppl(master): Improved subset_or_equal(const Bit_Row&, const Bit_Row&, bool&).
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: 33cd6b46113c1db583a43eccf9e0a9076018948a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=33cd6b46113c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 10:37:36 2009 +0200 Improved subset_or_equal(const Bit_Row&, const Bit_Row&, bool&). --- src/Bit_Row.cc | 21 +++++++++++++++++++-- 1 files changed, 19 insertions(+), 2 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index 32a3ff0..688fff8 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -279,16 +279,33 @@ PPL::subset_or_equal(const Bit_Row& x, const Bit_Row& y, assert(y_size >= 0); if (x_size > y_size) return false; - strict_subset = (x_size < y_size); mp_srcptr xp = x.vec->_mp_d; mp_srcptr yp = y.vec->_mp_d; + strict_subset = (x_size < y_size); + if (strict_subset) + goto strict_subset_loop; + while (x_size > 0) { const mp_limb_t xl = *xp; const mp_limb_t yl = *yp; if (xl & ~yl) return false; - if (!strict_subset && xl != yl) + ++xp; + ++yp; + --x_size; + if (xl != yl) { strict_subset = true; + goto strict_subset_loop; + } + } + return true; + + strict_subset_loop: + while (x_size > 0) { + const mp_limb_t xl = *xp; + const mp_limb_t yl = *yp; + if (xl & ~yl) + return false; ++xp; ++yp; --x_size;

1 0

PPL 0.10.2 on Cygwin
by Roberto Bagnara 20 Apr '09

20 Apr '09

http://www.cygwin.com/ml/cygwin-apps/2009-04/msg00074.html -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

[GIT] ppl/ppl(deprecated_0_11_removal): Removed tests for the deprecated *and_minimize() predicates.
by Patricia Hill 19 Apr '09

19 Apr '09

Module: ppl/ppl Branch: deprecated_0_11_removal Commit: 6d7e265c238bcc62cff25ded4f134882114d91d7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6d7e265c238b… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Sun Apr 19 20:42:46 2009 +0100 Removed tests for the deprecated *and_minimize() predicates. --- interfaces/Prolog/tests/pl_check.pl | 147 +------------------- ...face_generator_prolog_generated_test_pl_code.m4 | 113 --------------- 2 files changed, 3 insertions(+), 257 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=6d7e265c…

1 0

[GIT] ppl/ppl(deprecated_0_11_removal): Removed deprecated methods *and_minimize().
by Patricia Hill 18 Apr '09

18 Apr '09

Module: ppl/ppl Branch: deprecated_0_11_removal Commit: ee3078871418fbb8d3bc57c6fb0bbcd7ebdf00fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ee3078871418… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Sat Apr 18 22:19:12 2009 +0100 Removed deprecated methods *and_minimize(). --- tests/Grid/addcongruence1.cc | 33 +----- tests/Grid/addcongruences1.cc | 199 ++++++++------------------------- tests/Grid/addconstraint1.cc | 42 +------- tests/Grid/addconstraints1.cc | 123 ++------------------- tests/Grid/addgenerator1.cc | 55 ++------- tests/Grid/addgenerators1.cc | 100 +++-------------- tests/Grid/affinedim1.cc | 14 +- tests/Grid/affineimage2.cc | 8 +- tests/Grid/bounded1.cc | 16 ++-- tests/Grid/bounds1.cc | 18 ++-- tests/Grid/certificate1.cc | 2 +- tests/Grid/congruences1.cc | 2 +- tests/Grid/containsintegerpoint1.cc | 10 +- tests/Grid/discrete1.cc | 14 +- tests/Grid/generators1.cc | 2 +- tests/Grid/grid1.cc | 92 ++++++++-------- tests/Grid/grid2.cc | 78 +++++++------- tests/Grid/intersection1.cc | 213 +---------------------------------- tests/Grid/maxmin1.cc | 18 ++-- tests/Grid/mingenerators1.cc | 2 +- tests/Grid/partition1.cc | 3 +- tests/Grid/removespacedims1.cc | 6 +- tests/Grid/removespacedims2.cc | 4 +- tests/Grid/simplifyusingcontext1.cc | 8 +- tests/Grid/topclosed1.cc | 14 +- 25 files changed, 245 insertions(+), 831 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ee307887…

1 0

[GIT] ppl/ppl(master): Mark package ppl-yap as obsoleting ppl-yap-static.
by Roberto Bagnara 18 Apr '09

18 Apr '09

Module: ppl/ppl Branch: master Commit: 7c6f088f403eb8630960ab019f07d7c7bb205014 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7c6f088f403e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 18 15:11:52 2009 +0200 Mark package ppl-yap as obsoleting ppl-yap-static. --- fedora/ppl.spec | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/fedora/ppl.spec b/fedora/ppl.spec index 1f6b48a..351a883 100644 --- a/fedora/ppl.spec +++ b/fedora/ppl.spec @@ -106,6 +106,7 @@ Summary: The YAP Prolog interface of the Parma Polyhedra Library Group: Development/Libraries BuildRequires: yap-devel >= 5.1.1 Requires: %{name} = %{version}-%{release}, %{name}-pwl = %{version}-%{release}, yap >= 5.1.1 +Obsoletes: ppl-yap-static %description yap This package adds YAP Prolog support to the Parma Polyhedra Library (PPL). Install this package if you want to use the library in YAP Prolog programs.

1 0