diff options
Diffstat (limited to 'src/wrap_assign.hh')
| -rw-r--r-- | src/wrap_assign.hh | 389 |
1 files changed, 389 insertions, 0 deletions
diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh new file mode 100644 index 000000000..cbddcd385 --- /dev/null +++ b/src/wrap_assign.hh @@ -0,0 +1,389 @@ +/* Generic implementation of the wrap_assign() function. + Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> + Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com) + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#ifndef PPL_wrap_assign_hh +#define PPL_wrap_assign_hh 1 + +#include "globals.defs.hh" +#include "Coefficient.defs.hh" +#include "Variable.defs.hh" +#include "Constraint_System.defs.hh" +#include "assert.hh" + +namespace Parma_Polyhedra_Library { + +namespace Implementation { + +struct Wrap_Dim_Translations { + Variable var; + Coefficient first_quadrant; + Coefficient last_quadrant; + Wrap_Dim_Translations(Variable v, + Coefficient_traits::const_reference f, + Coefficient_traits::const_reference l) + : var(v), first_quadrant(f), last_quadrant(l) { + } +}; + +typedef std::vector<Wrap_Dim_Translations> Wrap_Translations; + +template <typename PSET> +void +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, + 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, + Coefficient& tmp) { + if (first == end) { + PSET p(src); + if (pcs != 0) + p.refine_with_constraints(*pcs); + for (Variables_Set::const_iterator i = vars.begin(), + 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); + } + dest.upper_bound_assign(p); + } + else { + const Wrap_Dim_Translations& wrap_dim_translations = *first; + 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& shift = tmp; + PPL_DIRTY_TEMP_COEFFICIENT(quadrant); + for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) { + if (quadrant != 0) { + mul_2exp_assign(shift, quadrant, w); + PSET p(src); + p.affine_image(x, x - shift, 1); + wrap_assign_col(dest, p, vars, first+1, end, w, min_value, max_value, + pcs, tmp); + } + else + wrap_assign_col(dest, src, vars, first+1, end, w, min_value, max_value, + pcs, tmp); + } + } +} + +template <typename PSET> +void +wrap_assign(PSET& pointset, + const Variables_Set& vars, + const Bounded_Integer_Type_Width w, + const Bounded_Integer_Type_Representation r, + const Bounded_Integer_Type_Overflow o, + const Constraint_System* pcs, + 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(). + + // Dimension-compatibility check of `*pcs', if any. + const dimension_type vars_space_dim = vars.space_dimension(); + if (pcs != 0) { + if (pcs->space_dimension() > vars_space_dim) { + std::ostringstream s; + s << "PPL::" << class_name << "::wrap_assign(..., pcs, ...):" + << std::endl + << "vars.space_dimension() == " << vars_space_dim + << ", pcs->space_dimension() == " << pcs->space_dimension() << "."; + throw std::invalid_argument(s.str()); + } + +#ifndef NDEBUG + // Check that all variables upon which `*pcs' depends are in `vars'. + // An assertion is violated otherwise. + const Constraint_System cs = *pcs; + 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) { + const Constraint& c = *i; + for (dimension_type d = cs_space_dim; d-- > 0; ) { + PPL_ASSERT(c.coefficient(Variable(d)) == 0 + || vars.find(d) != vars_end); + } + } +#endif + } + + // Wrapping no variable only requires refining with *pcs, if any. + if (vars.empty()) { + if (pcs != 0) + pointset.refine_with_constraints(*pcs); + return; + } + + // Dimension-compatibility check of `vars'. + const dimension_type space_dim = pointset.space_dimension(); + if (vars.space_dimension() > space_dim) { + std::ostringstream s; + s << "PPL::" << class_name << "::wrap_assign(vs, ...):" << std::endl + << "this->space_dimension() == " << space_dim + << ", required space dimension == " << vars.space_dimension() << "."; + throw std::invalid_argument(s.str()); + } + + // Wrapping an empty polyhedron is a no-op. + if (pointset.is_empty()) + return; + + // 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 (r == UNSIGNED) { + min_value = 0; + mul_2exp_assign(max_value, Coefficient_one(), w); + --max_value; + } + else { + PPL_ASSERT(r == 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 + // required translations are saved in `translations' instead of being + // immediately applied. + Wrap_Translations translations; + + // 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. + // As soon as this exceeds `complexity_threshold', counting will be + // interrupted and the full range will be the result of wrapping + // any dimension that is not fully contained in quadrant 0. + unsigned collective_wrap_complexity = 1; + + // This flag signals that the maximum complexity for collective + // wrapping as been exceeded. + bool collective_wrap_too_complex = false; + + if (!wrap_individually) { + translations.reserve(space_dim); + } + + // 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); + PPL_DIRTY_TEMP_COEFFICIENT(ld); + PPL_DIRTY_TEMP_COEFFICIENT(un); + PPL_DIRTY_TEMP_COEFFICIENT(ud); + + for (Variables_Set::const_iterator i = vars.begin(), + vars_end = vars.end(); i != vars_end; ++i) { + + const Variable x = Variable(*i); + + bool extremum; + + if (!pointset.minimize(x, ln, ld, extremum)) { + set_full_range: + pointset.unconstrain(x); + full_range_bounds.insert(min_value <= x); + full_range_bounds.insert(x <= max_value); + continue; + } + + if (!pointset.maximize(x, un, ud, extremum)) + goto set_full_range; + + div_assign_r(ln, ln, ld, ROUND_DOWN); + div_assign_r(un, un, ud, ROUND_DOWN); + ln -= min_value; + un -= min_value; + div_2exp_assign_r(ln, ln, w, ROUND_DOWN); + div_2exp_assign_r(un, un, w, ROUND_DOWN); + Coefficient& first_quadrant = ln; + Coefficient& last_quadrant = un; + + // Special case: this variable does not need wrapping. + if (first_quadrant == 0 && last_quadrant == 0) + continue; + + // If overflow is impossible, try not to add useless constraints. + if (o == OVERFLOW_IMPOSSIBLE) { + if (first_quadrant < 0) + full_range_bounds.insert(min_value <= x); + if (last_quadrant > 0) + full_range_bounds.insert(x <= max_value); + continue; + } + + if (o == OVERFLOW_UNDEFINED || collective_wrap_too_complex) + goto set_full_range; + + Coefficient& quadrants = ud; + quadrants = last_quadrant - first_quadrant + 1; + + unsigned extension; + Result res = assign_r(extension, quadrants, ROUND_IGNORE); + if (result_overflow(res) || extension > complexity_threshold) + goto set_full_range; + + if (!wrap_individually && !collective_wrap_too_complex) { + res = mul_assign_r(collective_wrap_complexity, + collective_wrap_complexity, extension, ROUND_IGNORE); + if (result_overflow(res) + || collective_wrap_complexity > complexity_threshold) + collective_wrap_too_complex = true; + if (collective_wrap_too_complex) { + // Set all the dimensions in `translations' to full range. + for (Wrap_Translations::const_iterator j = translations.begin(), + tend = translations.end(); j != tend; ++j) { + const Variable& y = j->var; + pointset.unconstrain(y); + full_range_bounds.insert(min_value <= y); + full_range_bounds.insert(y <= max_value); + } + } + } + + if (wrap_individually && pcs == 0) { + Coefficient& quadrant = first_quadrant; + // Temporary variable holding the shifts to be applied in order + // to implement the translations. + Coefficient& shift = ld; + PSET hull(space_dim, EMPTY); + for ( ; quadrant <= last_quadrant; ++quadrant) { + PSET p(pointset); + if (quadrant != 0) { + mul_2exp_assign(shift, quadrant, w); + p.affine_image(x, x - shift, 1); + } + p.refine_with_constraint(min_value <= x); + p.refine_with_constraint(x <= max_value); + hull.upper_bound_assign(p); + } + pointset.swap(hull); + } + else if (wrap_individually || !collective_wrap_too_complex) { + PPL_ASSERT(!wrap_individually || pcs != 0); + dimensions_to_be_translated.insert(x); + translations + .push_back(Wrap_Dim_Translations(x, first_quadrant, last_quadrant)); + } + } + + if (!translations.empty()) { + if (wrap_individually) { + PPL_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); + pointset.swap(hull); + } + } + + if (pcs != 0) + pointset.refine_with_constraints(*pcs); + pointset.refine_with_constraints(full_range_bounds); +} + +} // namespace Implementation + +} // namespace Parma_Polyhedra_Library + +#endif // !defined(PPL_wrap_assign_hh) |