[PPL-devel] [GIT] ppl/ppl(floating_point): Added a test in polyhedron2.cc

[Roberto Amadini]

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

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Sat Sep 26 17:09:48 2009 +0200

Added a test in polyhedron2.cc

---

 tests/Floating_Point_Expression/polyhedron2.cc |   96 ++++++++++++++++++++---
 1 files changed, 83 insertions(+), 13 deletions(-)

diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc
index 3b57c57..8dedc6f 100644
--- a/tests/Floating_Point_Expression/polyhedron2.cc
+++ b/tests/Floating_Point_Expression/polyhedron2.cc
@@ -25,6 +25,7 @@ site: http://www.cs.unipr.it/ppl/ . */
 
 namespace {
 
+// tests incompatible dimensions.
 bool
 test01() {
   C_Polyhedron pol(1);
@@ -42,6 +43,7 @@ test01() {
       pol.refine_with_linear_form_inequality(l1, l2, store);
     }
     catch (std::invalid_argument) {
+      nout << "incompatible dimensions." << endl;
       return true;
     }
   }
@@ -49,22 +51,25 @@ test01() {
   return false;
 }
 
+// tests A <= [57, 57]
 bool
 test02() {
-  C_Polyhedron result(1);
+  C_Polyhedron ph(1);
   FP_Interval_Abstract_Store store(1);
   store.set_interval(Variable(0), FP_Interval(1.5));
   FP_Interval interval(57);
   FP_Linear_Form lf1(Variable(0));
   FP_Linear_Form lf2(interval);
-  result.refine_with_linear_form_inequality(lf1, lf2, store);
-  print_constraints(result, "RESULT");
+  ph.refine_with_linear_form_inequality(lf1, lf2, store);
+  print_constraints(ph, "*** A <= [57, 57] ***");
   C_Polyhedron known_result(1);
   known_result.refine_with_constraint(Variable(0) <= 57);
-  print_constraints(known_result, "KNOWN RESULT");
-  return result == known_result;
+  print_constraints(known_result, "*** known_result ***");
+
+  return ph == known_result;
 }
 
+// tests -A <= 0 && A <= 2 && -A <= 1 && -B <= -1
 bool
 test03() {
   Variable A(0);
@@ -73,24 +78,87 @@ test03() {
   store.set_interval(A, FP_Interval(1));
   store.set_interval(B, FP_Interval(2));
 
-  C_Polyhedron result(2);
-  result.refine_with_linear_form_inequality(-FP_Linear_Form(A),
+  C_Polyhedron ph(2);
+  ph.refine_with_linear_form_inequality(-FP_Linear_Form(A),
 				 FP_Linear_Form(FP_Interval(0)), store);
-  result.refine_with_linear_form_inequality(FP_Linear_Form(A),
+  ph.refine_with_linear_form_inequality(FP_Linear_Form(A),
 				 FP_Linear_Form(FP_Interval(2)), store);
-  result.refine_with_linear_form_inequality(-FP_Linear_Form(A),
+  ph.refine_with_linear_form_inequality(-FP_Linear_Form(A),
 				 FP_Linear_Form(FP_Interval(1)), store);
-  result.refine_with_linear_form_inequality(-FP_Linear_Form(B),
+  ph.refine_with_linear_form_inequality(-FP_Linear_Form(B),
 				 FP_Linear_Form(FP_Interval(-1)), store);
-  print_constraints(result, "RESULT");
+  print_constraints(ph, "*** ph ***");
 
   C_Polyhedron known_result(2);
   known_result.add_constraint(A >= 0);
   known_result.add_constraint(A <= 2);
   known_result.add_constraint(B >= 1);
-  print_constraints(known_result, "KNOWN RESULT");
+  print_constraints(known_result, "*** known_result ***");
+
+  return ph == known_result;
+}
+
+// tests -A <= -1/3 && A <= 2/3 && -B <= 0 && B <= 1/3
+// and refine_fp_interval_abstract_store
+bool
+test04() {
+  Variable A(0);
+  Variable B(1);
+  FP_Interval tmp0(0);
+  tmp0.join_assign(10);
+  FP_Interval_Abstract_Store store(2);
+  store.set_interval(A, tmp0);
+  store.set_interval(B, tmp0);
+  FP_Interval tmp(tmp0);
+  tmp = 2;
+  //tmp.lower() = 2;
+  //tmp.upper() = 2;
+  tmp /= FP_Interval(3);
+  FP_Linear_Form la(A);
+  FP_Linear_Form lb(B);
+  FP_Linear_Form lk(tmp);
+
+  C_Polyhedron ph(2);
+  ph.refine_with_linear_form_inequality(la, lk, store);
+  tmp = 1;
+  lk -= tmp;
+  ph.refine_with_linear_form_inequality(-la, lk, store);
+  ph.refine_with_linear_form_inequality(lk, lb, store);
+  tmp = 3;
+  lk *= tmp;
+  tmp = 1;
+  lk += tmp;
+  ph.refine_with_linear_form_inequality(-lb, lk, store);
+  print_constraints(ph, "*** ph ***");
+
+  C_Polyhedron known_result1(2);
+  known_result1.add_constraint(3*A >= 1);
+  known_result1.add_constraint(3*A <= 2);
+  known_result1.add_constraint(B >= 0);
+  known_result1.add_constraint(3*B <= 1);
+  print_constraints(known_result1, "*** known_result1 ***");
+
+  bool ok1 = ph.contains(known_result1);
+
+  ph.refine_fp_interval_abstract_store(store);
+  nout << "*** FP_Interval_Abstract_Store ***" << endl;
+
+  nout << "A = " << store.get_interval(A) << endl;
+  bool ok2 = tmp0.contains(store.get_interval(A));
+
+  //FIXME: Sound, but not much precise.
+  nout << "B = " << store.get_interval(B) << endl;
+  bool ok3 = tmp0.contains(store.get_interval(B));
+
+  return ok1 && ok2 && ok3;
+
+}
+
+// tests (2/3)*B - 0.5 >= (1/3)*A
+bool
+test05() {
 
-  return result == known_result;
+  return true;
 }
 
 } // namespace
@@ -99,4 +167,6 @@ BEGIN_MAIN
   DO_TEST(test01);
   DO_TEST(test02);
   DO_TEST(test03);
+  DO_TEST(test04);
+  DO_TEST(test05);
 END_MAIN