[PPL-devel] [GIT] ppl/ppl(master): First draft of Box::wrap_assign() is now operational . Added a few tests.
Enea Zaffanella
zaffanella at cs.unipr.it
Mon May 18 10:20:04 CEST 2009
Module: ppl/ppl
Branch: master
Commit: 656fbd60bb14e3304468e8016937a188ead46418
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=656fbd60bb14e3304468e8016937a188ead46418
Author: Enea Zaffanella <zaffanella at 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.
---
src/Box.templates.hh | 82 +++++++++++++++++++++++++++++++++----------------
tests/Box/wrap1.cc | 70 ++++++++++++++++++++++++++++++++++++++++++
2 files changed, 125 insertions(+), 27 deletions(-)
diff --git a/src/Box.templates.hh b/src/Box.templates.hh
index 0561430..3f311fa 100644
--- a/src/Box.templates.hh
+++ b/src/Box.templates.hh
@@ -1420,7 +1420,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars,
const Constraint_System* pcs,
unsigned complexity_threshold,
bool wrap_individually) {
-#if 1 // Generic implementation commented out.
+#if 0 // Generic implementation commented out.
Implementation::wrap_assign(*this,
vars, w, r, o, pcs,
complexity_threshold, wrap_individually,
@@ -1429,66 +1429,94 @@ Box<ITV>::wrap_assign(const Variables_Set& vars,
used(wrap_individually);
used(complexity_threshold);
Box& x = *this;
- const dimension_type space_dim = x.space_dimension();
- // Dimension-compatibility check of `*pcs', if any.
- if (pcs != 0 && pcs->space_dimension() > space_dim)
- throw_dimension_incompatible("wrap_assign(vars, w, s, o, pcs, ...)", *pcs);
+
+ // Dimension-compatibility check for `*pcs', if any.
+ const dimension_type vars_space_dim = vars.space_dimension();
+ if (pcs != 0 && pcs->space_dimension() > vars_space_dim) {
+ std::ostringstream s;
+ s << "PPL::Box<ITV>::wrap_assign(vars, w, r, o, pcs, ...):"
+ << std::endl
+ << "vars.space_dimension() == " << vars_space_dim
+ << ", pcs->space_dimension() == " << pcs->space_dimension() << ".";
+ throw std::invalid_argument(s.str());
+ }
// Wrapping no variable only requires refining with *pcs, if any.
if (vars.empty()) {
if (pcs != 0)
- pointset.refine_with_constraints(*pcs);
+ refine_with_constraints(*pcs);
return;
}
- // Dimension-compatibility check.
- const dimension_type vars_space_dim = vars.space_dimension();
- if (space_dim < vars_space_dim)
- throw_dimension_incompatible("wrap_assign(vs, w, s, o, ...)",
- vars_space_dim);
+ // Dimension-compatibility check for `vars'.
+ const dimension_type space_dim = x.space_dimension();
+ if (space_dim < vars_space_dim) {
+ std::ostringstream s;
+ s << "PPL::Box<ITV>::wrap_assign(vars, ...):"
+ << std::endl
+ << "this->space_dimension() == " << space_dim
+ << ", required space dimension == " << vars_space_dim << ".";
+ throw std::invalid_argument(s.str());
+ }
+ // Wrapping an empty polyhedron is a no-op.
if (x.is_empty())
return;
- const Variables_Set::const_iterator vs_end = vars.end();
-
// 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) {
+ if (r == UNSIGNED) {
min_value = 0;
mul_2exp_assign(max_value, Coefficient_one(), w);
+ --max_value;
}
else {
- assert(s == SIGNED_2_COMPLEMENT);
+ assert(r == SIGNED_2_COMPLEMENT);
mul_2exp_assign(max_value, Coefficient_one(), w-1);
neg_assign(min_value, max_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);
- PPL_DIRTY_TEMP(ITV, quadrant_itv);
- quadrant_itv.build(lower, upper);
+
+ // FIXME: Build the (integer) quadrant interval.
+ PPL_DIRTY_TEMP(ITV, integer_quadrant_itv);
+ PPL_DIRTY_TEMP(ITV, rational_quadrant_itv);
+ {
+ I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value);
+ I_Constraint<Coefficient> upper = i_constraint(LESS_OR_EQUAL, max_value);
+ integer_quadrant_itv.build(lower, upper);
+ // The rational quadrant is only needed if overflow is undefined.
+ if (o == OVERFLOW_UNDEFINED) {
+ ++max_value;
+ upper = i_constraint(LESS_THAN, max_value);
+ rational_quadrant_itv.build(lower, upper);
+ }
+ }
+
+ const Variables_Set::const_iterator vs_end = vars.end();
if (pcs == 0) {
// No constraint refinement is needed here.
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);
+ x.seq[*i].wrap_assign(w, r, integer_quadrant_itv);
+ reset_empty_up_to_date();
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);
+ if (!rational_quadrant_itv.contains(x_seq_v)) {
+ x_seq_v.assign(integer_quadrant_itv);
+ }
}
break;
case OVERFLOW_IMPOSSIBLE:
for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i)
- x.seq[*i].intersect_assign(quadrant_itv);
+ x.seq[*i].intersect_assign(integer_quadrant_itv);
+ reset_empty_up_to_date();
break;
}
assert(x.OK());
@@ -1530,7 +1558,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars,
// 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;
+ refinement_itv = integer_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) {
@@ -1548,10 +1576,10 @@ Box<ITV>::wrap_assign(const Variables_Set& vars,
ITV& x_seq_v = x.seq[v];
switch (o) {
case OVERFLOW_WRAPS:
- x_seq_v.wrap_assign(w, s, refinement_itv);
+ x_seq_v.wrap_assign(w, r, refinement_itv);
break;
case OVERFLOW_UNDEFINED:
- if (!quadrant_itv.contains(x_seq_v))
+ if (!rational_quadrant_itv.contains(x_seq_v))
x_seq_v.assign(UNIVERSE);
break;
case OVERFLOW_IMPOSSIBLE:
diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc
index 0045246..6a0d1f9 100644
--- a/tests/Box/wrap1.cc
+++ b/tests/Box/wrap1.cc
@@ -124,10 +124,80 @@ test03() {
return ok;
}
+bool
+test04() {
+ Variable x(0);
+ TBox box1(1);
+ box1.add_constraint(2*x == 511);
+
+ print_constraints(box1, "*** box ***");
+
+ Variables_Set vars(x);
+
+ // Making copies before affecting box1.
+ TBox box2(box1);
+ TBox box3(box1);
+
+ TBox good_enough_result(box1);
+ TBox precise_result(1, EMPTY);
+
+ box1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS);
+ box2.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED);
+ box3.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE);
+
+ // FIXME: Implementation can be more precise than expected.
+ bool ok = box1.contains(precise_result) && good_enough_result.contains(box1)
+ && box2.contains(precise_result) && good_enough_result.contains(box2)
+ && box3.contains(precise_result) && good_enough_result.contains(box3);
+
+ print_constraints(box1, "*** box.wrap_assign(..., OVERFLOW_WRAPS) ***");
+ print_constraints(box2, "*** box.wrap_assign(..., OVERFLOW_UNDEFINED) ***");
+ print_constraints(box3, "*** box.wrap_assign(..., OVERFLOW_IMPOSSIBLE) ***");
+
+ return ok;
+}
+
+bool
+test05() {
+ Variable x(0);
+ TBox box1(1);
+ box1.add_constraint(2*x == 18*256 + 511);
+
+ print_constraints(box1, "*** box ***");
+
+ Variables_Set vars(x);
+
+ // Making copies before affecting box1.
+ TBox box2(box1);
+ TBox box3(box1);
+
+ box1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS);
+ box2.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED);
+ box3.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE);
+
+ TBox known_result1(1, EMPTY);
+ TBox known_result2(1);
+ known_result2.add_constraint(x >= 0);
+ known_result2.add_constraint(x <= 255);
+ TBox known_result3(1, EMPTY);
+
+ bool ok = (box1 == known_result1)
+ && (box2 == known_result2)
+ && (box3 == known_result3);
+
+ print_constraints(box1, "*** box.wrap_assign(..., OVERFLOW_WRAPS) ***");
+ print_constraints(box2, "*** box.wrap_assign(..., OVERFLOW_UNDEFINED) ***");
+ print_constraints(box3, "*** box.wrap_assign(..., OVERFLOW_IMPOSSIBLE) ***");
+
+ return ok;
+}
+
} // namespace
BEGIN_MAIN
DO_TEST_F8(test01);
DO_TEST_F8(test02);
DO_TEST_F(test03);
+ DO_TEST_F8(test04);
+ DO_TEST_F8(test05);
END_MAIN
More information about the PPL-devel
mailing list