1 /* Generic implementation of the wrap_assign() function.
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #ifndef PPL_wrap_assign_hh
25 #define PPL_wrap_assign_hh 1
26
27 #include "globals_defs.hh"
28 #include "Coefficient_defs.hh"
29 #include "Variable_defs.hh"
30 #include "Constraint_System_defs.hh"
31 #include "assertions.hh"
32
33 namespace Parma_Polyhedra_Library {
34
35 namespace Implementation {
36
37 struct Wrap_Dim_Translations {
38 Variable var;
39 Coefficient first_quadrant;
40 Coefficient last_quadrant;
Wrap_Dim_TranslationsParma_Polyhedra_Library::Implementation::Wrap_Dim_Translations41 Wrap_Dim_Translations(Variable v,
42 Coefficient_traits::const_reference f,
43 Coefficient_traits::const_reference l)
44 : var(v), first_quadrant(f), last_quadrant(l) {
45 }
46 };
47
48 typedef std::vector<Wrap_Dim_Translations> Wrap_Translations;
49
50 template <typename PSET>
51 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)52 wrap_assign_ind(PSET& pointset,
53 Variables_Set& vars,
54 Wrap_Translations::const_iterator first,
55 Wrap_Translations::const_iterator end,
56 Bounded_Integer_Type_Width w,
57 Coefficient_traits::const_reference min_value,
58 Coefficient_traits::const_reference max_value,
59 const Constraint_System& cs,
60 Coefficient& tmp1,
61 Coefficient& tmp2) {
62 const dimension_type space_dim = pointset.space_dimension();
63 for (Wrap_Translations::const_iterator i = first; i != end; ++i) {
64 const Wrap_Dim_Translations& wrap_dim_translations = *i;
65 const Variable x(wrap_dim_translations.var);
66 const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant;
67 const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant;
68 Coefficient& quadrant = tmp1;
69 Coefficient& shift = tmp2;
70 PSET hull(space_dim, EMPTY);
71 for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) {
72 PSET p(pointset);
73 if (quadrant != 0) {
74 mul_2exp_assign(shift, quadrant, w);
75 p.affine_image(x, x - shift, 1);
76 }
77 // `x' has just been wrapped.
78 vars.erase(x.id());
79
80 // Refine `p' with all the constraints in `cs' not depending
81 // on variables in `vars'.
82 if (vars.empty()) {
83 p.refine_with_constraints(cs);
84 }
85 else {
86 for (Constraint_System::const_iterator j = cs.begin(),
87 cs_end = cs.end(); j != cs_end; ++j) {
88 if (j->expression().all_zeroes(vars)) {
89 // `*j' does not depend on variables in `vars'.
90 p.refine_with_constraint(*j);
91 }
92 }
93 }
94 p.refine_with_constraint(min_value <= x);
95 p.refine_with_constraint(x <= max_value);
96 hull.upper_bound_assign(p);
97 }
98 pointset.m_swap(hull);
99 }
100 }
101
102 template <typename PSET>
103 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 * cs_p,Coefficient & tmp)104 wrap_assign_col(PSET& dest,
105 const PSET& src,
106 const Variables_Set& vars,
107 Wrap_Translations::const_iterator first,
108 Wrap_Translations::const_iterator end,
109 Bounded_Integer_Type_Width w,
110 Coefficient_traits::const_reference min_value,
111 Coefficient_traits::const_reference max_value,
112 const Constraint_System* cs_p,
113 Coefficient& tmp) {
114 if (first == end) {
115 PSET p(src);
116 if (cs_p != 0) {
117 p.refine_with_constraints(*cs_p);
118 }
119 for (Variables_Set::const_iterator i = vars.begin(),
120 vars_end = vars.end(); i != vars_end; ++i) {
121 const Variable x(*i);
122 p.refine_with_constraint(min_value <= x);
123 p.refine_with_constraint(x <= max_value);
124 }
125 dest.upper_bound_assign(p);
126 }
127 else {
128 const Wrap_Dim_Translations& wrap_dim_translations = *first;
129 const Variable x(wrap_dim_translations.var);
130 const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant;
131 const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant;
132 Coefficient& shift = tmp;
133 PPL_DIRTY_TEMP_COEFFICIENT(quadrant);
134 for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) {
135 if (quadrant != 0) {
136 mul_2exp_assign(shift, quadrant, w);
137 PSET p(src);
138 p.affine_image(x, x - shift, 1);
139 wrap_assign_col(dest, p, vars, first+1, end, w, min_value, max_value,
140 cs_p, tmp);
141 }
142 else {
143 wrap_assign_col(dest, src, vars, first+1, end, w, min_value, max_value,
144 cs_p, tmp);
145 }
146 }
147 }
148 }
149
150 template <typename PSET>
151 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 * cs_p,const unsigned complexity_threshold,const bool wrap_individually,const char * class_name)152 wrap_assign(PSET& pointset,
153 const Variables_Set& vars,
154 const Bounded_Integer_Type_Width w,
155 const Bounded_Integer_Type_Representation r,
156 const Bounded_Integer_Type_Overflow o,
157 const Constraint_System* cs_p,
158 const unsigned complexity_threshold,
159 const bool wrap_individually,
160 const char* class_name) {
161 // We must have cs_p->space_dimension() <= vars.space_dimension()
162 // and vars.space_dimension() <= pointset.space_dimension().
163
164 // Dimension-compatibility check of `*cs_p', if any.
165 if (cs_p != 0) {
166 const dimension_type vars_space_dim = vars.space_dimension();
167 if (cs_p->space_dimension() > vars_space_dim) {
168 std::ostringstream s;
169 s << "PPL::" << class_name << "::wrap_assign(..., cs_p, ...):"
170 << std::endl
171 << "vars.space_dimension() == " << vars_space_dim
172 << ", cs_p->space_dimension() == " << cs_p->space_dimension() << ".";
173 throw std::invalid_argument(s.str());
174 }
175
176 #ifndef NDEBUG
177 // Check that all variables upon which `*cs_p' depends are in `vars'.
178 // An assertion is violated otherwise.
179 const Constraint_System cs = *cs_p;
180 const dimension_type cs_space_dim = cs.space_dimension();
181 Variables_Set::const_iterator vars_end = vars.end();
182 for (Constraint_System::const_iterator i = cs.begin(),
183 cs_end = cs.end(); i != cs_end; ++i) {
184 const Constraint& c = *i;
185 for (dimension_type d = cs_space_dim; d-- > 0; ) {
186 PPL_ASSERT(c.coefficient(Variable(d)) == 0
187 || vars.find(d) != vars_end);
188 }
189 }
190 #endif
191 }
192
193 // Wrapping no variable only requires refining with *cs_p, if any.
194 if (vars.empty()) {
195 if (cs_p != 0) {
196 pointset.refine_with_constraints(*cs_p);
197 }
198 return;
199 }
200
201 // Dimension-compatibility check of `vars'.
202 const dimension_type space_dim = pointset.space_dimension();
203 if (vars.space_dimension() > space_dim) {
204 std::ostringstream s;
205 s << "PPL::" << class_name << "::wrap_assign(vs, ...):" << std::endl
206 << "this->space_dimension() == " << space_dim
207 << ", required space dimension == " << vars.space_dimension() << ".";
208 throw std::invalid_argument(s.str());
209 }
210
211 // Wrapping an empty polyhedron is a no-op.
212 if (pointset.is_empty()) {
213 return;
214 }
215 // Set `min_value' and `max_value' to the minimum and maximum values
216 // a variable of width `w' and signedness `s' can take.
217 PPL_DIRTY_TEMP_COEFFICIENT(min_value);
218 PPL_DIRTY_TEMP_COEFFICIENT(max_value);
219 if (r == UNSIGNED) {
220 min_value = 0;
221 mul_2exp_assign(max_value, Coefficient_one(), w);
222 --max_value;
223 }
224 else {
225 PPL_ASSERT(r == SIGNED_2_COMPLEMENT);
226 mul_2exp_assign(max_value, Coefficient_one(), w-1);
227 neg_assign(min_value, max_value);
228 --max_value;
229 }
230
231 // If we are wrapping variables collectively, the ranges for the
232 // required translations are saved in `translations' instead of being
233 // immediately applied.
234 Wrap_Translations translations;
235
236 // Dimensions subject to translation are added to this set if we are
237 // wrapping collectively or if `cs_p' is non null.
238 Variables_Set dimensions_to_be_translated;
239
240 // This will contain a lower bound to the number of abstractions
241 // to be joined in order to obtain the collective wrapping result.
242 // As soon as this exceeds `complexity_threshold', counting will be
243 // interrupted and the full range will be the result of wrapping
244 // any dimension that is not fully contained in quadrant 0.
245 unsigned collective_wrap_complexity = 1;
246
247 // This flag signals that the maximum complexity for collective
248 // wrapping as been exceeded.
249 bool collective_wrap_too_complex = false;
250
251 if (!wrap_individually) {
252 translations.reserve(space_dim);
253 }
254
255 // We use `full_range_bounds' to delay conversions whenever
256 // this delay does not negatively affect precision.
257 Constraint_System full_range_bounds;
258
259 PPL_DIRTY_TEMP_COEFFICIENT(l_n);
260 PPL_DIRTY_TEMP_COEFFICIENT(l_d);
261 PPL_DIRTY_TEMP_COEFFICIENT(u_n);
262 PPL_DIRTY_TEMP_COEFFICIENT(u_d);
263
264 for (Variables_Set::const_iterator i = vars.begin(),
265 vars_end = vars.end(); i != vars_end; ++i) {
266
267 const Variable x(*i);
268
269 bool extremum;
270
271 if (!pointset.minimize(x, l_n, l_d, extremum)) {
272 set_full_range:
273 pointset.unconstrain(x);
274 full_range_bounds.insert(min_value <= x);
275 full_range_bounds.insert(x <= max_value);
276 continue;
277 }
278
279 if (!pointset.maximize(x, u_n, u_d, extremum)) {
280 goto set_full_range;
281 }
282
283 div_assign_r(l_n, l_n, l_d, ROUND_DOWN);
284 div_assign_r(u_n, u_n, u_d, ROUND_DOWN);
285 l_n -= min_value;
286 u_n -= min_value;
287 div_2exp_assign_r(l_n, l_n, w, ROUND_DOWN);
288 div_2exp_assign_r(u_n, u_n, w, ROUND_DOWN);
289 Coefficient& first_quadrant = l_n;
290 const Coefficient& last_quadrant = u_n;
291
292 // Special case: this variable does not need wrapping.
293 if (first_quadrant == 0 && last_quadrant == 0) {
294 continue;
295 }
296
297 // If overflow is impossible, try not to add useless constraints.
298 if (o == OVERFLOW_IMPOSSIBLE) {
299 if (first_quadrant < 0) {
300 full_range_bounds.insert(min_value <= x);
301 }
302 if (last_quadrant > 0) {
303 full_range_bounds.insert(x <= max_value);
304 }
305 continue;
306 }
307
308 if (o == OVERFLOW_UNDEFINED || collective_wrap_too_complex) {
309 goto set_full_range;
310 }
311
312 Coefficient& quadrants = u_d;
313 quadrants = last_quadrant - first_quadrant + 1;
314
315 PPL_UNINITIALIZED(unsigned, extension);
316 Result res = assign_r(extension, quadrants, ROUND_IGNORE);
317 if (result_overflow(res) != 0 || extension > complexity_threshold) {
318 goto set_full_range;
319 }
320
321 if (!wrap_individually && !collective_wrap_too_complex) {
322 res = mul_assign_r(collective_wrap_complexity,
323 collective_wrap_complexity, extension, ROUND_IGNORE);
324 if (result_overflow(res) != 0
325 || collective_wrap_complexity > complexity_threshold) {
326 collective_wrap_too_complex = true;
327 }
328 if (collective_wrap_too_complex) {
329 // Set all the dimensions in `translations' to full range.
330 for (Wrap_Translations::const_iterator j = translations.begin(),
331 translations_end = translations.end();
332 j != translations_end;
333 ++j) {
334 const Variable y(j->var);
335 pointset.unconstrain(y);
336 full_range_bounds.insert(min_value <= y);
337 full_range_bounds.insert(y <= max_value);
338 }
339 }
340 }
341
342 if (wrap_individually && cs_p == 0) {
343 Coefficient& quadrant = first_quadrant;
344 // Temporary variable holding the shifts to be applied in order
345 // to implement the translations.
346 Coefficient& shift = l_d;
347 PSET hull(space_dim, EMPTY);
348 for ( ; quadrant <= last_quadrant; ++quadrant) {
349 PSET p(pointset);
350 if (quadrant != 0) {
351 mul_2exp_assign(shift, quadrant, w);
352 p.affine_image(x, x - shift, 1);
353 }
354 p.refine_with_constraint(min_value <= x);
355 p.refine_with_constraint(x <= max_value);
356 hull.upper_bound_assign(p);
357 }
358 pointset.m_swap(hull);
359 }
360 else if (wrap_individually || !collective_wrap_too_complex) {
361 PPL_ASSERT(!wrap_individually || cs_p != 0);
362 dimensions_to_be_translated.insert(x);
363 translations
364 .push_back(Wrap_Dim_Translations(x, first_quadrant, last_quadrant));
365 }
366 }
367
368 if (!translations.empty()) {
369 if (wrap_individually) {
370 PPL_ASSERT(cs_p != 0);
371 wrap_assign_ind(pointset, dimensions_to_be_translated,
372 translations.begin(), translations.end(),
373 w, min_value, max_value, *cs_p, l_n, l_d);
374 }
375 else {
376 PSET hull(space_dim, EMPTY);
377 wrap_assign_col(hull, pointset, dimensions_to_be_translated,
378 translations.begin(), translations.end(),
379 w, min_value, max_value, cs_p, l_n);
380 pointset.m_swap(hull);
381 }
382 }
383
384 if (cs_p != 0) {
385 pointset.refine_with_constraints(*cs_p);
386 }
387 pointset.refine_with_constraints(full_range_bounds);
388 }
389
390 } // namespace Implementation
391
392 } // namespace Parma_Polyhedra_Library
393
394 #endif // !defined(PPL_wrap_assign_hh)
395