[PPL-devel] [GIT] ppl/ppl(bounded_arithmetic): Added a new parameter `pcs' to Polyhedron::wrap_assign().
Roberto Bagnara
bagnara at cs.unipr.it
Mon Apr 27 22:14:30 CEST 2009
Module: ppl/ppl
Branch: bounded_arithmetic
Commit: 4917f7ba9b6d92f7e1556ed4d8fa89b060d71055
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4917f7ba9b6d92f7e1556ed4d8fa89b060d71055
Author: Roberto Bagnara <bagnara at 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;
}
More information about the PPL-devel
mailing list