[PPL-devel] [GIT] ppl/ppl(floating_point): Improved test01, ..., test04.

11 Dec 2009

Module: ppl/ppl
Branch: floating_point
Commit: a75d238a6bafe710454001b182151566a87e6e10
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a75d238a6bafe...
Author: Roberto Amadini r.amadini@virgilio.it
Date:   Fri Dec 11 14:26:56 2009 +0100
Improved test01, ..., test04.
---
tests/Floating_Point_Expression/digitalfilters1.cc |  130 +++++++++++---------
 1 files changed, 69 insertions(+), 61 deletions(-)

diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc
index fb841f2..e5f4fa7 100644
--- a/tests/Floating_Point_Expression/digitalfilters1.cc
+++ b/tests/Floating_Point_Expression/digitalfilters1.cc
@@ -66,6 +66,20 @@ test01() {
   FP_Interval y_begin(1);
   FP_Interval_Abstract_Store as_begin;
+  Constraint_System cs;
+  PPL_DIRTY_TEMP_COEFFICIENT(M);
+  ANALYZER_FP_FORMAT max_analyzed =
+    (2 - pow(2,
+       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
+       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
+                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
+  ANALYZER_FP_FORMAT max_analyzer =
+    std::numeric_limits<ANALYZER_FP_FORMAT>::max();
+  max_analyzer = std::min(max_analyzer, max_analyzed);
+  assign_r(M, max_analyzer, ROUND_DOWN);
+  cs.insert(Y <= M);
+  cs.insert(Y >= -M);
+
   // Y = 0;
   abstract_store.set_interval(Y, y);
   Box<FP_Interval> box(abstract_store);
@@ -111,19 +125,7 @@ test01() {
       "*** after if (R >= D)  Y = S + D; ***");
abstract_store.upper_bound_assign(as_begin);
-    Constraint_System cs;
-    PPL_DIRTY_TEMP_COEFFICIENT(M);
-    ANALYZER_FP_FORMAT max_analyzed =
-    (2 - pow(2,
-       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
-       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
-                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
-    ANALYZER_FP_FORMAT max_analyzer =
-      std::numeric_limits<ANALYZER_FP_FORMAT>::max();
-    max_analyzer = std::min(max_analyzer, max_analyzed);
-    assign_r(M, max_analyzer, ROUND_DOWN);
-    cs.insert(Y <= M);
-    cs.insert(Y >= -M);
+
     abstract_store.limited_CC76_extrapolation_assign(as_begin, cs);
     box = Box<FP_Interval>(abstract_store);
     print_constraints(box, "*** end loop ***");
@@ -155,6 +157,20 @@ test02() {
   FP_Interval y(0);
   FP_BD_Shape bd_begin;
+  Constraint_System cs;
+  PPL_DIRTY_TEMP_COEFFICIENT(M);
+  ANALYZER_FP_FORMAT max_analyzed =
+    (2 - pow(2,
+       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
+       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
+                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
+  ANALYZER_FP_FORMAT max_analyzer =
+    std::numeric_limits<ANALYZER_FP_FORMAT>::max();
+  max_analyzer = std::min(max_analyzer, max_analyzed);
+  assign_r(M, max_analyzer, ROUND_DOWN);
+  cs.insert(Y <= M);
+  cs.insert(Y >= -M);
+
   // Y = 0;
   bd.affine_image(Y, FP_Linear_Form(y));
   Box<FP_Interval> box(bd);
@@ -205,19 +221,7 @@ test02() {
          "*** after if (R >= D)  Y = S + D; ***");
bd.upper_bound_assign(bd_begin);
-    Constraint_System cs;
-    PPL_DIRTY_TEMP_COEFFICIENT(M);
-    ANALYZER_FP_FORMAT max_analyzed =
-    (2 - pow(2,
-       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
-       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
-                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
-    ANALYZER_FP_FORMAT max_analyzer =
-      std::numeric_limits<ANALYZER_FP_FORMAT>::max();
-    max_analyzer = std::min(max_analyzer, max_analyzed);
-    assign_r(M, max_analyzer, ROUND_DOWN);
-    cs.insert(Y <= M);
-    cs.insert(Y >= -M);
+
     bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs);
     box = Box<FP_Interval>(bd);
     print_constraints(box, "*** end loop ***");
@@ -249,6 +253,27 @@ test03() {
   FP_Interval y_begin(1);
   FP_Octagonal_Shape oc_begin;
+  Constraint_System cs;
+  PPL_DIRTY_TEMP_COEFFICIENT(M);
+  PPL_DIRTY_TEMP_COEFFICIENT(N);
+  ANALYZER_FP_FORMAT max_analyzed =
+    (2 - pow(2,
+       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
+       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
+                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
+  ANALYZER_FP_FORMAT max_analyzer =
+    std::numeric_limits<ANALYZER_FP_FORMAT>::max();
+  max_analyzer = std::min(max_analyzer, max_analyzed);
+  assign_r(M, max_analyzer, ROUND_DOWN);
+  div_2exp_assign_r(N, M, 1, ROUND_DOWN);
+  // FIXME: By inserting the constraints Y <= M and Y >= -M, we obtain
+  // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf.
+  // For a more precise analysis, it is better to insert the
+  // constraints Y <= N and Y >= -N, where N = M / 2.
+  // However, we could take any value of N >= 136.
+  cs.insert(Y <= N);
+  cs.insert(Y >= -N);
+
   // Y = 0;
   oc.affine_image(Y, FP_Linear_Form(y));
   Box<FP_Interval> box(oc);
@@ -297,26 +322,7 @@ test03() {
          "*** after (R >= D)  Y = S + D; ***");
oc.upper_bound_assign(oc_begin);
-    Constraint_System cs;
-    PPL_DIRTY_TEMP_COEFFICIENT(M);
-    PPL_DIRTY_TEMP_COEFFICIENT(N);
-    ANALYZER_FP_FORMAT max_analyzed =
-    (2 - pow(2,
-       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
-       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
-                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
-    ANALYZER_FP_FORMAT max_analyzer =
-      std::numeric_limits<ANALYZER_FP_FORMAT>::max();
-    max_analyzer = std::min(max_analyzer, max_analyzed);
-    assign_r(M, max_analyzer, ROUND_DOWN);
-    div_2exp_assign_r(N, M, 1, ROUND_DOWN);
-    // FIXME: By inserting the constraints Y <= M and Y >= -M, we obtain
-    // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf.
-    // For a more precise analysis, it is better to insert the
-    // constraints Y <= N and Y >= -N, where N = M / 2.
-    // However, we could take any value of N >= 136.
-    cs.insert(Y <= N);
-    cs.insert(Y >= -N);
+
     oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs);
     box = Box<FP_Interval>(oc);
     print_constraints(box, "*** end loop ***");
@@ -348,6 +354,21 @@ test04() {
   FP_Interval y_begin(1);
   NNC_Polyhedron ph_begin;
+  Constraint_System cs;
+  PPL_DIRTY_TEMP_COEFFICIENT(M);
+  ANALYZER_FP_FORMAT max_analyzed =
+    (2 - pow(2,
+    -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
+    * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
+                 - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
+  ANALYZER_FP_FORMAT max_analyzer =
+    std::numeric_limits<ANALYZER_FP_FORMAT>::max();
+  max_analyzer = std::min(max_analyzer, max_analyzed);
+  assign_r(M, max_analyzer, ROUND_DOWN);
+  // FIXME: we could take any value of M >= 128.
+  cs.insert(Y <= M);
+  cs.insert(Y >= -M);
+
   // Y = 0;
   ph.affine_image(Y, FP_Linear_Form(y));
   Box<FP_Interval> box(ph);
@@ -402,20 +423,7 @@ test04() {
          "*** after if (R >= D)  Y = S + D; ***");
ph.upper_bound_assign(ph_begin);
-    Constraint_System cs;
-    PPL_DIRTY_TEMP_COEFFICIENT(M);
-    ANALYZER_FP_FORMAT max_analyzed =
-    (2 - pow(2,
-       -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS)))
-       * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS)
-                    - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2);
-    ANALYZER_FP_FORMAT max_analyzer =
-      std::numeric_limits<ANALYZER_FP_FORMAT>::max();
-    max_analyzer = std::min(max_analyzer, max_analyzed);
-    assign_r(M, max_analyzer, ROUND_DOWN);
-    // FIXME: we could take any value of M >= 128.
-    cs.insert(Y <= M);
-    cs.insert(Y >= -M);
+
     ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs);
     box = Box<FP_Interval>(ph);
     print_constraints(box, "*** end loop ***");
@@ -601,7 +609,7 @@ test05() {
     bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs);
     abstract_store.limited_CC76_extrapolation_assign(as_begin, cs);
-    print_constraints(abstract_store,"*** end loop ***");
+    print_constraints(abstract_store, "*** end loop ***");
     y = abstract_store.get_interval(Y);
   }

    