Module: ppl/ppl Branch: master Commit: 656fbd60bb14e3304468e8016937a188ead46418 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=656fbd60bb14e... Author: Enea Zaffanella <zaffanella@cs.unipr.it> Date: Mon May 18 10:17:59 2009 +0200 First draft of Box::wrap_assign() is now operational. Added a few tests. --- src/Box.templates.hh | 82 +++++++++++++++++++++++++++++++++---------------- tests/Box/wrap1.cc | 70 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 125 insertions(+), 27 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 0561430..3f311fa 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1420,7 +1420,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, const Constraint_System* pcs, unsigned complexity_threshold, bool wrap_individually) { -#if 1 // Generic implementation commented out. +#if 0 // Generic implementation commented out. Implementation::wrap_assign(*this, vars, w, r, o, pcs, complexity_threshold, wrap_individually, @@ -1429,66 +1429,94 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, used(wrap_individually); used(complexity_threshold); Box& x = *this; - const dimension_type space_dim = x.space_dimension(); - // Dimension-compatibility check of `*pcs', if any. - if (pcs != 0 && pcs->space_dimension() > space_dim) - throw_dimension_incompatible("wrap_assign(vars, w, s, o, pcs, ...)", *pcs); + + // Dimension-compatibility check for `*pcs', if any. + const dimension_type vars_space_dim = vars.space_dimension(); + if (pcs != 0 && pcs->space_dimension() > vars_space_dim) { + std::ostringstream s; + s << "PPL::Box<ITV>::wrap_assign(vars, w, r, o, pcs, ...):" + << std::endl + << "vars.space_dimension() == " << vars_space_dim + << ", pcs->space_dimension() == " << pcs->space_dimension() << "."; + throw std::invalid_argument(s.str()); + } // Wrapping no variable only requires refining with *pcs, if any. if (vars.empty()) { if (pcs != 0) - pointset.refine_with_constraints(*pcs); + refine_with_constraints(*pcs); return; } - // Dimension-compatibility check. - const dimension_type vars_space_dim = vars.space_dimension(); - if (space_dim < vars_space_dim) - throw_dimension_incompatible("wrap_assign(vs, w, s, o, ...)", - vars_space_dim); + // Dimension-compatibility check for `vars'. + const dimension_type space_dim = x.space_dimension(); + if (space_dim < vars_space_dim) { + std::ostringstream s; + s << "PPL::Box<ITV>::wrap_assign(vars, ...):" + << std::endl + << "this->space_dimension() == " << space_dim + << ", required space dimension == " << vars_space_dim << "."; + throw std::invalid_argument(s.str()); + } + // Wrapping an empty polyhedron is a no-op. if (x.is_empty()) return; - const Variables_Set::const_iterator vs_end = vars.end(); - // FIXME: temporarily (ab-) using Coefficient. // Set `min_value' and `max_value' to the minimum and maximum values // a variable of width `w' and signedness `s' can take. PPL_DIRTY_TEMP_COEFFICIENT(min_value); PPL_DIRTY_TEMP_COEFFICIENT(max_value); - if (s == UNSIGNED) { + if (r == UNSIGNED) { min_value = 0; mul_2exp_assign(max_value, Coefficient_one(), w); + --max_value; } else { - assert(s == SIGNED_2_COMPLEMENT); + assert(r == SIGNED_2_COMPLEMENT); mul_2exp_assign(max_value, Coefficient_one(), w-1); neg_assign(min_value, max_value); + --max_value; } - // FIXME: Build the quadrant interval. - I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value); - I_Constraint<Coefficient> upper = i_constraint(LESS_THAN, max_value); - PPL_DIRTY_TEMP(ITV, quadrant_itv); - quadrant_itv.build(lower, upper); + + // FIXME: Build the (integer) quadrant interval. + PPL_DIRTY_TEMP(ITV, integer_quadrant_itv); + PPL_DIRTY_TEMP(ITV, rational_quadrant_itv); + { + I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value); + I_Constraint<Coefficient> upper = i_constraint(LESS_OR_EQUAL, max_value); + integer_quadrant_itv.build(lower, upper); + // The rational quadrant is only needed if overflow is undefined. + if (o == OVERFLOW_UNDEFINED) { + ++max_value; + upper = i_constraint(LESS_THAN, max_value); + rational_quadrant_itv.build(lower, upper); + } + } + + const Variables_Set::const_iterator vs_end = vars.end(); if (pcs == 0) { // No constraint refinement is needed here. switch (o) { case OVERFLOW_WRAPS: for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) - x.seq[*i].wrap_assign(w, s, quadrant_itv); + x.seq[*i].wrap_assign(w, r, integer_quadrant_itv); + reset_empty_up_to_date(); break; case OVERFLOW_UNDEFINED: for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { ITV& x_seq_v = x.seq[*i]; - if (!quadrant_itv.contains(x_seq_v)) - x_seq_v.assign(UNIVERSE); + if (!rational_quadrant_itv.contains(x_seq_v)) { + x_seq_v.assign(integer_quadrant_itv); + } } break; case OVERFLOW_IMPOSSIBLE: for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) - x.seq[*i].intersect_assign(quadrant_itv); + x.seq[*i].intersect_assign(integer_quadrant_itv); + reset_empty_up_to_date(); break; } assert(x.OK()); @@ -1530,7 +1558,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, // Loop through the variable indexes in `vars'. for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { const dimension_type v = *i; - refinement_itv = quadrant_itv; + refinement_itv = integer_quadrant_itv; // Look for the refinement constraints for space dimension index `v'. map_type::const_iterator var_cs_map_iter = var_cs_map.find(v); if (var_cs_map_iter != var_cs_map_end) { @@ -1548,10 +1576,10 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, ITV& x_seq_v = x.seq[v]; switch (o) { case OVERFLOW_WRAPS: - x_seq_v.wrap_assign(w, s, refinement_itv); + x_seq_v.wrap_assign(w, r, refinement_itv); break; case OVERFLOW_UNDEFINED: - if (!quadrant_itv.contains(x_seq_v)) + if (!rational_quadrant_itv.contains(x_seq_v)) x_seq_v.assign(UNIVERSE); break; case OVERFLOW_IMPOSSIBLE: diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc index 0045246..6a0d1f9 100644 --- a/tests/Box/wrap1.cc +++ b/tests/Box/wrap1.cc @@ -124,10 +124,80 @@ test03() { return ok; } +bool +test04() { + Variable x(0); + TBox box1(1); + box1.add_constraint(2*x == 511); + + print_constraints(box1, "*** box ***"); + + Variables_Set vars(x); + + // Making copies before affecting box1. + TBox box2(box1); + TBox box3(box1); + + TBox good_enough_result(box1); + TBox precise_result(1, EMPTY); + + box1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + box2.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + box3.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE); + + // FIXME: Implementation can be more precise than expected. + bool ok = box1.contains(precise_result) && good_enough_result.contains(box1) + && box2.contains(precise_result) && good_enough_result.contains(box2) + && box3.contains(precise_result) && good_enough_result.contains(box3); + + print_constraints(box1, "*** box.wrap_assign(..., OVERFLOW_WRAPS) ***"); + print_constraints(box2, "*** box.wrap_assign(..., OVERFLOW_UNDEFINED) ***"); + print_constraints(box3, "*** box.wrap_assign(..., OVERFLOW_IMPOSSIBLE) ***"); + + return ok; +} + +bool +test05() { + Variable x(0); + TBox box1(1); + box1.add_constraint(2*x == 18*256 + 511); + + print_constraints(box1, "*** box ***"); + + Variables_Set vars(x); + + // Making copies before affecting box1. + TBox box2(box1); + TBox box3(box1); + + box1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + box2.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + box3.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE); + + TBox known_result1(1, EMPTY); + TBox known_result2(1); + known_result2.add_constraint(x >= 0); + known_result2.add_constraint(x <= 255); + TBox known_result3(1, EMPTY); + + bool ok = (box1 == known_result1) + && (box2 == known_result2) + && (box3 == known_result3); + + print_constraints(box1, "*** box.wrap_assign(..., OVERFLOW_WRAPS) ***"); + print_constraints(box2, "*** box.wrap_assign(..., OVERFLOW_UNDEFINED) ***"); + print_constraints(box3, "*** box.wrap_assign(..., OVERFLOW_IMPOSSIBLE) ***"); + + return ok; +} + } // namespace BEGIN_MAIN DO_TEST_F8(test01); DO_TEST_F8(test02); DO_TEST_F(test03); + DO_TEST_F8(test04); + DO_TEST_F8(test05); END_MAIN