Module: ppl/ppl Branch: floating_point Commit: fae817ce8120f46f89a3f254c00cd80725db09e1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fae817ce8120f... Author: Roberto Amadini <r.amadini@virgilio.it> Date: Wed Sep 16 20:13:44 2009 +0200 Added another test. Coverage of 100% reached for affine_image and linear_form_upper_bound methods. Temporarily(?) removed some checks in linear_form_upper_bound. --- src/Octagonal_Shape.templates.hh | 12 +++--- tests/Floating_Point_Expression/affineimage3.cc | 39 ++++++++++++++++++---- 2 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index da27f9d..0cd06f5 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5356,27 +5356,27 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); - if (is_plus_infinity(curr_var_ub)) { + /*if (is_plus_infinity(curr_var_ub)) { assign_r(first_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); assign_r(third_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); } - else { + else {*/ add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, ROUND_UP); add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, ROUND_UP); - } + /*} if (is_minus_infinity(curr_minus_var_ub)) { assign_r(second_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); assign_r(fourth_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); } - else { + else { */ add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, ROUND_UP); add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, ROUND_UP); - } + //} assign_r(first_comparison_term, std::max(first_comparison_term, second_comparison_term), @@ -5392,7 +5392,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, } } - n_var += 2; + n_var += 2; } } diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index 8438ea3..5736f8d 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -259,8 +259,36 @@ bool test08() { return ok; } -// tests affine_image(A, i1*A + i2*B + i3) +// tests affine_image(B, [-0.5, 0.5]*A) 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); + db_r_oc coeff(-0.5); + coeff.join_assign(0.5); + Linear_Form<db_r_oc> l(A); + l *= coeff; + oc1.affine_image(B, l); + print_constraints(oc1, "*** oc1.affine_image(B, [-0.5, 0.5]*A) ***"); + + Octagonal_Shape<double> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(-B + A <= 3); + known_result.add_constraint(A + B <= 3); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; +} + + +// tests affine_image(A, i + i0*A + i1*B) +bool test10() { Variable A(0); Variable B(1); @@ -271,22 +299,17 @@ bool test09() { oc1.add_constraint(B >= 0); oc1.add_constraint(B <= 2); oc1.add_constraint(A - B >= 0); - - print_constraints(oc1, "*** oc1 ***"); - 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);; - print_constraints(oc1, "*** oc1.affine_image(A,i1*A+i2*B+i3) ***"); oc1.affine_image(A,l); + print_constraints(oc1, "*** oc1.affine_image(A, i + i0*A + i1*B) ***"); Octagonal_Shape<double> know_result(2); know_result.add_constraint(A >= 0); @@ -297,6 +320,7 @@ bool test09() { know_result.add_constraint(A + B <= 10); know_result.add_constraint(-A + B <= 0); know_result.add_constraint(-A - B <= 0); + print_constraints(know_result, "*** know_result ***"); bool ok = (oc1 == know_result); @@ -315,4 +339,5 @@ BEGIN_MAIN DO_TEST(test07); DO_TEST(test08); DO_TEST(test09); + DO_TEST(test10); END_MAIN