- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Updated list of bug fixes.
by Enea Zaffanella 19 Oct '10

19 Oct '10

Module: ppl/ppl Branch: master Commit: 91b316106e1d492b61ef2c6f73596fb9114eac3e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=91b316106e1d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 09:10:47 2010 +0200 Updated list of bug fixes. --- NEWS | 8 ++++++++ 1 files changed, 8 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index eca7a4d..fdf1630 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,14 @@ o The input routine for PPL numeric datatypes has been extended to Bugfixes ======== +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 an efficiency bug in the C language interface function ppl_Linear_Expression_add_to_coefficient().

1 0

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

19 Oct '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b250e9ec20fb… Merge: 951fdb8a9ff89a2ae59fcc1f726a2d4b05af445a 5c95fc0eab6a38442751ed16c6cfa9d538917f3f Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 08:37:09 2010 +0200 Merge branch 'master' into floating_point URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c95fc0eab6a… 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. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=78ef497331ef… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 17 08:17:46 2010 +0200 Dense_Row: remove the unused assign() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5cf4362e714d… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:18:04 2010 +0200 Sparse_Matrix: add some methods, to be fully compatible with Dense_Matrix. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=51b8b9197551… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:17:45 2010 +0200 Sparse_Row: add some methods, to be fully compatible with Dense_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d535b8db149… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:13:35 2010 +0200 CO_Tree: add a max_size() static method.

1 0

Octagonal_Shape::affine_image too imprecise?
by FABIO BOSSI 19 Oct '10

19 Oct '10

Octagonal_Shape::affine_image seems a bit too imprecise when treating assignments of the form Y = -Y + c. Here's the code involved: // 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); } This approach that discards all old binary constraints on the assigned variable looks a little too naive to me. Consider for instance this assigment sequence: X = Y; Y = -Y; The octagonal domain will not be able to deduce X + Y = 0 as I would expect. A similar problem probably exists for BD Shapes.

2 1

[GIT] ppl/ppl(master): Improved precision of Octagonal_Shape::affine_image( ).
by Enea Zaffanella 19 Oct '10

19 Oct '10

Module: ppl/ppl Branch: master Commit: 5c95fc0eab6a38442751ed16c6cfa9d538917f3f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c95fc0eab6a… 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 7f74de5..8358b85 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4493,75 +4493,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 @@ -4570,7 +4548,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); @@ -4579,7 +4557,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); @@ -4589,6 +4568,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 cdb850b..3f4e8b4 100644 --- a/tests/Octagonal_Shape/affineimage1.cc +++ b/tests/Octagonal_Shape/affineimage1.cc @@ -403,6 +403,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); @@ -493,6 +494,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 @@ -514,4 +537,5 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); + DO_TEST(test19); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug.
by Fabio Bossi 18 Oct '10

18 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 951fdb8a9ff89a2ae59fcc1f726a2d4b05af445a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=951fdb8a9ff8… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Oct 18 16:53:27 2010 +0200 Fixed a bug. --- src/BD_Shape.templates.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index b2187f2..6df152e 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4510,7 +4510,7 @@ BD_Shape<T> const N& negated_l = dbm[i+1][0]; if (!is_plus_infinity(negated_l)) { neg_assign_r(tmp, negated_l, ROUND_DOWN); - if (!dest.restrict_lower(i, negated_l.raw_value())) + if (!dest.restrict_lower(i, tmp.raw_value())) return; } }

1 0

[GIT] ppl/ppl(master): Dense_Row: remove the unused assign() method.
by Marco Poletti 17 Oct '10

17 Oct '10

