Module: ppl/ppl Branch: master Commit: 5c95fc0eab6a38442751ed16c6cfa9d538917f3f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c95fc0eab6a3... Author: Enea Zaffanella <zaffanella@cs.unipr.it> Date: Tue Oct 19 08:15:12 2010 +0200 Improved precision of Octagonal_Shape::affine_image(). The method was rather imprecise on sign-symmetry affine transformations. Also noted that strong reduction is preserved in that case. --- src/Octagonal_Shape.templates.hh | 120 ++++++++++++++------------------- tests/Octagonal_Shape/affineimage1.cc | 24 +++++++ 2 files changed, 74 insertions(+), 70 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 7f74de5..8358b85 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4493,75 +4493,53 @@ Octagonal_Shape<T>::affine_image(const Variable var, // Case 2: expr = w_coeff*w + b, with w_coeff = +/- denominator. if (w_id == var_id) { // Here `expr' is of the form: +/- denominator * v + b. - if (w_coeff == denominator) { - if (b == 0) - // The transformation is the identity function. - return; - else { - // Translate all the constraints on `var' adding or - // subtracting the value `b/denominator'. - PPL_DIRTY_TEMP(N, d); - div_round_up(d, b, denominator); - PPL_DIRTY_TEMP(N, minus_d); - div_round_up(minus_d, b, minus_den); - const Row_Iterator m_begin = matrix.row_begin(); - const Row_Iterator m_end = matrix.row_end(); - Row_Iterator m_iter = m_begin + n_var; - Row_Reference m_v = *m_iter; - ++m_iter; - Row_Reference m_cv = *m_iter; - ++m_iter; - // NOTE: delay update of unary constraints on `var'. - for (dimension_type j = n_var; j-- > 0; ) { - N& m_v_j = m_v[j]; - add_assign_r(m_v_j, m_v_j, minus_d, ROUND_UP); - N& m_cv_j = m_cv[j]; - add_assign_r(m_cv_j, m_cv_j, d, ROUND_UP); - } - for ( ; m_iter != m_end; ++m_iter) { - Row_Reference m_i = *m_iter; - N& m_i_v = m_i[n_var]; - add_assign_r(m_i_v, m_i_v, d, ROUND_UP); - N& m_i_cv = m_i[n_var+1]; - add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); - } - // Now update unary constraints on var. - mul_2exp_assign_r(d, d, 1, ROUND_UP); - N& m_cv_v = m_cv[n_var]; - add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); - N& m_v_cv = m_v[n_var+1]; - add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); - } - reset_strongly_closed(); + const bool sign_symmetry = (w_coeff != denominator); + if (!sign_symmetry && b == 0) + // The transformation is the identity function. + return; + // Translate all the constraints on `var' adding or + // subtracting the value `b/denominator'. + PPL_DIRTY_TEMP(N, d); + div_round_up(d, b, denominator); + PPL_DIRTY_TEMP(N, minus_d); + div_round_up(minus_d, b, minus_den); + if (sign_symmetry) + std::swap(d, minus_d); + const Row_Iterator m_begin = matrix.row_begin(); + const Row_Iterator m_end = matrix.row_end(); + Row_Iterator m_iter = m_begin + n_var; + Row_Reference m_v = *m_iter; + ++m_iter; + Row_Reference m_cv = *m_iter; + ++m_iter; + // NOTE: delay update of unary constraints on `var'. + for (dimension_type j = n_var; j-- > 0; ) { + N& m_v_j = m_v[j]; + add_assign_r(m_v_j, m_v_j, minus_d, ROUND_UP); + N& m_cv_j = m_cv[j]; + add_assign_r(m_cv_j, m_cv_j, d, ROUND_UP); + if (sign_symmetry) + std::swap(m_v_j, m_cv_j); } - else { - // Here `w_coeff == -denominator'. - // Remove the binary constraints on `var'. - forget_binary_octagonal_constraints(var_id); - const Row_Iterator m_begin = matrix.row_begin(); - Row_Iterator m_iter = m_begin + n_var; - N& m_v_cv = (*m_iter)[n_var+1]; - ++m_iter; - N& m_cv_v = (*m_iter)[n_var]; - // Swap the unary constraints on `var'. - std::swap(m_v_cv, m_cv_v); - // Strong closure is not preserved. - reset_strongly_closed(); - if (b != 0) { - // Translate the unary constraints on `var', - // adding or subtracting the value `b/denominator'. - PPL_DIRTY_TEMP(N, d); - div_round_up(d, b, denominator); - mul_2exp_assign_r(d, d, 1, ROUND_UP); - add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); - PPL_DIRTY_TEMP(N, minus_d); - div_round_up(minus_d, b, minus_den); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); - add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); - } - incremental_strong_closure_assign(var); - } + for ( ; m_iter != m_end; ++m_iter) { + Row_Reference m_i = *m_iter; + N& m_i_v = m_i[n_var]; + add_assign_r(m_i_v, m_i_v, d, ROUND_UP); + N& m_i_cv = m_i[n_var+1]; + add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); + if (sign_symmetry) + std::swap(m_i_v, m_i_cv); + } + // Now update unary constraints on var. + mul_2exp_assign_r(d, d, 1, ROUND_UP); + N& m_cv_v = m_cv[n_var]; + add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); + mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); + N& m_v_cv = m_v[n_var+1]; + add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); + if (sign_symmetry) + std::swap(m_cv_v, m_v_cv); + // Note: strong closure is preserved. } else { // Here `w != var', so that `expr' is of the form @@ -4570,7 +4548,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, forget_all_octagonal_constraints(var_id); const dimension_type n_w = 2*w_id; // Add the new constraint `var - w = b/denominator'. - if (w_coeff == denominator) + if (w_coeff == denominator) { if (var_id < w_id) { add_octagonal_constraint(n_w, n_var, b, denominator); add_octagonal_constraint(n_w+1, n_var+1, b, minus_den); @@ -4579,7 +4557,8 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_octagonal_constraint(n_var+1, n_w+1, b, denominator); add_octagonal_constraint(n_var, n_w, b, minus_den); } - else + } + else { // Add the new constraint `var + w = b/denominator'. if (var_id < w_id) { add_octagonal_constraint(n_w+1, n_var, b, denominator); @@ -4589,6 +4568,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_octagonal_constraint(n_var+1, n_w, b, denominator); add_octagonal_constraint(n_var, n_w+1, b, minus_den); } + } incremental_strong_closure_assign(var); } PPL_ASSERT(OK()); diff --git a/tests/Octagonal_Shape/affineimage1.cc b/tests/Octagonal_Shape/affineimage1.cc index cdb850b..3f4e8b4 100644 --- a/tests/Octagonal_Shape/affineimage1.cc +++ b/tests/Octagonal_Shape/affineimage1.cc @@ -403,6 +403,7 @@ test15() { known_result.add_constraint(2*A <= -1); known_result.add_constraint(2*A >= -3); known_result.add_constraint(B >= 4); + known_result.add_constraint(2*A + 2*B >= 7); bool ok = check_result(oc, known_result); @@ -493,6 +494,28 @@ test18() { return ok; } +bool +test19() { + Variable x(0); + Variable y(1); + + TOctagonal_Shape oc1(2); + oc1.add_constraint(x + y == 0); + + print_constraints(oc1, "*** oc1 ***"); + + oc1.affine_image(x, -x); + + Octagonal_Shape<mpq_class> known_result(2); + known_result.add_constraint(x - y == 0); + + bool ok = (Octagonal_Shape<mpq_class>(oc1) == known_result); + + print_constraints(oc1, "*** oc1.affine_image(x, y) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -514,4 +537,5 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); + DO_TEST(test19); END_MAIN