[GIT] ppl/ppl(floating_point): Added more cases for refine_linear_form_inequality.

16 Sep 2009

Module: ppl/ppl
Branch: floating_point
Commit: e492c9a5c5291b95b3abffee549174744a9c8fe3
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e492c9a5c5291...
Author: Fabio Bossi bossi@cs.unipr.it
Date:   Wed Sep 16 12:21:30 2009 +0200
Added more cases for refine_linear_form_inequality.
---
src/Octagonal_Shape.templates.hh |  188 +++++++++++++++++++++++++++++++++++++-
 1 files changed, 183 insertions(+), 5 deletions(-)

diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index 9d4e70c..08feb94 100644
--- a/src/Octagonal_Shape.templates.hh
+++ b/src/Octagonal_Shape.templates.hh
@@ -506,10 +506,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality(
   if (marked_empty())
     return;
-  /*
-    FIXME: these are not really necessary right now. They will come in
-    handy when we optimize the most common cases.
-  */
   // Number of non-zero coefficients in `left': will be set to
   // 0, 1, or 2, the latter value meaning any value greater than 1.
   dimension_type left_t = 0;
@@ -545,7 +541,189 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality(
   typedef typename OR_Matrix<N>::const_row_reference_type Row_reference;
   typedef Interval<T, Interval_Info> FP_Interval_Type;
-  // TODO: optimize the most common cases.
+  if (left_t == 0) {
+    if (right_t == 0) {
+      // The constraint involves constants only. Ignore it: it is up to
+      // the analyzer to handle it.
+      return;
+    }
+
+    if (right_t == 1) {
+      // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x.
+      // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1].
+      const FP_Interval_Type& right_w_coeff =
+	                      right.coefficient(Variable(right_w_id));
+      if (right_w_coeff == 1) {
+        const dimension_type n_right = right_w_id * 2;
+        PPL_DIRTY_TEMP(N, b_plus_minus_a_minus);
+        const FP_Interval_Type& left_a = left.inhomogeneous_term();
+        const FP_Interval_Type& right_b = right.inhomogeneous_term();
+        sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1,
+                        ROUND_IGNORE);
+        add_octagonal_constraint(n_right, n_right+1, b_plus_minus_a_minus);
+        return;
+      }
+
+      if (right_w_coeff == -1) {
+        const dimension_type n_right = right_w_id * 2;
+        PPL_DIRTY_TEMP(N, b_plus_minus_a_minus);
+        const FP_Interval_Type& left_a = left.inhomogeneous_term();
+        const FP_Interval_Type& right_b = right.inhomogeneous_term();
+        sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1,
+                        ROUND_IGNORE);
+        add_octagonal_constraint(n_right+1, n_right, b_plus_minus_a_minus);
+        return;
+      }
+    }
+  }
+  else if (left_t == 1) {
+    if (right_t == 0) {
+      // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+]
+      // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1].
+      const FP_Interval_Type& left_w_coeff =
+	                      left.coefficient(Variable(left_w_id));
+      if (left_w_coeff == 1) {
+        const dimension_type n_left = left_w_id * 2;
+        PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+        const FP_Interval_Type& left_b = left.inhomogeneous_term();
+        const FP_Interval_Type& right_a = right.inhomogeneous_term();
+        sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1,
+                        ROUND_IGNORE);
+        add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus);
+        return;
+      }
+
+      if (left_w_coeff == -1) {
+        const dimension_type n_left = left_w_id * 2;
+        PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+        const FP_Interval_Type& left_b = left.inhomogeneous_term();
+        const FP_Interval_Type& right_a = right.inhomogeneous_term();
+        sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1,
+                        ROUND_IGNORE);
+        add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus);
+        return;
+      }
+    }
+
+    if (right_t == 1) {
+      // The constraint has the form:
+      // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y.
+      // Reduce it to the constraint +/-x +/-y <= c+ - a-
+      // if [b-;b+] = +/-[1;1] and [d-;d+] = +/-[1;1].
+      const FP_Interval_Type& left_w_coeff =
+                              left.coefficient(Variable(left_w_id));
+      const FP_Interval_Type& right_w_coeff =
+	                      right.coefficient(Variable(right_w_id));
+      bool is_left_coeff_one = (left_w_coeff == 1);
+      bool is_left_coeff_minus_one = (left_w_coeff == -1);
+      bool is_right_coeff_one = (right_w_coeff == 1);
+      bool is_right_coeff_minus_one = (right_w_coeff == -1);
+      if (left_w_id == right_w_id) {
+        if (is_left_coeff_one && is_right_coeff_one ||
+            is_left_coeff_minus_one && is_right_constraint_minus_one) {
+          // Here we have an identity or a constants-only constraint.
+          return;
+        }
+        if (is_left_coeff_one && is_right_coeff_minus_one) {
+          // We fall back to a previous case
+          // (but we do not need to multiply the result by two).
+          const dimension_type n_left = left_w_id * 2;
+          PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+          const FP_Interval_Type& left_b = left.inhomogeneous_term();
+          const FP_Interval_Type& right_a = right.inhomogeneous_term();
+          sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+                       ROUND_UP);
+          add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus);
+          return;
+        }
+        if (is_left_coeff_minus_one && is_right_coeff_one) {
+          // We fall back to a previous case
+          // (but we do not need to multiply the result by two).
+          const dimension_type n_left = left_w_id * 2;
+          PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+          const FP_Interval_Type& left_b = left.inhomogeneous_term();
+          const FP_Interval_Type& right_a = right.inhomogeneous_term();
+          sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+                       ROUND_UP);
+          add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus);
+          return;
+        }
+      }
+      else if (is_left_coeff_one && is_right_coeff_one) {
+        const dimension_type n_left = left_w_id * 2;
+        const dimension_type n_right = right_w_id * 2;
+        PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+        const FP_Interval_Type& left_a = left.inhomogeneous_term();
+        const FP_Interval_Type& right_c = right.inhomogeneous_term();
+        sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+                        ROUND_IGNORE);
+        if (left_w_id < right_w_id)
+          add_octagonal_constraint(n_right, n_left, c_plus_minus_a_minus);
+        else
+          add_octagonal_constraint(n_left+1, n_right+1, c_plus_minus_a_minus);
+        return;
+      }
+      if (is_left_coeff_one && is_right_coeff_minus_one) {
+        const dimension_type n_left = left_w_id * 2;
+        const dimension_type n_right = right_w_id * 2;
+        PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+        const FP_Interval_Type& left_a = left.inhomogeneous_term();
+        const FP_Interval_Type& right_c = right.inhomogeneous_term();
+        sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+                        ROUND_IGNORE);
+        if (left_w_id < right_w_id)
+          add_octagonal_constraint(n_right+1, n_left, c_plus_minus_a_minus);
+        else
+          add_octagonal_constraint(n_left+1, n_right, c_plus_minus_a_minus);
+        return;
+      }
+      if (is_left_coeff_minus_one && is_right_coeff_one) {
+        const dimension_type n_left = left_w_id * 2;
+        const dimension_type n_right = right_w_id * 2;
+        PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+        const FP_Interval_Type& left_a = left.inhomogeneous_term();
+        const FP_Interval_Type& right_c = right.inhomogeneous_term();
+        sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+                        ROUND_IGNORE);
+        if (left_w_id < right_w_id)
+          add_octagonal_constraint(n_right, n_left+1, c_plus_minus_a_minus);
+        else
+          add_octagonal_constraint(n_left, n_right+1, c_plus_minus_a_minus);
+        return;
+      }
+      if (is_left_coeff_minus_one && is_right_coeff_minus_one) {
+        const dimension_type n_left = left_w_id * 2;
+        const dimension_type n_right = right_w_id * 2;
+        PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+        const FP_Interval_Type& left_a = left.inhomogeneous_term();
+        const FP_Interval_Type& right_c = right.inhomogeneous_term();
+        sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(),
+                     ROUND_UP);
+        mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+                        ROUND_IGNORE);
+        if (left_w_id < right_w_id)
+          add_octagonal_constraint(n_right+1, n_left+1, c_plus_minus_a_minus);
+        else
+          add_octagonal_constraint(n_left, n_right, c_plus_minus_a_minus);
+        return;
+      }
+    }
+
+  }
// General case.

    

Fabio Bossi

tags (0)

participants (1)