[PPL-devel] [GIT] ppl/ppl(floating_point): Added two tests;

[Fabio Biselli]

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

Author: Fabio Biselli <fabio.biselli at studenti.unipr.it>
Date:   Tue Sep 29 14:57:47 2009 +0200

Added two tests;
Fixed a bug in left_one_var_refine() function.

---

 src/BD_Shape.templates.hh                   |    2 +-
 tests/Floating_Point_Expression/Makefile.am |    5 ++-
 tests/Floating_Point_Expression/bdshape2.cc |   49 ++++++++++++++++++++++++--
 3 files changed, 50 insertions(+), 6 deletions(-)

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh
index 657a1c4..46ba6b7 100644
--- a/src/BD_Shape.templates.hh
+++ b/src/BD_Shape.templates.hh
@@ -4485,7 +4485,7 @@ BD_Shape<T>
         const FP_Interval_Type& right_c = right.inhomogeneous_term();
         sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(),
                      ROUND_UP);
-        add_dbm_constraint(left_w_id+1, right_w_id+1, c_plus_minus_a_minus);
+        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) {
diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am
index fd77e8a..941c905 100644
--- a/tests/Floating_Point_Expression/Makefile.am
+++ b/tests/Floating_Point_Expression/Makefile.am
@@ -51,7 +51,8 @@ $(top_builddir)/src/libppl.la \
 @extra_libraries@
 
 ORIGINAL_TESTS = \
-digitalfilters1
+digitalfilters1 \
+bdshape2
 
 #bdshape1 \
 #floatingpointexpr1 \
@@ -134,6 +135,8 @@ print_INSTANCES:
 
 digitalfilters1_SOURCES = digitalfilters1.cc
 
+bdshape2_SOURCE = bdshape2.cc
+
 #polyhedron2_SOURCES = polyhedron2.cc
 
 #polyhedron1_SOURCES = polyhedron1.cc
diff --git a/tests/Floating_Point_Expression/bdshape2.cc b/tests/Floating_Point_Expression/bdshape2.cc
index f4b4b47..fab904b 100644
--- a/tests/Floating_Point_Expression/bdshape2.cc
+++ b/tests/Floating_Point_Expression/bdshape2.cc
@@ -107,7 +107,7 @@ test03() {
   Variable A(0);
   Variable B(1);
 
-  FP_Octagonal_Shape bd1(3);
+  FP_Octagonal_Shape bd1(2);
   bd1.add_constraint(A <= 2);
   bd1.add_constraint(A - B <= 3);
   bd1.add_constraint(B <= 2);
@@ -138,10 +138,51 @@ test03() {
   return ok1 && ok2;
 
 }
+
+// tests [-0.5, 1] + A <= [2.5, 5] + B and [2.5, 5] + B <= [-0.5, 1] + A
+bool
+test04() {
+  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.5);
+  tmp.join_assign(1);
+  FP_Linear_Form l1(A);
+  l1 += tmp;
+  FP_Linear_Form l2(B);
+  tmp.lower() = 2.5;
+  tmp.upper() = 5;
+  l2 += tmp;
+  bd1.refine_with_linear_form_inequality(l1, l2);
+  print_constraints(bd1, "*** [-0.5, 1] + A <= [2.5, 5] + B ***");
+
+  known_result.add_constraint(2*A - 2*B <= 11);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok1 = (bd1 == known_result);
+
+  bd1.refine_with_linear_form_inequality(l2, l1);
+  print_constraints(bd1, "*** [2.5, 5] + B <= [-0.5, 1] + A ***");
+
+  known_result.add_constraint((2*B) - (2*A) <= -3);
+  print_constraints(known_result, "*** known_result2 ***");
+
+  bool ok2 = (bd1 == known_result);
+
+  return ok1 && ok2;
+
+}
+
 } // namespace
 
 BEGIN_MAIN
-  DO_TEST(test01);
-  DO_TEST(test02);
-// DO_TEST(test03);
+//DO_TEST(test01);
+//DO_TEST(test02);
+//DO_TEST(test03);
+  DO_TEST(test04);
 END_MAIN