- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): New commits
by Roberto Bagnara 16 Oct '10

16 Oct '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e6885ff58136… Merge: 3f052c1b8df2482f0adeb0c4627c7ede4876bc26 ff5b0796773b34ef9d1e26d2a40b4fdb8376dc8f Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Oct 16 09:16:23 2010 +0200 Merge branch 'master' into floating_point URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ff5b0796773b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Oct 16 09:11:15 2010 +0200 Fixed a bug whereby the argument of all the methods unconstrain(Variable var) was not checked correctly for space dimension compatibility. (Thanks to Volker Braun.) URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=97150b49891b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Oct 10 17:41:52 2010 +0200 Documented precondition of method Bit_Matrix::remove_trailing_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3592af215e8a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Oct 10 16:34:30 2010 +0200 In method Bit_Matrix::OK(), do also check the first Bit_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=27a720c897ec… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 3 17:13:33 2010 +0200 Sparse_Row: optimize linear_combine(), avoiding the insertion of too many elements. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e9f743717517… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 3 09:24:55 2010 +0200 Dense_Matrix, Sparse_Matrix: remove useless typedefs for row_type. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=58d732406162… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Oct 1 15:34:50 2010 +0200 CO_Tree: fix comment. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e80dc1425eb… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Mon Sep 27 10:51:10 2010 +0200 CO_Tree: rename the size field into size_, and add a size() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3cb542d4fe76… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Mon Sep 27 10:50:20 2010 +0200 CO_Tree: avoid shadowing a field with a local variable, in external_memory_in_bytes(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6475eea32239… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:51:09 2010 +0200 Dense_Row: mark the constructor from a Sparse_Row as explicit. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d1088ad4fc32… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:50:32 2010 +0200 Sparse_Row: add an assignment operator from a Dense_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9707c1e408c1… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:45:16 2010 +0200 Sparse_Row: copy flags too, in the constructor from a Dense_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5b123a9d2528… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:44:35 2010 +0200 Dense_Row: add a constructor and an assignment operator that take a Sparse_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3426ae69e61c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:43:53 2010 +0200 CO_Tree: fix bug in the constructor from a sequence and remove its second argument, it is used in assertions only.

1 0

[GIT] ppl/ppl(master): Fixed a bug whereby the argument of all the methods unconstrain( Variable var) was not checked correctly for space dimension compatibility.
by Roberto Bagnara 16 Oct '10

16 Oct '10

Module: ppl/ppl Branch: master Commit: ff5b0796773b34ef9d1e26d2a40b4fdb8376dc8f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ff5b0796773b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Oct 16 09:11:15 2010 +0200 Fixed a bug whereby the argument of all the methods unconstrain(Variable var) was not checked correctly for space dimension compatibility. (Thanks to Volker Braun.) --- NEWS | 9 ++++++++- src/BD_Shape.templates.hh | 8 ++++---- src/Box.inlines.hh | 10 ++++++---- src/Grid_public.cc | 4 ++-- src/Octagonal_Shape.templates.hh | 20 ++++++++++---------- src/Polyhedron_public.cc | 4 ++-- tests/BD_Shape/unconstrain1.cc | 22 ++++++++++++++++++++++ tests/Box/unconstrain1.cc | 22 ++++++++++++++++++++++ tests/Grid/unconstrain1.cc | 22 ++++++++++++++++++++++ tests/Octagonal_Shape/unconstrain1.cc | 22 ++++++++++++++++++++++ tests/Polyhedron/unconstrain1.cc | 22 ++++++++++++++++++++++ 11 files changed, 142 insertions(+), 23 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ff5b0796…

1 0

PPL configuration [--enable-instanciations=c should be default]
by Basile Starynkevitch 12 Oct '10

12 Oct '10

