Module: ppl/ppl Branch: floating_point Commit: f3324f27c92998f4d79e61f7daa6f9f3b5ce0ab2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f3324f27c9299...
Author: Fabio Biselli fabio.biselli@studenti.unipr.it Date: Wed Sep 30 16:49:14 2009 +0200
Few tests added; Fixed refine_with_linear_form_inequality();
---
src/BD_Shape.templates.hh | 10 --- tests/Floating_Point_Expression/Makefile.am | 14 ++-- tests/Floating_Point_Expression/bdshape2.cc | 107 +++++++++++++++++++++++++++ 3 files changed, 114 insertions(+), 17 deletions(-)
diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index a4c1726..aa6a981 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4404,7 +4404,6 @@ BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t, return; } } - return; } // end of left_inhomogeneous_refine
@@ -4521,14 +4520,6 @@ BD_Shape<T> 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) { - // if right coefficent is negative the constraint x + y <= b - // is ignored; - - // FIXME: manage this case adding a costraint x <= k - // where k is an overaproximation of b - y - return; - } if (is_left_coeff_minus_one && is_right_coeff_minus_one) { PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); const FP_Interval_Type& left_a = left.inhomogeneous_term(); @@ -4539,7 +4530,6 @@ BD_Shape<T> return; } } - return; }
template <typename T> diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index 941c905..f91ef32 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -137,19 +137,19 @@ digitalfilters1_SOURCES = digitalfilters1.cc
bdshape2_SOURCE = bdshape2.cc
-#polyhedron2_SOURCES = polyhedron2.cc +polyhedron2_SOURCES = polyhedron2.cc
-#polyhedron1_SOURCES = polyhedron1.cc +polyhedron1_SOURCES = polyhedron1.cc
-#bdshape1_SOURCES = bdshape1.cc +bdshape1_SOURCES = bdshape1.cc
-#floatingpointexpr1_SOURCES = floatingpointexpr1.cc +floatingpointexpr1_SOURCES = floatingpointexpr1.cc
-#linearform1_SOURCES = linearform1.cc +linearform1_SOURCES = linearform1.cc
-#octagonalshape1_SOURCES = octagonalshape1.cc +octagonalshape1_SOURCES = octagonalshape1.cc
-#octagonalshape2_SOURCES = octagonalshape2.cc +octagonalshape2_SOURCES = octagonalshape2.cc
# diff --git a/tests/Floating_Point_Expression/bdshape2.cc b/tests/Floating_Point_Expression/bdshape2.cc index 4b5277d..5a70ad3 100644 --- a/tests/Floating_Point_Expression/bdshape2.cc +++ b/tests/Floating_Point_Expression/bdshape2.cc @@ -442,6 +442,110 @@ test11() { return ok1 && ok2; }
+// tests - A <= [-1, 0] and [0, 1] <= A +bool +test12() { + 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); + tmp.join_assign(-1); + FP_Linear_Form l2(tmp); + FP_Linear_Form l1(-A); + + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** - A <= [-1, 0] ***"); + + known_result.add_constraint( - A <= 0); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** [0, 1] <= - A ***"); + known_result.add_constraint( A <= 1); + print_constraints(known_result, "*** known_result ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; +} + +// tests A <= - B + [-1, 0] and - B + [0, 1] <= A +bool +test13() { + 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); + tmp.join_assign(-1); + FP_Linear_Form l2(-B); + FP_Linear_Form l1(A); + l2 += tmp; + + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** A <= - B + [-1, 0] ***"); + + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** - B + [0, 1] <= A ***"); + + print_constraints(known_result, "*** known_result ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; +} + +// tests A <= - A + [-1, 0] and - A + [0, 1] <= A +bool +test14() { + 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); + tmp.join_assign(-1); + FP_Linear_Form l2(-A); + FP_Linear_Form l1(A); + l2 += tmp; + + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** A <= - A + [-1, 0] ***"); + + known_result.add_constraint(2*A <= 0); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** - A + [0, 1] <= A ***"); + + known_result.add_constraint(2*(-A) <= 1); + print_constraints(known_result, "*** known_result ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; +} + } // namespace
BEGIN_MAIN @@ -456,4 +560,7 @@ BEGIN_MAIN DO_TEST(test09); DO_TEST(test10); DO_TEST(test11); + DO_TEST(test12); + DO_TEST(test13); + DO_TEST(test14); END_MAIN