[PPL-devel] [GIT] ppl/ppl(master): Adapted generic implementation of wrap_assign to model the rational case.
Enea Zaffanella
zaffanella at cs.unipr.it
Thu May 14 21:07:25 CEST 2009
Module: ppl/ppl
Branch: master
Commit: 74ade8b7dbf158e7473d8375c724e4a706506267
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=74ade8b7dbf158e7473d8375c724e4a706506267
Author: Enea Zaffanella <zaffanella at 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
More information about the PPL-devel
mailing list