May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(products): Added two tests based on the examples 5(a), 5(b) in SenS07.
by Patricia Hill 14 May '09

14 May '09

Module: ppl/ppl Branch: products Commit: 7d519208391e933089c023ddf4d29e1b8b50f9c7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d519208391e… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu May 14 21:20:06 2009 +0100 Added two tests based on the examples 5(a), 5(b) in SenS07. Added print_constraints(const Affine_Space&) to ppl_test. --- .../constraintsproduct1.cc | 248 ++++++++++++++++++-- tests/ppl_test.cc | 6 + tests/ppl_test.hh | 5 + 3 files changed, 241 insertions(+), 18 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=7d519208…

1 0

[GIT] ppl/ppl(master): Fixed the bug witnessed by test15().
by Roberto Bagnara 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 30dfe89368c392d62339f5d962bef4e676ee61d7 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(). --- src/wrap_assign.hh | 7 +++++-- tests/Polyhedron/wrap1.cc | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 3ba5b96..10c2874 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -115,9 +115,12 @@ wrap_assign(PSET& pointset, throw std::invalid_argument(s.str()); } - // Wrapping no variable is a no-op. - if (vars.empty()) + // Wrapping no variable only requires refining with *pcs, if any. + if (vars.empty()) { + if (pcs != 0) + pointset.refine_with_constraints(*pcs); return; + } // Dimension-compatibility check of `vars'. if (space_dim < vars.space_dimension()) { diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 90b4ba8..23ddd5d 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -500,6 +500,6 @@ BEGIN_MAIN DO_TEST_F8(test12); DO_TEST_F16(test13); DO_TEST_F8(test14); - DO_TEST_F(test15); + DO_TEST(test15); DO_TEST_F(test16); END_MAIN

1 0

[GIT] ppl/ppl(master): Partially reverted changes 71e9992afa9bc049b93d0b29fd9dbe52ead850cf.
by Enea Zaffanella 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 972db0c00ebac6b9ad2d97ccd86707285c1a27d5 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. --- TODO | 2 ++ src/MIP_Problem.cc | 22 +++++++++++++++++++--- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/TODO b/TODO index f63140e..114ce6f 100644 --- a/TODO +++ b/TODO @@ -11,6 +11,8 @@ Enhancements for PPL 0.11 - Make all the *affine*image() methods uniform as far as the specification is concerned. - Check the use or the NOT_EQUAL Relation_Symbol everywhere. +- Get rid of ugly assign functions defined in anonymous namespace of + MIP_Problem.cc replacing it with a more general-purpose approach. - Reconsider the datatype for the units parameter in the Watchdog constructors: should we prefer an unsigned? - Intervals are best instantiated with checked numbers with diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index e26afe6..3e6bcab 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -855,6 +855,22 @@ PPL::MIP_Problem::process_pending_constraints() { return true; } +namespace { + +inline void +assign(double& d, const mpz_class& c) { + d = c.get_d(); +} + +template <typename T, typename Policy> +inline void +assign(double& d, + const Parma_Polyhedra_Library::Checked_Number<T, Policy>& c) { + d = raw_value(c); +} + +} // namespace + PPL::dimension_type PPL::MIP_Problem::steepest_edge_float_entering_index() const { const dimension_type tableau_num_rows = tableau.num_rows(); @@ -871,7 +887,7 @@ PPL::MIP_Problem::steepest_edge_float_entering_index() const { if (sgn(cost_j) == cost_sign) { // We cannot compute the (exact) square root of abs(\Delta x_j). // The workaround is to compute the square of `cost[j]'. - assign_r(challenger_num, cost_j, ROUND_IGNORE); + assign(challenger_num, cost_j); challenger_num = fabs(challenger_num); // Due to our integer implementation, the `1' term in the denominator // of the original formula has to be replaced by `squared_lcm_basis'. @@ -881,8 +897,8 @@ PPL::MIP_Problem::steepest_edge_float_entering_index() const { const Coefficient& tableau_ij = tableau_i[j]; if (tableau_ij != 0) { assert(tableau_i[base[i]] != 0); - assign_r(float_tableau_value, tableau_ij, ROUND_IGNORE); - assign_r(float_tableau_denum, tableau_i[base[i]], ROUND_IGNORE); + assign(float_tableau_value, tableau_ij); + assign(float_tableau_denum, tableau_i[base[i]]); float_tableau_value /= float_tableau_denum; challenger_den += float_tableau_value * float_tableau_value; }

1 0