Module: ppl/ppl Branch: master Commit: 78ef497331ef00e045da0428105fdfae47165cf3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=78ef497331ef… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 17 08:17:46 2010 +0200 Dense_Row: remove the unused assign() method. --- src/Dense_Row.defs.hh | 7 ------- src/Dense_Row.inlines.hh | 8 -------- 2 files changed, 0 insertions(+), 15 deletions(-) diff --git a/src/Dense_Row.defs.hh b/src/Dense_Row.defs.hh index df97808..e991de6 100644 --- a/src/Dense_Row.defs.hh +++ b/src/Dense_Row.defs.hh @@ -179,13 +179,6 @@ public: //! Swaps \p *this with \p y. void swap(Dense_Row& y); - //! Assigns the implementation of \p y to \p *this. - /*! - To be used with extra care, since it may easily cause memory leaks - or undefined behavior. - */ - void assign(Dense_Row& y); - /*! \brief Allocates memory for a default constructed Dense_Row object, setting flags to \p f and allowing for \p capacity coefficients at most. diff --git a/src/Dense_Row.inlines.hh b/src/Dense_Row.inlines.hh index e6b6f35..ca7ae9d 100644 --- a/src/Dense_Row.inlines.hh +++ b/src/Dense_Row.inlines.hh @@ -283,14 +283,6 @@ Dense_Row::swap(Dense_Row& y) { #endif } -inline void -Dense_Row::assign(Dense_Row& y) { - impl = y.impl; -#if PPL_DENSE_ROW_EXTRA_DEBUG - capacity_ = y.capacity_; -#endif -} - inline Dense_Row& Dense_Row::operator=(const Dense_Row& y) { // Copy-construct `tmp' from `y'.

1 0

[GIT] ppl/ppl(master): Sparse_Matrix: add some methods, to be fully compatible with Dense_Matrix.
by Marco Poletti 16 Oct '10

16 Oct '10

