1 /* Polyhedron class implementation
2 (non-inline operators that may change the dimension of the vector space).
3 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
4 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
5
6 This file is part of the Parma Polyhedra Library (PPL).
7
8 The PPL is free software; you can redistribute it and/or modify it
9 under the terms of the GNU General Public License as published by the
10 Free Software Foundation; either version 3 of the License, or (at your
11 option) any later version.
12
13 The PPL is distributed in the hope that it will be useful, but WITHOUT
14 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
15 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
16 for more details.
17
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software Foundation,
20 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
21
22 For the most up-to-date information see the Parma Polyhedra Library
23 site: http://bugseng.com/products/ppl/ . */
24
25 #include "ppl-config.h"
26 #include "Polyhedron_defs.hh"
27 #include "Variables_Set_defs.hh"
28 #include "assertions.hh"
29
30 #define BE_LAZY 1
31
32 namespace PPL = Parma_Polyhedra_Library;
33
34 void
add_space_dimensions_and_embed(dimension_type m)35 PPL::Polyhedron::add_space_dimensions_and_embed(dimension_type m) {
36 // The space dimension of the resulting polyhedron should not
37 // overflow the maximum allowed space dimension.
38 check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
39 topology(),
40 "add_space_dimensions_and_embed(m)",
41 "adding m new space dimensions exceeds "
42 "the maximum allowed space dimension");
43
44 // Adding no dimensions to any polyhedron is a no-op.
45 if (m == 0) {
46 return;
47 }
48
49 // Adding dimensions to an empty polyhedron is obtained by adjusting
50 // `space_dim' and clearing `con_sys' (since it can contain the
51 // unsatisfiable constraint system of the wrong dimension).
52 if (marked_empty()) {
53 space_dim += m;
54 con_sys.clear();
55 return;
56 }
57
58 // The case of a zero-dimensional space polyhedron.
59 if (space_dim == 0) {
60 // Since it is not empty, it has to be the universe polyhedron.
61 PPL_ASSERT(status.test_zero_dim_univ());
62 // We swap `*this' with a newly created
63 // universe polyhedron of dimension `m'.
64 Polyhedron ph(topology(), m, UNIVERSE);
65 m_swap(ph);
66 return;
67 }
68
69 // To embed an n-dimension space polyhedron in a (n+m)-dimension space,
70 // we just add `m' zero-columns to the rows in the system of constraints;
71 // in contrast, the system of generators needs additional rows,
72 // corresponding to the vectors of the canonical basis
73 // for the added dimensions. That is, for each new dimension `x[k]'
74 // we add the line having that direction. This is done by invoking
75 // the function add_space_dimensions() giving the system of generators
76 // as the second argument.
77 if (constraints_are_up_to_date()) {
78 if (generators_are_up_to_date()) {
79 // `sat_c' must be up to date for add_space_dimensions().
80 if (!sat_c_is_up_to_date()) {
81 update_sat_c();
82 }
83 // Adds rows and/or columns to both matrices.
84 // `add_space_dimensions' correctly handles pending constraints
85 // or generators.
86 add_space_dimensions(con_sys, gen_sys, sat_c, sat_g, m);
87 }
88 else {
89 // Only constraints are up-to-date: no need to modify the generators.
90 con_sys.set_space_dimension(con_sys.space_dimension() + m);
91 }
92 }
93 else {
94 // Only generators are up-to-date: no need to modify the constraints.
95 PPL_ASSERT(generators_are_up_to_date());
96 gen_sys.add_universe_rows_and_space_dimensions(m);
97 }
98 // Update the space dimension.
99 space_dim += m;
100
101 // Note: we do not check for satisfiability, because the system of
102 // constraints may be unsatisfiable.
103 PPL_ASSERT_HEAVY(OK());
104 }
105
106 void
add_space_dimensions_and_project(dimension_type m)107 PPL::Polyhedron::add_space_dimensions_and_project(dimension_type m) {
108 // The space dimension of the resulting polyhedron should not
109 // overflow the maximum allowed space dimension.
110 check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
111 topology(),
112 "add_space_dimensions_and_project(m)",
113 "adding m new space dimensions exceeds "
114 "the maximum allowed space dimension");
115
116 // Adding no dimensions to any polyhedron is a no-op.
117 if (m == 0) {
118 return;
119 }
120
121 // Adding dimensions to an empty polyhedron is obtained
122 // by merely adjusting `space_dim'.
123 if (marked_empty()) {
124 space_dim += m;
125 con_sys.clear();
126 return;
127 }
128
129 if (space_dim == 0) {
130 PPL_ASSERT(status.test_zero_dim_univ() && gen_sys.has_no_rows());
131 // The system of generators for this polyhedron has only
132 // the origin as a point.
133 // In an NNC polyhedron, all points have to be accompanied
134 // by the corresponding closure points
135 // (this time, dimensions are automatically adjusted).
136 if (!is_necessarily_closed()) {
137 gen_sys.insert(Generator::zero_dim_closure_point());
138 }
139 gen_sys.insert(Generator::zero_dim_point());
140 gen_sys.adjust_topology_and_space_dimension(topology(), m);
141 set_generators_minimized();
142 space_dim = m;
143 PPL_ASSERT_HEAVY(OK());
144 return;
145 }
146
147 // To project an n-dimension space polyhedron in a (n+m)-dimension space,
148 // we just add to the system of generators `m' zero-columns;
149 // In contrast, in the system of constraints, new rows are needed
150 // in order to avoid embedding the old polyhedron in the new space.
151 // Thus, for each new dimensions `x[k]', we add the constraint
152 // x[k] = 0: this is done by invoking the function add_space_dimensions()
153 // giving the system of constraints as the second argument.
154 if (constraints_are_up_to_date()) {
155 if (generators_are_up_to_date()) {
156 // `sat_g' must be up to date for add_space_dimensions().
157 if (!sat_g_is_up_to_date()) {
158 update_sat_g();
159 }
160 // Adds rows and/or columns to both matrices.
161 // `add_space_dimensions()' correctly handles pending constraints
162 // or generators.
163 add_space_dimensions(gen_sys, con_sys, sat_g, sat_c, m);
164 }
165 else {
166 // Only constraints are up-to-date: no need to modify the generators.
167 con_sys.add_universe_rows_and_space_dimensions(m);
168 }
169 }
170 else {
171 // Only generators are up-to-date: no need to modify the constraints.
172 PPL_ASSERT(generators_are_up_to_date());
173 gen_sys.set_space_dimension(gen_sys.space_dimension() + m);
174 }
175 // Now we update the space dimension.
176 space_dim += m;
177
178 // Note: we do not check for satisfiability, because the system of
179 // constraints may be unsatisfiable.
180 PPL_ASSERT_HEAVY(OK());
181 }
182
183 void
concatenate_assign(const Polyhedron & y)184 PPL::Polyhedron::concatenate_assign(const Polyhedron& y) {
185 if (topology() != y.topology()) {
186 throw_topology_incompatible("concatenate_assign(y)", "y", y);
187 }
188
189 // The space dimension of the resulting polyhedron should not
190 // overflow the maximum allowed space dimension.
191 const dimension_type added_columns = y.space_dim;
192 check_space_dimension_overflow(added_columns,
193 max_space_dimension() - space_dimension(),
194 topology(),
195 "concatenate_assign(y)",
196 "concatenation exceeds the maximum "
197 "allowed space dimension");
198
199 // If `*this' or `y' are empty polyhedra, it is sufficient to adjust
200 // the dimension of the space.
201 if (marked_empty() || y.marked_empty()) {
202 space_dim += added_columns;
203 set_empty();
204 return;
205 }
206
207 // If `y' is a non-empty 0-dim space polyhedron, the result is `*this'.
208 if (added_columns == 0) {
209 return;
210 }
211
212 // If `*this' is a non-empty 0-dim space polyhedron, the result is `y'.
213 if (space_dim == 0) {
214 *this = y;
215 return;
216 }
217
218 // TODO: this implementation is just an executable specification.
219 Constraint_System cs = y.constraints();
220
221 // The constraints of `x' (possibly with pending rows) are required.
222 if (has_pending_generators()) {
223 process_pending_generators();
224 }
225 else if (!constraints_are_up_to_date()) {
226 update_constraints();
227 }
228
229 // The matrix for the new system of constraints is obtained
230 // by leaving the old system of constraints in the upper left-hand side
231 // and placing the constraints of `cs' in the lower right-hand side.
232 // NOTE: here topologies agree, whereas dimensions may not agree.
233 const dimension_type added_rows = cs.num_rows();
234
235 // We already dealt with the cases of an empty or zero-dim `y' polyhedron;
236 // also, `cs' contains the low-level constraints, at least.
237 PPL_ASSERT(added_rows > 0 && added_columns > 0);
238
239 con_sys.set_space_dimension(con_sys.space_dimension() + added_columns);
240
241 if (can_have_something_pending()) {
242 // Steal the constraints from `cs' and put them in `con_sys'
243 // using the right displacement for coefficients.
244 for (dimension_type i = 0; i < added_rows; ++i) {
245 cs.sys.rows[i].shift_space_dimensions(Variable(0), space_dim);
246 con_sys.insert_pending(cs.sys.rows[i], Recycle_Input());
247 }
248 cs.clear();
249
250 // If `*this' can support pending constraints, then, since we have
251 // resized the system of constraints, we must also add to the generator
252 // system those lines corresponding to the newly added dimensions,
253 // because the non-pending parts of `con_sys' and `gen_sys' must still
254 // be a DD pair in minimal form.
255 gen_sys.add_universe_rows_and_space_dimensions(added_columns);
256 // Since we added new lines at the beginning of `x.gen_sys',
257 // we also have to adjust the saturation matrix `sat_c'.
258 // FIXME: if `sat_c' is not up-to-date, could not we directly update
259 // `sat_g' by resizing it and shifting its columns?
260 if (!sat_c_is_up_to_date()) {
261 sat_c.transpose_assign(sat_g);
262 set_sat_c_up_to_date();
263 }
264 clear_sat_g_up_to_date();
265 sat_c.resize(sat_c.num_rows() + added_columns, sat_c.num_columns());
266 // The old saturation rows are copied at the end of the matrix.
267 // The newly introduced lines saturate all the non-pending constraints,
268 // thus their saturation rows are made of zeroes.
269 using std::swap;
270 for (dimension_type i = sat_c.num_rows() - added_columns;
271 i-- > 0; ) {
272 swap(sat_c[i], sat_c[i+added_columns]);
273 }
274 // Since `added_rows > 0', we now have pending constraints.
275 set_constraints_pending();
276 }
277 else {
278 // Steal the constraints from `cs' and put them in `con_sys'
279 // using the right displacement for coefficients.
280 for (dimension_type i = 0; i < added_rows; ++i) {
281 cs.sys.rows[i].shift_space_dimensions(Variable(0), space_dim);
282 con_sys.insert(cs.sys.rows[i], Recycle_Input());
283 }
284 #if !BE_LAZY
285 con_sys.sort_rows();
286 #endif
287 clear_constraints_minimized();
288 clear_generators_up_to_date();
289 clear_sat_g_up_to_date();
290 clear_sat_c_up_to_date();
291 }
292 // Update space dimension.
293 space_dim += added_columns;
294
295 // The system of constraints may be unsatisfiable,
296 // thus we do not check for satisfiability.
297 PPL_ASSERT_HEAVY(OK());
298 }
299
300 void
remove_space_dimensions(const Variables_Set & vars)301 PPL::Polyhedron::remove_space_dimensions(const Variables_Set& vars) {
302 // The removal of no dimensions from any polyhedron is a no-op.
303 // Note that this case also captures the only legal removal of
304 // dimensions from a polyhedron in a 0-dim space.
305 if (vars.empty()) {
306 PPL_ASSERT_HEAVY(OK());
307 return;
308 }
309
310 // Dimension-compatibility check.
311 const dimension_type min_space_dim = vars.space_dimension();
312 if (space_dim < min_space_dim) {
313 throw_dimension_incompatible("remove_space_dimensions(vs)", min_space_dim);
314 }
315
316 const dimension_type new_space_dim = space_dim - vars.size();
317
318 // We need updated generators; note that keeping pending generators
319 // is useless because the constraints will be dropped anyway.
320 if (marked_empty()
321 || (has_something_pending() && !remove_pending_to_obtain_generators())
322 || (!generators_are_up_to_date() && !update_generators())) {
323 // Removing dimensions from the empty polyhedron:
324 // we clear `con_sys' since it could have contained the
325 // unsatisfiable constraint of the wrong dimension.
326 con_sys.clear();
327 // Update the space dimension.
328 space_dim = new_space_dim;
329 PPL_ASSERT_HEAVY(OK());
330 return;
331 }
332
333 // When removing _all_ dimensions from a non-empty polyhedron,
334 // we obtain the zero-dimensional universe polyhedron.
335 if (new_space_dim == 0) {
336 set_zero_dim_univ();
337 return;
338 }
339
340 gen_sys.remove_space_dimensions(vars);
341
342 // Constraints are not up-to-date and generators are not minimized.
343 clear_constraints_up_to_date();
344 clear_generators_minimized();
345
346 // Update the space dimension.
347 space_dim = new_space_dim;
348
349 PPL_ASSERT_HEAVY(OK(true));
350 }
351
352 void
remove_higher_space_dimensions(dimension_type new_dimension)353 PPL::Polyhedron::remove_higher_space_dimensions(dimension_type new_dimension) {
354 // Dimension-compatibility check.
355 if (new_dimension > space_dim) {
356 throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
357 new_dimension);
358 }
359
360 // The removal of no dimensions from any polyhedron is a no-op.
361 // Note that this case also captures the only legal removal of
362 // dimensions from a polyhedron in a 0-dim space.
363 if (new_dimension == space_dim) {
364 PPL_ASSERT_HEAVY(OK());
365 return;
366 }
367
368 // We need updated generators; note that keeping pending generators
369 // is useless because constraints will be dropped anyway.
370 if (marked_empty()
371 || (has_something_pending() && !remove_pending_to_obtain_generators())
372 || (!generators_are_up_to_date() && !update_generators())) {
373 // Removing dimensions from the empty polyhedron:
374 // just updates the space dimension.
375 space_dim = new_dimension;
376 con_sys.clear();
377 PPL_ASSERT_HEAVY(OK());
378 return;
379 }
380
381 if (new_dimension == 0) {
382 // Removing all dimensions from a non-empty polyhedron:
383 // just return the zero-dimensional universe polyhedron.
384 set_zero_dim_univ();
385 return;
386 }
387
388 gen_sys.set_space_dimension(new_dimension);
389
390 // Constraints are not up-to-date and generators are not minimized.
391 clear_constraints_up_to_date();
392 clear_generators_minimized();
393
394 // Update the space dimension.
395 space_dim = new_dimension;
396
397 PPL_ASSERT_HEAVY(OK(true));
398 }
399
400 void
expand_space_dimension(Variable var,dimension_type m)401 PPL::Polyhedron::expand_space_dimension(Variable var, dimension_type m) {
402 // `var' should be one of the dimensions of the vector space.
403 if (var.space_dimension() > space_dim) {
404 throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var);
405 }
406
407 // The space dimension of the resulting polyhedron should not
408 // overflow the maximum allowed space dimension.
409 check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
410 topology(),
411 "expand_dimension(v, m)",
412 "adding m new space dimensions exceeds "
413 "the maximum allowed space dimension");
414
415 // Nothing to do, if no dimensions must be added.
416 if (m == 0) {
417 return;
418 }
419
420 // Keep track of the dimension before adding the new ones.
421 const dimension_type old_dim = space_dim;
422
423 // Add the required new dimensions.
424 add_space_dimensions_and_embed(m);
425
426 const Constraint_System& cs = constraints();
427 Constraint_System new_constraints(cs.topology());
428 for (Constraint_System::const_iterator i = cs.begin(),
429 cs_end = cs.end(); i != cs_end; ++i) {
430 const Constraint& c = *i;
431
432 Coefficient_traits::const_reference coeff = c.coefficient(var);
433
434 // If `c' does not constrain `var', skip it.
435 if (coeff == 0) {
436 continue;
437 }
438
439 Constraint c_template = c;
440 c_template.expr.set_coefficient(var, Coefficient_zero());
441
442 // Each relevant constraint results in `m' new constraints.
443 for (dimension_type dst_d = old_dim; dst_d < old_dim+m; ++dst_d) {
444 Constraint new_c = c_template;
445 add_mul_assign(new_c.expr, coeff, Variable(dst_d));
446 PPL_ASSERT(new_c.OK());
447 new_constraints.insert(new_c, Recycle_Input());
448 }
449 }
450 add_recycled_constraints(new_constraints);
451 PPL_ASSERT_HEAVY(OK());
452 }
453
454 void
fold_space_dimensions(const Variables_Set & vars,Variable dest)455 PPL::Polyhedron::fold_space_dimensions(const Variables_Set& vars,
456 Variable dest) {
457 // TODO: this implementation is _really_ an executable specification.
458
459 // `dest' should be one of the dimensions of the polyhedron.
460 if (dest.space_dimension() > space_dim) {
461 throw_dimension_incompatible("fold_space_dimensions(vs, v)", "v", dest);
462 }
463
464 // The folding of no dimensions is a no-op.
465 if (vars.empty()) {
466 return;
467 }
468
469 // All variables in `vars' should be dimensions of the polyhedron.
470 if (vars.space_dimension() > space_dim) {
471 throw_dimension_incompatible("fold_space_dimensions(vs, v)",
472 "vs.space_dimension()",
473 vars.space_dimension());
474 }
475
476 // Moreover, `dest.id()' should not occur in `vars'.
477 if (vars.find(dest.id()) != vars.end()) {
478 throw_invalid_argument("fold_space_dimensions(vs, v)",
479 "v should not occur in vs");
480 }
481
482 // All of the affine images we are going to compute are not invertible,
483 // hence we will need to compute the generators of the polyhedron.
484 // Since we keep taking copies, make sure that a single conversion
485 // from constraints to generators is computed.
486 (void) generators();
487 // Having generators, we now know if the polyhedron is empty:
488 // in that case, folding is equivalent to just removing space dimensions.
489 if (!marked_empty()) {
490 for (Variables_Set::const_iterator i = vars.begin(),
491 vs_end = vars.end(); i != vs_end; ++i) {
492 Polyhedron copy = *this;
493 copy.affine_image(dest, Linear_Expression(Variable(*i)));
494 poly_hull_assign(copy);
495 }
496 }
497 remove_space_dimensions(vars);
498 PPL_ASSERT_HEAVY(OK());
499 }
500