[PPL-devel] [GIT] ppl/ppl(floating_point): Fixed a bug in affine_image and implemented three new tests.

[Roberto Amadini]

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

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Mon Sep 21 15:26:05 2009 +0200

Fixed a bug in affine_image and implemented three new tests.

---

 src/BD_Shape.templates.hh                   |    6 +-
 tests/Floating_Point_Expression/bdshape1.cc |   91 ++++++++++++++++++++++++++-
 2 files changed, 93 insertions(+), 4 deletions(-)

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh
index db11ab5..734f503 100644
--- a/src/BD_Shape.templates.hh
+++ b/src/BD_Shape.templates.hh
@@ -4212,10 +4212,10 @@ void BD_Shape<T>
       else {
         // We have to add the constraint `v + w == b', over-approximating it
         // by computing lower and upper bounds for `w'.
-        const N& lb_w = dbm[w_id][0];
-        if (!is_plus_infinity(lb_w)) {
+        const N& mlb_w = dbm[w_id][0];
+        if (!is_plus_infinity(mlb_w)) {
           // Add the constraint `v <= ub - lb_w'.
-          sub_assign_r(dbm[0][var_id], b_ub, lb_w, ROUND_UP);
+          add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP);
           reset_shortest_path_closed();
         }
         const N& ub_w = dbm[0][w_id];
diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc
index 2c0ab15..a9886b4 100644
--- a/tests/Floating_Point_Expression/bdshape1.cc
+++ b/tests/Floating_Point_Expression/bdshape1.cc
@@ -61,7 +61,6 @@ test01() {
 
 
 // tests affine_image(A, [-2, 1])
-// FIXME: It's a preliminary version, not sound at the moment.
 bool
 test02() {
   Variable A(0);
@@ -168,6 +167,93 @@ bool test05() {
   return ok;
 }
 
+// tests affine_image(B, [1, 1]*A + [-3, 1])
+bool test06() {
+  Variable A(0);
+  Variable B(1);
+
+  BD_Shape<double> bd1(3);
+  bd1.add_constraint(A <= 2);
+  bd1.add_constraint(A - B <= 3);
+  bd1.add_constraint(B <= 2);
+  db_r_oc free_term(-3);
+  free_term.join_assign(1);
+  Linear_Form<db_r_oc> l(A);
+  l += free_term;
+  bd1.affine_image(B, l);
+  print_constraints(bd1, "*** bd1.affine_image(B, A + [-3, 1]) ***");
+
+  BD_Shape<double> known_result(3);
+  known_result.add_constraint(A <= 2);
+  known_result.add_constraint(B <= 3);
+  known_result.add_constraint(B - A <= 1);
+  known_result.add_constraint(A - B <= 3);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok = (bd1 == known_result);
+
+  return ok;
+}
+
+// tests affine_image(B, [-1, -1]*A + [0, 4])
+bool test07() {
+  Variable A(0);
+  Variable B(1);
+
+  BD_Shape<float> bd1(3);
+  bd1.add_constraint(A <= 2);
+  bd1.add_constraint(A - B <= 3);
+  bd1.add_constraint(B <= 2);
+  fl_r_oc free_term(0);
+  free_term.join_assign(4);
+  Linear_Form<fl_r_oc> l(-A);
+  l += free_term;
+  bd1.affine_image(B, l);
+  print_constraints(bd1, "*** bd1.affine_image(B, -A + [0, 4]) ***");
+
+  BD_Shape<float> known_result(3);
+  known_result.add_constraint(A <= 2);
+  known_result.add_constraint(-B <= 2);
+  known_result.add_constraint(A - B <= 4);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok = (bd1 == known_result);
+
+  return ok;
+}
+
+// tests affine_image(A, [-1, -1]*B + [0, 2])
+bool test08() {
+  Variable A(0);
+  Variable B(1);
+
+  BD_Shape<float> bd1(3);
+  bd1.add_constraint(A <= 2);
+  bd1.add_constraint(A - B <= 3);
+  bd1.add_constraint(B <= 2);
+  bd1.add_constraint(B >= -10);
+  fl_r_oc free_term(0);
+  free_term.join_assign(2);
+  Linear_Form<fl_r_oc> l(-B);
+  l += free_term;
+  bd1.affine_image(A, l);
+  print_constraints(bd1, "*** bd1.affine_image(A, -B + [0, 2]) ***");
+
+  BD_Shape<float> known_result(3);
+  known_result.add_constraint(-A <= 2);
+  known_result.add_constraint(A <= 12);
+  known_result.add_constraint(B <= 2);
+  known_result.add_constraint(B >= -10);
+  //known_result.add_constraint(-B - A <= 0);
+  known_result.add_constraint(-A + B <= 4);
+  known_result.add_constraint(A - B <= 22);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok = (bd1 == known_result);
+
+  return ok;
+}
+
 } // namespace
 
 BEGIN_MAIN
@@ -176,4 +262,7 @@ BEGIN_MAIN
   DO_TEST(test03);
   DO_TEST(test04);
   DO_TEST(test05);
+  DO_TEST(test06);
+  DO_TEST(test07);
+  DO_TEST(test08);
 END_MAIN