[GIT] ppl/ppl(master): Temporarily marked test15() and test16() as expected to fail.
by Roberto Bagnara 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 1eb58559607caafc821eaaa564b6b211d7c9e243 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. --- tests/Polyhedron/wrap1.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index c99b59c..90b4ba8 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -500,6 +500,6 @@ BEGIN_MAIN DO_TEST_F8(test12); DO_TEST_F16(test13); DO_TEST_F8(test14); - DO_TEST(test15); - DO_TEST(test16); + DO_TEST_F(test15); + DO_TEST_F(test16); END_MAIN

1 0

[GIT] ppl/ppl(master): Last commit partly undone.
by Roberto Bagnara 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: fa6ebeae31b46566555455e579fdacd213340e99 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. --- src/wrap_assign.hh | 13 +++++++------ 1 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 8e98b82..3ba5b96 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -68,7 +68,7 @@ wrap_assign_rec(PSET& dest, vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); p.refine_with_constraint(min_value <= x); - p.refine_with_constraint(x < max_value); + p.refine_with_constraint(x <= max_value); } dest.upper_bound_assign(p); } @@ -135,17 +135,18 @@ wrap_assign(PSET& pointset, // Set `min_value' and `max_value' to the minimum and maximum values // a variable of width `w' and signedness `s' can take. - // NOTE: value is meant to range in [min_value, max_value). PPL_DIRTY_TEMP_COEFFICIENT(min_value); PPL_DIRTY_TEMP_COEFFICIENT(max_value); if (s == UNSIGNED) { min_value = 0; mul_2exp_assign(max_value, Coefficient_one(), w); + --max_value; } else { assert(s == SIGNED_2_COMPLEMENT); mul_2exp_assign(max_value, Coefficient_one(), w-1); neg_assign(min_value, max_value); + --max_value; } // If we are wrapping variables collectively, the ranges for the @@ -194,7 +195,7 @@ wrap_assign(PSET& pointset, set_full_range: pointset.unconstrain(x); full_range_bounds.insert(min_value <= x); - full_range_bounds.insert(x < max_value); + full_range_bounds.insert(x <= max_value); continue; } @@ -219,7 +220,7 @@ wrap_assign(PSET& pointset, if (first_quadrant < 0) full_range_bounds.insert(min_value <= x); if (last_quadrant > 0) - full_range_bounds.insert(x < max_value); + full_range_bounds.insert(x <= max_value); continue; } @@ -256,7 +257,7 @@ wrap_assign(PSET& pointset, const Variable& x = i->var; pointset.unconstrain(x); full_range_bounds.insert(min_value <= x); - full_range_bounds.insert(x < max_value); + full_range_bounds.insert(x <= max_value); } } } @@ -276,7 +277,7 @@ wrap_assign(PSET& pointset, if (pcs != 0) p.refine_with_constraints(*pcs); p.refine_with_constraint(min_value <= x); - p.refine_with_constraint(x < max_value); + p.refine_with_constraint(x <= max_value); hull.upper_bound_assign(p); } pointset.swap(hull);

1 0

[GIT] ppl/ppl(master): Adapted generic implementation of wrap_assign to model the rational case.
by Enea Zaffanella 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 74ade8b7dbf158e7473d8375c724e4a706506267 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. --- src/wrap_assign.hh | 15 +++++------ tests/Box/wrap1.cc | 24 ++++++++++---------- tests/Polyhedron/wrap1.cc | 54 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 73 insertions(+), 20 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 27ba7b0..8e98b82 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -68,7 +68,7 @@ wrap_assign_rec(PSET& dest, vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); p.refine_with_constraint(min_value <= x); - p.refine_with_constraint(x <= max_value); + p.refine_with_constraint(x < max_value); } dest.upper_bound_assign(p); } @@ -106,7 +106,7 @@ wrap_assign(PSET& pointset, bool wrap_individually) { const dimension_type space_dim = pointset.space_dimension(); // Dimension-compatibility check of `*pcs', if any. - if (pcs != 0 && pcs->space_dimension() != space_dim) { + if (pcs != 0 && pcs->space_dimension() > space_dim) { std::ostringstream s; // FIXME: how can we write the class name of PSET here? s << "PPL::...::wrap_assign(..., pcs, ...):" << std::endl @@ -135,18 +135,17 @@ wrap_assign(PSET& pointset, // Set `min_value' and `max_value' to the minimum and maximum values // a variable of width `w' and signedness `s' can take. + // NOTE: value is meant to range in [min_value, max_value). PPL_DIRTY_TEMP_COEFFICIENT(min_value); PPL_DIRTY_TEMP_COEFFICIENT(max_value); if (s == UNSIGNED) { min_value = 0; mul_2exp_assign(max_value, Coefficient_one(), w); - --max_value; } else { assert(s == SIGNED_2_COMPLEMENT); mul_2exp_assign(max_value, Coefficient_one(), w-1); neg_assign(min_value, max_value); - --max_value; } // If we are wrapping variables collectively, the ranges for the @@ -195,7 +194,7 @@ wrap_assign(PSET& pointset, set_full_range: pointset.unconstrain(x); full_range_bounds.insert(min_value <= x); - full_range_bounds.insert(x <= max_value); + full_range_bounds.insert(x < max_value); continue; } @@ -220,7 +219,7 @@ wrap_assign(PSET& pointset, if (first_quadrant < 0) full_range_bounds.insert(min_value <= x); if (last_quadrant > 0) - full_range_bounds.insert(x <= max_value); + full_range_bounds.insert(x < max_value); continue; } @@ -257,7 +256,7 @@ wrap_assign(PSET& pointset, const Variable& x = i->var; pointset.unconstrain(x); full_range_bounds.insert(min_value <= x); - full_range_bounds.insert(x <= max_value); + full_range_bounds.insert(x < max_value); } } } @@ -277,7 +276,7 @@ wrap_assign(PSET& pointset, if (pcs != 0) p.refine_with_constraints(*pcs); p.refine_with_constraint(min_value <= x); - p.refine_with_constraint(x <= max_value); + p.refine_with_constraint(x < max_value); hull.upper_bound_assign(p); } pointset.swap(hull); diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc index 15f7e79..f9e757f 100644 --- a/tests/Box/wrap1.cc +++ b/tests/Box/wrap1.cc @@ -41,10 +41,10 @@ test01() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); TBox known_result(2); - known_result.add_constraint(0 <= x); - known_result.add_constraint(x <= 255); - known_result.add_constraint(0 <= y); - known_result.add_constraint(y <= 255); + known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(x < 256); + known_result.refine_with_constraint(0 <= y); + known_result.refine_with_constraint(y < 256); bool ok = (box == known_result); @@ -74,10 +74,10 @@ test02() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); TBox known_result(2); - known_result.add_constraint(0 <= x); - known_result.add_constraint(x <= 255); - known_result.add_constraint(0 <= y); - known_result.add_constraint(y <= 50); + known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(x < 256); + known_result.refine_with_constraint(0 <= y); + known_result.refine_with_constraint(y <= 50); bool ok = (box == known_result); @@ -108,10 +108,10 @@ test03() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); TBox known_result(2); - known_result.add_constraint(0 <= x); - known_result.add_constraint(x <= 255); - known_result.add_constraint(0 <= y); - known_result.add_constraint(y <= 50); + known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(x < 256); + known_result.refine_with_constraint(0 <= y); + known_result.refine_with_constraint(y <= 50); bool ok = (box == known_result); diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 97beb08..c99b59c 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -431,6 +431,58 @@ test14() { return ok; } +bool +test15() { + C_Polyhedron ph(1); + print_constraints(ph, "*** ph ***"); + + Variables_Set vars; + + Variable x(0); + Constraint_System cs; + cs.insert(x == 10); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); + + C_Polyhedron known_result(1); + known_result.add_constraint(x == 10); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + +bool +test16() { + Variable x(0); + Variable y(1); + + C_Polyhedron ph(2); + ph.add_constraint(x == 256); + ph.add_constraint(y == 256 + 256 + 1); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + Constraint_System cs; + cs.insert(x + 1 == y); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); + + C_Polyhedron known_result(2); + known_result.add_constraint(x == 0); + known_result.add_constraint(y == 1); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -448,4 +500,6 @@ BEGIN_MAIN DO_TEST_F8(test12); DO_TEST_F16(test13); DO_TEST_F8(test14); + DO_TEST(test15); + DO_TEST(test16); END_MAIN

1 0

[GIT] ppl/ppl(master): Use PPL_DIRTY_TEMP for temporary objects.
by Enea Zaffanella 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 1db2683636da9c4439f72abc28bbeca65f880f8f 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. --- src/Box.inlines.hh | 4 ++-- src/Box.templates.hh | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Box.inlines.hh b/src/Box.inlines.hh index 665c180..c4a9888 100644 --- a/src/Box.inlines.hh +++ b/src/Box.inlines.hh @@ -406,9 +406,9 @@ Box<ITV>::refine_interval_no_check(ITV& itv, : LESS_THAN, q)); break; default: - // Silence an annoying GCC warning. - res = I_ANY; + // Silence an annoying GCC warning (should never reach this point). assert(false); + res = I_ANY; } assert(itv.OK()); return res; diff --git a/src/Box.templates.hh b/src/Box.templates.hh index dbe1a76..3cef96e 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1465,7 +1465,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, // FIXME: Build the quadrant interval. I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value); I_Constraint<Coefficient> upper = i_constraint(LESS_THAN, max_value); - ITV quadrant_itv; + PPL_DIRTY_TEMP(ITV, quadrant_itv); quadrant_itv.build(lower, upper); if (pcs == 0) { @@ -1497,11 +1497,11 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, // A map associating interval constraints to variable indexes. typedef std::map<dimension_type, std::vector<const Constraint*> > map_type; map_type var_cs_map; - dimension_type c_num_vars = 0; - dimension_type c_only_var = 0; for (Constraint_System::const_iterator i = cs.begin(), i_end = cs.end(); i != i_end; ++i) { const Constraint& c = *i; + dimension_type c_num_vars = 0; + dimension_type c_only_var = 0; if (extract_interval_constraint(c, cs_space_dim, c_num_vars, c_only_var)) { if (c_num_vars == 1) { @@ -1521,7 +1521,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, } } - ITV refinement_itv; + PPL_DIRTY_TEMP(ITV, refinement_itv); const map_type::const_iterator var_cs_map_end = var_cs_map.end(); // Loop through the variable indexes in `vars'. for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) {

