Line data Source code
1 : /*
2 : * Copyright 2010-2011 INRIA Saclay
3 : * Copyright 2014 Ecole Normale Superieure
4 : *
5 : * Use of this software is governed by the MIT license
6 : *
7 : * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
8 : * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
9 : * 91893 Orsay, France
10 : * and Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France
11 : */
12 :
13 : #include <isl_map_private.h>
14 : #include <isl_aff_private.h>
15 : #include <isl_morph.h>
16 : #include <isl_seq.h>
17 : #include <isl_mat_private.h>
18 : #include <isl_space_private.h>
19 : #include <isl_equalities.h>
20 : #include <isl_id_private.h>
21 :
22 0 : isl_ctx *isl_morph_get_ctx(__isl_keep isl_morph *morph)
23 : {
24 0 : if (!morph)
25 0 : return NULL;
26 0 : return isl_basic_set_get_ctx(morph->dom);
27 : }
28 :
29 43956343 : __isl_give isl_morph *isl_morph_alloc(
30 : __isl_take isl_basic_set *dom, __isl_take isl_basic_set *ran,
31 : __isl_take isl_mat *map, __isl_take isl_mat *inv)
32 : {
33 : isl_morph *morph;
34 :
35 43956343 : if (!dom || !ran || !map || !inv)
36 : goto error;
37 :
38 43956343 : morph = isl_alloc_type(dom->ctx, struct isl_morph);
39 43956343 : if (!morph)
40 0 : goto error;
41 :
42 43956343 : morph->ref = 1;
43 43956343 : morph->dom = dom;
44 43956343 : morph->ran = ran;
45 43956343 : morph->map = map;
46 43956343 : morph->inv = inv;
47 :
48 43956343 : return morph;
49 : error:
50 0 : isl_basic_set_free(dom);
51 0 : isl_basic_set_free(ran);
52 0 : isl_mat_free(map);
53 0 : isl_mat_free(inv);
54 0 : return NULL;
55 : }
56 :
57 221199 : __isl_give isl_morph *isl_morph_copy(__isl_keep isl_morph *morph)
58 : {
59 221199 : if (!morph)
60 0 : return NULL;
61 :
62 221199 : morph->ref++;
63 221199 : return morph;
64 : }
65 :
66 0 : __isl_give isl_morph *isl_morph_dup(__isl_keep isl_morph *morph)
67 : {
68 0 : if (!morph)
69 0 : return NULL;
70 :
71 0 : return isl_morph_alloc(isl_basic_set_copy(morph->dom),
72 : isl_basic_set_copy(morph->ran),
73 : isl_mat_copy(morph->map), isl_mat_copy(morph->inv));
74 : }
75 :
76 92093 : __isl_give isl_morph *isl_morph_cow(__isl_take isl_morph *morph)
77 : {
78 92093 : if (!morph)
79 0 : return NULL;
80 :
81 92093 : if (morph->ref == 1)
82 92093 : return morph;
83 0 : morph->ref--;
84 0 : return isl_morph_dup(morph);
85 : }
86 :
87 44177542 : __isl_null isl_morph *isl_morph_free(__isl_take isl_morph *morph)
88 : {
89 44177542 : if (!morph)
90 0 : return NULL;
91 :
92 44177542 : if (--morph->ref > 0)
93 221199 : return NULL;
94 :
95 43956343 : isl_basic_set_free(morph->dom);
96 43956343 : isl_basic_set_free(morph->ran);
97 43956343 : isl_mat_free(morph->map);
98 43956343 : isl_mat_free(morph->inv);
99 43956343 : free(morph);
100 :
101 43956343 : return NULL;
102 : }
103 :
104 : /* Is "morph" an identity on the parameters?
105 : */
106 0 : static int identity_on_parameters(__isl_keep isl_morph *morph)
107 : {
108 : int is_identity;
109 : unsigned nparam;
110 : isl_mat *sub;
111 :
112 0 : nparam = isl_morph_dom_dim(morph, isl_dim_param);
113 0 : if (nparam != isl_morph_ran_dim(morph, isl_dim_param))
114 0 : return 0;
115 0 : if (nparam == 0)
116 0 : return 1;
117 0 : sub = isl_mat_sub_alloc(morph->map, 0, 1 + nparam, 0, 1 + nparam);
118 0 : is_identity = isl_mat_is_scaled_identity(sub);
119 0 : isl_mat_free(sub);
120 :
121 0 : return is_identity;
122 : }
123 :
124 : /* Return an affine expression of the variables of the range of "morph"
125 : * in terms of the parameters and the variables of the domain on "morph".
126 : *
127 : * In order for the space manipulations to make sense, we require
128 : * that the parameters are not modified by "morph".
129 : */
130 0 : __isl_give isl_multi_aff *isl_morph_get_var_multi_aff(
131 : __isl_keep isl_morph *morph)
132 : {
133 : isl_space *dom, *ran, *space;
134 : isl_local_space *ls;
135 : isl_multi_aff *ma;
136 : unsigned nparam, nvar;
137 : int i;
138 : int is_identity;
139 :
140 0 : if (!morph)
141 0 : return NULL;
142 :
143 0 : is_identity = identity_on_parameters(morph);
144 0 : if (is_identity < 0)
145 0 : return NULL;
146 0 : if (!is_identity)
147 0 : isl_die(isl_morph_get_ctx(morph), isl_error_invalid,
148 : "cannot handle parameter compression", return NULL);
149 :
150 0 : dom = isl_morph_get_dom_space(morph);
151 0 : ls = isl_local_space_from_space(isl_space_copy(dom));
152 0 : ran = isl_morph_get_ran_space(morph);
153 0 : space = isl_space_map_from_domain_and_range(dom, ran);
154 0 : ma = isl_multi_aff_zero(space);
155 :
156 0 : nparam = isl_multi_aff_dim(ma, isl_dim_param);
157 0 : nvar = isl_multi_aff_dim(ma, isl_dim_out);
158 0 : for (i = 0; i < nvar; ++i) {
159 : isl_val *val;
160 : isl_vec *v;
161 : isl_aff *aff;
162 :
163 0 : v = isl_mat_get_row(morph->map, 1 + nparam + i);
164 0 : v = isl_vec_insert_els(v, 0, 1);
165 0 : val = isl_mat_get_element_val(morph->map, 0, 0);
166 0 : v = isl_vec_set_element_val(v, 0, val);
167 0 : aff = isl_aff_alloc_vec(isl_local_space_copy(ls), v);
168 0 : ma = isl_multi_aff_set_aff(ma, i, aff);
169 : }
170 :
171 0 : isl_local_space_free(ls);
172 0 : return ma;
173 : }
174 :
175 : /* Return the domain space of "morph".
176 : */
177 0 : __isl_give isl_space *isl_morph_get_dom_space(__isl_keep isl_morph *morph)
178 : {
179 0 : if (!morph)
180 0 : return NULL;
181 :
182 0 : return isl_basic_set_get_space(morph->dom);
183 : }
184 :
185 0 : __isl_give isl_space *isl_morph_get_ran_space(__isl_keep isl_morph *morph)
186 : {
187 0 : if (!morph)
188 0 : return NULL;
189 :
190 0 : return isl_space_copy(morph->ran->dim);
191 : }
192 :
193 0 : unsigned isl_morph_dom_dim(__isl_keep isl_morph *morph, enum isl_dim_type type)
194 : {
195 0 : if (!morph)
196 0 : return 0;
197 :
198 0 : return isl_basic_set_dim(morph->dom, type);
199 : }
200 :
201 0 : unsigned isl_morph_ran_dim(__isl_keep isl_morph *morph, enum isl_dim_type type)
202 : {
203 0 : if (!morph)
204 0 : return 0;
205 :
206 0 : return isl_basic_set_dim(morph->ran, type);
207 : }
208 :
209 0 : __isl_give isl_morph *isl_morph_remove_dom_dims(__isl_take isl_morph *morph,
210 : enum isl_dim_type type, unsigned first, unsigned n)
211 : {
212 : unsigned dom_offset;
213 :
214 0 : if (n == 0)
215 0 : return morph;
216 :
217 0 : morph = isl_morph_cow(morph);
218 0 : if (!morph)
219 0 : return NULL;
220 :
221 0 : dom_offset = 1 + isl_space_offset(morph->dom->dim, type);
222 :
223 0 : morph->dom = isl_basic_set_remove_dims(morph->dom, type, first, n);
224 :
225 0 : morph->map = isl_mat_drop_cols(morph->map, dom_offset + first, n);
226 :
227 0 : morph->inv = isl_mat_drop_rows(morph->inv, dom_offset + first, n);
228 :
229 0 : if (morph->dom && morph->ran && morph->map && morph->inv)
230 0 : return morph;
231 :
232 0 : isl_morph_free(morph);
233 0 : return NULL;
234 : }
235 :
236 0 : __isl_give isl_morph *isl_morph_remove_ran_dims(__isl_take isl_morph *morph,
237 : enum isl_dim_type type, unsigned first, unsigned n)
238 : {
239 : unsigned ran_offset;
240 :
241 0 : if (n == 0)
242 0 : return morph;
243 :
244 0 : morph = isl_morph_cow(morph);
245 0 : if (!morph)
246 0 : return NULL;
247 :
248 0 : ran_offset = 1 + isl_space_offset(morph->ran->dim, type);
249 :
250 0 : morph->ran = isl_basic_set_remove_dims(morph->ran, type, first, n);
251 :
252 0 : morph->map = isl_mat_drop_rows(morph->map, ran_offset + first, n);
253 :
254 0 : morph->inv = isl_mat_drop_cols(morph->inv, ran_offset + first, n);
255 :
256 0 : if (morph->dom && morph->ran && morph->map && morph->inv)
257 0 : return morph;
258 :
259 0 : isl_morph_free(morph);
260 0 : return NULL;
261 : }
262 :
263 : /* Project domain of morph onto its parameter domain.
264 : */
265 0 : __isl_give isl_morph *isl_morph_dom_params(__isl_take isl_morph *morph)
266 : {
267 : unsigned n;
268 :
269 0 : morph = isl_morph_cow(morph);
270 0 : if (!morph)
271 0 : return NULL;
272 0 : n = isl_basic_set_dim(morph->dom, isl_dim_set);
273 0 : morph = isl_morph_remove_dom_dims(morph, isl_dim_set, 0, n);
274 0 : if (!morph)
275 0 : return NULL;
276 0 : morph->dom = isl_basic_set_params(morph->dom);
277 0 : if (morph->dom)
278 0 : return morph;
279 :
280 0 : isl_morph_free(morph);
281 0 : return NULL;
282 : }
283 :
284 : /* Project range of morph onto its parameter domain.
285 : */
286 0 : __isl_give isl_morph *isl_morph_ran_params(__isl_take isl_morph *morph)
287 : {
288 : unsigned n;
289 :
290 0 : morph = isl_morph_cow(morph);
291 0 : if (!morph)
292 0 : return NULL;
293 0 : n = isl_basic_set_dim(morph->ran, isl_dim_set);
294 0 : morph = isl_morph_remove_ran_dims(morph, isl_dim_set, 0, n);
295 0 : if (!morph)
296 0 : return NULL;
297 0 : morph->ran = isl_basic_set_params(morph->ran);
298 0 : if (morph->ran)
299 0 : return morph;
300 :
301 0 : isl_morph_free(morph);
302 0 : return NULL;
303 : }
304 :
305 0 : void isl_morph_print_internal(__isl_take isl_morph *morph, FILE *out)
306 : {
307 0 : if (!morph)
308 0 : return;
309 :
310 0 : isl_basic_set_dump(morph->dom);
311 0 : isl_basic_set_dump(morph->ran);
312 0 : isl_mat_print_internal(morph->map, out, 4);
313 0 : isl_mat_print_internal(morph->inv, out, 4);
314 : }
315 :
316 0 : void isl_morph_dump(__isl_take isl_morph *morph)
317 : {
318 0 : isl_morph_print_internal(morph, stderr);
319 0 : }
320 :
321 43827237 : __isl_give isl_morph *isl_morph_identity(__isl_keep isl_basic_set *bset)
322 : {
323 : isl_mat *id;
324 : isl_basic_set *universe;
325 : unsigned total;
326 :
327 43827237 : if (!bset)
328 0 : return NULL;
329 :
330 43827237 : total = isl_basic_set_total_dim(bset);
331 43827237 : id = isl_mat_identity(bset->ctx, 1 + total);
332 43827237 : universe = isl_basic_set_universe(isl_space_copy(bset->dim));
333 :
334 43827237 : return isl_morph_alloc(universe, isl_basic_set_copy(universe),
335 : id, isl_mat_copy(id));
336 : }
337 :
338 : /* Create a(n identity) morphism between empty sets of the same dimension
339 : * a "bset".
340 : */
341 0 : __isl_give isl_morph *isl_morph_empty(__isl_keep isl_basic_set *bset)
342 : {
343 : isl_mat *id;
344 : isl_basic_set *empty;
345 : unsigned total;
346 :
347 0 : if (!bset)
348 0 : return NULL;
349 :
350 0 : total = isl_basic_set_total_dim(bset);
351 0 : id = isl_mat_identity(bset->ctx, 1 + total);
352 0 : empty = isl_basic_set_empty(isl_space_copy(bset->dim));
353 :
354 0 : return isl_morph_alloc(empty, isl_basic_set_copy(empty),
355 : id, isl_mat_copy(id));
356 : }
357 :
358 : /* Construct a basic set described by the "n" equalities of "bset" starting
359 : * at "first".
360 : */
361 0 : static __isl_give isl_basic_set *copy_equalities(__isl_keep isl_basic_set *bset,
362 : unsigned first, unsigned n)
363 : {
364 : int i, k;
365 : isl_basic_set *eq;
366 : unsigned total;
367 :
368 0 : isl_assert(bset->ctx, bset->n_div == 0, return NULL);
369 :
370 0 : total = isl_basic_set_total_dim(bset);
371 0 : eq = isl_basic_set_alloc_space(isl_space_copy(bset->dim), 0, n, 0);
372 0 : if (!eq)
373 0 : return NULL;
374 0 : for (i = 0; i < n; ++i) {
375 0 : k = isl_basic_set_alloc_equality(eq);
376 0 : if (k < 0)
377 0 : goto error;
378 0 : isl_seq_cpy(eq->eq[k], bset->eq[first + i], 1 + total);
379 : }
380 :
381 0 : return eq;
382 : error:
383 0 : isl_basic_set_free(eq);
384 0 : return NULL;
385 : }
386 :
387 : /* Given a basic set, exploit the equalities in the basic set to construct
388 : * a morphism that maps the basic set to a lower-dimensional space
389 : * with identifier "id".
390 : * Specifically, the morphism reduces the number of dimensions of type "type".
391 : *
392 : * We first select the equalities of interest, that is those that involve
393 : * variables of type "type" and no later variables.
394 : * Denote those equalities as
395 : *
396 : * -C(p) + M x = 0
397 : *
398 : * where C(p) depends on the parameters if type == isl_dim_set and
399 : * is a constant if type == isl_dim_param.
400 : *
401 : * Use isl_mat_final_variable_compression to construct a compression
402 : *
403 : * x = T x'
404 : *
405 : * x' = Q x
406 : *
407 : * If T is a zero-column matrix, then the set of equality constraints
408 : * do not admit a solution. In this case, an empty morphism is returned.
409 : *
410 : * Both matrices are extended to map the full original space to the full
411 : * compressed space.
412 : */
413 0 : __isl_give isl_morph *isl_basic_set_variable_compression_with_id(
414 : __isl_keep isl_basic_set *bset, enum isl_dim_type type,
415 : __isl_keep isl_id *id)
416 : {
417 : unsigned otype;
418 : unsigned ntype;
419 : unsigned orest;
420 : unsigned nrest;
421 : int f_eq, n_eq;
422 : isl_space *space;
423 : isl_mat *E, *Q, *C;
424 : isl_basic_set *dom, *ran;
425 :
426 0 : if (!bset)
427 0 : return NULL;
428 :
429 0 : if (isl_basic_set_plain_is_empty(bset))
430 0 : return isl_morph_empty(bset);
431 :
432 0 : isl_assert(bset->ctx, bset->n_div == 0, return NULL);
433 :
434 0 : otype = 1 + isl_space_offset(bset->dim, type);
435 0 : ntype = isl_basic_set_dim(bset, type);
436 0 : orest = otype + ntype;
437 0 : nrest = isl_basic_set_total_dim(bset) - (orest - 1);
438 :
439 0 : for (f_eq = 0; f_eq < bset->n_eq; ++f_eq)
440 0 : if (isl_seq_first_non_zero(bset->eq[f_eq] + orest, nrest) == -1)
441 0 : break;
442 0 : for (n_eq = 0; f_eq + n_eq < bset->n_eq; ++n_eq)
443 0 : if (isl_seq_first_non_zero(bset->eq[f_eq + n_eq] + otype, ntype) == -1)
444 0 : break;
445 0 : if (n_eq == 0)
446 0 : return isl_morph_identity(bset);
447 :
448 0 : E = isl_mat_sub_alloc6(bset->ctx, bset->eq, f_eq, n_eq, 0, orest);
449 0 : C = isl_mat_final_variable_compression(E, otype - 1, &Q);
450 0 : if (!Q)
451 0 : C = isl_mat_free(C);
452 0 : if (C && C->n_col == 0) {
453 0 : isl_mat_free(C);
454 0 : isl_mat_free(Q);
455 0 : return isl_morph_empty(bset);
456 : }
457 :
458 0 : Q = isl_mat_diagonal(Q, isl_mat_identity(bset->ctx, nrest));
459 0 : C = isl_mat_diagonal(C, isl_mat_identity(bset->ctx, nrest));
460 :
461 0 : space = isl_space_copy(bset->dim);
462 0 : space = isl_space_drop_dims(space, type, 0, ntype);
463 0 : space = isl_space_add_dims(space, type, ntype - n_eq);
464 0 : space = isl_space_set_tuple_id(space, isl_dim_set, isl_id_copy(id));
465 0 : ran = isl_basic_set_universe(space);
466 0 : dom = copy_equalities(bset, f_eq, n_eq);
467 :
468 0 : return isl_morph_alloc(dom, ran, Q, C);
469 : }
470 :
471 : /* Given a basic set, exploit the equalities in the basic set to construct
472 : * a morphism that maps the basic set to a lower-dimensional space.
473 : * Specifically, the morphism reduces the number of dimensions of type "type".
474 : */
475 0 : __isl_give isl_morph *isl_basic_set_variable_compression(
476 : __isl_keep isl_basic_set *bset, enum isl_dim_type type)
477 : {
478 0 : return isl_basic_set_variable_compression_with_id(bset, type,
479 : &isl_id_none);
480 : }
481 :
482 : /* Construct a parameter compression for "bset".
483 : * We basically just call isl_mat_parameter_compression with the right input
484 : * and then extend the resulting matrix to include the variables.
485 : *
486 : * The implementation assumes that "bset" does not have any equalities
487 : * that only involve the parameters and that isl_basic_set_gauss has
488 : * been applied to "bset".
489 : *
490 : * Let the equalities be given as
491 : *
492 : * B(p) + A x = 0.
493 : *
494 : * We use isl_mat_parameter_compression_ext to compute the compression
495 : *
496 : * p = T p'.
497 : */
498 0 : __isl_give isl_morph *isl_basic_set_parameter_compression(
499 : __isl_keep isl_basic_set *bset)
500 : {
501 : unsigned nparam;
502 : unsigned nvar;
503 : unsigned n_div;
504 : int n_eq;
505 : isl_mat *H, *B;
506 : isl_mat *map, *inv;
507 : isl_basic_set *dom, *ran;
508 :
509 0 : if (!bset)
510 0 : return NULL;
511 :
512 0 : if (isl_basic_set_plain_is_empty(bset))
513 0 : return isl_morph_empty(bset);
514 0 : if (bset->n_eq == 0)
515 0 : return isl_morph_identity(bset);
516 :
517 0 : n_eq = bset->n_eq;
518 0 : nparam = isl_basic_set_dim(bset, isl_dim_param);
519 0 : nvar = isl_basic_set_dim(bset, isl_dim_set);
520 0 : n_div = isl_basic_set_dim(bset, isl_dim_div);
521 :
522 0 : if (isl_seq_first_non_zero(bset->eq[bset->n_eq - 1] + 1 + nparam,
523 : nvar + n_div) == -1)
524 0 : isl_die(isl_basic_set_get_ctx(bset), isl_error_invalid,
525 : "input not allowed to have parameter equalities",
526 : return NULL);
527 0 : if (n_eq > nvar + n_div)
528 0 : isl_die(isl_basic_set_get_ctx(bset), isl_error_invalid,
529 : "input not gaussed", return NULL);
530 :
531 0 : B = isl_mat_sub_alloc6(bset->ctx, bset->eq, 0, n_eq, 0, 1 + nparam);
532 0 : H = isl_mat_sub_alloc6(bset->ctx, bset->eq,
533 : 0, n_eq, 1 + nparam, nvar + n_div);
534 0 : inv = isl_mat_parameter_compression_ext(B, H);
535 0 : inv = isl_mat_diagonal(inv, isl_mat_identity(bset->ctx, nvar));
536 0 : map = isl_mat_right_inverse(isl_mat_copy(inv));
537 :
538 0 : dom = isl_basic_set_universe(isl_space_copy(bset->dim));
539 0 : ran = isl_basic_set_universe(isl_space_copy(bset->dim));
540 :
541 0 : return isl_morph_alloc(dom, ran, map, inv);
542 : }
543 :
544 : /* Add stride constraints to "bset" based on the inverse mapping
545 : * that was plugged in. In particular, if morph maps x' to x,
546 : * the constraints of the original input
547 : *
548 : * A x' + b >= 0
549 : *
550 : * have been rewritten to
551 : *
552 : * A inv x + b >= 0
553 : *
554 : * However, this substitution may loose information on the integrality of x',
555 : * so we need to impose that
556 : *
557 : * inv x
558 : *
559 : * is integral. If inv = B/d, this means that we need to impose that
560 : *
561 : * B x = 0 mod d
562 : *
563 : * or
564 : *
565 : * exists alpha in Z^m: B x = d alpha
566 : *
567 : * This function is similar to add_strides in isl_affine_hull.c
568 : */
569 129106 : static __isl_give isl_basic_set *add_strides(__isl_take isl_basic_set *bset,
570 : __isl_keep isl_morph *morph)
571 : {
572 : int i, div, k;
573 : isl_int gcd;
574 :
575 129106 : if (isl_int_is_one(morph->inv->row[0][0]))
576 129106 : return bset;
577 :
578 0 : isl_int_init(gcd);
579 :
580 0 : for (i = 0; 1 + i < morph->inv->n_row; ++i) {
581 0 : isl_seq_gcd(morph->inv->row[1 + i], morph->inv->n_col, &gcd);
582 0 : if (isl_int_is_divisible_by(gcd, morph->inv->row[0][0]))
583 0 : continue;
584 0 : div = isl_basic_set_alloc_div(bset);
585 0 : if (div < 0)
586 0 : goto error;
587 0 : isl_int_set_si(bset->div[div][0], 0);
588 0 : k = isl_basic_set_alloc_equality(bset);
589 0 : if (k < 0)
590 0 : goto error;
591 0 : isl_seq_cpy(bset->eq[k], morph->inv->row[1 + i],
592 0 : morph->inv->n_col);
593 0 : isl_seq_clr(bset->eq[k] + morph->inv->n_col, bset->n_div);
594 0 : isl_int_set(bset->eq[k][morph->inv->n_col + div],
595 : morph->inv->row[0][0]);
596 : }
597 :
598 0 : isl_int_clear(gcd);
599 :
600 0 : return bset;
601 : error:
602 0 : isl_int_clear(gcd);
603 0 : isl_basic_set_free(bset);
604 0 : return NULL;
605 : }
606 :
607 : /* Apply the morphism to the basic set.
608 : * We basically just compute the preimage of "bset" under the inverse mapping
609 : * in morph, add in stride constraints and intersect with the range
610 : * of the morphism.
611 : */
612 129106 : __isl_give isl_basic_set *isl_morph_basic_set(__isl_take isl_morph *morph,
613 : __isl_take isl_basic_set *bset)
614 : {
615 129106 : isl_basic_set *res = NULL;
616 129106 : isl_mat *mat = NULL;
617 : int i, k;
618 : int max_stride;
619 :
620 129106 : if (!morph || !bset)
621 : goto error;
622 :
623 129106 : isl_assert(bset->ctx, isl_space_is_equal(bset->dim, morph->dom->dim),
624 : goto error);
625 :
626 129106 : max_stride = morph->inv->n_row - 1;
627 129106 : if (isl_int_is_one(morph->inv->row[0][0]))
628 129106 : max_stride = 0;
629 387318 : res = isl_basic_set_alloc_space(isl_space_copy(morph->ran->dim),
630 258212 : bset->n_div + max_stride, bset->n_eq + max_stride, bset->n_ineq);
631 :
632 129106 : for (i = 0; i < bset->n_div; ++i)
633 0 : if (isl_basic_set_alloc_div(res) < 0)
634 0 : goto error;
635 :
636 129106 : mat = isl_mat_sub_alloc6(bset->ctx, bset->eq, 0, bset->n_eq,
637 129106 : 0, morph->inv->n_row);
638 129106 : mat = isl_mat_product(mat, isl_mat_copy(morph->inv));
639 129106 : if (!mat)
640 0 : goto error;
641 129106 : for (i = 0; i < bset->n_eq; ++i) {
642 0 : k = isl_basic_set_alloc_equality(res);
643 0 : if (k < 0)
644 0 : goto error;
645 0 : isl_seq_cpy(res->eq[k], mat->row[i], mat->n_col);
646 0 : isl_seq_scale(res->eq[k] + mat->n_col, bset->eq[i] + mat->n_col,
647 0 : morph->inv->row[0][0], bset->n_div);
648 : }
649 129106 : isl_mat_free(mat);
650 :
651 129106 : mat = isl_mat_sub_alloc6(bset->ctx, bset->ineq, 0, bset->n_ineq,
652 129106 : 0, morph->inv->n_row);
653 129106 : mat = isl_mat_product(mat, isl_mat_copy(morph->inv));
654 129106 : if (!mat)
655 0 : goto error;
656 897584 : for (i = 0; i < bset->n_ineq; ++i) {
657 768478 : k = isl_basic_set_alloc_inequality(res);
658 768478 : if (k < 0)
659 0 : goto error;
660 768478 : isl_seq_cpy(res->ineq[k], mat->row[i], mat->n_col);
661 3073912 : isl_seq_scale(res->ineq[k] + mat->n_col,
662 1536956 : bset->ineq[i] + mat->n_col,
663 768478 : morph->inv->row[0][0], bset->n_div);
664 : }
665 129106 : isl_mat_free(mat);
666 :
667 129106 : mat = isl_mat_sub_alloc6(bset->ctx, bset->div, 0, bset->n_div,
668 129106 : 1, morph->inv->n_row);
669 129106 : mat = isl_mat_product(mat, isl_mat_copy(morph->inv));
670 129106 : if (!mat)
671 0 : goto error;
672 129106 : for (i = 0; i < bset->n_div; ++i) {
673 0 : isl_int_mul(res->div[i][0],
674 : morph->inv->row[0][0], bset->div[i][0]);
675 0 : isl_seq_cpy(res->div[i] + 1, mat->row[i], mat->n_col);
676 0 : isl_seq_scale(res->div[i] + 1 + mat->n_col,
677 0 : bset->div[i] + 1 + mat->n_col,
678 0 : morph->inv->row[0][0], bset->n_div);
679 : }
680 129106 : isl_mat_free(mat);
681 :
682 129106 : res = add_strides(res, morph);
683 :
684 129106 : if (isl_basic_set_is_rational(bset))
685 0 : res = isl_basic_set_set_rational(res);
686 :
687 129106 : res = isl_basic_set_simplify(res);
688 129106 : res = isl_basic_set_finalize(res);
689 :
690 129106 : res = isl_basic_set_intersect(res, isl_basic_set_copy(morph->ran));
691 :
692 129106 : isl_morph_free(morph);
693 129106 : isl_basic_set_free(bset);
694 129106 : return res;
695 : error:
696 0 : isl_mat_free(mat);
697 0 : isl_morph_free(morph);
698 0 : isl_basic_set_free(bset);
699 0 : isl_basic_set_free(res);
700 0 : return NULL;
701 : }
702 :
703 : /* Apply the morphism to the set.
704 : */
705 0 : __isl_give isl_set *isl_morph_set(__isl_take isl_morph *morph,
706 : __isl_take isl_set *set)
707 : {
708 : int i;
709 :
710 0 : if (!morph || !set)
711 : goto error;
712 :
713 0 : isl_assert(set->ctx, isl_space_is_equal(set->dim, morph->dom->dim), goto error);
714 :
715 0 : set = isl_set_cow(set);
716 0 : if (!set)
717 0 : goto error;
718 :
719 0 : isl_space_free(set->dim);
720 0 : set->dim = isl_space_copy(morph->ran->dim);
721 0 : if (!set->dim)
722 0 : goto error;
723 :
724 0 : for (i = 0; i < set->n; ++i) {
725 0 : set->p[i] = isl_morph_basic_set(isl_morph_copy(morph), set->p[i]);
726 0 : if (!set->p[i])
727 0 : goto error;
728 : }
729 :
730 0 : isl_morph_free(morph);
731 :
732 0 : ISL_F_CLR(set, ISL_SET_NORMALIZED);
733 :
734 0 : return set;
735 : error:
736 0 : isl_set_free(set);
737 0 : isl_morph_free(morph);
738 0 : return NULL;
739 : }
740 :
741 : /* Construct a morphism that first does morph2 and then morph1.
742 : */
743 0 : __isl_give isl_morph *isl_morph_compose(__isl_take isl_morph *morph1,
744 : __isl_take isl_morph *morph2)
745 : {
746 : isl_mat *map, *inv;
747 : isl_basic_set *dom, *ran;
748 :
749 0 : if (!morph1 || !morph2)
750 : goto error;
751 :
752 0 : map = isl_mat_product(isl_mat_copy(morph1->map), isl_mat_copy(morph2->map));
753 0 : inv = isl_mat_product(isl_mat_copy(morph2->inv), isl_mat_copy(morph1->inv));
754 0 : dom = isl_morph_basic_set(isl_morph_inverse(isl_morph_copy(morph2)),
755 : isl_basic_set_copy(morph1->dom));
756 0 : dom = isl_basic_set_intersect(dom, isl_basic_set_copy(morph2->dom));
757 0 : ran = isl_morph_basic_set(isl_morph_copy(morph1),
758 : isl_basic_set_copy(morph2->ran));
759 0 : ran = isl_basic_set_intersect(ran, isl_basic_set_copy(morph1->ran));
760 :
761 0 : isl_morph_free(morph1);
762 0 : isl_morph_free(morph2);
763 :
764 0 : return isl_morph_alloc(dom, ran, map, inv);
765 : error:
766 0 : isl_morph_free(morph1);
767 0 : isl_morph_free(morph2);
768 0 : return NULL;
769 : }
770 :
771 92093 : __isl_give isl_morph *isl_morph_inverse(__isl_take isl_morph *morph)
772 : {
773 : isl_basic_set *bset;
774 : isl_mat *mat;
775 :
776 92093 : morph = isl_morph_cow(morph);
777 92093 : if (!morph)
778 0 : return NULL;
779 :
780 92093 : bset = morph->dom;
781 92093 : morph->dom = morph->ran;
782 92093 : morph->ran = bset;
783 :
784 92093 : mat = morph->map;
785 92093 : morph->map = morph->inv;
786 92093 : morph->inv = mat;
787 :
788 92093 : return morph;
789 : }
790 :
791 : /* We detect all the equalities first to avoid implicit equalities
792 : * being discovered during the computations. In particular,
793 : * the compression on the variables could expose additional stride
794 : * constraints on the parameters. This would result in existentially
795 : * quantified variables after applying the resulting morph, which
796 : * in turn could break invariants of the calling functions.
797 : */
798 0 : __isl_give isl_morph *isl_basic_set_full_compression(
799 : __isl_keep isl_basic_set *bset)
800 : {
801 : isl_morph *morph, *morph2;
802 :
803 0 : bset = isl_basic_set_copy(bset);
804 0 : bset = isl_basic_set_detect_equalities(bset);
805 :
806 0 : morph = isl_basic_set_variable_compression(bset, isl_dim_param);
807 0 : bset = isl_morph_basic_set(isl_morph_copy(morph), bset);
808 :
809 0 : morph2 = isl_basic_set_parameter_compression(bset);
810 0 : bset = isl_morph_basic_set(isl_morph_copy(morph2), bset);
811 :
812 0 : morph = isl_morph_compose(morph2, morph);
813 :
814 0 : morph2 = isl_basic_set_variable_compression(bset, isl_dim_set);
815 0 : isl_basic_set_free(bset);
816 :
817 0 : morph = isl_morph_compose(morph2, morph);
818 :
819 0 : return morph;
820 : }
821 :
822 92093 : __isl_give isl_vec *isl_morph_vec(__isl_take isl_morph *morph,
823 : __isl_take isl_vec *vec)
824 : {
825 92093 : if (!morph)
826 0 : goto error;
827 :
828 92093 : vec = isl_mat_vec_product(isl_mat_copy(morph->map), vec);
829 :
830 92093 : isl_morph_free(morph);
831 92093 : return vec;
832 : error:
833 0 : isl_morph_free(morph);
834 0 : isl_vec_free(vec);
835 0 : return NULL;
836 : }
|