Hello All, & specially Roberto. May I suggest a wish for next versions of PPL: always --enable-interfaces=c at least, and possibly --enable-instanciations=c also (so perhaps make that option obsolete). C++ being conceptually a superset of C, I would believe that every PPL client wants at least a C API. (and on todays computers, getting it is cheap in compilation time). While I understand that not every PPL user is using Ocaml, I would believe that each PPL user has a C compiler (usually, gcc). FWIW, GCC MELT (see http://gcc.gnu.or/wiki/MELT for more) needs the ppl_io_asprint_Polyhedron and other ppl_io_asprint_ functions from the C API of PPL), and very strangely, depending upon distributions, even with exactly the same version of PPL, this function is available with some distributions and missing in others (it might be related to the libppl-c-dev package of debian, which seems to have died.?). Alternatively, autoconf tricks (compatible with the autoconf version used by GCC 4.5.1) to test availability of ppl_io_asprint_Polyhedron are welcome. Don't forget Roberto that I am not as fluent with autoconf as you are! If you read French, more details are available on http://groups.google.com/group/gcc-melt-french/browse_thread/thread/ae12861… (or you can ask them to me, or better yet, try to build GCC MELT). Cheers. -- Basile STARYNKEVITCH http://starynkevitch.net/Basile/ email: basile<at>starynkevitch<dot>net mobile: +33 6 8501 2359 8, rue de la Faiencerie, 92340 Bourg La Reine, France *** opinions {are only mine, sont seulement les miennes} ***

2 1

[GIT] ppl/ppl(master): Documented precondition of method Bit_Matrix:: remove_trailing_columns().
by Enea Zaffanella 10 Oct '10

10 Oct '10

Module: ppl/ppl Branch: master Commit: 97150b49891b3cd74963f0e4382da44e1f9abc81 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=97150b49891b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Oct 10 17:41:52 2010 +0200 Documented precondition of method Bit_Matrix::remove_trailing_columns(). --- src/Bit_Matrix.defs.hh | 5 +++++ 1 files changed, 5 insertions(+), 0 deletions(-) diff --git a/src/Bit_Matrix.defs.hh b/src/Bit_Matrix.defs.hh index 97191ce..a1ac21f 100644 --- a/src/Bit_Matrix.defs.hh +++ b/src/Bit_Matrix.defs.hh @@ -106,6 +106,11 @@ public: void remove_trailing_rows(dimension_type n); //! Removes the last \p n columns. + /*! + \pre + The last \p n columns of the matrix are all made of zeros. + If such an assumption is not met, the behavior is undefined. + */ void remove_trailing_columns(dimension_type n); //! Resizes the matrix copying the old contents.

1 0

[GIT] ppl/ppl(master): In method Bit_Matrix::OK(), do also check the first Bit_Row.
by Enea Zaffanella 10 Oct '10

10 Oct '10

Module: ppl/ppl Branch: master Commit: 3592af215e8a58aac07e7e76a28c66246f2abc6a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3592af215e8a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Oct 10 16:34:30 2010 +0200 In method Bit_Matrix::OK(), do also check the first Bit_Row. --- src/Bit_Matrix.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Bit_Matrix.cc b/src/Bit_Matrix.cc index 54a5024..7a7a8d0 100644 --- a/src/Bit_Matrix.cc +++ b/src/Bit_Matrix.cc @@ -200,7 +200,7 @@ PPL::Bit_Matrix::OK() const { #endif const Bit_Matrix& x = *this; - for (dimension_type i = num_rows(); i-- > 1; ) { + for (dimension_type i = num_rows(); i-- > 0; ) { const Bit_Row& row = x[i]; if (!row.OK()) return false;

1 0

compiling PPL 0.11 with -flto option to GCC 4.5?
by Basile Starynkevitch 10 Oct '10

10 Oct '10

Hello All & specially Roberto Have anyone been able to compile PPL (e.g. the 0.11 release) with the link time optimization to GCC 4.5.1? I have tried to ./configure CC='gcc-4.5 -flto' CXX='g++-4.5 -flto' --enable-interfaces=c,ocaml but did not succeed. (the gcc-4.5 is from Debian/Experimental, but even with an self built gcc from FSF tarball, it seems to be the same). And -flto is passed thru CC or CXX since it is both a compile & a link time flag. It is probably not a PPL bug, but perhaps a GCC or a binutils (the gold variant) one... Cheers. -- Basile STARYNKEVITCH http://starynkevitch.net/Basile/ email: basile<at>starynkevitch<dot>net mobile: +33 6 8501 2359 8, rue de la Faiencerie, 92340 Bourg La Reine, France *** opinions {are only mine, sont seulement les miennes} ***

1 0

[GIT] ppl/ppl(floating_point): Added two FIXME notes.
by Fabio Bossi 05 Oct '10

05 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 3f052c1b8df2482f0adeb0c4627c7ede4876bc26 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3f052c1b8df2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 5 19:00:03 2010 +0200 Added two FIXME notes. --- src/linearize.hh | 8 ++++++++ 1 files changed, 8 insertions(+), 0 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 1a06b84..72e759a 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -604,6 +604,10 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, result == FP_Linear_Form(FP_Interval_Type(0)) || result == FP_Linear_Form(FP_Interval_Type(1))) /* + FIXME: find a general way to check if the casted constant + is exactly representable in the less precise format. + */ + /* We are casting to a more precise format or casting a definitely safe value: do not add errors. */ @@ -618,6 +622,10 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, result == FP_Linear_Form(FP_Interval_Type(0)) || result == FP_Linear_Form(FP_Interval_Type(1))) /* + FIXME: find a general way to check if the casted constant + is exactly representable in the less precise format. + */ + /* We are casting to a more precise format or casting a definitely safe value: do not add errors. */

