May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Improved a few timeout and exception tests.
by Enea Zaffanella 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: f62a4633701eda94f86bfd2cb9bced1b10436a6d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f62a4633701e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat May 16 09:16:46 2009 +0200 Improved a few timeout and exception tests. Make sure an out_of_memory exception is thrown as expected even when a large amount of memory is available. Do not set timeouts out of catch constructs. --- interfaces/Prolog/tests/pl_check.pl | 54 +++++++++++++++------------------- 1 files changed, 24 insertions(+), 30 deletions(-) diff --git a/interfaces/Prolog/tests/pl_check.pl b/interfaces/Prolog/tests/pl_check.pl index 9a91609..ff16d1b 100644 --- a/interfaces/Prolog/tests/pl_check.pl +++ b/interfaces/Prolog/tests/pl_check.pl @@ -1957,38 +1957,37 @@ build_hypercube_constraints(Dim, [V|Vars], [V >= 0, V =< 1|CS]) :- % Find the dimension and constraints for % a hypercube that causes a timeout exception. -compute_timeout_hypercube(T, Dim_in, Dim_out, CS_out) :- +compute_timeout_hypercube(Hsecs, T, Dim_in, Dim_out, CS_out) :- Dim_in =< 100, clean_ppl_new_Polyhedron_from_space_dimension(T, Dim_in, universe, P), make_vars(Dim_in, Vars), build_hypercube_constraints(Dim_in, Vars, CS), ppl_timeout_exception_atom(Time_Out_Atom), - catch(add_constraints_and_get_minimized_constraints(P, CS), - Time_Out_Atom, Catch_Exception = ok), + catch((ppl_set_timeout(Hsecs), + add_constraints_and_get_minimized_constraints(P, CS)), + Time_Out_Atom, Catch_Exception = ok), + ppl_reset_timeout, (Catch_Exception == ok -> Dim_out = Dim_in, CS_out = CS ; Dim1 is Dim_in+1, ppl_delete_Polyhedron(P), - compute_timeout_hypercube(T, Dim1, Dim_out, CS_out) + compute_timeout_hypercube(Hsecs, T, Dim1, Dim_out, CS_out) ). time_out(T) :- ppl_set_timeout_exception_atom(pl_time_out), \+ ppl_timeout_exception_atom(pl_x), ppl_timeout_exception_atom(pl_time_out), - ppl_set_timeout(10), - compute_timeout_hypercube(T, 1, Dim, CS), + compute_timeout_hypercube(10, T, 1, Dim, CS), !, N1 is 1, - ppl_reset_timeout, - ppl_set_timeout_exception_atom(pl_time_out), - ppl_set_timeout(N1), - ppl_timeout_exception_atom(Time_Out_Atom), clean_ppl_new_Polyhedron_from_space_dimension(T, Dim, universe, P), - catch(add_constraints_and_get_minimized_constraints(P, CS), - Time_Out_Atom, Catch_Exception = ok), + catch((ppl_set_timeout(N1), + add_constraints_and_get_minimized_constraints(P, CS)), + pl_time_out, Catch_Exception = ok), + ppl_reset_timeout, (Catch_Exception == ok -> display_message(['while testing time_out, polyhedron with topology', T, 'timeout after', N1, ms]) @@ -2001,13 +2000,11 @@ time_out(T) :- !, ppl_delete_Polyhedron(P), N2 is 40, - ppl_reset_timeout, - ppl_set_timeout_exception_atom(pl_time_out), - ppl_set_timeout(N2), - ppl_timeout_exception_atom(Time_Out_Atom1), clean_ppl_new_Polyhedron_from_space_dimension(T, Dim, universe, Q), - catch(ppl_Polyhedron_is_universe(Q), - Time_Out_Atom1, Catch_Exception = not_ok), + catch((ppl_set_timeout(N2), + ppl_Polyhedron_is_universe(Q)), + pl_time_out, Catch_Exception = not_ok), + ppl_reset_timeout, (Catch_Exception == not_ok -> display_message(['while testing time_out, polyhedron with topology', T, 'timeout after', N2, ms]), @@ -2446,23 +2443,21 @@ exception_prolog1(N, V) :- %% TEST: Prolog_unsigned_out_of_range. %% This test accepts any one of three exceptions: -%% ppl_invalid_argument: with a 32 bit system, the number 1 << 34 is expected +%% ppl_invalid_argument: with a 32 bit system, the number 1 << 59 is expected %% to throw this Prolog exception; -%% out_of_memory: with a 64 bit system, the number 1 << 34 does not -%% throw an exception on the Prolog side, but, with -%% unbounded integers, the large number of dimensions -%% will throw a bad_alloc exception in C++; -%% ppl_overflow_error: with bounded integers, when the number is too large, -%% an overflow exception may be thrown. +%% out_of_memory: with a 64 bit system, the number 1 << 59 does not +%% throw an exception on the Prolog side, but the +%% large number of dimensions will cause a bad_alloc +%% exception in C++. %% exception_prolog(1, _) :- pl_check_prolog_flag(bounded, Y), (Y == true -> true ; - (I is 1 << 34, - must_catch(ppl_new_C_Polyhedron_from_generators([point('$VAR'(I))], _), - prolog_exception_error) + (I is 1 << 59, + must_catch(ppl_new_C_Polyhedron_from_generators([point('$VAR'(I))], _), + prolog_exception_error) ) ). @@ -2479,8 +2474,7 @@ exception_prolog(2, _) :- %% TEST: not_unsigned_integer exception_prolog(3, _) :- - must_catch(ppl_set_timeout(-1), ppl_invalid_argument). - + must_catch(ppl_set_timeout(-1), ppl_invalid_argument). %% TEST: not_unsigned_integer exception_prolog(4, _) :-

1 0

[GIT] ppl/ppl(master): test19() must fail with 8-bit coefficients.
by Roberto Bagnara 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: a169691f1a9d7bc94a5d2372aa50ec273504c504 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a169691f1a9d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 08:57:00 2009 +0200 test19() must fail with 8-bit coefficients. --- tests/Polyhedron/wrap1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index cc622ba..3695a97 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -587,5 +587,5 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); - DO_TEST(test19); + DO_TEST_F8(test19); END_MAIN

1 0

[GIT] ppl/ppl(master): These tests fails with 16 bit coefficients.
by Abramo Bagnara 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: 4b6d78c1026ca2ab659348e4286ce62a9fdf808e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4b6d78c1026c… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sat May 16 08:25:03 2009 +0200 These tests fails with 16 bit coefficients. --- tests/Box/propagateconstraints2.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Box/propagateconstraints2.cc b/tests/Box/propagateconstraints2.cc index 14978bd..a305e2a 100644 --- a/tests/Box/propagateconstraints2.cc +++ b/tests/Box/propagateconstraints2.cc @@ -444,6 +444,6 @@ bool test03() { BEGIN_MAIN DO_TEST_F32(test01); - DO_TEST_F8(test02); - DO_TEST_F8(test03); + DO_TEST_F16(test02); + DO_TEST_F16(test03); END_MAIN

1 0

[GIT] ppl/ppl(master): Item removed: no big deal.
by Roberto Bagnara 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: c6576478c6adb1d96bc9ce3d79d05f0e5cf4f988 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c6576478c6ad… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 06:54:56 2009 +0200 Item removed: no big deal. --- TODO | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) diff --git a/TODO b/TODO index 114ce6f..bae17fa 100644 --- a/TODO +++ b/TODO @@ -11,8 +11,6 @@ Enhancements for PPL 0.11 - Make all the *affine*image() methods uniform as far as the specification is concerned. - Check the use or the NOT_EQUAL Relation_Symbol everywhere. -- Get rid of ugly assign functions defined in anonymous namespace of - MIP_Problem.cc replacing it with a more general-purpose approach. - Reconsider the datatype for the units parameter in the Watchdog constructors: should we prefer an unsigned? - Intervals are best instantiated with checked numbers with @@ -23,6 +21,7 @@ Enhancements for PPL 0.11 at the time of writing): they provide features we have been looking for for years. + Commits to consider should we release PPL 0.10.3 ================================================

1 0

[GIT] ppl/ppl(master): The test fails also with 32 bit coefficients.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 2fd53aaf53c5c90259a5acce36f68c0036f5651a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fd53aaf53c5… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 21:32:37 2009 +0200 The test fails also with 32 bit coefficients. --- tests/BD_Shape/closure1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/BD_Shape/closure1.cc b/tests/BD_Shape/closure1.cc index 655b95a..49d15ca 100644 --- a/tests/BD_Shape/closure1.cc +++ b/tests/BD_Shape/closure1.cc @@ -593,7 +593,7 @@ test03() { } // namespace BEGIN_MAIN - DO_TEST_F8(test01); + DO_TEST_F32(test01); DO_TEST_MAY_OVERFLOW_IF_INEXACT(test02, TBD_Shape); DO_TEST(test03); END_MAIN

1 0

[GIT] ppl/ppl(master): FIXME resolved.
by Roberto Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 1c9efaf9e303b17f107435b665d1aaab5ad1d269 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1c9efaf9e303… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 21:08:49 2009 +0200 FIXME resolved. --- src/Octagonal_Shape.defs.hh | 6 ------ src/Octagonal_Shape.inlines.hh | 14 +++++++++++++- src/Octagonal_Shape.templates.hh | 19 +++++++++++++++++++ 3 files changed, 32 insertions(+), 7 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 08f951a..f74577b 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -297,12 +297,6 @@ bool extract_octagonal_difference(const Constraint& c, Coefficient& c_coeff, Coefficient& c_term); -#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS -//! Returns the index coherent to \p i. -/*! \relates Octagonal_Shape */ -#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -dimension_type coherent_index(dimension_type i); - } // namespace Parma_Polyhedra_Library //! An octagonal shape. diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh index b70391f..77fccd4 100644 --- a/src/Octagonal_Shape.inlines.hh +++ b/src/Octagonal_Shape.inlines.hh @@ -36,13 +36,23 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace Parma_Polyhedra_Library { -// FIXME: find the appropriate place for this. +namespace Implementation { + +namespace Octagonal_Shapes { + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! Returns the index coherent to \p i. /*! \relates Octagonal_Shape */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) inline dimension_type coherent_index(const dimension_type i) { return (i % 2 != 0) ? i-1 : i+1; } +} // namespace Octagonal_Shapes + +} // namespace Implementation + template <typename T> inline dimension_type Octagonal_Shape<T>::max_space_dimension() { @@ -345,6 +355,7 @@ inline const typename Octagonal_Shape<T>::coefficient_type& Octagonal_Shape<T>::matrix_at(const dimension_type i, const dimension_type j) const { assert(i < matrix.num_rows() && j < matrix.num_rows()); + using namespace Implementation::Octagonal_Shapes; return (j < matrix.row_size(i)) ? matrix[i][j] : matrix[coherent_index(j)][coherent_index(i)]; @@ -355,6 +366,7 @@ inline typename Octagonal_Shape<T>::coefficient_type& Octagonal_Shape<T>::matrix_at(const dimension_type i, const dimension_type j) { assert(i < matrix.num_rows() && j < matrix.num_rows()); + using namespace Implementation::Octagonal_Shapes; return (j < matrix.row_size(i)) ? matrix[i][j] : matrix[coherent_index(j)][coherent_index(i)]; diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 6a041c8..df6de2d 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -431,6 +431,7 @@ Octagonal_Shape<T>::add_constraint(const Constraint& c) { --i_iter; typename OR_Matrix<N>::row_reference_type m_ci = *i_iter; + using namespace Implementation::Octagonal_Shapes; dimension_type cj = coherent_index(j); N& m_ci_cj = m_ci[cj]; // Also compute the bound for `m_ci_cj', rounding towards plus infinity. @@ -527,6 +528,7 @@ Octagonal_Shape<T>::refine_no_check(const Constraint& c) { --i_iter; typename OR_Matrix<N>::row_reference_type m_ci = *i_iter; + using namespace Implementation::Octagonal_Shapes; dimension_type cj = coherent_index(j); N& m_ci_cj = m_ci[cj]; // Also compute the bound for `m_ci_cj', rounding towards plus infinity. @@ -645,6 +647,7 @@ Octagonal_Shape<T>::minimized_congruences() const { { const N& c_i_li = matrix[i][lead_i]; #ifndef NDEBUG + using namespace Implementation::Octagonal_Shapes; const N& c_ii_lii = matrix[i+1][coherent_index(lead_i)]; assert(is_additive_inverse(c_ii_lii, c_i_li)); #endif @@ -773,6 +776,7 @@ Octagonal_Shape<T>::is_disjoint_from(const Octagonal_Shape& y) const { PPL_DIRTY_TEMP(N, neg_y_ci_cj); for (Row_Iterator i_iter = m_begin; i_iter != m_end; ++i_iter) { + using namespace Implementation::Octagonal_Shapes; const dimension_type i = i_iter.index(); const dimension_type ci = coherent_index(i); const dimension_type rs_i = i_iter.row_size(); @@ -939,6 +943,7 @@ Octagonal_Shape<T>::is_strong_coherent() const { for (dimension_type i = num_rows; i-- > 0; ) { typename OR_Matrix<N>::const_row_iterator iter = matrix.row_begin() + i; typename OR_Matrix<N>::const_row_reference_type m_i = *iter; + using namespace Implementation::Octagonal_Shapes; const N& m_i_ci = m_i[coherent_index(i)]; for (dimension_type j = matrix.row_size(i); j-- > 0; ) // Note: on the main diagonal only PLUS_INFINITY can occur. @@ -1408,6 +1413,7 @@ Octagonal_Shape<T>::relation_with(const Constraint& c) const { else --i_iter; typename OR_Matrix<N>::const_row_reference_type m_ci = *i_iter; + using namespace Implementation::Octagonal_Shapes; const N& m_ci_cj = m_ci[coherent_index(j)]; PPL_DIRTY_TEMP_COEFFICIENT(numer); PPL_DIRTY_TEMP_COEFFICIENT(denom); @@ -1855,6 +1861,7 @@ Octagonal_Shape<T>::strong_closure_assign() const { } for (dimension_type i = 0; i < n_rows; ++i) { + using namespace Implementation::Octagonal_Shapes; const dimension_type ci = coherent_index(i); const N& vec_k_ci = vec_k[ci]; const N& vec_ck_ci = vec_ck[ci]; @@ -1918,6 +1925,7 @@ Octagonal_Shape<T>::strong_coherence_assign() { i_end = matrix.row_end(); i_iter != i_end; ++i_iter) { typename OR_Matrix<N>::row_reference_type x_i = *i_iter; const dimension_type i = i_iter.index(); + using namespace Implementation::Octagonal_Shapes; const N& x_i_ci = x_i[coherent_index(i)]; // Avoid to do unnecessary sums. if (!is_plus_infinity(x_i_ci)) @@ -2023,6 +2031,7 @@ Octagonal_Shape<T> const dimension_type rs_v = v_iter.row_size(); const dimension_type n_rows = x.matrix.num_rows(); PPL_DIRTY_TEMP(N, sum); + using namespace Implementation::Octagonal_Shapes; for (Row_Iterator k_iter = m_begin; k_iter != m_end; ++k_iter) { const dimension_type k = k_iter.index(); const dimension_type ck = coherent_index(k); @@ -2146,7 +2155,9 @@ Octagonal_Shape<T> typename OR_Matrix<N>::const_row_reference_type m_ci = (i % 2 != 0) ? *(i_iter-1) : *(i_iter+1); for (dimension_type j = 0; j < i; ++j) { + // FIXME: what is the following, commented-out for? //for (dimension_type j = i; j-- > 0; ) { + using namespace Implementation::Octagonal_Shapes; dimension_type cj = coherent_index(j); if (is_additive_inverse(m_ci[cj], m_i[j])) // Choose as successor the variable having the greatest index. @@ -2178,6 +2189,7 @@ Octagonal_Shape<T> typename OR_Matrix<N>::const_row_reference_type m_ci = (i % 2 != 0) ? *(i_iter-1) : *(i_iter+1); for (dimension_type j = 0; j < i; ++j) { + using namespace Implementation::Octagonal_Shapes; dimension_type cj = coherent_index(j); if (is_additive_inverse(m_ci[cj], m_i[j])) // Choose as leader the variable having the smaller index. @@ -2202,6 +2214,7 @@ Octagonal_Shape<T> if (!dealt_with[i]) { // The index is a leader. // Now check if it is a leader of a singular class or not. + using namespace Implementation::Octagonal_Shapes; if (next_i == coherent_index(i)) { exist_sing_class = true; sing_leader = i; @@ -2276,10 +2289,12 @@ Octagonal_Shape<T> compute_leaders(successor, no_sing_leaders, exist_sing_class, sing_leader); const dimension_type num_no_sing_leaders = no_sing_leaders.size(); + // Step 2: flag redundant constraints in `redundancy'. // Go through non-singular leaders first. for (dimension_type li = 0; li < num_no_sing_leaders; ++li) { const dimension_type i = no_sing_leaders[li]; + using namespace Implementation::Octagonal_Shapes; const dimension_type ci = coherent_index(i); typename OR_Matrix<N>::const_row_reference_type m_i = *(matrix.row_begin()+i); @@ -3111,6 +3126,7 @@ Octagonal_Shape<T> Row_reference m_ci = *i_iter; Row_Reference lo_m_ci = *lo_iter; // Select the right column of the cell. + using namespace Implementation::Octagonal_Shapes; dimension_type cj = coherent_index(j); N& lo_m_ci_cj = lo_m_ci[cj]; neg_assign(term); @@ -6234,6 +6250,7 @@ Octagonal_Shape<T>::fold_space_dimensions(const Variables_Set& vars, const dimension_type min_id = std::min(n_dest, tbf_var); const dimension_type max_id = std::max(n_dest, tbf_var); + using namespace Implementation::Octagonal_Shapes; for (dimension_type j = 0; j < min_id; ++j) { const dimension_type cj = coherent_index(j); max_assign(m_v[j], m_tbf[j]); @@ -6330,6 +6347,7 @@ Octagonal_Shape<T>::upper_bound_assign_if_exact(const Octagonal_Shape& y) { for (dimension_type i = n_rows; i-- > 0; ) { const Bit_Row& x_non_red_i = x_non_red[i]; + using namespace Implementation::Octagonal_Shapes; const dimension_type ci = coherent_index(i); const dimension_type row_size_i = OR_Matrix<N>::row_size(i); Row_Reference x_i = *(x_m_begin + i); @@ -6507,6 +6525,7 @@ Octagonal_Shape<T> for (dimension_type i = n_rows; i-- > 0; ) { const Bit_Row& tx_non_red_i = tx_non_red[i]; + using namespace Implementation::Octagonal_Shapes; const dimension_type ci = coherent_index(i); const dimension_type row_size_i = OR_Matrix<N>::row_size(i); Row_Reference tx_i = *(tx_m_begin + i);

1 0

[GIT] ppl/ppl(master): The test fails also with 32 bit coefficients.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 4496b18b54f3d42984d3103dfe5887946d6d5084 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4496b18b54f3… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 20:48:56 2009 +0200 The test fails also with 32 bit coefficients. --- tests/Box/propagateconstraints2.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Box/propagateconstraints2.cc b/tests/Box/propagateconstraints2.cc index 1d94841..14978bd 100644 --- a/tests/Box/propagateconstraints2.cc +++ b/tests/Box/propagateconstraints2.cc @@ -443,7 +443,7 @@ bool test03() { } BEGIN_MAIN - DO_TEST_F16(test01); + DO_TEST_F32(test01); DO_TEST_F8(test02); DO_TEST_F8(test03); END_MAIN

1 0

[GIT] ppl/ppl(master): Fixed the generic implementation of wrap_assign().
by Roberto Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 30f456f032cf56ef3f62452a678b398d057e990c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30f456f032cf… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 19:45:25 2009 +0200 Fixed the generic implementation of wrap_assign(). --- src/wrap_assign.hh | 129 +++++++++++++++++++++++++++++++++------------ tests/Box/wrap1.cc | 6 +-- tests/Polyhedron/wrap1.cc | 2 +- 3 files changed, 98 insertions(+), 39 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index c6c76eb..abb3327 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -48,16 +48,75 @@ typedef std::vector<Wrap_Dim_Translations> Wrap_Translations; template <typename PSET> void -wrap_assign_rec(PSET& dest, +wrap_assign_ind(PSET& pointset, + Variables_Set& vars, + Wrap_Translations::const_iterator first, + Wrap_Translations::const_iterator end, + Bounded_Integer_Type_Width w, + Coefficient_traits::const_reference min_value, + Coefficient_traits::const_reference max_value, + const Constraint_System& cs, + Coefficient& tmp1, + Coefficient& tmp2) { + const dimension_type space_dim = pointset.space_dimension(); + const dimension_type cs_space_dim = cs.space_dimension(); + for (Wrap_Translations::const_iterator i = first; i != end; ++i) { + const Wrap_Dim_Translations& wrap_dim_translations = *i; + const Variable& x = wrap_dim_translations.var; + const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant; + const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant; + Coefficient& quadrant = tmp1; + Coefficient& shift = tmp2; + PSET hull(space_dim, EMPTY); + for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) { + PSET p(pointset); + if (quadrant != 0) { + mul_2exp_assign(shift, quadrant, w); + p.affine_image(x, x - shift, 1); + } + // `x' has just been wrapped. + vars.erase(x.id()); + + // Refine `p' with all the constraints in `cs' not depending + // on variables in `vars'. + if (vars.empty()) + p.refine_with_constraints(cs); + else { + Variables_Set::const_iterator vars_end = vars.end(); + for (Constraint_System::const_iterator j = cs.begin(), + cs_end = cs.end(); j != cs_end; ++j) { + const Constraint& c = *j; + for (dimension_type d = cs_space_dim; d-- > 0; ) { + if (c.coefficient(Variable(d)) != 0 && vars.find(d) != vars_end) + goto skip; + } + // If we are here it means `c' does not depend on variables + // in `vars'. + p.refine_with_constraint(c); + + skip: + continue; + } + } + p.refine_with_constraint(min_value <= x); + p.refine_with_constraint(x <= max_value); + hull.upper_bound_assign(p); + } + pointset.swap(hull); + } +} + +template <typename PSET> +void +wrap_assign_col(PSET& dest, const PSET& src, - Variables_Set vars, - Wrap_Translations::iterator first, - Wrap_Translations::iterator end, + const Variables_Set& vars, + Wrap_Translations::const_iterator first, + Wrap_Translations::const_iterator end, Bounded_Integer_Type_Width w, Coefficient_traits::const_reference min_value, Coefficient_traits::const_reference max_value, const Constraint_System* pcs, - unsigned complexity_threshold, Coefficient& tmp1, Coefficient& tmp2) { if (first == end) { @@ -84,12 +143,12 @@ wrap_assign_rec(PSET& dest, mul_2exp_assign(shift, quadrant, w); PSET p(src); p.affine_image(x, x - shift, 1); - wrap_assign_rec(dest, p, vars, first+1, end, w, min_value, max_value, - pcs, complexity_threshold, tmp1, tmp2); + wrap_assign_col(dest, p, vars, first+1, end, w, min_value, max_value, + pcs, tmp1, tmp2); } else - wrap_assign_rec(dest, src, vars, first+1, end, w, min_value, max_value, - pcs, complexity_threshold, tmp1, tmp2); + wrap_assign_col(dest, src, vars, first+1, end, w, min_value, max_value, + pcs, tmp1, tmp2); } } } @@ -98,12 +157,12 @@ template <typename PSET> void wrap_assign(PSET& pointset, const Variables_Set& vars, - Bounded_Integer_Type_Width w, - Bounded_Integer_Type_Signedness s, - Bounded_Integer_Type_Overflow o, + const Bounded_Integer_Type_Width w, + const Bounded_Integer_Type_Signedness s, + const Bounded_Integer_Type_Overflow o, const Constraint_System* pcs, - unsigned complexity_threshold, - bool wrap_individually, + const unsigned complexity_threshold, + const bool wrap_individually, const char* class_name) { // We must have pcs->space_dimension() <= vars.space_dimension() // and vars.space_dimension() <= pointset.space_dimension(). @@ -124,7 +183,7 @@ wrap_assign(PSET& pointset, // Check that all variables upon which `*pcs' depends are in `vars'. // An assertion is violated otherwise. const Constraint_System cs = *pcs; - dimension_type cs_space_dim = cs.space_dimension(); + const dimension_type cs_space_dim = cs.space_dimension(); Variables_Set::const_iterator vars_end = vars.end(); for (Constraint_System::const_iterator i = cs.begin(), cs_end = cs.end(); i != cs_end; ++i) { @@ -179,9 +238,9 @@ wrap_assign(PSET& pointset, // immediately applied. Wrap_Translations translations; - // If we are wrapping variables collectively, dimensions subject - // to translation are added to this set. - Variables_Set translated_dimensions; + // Dimensions subject to translation are added to this set if we are + // wrapping collectively or if `pcs' is non null. + Variables_Set dimensions_to_be_translated; // This will contain a lower bound to the number of abstractions // to be joined in order to obtain the collective wrapping result. @@ -207,8 +266,6 @@ wrap_assign(PSET& pointset, PPL_DIRTY_TEMP_COEFFICIENT(un); PPL_DIRTY_TEMP_COEFFICIENT(ud); - //using namespace IO_Operators; - for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars_end; ++i) { @@ -287,7 +344,7 @@ wrap_assign(PSET& pointset, } } - if (wrap_individually) { + if (wrap_individually && pcs == 0) { Coefficient& quadrant = first_quadrant; // Temporary variable holding the shifts to be applied in order // to implement the translations. @@ -299,28 +356,34 @@ wrap_assign(PSET& pointset, mul_2exp_assign(shift, quadrant, w); p.affine_image(x, x - shift, 1); } - if (pcs != 0) - p.refine_with_constraints(*pcs); p.refine_with_constraint(min_value <= x); p.refine_with_constraint(x <= max_value); hull.upper_bound_assign(p); } pointset.swap(hull); } - else if (!collective_wrap_too_complex) - // !wrap_individually. - translated_dimensions.insert(x); + else if (wrap_individually || !collective_wrap_too_complex) { + assert(!wrap_individually || pcs != 0); + dimensions_to_be_translated.insert(x); translations .push_back(Wrap_Dim_Translations(x, first_quadrant, last_quadrant)); + } } - if (!wrap_individually && !translations.empty()) { - PSET hull(space_dim, EMPTY); - wrap_assign_rec(hull, pointset, translated_dimensions, - translations.begin(), translations.end(), - w, min_value, max_value, pcs, complexity_threshold, - ln, ld); - pointset.swap(hull); + if (!translations.empty()) { + if (wrap_individually) { + assert(pcs != 0); + wrap_assign_ind(pointset, dimensions_to_be_translated, + translations.begin(), translations.end(), + w, min_value, max_value, *pcs, ln, ld); + } + else { + PSET hull(space_dim, EMPTY); + wrap_assign_col(hull, pointset, dimensions_to_be_translated, + translations.begin(), translations.end(), + w, min_value, max_value, pcs, ln, ld); + pointset.swap(hull); + } } if (pcs != 0) diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc index d2799bc..0045246 100644 --- a/tests/Box/wrap1.cc +++ b/tests/Box/wrap1.cc @@ -44,10 +44,8 @@ test01() { TBox known_result(2); known_result.refine_with_constraint(0 <= x); known_result.refine_with_constraint(x <= 255); - // known_result.refine_with_constraint(x < 256); known_result.refine_with_constraint(0 <= y); known_result.refine_with_constraint(y <= 255); - // known_result.refine_with_constraint(y < 256); bool ok = (box == known_result); @@ -80,7 +78,6 @@ test02() { TBox known_result(2); known_result.refine_with_constraint(0 <= x); known_result.refine_with_constraint(x <= 255); - // known_result.refine_with_constraint(x < 256); known_result.refine_with_constraint(0 <= y); known_result.refine_with_constraint(y <= 50); @@ -117,7 +114,6 @@ test03() { known_result.refine_with_constraint(6 <= x); // known_result.refine_with_constraint(0 <= x); known_result.refine_with_constraint(x <= 255); - // known_result.refine_with_constraint(x < 256); known_result.refine_with_constraint(0 <= y); known_result.refine_with_constraint(y <= 50); @@ -133,5 +129,5 @@ test03() { BEGIN_MAIN DO_TEST_F8(test01); DO_TEST_F8(test02); - DO_TEST_F8(test03); + DO_TEST_F(test03); END_MAIN diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 5d7c795..cc622ba 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -587,5 +587,5 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); - DO_TEST_F(test19); + DO_TEST(test19); END_MAIN

1 0

[GIT] ppl/ppl(master): A strict relation info is required here too.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 4845f4d529daf3beb90f9d49ba188b0c5e087396 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4845f4d529da… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 18:27:01 2009 +0200 A strict relation info is required here too. --- src/math_utilities.inlines.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math_utilities.inlines.hh b/src/math_utilities.inlines.hh index b599d2b..dc06c30 100644 --- a/src/math_utilities.inlines.hh +++ b/src/math_utilities.inlines.hh @@ -92,7 +92,7 @@ template <typename T, typename Policy> inline bool is_even(const Checked_Number<T, Policy>& x) { Checked_Number<T, Policy> half_x; - return div_2exp_assign_r(half_x, x, 1, ROUND_DIRECT) == V_EQ + return div_2exp_assign_r(half_x, x, 1, ROUND_DIRECT | ROUND_STRICT_RELATION) == V_EQ && is_integer(half_x); } @@ -101,7 +101,7 @@ inline bool is_additive_inverse(const Checked_Number<T, Policy>& x, const Checked_Number<T, Policy>& y) { Checked_Number<T, Policy> negated_x; - return neg_assign_r(negated_x, x, ROUND_DIRECT) == V_EQ + return neg_assign_r(negated_x, x, ROUND_DIRECT | ROUND_STRICT_RELATION) == V_EQ && negated_x == y; }

1 0

[GIT] ppl/ppl(master): A strict relation info is required here.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: ab230a684a4d2ce0b8cc07a0cb5a6f5b586525c9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ab230a684a4d… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 18:22:02 2009 +0200 A strict relation info is required here. --- src/Octagonal_Shape.templates.hh | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 464a87a..6a041c8 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -6665,7 +6665,7 @@ IO_Operators::operator<<(std::ostream& s, const Octagonal_Shape<T>& x) { s << ", "; // If the value bound can NOT be divided by 2 exactly, // then we output the constraint `2*v_i == bound'. - if (div_2exp_assign_r(half, x_ii_i, 1, ROUND_UP) == V_EQ) + if (div_2exp_assign_r(half, x_ii_i, 1, ROUND_UP | ROUND_STRICT_RELATION) == V_EQ) s << v_i << " == " << half; else s << "2*" << v_i << " == " << x_ii_i; @@ -6680,7 +6680,7 @@ IO_Operators::operator<<(std::ostream& s, const Octagonal_Shape<T>& x) { neg_assign_r(negation, x_i_ii, ROUND_NOT_NEEDED); // If the value bound can NOT be divided by 2 exactly, // then we output the constraint `2*v_i >= negation'. - if (div_2exp_assign_r(half, negation, 1, ROUND_UP) == V_EQ) + if (div_2exp_assign_r(half, negation, 1, ROUND_UP | ROUND_STRICT_RELATION) == V_EQ) s << v_i << " >= " << half; else s << "2*" << v_i << " >= " << negation; @@ -6692,7 +6692,7 @@ IO_Operators::operator<<(std::ostream& s, const Octagonal_Shape<T>& x) { s << ", "; // If the value bound can NOT be divided by 2 exactly, // then we output the constraint `2*v_i <= bound'. - if (div_2exp_assign_r(half, x_ii_i, 1, ROUND_UP) == V_EQ) + if (div_2exp_assign_r(half, x_ii_i, 1, ROUND_UP | ROUND_STRICT_RELATION) == V_EQ) s << v_i << " <= " << half; else s << "2*" << v_i << " <= " << x_ii_i;

1 0