Module: ppl/ppl Branch: master Commit: 5cf4362e714d714e0595a0d8baa73101220a3dbe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5cf4362e714d… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:18:04 2010 +0200 Sparse_Matrix: add some methods, to be fully compatible with Dense_Matrix. --- src/Sparse_Matrix.cc | 17 ++++++++++ src/Sparse_Matrix.defs.hh | 73 ++++++++++++++++++++++++++++++++++++++++- src/Sparse_Matrix.inlines.hh | 30 +++++++++++++++++ 3 files changed, 118 insertions(+), 2 deletions(-) diff --git a/src/Sparse_Matrix.cc b/src/Sparse_Matrix.cc index 1061baf..339e500 100644 --- a/src/Sparse_Matrix.cc +++ b/src/Sparse_Matrix.cc @@ -170,3 +170,20 @@ PPL::Sparse_Matrix::OK() const { return false; return true; } + +bool +PPL::operator==(const Sparse_Matrix& x, const Sparse_Matrix& y) { + if (x.num_rows() != y.num_rows()) + return false; + if (x.num_columns() != y.num_columns()) + return false; + for (dimension_type i = x.num_rows(); i-- > 0; ) + if (x[i] != y[i]) + return false; + return true; +} + +bool +PPL::operator!=(const Sparse_Matrix& x, const Sparse_Matrix& y) { + return !(x == y); +} diff --git a/src/Sparse_Matrix.defs.hh b/src/Sparse_Matrix.defs.hh index 9f6c2d7..cb09eeb 100644 --- a/src/Sparse_Matrix.defs.hh +++ b/src/Sparse_Matrix.defs.hh @@ -59,6 +59,12 @@ public: typedef Sparse_Row::Flags Flags; + //! Returns the maximum number of rows of a Sparse_Matrix. + static dimension_type max_num_rows(); + + //! Returns the maximum number of columns of a Sparse_Matrix. + static dimension_type max_num_columns(); + /*! \brief Constructs a square matrix with the given size, filled with unstored zeroes. @@ -115,6 +121,17 @@ public: */ dimension_type num_columns() const; + //! Returns <CODE>true</CODE> if and only if \p *this has no rows. + /*! + \note + The unusual naming for this method is \em intentional: + we do not want it to be named \c empty because this would cause + an error prone name clash with the corresponding methods in derived + classes Constraint_System and Congruence_System (which have a + different semantics). + */ + bool has_no_rows() const; + //! Equivalent to resize(n, n, row_flags). void resize(dimension_type n, Flags row_flags = Flags()); @@ -152,6 +169,26 @@ public: void resize(dimension_type num_rows, dimension_type num_columns, Flags row_flags = Flags()); + //! Resizes the matrix without worrying about the old contents. + /*! + \param new_n_rows + The number of rows of the resized matrix; + + \param new_n_columns + The number of columns of the resized matrix. + + \param row_flags + The flags of the rows eventually added to the matrix. + + The matrix is expanded to the specified dimensions avoiding + reallocation whenever possible. + The contents of the original matrix is lost. + + This method is provided for compatibility with Dense_Matrix. + */ + void resize_no_copy(dimension_type new_n_rows, dimension_type new_n_columns, + Flags row_flags); + //! Adds \p n rows and \p m columns of zeroes to the matrix. /*! \param n @@ -206,14 +243,30 @@ public: */ void add_row(const Sparse_Row& x); + //! Adds the row \p y to the matrix. + /*! + \param y + The row to be added: it must have the same size and capacity as + \p *this. It is not declared <CODE>const</CODE> because its + data-structures will recycled to build the new matrix row. + + Turns the \f$r \times c\f$ matrix \f$M\f$ into + the \f$(r+1) \times c\f$ matrix + \f$\genfrac{(}{)}{0pt}{}{M}{y}\f$. + The matrix is expanded avoiding reallocation whenever possible. + + This method is provided for compatibility with Dense_Matrix. + */ + void add_recycled_row(Sparse_Row& y); + /*! \brief Removes from the matrix the last \p n rows. \param n The number of row that will be removed. - Provided for compatibility with Dense_Row. - It is equivalent to resize(num_rows() - n, num_columns()). + Provided for compatibility with Dense_Matrix. + It is equivalent to num_rows() - n, num_columns()). This method takes \f$O(n+k)\f$ amortized time, where k is the total number of elements stored in the removed rows and n is the number of removed @@ -422,6 +475,22 @@ void swap(Parma_Polyhedra_Library::Sparse_Matrix& x, } // namespace std +namespace Parma_Polyhedra_Library { + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! Returns <CODE>true</CODE> if and only if \p x and \p y are identical. +/*! \relates Sparse_Matrix */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +bool operator==(const Sparse_Matrix& x, const Sparse_Matrix& y); + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! Returns <CODE>true</CODE> if and only if \p x and \p y are different. +/*! \relates Sparse_Matrix */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +bool operator!=(const Sparse_Matrix& x, const Sparse_Matrix& y); + +} // namespace Parma_Polyhedra_Library + #include "Sparse_Matrix.inlines.hh" diff --git a/src/Sparse_Matrix.inlines.hh b/src/Sparse_Matrix.inlines.hh index 1feb4b4..1fb3ffa 100644 --- a/src/Sparse_Matrix.inlines.hh +++ b/src/Sparse_Matrix.inlines.hh @@ -25,6 +25,16 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace Parma_Polyhedra_Library { +inline dimension_type +Sparse_Matrix::max_num_rows() { + return std::vector<Sparse_Row>().max_size(); +} + +inline dimension_type +Sparse_Matrix::max_num_columns() { + return Sparse_Row::max_size(); +} + inline void Sparse_Matrix::swap(Sparse_Matrix& x) { std::swap(rows, x.rows); @@ -41,12 +51,25 @@ Sparse_Matrix::num_columns() const { return num_columns_; } +inline bool +Sparse_Matrix::has_no_rows() const { + return num_rows() == 0; +} + inline void Sparse_Matrix::resize(dimension_type n, Flags row_flags) { resize(n, n, row_flags); } inline void +Sparse_Matrix::resize_no_copy(dimension_type new_n_rows, + dimension_type new_n_columns, + Flags row_flags) { + clear(); + resize(new_n_rows, new_n_columns, row_flags); +} + +inline void Sparse_Matrix::add_zero_rows_and_columns(dimension_type n, dimension_type m, Flags row_flags) { @@ -68,6 +91,13 @@ Sparse_Matrix::add_row(const Sparse_Row& x) { } inline void +Sparse_Matrix::add_recycled_row(Sparse_Row& x) { + add_zero_rows(1, Flags()); + rows.back().swap(x); + PPL_ASSERT(OK()); +} + +inline void Sparse_Matrix::remove_trailing_rows(dimension_type n) { resize(num_rows() - n, num_columns()); }

1 0

[GIT] ppl/ppl(master): Sparse_Row: add some methods, to be fully compatible with Dense_Row.
by Marco Poletti 16 Oct '10

16 Oct '10

