May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Merge branch 'gridwraps'
by Patricia Hill 19 May '09

19 May '09

Module: ppl/ppl Branch: master Commit: 3ef5a5122c7d9a50b3a96fce36c9d9d033393e5f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ef5a5122c7d… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue May 19 07:42:41 2009 +0100 Merge branch 'gridwraps' ---

1 0

[GIT] ppl/ppl(master): Where cost is negligible, enforce integrality.
by Patricia Hill 19 May '09

19 May '09

Module: ppl/ppl Branch: master Commit: f184d82d2e3105d671a089a1302ed6dff993a395 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f184d82d2e31… Author: Patricia Hill <p.m.hill(a)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

1 0

[GIT] ppl/ppl(master): The refine_with_congrueces() detects inconsistent equalities.
by Patricia Hill 19 May '09

19 May '09

Module: ppl/ppl Branch: master Commit: a7fe4a03836b380714189d0006eeb9448a0e43a3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7fe4a03836b… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 18 14:21:42 2009 +0100 The refine_with_congrueces() detects inconsistent equalities. --- tests/Box/congruences1.cc | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/Box/congruences1.cc b/tests/Box/congruences1.cc index 39158d0..ed1be18 100644 --- a/tests/Box/congruences1.cc +++ b/tests/Box/congruences1.cc @@ -142,16 +142,14 @@ test06() { Congruence_System cgs; cgs.insert((A %= 7) / 0); cgs.insert((B %= 3) / 0); - // This inconsistent equality is ignored when refining. + // This inconsistent equality is not ignored when refining. cgs.insert((A + B %= 0) / 0); cgs.insert(C %= 7); TBox box(cgs.space_dimension(), UNIVERSE); box.refine_with_congruences(cgs); - Rational_Box known_result(3); - known_result.add_constraint(A == 7); - known_result.add_constraint(B == 3); + Rational_Box known_result(3, EMPTY); bool ok = check_result(box, known_result);

1 0

[GIT] ppl/ppl(master): Fixed omitted renaming.
by Abramo Bagnara 19 May '09

19 May '09

Module: ppl/ppl Branch: master Commit: 0fa67508390338eaa04737e01a2b5b7aaef34237 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0fa675083903… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Mon May 18 18:25:19 2009 +0200 Fixed omitted renaming. --- src/checked_float.inlines.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 92455b9..078b536 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -598,7 +598,7 @@ struct Float_2exp { template <typename To_Policy, typename From_Policy, typename Type> inline Result add_2exp_float(Type& to, const Type x, unsigned int exp, Rounding_Dir dir) { - if (To_Policy::check_nan_result && is_nan<From_Policy>(x)) + if (To_Policy::fpu_check_nan_result && is_nan<From_Policy>(x)) return assign_special<To_Policy>(to, VC_NAN, ROUND_IGNORE); assert(exp < sizeof(unsigned long long) * CHAR_BIT); return @@ -611,7 +611,7 @@ add_2exp_float(Type& to, const Type x, unsigned int exp, Rounding_Dir dir) { template <typename To_Policy, typename From_Policy, typename Type> inline Result sub_2exp_float(Type& to, const Type x, unsigned int exp, Rounding_Dir dir) { - if (To_Policy::check_nan_result && is_nan<From_Policy>(x)) + if (To_Policy::fpu_check_nan_result && is_nan<From_Policy>(x)) return assign_special<To_Policy>(to, VC_NAN, ROUND_IGNORE); assert(exp < sizeof(unsigned long long) * CHAR_BIT); return

1 0

[GIT] ppl/ppl(master): The generated Java tests now exploit the Test_Executor class functionality .
by Enea Zaffanella 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: 947e19e6567f08472cf79dd16e02106a84424d14 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=947e19e6567f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 15:47:00 2009 +0200 The generated Java tests now exploit the Test_Executor class functionality. Added an helper function to set global success flag and report success or failure if in noisy mode. NOTE: we are still (just) checking for the well formedness of the object (using method OK()), rather than checking if the computed result is actually the same of th expected one. However, due to genericity, it is quite difficult to precisely state expectations in these tests. --- .../ppl_interface_generator_java_test_java.m4 | 30 +- .../ppl_interface_generator_java_test_java_code.m4 | 317 ++++--------------- interfaces/Java/tests/ppl_java_tests_common | 68 +++-- 3 files changed, 121 insertions(+), 294 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=947e19e6…

1 0

[GIT] ppl/ppl(master): When the congruences have inconsistent equalities, the box is set empty.
by Patricia Hill 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: 2239f1dbbfa678802ba445dcb5c91930e1776472 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2239f1dbbfa6… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 18 14:24:58 2009 +0100 When the congruences have inconsistent equalities, the box is set empty. --- tests/Box/congruences1.cc | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/Box/congruences1.cc b/tests/Box/congruences1.cc index 39158d0..ed1be18 100644 --- a/tests/Box/congruences1.cc +++ b/tests/Box/congruences1.cc @@ -142,16 +142,14 @@ test06() { Congruence_System cgs; cgs.insert((A %= 7) / 0); cgs.insert((B %= 3) / 0); - // This inconsistent equality is ignored when refining. + // This inconsistent equality is not ignored when refining. cgs.insert((A + B %= 0) / 0); cgs.insert(C %= 7); TBox box(cgs.space_dimension(), UNIVERSE); box.refine_with_congruences(cgs); - Rational_Box known_result(3); - known_result.add_constraint(A == 7); - known_result.add_constraint(B == 3); + Rational_Box known_result(3, EMPTY); bool ok = check_result(box, known_result);

1 0

[GIT] ppl/ppl(master): Started adapting the Java tests to make better use of class Test_Executor.
by Enea Zaffanella 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: 5b6358d380c87210fc20c961e3b0d22597fca275 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5b6358d380c8… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 13:48:05 2009 +0200 Started adapting the Java tests to make better use of class Test_Executor. --- interfaces/Java/tests/C_Polyhedron_test1.java | 30 +++++++-------- interfaces/Java/tests/MIP_Problem_test1.java | 13 +++---- interfaces/Java/tests/NNC_Polyhedron_test1.java | 23 +++++++----- .../Java/tests/Parma_Polyhedra_Library_test1.java | 2 +- .../Java/tests/Parma_Polyhedra_Library_test2.java | 17 ++++----- interfaces/Java/tests/Test_Executor.java | 38 ++++++++++--------- 6 files changed, 62 insertions(+), 61 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5b6358d3…

1 0

[GIT] ppl/ppl(products): New commits
by Roberto Bagnara 18 May '09

18 May '09

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=49a4bf80ee99… Merge: 7d94d1213ad812f7d2a1cec93763247bdab22d34 badd595a0c22e91f4f1653ff8c7d53a3bf15ec50 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 13:47:31 2009 +0200 Merge branch 'master' into products URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=badd595a0c22… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 18 12:05:10 2009 +0100 Improved the methods refine_with_congruence[s](). Congruences can now refine the box even when the congruence is not non-relational. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b827904975bb… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 18 11:26:03 2009 +0100 Improved the relation_with(Congruence) implementation for the weakly relational domains. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e8ea60a5e953… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 11:18:40 2009 +0200 New tests for Polyhedron::wrap_assign(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=79c098635956… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 10:22:09 2009 +0200 Known result for test03() corrected; test now marked to succeed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=656fbd60bb14… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 10:17:59 2009 +0200 First draft of Box::wrap_assign() is now operational. Added a few tests. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a1c80c743c7c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 10:13:53 2009 +0200 Fixed a bug in wrap_assign_col(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=21df1e86b0b5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 08:59:11 2009 +0200 Added a test showing a bug in wrap_assign when wrap_individually == false. Test is test20(), temporarily marked as an expected failure. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=beee742bea10… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 08:20:34 2009 +0200 8-bit coefficients are now enough for test07(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b8bd2d5df01c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 08:16:34 2009 +0200 Added declarations and stub implementations for drop_some_non_integer_points(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5a29f32dbb8b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun May 17 17:42:14 2009 +0200 Finished the documentation about the wrapping operator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4335c8f28a36… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 17 16:42:56 2009 +0200 Rounding direction is not relevant here. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a171dbe14ee… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 17 14:55:14 2009 +0200 Get rid of a comparison warning. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a30eaca4651e… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 17 11:41:21 2009 +0200 Simplified code. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c3dd71f3d2a0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun May 17 08:44:42 2009 +0200 Added more in the section about the wrapping operator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=abda7dc37e19… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 22:25:18 2009 +0200 More work on the documentation of approximations for bounded integer arithmetic. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ead00b0ac972… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 21:08:08 2009 +0200 Bounded_Integer_Type_Signedness renamed Bounded_Integer_Type_Representation. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=64ad90df3806… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 14:11:38 2009 +0200 Comments improved. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f04ae2cea940… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 12:05:35 2009 +0200 Started writing the section on approximating bounded arithmetic. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f28c8bf97087… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat May 16 12:04:14 2009 +0200 Further cleaning of relation_with(Congruence) implementations. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f62a4633701e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat May 16 09:16:46 2009 +0200 Improved a few timeout and exception tests. Make sure an out_of_memory exception is thrown as expected even when a large amount of memory is available. Do not set timeouts out of catch constructs. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a169691f1a9d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 08:57:00 2009 +0200 test19() must fail with 8-bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4b6d78c1026c… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sat May 16 08:25:03 2009 +0200 These tests fails with 16 bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c6576478c6ad… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 06:54:56 2009 +0200 Item removed: no big deal. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fd53aaf53c5… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 21:32:37 2009 +0200 The test fails also with 32 bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1c9efaf9e303… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 21:08:49 2009 +0200 FIXME resolved. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4496b18b54f3… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 20:48:56 2009 +0200 The test fails also with 32 bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30f456f032cf… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 19:45:25 2009 +0200 Fixed the generic implementation of wrap_assign(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4845f4d529da… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 18:27:01 2009 +0200 A strict relation info is required here too. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ab230a684a4d… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 18:22:02 2009 +0200 A strict relation info is required here. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=01d418b28136… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:51:14 2009 +0200 Fixed a typo. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1734ba44f5b5… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:23:19 2009 +0200 Added an assert(false) for unreachable code. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dbac03988bc9… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:22:21 2009 +0200 Avoid two warnings. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ec4eb24ac15… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:15:47 2009 +0200 Renamed and commented ROUND_STRICT_RELATION. Added some use of it. Added some optimizations when ROUND_NOT_NEEDED is specified. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eca9369a8272… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 15:40:35 2009 +0200 Improved method Polyhedron::relation_with(const Congruence&) const. Avoided several temporary objects; added a FIXME asking for the rounding mode. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=99eba6af0276… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 15:28:11 2009 +0200 Fixed the invocation of the generic implementation of wrap_assign(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=baa08eff6430… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 15:12:50 2009 +0200 Check that all variables upon which `*pcs' depends are in `vars'. An assertion is violated otherwise. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=db4eb892c038… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 14:54:23 2009 +0200 Several improvements to Octagonal_Shape<T>::relation_with(const Congruence&). Alaso added a couple of FIXME regarding missing comments and rounding modes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=72619d2aafd0… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 14:48:24 2009 +0200 Corrected typo in explanatory output. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1736b8c74e21… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 14:47:30 2009 +0200 Minor improvement. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d3d07f461687… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 14:50:43 2009 +0200 Fixed rounding. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cf2bebf45a8c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 14:30:05 2009 +0200 Changed the specification of wrap_assign(). If `*pcs' depends on variables not in `vars', the behavior is undefined. We perform only the quick test on space dimensions. In debugging mode we will check the condition thoroughly. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2cfd68c04c05… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 12:43:48 2009 +0200 Simplified a rounded assignment. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1b4760ed2114… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 12:30:24 2009 +0200 Permits to low level code to take benefits from knowing that result will be exact. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=68daf755d6f7… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 11:32:00 2009 +0200 Test fails with an overflow using 8 bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=96e74efed2e2… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 10:28:35 2009 +0200 Enable DEBUG_ROUND_NOT_NEEDED when assertions are enabled. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7c0a202b6d04… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 10:29:49 2009 +0200 Two tests fail with an overflow using 8 bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0d9773ebdcd9… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 10:09:52 2009 +0200 Improved comment for ROUND_NOT_NEEDED. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a28345ddb5a9… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 09:47:21 2009 +0200 Fixed DEBUG_ROUND_NOT_NEEDED. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a6dcbc984609… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 08:12:34 2009 +0200 Let the wrap_assign tests succeed until the specification is clarified. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=331d2714c64d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 08:00:30 2009 +0200 Added a note about the use of `assign' helper functions. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d286a5a4f475… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 07:46:59 2009 +0200 When wrapping no variable, do not ignore the optional constraint system. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fd333e0c585… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 14 23:35:26 2009 +0200 Added a few missing accessor methods to Java interface classes. Affected classes are Congruence, Generator and Grid_Generator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30dfe89368c3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 22:04:30 2009 +0200 Fixed the bug witnessed by test15(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=972db0c00eba… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 14 21:51:58 2009 +0200 Partially reverted changes 71e9992afa9bc049b93d0b29fd9dbe52ead850cf. The changes were not working on platforms where floating point rounding mode could not be set (e.g., ARM), even though rounding control is not actually needed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1eb58559607c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 21:53:56 2009 +0200 Temporarily marked test15() and test16() as expected to fail. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fa6ebeae31b4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 21:53:39 2009 +0200 Last commit partly undone. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=74ade8b7dbf1… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 14 21:05:22 2009 +0200 Adapted generic implementation of wrap_assign to model the rational case. Also added a couple of tests showing problems in the current implementation. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1db2683636da… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 14 15:46:36 2009 +0200 Use PPL_DIRTY_TEMP for temporary objects. Also corrected a type causing an assertion failure. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=92cfd0aae5bc… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 14 16:03:56 2009 +0200 Added missing clear. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=09bd1e66fee5… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 14 15:33:30 2009 +0200 Fixed typo. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7f20b6e3172f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 14 15:10:08 2009 +0200 Some progress on Box::wrap_assign(). Corrected a couple of typos in Interval::wrap_assign(). Silenced an annoying GCC warning. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b64080a7407e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 12:43:47 2009 +0200 Commits improved. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9f7260b5f092… Merge: c606710cfe67adb748857cfb840d20a2feb3a3b8 6c8a266be0f01266599542b7cdc3d3c2a47e62d2 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 12:36:18 2009 +0200 Merge branch 'bounded_arithmetic' URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6c8a266be0f0… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 14 09:41:30 2009 +0200 Silenced bogus comparison warnings. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9724ada507cd… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 14 10:11:31 2009 +0200 Added missing policy. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f922aa0fa152… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 14 08:45:36 2009 +0200 Added missing Result values. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6d905acbbe0a… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 14 08:28:05 2009 +0200 Fixed some typos. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e33e130ebcb9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 08:30:18 2009 +0200 New policy Debug_WRD_Extended_Number_Policy. This is the debugging policy for checked numbers used in weakly-relational domains. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8c4cee6feb0a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 08:12:12 2009 +0200 WRD_Extended_Number_Policy properly commented. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ffc6689ea022… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 14 07:10:26 2009 +0200 Marked tests that are expected to fail with 8-bit coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5f9892fcb2fc… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 13 23:42:29 2009 +0200 Added wrap_assign. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b55ca03354c3… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 13 23:41:38 2009 +0200 Added add_2exp and sub_2exp. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=37f8d8b4162a… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 13 23:33:01 2009 +0200 Added missing info clearing. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c606710cfe67… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Wed May 13 21:43:11 2009 +0100 Removed repeated specification of operators in the grids section. Ensure cross-references to these sections now refer to the equivalent sections for polyhedra. Fixed a typo in src/Determinate.defs.hh that caused a warning when compiling the documentation. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0edbd37a47bb… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 22:17:32 2009 +0200 Coefficient types of weakly-relational domains moved to new source files. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ee2d6c28172e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 21:29:11 2009 +0200 Comment fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bfc05d94ff20… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 20:29:09 2009 +0200 Got rid of Checked_Number_Default_Policy. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=76c766e5f4da… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 20:28:36 2009 +0200 Bounded_Integer_Coefficient_Policy::handle_result() commented. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6ea0b6f8a8ee… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 20:20:28 2009 +0200 Also check for NaN in Bounded_Integer_Coefficient_Policy::handle_result(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2ee98075c306… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 20:13:31 2009 +0200 Checked number policy parameter `check_nan_result' renamed `fpu_check_nan_result'. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0cb27e7158a1… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 13 20:05:05 2009 +0200 Fixed return type. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eb89cfe6722a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 20:01:01 2009 +0200 Use Bounded_Integer_Coefficient_Policy as the policy for checked coefficients. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a8f95c123cd3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 20:00:32 2009 +0200 Added Bounded_Integer_Coefficient_Policy. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=986d10992053… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 13 19:59:13 2009 +0200 Checked_Number_Transparent_Policy properly commented. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cbcb69446ece… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 13 11:39:15 2009 +0200 Fixed topological closure for unbounded intervals. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8c816f458ca9… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 13 11:48:59 2009 +0200 Reorganized and separated Result classes to be more informative. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ca38275a5e16… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Tue May 12 17:30:01 2009 +0200 Added smod_2exp and umod_2exp for boundary. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=80ba9754deb0… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 10 19:30:17 2009 +0200 Added umod_2exp and smod_2exp to checked numbers. Fixed rem for mpq to work similarly to other numeric types. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=98fb9c3061d1… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat May 9 14:22:25 2009 +0200 Drafted specialized implementation for Box<ITV>::wrap_assign. Code still commented out as it relies on a missing Interval method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=306db9d46d07… Merge: 7309a3a239bc75074827c6c61bd0df2b278088df 317f48d0d55391b07624e0f55a6228e3b2d39d6f Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue May 5 19:22:47 2009 +0200 Merge branch 'master' into bounded_arithmetic URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7309a3a239bc… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Tue May 5 13:59:21 2009 +0200 Fixed typo on assertion. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=962d7b0a74ec… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Tue May 5 10:47:36 2009 +0200 Added Circular Integer intervals.

1 0

[GIT] ppl/ppl(master): Improved the methods refine_with_congruence[s]().
by Patricia Hill 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: badd595a0c22e91f4f1653ff8c7d53a3bf15ec50 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=badd595a0c22… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 18 12:05:10 2009 +0100 Improved the methods refine_with_congruence[s](). Congruences can now refine the box even when the congruence is not non-relational. --- src/Box.templates.hh | 19 +--- tests/Box/Makefile.am | 7 +- tests/Box/refinewithcongruence1.cc | 194 ++++++++++++++++++++++++++++++++++++ 3 files changed, 201 insertions(+), 19 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 3f311fa..9918363 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -2192,23 +2192,8 @@ Box<ITV>::refine_no_check(const Congruence& cg) { } assert(cg.is_equality()); - dimension_type cg_num_vars = 0; - dimension_type cg_only_var = 0; - // Congruences that are not interval congruences are ignored. - if (!extract_interval_congruence(cg, cg_space_dim, cg_num_vars, cg_only_var)) - return; - - if (cg_num_vars == 0) { - // Dealing with a trivial congruence. - if (cg.inhomogeneous_term() != 0) - set_empty(); - return; - } - - assert(cg_num_vars == 1); - const Coefficient& n = cg.inhomogeneous_term(); - const Coefficient& d = cg.coefficient(Variable(cg_only_var)); - add_interval_constraint_no_check(cg_only_var, Constraint::EQUALITY, n, d); + Constraint c(cg); + refine_no_check(c); } template <typename ITV> diff --git a/tests/Box/Makefile.am b/tests/Box/Makefile.am index 4b53895..965ee15 100644 --- a/tests/Box/Makefile.am +++ b/tests/Box/Makefile.am @@ -100,6 +100,7 @@ propagateconstraints1 propagateconstraints2 \ relations1 relations2 relations3 relations4 \ refinewithconstraint1 refinewithconstraint2 \ refinewithconstraints1 \ +refinewithcongruence1 \ refinewithcongruences1 \ removespacedims1 \ simplifyusingcontext1 \ @@ -256,13 +257,15 @@ relations4_SOURCES = relations4.cc propagateconstraints1_SOURCES = propagateconstraints1.cc propagateconstraints2_SOURCES = propagateconstraints2.cc +refinewithcongruence1_SOURCES = refinewithcongruence1.cc + +refinewithcongruences1_SOURCES = refinewithcongruences1.cc + refinewithconstraint1_SOURCES = refinewithconstraint1.cc refinewithconstraint2_SOURCES = refinewithconstraint2.cc refinewithconstraints1_SOURCES = refinewithconstraints1.cc -refinewithcongruences1_SOURCES = refinewithcongruences1.cc - removespacedims1_SOURCES = removespacedims1.cc simplifyusingcontext1_SOURCES = simplifyusingcontext1.cc diff --git a/tests/Box/refinewithcongruence1.cc b/tests/Box/refinewithcongruence1.cc new file mode 100644 index 0000000..bba4477 --- /dev/null +++ b/tests/Box/refinewithcongruence1.cc @@ -0,0 +1,194 @@ +/* Test Box::refine_with_congruences(const Congruence_System&). + Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +// Universe Box, zero dimensions and trivial congruence. +bool +test01() { + Congruence cg(Linear_Expression(0) %= 1); + TBox box(0); + box.refine_with_congruence(cg); + + Rational_Box known_result(0); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// Universe Box, 4 dimensions and refine with a proper congruence +bool +test02() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + + Congruence cg(A + B %= 0); + TBox box(4); + box.refine_with_congruence(cg); + + Rational_Box known_result(4); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// Universe Box in 3D and refine with an equality congruence. +bool +test03() { + Variable A(0); + Variable B(1); + Variable C(2); + + Congruence cg((A %= 7) / 0); + + TBox box(3); + box.refine_with_congruence(cg); + + Rational_Box known_result(3); + known_result.add_constraint(A == 7); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// Box in 1D and refine with an inconsistent proper congruence. +bool +test04() { + Variable A(0); + + Congruence cg((0*A %= 1) / 2); + + TBox box(1); + box.refine_with_congruence(cg); + + Rational_Box known_result(1, EMPTY); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// refine_with_congruence() +bool +test05() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + + Constraint_System cs; + cs.insert(A <= 5); + cs.insert(A >= 0); + cs.insert(B <= 5); + cs.insert(B >= 0); + cs.insert(C <= 5); + cs.insert(C >= 0); + cs.insert(D <= 5); + cs.insert(D >= 0); + TBox box(cs); + box.refine_with_congruence((1*A + 2*B + 3*C + 4*D %= 0) / 0); + + Constraint_System known_cs; + known_cs.insert(A == 0); + known_cs.insert(B == 0); + known_cs.insert(C == 0); + known_cs.insert(D == 0); + Rational_Box known_result(known_cs); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + + +bool +test06() { + Variable x(0); + Variable y(1); + Variable z(2); + + TBox box1(2); + + try { + // This is an invalid use of method + // Box::refine_with_congruence: it is illegal + // to refine with a congruence with bigger dimension. + box1.refine_with_congruence(x %= 0); + box1.refine_with_congruence(y - x + z %= 0); + } + catch (std::invalid_argument& e) { + nout << "std::invalid_argument: " << endl; + return true; + } + catch (...) { + } + return false; +} + +bool +test07() { + Variable y(1); + + TBox box(1); + + try { + // This is an invalid use of the method + // Box::refine_with_congruence(c): it is illegal to refine with a + // congruence that contains a variable that is not in the space + // of the box. + box.refine_with_congruence((y %= 0) / 0); + } + catch (std::invalid_argument& e) { + nout << "std::invalid_argument: " << endl; + return true; + } + catch (...) { + } + return false; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test07); +END_MAIN

1 0

[GIT] ppl/ppl(master): Improved the relation_with(Congruence) implementation for the weakly relational domains.
by Patricia Hill 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: b827904975bbeff4079fbb5aedf66a3ac4cb8e30 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b827904975bb… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 18 11:26:03 2009 +0100 Improved the relation_with(Congruence) implementation for the weakly relational domains. --- src/BD_Shape.templates.hh | 61 ++++++++++++++++++++++++++++++------- src/Octagonal_Shape.templates.hh | 58 ++++++++++++++++++++++++++++------- 2 files changed, 95 insertions(+), 24 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index eeafd27..819b99e 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -1209,8 +1209,8 @@ BD_Shape<T>::relation_with(const Congruence& cg) const { if (cg.space_dimension() > space_dim) throw_dimension_incompatible("relation_with(cg)", cg); - // If the congruence is a bounded difference equality, - // find the relation with the equivalent equality constraint. + // If the congruence is an equality, find the relation with + // the equivalent equality constraint. if (cg.is_equality()) { Constraint c(cg); return relation_with(c); @@ -1231,26 +1231,63 @@ BD_Shape<T>::relation_with(const Congruence& cg) const { && Poly_Con_Relation::is_included(); } - // FIXME: add proper comments to the following. + // Find the lower bound for a hyperplane with direction + // defined by the congruence. Linear_Expression le = Linear_Expression(cg); PPL_DIRTY_TEMP_COEFFICIENT(min_num); PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; bool bounded_below = minimize(le, min_num, min_den, min_included); + // If there is no lower bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - PPL_DIRTY_TEMP_COEFFICIENT(value); - value = min_num / min_den; - const Coefficient& modulus = cg.modulus(); + // TODO: Consider adding a max_and_min() method, performing both + // maximization and minimization so as to possibly exploit + // incrementality of the MIP solver. + + // Find the upper bound for a hyperplane with direction + // defined by the congruence. + PPL_DIRTY_TEMP_COEFFICIENT(max_num); + PPL_DIRTY_TEMP_COEFFICIENT(max_den); + bool max_included; + bool bounded_above = maximize(le, max_num, max_den, max_included); + + // If there is no upper bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. + if (!bounded_above) + return Poly_Con_Relation::strictly_intersects(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); - signed_distance = value % modulus; - value -= signed_distance; - if (value * min_den < min_num) - value += modulus; - Constraint c(le == value); - return relation_with(c); + + // Find the position value for the hyperplane that satisfies the congruence + // and is above the lower bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + min_value = min_num / min_den; + const Coefficient& modulus = cg.modulus(); + signed_distance = min_value % modulus; + min_value -= signed_distance; + if (min_value * min_den < min_num) + min_value += modulus; + + // Find the position value for the hyperplane that satisfies the congruence + // and is below the upper bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + max_value = max_num / max_den; + signed_distance = max_value % modulus; + max_value += signed_distance; + if (max_value * max_den > max_num) + max_value -= modulus; + + // If the upper bound value is less than the lower bound value, + // then there is an empty intersection with the congruence; + // otherwise it will strictly intersect. + if (max_value < min_value) + return Poly_Con_Relation::is_disjoint(); + else + return Poly_Con_Relation::strictly_intersects(); } diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index de6bab5..4d46ac7 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -1214,29 +1214,63 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { && Poly_Con_Relation::is_included(); } - // FIXME: the following code has to be checked and improved. - // Add comment to explain what we are doing and why. + // Find the lower bound for a hyperplane with direction + // defined by the congruence. Linear_Expression le = Linear_Expression(cg); PPL_DIRTY_TEMP_COEFFICIENT(min_num); PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; bool bounded_below = minimize(le, min_num, min_den, min_included); + // If there is no lower bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - // FIXME: specify rounding mode. - PPL_DIRTY_TEMP_COEFFICIENT(value); - value = min_num / min_den; + // TODO: Consider adding a max_and_min() method, performing both + // maximization and minimization so as to possibly exploit + // incrementality of the MIP solver. + + // Find the upper bound for a hyperplane with direction + // defined by the congruence. + PPL_DIRTY_TEMP_COEFFICIENT(max_num); + PPL_DIRTY_TEMP_COEFFICIENT(max_den); + bool max_included; + bool bounded_above = maximize(le, max_num, max_den, max_included); + + // If there is no upper bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. + if (!bounded_above) + return Poly_Con_Relation::strictly_intersects(); - const Coefficient& modulus = cg.modulus(); PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); - signed_distance = value % modulus; - value -= signed_distance; - if (value * min_den < min_num) - value += modulus; - Constraint c(le == value); - return relation_with(c); + + // Find the position value for the hyperplane that satisfies the congruence + // and is above the lower bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + min_value = min_num / min_den; + const Coefficient& modulus = cg.modulus(); + signed_distance = min_value % modulus; + min_value -= signed_distance; + if (min_value * min_den < min_num) + min_value += modulus; + + // Find the position value for the hyperplane that satisfies the congruence + // and is below the upper bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + max_value = max_num / max_den; + signed_distance = max_value % modulus; + max_value += signed_distance; + if (max_value * max_den > max_num) + max_value -= modulus; + + // If the upper bound value is less than the lower bound value, + // then there is an empty intersection with the congruence; + // otherwise it will strictly intersect. + if (max_value < min_value) + return Poly_Con_Relation::is_disjoint(); + else + return Poly_Con_Relation::strictly_intersects(); } template <typename T>

1 0