1 0

[GIT] ppl/ppl(master): Added missing clear.
by Abramo Bagnara 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 92cfd0aae5bc460d30b0cdf2e4ccc98acdd6d4a2 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. --- src/Interval.defs.hh | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/Interval.defs.hh b/src/Interval.defs.hh index d0b71b1..bd52eb7 100644 --- a/src/Interval.defs.hh +++ b/src/Interval.defs.hh @@ -541,6 +541,7 @@ public: r = sub_2exp_assign_r(u, upper(), w, ROUND_UP); if (!result_overflow(r) && u > lower()) return assign(refinement); + info().clear(); switch (s) { case UNSIGNED: umod_2exp_assign(LOWER, lower(), info(),

1 0

[GIT] ppl/ppl(master): Fixed typo.
by Abramo Bagnara 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 09bd1e66fee53f1373417e9aa067d7c69e723cac 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. --- src/Boundary.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Boundary.defs.hh b/src/Boundary.defs.hh index 6e32424..6557099 100644 --- a/src/Boundary.defs.hh +++ b/src/Boundary.defs.hh @@ -733,7 +733,7 @@ inline Result umod_2exp_assign(Boundary_Type to_type, To& to, To_Info& to_info, Boundary_Type type, const T& x, const Info& info, unsigned int exp) { - assert(to_type != type); + assert(to_type == type); bool shrink; if (is_boundary_infinity(type, x, info)) { shrink = boundary_infinity_is_open(type, info); @@ -751,7 +751,7 @@ inline Result smod_2exp_assign(Boundary_Type to_type, To& to, To_Info& to_info, Boundary_Type type, const T& x, const Info& info, unsigned int exp) { - assert(to_type != type); + assert(to_type == type); bool shrink; if (is_boundary_infinity(type, x, info)) { shrink = boundary_infinity_is_open(type, info);

1 0

[GIT] ppl/ppl(master): Some progress on Box::wrap_assign().
by Enea Zaffanella 14 May '09

14 May '09

Module: ppl/ppl Branch: master Commit: 7f20b6e3172fb478fa38d4c71d84637a91138abd 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. --- src/Box.inlines.hh | 4 ++ src/Box.templates.hh | 79 ++++++++++++++++++++++++++++++++++---------------- src/Interval.defs.hh | 8 ++-- 3 files changed, 62 insertions(+), 29 deletions(-) diff --git a/src/Box.inlines.hh b/src/Box.inlines.hh index d71dd17..665c180 100644 --- a/src/Box.inlines.hh +++ b/src/Box.inlines.hh @@ -405,6 +405,10 @@ Box<ITV>::refine_interval_no_check(ITV& itv, ? GREATER_THAN : LESS_THAN, q)); break; + default: + // Silence an annoying GCC warning. + res = I_ANY; + assert(false); } assert(itv.OK()); return res; diff --git a/src/Box.templates.hh b/src/Box.templates.hh index abfb9d9..dbe1a76 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1440,24 +1440,52 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, // Dimension-compatibility check. const dimension_type vars_space_dim = vars.space_dimension(); if (space_dim < vars_space_dim) - throw_dimension_incompatible("wrap_space_dimensions(vs, w, s, o, ...)", + throw_dimension_incompatible("wrap_assign(vs, w, s, o, ...)", vars_space_dim); if (x.is_empty()) return; const Variables_Set::const_iterator vs_end = vars.end(); - const ITV* null_p_itv = 0; + + // FIXME: temporarily (ab-) using Coefficient. + // Set `min_value' and `max_value' to the minimum and maximum values + // a variable of width `w' and signedness `s' can take. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + if (s == UNSIGNED) { + min_value = 0; + mul_2exp_assign(max_value, Coefficient_one(), w); + } + else { + assert(s == SIGNED_2_COMPLEMENT); + mul_2exp_assign(max_value, Coefficient_one(), w-1); + neg_assign(min_value, max_value); + } + // FIXME: Build the quadrant interval. + I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value); + I_Constraint<Coefficient> upper = i_constraint(LESS_THAN, max_value); + ITV quadrant_itv; + quadrant_itv.build(lower, upper); if (pcs == 0) { // No constraint refinement is needed here. - for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { - ITV& seq_v = x.seq[*i]; - I_Result res = seq_v.wrap_assign(w, s, o, null_p_itv); - if (seq_v.check_empty(res)) { - x.set_empty(); - return; + switch (o) { + case OVERFLOW_WRAPS: + for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) + x.seq[*i].wrap_assign(w, s, quadrant_itv); + break; + case OVERFLOW_UNDEFINED: + for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { + ITV& x_seq_v = x.seq[*i]; + if (!quadrant_itv.contains(x_seq_v)) + x_seq_v.assign(UNIVERSE); } + break; + case OVERFLOW_IMPOSSIBLE: + for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) + x.seq[*i].intersect_assign(quadrant_itv); + break; } assert(x.OK()); return; @@ -1493,37 +1521,38 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, } } - const ITV* p_itv; - ITV refinement_interval; + ITV refinement_itv; const map_type::const_iterator var_cs_map_end = var_cs_map.end(); // Loop through the variable indexes in `vars'. for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { const dimension_type v = *i; + refinement_itv = quadrant_itv; // Look for the refinement constraints for space dimension index `v'. map_type::const_iterator var_cs_map_iter = var_cs_map.find(v); - if (var_cs_map_iter == var_cs_map_end) { - // No refinement constraint is available for variable `v'. - p_itv = null_p_itv; - } - else { - p_itv = &refinement_interval; - // Build a refinement interval for variable `v'. - refinement_interval.assign(UNIVERSE); - map_type::mapped_type& var_cs = var_cs_map_iter->second; + if (var_cs_map_iter != var_cs_map_end) { + // Refine interval for variable `v'. + const map_type::mapped_type& var_cs = var_cs_map_iter->second; for (dimension_type j = var_cs.size(); j-- > 0; ) { const Constraint& c = *var_cs[j]; - refine_interval_no_check(refinement_interval, + refine_interval_no_check(refinement_itv, c.type(), c.inhomogeneous_term(), c.coefficient(Variable(v))); } } // Wrap space dimension index `v'. - ITV& seq_v = x.seq[v]; - I_Result res = seq_v.wrap_assign(w, s, o, p_itv); - if (seq_v.check_empty(res)) { - x.set_empty(); - return; + ITV& x_seq_v = x.seq[v]; + switch (o) { + case OVERFLOW_WRAPS: + x_seq_v.wrap_assign(w, s, refinement_itv); + break; + case OVERFLOW_UNDEFINED: + if (!quadrant_itv.contains(x_seq_v)) + x_seq_v.assign(UNIVERSE); + break; + case OVERFLOW_IMPOSSIBLE: + x_seq_v.intersect_assign(refinement_itv); + break; } } assert(x.OK()); diff --git a/src/Interval.defs.hh b/src/Interval.defs.hh index 56b0b6c..d0b71b1 100644 --- a/src/Interval.defs.hh +++ b/src/Interval.defs.hh @@ -528,10 +528,10 @@ public: return u >= l; } - template <typename T> - typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, I_Result>::type + template <typename From> + typename Enable_If<Is_Singleton<From>::value || Is_Interval<From>::value, I_Result>::type wrap_assign(Bounded_Integer_Type_Width w, Bounded_Integer_Type_Signedness s, - const Interval& refinement) { + const From& refinement) { if (is_empty()) return I_EMPTY; if (lower_is_boundary_infinity() || upper_is_boundary_infinity()) @@ -561,7 +561,7 @@ public: if (le(LOWER, lower(), info(), UPPER, upper(), info())) return intersect_assign(refinement); PPL_DIRTY_TEMP(Interval, tmp); - tmp.info.clear(); + tmp.info().clear(); Boundary_NS::assign(LOWER, tmp.lower(), tmp.info(), LOWER, lower(), info()); set_unbounded(UPPER, tmp.upper(), tmp.info());

1 0