Module: ppl/ppl Branch: master Commit: 51b8b9197551f04bef467a5d3522e6d60ba86ac1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=51b8b9197551… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:17:45 2010 +0200 Sparse_Row: add some methods, to be fully compatible with Dense_Row. --- src/Sparse_Row.cc | 46 +++++++++++++++++++++++++++ src/Sparse_Row.defs.hh | 75 ++++++++++++++++++++++++++++++++++++++++++--- src/Sparse_Row.inlines.hh | 34 +++++++++++++++++++- 3 files changed, 148 insertions(+), 7 deletions(-) diff --git a/src/Sparse_Row.cc b/src/Sparse_Row.cc index 1dec76d..7a7a078 100644 --- a/src/Sparse_Row.cc +++ b/src/Sparse_Row.cc @@ -503,3 +503,49 @@ PPL::Sparse_Row::OK() const { --last; return (last.index() < size_); } + +bool +PPL::Sparse_Row::OK(dimension_type /* capacity */) const { + return OK(); +} + +bool +PPL::operator==(const Sparse_Row& x, const Sparse_Row& y) { + if (x.size() != y.size()) + return false; + Sparse_Row::const_iterator i = x.begin(); + Sparse_Row::const_iterator i_end = x.end(); + Sparse_Row::const_iterator j = y.begin(); + Sparse_Row::const_iterator j_end = y.end(); + while (i != i_end && j != j_end) { + if (i.index() == j.index()) { + if (*i != *j) + return false; + ++i; + ++j; + } else { + if (i.index() < j.index()) { + if (*i != 0) + return false; + ++i; + } else { + PPL_ASSERT(i.index() > j.index()); + if (*j != 0) + return false; + ++j; + } + } + } + for ( ; i != i_end; ++i) + if (*i != 0) + return false; + for ( ; j != j_end; ++j) + if (*j != 0) + return false; + return true; +} + +bool +PPL::operator!=(const Sparse_Row& x, const Sparse_Row& y) { + return !(x == y); +} diff --git a/src/Sparse_Row.defs.hh b/src/Sparse_Row.defs.hh index 1aca6ed..dc74266 100644 --- a/src/Sparse_Row.defs.hh +++ b/src/Sparse_Row.defs.hh @@ -133,7 +133,7 @@ public: Sparse_Row& operator=(const Dense_Row& row); - //! Resizes the row to size \p n. + //! Resizes the row to size \p n and sets the flags to \p flags. /*! \param n The new size for the row. @@ -145,9 +145,9 @@ public: row and removing the trailing k elements. It takes \f$O(1)\f$ time when enlarging the row. */ - void construct(dimension_type n); + void construct(dimension_type n, Flags flags = Flags()); - //! Resizes the row to size \p n. + //! Resizes the row to size \p n and sets the flags to \p flags. /*! \param n The new size for the row. @@ -162,7 +162,8 @@ public: row and removing the trailing k elements. It takes \f$O(1)\f$ time when enlarging the row. */ - void construct(dimension_type n, dimension_type capacity); + void construct(dimension_type n, dimension_type capacity, + Flags flags = Flags()); //! Swaps *this and x. /*! @@ -198,6 +199,18 @@ public: This method, with this signature, is needed for compatibility with Dense_Row. + This method takes \f$O(1)\f$ time. + */ + void expand_within_capacity(dimension_type new_size); + + //! Resizes the row to size \p n. + /*! + \param n + The new size for the row. + + This method, with this signature, is needed for compatibility with + Dense_Row. + This method takes \f$O(k*\log^2 n)\f$ amortized time where k is the number of removed elements. */ @@ -280,6 +293,9 @@ public: */ const const_iterator& cend() const; + //! Returns the size() of the largest possible Sparse_Row. + static dimension_type max_size(); + //! Returns the flags associated with this row. const Flags& flags() const; @@ -770,10 +786,47 @@ public: */ memory_size_type external_memory_in_bytes() const; -private: + //! Returns the size in bytes of the memory managed by \p *this. + /*! + This method is provided for compatibility with Dense_Row. + + This method takes \f$O(n)\f$ time. + + \param capacity + This parameter is ignored. + */ + memory_size_type external_memory_in_bytes(dimension_type capacity) const; + + //! Returns the size in bytes of the memory managed by \p *this. + /*! + This method takes \f$O(n)\f$ time. + */ + memory_size_type total_memory_in_bytes() const; + + //! Returns the size in bytes of the memory managed by \p *this. + /*! + This method is provided for compatibility with Dense_Row. + + This method takes \f$O(n)\f$ time. + + \param capacity + This parameter is ignored. + */ + memory_size_type total_memory_in_bytes(dimension_type capacity) const; + //! Checks the invariant. bool OK() const; + //! Checks the invariant. + /*! + This method is provided for compatibility with Dense_Row. + + \param capacity + This parameter is ignored. + */ + bool OK(dimension_type capacity) const; + +private: //! The tree used to store the elements. CO_Tree tree; @@ -800,6 +853,18 @@ void swap(Parma_Polyhedra_Library::Sparse_Row& x, } // namespace std +namespace Parma_Polyhedra_Library { + +//! Returns <CODE>true</CODE> if and only if \p x and \p y are equal. +/*! \relates Sparse_Row */ +bool operator==(const Sparse_Row& x, const Sparse_Row& y); + +//! Returns <CODE>true</CODE> if and only if \p x and \p y are different. +/*! \relates Sparse_Row */ +bool operator!=(const Sparse_Row& x, const Sparse_Row& y); + +} // namespace Parma_Polyhedra_Library + #include "Sparse_Row.templates.hh" #include "Sparse_Row.inlines.hh" diff --git a/src/Sparse_Row.inlines.hh b/src/Sparse_Row.inlines.hh index ec75549..2e7a17f 100644 --- a/src/Sparse_Row.inlines.hh +++ b/src/Sparse_Row.inlines.hh @@ -55,12 +55,15 @@ Sparse_Row::Sparse_Row(const Sparse_Row& y, dimension_type sz, } inline void -Sparse_Row::construct(dimension_type sz) { +Sparse_Row::construct(dimension_type sz, Flags flags1) { + flags() = flags1; resize(sz); } inline void -Sparse_Row::construct(dimension_type sz, dimension_type /* capacity */) { +Sparse_Row::construct(dimension_type sz, dimension_type /* capacity */, + Flags flags1) { + flags() = flags1; resize(sz); } @@ -88,6 +91,13 @@ Sparse_Row::resize(dimension_type n) { inline void Sparse_Row::shrink(dimension_type n) { + PPL_ASSERT(size() >= n); + resize(n); +} + +inline void +Sparse_Row::expand_within_capacity(dimension_type n) { + PPL_ASSERT(size() <= n); resize(n); } @@ -137,6 +147,11 @@ Sparse_Row::cend() const { return tree.cend(); } +inline dimension_type +Sparse_Row::max_size() { + return CO_Tree::max_size(); +} + inline const Sparse_Row::Flags& Sparse_Row::flags() const { return flags_; @@ -345,6 +360,21 @@ Sparse_Row::external_memory_in_bytes() const { return tree.external_memory_in_bytes(); } +inline memory_size_type +Sparse_Row::external_memory_in_bytes(dimension_type /* capacity */) const { + return external_memory_in_bytes(); +} + +inline memory_size_type +Sparse_Row::total_memory_in_bytes() const { + return external_memory_in_bytes() + sizeof(*this); +} + +inline memory_size_type +Sparse_Row::total_memory_in_bytes(dimension_type /* capacity */) const { + return total_memory_in_bytes(); +} + } // namespace Parma_Polyhedra_Library

