Module: ppl/ppl Branch: master Commit: 930f0a20a7bfdc920dc8baff9cae2c3347669cd7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=930f0a20a7bfd...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Mon Apr 5 18:14:15 2010 +0200

Fixed bugs in Octagonal_Shape:drop_some_on_integer_points().

---

src/Octagonal_Shape.templates.hh | 50 +++++++++++++++++--- tests/Octagonal_Shape/dropsomenonintegerpoints1.cc | 34 +++++++++---- 2 files changed, 66 insertions(+), 18 deletions(-)

diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index fb123c4..7dfb781 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -7572,6 +7572,23 @@ Octagonal_Shape<T>::drop_some_non_integer_points(Complexity_Class) { i_end = matrix.element_end(); i != i_end; ++i) drop_some_non_integer_points_helper(*i);

+ // Unary constraints should have an even integer boundary. + PPL_DIRTY_TEMP(N, temp_one); + assign_r(temp_one, 1, ROUND_NOT_NEEDED); + for (dimension_type i = 0; i < 2*space_dim; i += 2) { + const dimension_type ci = i+1; + N& mat_i_ci = matrix[i][ci]; + if (!is_plus_infinity(mat_i_ci) && !is_even(mat_i_ci)) { + sub_assign_r(mat_i_ci, mat_i_ci, temp_one, ROUND_UP); + reset_strongly_closed(); + } + N& mat_ci_i = matrix[ci][i]; + if (!is_plus_infinity(mat_ci_i) && !is_even(mat_ci_i)) { + sub_assign_r(mat_ci_i, mat_ci_i, temp_one, ROUND_UP); + reset_strongly_closed(); + } + } + PPL_ASSERT(OK()); }

@@ -7593,21 +7610,40 @@ Octagonal_Shape<T> if (marked_empty()) return;

+ PPL_DIRTY_TEMP(N, temp_one); + assign_r(temp_one, 1, ROUND_NOT_NEEDED); + const Variables_Set::const_iterator v_begin = vars.begin(); const Variables_Set::const_iterator v_end = vars.end(); PPL_ASSERT(v_begin != v_end); typedef typename OR_Matrix<N>::row_reference_type Row_Reference; for (Variables_Set::const_iterator v_i = v_begin; v_i != v_end; ++v_i) { - const dimension_type i = *v_i; - Row_Reference m_i = matrix[i]; + const dimension_type i = 2 * (*v_i); const dimension_type ci = i + 1; + Row_Reference m_i = matrix[i]; Row_Reference m_ci = matrix[ci]; - // Unary constaints. - drop_some_non_integer_points_helper(m_i[ci]); - drop_some_non_integer_points_helper(m_ci[i]); - // Binary constraint (note: only consider j < i). + + // Unary constaints: should be even integers. + N& m_i_ci = m_i[ci]; + if (!is_plus_infinity(m_i_ci)) { + drop_some_non_integer_points_helper(m_i_ci); + if (!is_even(m_i_ci)) { + sub_assign_r(m_i_ci, m_i_ci, temp_one, ROUND_UP); + reset_strongly_closed(); + } + } + N& m_ci_i = m_ci[i]; + if (!is_plus_infinity(m_ci_i)) { + drop_some_non_integer_points_helper(m_ci_i); + if (!is_even(m_ci_i)) { + sub_assign_r(m_ci_i, m_ci_i, temp_one, ROUND_UP); + reset_strongly_closed(); + } + } + + // Binary constraints (note: only consider j < i). for (Variables_Set::const_iterator v_j = v_begin; v_j != v_i; ++v_j) { - const dimension_type j = *v_j; + const dimension_type j = 2 * (*v_j); const dimension_type cj = j + 1; drop_some_non_integer_points_helper(m_i[j]); drop_some_non_integer_points_helper(m_i[cj]); diff --git a/tests/Octagonal_Shape/dropsomenonintegerpoints1.cc b/tests/Octagonal_Shape/dropsomenonintegerpoints1.cc index f5dca86..588c858 100644 --- a/tests/Octagonal_Shape/dropsomenonintegerpoints1.cc +++ b/tests/Octagonal_Shape/dropsomenonintegerpoints1.cc @@ -154,7 +154,7 @@ test06() { Variable A(0); Variable B(1);

- Octagonal_Shape<mpq_class>os(2); + Octagonal_Shape<mpq_class> os(2); os.add_constraint(2*A <= 1); os.add_constraint(2*B <= -1); os.add_constraint(4*A - 4*B <= 7); @@ -163,7 +163,12 @@ test06() {

os.drop_some_non_integer_points();

- bool ok = true; //(os1 == os2); + Octagonal_Shape<mpq_class> known_result(2); + known_result.add_constraint(A <= 0); + known_result.add_constraint(B <= -1); + known_result.add_constraint(A - B <= 1); + + bool ok = (os == known_result);

print_constraints(os, "*** after os.drop_some_non_integer_points() ***");

@@ -190,11 +195,12 @@ test07() { Octagonal_Shape<mpq_class> known_result(2); known_result.add_constraint(A >= 1); known_result.add_constraint(2*B >= -1); - known_result.add_constraint(2*A + 2*B >= 1); + known_result.add_constraint(2*A - 2*B >= 1);

bool ok = (os == known_result);

- print_constraints(os, "*** after os.drop_some_non_integer_points() ***"); + print_constraints(os, + "*** after os.drop_some_non_integer_points(varset_A) ***");

return ok; } @@ -311,7 +317,7 @@ test12() { Variables_Set varset_A; varset_A.insert(A);

- Octagonal_Shape<mpq_class>os(2); + Octagonal_Shape<mpq_class> os(2); os.add_constraint(2*A <= 1); os.add_constraint(2*B <= -1); os.add_constraint(4*A - 4*B <= 7); @@ -320,9 +326,15 @@ test12() {

os.drop_some_non_integer_points(varset_A);

- bool ok = true; //(os1 == os2); + Octagonal_Shape<mpq_class> known_result(2); + known_result.add_constraint(A <= 0); + known_result.add_constraint(2*B <= -1); + known_result.add_constraint(4*A - 4*B <= 7);

- print_constraints(os, "*** after os.drop_some_non_integer_points() ***"); + bool ok = (os == known_result); + + print_constraints(os, + "*** after os.drop_some_non_integer_points(varset_A) ***");

return ok; } @@ -330,16 +342,16 @@ test12() { } // namespace

BEGIN_MAIN - DO_TEST_F(test01); + DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - DO_TEST_F(test05); + DO_TEST(test05); DO_TEST(test06); - DO_TEST_F(test07); + DO_TEST(test07); DO_TEST(test08); DO_TEST(test09); DO_TEST(test10); -// DO_TEST(test11); + DO_TEST(test11); DO_TEST(test12); END_MAIN