Module: ppl/ppl Branch: bounded_arithmetic Commit: 4917f7ba9b6d92f7e1556ed4d8fa89b060d71055 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4917f7ba9b6d9...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Mon Apr 27 22:13:20 2009 +0200

Added a new parameter `pcs' to Polyhedron::wrap_assign(). Other parameters reordered. The tests now check for the expected result.

---

src/Polyhedron.defs.hh | 21 +++++++++++++++------ src/Polyhedron_public.cc | 36 ++++++++++++++++++++++++------------ tests/Polyhedron/wrap1.cc | 43 +++++++++++++++++++++++++++++++++++++------ 3 files changed, 76 insertions(+), 24 deletions(-)

diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 0c8f1e9..545150c 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1443,15 +1443,23 @@ public: The overflow behavior of the bounded integer type corresponding to all the dimensions to be wrapped.

- \param wrap_individually - <CODE>true</CODE> if the dimensions should be wrapped individually - (something that results in greater efficiency to the detriment of - precision). + \param pcs + Possibly null pointer to a constraint system. When non-null, + the pointed-to constraint system is assumed to represent the + guard with respect to which wrapping is performed. Passing + a constraint system in this way can be more precise then + adding the constraints in <CODE>*pcs</CODE> to the result + of the wrapping operation.

\param k_threshold A precision parameter of the \ref Wrap_Operator "wrapping operator": higher values result in possibly improved precision.

+ \param wrap_individually + <CODE>true</CODE> if the dimensions should be wrapped individually + (something that results in greater efficiency to the detriment of + precision). + \exception std::invalid_argument Thrown if \p *this is dimension-incompatible with one of the Variable objects contained in \p vars. @@ -1460,8 +1468,9 @@ public: Bounded_Integer_Type_Width w, Bounded_Integer_Type_Signedness s, Bounded_Integer_Type_Overflow o, - bool wrap_individually = true, - unsigned k_threshold = 16); + const Constraint_System* pcs = 0, + unsigned k_threshold = 16, + bool wrap_individually = true);

//! Assigns to \p *this its topological closure. void topological_closure_assign(); diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index bd21fa4..9111f31 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -3681,8 +3681,9 @@ PPL::Polyhedron::wrap_assign(const Variables_Set& vars, Bounded_Integer_Type_Width w, Bounded_Integer_Type_Signedness s, Bounded_Integer_Type_Overflow o, - bool wrap_individually, - unsigned k_threshold) { + const Constraint_System* pcs, + unsigned k_threshold, + bool wrap_individually) { // Wrapping no variable is a no-op. if (vars.empty()) return; @@ -3696,10 +3697,10 @@ PPL::Polyhedron::wrap_assign(const Variables_Set& vars, if (is_empty()) return;

- // Bound low and bound high assignment. + // 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); @@ -3716,8 +3717,8 @@ PPL::Polyhedron::wrap_assign(const Variables_Set& vars, //std::cout << "max_value = " << max_value << std::endl;

if (wrap_individually) { - // We use this to delay conversions when this does not negatively - // affect precision. + // We use `full_range_bounds' to delay conversions whenever + // this delay does not negatively affect precision. Constraint_System full_range_bounds;

PPL_DIRTY_TEMP_COEFFICIENT(ln); @@ -3755,20 +3756,29 @@ PPL::Polyhedron::wrap_assign(const Variables_Set& vars, un -= min_value; div_2exp_assign_r(ln, ln, w, ROUND_DOWN); div_2exp_assign_r(un, un, w, ROUND_DOWN); - if (un - ln > k_threshold) - goto set_full_range;

//std::cout << "ln = " << ln << std::endl; //std::cout << "un = " << un << std::endl;

+ // Special case: this variable does not need wrapping. + if (un == 0 && ln == 0) + continue; + + if (un - ln > k_threshold) + goto set_full_range; + Polyhedron hull(topology(), space_dimension(), EMPTY); for ( ; ln <= un; ++ln) { Polyhedron p(*this); //std::cout << "p: " << p << std::endl; - mul_2exp_assign(ld, ln, w); - //std::cout << "ld = " << ld << std::endl; - p.affine_image(x, x - ld, 1); - //std::cout << "affine_image: " << p << std::endl; + if (ln != 0) { + mul_2exp_assign(ld, ln, w); + //std::cout << "ld = " << ld << std::endl; + p.affine_image(x, x - ld, 1); + //std::cout << "affine_image: " << p << std::endl; + } + if (pcs != 0) + p.add_constraints(*pcs); p.add_constraint(min_value <= x); p.add_constraint(x <= max_value); hull.poly_hull_assign(p); @@ -3776,6 +3786,8 @@ PPL::Polyhedron::wrap_assign(const Variables_Set& vars, } swap(hull); } + if (pcs != 0) + add_constraints(*pcs); add_constraints(full_range_bounds); } else diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 97298f3..f997c1a 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -28,7 +28,7 @@ bool test01() { Variable x(0); Variable y(1); - C_Polyhedron ph(2, UNIVERSE); + C_Polyhedron ph(2); ph.add_constraint(x + 1024 == 8*y); ph.add_constraint(-64 <= x); ph.add_constraint(x <= 448); @@ -37,19 +37,50 @@ test01() {

Variables_Set vars(x, y);

- ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, true, 10); + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS);

- print_constraints(ph.minimized_constraints(), "*** ph.wrap_assign(...) ***"); + C_Polyhedron known_result(2); + known_result.add_constraint(x >= 0); + known_result.add_constraint(x <= 255); + known_result.add_constraint(x + 24*y >= 3072); + known_result.add_constraint(193*x + 504*y <= 129792); + known_result.add_constraint(x - 8*y >= -1280); + known_result.add_constraint(x - 8*y <= -768);

- bool ok = true; + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***");

return ok; }

bool test02() { - // FIXME: to be written. - bool ok = true; + Variable x(0); + Variable y(1); + C_Polyhedron ph(2); + ph.add_constraint(x + 1024 == 8*y); + ph.add_constraint(-64 <= x); + ph.add_constraint(x <= 448); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + Constraint_System cs; + cs.insert(x <= 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(x <= y); + known_result.add_constraint(x - 8*y >= -1280); + known_result.add_constraint(x - 8*y <= -1024); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***");

return ok; }