[GIT] ppl/ppl(floating_point): Modified test01, test02, test03 and test04.

4 Oct 2009

Module: ppl/ppl
Branch: floating_point
Commit: a0f084e697e6f17780d18ffa96e80a254d5e7620
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a0f084e697e6f...
Author: Roberto Amadini r.amadini@virgilio.it
Date:   Sun Oct  4 21:39:47 2009 +0200
Modified test01, test02, test03 and test04.
---
tests/Floating_Point_Expression/digitalfilters1.cc |   77 ++++++++++++++------
 1 files changed, 55 insertions(+), 22 deletions(-)

diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc
index 937e50e..27b15dc 100644
--- a/tests/Floating_Point_Expression/digitalfilters1.cc
+++ b/tests/Floating_Point_Expression/digitalfilters1.cc
@@ -21,6 +21,7 @@ For the most up-to-date information see the Parma Polyhedra Library
 site: http://www.cs.unipr.it/ppl/ . */
#include "ppl_test.hh"
+#include <limits>
namespace {
@@ -73,7 +74,7 @@ test01() {
     nout << "*** n = " << n << " ***" << endl;
     as_begin = abstract_store;
-    //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
+    // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
     tmp.lower() = -128;
     tmp.upper() = 128;
     abstract_store.set_interval(X, tmp);
@@ -84,7 +85,7 @@ test01() {
     abstract_store.affine_image(R, X - S);
     abstract_store.affine_image(Y, X);
-    //if (R <= -D) Y = S - D;
+    // if (R <= -D) Y = S - D;
     FP_Interval_Abstract_Store as_then(abstract_store);
     as_then.refine_with_constraint(R <= -D);
     as_then.affine_image(Y, S - D);
@@ -92,7 +93,7 @@ test01() {
     abstract_store.upper_bound_assign(as_then);
     print_constraints(abstract_store ,"*** if (R <= -D) Y = S - D; ***");
-    //if (R >= D)  Y = S + D;
+    // if (R >= D)  Y = S + D;
     as_then = abstract_store;
     as_then.refine_with_constraint(R >= D);
     as_then.affine_image(Y, S + D);
@@ -103,8 +104,16 @@ test01() {
     print_constraints(abstract_store ,"*** if (R >= D)  Y = S + D; ***");
abstract_store.upper_bound_assign(as_begin);
-    Constraint_System cs(abstract_store.constraints());
-    abstract_store.widening_assign(as_begin);
+    Constraint_System cs;
+    // FIXME: It's a temporary solution, waiting for a complete
+    // implementation of ANALYZED_FP_FORMAT.
+    //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max();
+    PPL_DIRTY_TEMP_COEFFICIENT(M);
+    //assign_r(M, max, ROUND_DOWN);
+    assign_r(M, 200, ROUND_DOWN);
+    cs.insert(Y <= M);
+    cs.insert(Y >= -M);
+    abstract_store.limited_CC76_extrapolation_assign(as_begin, cs);
     Box<FP_Interval> box(abstract_store);
     print_constraints(box, "*** after widening ***");
     tmp = box.get_interval(Y);
@@ -142,7 +151,7 @@ test02() {
     nout << "*** n = " << n << " ***" << endl;
     bd_begin = bd;
-    //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
+    // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
     tmp.lower() = -128;
     tmp.upper() = 128;
     bd.affine_image(X, FP_Linear_Form(tmp));
@@ -153,7 +162,7 @@ test02() {
     bd.affine_image(R, FP_Linear_Form(X - S));
     bd.affine_image(Y, FP_Linear_Form(X));
-    //if (R <= -D) Y = S - D;
+    // if (R <= -D) Y = S - D;
     FP_BD_Shape bd_then(bd);
     bd_then.refine_with_linear_form_inequality(FP_Linear_Form(R),
                                               -FP_Linear_Form(D));
@@ -165,7 +174,7 @@ test02() {
     print_constraints(Box<FP_Interval>(bd) ,
          "*** if (R <= -D) Y = S - D; ***");
-    //if (R >= D)  Y = S + D;
+    // if (R >= D)  Y = S + D;
     bd_then = bd;
     bd_then.refine_with_linear_form_inequality(FP_Linear_Form(D),
                                                FP_Linear_Form(R));
@@ -179,8 +188,16 @@ test02() {
          "*** if (R >= D)  Y = S + D; ***");
bd.upper_bound_assign(bd_begin);
-    Constraint_System cs(bd.constraints());
-    bd.widening_assign(bd_begin);
+    Constraint_System cs(abstract_store.constraints());
+    // FIXME: It's a temporary solution, waiting for a complete
+    // implementation of ANALYZED_FP_FORMAT.
+    //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max();
+    PPL_DIRTY_TEMP_COEFFICIENT(M);
+    //assign_r(M, max, ROUND_DOWN);
+    assign_r(M, 200, ROUND_DOWN);
+    cs.insert(Y <= M);
+    cs.insert(Y >= -M);
+    bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs);
     Box<FP_Interval> box(bd);
     print_constraints(box, "*** after widening ***");
     tmp = box.get_interval(Y);
@@ -255,7 +272,15 @@ test03() {
          "*** if (R >= D)  Y = S + D; ***");
oc.upper_bound_assign(oc_begin);
-    Constraint_System cs(oc.constraints());
+    Constraint_System cs(abstract_store.constraints());
+    // FIXME: It's a temporary solution, waiting for a complete
+    // implementation of ANALYZED_FP_FORMAT.
+    //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max();
+    PPL_DIRTY_TEMP_COEFFICIENT(M);
+    //assign_r(M, max, ROUND_DOWN);
+    assign_r(M, 200, ROUND_DOWN);
+    cs.insert(Y <= 500);//M);
+    cs.insert(Y >= -500);//-M);
     oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs);
     Box<FP_Interval> box(oc);
     print_constraints(box, "*** after widening ***");
@@ -294,7 +319,7 @@ test04() {
     nout << "*** n = " << n << " ***" << endl;
     ph_begin = ph;
-    //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
+    // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
     tmp.lower() = -128;
     tmp.upper() = 128;
     ph.affine_image(X, FP_Linear_Form(tmp), abstract_store);
@@ -308,7 +333,7 @@ test04() {
     abstract_store = Box<FP_Interval>(ph);
     ph.affine_image(Y, FP_Linear_Form(X), abstract_store);
-    //if (R <= -D) Y = S - D;
+    // if (R <= -D) Y = S - D;
     NNC_Polyhedron ph_then(ph);
     FP_Interval_Abstract_Store as_then(abstract_store);
     ph_then.refine_with_linear_form_inequality(FP_Linear_Form(R),
@@ -324,7 +349,7 @@ test04() {
     print_constraints(Box<FP_Interval>(ph) ,
          "*** if (R <= -D) Y = S - D; ***");
-    //if (R >= D)  Y = S + D;
+    // if (R >= D)  Y = S + D;
     ph_then = ph;
     as_then = abstract_store;
     ph_then.refine_with_linear_form_inequality(FP_Linear_Form(D),
@@ -341,7 +366,15 @@ test04() {
          "*** if (R >= D)  Y = S + D; ***");
ph.upper_bound_assign(ph_begin);
-    Constraint_System cs(ph.constraints());
+    Constraint_System cs(abstract_store.constraints());
+    // FIXME: It's a temporary solution, waiting for a complete
+    // implementation of ANALYZED_FP_FORMAT.
+    //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max();
+    PPL_DIRTY_TEMP_COEFFICIENT(M);
+    //assign_r(M, max, ROUND_DOWN);
+    assign_r(M, 200, ROUND_DOWN);
+    cs.insert(Y <= M);
+    cs.insert(Y >= -M);
     ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs);
     Box<FP_Interval> box(ph);
     print_constraints(box, "*** after widening ***");
@@ -410,7 +443,7 @@ test05() {
     var_x.linearize(abstract_store, lf_abstract_store, lx);
     oc.affine_image(Y, lx);
-    //if (R <= -D) Y = S - D;
+    // if (R <= -D) Y = S - D;
     FP_Octagonal_Shape oc_then(oc);
     oc_then.refine_with_linear_form_inequality(lr, -lk);
@@ -426,7 +459,7 @@ test05() {
     print_constraints(Box<FP_Interval>(oc) ,
          "*** if (R <= -D) Y = S - D; ***");
-    //if (R >= D)  Y = S + D;
+    // if (R >= D)  Y = S + D;
     oc_then = oc;
     oc_then.refine_with_linear_form_inequality(lk, lr);
@@ -443,7 +476,7 @@ test05() {
oc.upper_bound_assign(oc_begin);
     Constraint_System cs(oc.constraints());
-    // FIXME: not sound.
+    // FIXME: Not sound, we should use ANALYZED_FP_FORMAT.
     ANALYZER_FP_FORMAT max = std::numeric_limits<ANALYZER_FP_FORMAT>::max();
     PPL_DIRTY_TEMP_COEFFICIENT(M);
     assign_r(M, max, ROUND_DOWN);
@@ -496,7 +529,7 @@ test06() {
     nout << "*** n = " << n << " ***" << endl;
     ph_begin = ph;
-    //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
+    // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
     Con_FP_Expression con_x(-128, 128);
     con_x.linearize(abstract_store, lf_abstract_store, lk);
     ph.affine_image(X, lk, abstract_store);
@@ -522,7 +555,7 @@ test06() {
     var_x.linearize(abstract_store, lf_abstract_store, lx);
     ph.affine_image(Y, lx, abstract_store);
-    //if (R <= -D) Y = S - D;
+    // if (R <= -D) Y = S - D;
     NNC_Polyhedron ph_then(ph);
     FP_Interval_Abstract_Store as_then(abstract_store);
     ph_then.refine_with_linear_form_inequality(lr, -lk, as_then);
@@ -539,7 +572,7 @@ test06() {
     print_constraints(Box<FP_Interval>(ph) ,
          "*** if (R <= -D) Y = S - D; ***");
-    //if (R >= D)  Y = S + D;
+    // if (R >= D)  Y = S + D;
     ph_then = ph;
     as_then = abstract_store;
     ph_then.refine_with_linear_form_inequality(lk, lr, as_then);
@@ -559,7 +592,7 @@ test06() {
ph.upper_bound_assign(ph_begin);
     Constraint_System cs;
-    // FIXME: not sound.
+    // FIXME: This is not sound, it should use ANALYZED_FP_FORMAT
     ANALYZER_FP_FORMAT max = std::numeric_limits<ANALYZER_FP_FORMAT>::max();
     PPL_DIRTY_TEMP_COEFFICIENT(M);
     assign_r(M, max, ROUND_DOWN);

    

Roberto Amadini

tags (0)

participants (1)