[PPL-devel] [GIT] ppl/ppl(master): Improved precision of Octagonal_Shape::affine_image( ).
Enea Zaffanella
zaffanella at cs.unipr.it
Tue Oct 19 08:22:37 CEST 2010
Module: ppl/ppl
Branch: master
Commit: 5c95fc0eab6a38442751ed16c6cfa9d538917f3f
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c95fc0eab6a38442751ed16c6cfa9d538917f3f
Author: Enea Zaffanella <zaffanella at 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
More information about the PPL-devel
mailing list