Module: ppl/ppl Branch: floating_point Commit: 5decdfb92cce7eaa4aac059286afb163bac93016 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5decdfb92cce7...
Author: Roberto Amadini r.amadini@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