[PPL-devel] [GIT] ppl/ppl(floating_point): Added missing static_casts in Linear_Form.

Fabio Bossi bossi at cs.unipr.it
Mon Sep 14 16:01:03 CEST 2009


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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Mon Sep 14 16:02:12 2009 +0200

Added missing static_casts in Linear_Form.
Fixed one bug in linear_form_upper_bound.
Added a first complete implementation of affine_image.

---

 src/Linear_Form.templates.hh     |   24 ++++++------
 src/Octagonal_Shape.defs.hh      |    1 -
 src/Octagonal_Shape.templates.hh |   71 ++++++++++++++++++++++++++++++-------
 3 files changed, 69 insertions(+), 27 deletions(-)

diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh
index 335207f..db09aaf 100644
--- a/src/Linear_Form.templates.hh
+++ b/src/Linear_Form.templates.hh
@@ -40,7 +40,7 @@ Linear_Form<C>::Linear_Form(const Variable v)
                             "space dimension.");
   vec.reserve(compute_capacity(space_dim+1, vec_type().max_size()));
   vec.resize(space_dim+1, zero);
-  vec[v.space_dimension()] = 1.0;
+  vec[v.space_dimension()] = static_cast<C>(1.0);
 }
 
 template <typename C>
@@ -57,8 +57,8 @@ Linear_Form<C>::Linear_Form(const Variable v, const Variable w)
   vec.reserve(compute_capacity(space_dim+1, vec_type().max_size()));
   vec.resize(space_dim+1, zero);
   if (v_space_dim != w_space_dim) {
-    vec[v_space_dim] = 1.0;
-    vec[w_space_dim] = -1.0;
+    vec[v_space_dim] = static_cast<C>(1.0);
+    vec[w_space_dim] = -static_cast<C>(1.0);
   }
 }
 
@@ -125,7 +125,7 @@ operator+(const Variable v, const Linear_Form<C>& f) {
   Linear_Form<C> r(f);
   if (v_space_dim > f.space_dimension())
     r.extend(v_space_dim+1);
-  r[v_space_dim] += 1.0;
+  r[v_space_dim] += static_cast<C>(1.0);
   return r;
 }
 
@@ -199,7 +199,7 @@ operator-(const Variable v, const Linear_Form<C>& f) {
     r.extend(v_space_dim+1);
   for (dimension_type i = f.size(); i-- > 0; )
     r[i].neg_assign(r[i]);
-  r[v_space_dim] += 1.0;
+  r[v_space_dim] += static_cast<C>(1.0);
   return r;
 }
 
@@ -216,7 +216,7 @@ operator-(const Linear_Form<C>& f, const Variable v) {
   Linear_Form<C> r(f);
   if (v_space_dim > f.space_dimension())
     r.extend(v_space_dim+1);
-  r[v_space_dim] -= 1.0;
+  r[v_space_dim] -= static_cast<C>(1.0);
   return r;
 }
 
@@ -266,7 +266,7 @@ operator+=(Linear_Form<C>& f, const Variable v) {
 			    "v exceeds the maximum allowed space dimension.");
   if (v_space_dim > f.space_dimension())
     f.extend(v_space_dim+1);
-  f[v_space_dim] += 1.0;
+  f[v_space_dim] += static_cast<C>(1.0);
   return f;
 }
 
@@ -294,7 +294,7 @@ operator-=(Linear_Form<C>& f, const Variable v) {
 			    "v exceeds the maximum allowed space dimension.");
   if (v_space_dim > f.space_dimension())
     f.extend(v_space_dim+1);
-  f[v_space_dim] -= 1.0;
+  f[v_space_dim] -= static_cast<C>(1.0);
   return f;
 }
 
