Module: ppl/ppl Branch: master Commit: 74ade8b7dbf158e7473d8375c724e4a706506267 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=74ade8b7dbf15... Author: Enea Zaffanella <zaffanella@cs.unipr.it> Date: Thu May 14 21:05:22 2009 +0200 Adapted generic implementation of wrap_assign to model the rational case. Also added a couple of tests showing problems in the current implementation. --- src/wrap_assign.hh | 15 +++++------ tests/Box/wrap1.cc | 24 ++++++++++---------- tests/Polyhedron/wrap1.cc | 54 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 73 insertions(+), 20 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 27ba7b0..8e98b82 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -68,7 +68,7 @@ wrap_assign_rec(PSET& dest, vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); p.refine_with_constraint(min_value <= x); - p.refine_with_constraint(x <= max_value); + p.refine_with_constraint(x < max_value); } dest.upper_bound_assign(p); } @@ -106,7 +106,7 @@ wrap_assign(PSET& pointset, bool wrap_individually) { const dimension_type space_dim = pointset.space_dimension(); // Dimension-compatibility check of `*pcs', if any. - if (pcs != 0 && pcs->space_dimension() != space_dim) { + if (pcs != 0 && pcs->space_dimension() > space_dim) { std::ostringstream s; // FIXME: how can we write the class name of PSET here? s << "PPL::...::wrap_assign(..., pcs, ...):" << std::endl @@ -135,18 +135,17 @@ wrap_assign(PSET& pointset, // Set `min_value' and `max_value' to the minimum and maximum values // a variable of width `w' and signedness `s' can take. + // NOTE: value is meant to range in [min_value, max_value). PPL_DIRTY_TEMP_COEFFICIENT(min_value); PPL_DIRTY_TEMP_COEFFICIENT(max_value); if (s == UNSIGNED) { min_value = 0; mul_2exp_assign(max_value, Coefficient_one(), w); - --max_value; } else { assert(s == SIGNED_2_COMPLEMENT); mul_2exp_assign(max_value, Coefficient_one(), w-1); neg_assign(min_value, max_value); - --max_value; } // If we are wrapping variables collectively, the ranges for the @@ -195,7 +194,7 @@ wrap_assign(PSET& pointset, set_full_range: pointset.unconstrain(x); full_range_bounds.insert(min_value <= x); - full_range_bounds.insert(x <= max_value); + full_range_bounds.insert(x < max_value); continue; } @@ -220,7 +219,7 @@ wrap_assign(PSET& pointset, if (first_quadrant < 0) full_range_bounds.insert(min_value <= x); if (last_quadrant > 0) - full_range_bounds.insert(x <= max_value); + full_range_bounds.insert(x < max_value); continue; } @@ -257,7 +256,7 @@ wrap_assign(PSET& pointset, const Variable& x = i->var; pointset.unconstrain(x); full_range_bounds.insert(min_value <= x); - full_range_bounds.insert(x <= max_value); + full_range_bounds.insert(x < max_value); } } } @@ -277,7 +276,7 @@ wrap_assign(PSET& pointset, if (pcs != 0) p.refine_with_constraints(*pcs); p.refine_with_constraint(min_value <= x); - p.refine_with_constraint(x <= max_value); + p.refine_with_constraint(x < max_value); hull.upper_bound_assign(p); } pointset.swap(hull); diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc index 15f7e79..f9e757f 100644 --- a/tests/Box/wrap1.cc +++ b/tests/Box/wrap1.cc @@ -41,10 +41,10 @@ test01() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); TBox known_result(2); - known_result.add_constraint(0 <= x); - known_result.add_constraint(x <= 255); - known_result.add_constraint(0 <= y); - known_result.add_constraint(y <= 255); + known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(x < 256); + known_result.refine_with_constraint(0 <= y); + known_result.refine_with_constraint(y < 256); bool ok = (box == known_result); @@ -74,10 +74,10 @@ test02() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); TBox known_result(2); - known_result.add_constraint(0 <= x); - known_result.add_constraint(x <= 255); - known_result.add_constraint(0 <= y); - known_result.add_constraint(y <= 50); + known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(x < 256); + known_result.refine_with_constraint(0 <= y); + known_result.refine_with_constraint(y <= 50); bool ok = (box == known_result); @@ -108,10 +108,10 @@ test03() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); TBox known_result(2); - known_result.add_constraint(0 <= x); - known_result.add_constraint(x <= 255); - known_result.add_constraint(0 <= y); - known_result.add_constraint(y <= 50); + known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(x < 256); + known_result.refine_with_constraint(0 <= y); + known_result.refine_with_constraint(y <= 50); bool ok = (box == known_result); diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 97beb08..c99b59c 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -431,6 +431,58 @@ test14() { return ok; } +bool +test15() { + C_Polyhedron ph(1); + print_constraints(ph, "*** ph ***"); + + Variables_Set vars; + + Variable x(0); + Constraint_System cs; + cs.insert(x == 10); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); + + C_Polyhedron known_result(1); + known_result.add_constraint(x == 10); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + +bool +test16() { + Variable x(0); + Variable y(1); + + C_Polyhedron ph(2); + ph.add_constraint(x == 256); + ph.add_constraint(y == 256 + 256 + 1); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + Constraint_System cs; + cs.insert(x + 1 == y); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); + + C_Polyhedron known_result(2); + known_result.add_constraint(x == 0); + known_result.add_constraint(y == 1); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -448,4 +500,6 @@ BEGIN_MAIN DO_TEST_F8(test12); DO_TEST_F16(test13); DO_TEST_F8(test14); + DO_TEST(test15); + DO_TEST(test16); END_MAIN