1 0

[GIT] ppl/ppl(floating_point): Never add a rounding error when casting 1.
by Fabio Bossi 05 Oct '10

05 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 8c02f7d8aa8325c3771e4eb66da031d7e05c7b0b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8c02f7d8aa83… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 5 15:34:20 2010 +0200 Never add a rounding error when casting 1. --- src/linearize.hh | 14 ++++++++------ 1 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 5374a93..1a06b84 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -601,10 +601,11 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, return false; if (!is_less_precise_than(analyzed_format, cast_arg->type().floating_point_format()) || - result == FP_Linear_Form(FP_Interval_Type(0))) + result == FP_Linear_Form(FP_Interval_Type(0)) || + result == FP_Linear_Form(FP_Interval_Type(1))) /* - We are casting to a more precise format or casting the 0 value. - Do not add errors. + We are casting to a more precise format or casting + a definitely safe value: do not add errors. */ return true; } @@ -614,10 +615,11 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, return false; result = FP_Linear_Form(expr_value); if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format) || - result == FP_Linear_Form(FP_Interval_Type(0))) + result == FP_Linear_Form(FP_Interval_Type(0)) || + result == FP_Linear_Form(FP_Interval_Type(1))) /* - We are casting to a more precise format or casting the 0 value. - Do not add errors. + We are casting to a more precise format or casting + a definitely safe value: do not add errors. */ return true; }

1 0

[GIT] ppl/ppl(floating_point): Never add a rounding error when casting the 0 value.
by Fabio Bossi 05 Oct '10

05 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 500981d998d62c82210b01b5c22994e9c7ef1f4b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=500981d998d6… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 5 10:51:03 2010 +0200 Never add a rounding error when casting the 0 value. --- src/linearize.hh | 16 ++++++++++++---- 1 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 8767f80..5374a93 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -600,8 +600,12 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, if (!linearize(*cast_arg, oracle, lf_store, result)) return false; if (!is_less_precise_than(analyzed_format, - cast_arg->type().floating_point_format())) - // We are casting to a more precise format. Do not add errors. + cast_arg->type().floating_point_format()) || + result == FP_Linear_Form(FP_Interval_Type(0))) + /* + We are casting to a more precise format or casting the 0 value. + Do not add errors. + */ return true; } else { @@ -609,8 +613,12 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, if (!oracle.get_integer_expr_value(*cast_arg, expr_value)) return false; result = FP_Linear_Form(expr_value); - if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format)) - // We are rounding to a less precise format. Do not add errors. + if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format) || + result == FP_Linear_Form(FP_Interval_Type(0))) + /* + We are casting to a more precise format or casting the 0 value. + Do not add errors. + */ return true; }

1 0

[GIT] ppl/ppl(master): Sparse_Row: optimize linear_combine(), avoiding the insertion of too many elements.
by Marco Poletti 03 Oct '10

03 Oct '10

