[PPL-devel] [GIT] ppl/ppl(master): Fixed the generic implementation of wrap_assign().
Roberto Bagnara
bagnara at cs.unipr.it
Fri May 15 19:47:11 CEST 2009
Module: ppl/ppl
Branch: master
Commit: 30f456f032cf56ef3f62452a678b398d057e990c
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30f456f032cf56ef3f62452a678b398d057e990c
Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date: Fri May 15 19:45:25 2009 +0200
Fixed the generic implementation of wrap_assign().
---
src/wrap_assign.hh | 129 +++++++++++++++++++++++++++++++++------------
tests/Box/wrap1.cc | 6 +--
tests/Polyhedron/wrap1.cc | 2 +-
3 files changed, 98 insertions(+), 39 deletions(-)
diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh
index c6c76eb..abb3327 100644
--- a/src/wrap_assign.hh
+++ b/src/wrap_assign.hh
@@ -48,16 +48,75 @@ typedef std::vector<Wrap_Dim_Translations> Wrap_Translations;
template <typename PSET>
void
-wrap_assign_rec(PSET& dest,
+wrap_assign_ind(PSET& pointset,
+ Variables_Set& vars,
+ Wrap_Translations::const_iterator first,
+ Wrap_Translations::const_iterator end,
+ Bounded_Integer_Type_Width w,
+ Coefficient_traits::const_reference min_value,
+ Coefficient_traits::const_reference max_value,
+ const Constraint_System& cs,
+ Coefficient& tmp1,
+ Coefficient& tmp2) {
+ const dimension_type space_dim = pointset.space_dimension();
+ const dimension_type cs_space_dim = cs.space_dimension();
+ for (Wrap_Translations::const_iterator i = first; i != end; ++i) {
+ const Wrap_Dim_Translations& wrap_dim_translations = *i;
+ const Variable& x = wrap_dim_translations.var;
+ const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant;
+ const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant;
+ Coefficient& quadrant = tmp1;
+ Coefficient& shift = tmp2;
+ PSET hull(space_dim, EMPTY);
+ for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) {
+ PSET p(pointset);
+ if (quadrant != 0) {
+ mul_2exp_assign(shift, quadrant, w);
+ p.affine_image(x, x - shift, 1);
+ }
+ // `x' has just been wrapped.
+ vars.erase(x.id());
+
+ // Refine `p' with all the constraints in `cs' not depending
+ // on variables in `vars'.
+ if (vars.empty())
+ p.refine_with_constraints(cs);
+ else {
+ Variables_Set::const_iterator vars_end = vars.end();
+ for (Constraint_System::const_iterator j = cs.begin(),
+ cs_end = cs.end(); j != cs_end; ++j) {
+ const Constraint& c = *j;
+ for (dimension_type d = cs_space_dim; d-- > 0; ) {
+ if (c.coefficient(Variable(d)) != 0 && vars.find(d) != vars_end)
+ goto skip;
+ }
+ // If we are here it means `c' does not depend on variables
+ // in `vars'.
+ p.refine_with_constraint(c);
+
+ skip:
+ continue;
+ }
+ }
+ p.refine_with_constraint(min_value <= x);
+ p.refine_with_constraint(x <= max_value);
+ hull.upper_bound_assign(p);
+ }
+ pointset.swap(hull);
+ }
+}
+
+template <typename PSET>
+void
+wrap_assign_col(PSET& dest,
const PSET& src,
- Variables_Set vars,
- Wrap_Translations::iterator first,
- Wrap_Translations::iterator end,
+ const Variables_Set& vars,
+ Wrap_Translations::const_iterator first,
+ Wrap_Translations::const_iterator end,
Bounded_Integer_Type_Width w,
Coefficient_traits::const_reference min_value,
Coefficient_traits::const_reference max_value,
const Constraint_System* pcs,
- unsigned complexity_threshold,
Coefficient& tmp1,
Coefficient& tmp2) {
if (first == end) {
@@ -84,12 +143,12 @@ wrap_assign_rec(PSET& dest,
mul_2exp_assign(shift, quadrant, w);
PSET p(src);
p.affine_image(x, x - shift, 1);
- wrap_assign_rec(dest, p, vars, first+1, end, w, min_value, max_value,
- pcs, complexity_threshold, tmp1, tmp2);
+ wrap_assign_col(dest, p, vars, first+1, end, w, min_value, max_value,
+ pcs, tmp1, tmp2);
}
else
- wrap_assign_rec(dest, src, vars, first+1, end, w, min_value, max_value,
- pcs, complexity_threshold, tmp1, tmp2);
+ wrap_assign_col(dest, src, vars, first+1, end, w, min_value, max_value,
+ pcs, tmp1, tmp2);
}
}
}
@@ -98,12 +157,12 @@ template <typename PSET>
void
wrap_assign(PSET& pointset,
const Variables_Set& vars,
- Bounded_Integer_Type_Width w,
- Bounded_Integer_Type_Signedness s,
- Bounded_Integer_Type_Overflow o,
+ const Bounded_Integer_Type_Width w,
+ const Bounded_Integer_Type_Signedness s,
+ const Bounded_Integer_Type_Overflow o,
const Constraint_System* pcs,
- unsigned complexity_threshold,
- bool wrap_individually,
+ const unsigned complexity_threshold,
+ const bool wrap_individually,
const char* class_name) {
// We must have pcs->space_dimension() <= vars.space_dimension()
// and vars.space_dimension() <= pointset.space_dimension().
@@ -124,7 +183,7 @@ wrap_assign(PSET& pointset,
// Check that all variables upon which `*pcs' depends are in `vars'.
// An assertion is violated otherwise.
const Constraint_System cs = *pcs;
- dimension_type cs_space_dim = cs.space_dimension();
+ const dimension_type cs_space_dim = cs.space_dimension();
Variables_Set::const_iterator vars_end = vars.end();
for (Constraint_System::const_iterator i = cs.begin(),
cs_end = cs.end(); i != cs_end; ++i) {
@@ -179,9 +238,9 @@ wrap_assign(PSET& pointset,
// immediately applied.
Wrap_Translations translations;
- // If we are wrapping variables collectively, dimensions subject
- // to translation are added to this set.
- Variables_Set translated_dimensions;
+ // Dimensions subject to translation are added to this set if we are
+ // wrapping collectively or if `pcs' is non null.
+ Variables_Set dimensions_to_be_translated;
// This will contain a lower bound to the number of abstractions
// to be joined in order to obtain the collective wrapping result.
@@ -207,8 +266,6 @@ wrap_assign(PSET& pointset,
PPL_DIRTY_TEMP_COEFFICIENT(un);
PPL_DIRTY_TEMP_COEFFICIENT(ud);
- //using namespace IO_Operators;
-
for (Variables_Set::const_iterator i = vars.begin(),
vars_end = vars.end(); i != vars_end; ++i) {
@@ -287,7 +344,7 @@ wrap_assign(PSET& pointset,
}
}
- if (wrap_individually) {
+ if (wrap_individually && pcs == 0) {
Coefficient& quadrant = first_quadrant;
// Temporary variable holding the shifts to be applied in order
// to implement the translations.
@@ -299,28 +356,34 @@ wrap_assign(PSET& pointset,
mul_2exp_assign(shift, quadrant, w);
p.affine_image(x, x - shift, 1);
}
- if (pcs != 0)
- p.refine_with_constraints(*pcs);
p.refine_with_constraint(min_value <= x);
p.refine_with_constraint(x <= max_value);
hull.upper_bound_assign(p);
}
pointset.swap(hull);
}
- else if (!collective_wrap_too_complex)
- // !wrap_individually.
- translated_dimensions.insert(x);
+ else if (wrap_individually || !collective_wrap_too_complex) {
+ assert(!wrap_individually || pcs != 0);
+ dimensions_to_be_translated.insert(x);
translations
.push_back(Wrap_Dim_Translations(x, first_quadrant, last_quadrant));
+ }
}
- if (!wrap_individually && !translations.empty()) {
- PSET hull(space_dim, EMPTY);
- wrap_assign_rec(hull, pointset, translated_dimensions,
- translations.begin(), translations.end(),
- w, min_value, max_value, pcs, complexity_threshold,
- ln, ld);
- pointset.swap(hull);
+ if (!translations.empty()) {
+ if (wrap_individually) {
+ assert(pcs != 0);
+ wrap_assign_ind(pointset, dimensions_to_be_translated,
+ translations.begin(), translations.end(),
+ w, min_value, max_value, *pcs, ln, ld);
+ }
+ else {
+ PSET hull(space_dim, EMPTY);
+ wrap_assign_col(hull, pointset, dimensions_to_be_translated,
+ translations.begin(), translations.end(),
+ w, min_value, max_value, pcs, ln, ld);
+ pointset.swap(hull);
+ }
}
if (pcs != 0)
diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc
index d2799bc..0045246 100644
--- a/tests/Box/wrap1.cc
+++ b/tests/Box/wrap1.cc
@@ -44,10 +44,8 @@ test01() {
TBox known_result(2);
known_result.refine_with_constraint(0 <= x);
known_result.refine_with_constraint(x <= 255);
- // known_result.refine_with_constraint(x < 256);
known_result.refine_with_constraint(0 <= y);
known_result.refine_with_constraint(y <= 255);
- // known_result.refine_with_constraint(y < 256);
bool ok = (box == known_result);
@@ -80,7 +78,6 @@ test02() {
TBox known_result(2);
known_result.refine_with_constraint(0 <= x);
known_result.refine_with_constraint(x <= 255);
- // known_result.refine_with_constraint(x < 256);
known_result.refine_with_constraint(0 <= y);
known_result.refine_with_constraint(y <= 50);
@@ -117,7 +114,6 @@ test03() {
known_result.refine_with_constraint(6 <= x);
// known_result.refine_with_constraint(0 <= x);
known_result.refine_with_constraint(x <= 255);
- // known_result.refine_with_constraint(x < 256);
known_result.refine_with_constraint(0 <= y);
known_result.refine_with_constraint(y <= 50);
@@ -133,5 +129,5 @@ test03() {
BEGIN_MAIN
DO_TEST_F8(test01);
DO_TEST_F8(test02);
- DO_TEST_F8(test03);
+ DO_TEST_F(test03);
END_MAIN
diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc
index 5d7c795..cc622ba 100644
--- a/tests/Polyhedron/wrap1.cc
+++ b/tests/Polyhedron/wrap1.cc
@@ -587,5 +587,5 @@ BEGIN_MAIN
DO_TEST(test16);
DO_TEST(test17);
DO_TEST(test18);
- DO_TEST_F(test19);
+ DO_TEST(test19);
END_MAIN
More information about the PPL-devel
mailing list