[PPL-devel] [GIT] ppl/ppl(floating_point): Few tests added;

[Fabio Biselli]

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

Author: Fabio Biselli <fabio.biselli at studenti.unipr.it>
Date:   Wed Sep 30 16:49:14 2009 +0200

Few tests added;
Fixed refine_with_linear_form_inequality();

---

 src/BD_Shape.templates.hh                   |   10 ---
 tests/Floating_Point_Expression/Makefile.am |   14 ++--
 tests/Floating_Point_Expression/bdshape2.cc |  107 +++++++++++++++++++++++++++
 3 files changed, 114 insertions(+), 17 deletions(-)

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh
index a4c1726..aa6a981 100644
--- a/src/BD_Shape.templates.hh
+++ b/src/BD_Shape.templates.hh
@@ -4404,7 +4404,6 @@ BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t,
         return;
       }
     }
-    return;
 } // end of left_inhomogeneous_refine
 
 
@@ -4521,14 +4520,6 @@ BD_Shape<T>
         add_dbm_constraint(right_w_id+1, left_w_id+1, c_plus_minus_a_minus);
 	return;
       }
-      if (is_left_coeff_one && is_right_coeff_minus_one) {
-        // if right coefficent is negative the constraint x + y <= b
-	// is ignored;
-
-	// FIXME: manage this case adding a costraint x <= k
-	// where k is an overaproximation of b - y
-        return;
-      }
       if (is_left_coeff_minus_one && is_right_coeff_minus_one) {
         PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
         const FP_Interval_Type& left_a = left.inhomogeneous_term();
@@ -4539,7 +4530,6 @@ BD_Shape<T>
         return;
       }
     }
-    return;
 }
 
 template <typename T>
diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am
index 941c905..f91ef32 100644
--- a/tests/Floating_Point_Expression/Makefile.am
+++ b/tests/Floating_Point_Expression/Makefile.am
@@ -137,19 +137,19 @@ digitalfilters1_SOURCES = digitalfilters1.cc
 
 bdshape2_SOURCE = bdshape2.cc
 
-#polyhedron2_SOURCES = polyhedron2.cc
+polyhedron2_SOURCES = polyhedron2.cc
 
-#polyhedron1_SOURCES = polyhedron1.cc
+polyhedron1_SOURCES = polyhedron1.cc
 
-#bdshape1_SOURCES = bdshape1.cc
+bdshape1_SOURCES = bdshape1.cc
 
-#floatingpointexpr1_SOURCES = floatingpointexpr1.cc
+floatingpointexpr1_SOURCES = floatingpointexpr1.cc
 
-#linearform1_SOURCES = linearform1.cc
+linearform1_SOURCES = linearform1.cc
 
-#octagonalshape1_SOURCES = octagonalshape1.cc
+octagonalshape1_SOURCES = octagonalshape1.cc
 
-#octagonalshape2_SOURCES = octagonalshape2.cc
+octagonalshape2_SOURCES = octagonalshape2.cc
 
 
 #
diff --git a/tests/Floating_Point_Expression/bdshape2.cc b/tests/Floating_Point_Expression/bdshape2.cc
index 4b5277d..5a70ad3 100644
--- a/tests/Floating_Point_Expression/bdshape2.cc
+++ b/tests/Floating_Point_Expression/bdshape2.cc
@@ -442,6 +442,110 @@ test11() {
   return ok1 && ok2;
 }
 
+// tests - A <= [-1, 0] and [0, 1] <= A
+bool
+test12() {
+  Variable A(0);
+  Variable B(1);
+
+  FP_BD_Shape bd1(2);
+  bd1.add_constraint(A <= 2);
+  bd1.add_constraint(A - B <= 3);
+  bd1.add_constraint(B <= 2);
+  FP_BD_Shape known_result(bd1);
+  FP_Interval tmp(0);
+  tmp.join_assign(-1);
+  FP_Linear_Form l2(tmp);
+  FP_Linear_Form l1(-A);
+  
+  bd1.refine_with_linear_form_inequality(l1, l2);
+  print_constraints(bd1, "*** - A <= [-1, 0]  ***");
+
+  known_result.add_constraint( - A <= 0);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok1 = (bd1 == known_result);
+
+  bd1.refine_with_linear_form_inequality(l2, l1);
+  print_constraints(bd1, "*** [0, 1] <= - A  ***");
+  known_result.add_constraint( A <= 1);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok2 = (bd1 == known_result);
+
+  return ok1 && ok2;
+}
+
+// tests  A <= - B + [-1, 0] and - B + [0, 1] <= A
+bool
+test13() {
+  Variable A(0);
+  Variable B(1);
+
+  FP_BD_Shape bd1(2);
+  bd1.add_constraint(A <= 2);
+  bd1.add_constraint(A - B <= 3);
+  bd1.add_constraint(B <= 2);
+  FP_BD_Shape known_result(bd1);
+  FP_Interval tmp(0);
+  tmp.join_assign(-1);
+  FP_Linear_Form l2(-B);
+  FP_Linear_Form l1(A);
+   l2 += tmp;
+  
+  bd1.refine_with_linear_form_inequality(l1, l2);
+  print_constraints(bd1, "*** A <= - B + [-1, 0]  ***");
+
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok1 = (bd1 == known_result);
+
+  bd1.refine_with_linear_form_inequality(l2, l1);
+  print_constraints(bd1, "*** - B + [0, 1] <= A  ***");
+  
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok2 = (bd1 == known_result);
+
+  return ok1 && ok2;
+}
+
+// tests  A <= - A + [-1, 0] and - A + [0, 1] <= A
+bool
+test14() {
+  Variable A(0);
+  Variable B(1);
+
+  FP_BD_Shape bd1(2);
+  bd1.add_constraint(A <= 2);
+  bd1.add_constraint(A - B <= 3);
+  bd1.add_constraint(B <= 2);
+  FP_BD_Shape known_result(bd1);
+  FP_Interval tmp(0);
+  tmp.join_assign(-1);
+  FP_Linear_Form l2(-A);
+  FP_Linear_Form l1(A);
+  l2 += tmp;
+  
+  bd1.refine_with_linear_form_inequality(l1, l2);
+  print_constraints(bd1, "*** A <= - A + [-1, 0]  ***");
+
+  known_result.add_constraint(2*A <= 0);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok1 = (bd1 == known_result);
+
+  bd1.refine_with_linear_form_inequality(l2, l1);
+  print_constraints(bd1, "*** - A + [0, 1] <= A  ***");
+  
+  known_result.add_constraint(2*(-A) <= 1);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok2 = (bd1 == known_result);
+
+  return ok1 && ok2;
+}
+
 } // namespace
 
 BEGIN_MAIN
@@ -456,4 +560,7 @@ BEGIN_MAIN
   DO_TEST(test09);
   DO_TEST(test10);
   DO_TEST(test11);
+  DO_TEST(test12);
+  DO_TEST(test13);
+  DO_TEST(test14);
 END_MAIN