- PPL-devel - BUGSENG Mailman

[GIT] ppl/w3ppl(master): First steps at annoucing the release of PPL 0.11.1 .
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/w3ppl Branch: master Commit: 7d193dc29aa82f3693b8e23e6d036b5382a96b08 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=7d193dc29a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 14:44:22 2011 +0100 First steps at annoucing the release of PPL 0.11.1. --- htdocs/news.raw | 12 ++++++++++++ htdocs/ppl.raw | 30 ++++++++++++------------------ htdocs/templates/macros.tmpl | 2 +- 3 files changed, 25 insertions(+), 19 deletions(-) diff --git a/htdocs/news.raw b/htdocs/news.raw index ca741bf..135597c 100644 --- a/htdocs/news.raw +++ b/htdocs/news.raw @@ -10,6 +10,18 @@ of the Parma Polyhedra Library. <TABLE> <TR> + <TD VALIGN=TOP><TT>Feb 20, 2011</TT></TD> + <TD> + PPL 0.11.1 has been released + + This release includes several important bug fixes and performance + improvements. See the + <A HREF="Download/ftp/releases/0.11.1/NEWS">release notes</A> + for more information. + </TD> +</TR> + +<TR> <TD VALIGN=TOP><TT>Jan 24, 2011</TT></TD> <TD> BUGSENG is the new copyright holder diff --git a/htdocs/ppl.raw b/htdocs/ppl.raw index d320a75..1de2851 100644 --- a/htdocs/ppl.raw +++ b/htdocs/ppl.raw @@ -51,6 +51,18 @@ version 3</A> or any later version). <TABLE> <TR> + <TD VALIGN=TOP><TT>Feb 20, 2011</TT></TD> + <TD> + PPL 0.11.1 has been released + + This release includes several important bug fixes and performance + improvements. See the + <A HREF="Download/ftp/releases/0.11.1/NEWS">release notes</A> + for more information. + </TD> +</TR> + +<TR> <TD VALIGN=TOP><TT>Jan 24, 2011</TT></TD> <TD> BUGSENG is the new copyright holder @@ -64,24 +76,6 @@ version 3</A> or any later version). </TD> </TR> -<TR> - <TD VALIGN=TOP><TT>Nov 17, 2010</TT></TD> - <TD> - Two in one shot! - - Fabio Bossi got a Master's degree in Computer Science, with full marks - and honours and a thesis about the extensions he made to the PPL and - to the ECLAIR analyzer in order to support the correct approximation of - floating-point computations. - - Marco Poletti got a Laurea degree in Computer Science, with full marks - and honours and a thesis about his work on the sparse matrices that - are used in the MIP and PIP solvers of the PPL. - - Congratulations, Dottor2 Bossi and Dottor Poletti! - </TD> -</TR> - </TABLE> For older news items, see the <A HREF="news">complete news archive</A>. diff --git a/htdocs/templates/macros.tmpl b/htdocs/templates/macros.tmpl index c76a037..c17f2bc 100644 --- a/htdocs/templates/macros.tmpl +++ b/htdocs/templates/macros.tmpl @@ -1,4 +1,4 @@ -@PPL_VERSION=0.11@ +@PPL_VERSION=0.11.1@ @CHINA=CHINA@

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Update version.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: cbd212ba64a72eaa0401a7be07d41ca24ff3a035 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cbd212ba64a7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 11:13:37 2011 +0100 Update version. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index 8ba9bda..baab52d 100644 --- a/configure.ac +++ b/configure.ac @@ -24,7 +24,7 @@ # Process this file with Autoconf to produce a configure script. # Every other copy of the package version number gets its value from here. -AC_INIT([the Parma Polyhedra Library], [0.11.1pre8], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.11.1], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Mark ChangeLog.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: e5089616428bfc22d3921430929ae72727ba0e24 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e5089616428b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 11:13:37 2011 +0100 Mark ChangeLog. --- ChangeLog | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/ChangeLog b/ChangeLog index 351b74a..b305044 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2011-02-20 Roberto Bagnara <bagnara(a)cs.unipr.it> + * PPL 0.11.1 released. + +2011-02-20 Roberto Bagnara <bagnara(a)cs.unipr.it> + * NEWS: Added missing news items. 2010-10-19 Enea Zaffanella <zaffanella(a)cs.unipr.it>

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Mark ChangeLog.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: ab10f6c134e3a4c9cd84469bf62a626da07e97e8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ab10f6c134e3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 11:13:37 2011 +0100 Mark ChangeLog. --- Watchdog/ChangeLog | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/Watchdog/ChangeLog b/Watchdog/ChangeLog index 2ac6a76..1b78f74 100644 --- a/Watchdog/ChangeLog +++ b/Watchdog/ChangeLog @@ -1,3 +1,7 @@ +2011-02-20 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * PPL 0.11.1 released. + 2011-02-19 Roberto Bagnara <bagnara(a)cs.unipr.it> * NEWS, README, Watchdog/config.guess, Watchdog/config.sub,

