Module: ppl/ppl Branch: master Commit: 30f456f032cf56ef3f62452a678b398d057e990c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30f456f032cf5... Author: Roberto Bagnara <bagnara@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