[PPL-devel] [GIT] ppl/ppl(floating_point): Written Polyhedron:: refine_fp_interval_abstract_store.

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Tue Sep 22 11:50:35 2009 +0200

Written Polyhedron::refine_fp_interval_abstract_store.
Various other corrections.

---

 src/Octagonal_Shape.defs.hh      |    3 +-
 src/Octagonal_Shape.templates.hh |    2 +-
 src/Polyhedron.defs.hh           |   10 +++++++
 src/Polyhedron.templates.hh      |   51 ++++++++++++++++++++++++++++++++++++-
 4 files changed, 62 insertions(+), 4 deletions(-)

diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh
index 61aebe7..a893fb7 100644
--- a/src/Octagonal_Shape.defs.hh
+++ b/src/Octagonal_Shape.defs.hh
@@ -1746,7 +1746,8 @@ public:
   */
   template <typename Interval_Info>
   void refine_fp_interval_abstract_store(
-              std::map< dimension_type, Interval<T, Interval_Info> >& store);
+              std::map< dimension_type, Interval<T, Interval_Info> >& store)
+       const;
 
   //@} // Member Functions that May Modify the Dimension of the Vector Space
 
diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index f09d910..4b491bf 100644
--- a/src/Octagonal_Shape.templates.hh
+++ b/src/Octagonal_Shape.templates.hh
@@ -5426,7 +5426,7 @@ template <typename Interval_Info>
 void
 Octagonal_Shape<T>::
 refine_fp_interval_abstract_store(
-	  std::map< dimension_type, Interval<T, Interval_Info> >& store) {
+	  std::map< dimension_type, Interval<T, Interval_Info> >& store) const {
 
   // Check that T is a floating point type.
   PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact,
diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index 7ecc2cf..87ece79 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -1011,6 +1011,16 @@ public:
   const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
   const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store);
 
+  //! Refines \p store with the constraints defining \p *this.
+  /*!
+    \param store
+    The interval floating point abstract store to refine.
+  */
+  template <typename FP_Format, typename Interval_Info>
+  void refine_fp_interval_abstract_store(
+       std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store)
+       const;
+
   /*! \brief
     Computes the \ref Cylindrification "cylindrification" of \p *this with
     respect to space dimension \p var, assigning the result to \p *this.
diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh
index 7adf015..8f9be84 100644
--- a/src/Polyhedron.templates.hh
+++ b/src/Polyhedron.templates.hh
@@ -441,7 +441,6 @@ Polyhedron::convert_to_integer_expression(
   result = Linear_Expression();
 
   typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
-  typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type;
   std::vector<Coefficient> numerators(lf_dimension+1);
   std::vector<Coefficient> denominators(lf_dimension+1);
 
@@ -488,7 +487,6 @@ Polyhedron::convert_to_integer_expressions(
   res = Linear_Expression();
 
   typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
-  typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type;
   std::vector<Coefficient> numerators(lf_dimension+2);
   std::vector<Coefficient> denominators(lf_dimension+2);
 
@@ -541,6 +539,55 @@ Polyhedron::convert_to_integer_expressions(
     res_hi_coeff = Coefficient(0);
 }
 
+template <typename FP_Format, typename Interval_Info>
+void
+Polyhedron::
+refine_fp_interval_abstract_store(
+       std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store)
+       const {
+
+  // Check that FP_Format is indeed a floating point type.
+  PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
+                     "Polyhedron::refine_fp_interval_abstract_store:"
+                     " T not a floating point type.");
+
+  typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
+  typedef typename std::map<dimension_type, FP_Interval_Type>::iterator
+                   Map_Iterator;
+
+  // FIXME: there could be restrictions on Interval_Info.
+  Box<FP_Interval_Type> limits(*this);
+  PPL_DIRTY_TEMP_COEFFICIENT(numerator);
+  PPL_DIRTY_TEMP_COEFFICIENT(denominator);
+  Map_Iterator store_end = store.end();
+  for (Map_Iterator ite = store.begin(); ite != store_end; ++ite) {
+    dimension_type curr_var = ite->first;
+    PPL_ASSERT(curr_var < space_dim);
+    Variable var(curr_var);
+    Linear_Expression var_exp(var);
+    bool dummy;
+    FP_Interval_Type& curr_int = ite->second;
+    FP_Format& lb = curr_int.lower();
+    FP_Format& ub = curr_int.upper();
+    FP_Format comparison_term;
+    mpq_class tmp_rational;
+    if (limits.minimize(var_exp, numerator, denominator, dummy)) {
+      assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED);
+      assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED);
+      assign_r(comparison_term, tmp_rational, ROUND_DOWN);
+      if (comparison_term > lb)
+        lb = comparison_term;
+    }
+    if (limits.maximize(var_exp, numerator, denominator, dummy)) {
+      assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED);
+      assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED);
+      assign_r(comparison_term, tmp_rational, ROUND_UP);
+      if (comparison_term < ub)
+        ub = comparison_term;
+    }
+  }
+}
+
 template <typename C>
 void
 Polyhedron::throw_dimension_incompatible(const char* method,