[PPL-devel] [GIT] ppl/ppl(floating_point): Finished writing a first version of our affine_image variant.

Fabio Bossi bossi at cs.unipr.it
Mon Sep 21 11:34:46 CEST 2009


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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Mon Sep 21 10:11:18 2009 +0200

Finished writing a first version of our affine_image variant.

---

 src/Polyhedron.templates.hh |   18 ++++++++++++++----
 1 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh
index ab61ee1..8ac2f9d 100644
--- a/src/Polyhedron.templates.hh
+++ b/src/Polyhedron.templates.hh
@@ -318,18 +318,28 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) {
   if (space_dim < var_id + 1)
     throw_dimension_incompatible("affine_image(v, l, s)", var.id()+1);
 
+  // We suppose that the analyzer will not filter an unreachable test.
   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;
 
+  // Overapproximate lf.
   FP_Linear_Form lf_approx;
   overapproximate_linear_form(lf, lf_space_dim, store, lf_approx);
 
-
+  // Normalize lf.
+  Linear_Expression lf_approx_le;
+  PPL_DIRTY_TEMP_COEFFICIENT(lo_coeff);
+  PPL_DIRTY_TEMP_COEFFICIENT(hi_coeff);
+  convert_to_integer_expressions(lf_approx, lf_space_dim, lo_coeff, hi_coeff);
+
+  // Finally, do the assignment.
+  PPL_DIRTY_TEMP_COEFFICIENT(one_coeff);
+  one_coeff = 1;
+  generalized_affine_image(var, GREATER_OR_EQUAL, lf_approx + lo_coeff,
+                           one_coeff);
+  generalized_affine_image(var, LESS_OR_EQUAL, lf_approx + hi_coeff, one_coeff);
 
 }
 




More information about the PPL-devel mailing list