[PPL-devel] [GIT] ppl/ppl(bounded_arithmetic): Started the implementation of Polyhedron ::wrap_assign().

[Roberto Bagnara]

Module: ppl/ppl
Branch: bounded_arithmetic
Commit: df4d4fcfb09051070719d9348382a7e94a8dbf39
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=df4d4fcfb09051070719d9348382a7e94a8dbf39

Author: Roberto Bagnara <bagnara at 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;