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