Module: ppl/ppl Branch: bounded_arithmetic Commit: df4d4fcfb09051070719d9348382a7e94a8dbf39 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=df4d4fcfb0905...
Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sun Apr 26 23:34:10 2009 +0200
Started the implementation of Polyhedron::wrap_assign().
---
src/Polyhedron_public.cc | 116 +++++++++++++++++++++++++++++++++++++++++---- tests/Polyhedron/wrap1.cc | 16 ++++++- 2 files changed, 121 insertions(+), 11 deletions(-)
diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index ea0b69e..bd21fa4 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -3460,16 +3460,6 @@ PPL::Polyhedron::time_elapse_assign(const Polyhedron& y) { }
void -PPL::Polyhedron::wrap_assign(const Variables_Set& vars, - Bounded_Integer_Type_Width w, - Bounded_Integer_Type_Signedness s, - Bounded_Integer_Type_Overflow o, - bool wrap_individually, - unsigned k_threshold) { - // FIXME: to be written. -} - -void PPL::Polyhedron::topological_closure_assign() { // Necessarily closed polyhedra are trivially closed. if (is_necessarily_closed()) @@ -3685,3 +3675,109 @@ PPL::IO_Operators::operator<<(std::ostream& s, const Polyhedron& ph) { s << ph.minimized_constraints(); return s; } + +void +PPL::Polyhedron::wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Signedness s, + Bounded_Integer_Type_Overflow o, + bool wrap_individually, + unsigned k_threshold) { + // Wrapping no variable is a no-op. + if (vars.empty()) + return; + + // Dimension-compatibility check. + const dimension_type min_space_dim = vars.space_dimension(); + if (space_dim < min_space_dim) + throw_dimension_incompatible("wrap_assign(vs, ...)", min_space_dim); + + // Wrapping an empty polyhedron is a no-op. + if (is_empty()) + return; + + // Bound low and bound high assignment. + 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; + } + + //std::cout << "min_value = " << min_value << std::endl; + //std::cout << "max_value = " << max_value << std::endl; + + if (wrap_individually) { + // We use this to delay conversions when this does not negatively + // affect precision. + Constraint_System full_range_bounds; + + PPL_DIRTY_TEMP_COEFFICIENT(ln); + PPL_DIRTY_TEMP_COEFFICIENT(ld); + 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) { + + const Variable x = Variable(*i); + //std::cout << "Wrapping " << x << std::endl; + + bool extremum; + + if (!minimize(x, ln, ld, extremum)) { + set_full_range: + unconstrain(x); + full_range_bounds.insert(min_value <= x); + full_range_bounds.insert(x <= max_value); + continue; + } + + if (!maximize(x, un, ud, extremum)) + goto set_full_range; + + //std::cout << "min = " << ln << "/" << ld << std::endl; + //std::cout << "max = " << un << "/" << ud << std::endl; + + div_assign_r(ln, ln, ld, ROUND_DOWN); + div_assign_r(un, un, ud, ROUND_DOWN); + ln -= min_value; + un -= min_value; + div_2exp_assign_r(ln, ln, w, ROUND_DOWN); + div_2exp_assign_r(un, un, w, ROUND_DOWN); + if (un - ln > k_threshold) + goto set_full_range; + + //std::cout << "ln = " << ln << std::endl; + //std::cout << "un = " << un << std::endl; + + Polyhedron hull(topology(), space_dimension(), EMPTY); + for ( ; ln <= un; ++ln) { + Polyhedron p(*this); + //std::cout << "p: " << p << std::endl; + mul_2exp_assign(ld, ln, w); + //std::cout << "ld = " << ld << std::endl; + p.affine_image(x, x - ld, 1); + //std::cout << "affine_image: " << p << std::endl; + p.add_constraint(min_value <= x); + p.add_constraint(x <= max_value); + hull.poly_hull_assign(p); + //std::cout << "hull: " << hull << std::endl; + } + swap(hull); + } + add_constraints(full_range_bounds); + } + else + assert(false); +} diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index dfcb77e..97298f3 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -26,7 +26,21 @@ namespace {
bool test01() { - // FIXME: to be written. + Variable x(0); + Variable y(1); + C_Polyhedron ph(2, UNIVERSE); + ph.add_constraint(x + 1024 == 8*y); + ph.add_constraint(-64 <= x); + ph.add_constraint(x <= 448); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, true, 10); + + print_constraints(ph.minimized_constraints(), "*** ph.wrap_assign(...) ***"); + bool ok = true;
return ok;