[PPL-devel] [GIT] ppl/ppl(floating_point): Started the implementation of our affine_image variant.

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Fri Sep 18 14:16:25 2009 +0200

Started the implementation of our affine_image variant.

---

 src/Polyhedron.defs.hh      |    7 ++++++-
 src/Polyhedron.templates.hh |   34 +++++++++++++++++++++++++++++++++-
 src/Polyhedron_nonpublic.cc |    9 +++++++++
 3 files changed, 48 insertions(+), 2 deletions(-)

diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index 3ea0e58..ab4a7ce 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -1147,7 +1147,8 @@ public:
 
   template <typename FP_Format, typename Interval_Info>
   void affine_image(const Variable& var,
-              const Linear_Form<Interval <FP_Format, Interval_Info> >& lf);
+  const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
+  const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store);
 
   /*! \brief
     Assigns to \p *this the
@@ -2546,6 +2547,10 @@ protected:
   void throw_dimension_incompatible(const char* method,
 				    const char* cgs_name,
 				    const Congruence_System& cgs) const;
+  template <typename C>
+  void throw_dimension_incompatible(const char* method,
+				    const char* lf_name,
+				    const Linear_Form<C>& lf) const;
   void throw_dimension_incompatible(const char* method,
 				    const char* var_name,
 				    Variable var) const;
diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh
index 51c98c4..9109b83 100644
--- a/src/Polyhedron.templates.hh
+++ b/src/Polyhedron.templates.hh
@@ -299,7 +299,38 @@ Polyhedron::map_space_dimensions(const Partial_Function& pfunc) {
 template <typename FP_Format, typename Interval_Info>
 void
 Polyhedron::affine_image(const Variable& var,
-            const Linear_Form<Interval <FP_Format, Interval_Info> >& lf) {
+const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
+const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) {
+
+  // Check that FP_Format is indeed a floating point type.
+  PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
+                         "Polyhedron::overapproximate_linear_form:"
+                         " FP_Format not a floating point type.");
+
+  // Dimension compatibility checks.
+  // The dimension of lf should not be greater than the dimension of *this.
+  const dimension_type lf_space_dim = lf.space_dimension();
+  if (space_dim < lf_space_dim)
+    throw_dimension_incompatible("affine_image(v, l)", "l", lf);
+
+  // `var' should be one of the dimensions of the polyhedron.
+  const dimension_type var_id = var.id();
+  if (space_dim < var_id + 1)
+    throw_dimension_incompatible("affine_image(v, l)", var.id()+1);
+
+  PPL_ASSERT(!marked_empty());
+
+  minimize();
+  unconstrain(var);
+
+  typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
+  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
+
+  FP_Linear_Form lf_approx;
+  overapproximate_linear_form(lf, lf_space_dim, store, lf_approx);
+
+
+
 }
 
 template <typename FP_Format, typename Interval_Info>
@@ -330,6 +361,7 @@ Polyhedron::overapproximate_linear_form(
     FP_Format curr_lb = curr_coeff.lower();
     FP_Format curr_ub = curr_coeff.upper();
     if (curr_lb != 0 || curr_ub != 0) {
+      PPL_ASSERT(store.find(i) != store.end());
       FP_Interval_Type curr_addend(curr_ub - curr_lb);
       curr_addend *= aux_divisor2;
       curr_addend *= store[i];
diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc
index 1a55c5f..9dce752 100644
--- a/src/Polyhedron_nonpublic.cc
+++ b/src/Polyhedron_nonpublic.cc
@@ -25,6 +25,7 @@ site: http://www.cs.unipr.it/ppl/ . */
 
 #include "Polyhedron.defs.hh"
 #include "Scalar_Products.defs.hh"
+#include "Linear_Form.types.hh"
 #include "assert.hh"
 #include <string>
 #include <iostream>
@@ -2231,6 +2232,14 @@ PPL::Polyhedron::throw_dimension_incompatible(const char* method,
   throw_dimension_incompatible(method, cgs_name, cgs.space_dimension());
 }
 
+template <typename C>
+void
+PPL::Polyhedron::throw_dimension_incompatible(const char* method,
+					      const char* lf_name,
+					      const Linear_Form<C>& lf) const {
+  throw_dimension_incompatible(method, lf_name, lf.space_dimension());
+}
+
 void
 PPL::Polyhedron::throw_dimension_incompatible(const char* method,
 					      const char* var_name,