[PPL-devel] [GIT] ppl/ppl(floating_point): Added another test.

[Roberto Amadini]

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

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

Added another test.

---

 tests/Floating_Point_Expression/polyhedron2.cc |   43 +++++++++++++++++++++--
 1 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc
index 8dedc6f..06e88ae 100644
--- a/tests/Floating_Point_Expression/polyhedron2.cc
+++ b/tests/Floating_Point_Expression/polyhedron2.cc
@@ -111,8 +111,6 @@ test04() {
   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);
@@ -154,11 +152,48 @@ test04() {
 
 }
 
-// tests (2/3)*B - 0.5 >= (1/3)*A
+// tests (2/3)*B + [-0.5, 0.5] >= (1/3)*A
+// FIXME: Not pass at the moment.
 bool
 test05() {
+  Variable A(0);
+  Variable B(1);
+  FP_Interval tmp0(-1);
+  tmp0.join_assign(1);
+  FP_Interval_Abstract_Store store(2);
+  store.set_interval(A, tmp0);
+  store.set_interval(B, tmp0);
+  FP_Interval tmp(1);
+  tmp /= FP_Interval(3);
+  FP_Linear_Form la(A);
+  la *= tmp;
+  FP_Linear_Form lb(B);
+  tmp += tmp;
+  lb *= tmp;
+  tmp.lower() = -0.5;
+  tmp.upper() = 0.5;
+  lb += tmp;
+
+  C_Polyhedron ph(2);
+  ph.refine_with_linear_form_inequality(la, lb, store);
+  print_constraints(ph, "*** ph ***");
+
+  C_Polyhedron known_result1(2);
+  known_result1.add_constraint(2*A <= 4*B + 1);
+  print_constraints(known_result1, "*** known_result1 ***");
+
+  bool ok1 = ph.contains(known_result1);
 
-  return true;
+  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));
+
+  nout << "B = " << store.get_interval(B) << endl;
+  bool ok3 = tmp0.contains(store.get_interval(B));
+
+  return ok1 && ok2 && ok3;
 }
 
 } // namespace