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

Author: Roberto Amadini r.amadini@virgilio.it Date: Mon Sep 21 18:45:29 2009 +0200

Fixed a bug in affine_image and modified one_variable_affine_image. Added a new test for the general case.

---

src/BD_Shape.templates.hh | 130 +++++++++++++-------------- tests/Floating_Point_Expression/bdshape1.cc | 27 ++++++ 2 files changed, 90 insertions(+), 67 deletions(-)

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 5cbf5a5..08b1c5d 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4103,11 +4103,12 @@ BD_Shape<T>::affine_image(const Variable& var, } else if (t == 1) { const FP_Interval_Type& w_coeff = lf.coefficient(Variable(w_id - 1)); - one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim); - PPL_ASSERT(OK()); - return; + if(w_coeff == 1 || w_coeff == -1) { + one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim); + PPL_ASSERT(OK()); + return; + } } - two_variables_affine_image(var_id, lf, space_dim); PPL_ASSERT(OK()); } @@ -4154,76 +4155,71 @@ void BD_Shape<T> bool is_b_zero = (b_mlb == 0 && b_ub == 0); // true if w_coeff = [1;1] bool is_w_coeff_one = (w_coeff == 1); - // true if w_coeff = [-1;-1]. - bool is_w_coeff_minus_one = (w_coeff == -1); - if (is_w_coeff_one || is_w_coeff_minus_one) { - if (w_id == var_id) { - // Here `lf' is of the form: [+/-1;+/-1] * v + b. - if (is_w_coeff_one) { - if (is_b_zero) - // The transformation is the identity function. - return; - else { - // Translate all the constraints on `var' by adding the value - // `b_ub' or subtracting the value `b_lb'. - DB_Row<N>& dbm_v = dbm[var_id]; - for (dimension_type i = space_dim + 1; i-- > 0; ) { - N& dbm_vi = dbm_v[i]; - add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP); - N& dbm_iv = dbm[i][var_id]; - add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP); - } - // Both shortest-path closure and reduction are preserved. - }

- } + if (w_id == var_id) { + // Here `lf' is of the form: [+/-1;+/-1] * v + b. + if (is_w_coeff_one) { + if (is_b_zero) + // The transformation is the identity function. + return; else { - // Here `w_coeff = [-1;-1]. - // Remove the binary constraints on `var'. - forget_binary_dbm_constraints(var_id); - std::swap(dbm[var_id][0], dbm[0][var_id]); - // Shortest-path closure is not preserved. - reset_shortest_path_closed(); - if (!is_b_zero) { - // 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_mlb, ROUND_UP); - N& dbm_0v = dbm[0][var_id]; - add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP); + // Translate all the constraints on `var' by adding the value + // `b_ub' or subtracting the value `b_lb'. + DB_Row<N>& dbm_v = dbm[var_id]; + for (dimension_type i = space_dim + 1; i-- > 0; ) { + N& dbm_vi = dbm_v[i]; + add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP); + N& dbm_iv = dbm[i][var_id]; + add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP); } + // Both shortest-path closure and reduction are preserved. + } + } + else { + // Here `w_coeff = [-1;-1]. + // Remove the binary constraints on `var'. + forget_binary_dbm_constraints(var_id); + std::swap(dbm[var_id][0], dbm[0][var_id]); + // Shortest-path closure is not preserved. + reset_shortest_path_closed(); + if (!is_b_zero) { + // 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_mlb, ROUND_UP); + N& dbm_0v = dbm[0][var_id]; + add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP); } } + } + else { + // Here `w != var', so that `lf' is of the form + // [+/-1;+/-1] * w + b. + // Remove all constraints on `var'. + forget_all_dbm_constraints(var_id); + // Shortest-path closure is preserved, but not reduction. + if (marked_shortest_path_reduced()) + reset_shortest_path_reduced(); + if (is_w_coeff_one) { + // Add the new constraints `var - w >= b_lb' + // `and var - w <= b_ub'. + add_dbm_constraint(w_id, var_id, b_ub); + add_dbm_constraint(var_id, w_id, b_mlb); + } else { - // Here `w != var', so that `lf' is of the form - // [+/-1;+/-1] * w + b. - // Remove all constraints on `var'. - forget_all_dbm_constraints(var_id); - // Shortest-path closure is preserved, but not reduction. - if (marked_shortest_path_reduced()) - reset_shortest_path_reduced(); - - if (is_w_coeff_one) { - // Add the new constraints `var - w >= b_lb' - // `and var - w <= b_ub'. - add_dbm_constraint(w_id, var_id, b_ub); - add_dbm_constraint(var_id, w_id, b_mlb); + // We have to add the constraint `v + w == b', over-approximating it + // by computing lower and upper bounds for `w'. + const N& mlb_w = dbm[w_id][0]; + if (!is_plus_infinity(mlb_w)) { + // Add the constraint `v <= ub - lb_w'. + add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP); + reset_shortest_path_closed(); } - else { - // We have to add the constraint `v + w == b', over-approximating it - // by computing lower and upper bounds for `w'. - const N& mlb_w = dbm[w_id][0]; - if (!is_plus_infinity(mlb_w)) { - // Add the constraint `v <= ub - lb_w'. - add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP); - reset_shortest_path_closed(); - } - const N& ub_w = dbm[0][w_id]; - if (!is_plus_infinity(ub_w)) { - // Add the constraint `v >= lb - ub_w'. - add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP); - reset_shortest_path_closed(); - } + const N& ub_w = dbm[0][w_id]; + if (!is_plus_infinity(ub_w)) { + // Add the constraint `v >= lb - ub_w'. + add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP); + reset_shortest_path_closed(); } } } diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index e5f06d1..0c8e305 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -253,6 +253,32 @@ bool test08() { return ok; }

+// tests affine_image(B, [-0.5, 0.5]*A) +bool test09() { + 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 coeff(-0.5); + coeff.join_assign(0.5); + Linear_Form<db_r_oc> l(A); + l *= coeff; + bd1.affine_image(B, l); + print_constraints(bd1, "*** bd1.affine_image(B, [-0.5, 0.5]*A) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(A - B <= 3); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + } // namespace

BEGIN_MAIN @@ -264,4 +290,5 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); + DO_TEST(test09); END_MAIN