1 0

[GIT] ppl/w3ppl(master): Updated.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/w3ppl Branch: master Commit: 64515a421dfe114e74f7a93c71b8ea655aea56d9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=64515a421d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 10:33:24 2011 +0100 Updated. --- bin/ppl_release | 9 ++++----- 1 files changed, 4 insertions(+), 5 deletions(-) diff --git a/bin/ppl_release b/bin/ppl_release index d47acb1..9289f54 100755 --- a/bin/ppl_release +++ b/bin/ppl_release @@ -172,8 +172,7 @@ build_tarfiles() { changedir "${WORKING_DIRECTORY}" - # The GNU Coding Standards specify that all files should - # world readable. + # The GNU Coding Standards specify that all files should be world readable. chmod -R a+r ${SOURCE_DIRECTORY} # And that all directories have mode 777. find ${SOURCE_DIRECTORY} -type d -exec chmod 777 {} \; @@ -309,18 +308,18 @@ RFC_2822_DATE=`date --rfc-2822` #GIT_SERVER="localhost" GIT_SERVER="git.cs.unipr.it" # The path to the repository on that server. -GIT_REPOSITORY="/git/ppl/ppl.git" +GIT_REPOSITORY="/ppl/ppl" # The GIT protocol to use. GIT_PROTOCOL="ssh" # The username to use when connecting to the server. -GIT_USERNAME="${USER}" +GIT_USERNAME="git" # The machine to which files will be uploaded. PPL_HOSTNAME="ftp.cs.unipr.it" # The name of the account on the machine to which files are uploaded. PPL_USERNAME="root" # The directory in which the files will be placed. -FTP_PATH="/var/ftp/pub/ppl" +FTP_PATH="/srv/ftp/pub/ppl" # The major number for the release. For release `3.0.2' this would be # `3'

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Updated.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: e89c5db4c4e5207b222d5c8b987363e2496d457e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e89c5db4c4e5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 09:00:27 2011 +0100 Updated. --- ChangeLog | 16 ++++++++++++++++ 1 files changed, 16 insertions(+), 0 deletions(-) diff --git a/ChangeLog b/ChangeLog index 5ebf786..351b74a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2011-02-20 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * NEWS: Added missing news items. + +2010-10-19 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Octagonal_Shape.templates.hh, + tests/Octagonal_Shape/affineimage1.cc: Improved precision of + Octagonal_Shape::affine_image(). The method was rather imprecise on + sign-symmetry affine transformations. Also noted that strong + reduction is preserved in that case. + +2011-02-19 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * ChangeLog, Watchdog/ChangeLog: Updated. + 2011-02-19 Roberto Bagnara <bagnara(a)cs.unipr.it> * doc/libppl.3, doc/libppl_c.3, doc/ppl-config_extra_man_text:

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Added missing news items.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: d15416304a0918debbd1c4b105c55bef039fe27e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d15416304a09… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 08:57:46 2011 +0100 Added missing news items. --- NEWS | 14 +++++++++++++- 1 files changed, 13 insertions(+), 1 deletions(-) diff --git a/NEWS b/NEWS index b908360..0adac77 100644 --- a/NEWS +++ b/NEWS @@ -10,12 +10,24 @@ Parma Polyhedra Library NEWS -- history of user-visible changes -------------------------------------------------------------------------- -NEWS for version 0.11.1 (release on February 20, 2011) +NEWS for version 0.11.1 (released on February 20, 2011) -------------------------------------------------------------------------- Bugfixes ======== +o Corrected a problem in the simplification of PIP_Problem solution trees + whereby, under specific conditions, the node merging process produced + decision nodes that did not satisfy their class invariant. + +o Corrected a precision bug in method + + Octagonal_Shape<T>::affine_image() + + whereby in the case of an invertible affine transformation implementing + a variable sign symmetry (and optional translation), the computed result + was correct but unnecessarily imprecise. + o Corrected a problem in the input method for checked integers whereby, under specific conditions, the input stream state bits were not updated. The bug was only affecting builds using checked integer coefficients.

1 0

[GIT] ppl/ppl(master): All known bugs have been fixed for PPL 0.11.1.
by Roberto Bagnara 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: master Commit: 086927949fd92366d26e8b3fc8c93b63cc661b11 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=086927949fd9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 20 08:57:04 2011 +0100 All known bugs have been fixed for PPL 0.11.1. --- NEWS | 12 ++++-------- 1 files changed, 4 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index fad8110..8979ab9 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,10 @@ o The input routine for PPL numeric datatypes has been extended to accept the ISO9899 (C99) hexadecimal floating constant syntax. +-------------------------------------------------------------------------- +NEWS for version 0.11.1 (released on February 20, 2011) +-------------------------------------------------------------------------- + Bugfixes ======== @@ -50,14 +54,6 @@ o Corrected a precision bug in method a variable sign symmetry (and optional translation), the computed result was correct but unnecessarily imprecise. - --------------------------------------------------------------------------- -NEWS for version 0.11.1 (release on February 20, 2011) --------------------------------------------------------------------------- - -Bugfixes -======== - o Corrected a problem in the input method for checked integers whereby, under specific conditions, the input stream state bits were not updated. The bug was only affecting builds using checked integer coefficients.

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Improved precision of Octagonal_Shape:: affine_image().
by Enea Zaffanella 20 Feb '11

20 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: bb7c786d2e2934405b60f476f8f5f05065f1a08d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bb7c786d2e29… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 08:15:12 2010 +0200 Improved precision of Octagonal_Shape::affine_image(). The method was rather imprecise on sign-symmetry affine transformations. Also noted that strong reduction is preserved in that case. --- src/Octagonal_Shape.templates.hh | 120 ++++++++++++++------------------- tests/Octagonal_Shape/affineimage1.cc | 24 +++++++ 2 files changed, 74 insertions(+), 70 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index d383f8d..bc1ce89 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4494,75 +4494,53 @@ Octagonal_Shape<T>::affine_image(const Variable var, // Case 2: expr = w_coeff*w + b, with w_coeff = +/- denominator. if (w_id == var_id) { // Here `expr' is of the form: +/- denominator * v + b. - if (w_coeff == denominator) { - if (b == 0) - // The transformation is the identity function. - return; - else { - // Translate all the constraints on `var' adding or - // subtracting the value `b/denominator'. - PPL_DIRTY_TEMP(N, d); - div_round_up(d, b, denominator); - PPL_DIRTY_TEMP(N, minus_d); - div_round_up(minus_d, b, minus_den); - const Row_Iterator m_begin = matrix.row_begin(); - const Row_Iterator m_end = matrix.row_end(); - Row_Iterator m_iter = m_begin + n_var; - Row_Reference m_v = *m_iter; - ++m_iter; - Row_Reference m_cv = *m_iter; - ++m_iter; - // NOTE: delay update of unary constraints on `var'. - for (dimension_type j = n_var; j-- > 0; ) { - N& m_v_j = m_v[j]; - add_assign_r(m_v_j, m_v_j, minus_d, ROUND_UP); - N& m_cv_j = m_cv[j]; - add_assign_r(m_cv_j, m_cv_j, d, ROUND_UP); - } - for ( ; m_iter != m_end; ++m_iter) { - Row_Reference m_i = *m_iter; - N& m_i_v = m_i[n_var]; - add_assign_r(m_i_v, m_i_v, d, ROUND_UP); - N& m_i_cv = m_i[n_var+1]; - add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); - } - // Now update unary constraints on var. - mul_2exp_assign_r(d, d, 1, ROUND_UP); - N& m_cv_v = m_cv[n_var]; - add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); - N& m_v_cv = m_v[n_var+1]; - add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); - } - reset_strongly_closed(); + const bool sign_symmetry = (w_coeff != denominator); + if (!sign_symmetry && b == 0) + // The transformation is the identity function. + return; + // Translate all the constraints on `var' adding or + // subtracting the value `b/denominator'. + PPL_DIRTY_TEMP(N, d); + div_round_up(d, b, denominator); + PPL_DIRTY_TEMP(N, minus_d); + div_round_up(minus_d, b, minus_den); + if (sign_symmetry) + std::swap(d, minus_d); + const Row_Iterator m_begin = matrix.row_begin(); + const Row_Iterator m_end = matrix.row_end(); + Row_Iterator m_iter = m_begin + n_var; + Row_Reference m_v = *m_iter; + ++m_iter; + Row_Reference m_cv = *m_iter; + ++m_iter; + // NOTE: delay update of unary constraints on `var'. + for (dimension_type j = n_var; j-- > 0; ) { + N& m_v_j = m_v[j]; + add_assign_r(m_v_j, m_v_j, minus_d, ROUND_UP); + N& m_cv_j = m_cv[j]; + add_assign_r(m_cv_j, m_cv_j, d, ROUND_UP); + if (sign_symmetry) + std::swap(m_v_j, m_cv_j); } - else { - // Here `w_coeff == -denominator'. - // Remove the binary constraints on `var'. - forget_binary_octagonal_constraints(var_id); - const Row_Iterator m_begin = matrix.row_begin(); - Row_Iterator m_iter = m_begin + n_var; - N& m_v_cv = (*m_iter)[n_var+1]; - ++m_iter; - N& m_cv_v = (*m_iter)[n_var]; - // Swap the unary constraints on `var'. - std::swap(m_v_cv, m_cv_v); - // Strong closure is not preserved. - reset_strongly_closed(); - if (b != 0) { - // Translate the unary constraints on `var', - // adding or subtracting the value `b/denominator'. - PPL_DIRTY_TEMP(N, d); - div_round_up(d, b, denominator); - mul_2exp_assign_r(d, d, 1, ROUND_UP); - add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); - PPL_DIRTY_TEMP(N, minus_d); - div_round_up(minus_d, b, minus_den); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); - add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); - } - incremental_strong_closure_assign(var); - } + for ( ; m_iter != m_end; ++m_iter) { + Row_Reference m_i = *m_iter; + N& m_i_v = m_i[n_var]; + add_assign_r(m_i_v, m_i_v, d, ROUND_UP); + N& m_i_cv = m_i[n_var+1]; + add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); + if (sign_symmetry) + std::swap(m_i_v, m_i_cv); + } + // Now update unary constraints on var. + mul_2exp_assign_r(d, d, 1, ROUND_UP); + N& m_cv_v = m_cv[n_var]; + add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); + mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); + N& m_v_cv = m_v[n_var+1]; + add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); + if (sign_symmetry) + std::swap(m_cv_v, m_v_cv); + // Note: strong closure is preserved. } else { // Here `w != var', so that `expr' is of the form @@ -4571,7 +4549,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, forget_all_octagonal_constraints(var_id); const dimension_type n_w = 2*w_id; // Add the new constraint `var - w = b/denominator'. - if (w_coeff == denominator) + if (w_coeff == denominator) { if (var_id < w_id) { add_octagonal_constraint(n_w, n_var, b, denominator); add_octagonal_constraint(n_w+1, n_var+1, b, minus_den); @@ -4580,7 +4558,8 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_octagonal_constraint(n_var+1, n_w+1, b, denominator); add_octagonal_constraint(n_var, n_w, b, minus_den); } - else + } + else { // Add the new constraint `var + w = b/denominator'. if (var_id < w_id) { add_octagonal_constraint(n_w+1, n_var, b, denominator); @@ -4590,6 +4569,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_octagonal_constraint(n_var+1, n_w, b, denominator); add_octagonal_constraint(n_var, n_w+1, b, minus_den); } + } incremental_strong_closure_assign(var); } PPL_ASSERT(OK()); diff --git a/tests/Octagonal_Shape/affineimage1.cc b/tests/Octagonal_Shape/affineimage1.cc index ce10277..49d0464 100644 --- a/tests/Octagonal_Shape/affineimage1.cc +++ b/tests/Octagonal_Shape/affineimage1.cc @@ -404,6 +404,7 @@ test15() { known_result.add_constraint(2*A <= -1); known_result.add_constraint(2*A >= -3); known_result.add_constraint(B >= 4); + known_result.add_constraint(2*A + 2*B >= 7); bool ok = check_result(oc, known_result); @@ -494,6 +495,28 @@ test18() { return ok; } +bool +test19() { + Variable x(0); + Variable y(1); + + TOctagonal_Shape oc1(2); + oc1.add_constraint(x + y == 0); + + print_constraints(oc1, "*** oc1 ***"); + + oc1.affine_image(x, -x); + + Octagonal_Shape<mpq_class> known_result(2); + known_result.add_constraint(x - y == 0); + + bool ok = (Octagonal_Shape<mpq_class>(oc1) == known_result); + + print_constraints(oc1, "*** oc1.affine_image(x, y) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -515,4 +538,5 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); + DO_TEST(test19); END_MAIN

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Updated.
by Roberto Bagnara 19 Feb '11

19 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 03fb66aee2dd395fff190943ef2eb10c14029fd0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=03fb66aee2dd… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 19 17:54:36 2011 +0100 Updated. --- ChangeLog | 1342 ++++++++++++++++++++++++++++++++++++++++++++++++++++ Watchdog/ChangeLog | 900 +++++++++++++++++++++++++++++++++++ 2 files changed, 2242 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=03fb66ae…

1 0