1 /* Grid 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 "Grid_defs.hh"
27 #include "Variables_Set_defs.hh"
28 #include "assertions.hh"
29
30 namespace PPL = Parma_Polyhedra_Library;
31
32 // Used for add_space_dimensions_and_embed.
33 void
add_space_dimensions(Congruence_System & cgs,Grid_Generator_System & gs,const dimension_type dims)34 PPL::Grid::add_space_dimensions(Congruence_System& cgs,
35 Grid_Generator_System& gs,
36 const dimension_type dims) {
37 PPL_ASSERT(cgs.space_dimension() == gs.space_dimension());
38 PPL_ASSERT(dims > 0);
39
40 const dimension_type old_modulus_index = cgs.space_dimension() + 1;
41 cgs.set_space_dimension(space_dimension() + dims);
42
43 if (congruences_are_minimized() || generators_are_minimized()) {
44 dim_kinds.resize(old_modulus_index + dims, CON_VIRTUAL /* a.k.a. LINE */);
45 }
46
47 gs.add_universe_rows_and_columns(dims);
48 }
49
50 // Used for add_space_dimensions_and_project.
51 void
add_space_dimensions(Grid_Generator_System & gs,Congruence_System & cgs,const dimension_type dims)52 PPL::Grid::add_space_dimensions(Grid_Generator_System& gs,
53 Congruence_System& cgs,
54 const dimension_type dims) {
55 PPL_ASSERT(cgs.space_dimension() == gs.space_dimension());
56 PPL_ASSERT(dims > 0);
57
58 cgs.add_unit_rows_and_space_dimensions(dims);
59
60 // Add `dims' zero columns onto gs.
61 gs.set_space_dimension(space_dim + dims);
62
63 normalize_divisors(gs);
64
65 dim_kinds.resize(cgs.space_dimension() + 1, EQUALITY /* a.k.a GEN_VIRTUAL */);
66 }
67
68 // (o is a point) y
69 //
70 // | | |
71 // => | | |
72 // | | |
73 // o---o---o-- x |---|---|-- x
74 // 0 1 2 3 4 5 0 1 2 3 4 5
75 // R^1 R^2
76 void
add_space_dimensions_and_embed(dimension_type m)77 PPL::Grid::add_space_dimensions_and_embed(dimension_type m) {
78 if (m == 0) {
79 return;
80 }
81
82 // The space dimension of the resulting grid must be at most the
83 // maximum allowed space dimension.
84 check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
85 "PPL::Grid::",
86 "add_space_dimensions_and_embed(m)",
87 "adding m new space dimensions exceeds "
88 "the maximum allowed space dimension");
89
90 // Adding dimensions to an empty grid is obtained by adjusting
91 // `space_dim' and clearing `con_sys' (since it can contain the
92 // integrality congruence of the current dimension).
93 if (marked_empty()) {
94 space_dim += m;
95 set_empty();
96 return;
97 }
98
99 // The case of a zero-dimension space grid.
100 if (space_dim == 0) {
101 // Since it is not empty, it has to be the universe grid.
102 PPL_ASSERT(status.test_zero_dim_univ());
103 // Swap *this with a newly created `m'-dimensional universe grid.
104 Grid gr(m, UNIVERSE);
105 m_swap(gr);
106 return;
107 }
108
109 // To embed an n-dimension space grid in a (n+m)-dimension space, we
110 // add `m' zero-columns to the rows in the system of congruences; in
111 // contrast, the system of generators needs additional rows,
112 // corresponding to the vectors of the canonical basis for the added
113 // dimensions. That is, for each new dimension we add the line
114 // having that direction. This is done by invoking the function
115 // add_space_dimensions().
116 if (congruences_are_up_to_date()) {
117 if (generators_are_up_to_date()) {
118 // Adds rows and/or columns to both matrices.
119 add_space_dimensions(con_sys, gen_sys, m);
120 }
121 else {
122 // Only congruences are up-to-date, so modify only them.
123 con_sys.set_space_dimension(con_sys.space_dimension() + m);
124 if (congruences_are_minimized()) {
125 dim_kinds.resize(con_sys.space_dimension() + 1, CON_VIRTUAL);
126 }
127 }
128 }
129 else {
130 // Only generators are up-to-date, so modify only them.
131 PPL_ASSERT(generators_are_up_to_date());
132 gen_sys.add_universe_rows_and_columns(m);
133 if (generators_are_minimized()) {
134 dim_kinds.resize(gen_sys.space_dimension() + 1, LINE);
135 }
136 }
137 // Update the space dimension.
138 space_dim += m;
139
140 // Note: we do not check for satisfiability, because the system of
141 // congruences may be unsatisfiable.
142 PPL_ASSERT(OK());
143 }
144
145 // (o is a point) y
146 //
147 //
148 // =>
149 //
150 // o---o---o-- x o---o---o-- x
151 // 0 1 2 3 4 5 0 1 2 3 4 5
152 // R^1 R^2
153 void
add_space_dimensions_and_project(dimension_type m)154 PPL::Grid::add_space_dimensions_and_project(dimension_type m) {
155 if (m == 0) {
156 return;
157 }
158
159 // The space dimension of the resulting grid should be at most the
160 // maximum allowed space dimension.
161 check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
162 "PPL::Grid::",
163 "add_space_dimensions_and_project(m)",
164 "adding m new space dimensions exceeds "
165 "the maximum allowed space dimension");
166
167 // Adding dimensions to an empty grid is obtained by merely
168 // adjusting `space_dim'.
169 if (marked_empty()) {
170 space_dim += m;
171 set_empty();
172 return;
173 }
174
175 if (space_dim == 0) {
176 PPL_ASSERT(status.test_zero_dim_univ());
177 // Swap *this with a newly created `n'-dimensional universe grid.
178 Grid gr(m, UNIVERSE);
179 m_swap(gr);
180 return;
181 }
182
183 // To project an n-dimension space grid in a (n+m)-dimension space,
184 // we just add to the system of generators `m' zero-columns; in
185 // contrast, in the system of congruences, new rows are needed in
186 // order to avoid embedding the old grid in the new space. Thus,
187 // for each new dimensions `x[k]', we add the constraint x[k] = 0;
188 // this is done by invoking the function add_space_dimensions()
189 // giving the system of constraints as the second argument.
190 if (congruences_are_up_to_date()) {
191 if (generators_are_up_to_date()) {
192 // Add rows and/or columns to both matrices.
193 add_space_dimensions(gen_sys, con_sys, m);
194 }
195 else {
196 // Only congruences are up-to-date so modify only them.
197 con_sys.add_unit_rows_and_space_dimensions(m);
198 if (congruences_are_minimized()) {
199 dim_kinds.resize(con_sys.space_dimension() + 1, EQUALITY);
200 }
201 }
202 }
203 else {
204 // Only generators are up-to-date so modify only them.
205 PPL_ASSERT(generators_are_up_to_date());
206
207 // Add m zero columns onto gs.
208 gen_sys.set_space_dimension(space_dim + m);
209
210 normalize_divisors(gen_sys);
211
212 if (generators_are_minimized()) {
213 dim_kinds.resize(gen_sys.space_dimension() + 1, EQUALITY);
214 }
215 }
216 // Now update the space dimension.
217 space_dim += m;
218
219 // Note: we do not check for satisfiability, because the system of
220 // congruences may be unsatisfiable.
221 PPL_ASSERT(OK());
222 }
223
224 void
concatenate_assign(const Grid & y)225 PPL::Grid::concatenate_assign(const Grid& y) {
226 // The space dimension of the resulting grid must be at most the
227 // maximum allowed space dimension.
228 check_space_dimension_overflow(y.space_dimension(),
229 max_space_dimension() - space_dimension(),
230 "PPL::Grid::",
231 "concatenate_assign(y)",
232 "concatenation exceeds the maximum "
233 "allowed space dimension");
234
235 const dimension_type added_columns = y.space_dim;
236
237 // If `*this' or `y' are empty grids just adjust the space
238 // dimension.
239 if (marked_empty() || y.marked_empty()) {
240 space_dim += added_columns;
241 set_empty();
242 return;
243 }
244
245 // If `y' is a universe 0-dim grid, the result is `*this'.
246 if (added_columns == 0) {
247 return;
248 }
249
250 // If `*this' is a universe 0-dim space grid, the result is `y'.
251 if (space_dim == 0) {
252 *this = y;
253 return;
254 }
255
256 if (!congruences_are_up_to_date()) {
257 update_congruences();
258 }
259
260 con_sys.concatenate(y.congruences());
261
262 space_dim += added_columns;
263
264 clear_congruences_minimized();
265 clear_generators_up_to_date();
266
267 // Check that the system is OK, taking into account that the system
268 // of congruences may now be empty.
269 PPL_ASSERT(OK());
270 }
271
272 void
remove_space_dimensions(const Variables_Set & vars)273 PPL::Grid::remove_space_dimensions(const Variables_Set& vars) {
274 // The removal of no dimensions from any grid is a no-op. This case
275 // also captures the only legal removal of dimensions from a grid in
276 // a 0-dim space.
277 if (vars.empty()) {
278 PPL_ASSERT(OK());
279 return;
280 }
281
282 // Dimension-compatibility check.
283 const dimension_type min_space_dim = vars.space_dimension();
284 if (space_dim < min_space_dim) {
285 throw_dimension_incompatible("remove_space_dimensions(vs)", min_space_dim);
286 }
287
288 const dimension_type new_space_dim = space_dim - vars.size();
289
290 if (marked_empty()
291 || (!generators_are_up_to_date() && !update_generators())) {
292 // Update the space dimension.
293 space_dim = new_space_dim;
294 set_empty();
295 PPL_ASSERT(OK());
296 return;
297 }
298
299 // Removing _all_ dimensions from a non-empty grid obtains the
300 // zero-dimensional universe grid.
301 if (new_space_dim == 0) {
302 set_zero_dim_univ();
303 return;
304 }
305
306 gen_sys.remove_space_dimensions(vars);
307
308 clear_congruences_up_to_date();
309 clear_generators_minimized();
310
311 // Update the space dimension.
312 space_dim = new_space_dim;
313
314 PPL_ASSERT(OK(true));
315 }
316
317 void
remove_higher_space_dimensions(const dimension_type new_dimension)318 PPL::Grid::remove_higher_space_dimensions(const dimension_type new_dimension) {
319 // Dimension-compatibility check.
320 if (new_dimension > space_dim) {
321 throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
322 new_dimension);
323 }
324 // The removal of no dimensions from any grid is a no-op.
325 // Note that this case also captures the only legal removal of
326 // dimensions from a grid in a 0-dim space.
327 if (new_dimension == space_dim) {
328 PPL_ASSERT(OK());
329 return;
330 }
331
332 if (is_empty()) {
333 // Removing dimensions from the empty grid just updates the space
334 // dimension.
335 space_dim = new_dimension;
336 set_empty();
337 PPL_ASSERT(OK());
338 return;
339 }
340
341 if (new_dimension == 0) {
342 // Removing all dimensions from a non-empty grid just returns the
343 // zero-dimensional universe grid.
344 set_zero_dim_univ();
345 return;
346 }
347
348 // Favor the generators, as is done by is_empty().
349 if (generators_are_up_to_date()) {
350 gen_sys.set_space_dimension(new_dimension);
351 if (generators_are_minimized()) {
352 // Count the actual number of rows that are now redundant.
353 dimension_type num_redundant = 0;
354 const dimension_type num_old_gs = space_dim - new_dimension;
355 for (dimension_type row = 0; row < num_old_gs; ++row) {
356 if (dim_kinds[row] != GEN_VIRTUAL) {
357 ++num_redundant;
358 }
359 }
360 if (num_redundant > 0) {
361 // Chop zero rows from end of system, to keep minimal form.
362 gen_sys.remove_trailing_rows(num_redundant);
363 gen_sys.unset_pending_rows();
364 }
365 dim_kinds.resize(new_dimension + 1);
366 // TODO: Consider if it is worth also preserving the congruences
367 // if they are also in minimal form.
368 }
369 clear_congruences_up_to_date();
370 // Extend the zero dim false congruence system to the appropriate
371 // dimension and then swap it with `con_sys'.
372 Congruence_System cgs(Congruence::zero_dim_false());
373 // Extra 2 columns for inhomogeneous term and modulus.
374 cgs.set_space_dimension(new_dimension + 2);
375 swap(con_sys, cgs);
376 }
377 else {
378 PPL_ASSERT(congruences_are_minimized());
379 con_sys.set_space_dimension(new_dimension);
380 // Count the actual number of rows that are now redundant.
381 dimension_type num_redundant = 0;
382 for (dimension_type row = space_dim; row > new_dimension; --row) {
383 if (dim_kinds[row] != CON_VIRTUAL) {
384 ++num_redundant;
385 }
386 }
387
388 con_sys.remove_rows(0, num_redundant, true);
389 dim_kinds.erase(dim_kinds.begin() + (new_dimension + 1),
390 dim_kinds.end());
391
392 clear_generators_up_to_date();
393 // Replace gen_sys with an empty system of the right dimension.
394 // Extra 2 columns for inhomogeneous term and modulus.
395 Grid_Generator_System gs(new_dimension + 2);
396 gen_sys.m_swap(gs);
397 }
398
399 // Update the space dimension.
400 space_dim = new_dimension;
401
402 PPL_ASSERT(OK(true));
403 }
404
405 void
expand_space_dimension(Variable var,dimension_type m)406 PPL::Grid::expand_space_dimension(Variable var, dimension_type m) {
407 // `var' must be one of the dimensions of the vector space.
408 if (var.space_dimension() > space_dim) {
409 throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var);
410 }
411
412 // Adding 0 dimensions leaves the same grid.
413 if (m == 0) {
414 return;
415 }
416
417 // The resulting space dimension must be at most the maximum.
418 check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
419 "PPL::Grid::",
420 "expand_space_dimension(v, m)",
421 "adding m new space dimensions exceeds "
422 "the maximum allowed space dimension");
423
424 // Save the number of dimensions before adding new ones.
425 const dimension_type old_dim = space_dim;
426
427 // Add the required new dimensions.
428 add_space_dimensions_and_embed(m);
429
430 const Congruence_System& cgs = congruences();
431 Congruence_System new_congruences;
432 for (Congruence_System::const_iterator i = cgs.begin(),
433 cgs_end = cgs.end(); i != cgs_end; ++i) {
434 const Congruence& cg = *i;
435
436 Coefficient_traits::const_reference coeff = cg.coefficient(var);
437
438 // Only consider congruences that constrain `var'.
439 if (coeff == 0) {
440 continue;
441 }
442
443 Congruence cg_copy = cg;
444 cg_copy.expr.set_coefficient(var, Coefficient_zero());
445
446 // Each relevant congruence results in `m' new congruences.
447 for (dimension_type dst_d = old_dim; dst_d < old_dim+m; ++dst_d) {
448 Congruence x = cg_copy;
449 add_mul_assign(x.expr, coeff, Variable(dst_d));
450 new_congruences.insert_verbatim(x, Recycle_Input());
451 }
452 }
453 add_recycled_congruences(new_congruences);
454 PPL_ASSERT(OK());
455 }
456
457 void
fold_space_dimensions(const Variables_Set & vars,Variable dest)458 PPL::Grid::fold_space_dimensions(const Variables_Set& vars, Variable dest) {
459 // TODO: this implementation is _really_ an executable specification.
460
461 // `dest' should be one of the dimensions of the grid.
462 if (dest.space_dimension() > space_dim) {
463 throw_dimension_incompatible("fold_space_dimensions(vs, v)", "v", dest);
464 }
465
466 // Folding only has effect if dimensions are given.
467 if (vars.empty()) {
468 return;
469 }
470
471 // All variables in `vars' must be dimensions of the grid.
472 if (vars.space_dimension() > space_dim) {
473 throw_dimension_incompatible("fold_space_dimensions(vs, v)",
474 "vs.space_dimension()",
475 vars.space_dimension());
476 }
477
478 // Moreover, `dest.id()' must not occur in `vars'.
479 if (vars.find(dest.id()) != vars.end()) {
480 throw_invalid_argument("fold_space_dimensions(vs, v)",
481 "v should not occur in vs");
482 }
483 // All of the affine images we are going to compute are not invertible,
484 // hence we will need to compute the grid generators of the polyhedron.
485 // Since we keep taking copies, make sure that a single conversion
486 // from congruences to grid generators is computed.
487 (void) grid_generators();
488 // Having grid generators, we now know if the grid is empty:
489 // in that case, folding is equivalent to just removing space dimensions.
490 if (!marked_empty()) {
491 for (Variables_Set::const_iterator i = vars.begin(),
492 vs_end = vars.end(); i != vs_end; ++i) {
493 Grid copy = *this;
494 copy.affine_image(dest, Linear_Expression(Variable(*i)));
495 upper_bound_assign(copy);
496 }
497 }
498 remove_space_dimensions(vars);
499 PPL_ASSERT(OK());
500 }
501