@@ -385,18 +385,18 @@ IO_Operators::operator<<(std::ostream& s, const Linear_Form<C>& f) {
     const C& fv = f[v+1];
     if (fv != 0) {
       if (first) {
-        if (fv == -1.0)
+        if (fv == -static_cast<C>(1.0))
           s << "-";
-        else if (fv != 1.0)
+        else if (fv != static_cast<C>(1.0))
           s << fv << "*";
         first = false;
       }
       else {
-        if (fv == -1.0)
+        if (fv == -static_cast<C>(1.0))
           s << " - ";
         else {
           s << " + ";
-          if (fv != 1.0)
+          if (fv != static_cast<C>(1.0))
             s << fv << "*";
         }
       }
diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh
index 3bb7cd1..ab89bcd 100644
--- a/src/Octagonal_Shape.defs.hh
+++ b/src/Octagonal_Shape.defs.hh
@@ -1795,7 +1795,6 @@ private:
   template <typename Interval_Info>
   void linear_form_upper_bound(
 		   const Linear_Form< Interval<T, Interval_Info> >& lf,
-                   const dimension_type last_coefficient,
                    N& result) const;
 
   // FIXME: the name is questionable.
diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index 54c8e59..783fcfb 100644
--- a/src/Octagonal_Shape.templates.hh
+++ b/src/Octagonal_Shape.templates.hh
@@ -4867,22 +4867,65 @@ Octagonal_Shape<T>::affine_image(Variable var,
   // expr == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2,
   // or t == 1, expr == i*w + b, but i <> [+/-1;+/-1].
 
-  // Calculate upper bounds for lf, -lf, lf + var, lf - var,
-  // var - lf, - lf - var.
+  // In the following, strong closure will be definitely lost.
+  reset_strongly_closed();
+
+  Linear_Form<FP_Interval_Type> minus_lf(-lf);
+
   PPL_DIRTY_TEMP(N, lf_ub);
-  assign_r(lf_ub, b_ub, ROUND_NOT_NEEDED);
+  linear_form_upper_bound(lf, lf_ub);
   PPL_DIRTY_TEMP(N, minus_lf_ub);
-  assign_r(minus_lf_ub, b_mlb, ROUND_NOT_NEEDED);
+  linear_form_upper_bound(minus_lf, minus_lf_ub);
+
+  // Update unary constraints on var.
+  mul_2exp_assign_r(lf_ub, lf_ub, 1, ROUND_IGNORE);
+  assign_r(matrix[n_var+1][n_var], lf_ub, ROUND_NOT_NEEDED);
+  mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_IGNORE);
+  assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED);
+
+  // Declare temporaries outside the loop.
   PPL_DIRTY_TEMP(N, lf_plus_var_ub);
-  assign_r(lf_plus_var_ub, b_ub, ROUND_NOT_NEEDED);
   PPL_DIRTY_TEMP(N, lf_minus_var_ub);
-  assign_r(lf_minus_var_ub, b_ub, ROUND_NOT_NEEDED);
   PPL_DIRTY_TEMP(N, var_minus_lf_ub);
-  assign_r(var_minus_lf_ub, b_mlb, ROUND_NOT_NEEDED);
   PPL_DIRTY_TEMP(N, minus_lf_minus_var_ub);
-  assign_r(minus_lf_minus_var_ub, b_mlb, ROUND_NOT_NEEDED);
 
-  linear_form_upper_bound(lf, w_id, lf_ub);
+  Row_Iterator m_iter = matrix.row_begin();
+  m_iter += n_var;
+  Row_Reference var_ite = *m_iter;
+  ++m_iter;
+  Row_Reference var_cv_ite = *m_iter;
+  ++m_iter;
+  Row_Iterator m_end = matrix.row_end();
+
+  // Update binary constraints on var.
+  for (dimension_type curr_var = var_id, n_curr_var = n_var - 2;
+       curr_var-- > 0; ) {
+    Variable current(curr_var);
+    linear_form_upper_bound(lf + current, lf_plus_var_ub);
+    linear_form_upper_bound(lf - current, lf_minus_var_ub);
+    linear_form_upper_bound(minus_lf + current, var_minus_lf_ub);
+    linear_form_upper_bound(minus_lf - current, minus_lf_minus_var_ub);
+    assign_r(var_ite[n_curr_var], var_minus_lf_ub, ROUND_NOT_NEEDED);
+    assign_r(var_ite[n_curr_var+1], minus_lf_minus_var_ub, ROUND_NOT_NEEDED);
+    assign_r(var_cv_ite[n_curr_var], lf_plus_var_ub, ROUND_NOT_NEEDED);
+    assign_r(var_cv_ite[n_curr_var+1], lf_minus_var_ub, ROUND_NOT_NEEDED);
+    n_curr_var -= 2;
+  }
+  for (dimension_type curr_var = var_id+1; m_iter != m_end; ++m_iter) {
+    Row_Reference m_v_ite = *m_iter;
+    ++m_iter;
+    Row_Reference m_cv_ite = *m_iter;
+    Variable current(curr_var);
+    linear_form_upper_bound(lf + current, lf_plus_var_ub);
+    linear_form_upper_bound(lf - current, lf_minus_var_ub);
+    linear_form_upper_bound(minus_lf + current, var_minus_lf_ub);
+    linear_form_upper_bound(minus_lf - current, minus_lf_minus_var_ub);
+    assign_r(m_v_ite[n_var], lf_minus_var_ub, ROUND_NOT_NEEDED);
+    assign_r(m_v_ite[n_var+1], minus_lf_minus_var_ub, ROUND_NOT_NEEDED);
+    assign_r(m_cv_ite[n_var], lf_plus_var_ub, ROUND_NOT_NEEDED);
+    assign_r(m_cv_ite[n_var+1], var_minus_lf_ub, ROUND_NOT_NEEDED);
+    ++curr_var;
+  }
 
 }
 
@@ -4891,10 +4934,7 @@ template <typename Interval_Info>
 void
 Octagonal_Shape<T>::
 linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf,
-                        const dimension_type last_coefficient,
                         N& result) const {
-  PPL_ASSERT(last_coefficient < lf.space_dimension());
-
   /*
     FIXME: this way for checking that T is a floating point type is a bit
     unelengant.
@@ -4902,7 +4942,10 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf,
   // Check that T is a floating point type.
   PPL_ASSERT(std::numeric_limits<T>::max_exponent);
 
+  const dimension_type lf_space_dimension = lf.space_dimension();
+
   typedef Interval<T, Interval_Info> FP_Interval_Type;
+
   const FP_Interval_Type* curr_coefficient;
   PPL_DIRTY_TEMP(N, curr_lb);
   PPL_DIRTY_TEMP(N, curr_ub);
@@ -4916,9 +4959,9 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf,
 
   PPL_DIRTY_TEMP(N, negator);
 
-  assign_r(result, 0, ROUND_NOT_NEEDED);
+  assign_r(result, lf.inhomogeneous_term().upper(), ROUND_NOT_NEEDED);
 
-  for (dimension_type curr_var = 0, n_var = 0; curr_var <= last_coefficient;
+  for (dimension_type curr_var = 0, n_var = 0; curr_var < lf_space_dimension;
        ++curr_var) {
     curr_coefficient = &(lf.coefficient(Variable(curr_var)));
     assign_r(curr_lb, curr_coefficient->lower(), ROUND_NOT_NEEDED);




More information about the PPL-devel mailing list