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

Author: Fabio Biselli fabio.biselli@studenti.unipr.it Date: Tue Sep 29 14:57:47 2009 +0200

Added two tests; Fixed a bug in left_one_var_refine() function.

---

src/BD_Shape.templates.hh | 2 +- tests/Floating_Point_Expression/Makefile.am | 5 ++- tests/Floating_Point_Expression/bdshape2.cc | 49 ++++++++++++++++++++++++-- 3 files changed, 50 insertions(+), 6 deletions(-)

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 657a1c4..46ba6b7 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4485,7 +4485,7 @@ BD_Shape<T> const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - add_dbm_constraint(left_w_id+1, right_w_id+1, c_plus_minus_a_minus); + 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) { diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index fd77e8a..941c905 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -51,7 +51,8 @@ $(top_builddir)/src/libppl.la \ @extra_libraries@

ORIGINAL_TESTS = \ -digitalfilters1 +digitalfilters1 \ +bdshape2

#bdshape1 \ #floatingpointexpr1 \ @@ -134,6 +135,8 @@ print_INSTANCES:

digitalfilters1_SOURCES = digitalfilters1.cc

+bdshape2_SOURCE = bdshape2.cc + #polyhedron2_SOURCES = polyhedron2.cc

#polyhedron1_SOURCES = polyhedron1.cc diff --git a/tests/Floating_Point_Expression/bdshape2.cc b/tests/Floating_Point_Expression/bdshape2.cc index f4b4b47..fab904b 100644 --- a/tests/Floating_Point_Expression/bdshape2.cc +++ b/tests/Floating_Point_Expression/bdshape2.cc @@ -107,7 +107,7 @@ test03() { Variable A(0); Variable B(1);

- FP_Octagonal_Shape bd1(3); + FP_Octagonal_Shape bd1(2); bd1.add_constraint(A <= 2); bd1.add_constraint(A - B <= 3); bd1.add_constraint(B <= 2); @@ -138,10 +138,51 @@ test03() { return ok1 && ok2;

} + +// tests [-0.5, 1] + A <= [2.5, 5] + B and [2.5, 5] + B <= [-0.5, 1] + A +bool +test04() { + 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.5); + tmp.join_assign(1); + FP_Linear_Form l1(A); + l1 += tmp; + FP_Linear_Form l2(B); + tmp.lower() = 2.5; + tmp.upper() = 5; + l2 += tmp; + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** [-0.5, 1] + A <= [2.5, 5] + B ***"); + + known_result.add_constraint(2*A - 2*B <= 11); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** [2.5, 5] + B <= [-0.5, 1] + A ***"); + + known_result.add_constraint((2*B) - (2*A) <= -3); + print_constraints(known_result, "*** known_result2 ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; + +} + } // namespace

BEGIN_MAIN - DO_TEST(test01); - DO_TEST(test02); -// DO_TEST(test03); +//DO_TEST(test01); +//DO_TEST(test02); +//DO_TEST(test03); + DO_TEST(test04); END_MAIN