1 0

[GIT] ppl/ppl(master): CO_Tree: add a max_size() static method.
by Marco Poletti 16 Oct '10

16 Oct '10

Module: ppl/ppl Branch: master Commit: 3d535b8db149168861bfbb0b9d5880d01d14b4d0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d535b8db149… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:13:35 2010 +0200 CO_Tree: add a max_size() static method. --- src/CO_Tree.defs.hh | 3 +++ src/CO_Tree.inlines.hh | 5 +++++ 2 files changed, 8 insertions(+), 0 deletions(-) diff --git a/src/CO_Tree.defs.hh b/src/CO_Tree.defs.hh index 76ff01c..787acd6 100644 --- a/src/CO_Tree.defs.hh +++ b/src/CO_Tree.defs.hh @@ -530,6 +530,9 @@ public: */ dimension_type size() const; + //! Returns the size() of the largest possible CO_Tree. + static dimension_type max_size(); + //! Dumps the tree to stdout, for debugging purposes. void dump_tree() const; diff --git a/src/CO_Tree.inlines.hh b/src/CO_Tree.inlines.hh index de0d8f5..a6a4a88 100644 --- a/src/CO_Tree.inlines.hh +++ b/src/CO_Tree.inlines.hh @@ -96,6 +96,11 @@ CO_Tree::size() const { return size_; } +inline dimension_type +CO_Tree::max_size() { + return (-dimension_type(1))/100; +} + inline void CO_Tree::dump_tree() const { if (empty())

1 0

[GIT] ppl/ppl(ppl-0_11-branch): 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: ppl-0_11-branch Commit: 16feb94de535ec73b94e50c32d3e8ead2017a5ea URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=16feb94de535… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Oct 16 09:31:49 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 | 12 ++++++++++-- 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, 144 insertions(+), 24 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=16feb94d…

1 0