Module: ppl/ppl Branch: master Commit: f184d82d2e3105d671a089a1302ed6dff993a395 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f184d82d2e310... Author: Patricia Hill <p.m.hill@leeds.ac.uk> Date: Tue May 19 07:40:39 2009 +0100 Where cost is negligible, enforce integrality. --- src/Grid_public.cc | 68 +++++++++++++++++++++++--------- tests/Grid/wrap1.cc | 108 ++++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 156 insertions(+), 20 deletions(-) diff --git a/src/Grid_public.cc b/src/Grid_public.cc index 1e0919f..7aa5e71 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2704,58 +2704,73 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); + // Find the frequency and a value for `x' in `gr'. if (!gr.frequency_no_check(x, f_n, f_d, v_n, v_d)) continue; if (f_n == 0) { // `x' is a constant in `gr'. - if ((v_n > max_value * v_d) || (v_n < min_value * v_d)) { + if (v_d != 1) { + // The value for `x' is not integral (`frequency_no_check()' + // ensures that `v_n' and `v_d' have no common divisors). + set_empty(); + return; + } + + // `x' is a constant and has an integral value. + if ((v_n > max_value) || (v_n < min_value)) { // The value is outside the range of the bounded integer type. if (o == OVERFLOW_IMPOSSIBLE) { - // Then `x' has no possible value and hence `gr' is set empty. + // Then `x' has no possible value and hence set empty. set_empty(); return; } assert(o == OVERFLOW_WRAPS); // The value v_n for `x' is wrapped modulo the 'wrap_frequency'. - Coefficient& wrap_modulus = f_n; - wrap_modulus = v_d * wrap_frequency; - v_n %= wrap_modulus; + v_n %= wrap_frequency; // `v_n' is the value closest to 0 and may be negative. if (r == UNSIGNED && v_n < 0) - v_n += wrap_modulus; + v_n += wrap_frequency; unconstrain(x); - add_constraint(v_d * x == v_n); + add_constraint(x == v_n); } continue; } // `x' is not a constant in `gr'. assert(f_n != 0); - Coefficient& wrap_modulus = f_n; - f_d_wrap_frequency = f_d * wrap_frequency; - if (o == OVERFLOW_WRAPS && f_n != f_d * wrap_frequency) + + if (f_d % v_d != 0) { + // Then `x' has no integral value and hence `gr' is set empty. + set_empty(); + return; + } + if (f_d != 1) { + // `x' has non-integral values, so add the integrality + // congruence for `x'. + add_congruence((x %= 0) / 1); + } + if (o == OVERFLOW_WRAPS && f_n != wrap_frequency) // We know that `x' is not a constant, so, if overflow wraps, // `x' may wrap to a value modulo the `wrap_frequency'. add_grid_generator(parameter(wrap_frequency * x)); - else if ((o == OVERFLOW_IMPOSSIBLE && 2*f_n >= f_d_wrap_frequency) - || (f_n == f_d_wrap_frequency)) { + else if ((o == OVERFLOW_IMPOSSIBLE && 2*f_n >= wrap_frequency) + || (f_n == wrap_frequency)) { // In these cases, `x' can only take a unique (ie constant) // value. if (r == UNSIGNED && v_n < 0) { // `v_n' is the value closest to 0 and may be negative. - v_n *= f_d; - add_mul_assign(v_n, f_n, v_d); - v_d *= f_d; + v_n += f_n; } - add_constraint(v_d * x == v_n); + unconstrain(x); + add_constraint(x == v_n); } else // If overflow is impossible but the grid frequency is less than // half the wrap frequency, then there is more than one possible // value for `x' in the range of the bounded integer type, // so the grid is unchanged. - assert(o == OVERFLOW_IMPOSSIBLE && 2*f_n < f_d_wrap_frequency); + assert(o == OVERFLOW_IMPOSSIBLE && 2*f_n < wrap_frequency); } return; } @@ -2763,7 +2778,7 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, assert(o == OVERFLOW_UNDEFINED); // If overflow is undefined, then all we know is that the variable // may take any integer within the range of the bounded integer type. - const Grid_Generator& point = gen_sys[0]; + const Grid_Generator& point = gr.gen_sys[0]; const Coefficient& div = point.divisor(); max_value *= div; min_value *= div; @@ -2774,11 +2789,26 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // `x' is not a constant in `gr'. // We know that `x' is not a constant, so `x' may wrap to any // value `x + z' where z is an integer. - add_grid_generator(parameter(x)); + if (point.coefficient(x) % div != 0) { + // We know that `x' can take non-integral values, so enforce + // integrality. + unconstrain(x); + add_congruence(x %= 0); + } + else + // `x' has at least one integral value. + // `x' may also take other non-integral values, + // but checking could be costly so we ignore this. + add_grid_generator(parameter(x)); } else { // `x' is a constant `v' in `gr'. const Coefficient& coeff_x = point.coefficient(x); + // `x' should be integral. + if (coeff_x % div != 0) { + set_empty(); + return; + } // If the value `v' for `x' is not within the range for the // bounded integer type, then `x' may wrap to any value `v + z' // where `z' is an integer; otherwise `x' is unchanged. diff --git a/tests/Grid/wrap1.cc b/tests/Grid/wrap1.cc index cf45a97..59094ac 100644 --- a/tests/Grid/wrap1.cc +++ b/tests/Grid/wrap1.cc @@ -86,7 +86,7 @@ test03() { Grid known_result(2); known_result.add_congruence(x %= 0); - known_result.add_congruence((x + 24 %= 8*y) / 255); + known_result.add_congruence((32*x + 3 %= y) / 255); bool ok = (gr == known_result); @@ -407,6 +407,108 @@ test15() { } +bool +test16() { + Variable x(0); + Variable y(1); + + Grid gr1(2); + gr1.add_congruence((2*x %= 245) / 0); + Grid gr2(gr1); + + Variables_Set vars(x); + + gr1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + gr2.wrap_assign(vars, BITS_8, SIGNED_2_COMPLEMENT, OVERFLOW_WRAPS); + + Grid known_result1(2, EMPTY); + Grid known_result2(2, EMPTY); + + bool ok = (gr1 == known_result1 && gr2 == known_result2); + + print_congruences(gr1, "*** gr1.wrap_assign(...) ***"); + print_congruences(gr2, "*** gr2.wrap_assign(...) ***"); + + return ok; +} + +bool +test17() { + Variable x(0); + Variable y(1); + + Grid gr1(2); + gr1.add_congruence((4*x %= 3) / 2); + Grid gr2(gr1); + + Variables_Set vars(x); + + gr1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + gr2.wrap_assign(vars, BITS_8, SIGNED_2_COMPLEMENT, OVERFLOW_WRAPS); + + Grid known_result1(2, EMPTY); + Grid known_result2(2, EMPTY); + + bool ok = (gr1 == known_result1 && gr2 == known_result2); + + print_congruences(gr1, "*** gr1.wrap_assign(...) ***"); + print_congruences(gr2, "*** gr2.wrap_assign(...) ***"); + + return ok; +} + +bool +test18() { + Variable x(0); + Variable y(1); + + Grid gr1(2); + gr1.add_congruence((4*x %= 2) / 1); + Grid gr2(gr1); + + Variables_Set vars(x); + + gr1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + gr2.wrap_assign(vars, BITS_8, SIGNED_2_COMPLEMENT, OVERFLOW_WRAPS); + + Grid known_result1(2); + known_result1.add_congruence((x %= 0) / 1); + Grid known_result2(2); + known_result2.add_congruence((x %= 0) / 1); + + bool ok = (gr1 == known_result1 && gr2 == known_result2); + + print_congruences(gr1, "*** gr1.wrap_assign(...) ***"); + print_congruences(gr2, "*** gr2.wrap_assign(...) ***"); + + return ok; +} + +bool +test19() { + Variable x(0); + Variable y(1); + + Grid gr1(2); + gr1.add_congruence((2*x %= 245) / 0); + Grid gr2(gr1); + + Variables_Set vars(x, y); + + gr1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + gr2.wrap_assign(vars, BITS_8, SIGNED_2_COMPLEMENT, OVERFLOW_UNDEFINED); + + Grid known_result1(2, EMPTY); + Grid known_result2(2, EMPTY); + + bool ok = (gr1 == known_result1 && gr2 == known_result2); + + print_congruences(gr1, "*** gr1.wrap_assign(...) ***"); + print_congruences(gr2, "*** gr2.wrap_assign(...) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -425,4 +527,8 @@ BEGIN_MAIN DO_TEST_F8(test13); DO_TEST_F8(test14); DO_TEST_F8(test15); + DO_TEST_F8(test16); + DO_TEST_F8(test17); + DO_TEST_F8(test18); + DO_TEST_F8(test19); END_MAIN