[PPL-devel] [GIT] ppl/ppl(floating_point): Added other simple cases of affine_image.

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Fri Sep 11 17:04:11 2009 +0200

Added other simple cases of affine_image.

---

 src/Octagonal_Shape.templates.hh |   77 ++++++++++++++++++++++++++++++-------
 1 files changed, 62 insertions(+), 15 deletions(-)

diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index 0d6b04a..a36f67c 100644
--- a/src/Octagonal_Shape.templates.hh
+++ b/src/Octagonal_Shape.templates.hh
@@ -4731,26 +4731,26 @@ Octagonal_Shape<T>::affine_image(Variable var,
   //   variable;
   // - If t == 2, the `lf' is of the general form.
 
+  PPL_DIRTY_TEMP(N, b_ub);
+  assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED);
+  PPL_DIRTY_TEMP(N, b_lb);
+  assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED);
+  PPL_DIRTY_TEMP(N, b_mlb);
+  neg_assign_r(b_mlb, b_lb, ROUND_NOT_NEEDED);
+
   if (t == 0) {
     // Case 1: lf = [lb;ub];
     forget_all_octagonal_constraints(var_id);
-    PPL_DIRTY_TEMP(N, two_mlb);
-    neg_assign_r(two_mlb, b.lower(), ROUND_NOT_NEEDED);
-    mul_2exp_assign_r(two_mlb, two_mlb, 1, ROUND_UP);
+    mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP);
     PPL_DIRTY_TEMP(N, two_ub);
-    mul_2exp_assign_r(two_ub, b.upper(), 1, ROUND_UP);
+    mul_2exp_assign_r(two_ub, b_ub, 1, ROUND_UP);
     // Add the constraint `var >= lb && var <= ub'.
     add_octagonal_constraint(n_var+1, n_var, two_ub);
-    add_octagonal_constraint(n_var, n_var+1, two_mlb);
+    add_octagonal_constraint(n_var, n_var+1, b_mlb);
     PPL_ASSERT(OK());
     return;
   }
 
-  PPL_DIRTY_TEMP(N, b_ub);
-  assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED);
-  PPL_DIRTY_TEMP(N, b_lb);
-  assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED);
-
   // true if b = [0;0].
   bool is_b_zero = (b_lb == 0 && b_ub == 0);
 
@@ -4776,8 +4776,6 @@ Octagonal_Shape<T>::affine_image(Variable var,
           else {
             // Translate all the constraints on `var' by adding the value
             // `b_ub' or subtracting the value `b_lb'.
-            PPL_DIRTY_TEMP(N, b_mlb);
-            neg_assign_r(b_mlb, b_lb, ROUND_NOT_NEEDED);
             const Row_Iterator m_begin = matrix.row_begin();
             const Row_Iterator m_end = matrix.row_end();
             Row_Iterator m_iter = m_begin + n_var;
@@ -4807,16 +4805,65 @@ Octagonal_Shape<T>::affine_image(Variable var,
             mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE);
             N& m_v_cv = m_v[n_var+1];
             add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP);
+            reset_strongly_closed();
           }
-	 // FIXME: can't we put it above?
-	 reset_strongly_closed();
         }
-        // Here `w_coeff = [-1;-1].
+        else {
+          // Here `w_coeff = [-1;-1].
+          // Remove the binary constraints on `var'.
+          forget_binary_octagonal_constraints(var_id);
+          const Row_Iterator m_begin = matrix.row_begin();
+          Row_Iterator m_iter = m_begin + n_var;
+          N& m_v_cv = (*m_iter)[n_var+1];
+          ++m_iter;
+          N& m_cv_v = (*m_iter)[n_var];
+          // Swap the unary constraints on `var'.
+          std::swap(m_v_cv, m_cv_v);
+          // Strong closure is not preserved.
+          reset_strongly_closed();
+          if (b != 0) {
+            // Translate the unary constraints on `var' by adding the value
+            // `b_ub' or subtracting the value `b_lb'.
+            mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_IGNORE);
+            mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE);
+            add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP);
+            add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP);
+          }
+          incremental_strong_closure_assign(var);
+        }
       }
       else {
         // Here `w != var', so that `lf' is of the form
         // [+/-1;+/-1] * w + b.
+        // Remove all constraints on `var'.
+        forget_all_octagonal_constraints(var_id);
+        const dimension_type n_w = 2*w_id;
+        if (is_w_coeff_one)
+          // Add the new constraints `var - w >= b_lb'
+          // `and var - w <= b_ub'.
+          if (var_id < w_id) {
+            add_octagonal_constraint(n_w, n_var, b_ub);
+            add_octagonal_constraint(n_w+1, n_var+1, b_mlb);
+          }
+          else {
+            add_octagonal_constraint(n_var+1, n_w+1, b_ub);
+            add_octagonal_constraint(n_var, n_w, b_mlb);
+          }
+        else
+          // Add the new constraints `var + w >= b_lb'
+          // `and var + w <= b_ub'.
+          if (var_id < w_id) {
+            add_octagonal_constraint(n_w+1, n_var, b_ub);
+            add_octagonal_constraint(n_w, n_var+1, b_mlb);
+          }
+          else {
+            add_octagonal_constraint(n_var+1, n_w, b_ub);
+            add_octagonal_constraint(n_var, n_w+1, b_mlb);
+          }
+        incremental_strong_closure_assign(var);
       }
+      PPL_ASSERT(OK());
+      return;
     }
   }