[PPL-devel] [GIT] ppl/ppl(floating_point): Added two more tests in refinelf1.cc

[Roberto Amadini]

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

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Fri Sep 18 09:48:03 2009 +0200

Added two more tests in refinelf1.cc
Improved a test in affineimage3.cc

---

 tests/Floating_Point_Expression/affineimage3.cc |   19 +++---
 tests/Floating_Point_Expression/refinelf1.cc    |   75 +++++++++++++++++++++++
 2 files changed, 85 insertions(+), 9 deletions(-)

diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc
index 5736f8d..6633d3e 100644
--- a/tests/Floating_Point_Expression/affineimage3.cc
+++ b/tests/Floating_Point_Expression/affineimage3.cc
@@ -299,15 +299,16 @@ bool test10() {
   oc1.add_constraint(B >= 0);
   oc1.add_constraint(B <= 2);
   oc1.add_constraint(A - B >= 0);
-  db_r_oc i3(0);
-  i3.join_assign(2);
-  db_r_oc i2(1);
-  i2.join_assign(2);
-  db_r_oc i1(1);
-  i1.join_assign(1);
-  Linear_Form<db_r_oc> l(i3);
-  l += i1*Linear_Form<db_r_oc>(A);
-  l += i2*Linear_Form<db_r_oc>(B);;
+  db_r_oc tmp(1);
+  tmp.join_assign(1);
+  Linear_Form<db_r_oc> l(A);
+  l *= tmp;
+  tmp.lower() = 0;
+  tmp.upper() = 2;
+  l += tmp;
+  tmp.lower() = 1;
+  tmp.upper() = 2;
+  l += tmp * Linear_Form<db_r_oc>(B);
   oc1.affine_image(A,l);
   print_constraints(oc1, "*** oc1.affine_image(A, i + i0*A + i1*B) ***");
 
diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc
index 4515350..7998d21 100644
--- a/tests/Floating_Point_Expression/refinelf1.cc
+++ b/tests/Floating_Point_Expression/refinelf1.cc
@@ -322,6 +322,79 @@ test08() {
   return ok;
 }
 
+// tests [0.25, 0.5] * A + [-2, -1] * B <= [-7, -2]
+bool
+test09() {
+  Variable A(0);
+  Variable B(1);
+
+  Octagonal_Shape<double> oc1(3);
+  oc1.add_constraint(A <= 2);
+  oc1.add_constraint(A - B <= 3);
+  oc1.add_constraint(B <= 2);
+  Octagonal_Shape<double> known_result(oc1);
+
+  db_r_oc tmp(-7);
+  tmp.join_assign(-2);
+  Linear_Form<db_r_oc> l2(tmp);
+  Linear_Form<db_r_oc> l1(A);
+  tmp.lower() = 0.25;
+  tmp.upper() = 0.5;
+  l1 *= tmp;
+  tmp.lower() = -2;
+  tmp.upper() = -1;
+  l1 += tmp * Linear_Form<db_r_oc>(B);
+  oc1.refine_with_linear_form_inequality(l1, l2);
+  print_constraints(oc1, "*** [0.25, 0.5]*A + [-2, -1]*B <= [-7, -2] ***");
+
+  known_result.add_constraint(2*B + 2*A <= 11);
+  known_result.add_constraint(-2*B + 2*A <= 3);
+  known_result.add_constraint(2*A <= 7);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok = (oc1 == known_result);
+
+  return ok;
+}
+
+// tests [-5, -1] * A <= [2, 3] * B + [0.5, 1]
+bool
+test10() {
+  Variable A(0);
+  Variable B(1);
+
+  Octagonal_Shape<float> oc1(3);
+  oc1.add_constraint(A <= 2);
+  oc1.add_constraint(A - B <= 3);
+  oc1.add_constraint(B <= 2);
+  Octagonal_Shape<float> known_result(oc1);
+  fl_r_oc tmp(2);
+  tmp.join_assign(3);
+  Linear_Form<fl_r_oc> l2(B);
+  l2 *= tmp;
+  tmp.lower() = 0.5;
+  tmp.upper() = 1;
+  l2 += tmp;
+  Linear_Form<fl_r_oc> l1(A);
+  tmp.lower() = -5;
+  tmp.upper() = -1;
+  l1 *= tmp;
+  oc1.refine_with_linear_form_inequality(l1, l2);
+  print_constraints(oc1, "*** [-5, -1] * A <= [2, 3] * B + [0.5, 1] ***");
+
+  known_result.add_constraint(B - A <= 17);
+  known_result.add_constraint(B + A <= 21);
+  known_result.add_constraint(-B - A <= 13);
+  known_result.add_constraint(-B + A <= 17);
+  known_result.add_constraint(A <= 19);
+  known_result.add_constraint(-A <= 15);
+  print_constraints(known_result, "*** known_result ***");
+
+  bool ok = (oc1 == known_result);
+
+  return ok;
+}
+
 } //namespace
 
 BEGIN_MAIN
@@ -333,4 +406,6 @@ BEGIN_MAIN
   DO_TEST(test06);
   DO_TEST(test07);
   DO_TEST(test08);
+  DO_TEST(test09); //FIXME: A <= 1.75 (cut&paste error???)
+  DO_TEST(test10); //FIXME: A >= -7.5 (cut&paste error???)
 END_MAIN