Module: ppl/ppl Branch: floating_point Commit: c07b5cfd78cea7c03c90c48697025d595e9cdb2f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c07b5cfd78cea... Author: Roberto Amadini <r.amadini@virgilio.it> Date: Mon Sep 21 13:16:17 2009 +0200 Fixed a bug in BD_Shape<T>::affine_image and added more tests for this method. --- src/BD_Shape.templates.hh | 19 +++--- tests/Floating_Point_Expression/bdshape1.cc | 89 +++++++++++++++++++++++++-- 2 files changed, 93 insertions(+), 15 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 6d44f5e..db11ab5 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4108,16 +4108,11 @@ BD_Shape<T>::affine_image(const Variable& var, return; } - // General case. - // Either t == 2, so that - // lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, - // or t == 1, lf == i*w + b, but i <> [+/-1;+/-1]. - //two_variables_affine_image(var, var_id, lf); PPL_ASSERT(OK()); } -// Case 1: var = [-b, b]. +// Case 1: var = b, where b = [-b_mlb, b_ub] template <typename T> template <typename Interval_Info> void @@ -4139,7 +4134,7 @@ BD_Shape<T>::inhomogeneous_affine_image(const dimension_type& var_id, return; } -// case 2: var = (+/-1) * w + [lb, -mlb], where `w' can be `var' +// case 2: var = (+/-1) * w + [-b_mlb, b_ub], where `w' can be `var' // or another variable. template <typename T> template <typename Interval_Info> @@ -4155,7 +4150,7 @@ void BD_Shape<T> PPL_DIRTY_TEMP(N, b_mlb); neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED); - // true if b = [b_lb, b_ub] = [-mlb, ub] = [0;0]. + // true if b = [b_lb, b_ub] = [0;0]. bool is_b_zero = (b_mlb == 0 && b_ub == 0); // true if w_coeff = [1;1] bool is_w_coeff_one = (w_coeff == 1); @@ -4193,9 +4188,9 @@ void BD_Shape<T> // Translate the unary constraints on `var' by adding the value // `b_ub' or subtracting the value `b_lb'. N& dbm_v0 = dbm[var_id][0]; - add_assign_r(dbm_v0, dbm_v0, b_ub, ROUND_UP); + add_assign_r(dbm_v0, dbm_v0, b_mlb, ROUND_UP); N& dbm_0v = dbm[0][var_id]; - add_assign_r(dbm_v0, dbm_0v, b_mlb, ROUND_UP); + add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP); } } } @@ -4235,6 +4230,10 @@ void BD_Shape<T> return; } +// General case. +// Either t == 2, so that +// lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, +// or t == 1, lf == i*w + b, but i <> [+/-1;+/-1]. template <typename T> template <typename Interval_Info> void BD_Shape<T> diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index cd17822..2c0ab15 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -77,14 +77,90 @@ test02() { bd1.affine_image(A, l); print_constraints(bd1, "*** bd1.affine_image(A, [-2, 1]) ***"); - bd1.ascii_dump(); - // At the moment, affine_image is simply an identity function. - BD_Shape<float> known_result(2); known_result.add_constraint(A <= 1); - known_result.add_constraint(- A <= 2); + known_result.add_constraint(-A <= 2); + known_result.add_constraint(B <= 2); + print_constraints(bd1, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(A, [-1, -1]*A + [0.5, 2]) +bool test03() { + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + db_r_oc free_term(0.5); + free_term.join_assign(2); + Linear_Form<db_r_oc> l(-A); + l += free_term; + bd1.affine_image(A, l); + print_constraints(bd1, "*** bd1.affine_image(A, -A + [0.5, 2]) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(-2*A <= 3); + known_result.add_constraint(B <= 2); + print_constraints(known_result, "*** known_result ***"); + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(B, [1, 1]*B + [-1.5, 3.5]) +bool test04() { + Variable A(0); + Variable B(1); + + BD_Shape<float> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + fl_r_oc free_term(-1.5); + free_term.join_assign(3.5); + Linear_Form<fl_r_oc> l(B); + l += free_term; + bd1.affine_image(B, l); + print_constraints(bd1, "*** bd1.affine_image(B, B + [-1.5, 3.5]) ***"); + + BD_Shape<float> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(2*B <= 11); + known_result.add_constraint(-2*B + 2*A <= 9); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(A, [1, 1]*B + [-1, 0.5]) +bool test05() { + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + db_r_oc free_term(-1); + free_term.join_assign(0.5); + Linear_Form<db_r_oc> l(B); + l += free_term; + bd1.affine_image(A, l); + print_constraints(bd1, "*** bd1.affine_image(A, B + [-1, 0.5]) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(2*A <= 5); known_result.add_constraint(B <= 2); - + known_result.add_constraint(B - A <= 1); + known_result.add_constraint(2*A - 2*B <= 1); print_constraints(known_result, "*** known_result ***"); bool ok = (bd1 == known_result); @@ -97,4 +173,7 @@ test02() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); END_MAIN