Module: ppl/ppl Branch: master Commit: 27a720c897ec87c9854374630e9846d882e86e7b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=27a720c897ec… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 3 17:13:33 2010 +0200 Sparse_Row: optimize linear_combine(), avoiding the insertion of too many elements. --- src/Sparse_Row.cc | 164 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 files changed, 163 insertions(+), 1 deletions(-) diff --git a/src/Sparse_Row.cc b/src/Sparse_Row.cc index c3c0f3f..1dec76d 100644 --- a/src/Sparse_Row.cc +++ b/src/Sparse_Row.cc @@ -232,6 +232,107 @@ PPL::Sparse_Row::normalize() { PPL_ASSERT(OK()); } +namespace { + +class sparse_row_linear_combine_helper_iterator { +public: + sparse_row_linear_combine_helper_iterator( + const PPL::Sparse_Row& x, const PPL::Sparse_Row& y, + PPL::Coefficient_traits::const_reference coeff1_1, + PPL::Coefficient_traits::const_reference coeff2_1) + : coeff1(coeff1_1), coeff2(coeff2_1) { + i = x.begin(); + i_end = x.end(); + j = y.begin(); + j_end = y.end(); + update_current_data(); + } + + void operator++() { + if (from_i) + ++i; + if (from_j) + ++j; + update_current_data(); + } + + PPL::Coefficient_traits::const_reference operator*() { + return current_value; + } + + PPL::dimension_type index() { + return current_index; + } + +private: + void update_current_data() { + if (i == i_end) { + if (j == j_end) { + return; + } else { + // i == i_end, j != j_end, so use j. + current_index = j.index(); + current_value = *j; + current_value *= coeff2; + from_i = false; + from_j = true; + } + } else { + if (j == j_end) { + // i != i_end, j == j_end, so use i. + current_index = i.index(); + current_value = *i; + current_value *= coeff1; + from_i = true; + from_j = false; + } else { + // i != i_end and j != j_end. + if (i.index() < j.index()) { + // i.index() < j.index(), so use i. + current_index = i.index(); + current_value = *i; + current_value *= coeff1; + from_i = true; + from_j = false; + } else { + if (i.index() != j.index()) { + PPL_ASSERT(i.index() > j.index()); + // i.index() > j.index(), so use j. + current_index = j.index(); + current_value = *j; + current_value *= coeff2; + from_i = false; + from_j = true; + } else { + // i.index() == j.index(), so use both i and j. + current_index = i.index(); + current_value = *i; + current_value *= coeff1; + PPL::add_mul_assign(current_value, *j, coeff2); + from_i = true; + from_j = true; + } + } + } + } + PPL_ASSERT(!from_i || i != i_end); + PPL_ASSERT(!from_j || j != j_end); + } + + PPL::Coefficient_traits::const_reference coeff1; + PPL::Coefficient_traits::const_reference coeff2; + PPL::Sparse_Row::const_iterator i; + PPL::Sparse_Row::const_iterator i_end; + PPL::Sparse_Row::const_iterator j; + PPL::Sparse_Row::const_iterator j_end; + PPL::dimension_type current_index; + PPL::Coefficient current_value; + bool from_i; + bool from_j; +}; + +} // namespace + void PPL::Sparse_Row::linear_combine(const Sparse_Row& y, Coefficient_traits::const_reference coeff1, @@ -239,7 +340,9 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, PPL_ASSERT(coeff1 != 0); PPL_ASSERT(coeff2 != 0); PPL_ASSERT(this != &y); + if (coeff1 == 1) { + // Optimize for this special case. iterator i = end(); for (const_iterator j = y.begin(), j_end = y.end(); j != j_end; ++j) { i = insert(i, j.index()); @@ -247,7 +350,45 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, if (*i == 0) i = reset(i); } - } else { + return; + } + + dimension_type counter = 0; + // Count the number of elements that are stored in y but not in *this. + { + iterator i = begin(); + iterator i_end = end(); + const_iterator j = y.begin(); + const_iterator j_end = y.end(); + if (i != i_end) { + while (j != j_end) { + PPL_ASSERT(i != i_end); + if (i.index() == j.index()) { + ++i; + ++j; + if (i == i_end) + break; + } else + if (i.index() < j.index()) { + i = lower_bound(i, j.index()); + if (i == i_end) + break; + } else { + PPL_ASSERT(i.index() > j.index()); + ++counter; + ++j; + } + } + } + PPL_ASSERT(i == i_end || j == j_end); + for ( ; j != j_end; ++j) + ++counter; + } + // This condition is arbitrary. Changing it affects performance but not + // correctness. The values have been tuned using some ppl_lpsol benchmarks + // on 2 October 2010. + if (counter == 0 || counter < 7 * size() / 64) { + // Few insertions needed, do them directly. iterator i = begin(); // This is a const reference to an internal iterator, that is kept valid. // If we just stored a copy, that would be invalidated by the calls to @@ -283,6 +424,27 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, i = insert(i, j.index(), *j); (*i) *= coeff2; } + } else { + // Too many insertions needed, a full copy is probably faster than + // inserting all those new elements into *this. + CO_Tree new_tree(sparse_row_linear_combine_helper_iterator(*this, y, + coeff1, + coeff2), + counter + tree.size()); + std::swap(tree, new_tree); + + // Now remove stored zeroes. + iterator i = begin(); + // Note that end() can not be called only once, because reset() + // invalidates all iterators. + while (i != end()) { + if (*i == 0) { + const dimension_type old_index = i.index(); + i = reset(i); + PPL_ASSERT(find(old_index) == end()); + } else + ++i; + } } }

1 0