File: | polly/lib/External/isl/isl_transitive_closure.c |
Location: | line 1530, column 26 |
Description: | Branch condition evaluates to a garbage value |
1 | /* | |||
2 | * Copyright 2010 INRIA Saclay | |||
3 | * | |||
4 | * Use of this software is governed by the MIT 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_ctx_private.h> | |||
12 | #include <isl_map_private.h> | |||
13 | #include <isl/map.h> | |||
14 | #include <isl_seq.h> | |||
15 | #include <isl_space_private.h> | |||
16 | #include <isl_lp_private.h> | |||
17 | #include <isl/union_map.h> | |||
18 | #include <isl_mat_private.h> | |||
19 | #include <isl_vec_private.h> | |||
20 | #include <isl_options_private.h> | |||
21 | #include <isl_tarjan.h> | |||
22 | ||||
23 | int isl_map_is_transitively_closed(__isl_keep isl_map *map) | |||
24 | { | |||
25 | isl_map *map2; | |||
26 | int closed; | |||
27 | ||||
28 | map2 = isl_map_apply_range(isl_map_copy(map), isl_map_copy(map)); | |||
29 | closed = isl_map_is_subset(map2, map); | |||
30 | isl_map_free(map2); | |||
31 | ||||
32 | return closed; | |||
33 | } | |||
34 | ||||
35 | int isl_union_map_is_transitively_closed(__isl_keep isl_union_map *umap) | |||
36 | { | |||
37 | isl_union_map *umap2; | |||
38 | int closed; | |||
39 | ||||
40 | umap2 = isl_union_map_apply_range(isl_union_map_copy(umap), | |||
41 | isl_union_map_copy(umap)); | |||
42 | closed = isl_union_map_is_subset(umap2, umap); | |||
43 | isl_union_map_free(umap2); | |||
44 | ||||
45 | return closed; | |||
46 | } | |||
47 | ||||
48 | /* Given a map that represents a path with the length of the path | |||
49 | * encoded as the difference between the last output coordindate | |||
50 | * and the last input coordinate, set this length to either | |||
51 | * exactly "length" (if "exactly" is set) or at least "length" | |||
52 | * (if "exactly" is not set). | |||
53 | */ | |||
54 | static __isl_give isl_map *set_path_length(__isl_take isl_map *map, | |||
55 | int exactly, int length) | |||
56 | { | |||
57 | isl_space *dim; | |||
58 | struct isl_basic_map *bmap; | |||
59 | unsigned d; | |||
60 | unsigned nparam; | |||
61 | int k; | |||
62 | isl_int *c; | |||
63 | ||||
64 | if (!map) | |||
65 | return NULL((void*)0); | |||
66 | ||||
67 | dim = isl_map_get_space(map); | |||
68 | d = isl_space_dim(dim, isl_dim_in); | |||
69 | nparam = isl_space_dim(dim, isl_dim_param); | |||
70 | bmap = isl_basic_map_alloc_space(dim, 0, 1, 1); | |||
71 | if (exactly) { | |||
72 | k = isl_basic_map_alloc_equality(bmap); | |||
73 | if (k < 0) | |||
74 | goto error; | |||
75 | c = bmap->eq[k]; | |||
76 | } else { | |||
77 | k = isl_basic_map_alloc_inequality(bmap); | |||
78 | if (k < 0) | |||
79 | goto error; | |||
80 | c = bmap->ineq[k]; | |||
81 | } | |||
82 | isl_seq_clr(c, 1 + isl_basic_map_total_dim(bmap)); | |||
83 | isl_int_set_si(c[0], -length)impz_set_si(c[0],-length); | |||
84 | isl_int_set_si(c[1 + nparam + d - 1], -1)impz_set_si(c[1 + nparam + d - 1],-1); | |||
85 | isl_int_set_si(c[1 + nparam + d + d - 1], 1)impz_set_si(c[1 + nparam + d + d - 1],1); | |||
86 | ||||
87 | bmap = isl_basic_map_finalize(bmap); | |||
88 | map = isl_map_intersect(map, isl_map_from_basic_map(bmap)); | |||
89 | ||||
90 | return map; | |||
91 | error: | |||
92 | isl_basic_map_free(bmap); | |||
93 | isl_map_free(map); | |||
94 | return NULL((void*)0); | |||
95 | } | |||
96 | ||||
97 | /* Check whether the overapproximation of the power of "map" is exactly | |||
98 | * the power of "map". Let R be "map" and A_k the overapproximation. | |||
99 | * The approximation is exact if | |||
100 | * | |||
101 | * A_1 = R | |||
102 | * A_k = A_{k-1} \circ R k >= 2 | |||
103 | * | |||
104 | * Since A_k is known to be an overapproximation, we only need to check | |||
105 | * | |||
106 | * A_1 \subset R | |||
107 | * A_k \subset A_{k-1} \circ R k >= 2 | |||
108 | * | |||
109 | * In practice, "app" has an extra input and output coordinate | |||
110 | * to encode the length of the path. So, we first need to add | |||
111 | * this coordinate to "map" and set the length of the path to | |||
112 | * one. | |||
113 | */ | |||
114 | static int check_power_exactness(__isl_take isl_map *map, | |||
115 | __isl_take isl_map *app) | |||
116 | { | |||
117 | int exact; | |||
118 | isl_map *app_1; | |||
119 | isl_map *app_2; | |||
120 | ||||
121 | map = isl_map_add_dims(map, isl_dim_in, 1); | |||
122 | map = isl_map_add_dims(map, isl_dim_out, 1); | |||
123 | map = set_path_length(map, 1, 1); | |||
124 | ||||
125 | app_1 = set_path_length(isl_map_copy(app), 1, 1); | |||
126 | ||||
127 | exact = isl_map_is_subset(app_1, map); | |||
128 | isl_map_free(app_1); | |||
129 | ||||
130 | if (!exact || exact < 0) { | |||
131 | isl_map_free(app); | |||
132 | isl_map_free(map); | |||
133 | return exact; | |||
134 | } | |||
135 | ||||
136 | app_1 = set_path_length(isl_map_copy(app), 0, 1); | |||
137 | app_2 = set_path_length(app, 0, 2); | |||
138 | app_1 = isl_map_apply_range(map, app_1); | |||
139 | ||||
140 | exact = isl_map_is_subset(app_2, app_1); | |||
141 | ||||
142 | isl_map_free(app_1); | |||
143 | isl_map_free(app_2); | |||
144 | ||||
145 | return exact; | |||
146 | } | |||
147 | ||||
148 | /* Check whether the overapproximation of the power of "map" is exactly | |||
149 | * the power of "map", possibly after projecting out the power (if "project" | |||
150 | * is set). | |||
151 | * | |||
152 | * If "project" is set and if "steps" can only result in acyclic paths, | |||
153 | * then we check | |||
154 | * | |||
155 | * A = R \cup (A \circ R) | |||
156 | * | |||
157 | * where A is the overapproximation with the power projected out, i.e., | |||
158 | * an overapproximation of the transitive closure. | |||
159 | * More specifically, since A is known to be an overapproximation, we check | |||
160 | * | |||
161 | * A \subset R \cup (A \circ R) | |||
162 | * | |||
163 | * Otherwise, we check if the power is exact. | |||
164 | * | |||
165 | * Note that "app" has an extra input and output coordinate to encode | |||
166 | * the length of the part. If we are only interested in the transitive | |||
167 | * closure, then we can simply project out these coordinates first. | |||
168 | */ | |||
169 | static int check_exactness(__isl_take isl_map *map, __isl_take isl_map *app, | |||
170 | int project) | |||
171 | { | |||
172 | isl_map *test; | |||
173 | int exact; | |||
174 | unsigned d; | |||
175 | ||||
176 | if (!project) | |||
177 | return check_power_exactness(map, app); | |||
178 | ||||
179 | d = isl_map_dim(map, isl_dim_in); | |||
180 | app = set_path_length(app, 0, 1); | |||
181 | app = isl_map_project_out(app, isl_dim_in, d, 1); | |||
182 | app = isl_map_project_out(app, isl_dim_out, d, 1); | |||
183 | ||||
184 | app = isl_map_reset_space(app, isl_map_get_space(map)); | |||
185 | ||||
186 | test = isl_map_apply_range(isl_map_copy(map), isl_map_copy(app)); | |||
187 | test = isl_map_union(test, isl_map_copy(map)); | |||
188 | ||||
189 | exact = isl_map_is_subset(app, test); | |||
190 | ||||
191 | isl_map_free(app); | |||
192 | isl_map_free(test); | |||
193 | ||||
194 | isl_map_free(map); | |||
195 | ||||
196 | return exact; | |||
197 | } | |||
198 | ||||
199 | /* | |||
200 | * The transitive closure implementation is based on the paper | |||
201 | * "Computing the Transitive Closure of a Union of Affine Integer | |||
202 | * Tuple Relations" by Anna Beletska, Denis Barthou, Wlodzimierz Bielecki and | |||
203 | * Albert Cohen. | |||
204 | */ | |||
205 | ||||
206 | /* Given a set of n offsets v_i (the rows of "steps"), construct a relation | |||
207 | * of the given dimension specification (Z^{n+1} -> Z^{n+1}) | |||
208 | * that maps an element x to any element that can be reached | |||
209 | * by taking a non-negative number of steps along any of | |||
210 | * the extended offsets v'_i = [v_i 1]. | |||
211 | * That is, construct | |||
212 | * | |||
213 | * { [x] -> [y] : exists k_i >= 0, y = x + \sum_i k_i v'_i } | |||
214 | * | |||
215 | * For any element in this relation, the number of steps taken | |||
216 | * is equal to the difference in the final coordinates. | |||
217 | */ | |||
218 | static __isl_give isl_map *path_along_steps(__isl_take isl_space *dim, | |||
219 | __isl_keep isl_mat *steps) | |||
220 | { | |||
221 | int i, j, k; | |||
222 | struct isl_basic_map *path = NULL((void*)0); | |||
223 | unsigned d; | |||
224 | unsigned n; | |||
225 | unsigned nparam; | |||
226 | ||||
227 | if (!dim || !steps) | |||
228 | goto error; | |||
229 | ||||
230 | d = isl_space_dim(dim, isl_dim_in); | |||
231 | n = steps->n_row; | |||
232 | nparam = isl_space_dim(dim, isl_dim_param); | |||
233 | ||||
234 | path = isl_basic_map_alloc_space(isl_space_copy(dim), n, d, n); | |||
235 | ||||
236 | for (i = 0; i < n; ++i) { | |||
237 | k = isl_basic_map_alloc_div(path); | |||
238 | if (k < 0) | |||
239 | goto error; | |||
240 | isl_assert(steps->ctx, i == k, goto error)do { if (i == k) break; do { isl_handle_error(steps->ctx, isl_error_unknown , "Assertion \"" "i == k" "\" failed", "/tmp/buildd/llvm-toolchain-snapshot-3.7~svn239931/polly/lib/External/isl/isl_transitive_closure.c" , 240); goto error; } while (0); } while (0); | |||
241 | isl_int_set_si(path->div[k][0], 0)impz_set_si(path->div[k][0],0); | |||
242 | } | |||
243 | ||||
244 | for (i = 0; i < d; ++i) { | |||
245 | k = isl_basic_map_alloc_equality(path); | |||
246 | if (k < 0) | |||
247 | goto error; | |||
248 | isl_seq_clr(path->eq[k], 1 + isl_basic_map_total_dim(path)); | |||
249 | isl_int_set_si(path->eq[k][1 + nparam + i], 1)impz_set_si(path->eq[k][1 + nparam + i],1); | |||
250 | isl_int_set_si(path->eq[k][1 + nparam + d + i], -1)impz_set_si(path->eq[k][1 + nparam + d + i],-1); | |||
251 | if (i == d - 1) | |||
252 | for (j = 0; j < n; ++j) | |||
253 | isl_int_set_si(path->eq[k][1 + nparam + 2 * d + j], 1)impz_set_si(path->eq[k][1 + nparam + 2 * d + j],1); | |||
254 | else | |||
255 | for (j = 0; j < n; ++j) | |||
256 | isl_int_set(path->eq[k][1 + nparam + 2 * d + j],impz_set(path->eq[k][1 + nparam + 2 * d + j],steps->row [j][i]) | |||
257 | steps->row[j][i])impz_set(path->eq[k][1 + nparam + 2 * d + j],steps->row [j][i]); | |||
258 | } | |||
259 | ||||
260 | for (i = 0; i < n; ++i) { | |||
261 | k = isl_basic_map_alloc_inequality(path); | |||
262 | if (k < 0) | |||
263 | goto error; | |||
264 | isl_seq_clr(path->ineq[k], 1 + isl_basic_map_total_dim(path)); | |||
265 | isl_int_set_si(path->ineq[k][1 + nparam + 2 * d + i], 1)impz_set_si(path->ineq[k][1 + nparam + 2 * d + i],1); | |||
266 | } | |||
267 | ||||
268 | isl_space_free(dim); | |||
269 | ||||
270 | path = isl_basic_map_simplify(path); | |||
271 | path = isl_basic_map_finalize(path); | |||
272 | return isl_map_from_basic_map(path); | |||
273 | error: | |||
274 | isl_space_free(dim); | |||
275 | isl_basic_map_free(path); | |||
276 | return NULL((void*)0); | |||
277 | } | |||
278 | ||||
279 | #define IMPURE0 0 | |||
280 | #define PURE_PARAM1 1 | |||
281 | #define PURE_VAR2 2 | |||
282 | #define MIXED3 3 | |||
283 | ||||
284 | /* Check whether the parametric constant term of constraint c is never | |||
285 | * positive in "bset". | |||
286 | */ | |||
287 | static int parametric_constant_never_positive(__isl_keep isl_basic_setisl_basic_map *bset, | |||
288 | isl_int *c, int *div_purity) | |||
289 | { | |||
290 | unsigned d; | |||
291 | unsigned n_div; | |||
292 | unsigned nparam; | |||
293 | int i; | |||
294 | int k; | |||
295 | int empty; | |||
296 | ||||
297 | n_div = isl_basic_set_dim(bset, isl_dim_div); | |||
298 | d = isl_basic_set_dim(bset, isl_dim_set); | |||
299 | nparam = isl_basic_set_dim(bset, isl_dim_param); | |||
300 | ||||
301 | bset = isl_basic_set_copy(bset); | |||
302 | bset = isl_basic_set_cow(bset); | |||
303 | bset = isl_basic_set_extend_constraints(bset, 0, 1); | |||
304 | k = isl_basic_set_alloc_inequality(bset); | |||
305 | if (k < 0) | |||
306 | goto error; | |||
307 | isl_seq_clr(bset->ineq[k], 1 + isl_basic_set_total_dim(bset)); | |||
308 | isl_seq_cpy(bset->ineq[k], c, 1 + nparam); | |||
309 | for (i = 0; i < n_div; ++i) { | |||
310 | if (div_purity[i] != PURE_PARAM1) | |||
311 | continue; | |||
312 | isl_int_set(bset->ineq[k][1 + nparam + d + i],impz_set(bset->ineq[k][1 + nparam + d + i],c[1 + nparam + d + i]) | |||
313 | c[1 + nparam + d + i])impz_set(bset->ineq[k][1 + nparam + d + i],c[1 + nparam + d + i]); | |||
314 | } | |||
315 | isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1)impz_sub_ui(bset->ineq[k][0],bset->ineq[k][0],1); | |||
316 | empty = isl_basic_set_is_empty(bset); | |||
317 | isl_basic_set_free(bset); | |||
318 | ||||
319 | return empty; | |||
320 | error: | |||
321 | isl_basic_set_free(bset); | |||
322 | return -1; | |||
323 | } | |||
324 | ||||
325 | /* Return PURE_PARAM if only the coefficients of the parameters are non-zero. | |||
326 | * Return PURE_VAR if only the coefficients of the set variables are non-zero. | |||
327 | * Return MIXED if only the coefficients of the parameters and the set | |||
328 | * variables are non-zero and if moreover the parametric constant | |||
329 | * can never attain positive values. | |||
330 | * Return IMPURE otherwise. | |||
331 | */ | |||
332 | static int purity(__isl_keep isl_basic_setisl_basic_map *bset, isl_int *c, int *div_purity, | |||
333 | int eq) | |||
334 | { | |||
335 | unsigned d; | |||
336 | unsigned n_div; | |||
337 | unsigned nparam; | |||
338 | int empty; | |||
339 | int i; | |||
340 | int p = 0, v = 0; | |||
341 | ||||
342 | n_div = isl_basic_set_dim(bset, isl_dim_div); | |||
343 | d = isl_basic_set_dim(bset, isl_dim_set); | |||
344 | nparam = isl_basic_set_dim(bset, isl_dim_param); | |||
345 | ||||
346 | for (i = 0; i < n_div; ++i) { | |||
347 | if (isl_int_is_zero(c[1 + nparam + d + i])(impz_sgn(c[1 + nparam + d + i]) == 0)) | |||
348 | continue; | |||
349 | switch (div_purity[i]) { | |||
350 | case PURE_PARAM1: p = 1; break; | |||
351 | case PURE_VAR2: v = 1; break; | |||
352 | default: return IMPURE0; | |||
353 | } | |||
354 | } | |||
355 | if (!p && isl_seq_first_non_zero(c + 1, nparam) == -1) | |||
356 | return PURE_VAR2; | |||
357 | if (!v && isl_seq_first_non_zero(c + 1 + nparam, d) == -1) | |||
358 | return PURE_PARAM1; | |||
359 | ||||
360 | empty = parametric_constant_never_positive(bset, c, div_purity); | |||
361 | if (eq && empty >= 0 && !empty) { | |||
362 | isl_seq_neg(c, c, 1 + nparam + d + n_div); | |||
363 | empty = parametric_constant_never_positive(bset, c, div_purity); | |||
364 | } | |||
365 | ||||
366 | return empty < 0 ? -1 : empty ? MIXED3 : IMPURE0; | |||
367 | } | |||
368 | ||||
369 | /* Return an array of integers indicating the type of each div in bset. | |||
370 | * If the div is (recursively) defined in terms of only the parameters, | |||
371 | * then the type is PURE_PARAM. | |||
372 | * If the div is (recursively) defined in terms of only the set variables, | |||
373 | * then the type is PURE_VAR. | |||
374 | * Otherwise, the type is IMPURE. | |||
375 | */ | |||
376 | static __isl_give int *get_div_purity(__isl_keep isl_basic_setisl_basic_map *bset) | |||
377 | { | |||
378 | int i, j; | |||
379 | int *div_purity; | |||
380 | unsigned d; | |||
381 | unsigned n_div; | |||
382 | unsigned nparam; | |||
383 | ||||
384 | if (!bset) | |||
385 | return NULL((void*)0); | |||
386 | ||||
387 | n_div = isl_basic_set_dim(bset, isl_dim_div); | |||
388 | d = isl_basic_set_dim(bset, isl_dim_set); | |||
389 | nparam = isl_basic_set_dim(bset, isl_dim_param); | |||
390 | ||||
391 | div_purity = isl_alloc_array(bset->ctx, int, n_div)((int *)isl_malloc_or_die(bset->ctx, (n_div)*sizeof(int))); | |||
392 | if (n_div && !div_purity) | |||
393 | return NULL((void*)0); | |||
394 | ||||
395 | for (i = 0; i < bset->n_div; ++i) { | |||
396 | int p = 0, v = 0; | |||
397 | if (isl_int_is_zero(bset->div[i][0])(impz_sgn(bset->div[i][0]) == 0)) { | |||
398 | div_purity[i] = IMPURE0; | |||
399 | continue; | |||
400 | } | |||
401 | if (isl_seq_first_non_zero(bset->div[i] + 2, nparam) != -1) | |||
402 | p = 1; | |||
403 | if (isl_seq_first_non_zero(bset->div[i] + 2 + nparam, d) != -1) | |||
404 | v = 1; | |||
405 | for (j = 0; j < i; ++j) { | |||
406 | if (isl_int_is_zero(bset->div[i][2 + nparam + d + j])(impz_sgn(bset->div[i][2 + nparam + d + j]) == 0)) | |||
407 | continue; | |||
408 | switch (div_purity[j]) { | |||
409 | case PURE_PARAM1: p = 1; break; | |||
410 | case PURE_VAR2: v = 1; break; | |||
411 | default: p = v = 1; break; | |||
412 | } | |||
413 | } | |||
414 | div_purity[i] = v ? p ? IMPURE0 : PURE_VAR2 : PURE_PARAM1; | |||
415 | } | |||
416 | ||||
417 | return div_purity; | |||
418 | } | |||
419 | ||||
420 | /* Given a path with the as yet unconstrained length at position "pos", | |||
421 | * check if setting the length to zero results in only the identity | |||
422 | * mapping. | |||
423 | */ | |||
424 | static int empty_path_is_identity(__isl_keep isl_basic_map *path, unsigned pos) | |||
425 | { | |||
426 | isl_basic_map *test = NULL((void*)0); | |||
427 | isl_basic_map *id = NULL((void*)0); | |||
428 | int k; | |||
429 | int is_id; | |||
430 | ||||
431 | test = isl_basic_map_copy(path); | |||
432 | test = isl_basic_map_extend_constraints(test, 1, 0); | |||
433 | k = isl_basic_map_alloc_equality(test); | |||
434 | if (k < 0) | |||
435 | goto error; | |||
436 | isl_seq_clr(test->eq[k], 1 + isl_basic_map_total_dim(test)); | |||
437 | isl_int_set_si(test->eq[k][pos], 1)impz_set_si(test->eq[k][pos],1); | |||
438 | id = isl_basic_map_identity(isl_basic_map_get_space(path)); | |||
439 | is_id = isl_basic_map_is_equal(test, id); | |||
440 | isl_basic_map_free(test); | |||
441 | isl_basic_map_free(id); | |||
442 | return is_id; | |||
443 | error: | |||
444 | isl_basic_map_free(test); | |||
445 | return -1; | |||
446 | } | |||
447 | ||||
448 | /* If any of the constraints is found to be impure then this function | |||
449 | * sets *impurity to 1. | |||
450 | * | |||
451 | * If impurity is NULL then we are dealing with a non-parametric set | |||
452 | * and so the constraints are obviously PURE_VAR. | |||
453 | */ | |||
454 | static __isl_give isl_basic_map *add_delta_constraints( | |||
455 | __isl_take isl_basic_map *path, | |||
456 | __isl_keep isl_basic_setisl_basic_map *delta, unsigned off, unsigned nparam, | |||
457 | unsigned d, int *div_purity, int eq, int *impurity) | |||
458 | { | |||
459 | int i, k; | |||
460 | int n = eq ? delta->n_eq : delta->n_ineq; | |||
461 | isl_int **delta_c = eq ? delta->eq : delta->ineq; | |||
462 | unsigned n_div; | |||
463 | ||||
464 | n_div = isl_basic_set_dim(delta, isl_dim_div); | |||
465 | ||||
466 | for (i = 0; i < n; ++i) { | |||
467 | isl_int *path_c; | |||
468 | int p = PURE_VAR2; | |||
469 | if (impurity) | |||
470 | p = purity(delta, delta_c[i], div_purity, eq); | |||
471 | if (p < 0) | |||
472 | goto error; | |||
473 | if (p != PURE_VAR2 && p != PURE_PARAM1 && !*impurity) | |||
474 | *impurity = 1; | |||
475 | if (p == IMPURE0) | |||
476 | continue; | |||
477 | if (eq && p != MIXED3) { | |||
478 | k = isl_basic_map_alloc_equality(path); | |||
479 | if (k < 0) | |||
480 | goto error; | |||
481 | path_c = path->eq[k]; | |||
482 | } else { | |||
483 | k = isl_basic_map_alloc_inequality(path); | |||
484 | if (k < 0) | |||
485 | goto error; | |||
486 | path_c = path->ineq[k]; | |||
487 | } | |||
488 | isl_seq_clr(path_c, 1 + isl_basic_map_total_dim(path)); | |||
489 | if (p == PURE_VAR2) { | |||
490 | isl_seq_cpy(path_c + off, | |||
491 | delta_c[i] + 1 + nparam, d); | |||
492 | isl_int_set(path_c[off + d], delta_c[i][0])impz_set(path_c[off + d],delta_c[i][0]); | |||
493 | } else if (p == PURE_PARAM1) { | |||
494 | isl_seq_cpy(path_c, delta_c[i], 1 + nparam); | |||
495 | } else { | |||
496 | isl_seq_cpy(path_c + off, | |||
497 | delta_c[i] + 1 + nparam, d); | |||
498 | isl_seq_cpy(path_c, delta_c[i], 1 + nparam); | |||
499 | } | |||
500 | isl_seq_cpy(path_c + off - n_div, | |||
501 | delta_c[i] + 1 + nparam + d, n_div); | |||
502 | } | |||
503 | ||||
504 | return path; | |||
505 | error: | |||
506 | isl_basic_map_free(path); | |||
507 | return NULL((void*)0); | |||
508 | } | |||
509 | ||||
510 | /* Given a set of offsets "delta", construct a relation of the | |||
511 | * given dimension specification (Z^{n+1} -> Z^{n+1}) that | |||
512 | * is an overapproximation of the relations that | |||
513 | * maps an element x to any element that can be reached | |||
514 | * by taking a non-negative number of steps along any of | |||
515 | * the elements in "delta". | |||
516 | * That is, construct an approximation of | |||
517 | * | |||
518 | * { [x] -> [y] : exists f \in \delta, k \in Z : | |||
519 | * y = x + k [f, 1] and k >= 0 } | |||
520 | * | |||
521 | * For any element in this relation, the number of steps taken | |||
522 | * is equal to the difference in the final coordinates. | |||
523 | * | |||
524 | * In particular, let delta be defined as | |||
525 | * | |||
526 | * \delta = [p] -> { [x] : A x + a >= 0 and B p + b >= 0 and | |||
527 | * C x + C'p + c >= 0 and | |||
528 | * D x + D'p + d >= 0 } | |||
529 | * | |||
530 | * where the constraints C x + C'p + c >= 0 are such that the parametric | |||
531 | * constant term of each constraint j, "C_j x + C'_j p + c_j", | |||
532 | * can never attain positive values, then the relation is constructed as | |||
533 | * | |||
534 | * { [x] -> [y] : exists [f, k] \in Z^{n+1} : y = x + f and | |||
535 | * A f + k a >= 0 and B p + b >= 0 and | |||
536 | * C f + C'p + c >= 0 and k >= 1 } | |||
537 | * union { [x] -> [x] } | |||
538 | * | |||
539 | * If the zero-length paths happen to correspond exactly to the identity | |||
540 | * mapping, then we return | |||
541 | * | |||
542 | * { [x] -> [y] : exists [f, k] \in Z^{n+1} : y = x + f and | |||
543 | * A f + k a >= 0 and B p + b >= 0 and | |||
544 | * C f + C'p + c >= 0 and k >= 0 } | |||
545 | * | |||
546 | * instead. | |||
547 | * | |||
548 | * Existentially quantified variables in \delta are handled by | |||
549 | * classifying them as independent of the parameters, purely | |||
550 | * parameter dependent and others. Constraints containing | |||
551 | * any of the other existentially quantified variables are removed. | |||
552 | * This is safe, but leads to an additional overapproximation. | |||
553 | * | |||
554 | * If there are any impure constraints, then we also eliminate | |||
555 | * the parameters from \delta, resulting in a set | |||
556 | * | |||
557 | * \delta' = { [x] : E x + e >= 0 } | |||
558 | * | |||
559 | * and add the constraints | |||
560 | * | |||
561 | * E f + k e >= 0 | |||
562 | * | |||
563 | * to the constructed relation. | |||
564 | */ | |||
565 | static __isl_give isl_map *path_along_delta(__isl_take isl_space *dim, | |||
566 | __isl_take isl_basic_setisl_basic_map *delta) | |||
567 | { | |||
568 | isl_basic_map *path = NULL((void*)0); | |||
569 | unsigned d; | |||
570 | unsigned n_div; | |||
571 | unsigned nparam; | |||
572 | unsigned off; | |||
573 | int i, k; | |||
574 | int is_id; | |||
575 | int *div_purity = NULL((void*)0); | |||
576 | int impurity = 0; | |||
577 | ||||
578 | if (!delta) | |||
579 | goto error; | |||
580 | n_div = isl_basic_set_dim(delta, isl_dim_div); | |||
581 | d = isl_basic_set_dim(delta, isl_dim_set); | |||
582 | nparam = isl_basic_set_dim(delta, isl_dim_param); | |||
583 | path = isl_basic_map_alloc_space(isl_space_copy(dim), n_div + d + 1, | |||
584 | d + 1 + delta->n_eq, delta->n_eq + delta->n_ineq + 1); | |||
585 | off = 1 + nparam + 2 * (d + 1) + n_div; | |||
586 | ||||
587 | for (i = 0; i < n_div + d + 1; ++i) { | |||
588 | k = isl_basic_map_alloc_div(path); | |||
589 | if (k < 0) | |||
590 | goto error; | |||
591 | isl_int_set_si(path->div[k][0], 0)impz_set_si(path->div[k][0],0); | |||
592 | } | |||
593 | ||||
594 | for (i = 0; i < d + 1; ++i) { | |||
595 | k = isl_basic_map_alloc_equality(path); | |||
596 | if (k < 0) | |||
597 | goto error; | |||
598 | isl_seq_clr(path->eq[k], 1 + isl_basic_map_total_dim(path)); | |||
599 | isl_int_set_si(path->eq[k][1 + nparam + i], 1)impz_set_si(path->eq[k][1 + nparam + i],1); | |||
600 | isl_int_set_si(path->eq[k][1 + nparam + d + 1 + i], -1)impz_set_si(path->eq[k][1 + nparam + d + 1 + i],-1); | |||
601 | isl_int_set_si(path->eq[k][off + i], 1)impz_set_si(path->eq[k][off + i],1); | |||
602 | } | |||
603 | ||||
604 | div_purity = get_div_purity(delta); | |||
605 | if (n_div && !div_purity) | |||
606 | goto error; | |||
607 | ||||
608 | path = add_delta_constraints(path, delta, off, nparam, d, | |||
609 | div_purity, 1, &impurity); | |||
610 | path = add_delta_constraints(path, delta, off, nparam, d, | |||
611 | div_purity, 0, &impurity); | |||
612 | if (impurity) { | |||
613 | isl_space *dim = isl_basic_set_get_space(delta); | |||
614 | delta = isl_basic_set_project_out(delta, | |||
615 | isl_dim_param, 0, nparam); | |||
616 | delta = isl_basic_set_add_dims(delta, isl_dim_param, nparam); | |||
617 | delta = isl_basic_set_reset_space(delta, dim); | |||
618 | if (!delta) | |||
619 | goto error; | |||
620 | path = isl_basic_map_extend_constraints(path, delta->n_eq, | |||
621 | delta->n_ineq + 1); | |||
622 | path = add_delta_constraints(path, delta, off, nparam, d, | |||
623 | NULL((void*)0), 1, NULL((void*)0)); | |||
624 | path = add_delta_constraints(path, delta, off, nparam, d, | |||
625 | NULL((void*)0), 0, NULL((void*)0)); | |||
626 | path = isl_basic_map_gauss(path, NULL((void*)0)); | |||
627 | } | |||
628 | ||||
629 | is_id = empty_path_is_identity(path, off + d); | |||
630 | if (is_id < 0) | |||
631 | goto error; | |||
632 | ||||
633 | k = isl_basic_map_alloc_inequality(path); | |||
634 | if (k < 0) | |||
635 | goto error; | |||
636 | isl_seq_clr(path->ineq[k], 1 + isl_basic_map_total_dim(path)); | |||
637 | if (!is_id) | |||
638 | isl_int_set_si(path->ineq[k][0], -1)impz_set_si(path->ineq[k][0],-1); | |||
639 | isl_int_set_si(path->ineq[k][off + d], 1)impz_set_si(path->ineq[k][off + d],1); | |||
640 | ||||
641 | free(div_purity); | |||
642 | isl_basic_set_free(delta); | |||
643 | path = isl_basic_map_finalize(path); | |||
644 | if (is_id) { | |||
645 | isl_space_free(dim); | |||
646 | return isl_map_from_basic_map(path); | |||
647 | } | |||
648 | return isl_basic_map_union(path, isl_basic_map_identity(dim)); | |||
649 | error: | |||
650 | free(div_purity); | |||
651 | isl_space_free(dim); | |||
652 | isl_basic_set_free(delta); | |||
653 | isl_basic_map_free(path); | |||
654 | return NULL((void*)0); | |||
655 | } | |||
656 | ||||
657 | /* Given a dimension specification Z^{n+1} -> Z^{n+1} and a parameter "param", | |||
658 | * construct a map that equates the parameter to the difference | |||
659 | * in the final coordinates and imposes that this difference is positive. | |||
660 | * That is, construct | |||
661 | * | |||
662 | * { [x,x_s] -> [y,y_s] : k = y_s - x_s > 0 } | |||
663 | */ | |||
664 | static __isl_give isl_map *equate_parameter_to_length(__isl_take isl_space *dim, | |||
665 | unsigned param) | |||
666 | { | |||
667 | struct isl_basic_map *bmap; | |||
668 | unsigned d; | |||
669 | unsigned nparam; | |||
670 | int k; | |||
671 | ||||
672 | d = isl_space_dim(dim, isl_dim_in); | |||
673 | nparam = isl_space_dim(dim, isl_dim_param); | |||
674 | bmap = isl_basic_map_alloc_space(dim, 0, 1, 1); | |||
675 | k = isl_basic_map_alloc_equality(bmap); | |||
676 | if (k < 0) | |||
677 | goto error; | |||
678 | isl_seq_clr(bmap->eq[k], 1 + isl_basic_map_total_dim(bmap)); | |||
679 | isl_int_set_si(bmap->eq[k][1 + param], -1)impz_set_si(bmap->eq[k][1 + param],-1); | |||
680 | isl_int_set_si(bmap->eq[k][1 + nparam + d - 1], -1)impz_set_si(bmap->eq[k][1 + nparam + d - 1],-1); | |||
681 | isl_int_set_si(bmap->eq[k][1 + nparam + d + d - 1], 1)impz_set_si(bmap->eq[k][1 + nparam + d + d - 1],1); | |||
682 | ||||
683 | k = isl_basic_map_alloc_inequality(bmap); | |||
684 | if (k < 0) | |||
685 | goto error; | |||
686 | isl_seq_clr(bmap->ineq[k], 1 + isl_basic_map_total_dim(bmap)); | |||
687 | isl_int_set_si(bmap->ineq[k][1 + param], 1)impz_set_si(bmap->ineq[k][1 + param],1); | |||
688 | isl_int_set_si(bmap->ineq[k][0], -1)impz_set_si(bmap->ineq[k][0],-1); | |||
689 | ||||
690 | bmap = isl_basic_map_finalize(bmap); | |||
691 | return isl_map_from_basic_map(bmap); | |||
692 | error: | |||
693 | isl_basic_map_free(bmap); | |||
694 | return NULL((void*)0); | |||
695 | } | |||
696 | ||||
697 | /* Check whether "path" is acyclic, where the last coordinates of domain | |||
698 | * and range of path encode the number of steps taken. | |||
699 | * That is, check whether | |||
700 | * | |||
701 | * { d | d = y - x and (x,y) in path } | |||
702 | * | |||
703 | * does not contain any element with positive last coordinate (positive length) | |||
704 | * and zero remaining coordinates (cycle). | |||
705 | */ | |||
706 | static int is_acyclic(__isl_take isl_map *path) | |||
707 | { | |||
708 | int i; | |||
709 | int acyclic; | |||
710 | unsigned dim; | |||
711 | struct isl_setisl_map *delta; | |||
712 | ||||
713 | delta = isl_map_deltas(path); | |||
714 | dim = isl_set_dim(delta, isl_dim_set); | |||
715 | for (i = 0; i < dim; ++i) { | |||
716 | if (i == dim -1) | |||
717 | delta = isl_set_lower_bound_si(delta, isl_dim_set, i, 1); | |||
718 | else | |||
719 | delta = isl_set_fix_si(delta, isl_dim_set, i, 0); | |||
720 | } | |||
721 | ||||
722 | acyclic = isl_set_is_empty(delta); | |||
723 | isl_set_free(delta); | |||
724 | ||||
725 | return acyclic; | |||
726 | } | |||
727 | ||||
728 | /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D | |||
729 | * and a dimension specification (Z^{n+1} -> Z^{n+1}), | |||
730 | * construct a map that is an overapproximation of the map | |||
731 | * that takes an element from the space D \times Z to another | |||
732 | * element from the same space, such that the first n coordinates of the | |||
733 | * difference between them is a sum of differences between images | |||
734 | * and pre-images in one of the R_i and such that the last coordinate | |||
735 | * is equal to the number of steps taken. | |||
736 | * That is, let | |||
737 | * | |||
738 | * \Delta_i = { y - x | (x, y) in R_i } | |||
739 | * | |||
740 | * then the constructed map is an overapproximation of | |||
741 | * | |||
742 | * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : | |||
743 | * d = (\sum_i k_i \delta_i, \sum_i k_i) } | |||
744 | * | |||
745 | * The elements of the singleton \Delta_i's are collected as the | |||
746 | * rows of the steps matrix. For all these \Delta_i's together, | |||
747 | * a single path is constructed. | |||
748 | * For each of the other \Delta_i's, we compute an overapproximation | |||
749 | * of the paths along elements of \Delta_i. | |||
750 | * Since each of these paths performs an addition, composition is | |||
751 | * symmetric and we can simply compose all resulting paths in any order. | |||
752 | */ | |||
753 | static __isl_give isl_map *construct_extended_path(__isl_take isl_space *dim, | |||
754 | __isl_keep isl_map *map, int *project) | |||
755 | { | |||
756 | struct isl_mat *steps = NULL((void*)0); | |||
757 | struct isl_map *path = NULL((void*)0); | |||
758 | unsigned d; | |||
759 | int i, j, n; | |||
760 | ||||
761 | if (!map) | |||
762 | goto error; | |||
763 | ||||
764 | d = isl_map_dim(map, isl_dim_in); | |||
765 | ||||
766 | path = isl_map_identity(isl_space_copy(dim)); | |||
767 | ||||
768 | steps = isl_mat_alloc(map->ctx, map->n, d); | |||
769 | if (!steps) | |||
770 | goto error; | |||
771 | ||||
772 | n = 0; | |||
773 | for (i = 0; i < map->n; ++i) { | |||
774 | struct isl_basic_setisl_basic_map *delta; | |||
775 | ||||
776 | delta = isl_basic_map_deltas(isl_basic_map_copy(map->p[i])); | |||
777 | ||||
778 | for (j = 0; j < d; ++j) { | |||
779 | int fixed; | |||
780 | ||||
781 | fixed = isl_basic_set_plain_dim_is_fixed(delta, j, | |||
782 | &steps->row[n][j]); | |||
783 | if (fixed < 0) { | |||
784 | isl_basic_set_free(delta); | |||
785 | goto error; | |||
786 | } | |||
787 | if (!fixed) | |||
788 | break; | |||
789 | } | |||
790 | ||||
791 | ||||
792 | if (j < d) { | |||
793 | path = isl_map_apply_range(path, | |||
794 | path_along_delta(isl_space_copy(dim), delta)); | |||
795 | path = isl_map_coalesce(path); | |||
796 | } else { | |||
797 | isl_basic_set_free(delta); | |||
798 | ++n; | |||
799 | } | |||
800 | } | |||
801 | ||||
802 | if (n > 0) { | |||
803 | steps->n_row = n; | |||
804 | path = isl_map_apply_range(path, | |||
805 | path_along_steps(isl_space_copy(dim), steps)); | |||
806 | } | |||
807 | ||||
808 | if (project && *project) { | |||
809 | *project = is_acyclic(isl_map_copy(path)); | |||
810 | if (*project < 0) | |||
811 | goto error; | |||
812 | } | |||
813 | ||||
814 | isl_space_free(dim); | |||
815 | isl_mat_free(steps); | |||
816 | return path; | |||
817 | error: | |||
818 | isl_space_free(dim); | |||
819 | isl_mat_free(steps); | |||
820 | isl_map_free(path); | |||
821 | return NULL((void*)0); | |||
822 | } | |||
823 | ||||
824 | static int isl_set_overlaps(__isl_keep isl_setisl_map *set1, __isl_keep isl_setisl_map *set2) | |||
825 | { | |||
826 | isl_setisl_map *i; | |||
827 | int no_overlap; | |||
828 | ||||
829 | if (!set1 || !set2) | |||
830 | return -1; | |||
831 | ||||
832 | if (!isl_space_tuple_is_equal(set1->dim, isl_dim_set, | |||
833 | set2->dim, isl_dim_set)) | |||
834 | return 0; | |||
835 | ||||
836 | i = isl_set_intersect(isl_set_copy(set1), isl_set_copy(set2)); | |||
837 | no_overlap = isl_set_is_empty(i); | |||
838 | isl_set_free(i); | |||
839 | ||||
840 | return no_overlap < 0 ? -1 : !no_overlap; | |||
841 | } | |||
842 | ||||
843 | /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D | |||
844 | * and a dimension specification (Z^{n+1} -> Z^{n+1}), | |||
845 | * construct a map that is an overapproximation of the map | |||
846 | * that takes an element from the dom R \times Z to an | |||
847 | * element from ran R \times Z, such that the first n coordinates of the | |||
848 | * difference between them is a sum of differences between images | |||
849 | * and pre-images in one of the R_i and such that the last coordinate | |||
850 | * is equal to the number of steps taken. | |||
851 | * That is, let | |||
852 | * | |||
853 | * \Delta_i = { y - x | (x, y) in R_i } | |||
854 | * | |||
855 | * then the constructed map is an overapproximation of | |||
856 | * | |||
857 | * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : | |||
858 | * d = (\sum_i k_i \delta_i, \sum_i k_i) and | |||
859 | * x in dom R and x + d in ran R and | |||
860 | * \sum_i k_i >= 1 } | |||
861 | */ | |||
862 | static __isl_give isl_map *construct_component(__isl_take isl_space *dim, | |||
863 | __isl_keep isl_map *map, int *exact, int project) | |||
864 | { | |||
865 | struct isl_setisl_map *domain = NULL((void*)0); | |||
866 | struct isl_setisl_map *range = NULL((void*)0); | |||
867 | struct isl_map *app = NULL((void*)0); | |||
868 | struct isl_map *path = NULL((void*)0); | |||
869 | int overlaps; | |||
870 | ||||
871 | domain = isl_map_domain(isl_map_copy(map)); | |||
872 | domain = isl_set_coalesce(domain); | |||
873 | range = isl_map_range(isl_map_copy(map)); | |||
874 | range = isl_set_coalesce(range); | |||
875 | overlaps = isl_set_overlaps(domain, range); | |||
876 | if (overlaps < 0 || !overlaps) { | |||
877 | isl_set_free(domain); | |||
878 | isl_set_free(range); | |||
879 | isl_space_free(dim); | |||
880 | ||||
881 | if (overlaps < 0) | |||
882 | map = NULL((void*)0); | |||
883 | map = isl_map_copy(map); | |||
884 | map = isl_map_add_dims(map, isl_dim_in, 1); | |||
885 | map = isl_map_add_dims(map, isl_dim_out, 1); | |||
886 | map = set_path_length(map, 1, 1); | |||
887 | return map; | |||
888 | } | |||
889 | app = isl_map_from_domain_and_range(domain, range); | |||
890 | app = isl_map_add_dims(app, isl_dim_in, 1); | |||
891 | app = isl_map_add_dims(app, isl_dim_out, 1); | |||
892 | ||||
893 | path = construct_extended_path(isl_space_copy(dim), map, | |||
894 | exact && *exact ? &project : NULL((void*)0)); | |||
895 | app = isl_map_intersect(app, path); | |||
896 | ||||
897 | if (exact && *exact && | |||
898 | (*exact = check_exactness(isl_map_copy(map), isl_map_copy(app), | |||
899 | project)) < 0) | |||
900 | goto error; | |||
901 | ||||
902 | isl_space_free(dim); | |||
903 | app = set_path_length(app, 0, 1); | |||
904 | return app; | |||
905 | error: | |||
906 | isl_space_free(dim); | |||
907 | isl_map_free(app); | |||
908 | return NULL((void*)0); | |||
909 | } | |||
910 | ||||
911 | /* Call construct_component and, if "project" is set, project out | |||
912 | * the final coordinates. | |||
913 | */ | |||
914 | static __isl_give isl_map *construct_projected_component( | |||
915 | __isl_take isl_space *dim, | |||
916 | __isl_keep isl_map *map, int *exact, int project) | |||
917 | { | |||
918 | isl_map *app; | |||
919 | unsigned d; | |||
920 | ||||
921 | if (!dim) | |||
922 | return NULL((void*)0); | |||
923 | d = isl_space_dim(dim, isl_dim_in); | |||
924 | ||||
925 | app = construct_component(dim, map, exact, project); | |||
926 | if (project) { | |||
927 | app = isl_map_project_out(app, isl_dim_in, d - 1, 1); | |||
928 | app = isl_map_project_out(app, isl_dim_out, d - 1, 1); | |||
929 | } | |||
930 | return app; | |||
931 | } | |||
932 | ||||
933 | /* Compute an extended version, i.e., with path lengths, of | |||
934 | * an overapproximation of the transitive closure of "bmap" | |||
935 | * with path lengths greater than or equal to zero and with | |||
936 | * domain and range equal to "dom". | |||
937 | */ | |||
938 | static __isl_give isl_map *q_closure(__isl_take isl_space *dim, | |||
939 | __isl_take isl_setisl_map *dom, __isl_keep isl_basic_map *bmap, int *exact) | |||
940 | { | |||
941 | int project = 1; | |||
942 | isl_map *path; | |||
943 | isl_map *map; | |||
944 | isl_map *app; | |||
945 | ||||
946 | dom = isl_set_add_dims(dom, isl_dim_set, 1); | |||
947 | app = isl_map_from_domain_and_range(dom, isl_set_copy(dom)); | |||
948 | map = isl_map_from_basic_map(isl_basic_map_copy(bmap)); | |||
949 | path = construct_extended_path(dim, map, &project); | |||
950 | app = isl_map_intersect(app, path); | |||
951 | ||||
952 | if ((*exact = check_exactness(map, isl_map_copy(app), project)) < 0) | |||
953 | goto error; | |||
954 | ||||
955 | return app; | |||
956 | error: | |||
957 | isl_map_free(app); | |||
958 | return NULL((void*)0); | |||
959 | } | |||
960 | ||||
961 | /* Check whether qc has any elements of length at least one | |||
962 | * with domain and/or range outside of dom and ran. | |||
963 | */ | |||
964 | static int has_spurious_elements(__isl_keep isl_map *qc, | |||
965 | __isl_keep isl_setisl_map *dom, __isl_keep isl_setisl_map *ran) | |||
966 | { | |||
967 | isl_setisl_map *s; | |||
968 | int subset; | |||
969 | unsigned d; | |||
970 | ||||
971 | if (!qc || !dom || !ran) | |||
972 | return -1; | |||
973 | ||||
974 | d = isl_map_dim(qc, isl_dim_in); | |||
975 | ||||
976 | qc = isl_map_copy(qc); | |||
977 | qc = set_path_length(qc, 0, 1); | |||
978 | qc = isl_map_project_out(qc, isl_dim_in, d - 1, 1); | |||
979 | qc = isl_map_project_out(qc, isl_dim_out, d - 1, 1); | |||
980 | ||||
981 | s = isl_map_domain(isl_map_copy(qc)); | |||
982 | subset = isl_set_is_subset(s, dom); | |||
983 | isl_set_free(s); | |||
984 | if (subset < 0) | |||
985 | goto error; | |||
986 | if (!subset) { | |||
987 | isl_map_free(qc); | |||
988 | return 1; | |||
989 | } | |||
990 | ||||
991 | s = isl_map_range(qc); | |||
992 | subset = isl_set_is_subset(s, ran); | |||
993 | isl_set_free(s); | |||
994 | ||||
995 | return subset < 0 ? -1 : !subset; | |||
996 | error: | |||
997 | isl_map_free(qc); | |||
998 | return -1; | |||
999 | } | |||
1000 | ||||
1001 | #define LEFT2 2 | |||
1002 | #define RIGHT1 1 | |||
1003 | ||||
1004 | /* For each basic map in "map", except i, check whether it combines | |||
1005 | * with the transitive closure that is reflexive on C combines | |||
1006 | * to the left and to the right. | |||
1007 | * | |||
1008 | * In particular, if | |||
1009 | * | |||
1010 | * dom map_j \subseteq C | |||
1011 | * | |||
1012 | * then right[j] is set to 1. Otherwise, if | |||
1013 | * | |||
1014 | * ran map_i \cap dom map_j = \emptyset | |||
1015 | * | |||
1016 | * then right[j] is set to 0. Otherwise, composing to the right | |||
1017 | * is impossible. | |||
1018 | * | |||
1019 | * Similar, for composing to the left, we have if | |||
1020 | * | |||
1021 | * ran map_j \subseteq C | |||
1022 | * | |||
1023 | * then left[j] is set to 1. Otherwise, if | |||
1024 | * | |||
1025 | * dom map_i \cap ran map_j = \emptyset | |||
1026 | * | |||
1027 | * then left[j] is set to 0. Otherwise, composing to the left | |||
1028 | * is impossible. | |||
1029 | * | |||
1030 | * The return value is or'd with LEFT if composing to the left | |||
1031 | * is possible and with RIGHT if composing to the right is possible. | |||
1032 | */ | |||
1033 | static int composability(__isl_keep isl_setisl_map *C, int i, | |||
1034 | isl_setisl_map **dom, isl_setisl_map **ran, int *left, int *right, | |||
1035 | __isl_keep isl_map *map) | |||
1036 | { | |||
1037 | int j; | |||
1038 | int ok; | |||
1039 | ||||
1040 | ok = LEFT2 | RIGHT1; | |||
1041 | for (j = 0; j < map->n && ok; ++j) { | |||
1042 | int overlaps, subset; | |||
1043 | if (j == i) | |||
1044 | continue; | |||
1045 | ||||
1046 | if (ok & RIGHT1) { | |||
1047 | if (!dom[j]) | |||
1048 | dom[j] = isl_set_from_basic_set( | |||
1049 | isl_basic_map_domain( | |||
1050 | isl_basic_map_copy(map->p[j]))); | |||
1051 | if (!dom[j]) | |||
1052 | return -1; | |||
1053 | overlaps = isl_set_overlaps(ran[i], dom[j]); | |||
1054 | if (overlaps < 0) | |||
1055 | return -1; | |||
1056 | if (!overlaps) | |||
1057 | right[j] = 0; | |||
1058 | else { | |||
1059 | subset = isl_set_is_subset(dom[j], C); | |||
1060 | if (subset < 0) | |||
1061 | return -1; | |||
1062 | if (subset) | |||
1063 | right[j] = 1; | |||
1064 | else | |||
1065 | ok &= ~RIGHT1; | |||
1066 | } | |||
1067 | } | |||
1068 | ||||
1069 | if (ok & LEFT2) { | |||
1070 | if (!ran[j]) | |||
1071 | ran[j] = isl_set_from_basic_set( | |||
1072 | isl_basic_map_range( | |||
1073 | isl_basic_map_copy(map->p[j]))); | |||
1074 | if (!ran[j]) | |||
1075 | return -1; | |||
1076 | overlaps = isl_set_overlaps(dom[i], ran[j]); | |||
1077 | if (overlaps < 0) | |||
1078 | return -1; | |||
1079 | if (!overlaps) | |||
1080 | left[j] = 0; | |||
1081 | else { | |||
1082 | subset = isl_set_is_subset(ran[j], C); | |||
1083 | if (subset < 0) | |||
1084 | return -1; | |||
1085 | if (subset) | |||
1086 | left[j] = 1; | |||
1087 | else | |||
1088 | ok &= ~LEFT2; | |||
1089 | } | |||
1090 | } | |||
1091 | } | |||
1092 | ||||
1093 | return ok; | |||
1094 | } | |||
1095 | ||||
1096 | static __isl_give isl_map *anonymize(__isl_take isl_map *map) | |||
1097 | { | |||
1098 | map = isl_map_reset(map, isl_dim_in); | |||
1099 | map = isl_map_reset(map, isl_dim_out); | |||
1100 | return map; | |||
1101 | } | |||
1102 | ||||
1103 | /* Return a map that is a union of the basic maps in "map", except i, | |||
1104 | * composed to left and right with qc based on the entries of "left" | |||
1105 | * and "right". | |||
1106 | */ | |||
1107 | static __isl_give isl_map *compose(__isl_keep isl_map *map, int i, | |||
1108 | __isl_take isl_map *qc, int *left, int *right) | |||
1109 | { | |||
1110 | int j; | |||
1111 | isl_map *comp; | |||
1112 | ||||
1113 | comp = isl_map_empty(isl_map_get_space(map)); | |||
1114 | for (j = 0; j < map->n; ++j) { | |||
1115 | isl_map *map_j; | |||
1116 | ||||
1117 | if (j == i) | |||
1118 | continue; | |||
1119 | ||||
1120 | map_j = isl_map_from_basic_map(isl_basic_map_copy(map->p[j])); | |||
1121 | map_j = anonymize(map_j); | |||
1122 | if (left && left[j]) | |||
1123 | map_j = isl_map_apply_range(map_j, isl_map_copy(qc)); | |||
1124 | if (right && right[j]) | |||
1125 | map_j = isl_map_apply_range(isl_map_copy(qc), map_j); | |||
1126 | comp = isl_map_union(comp, map_j); | |||
1127 | } | |||
1128 | ||||
1129 | comp = isl_map_compute_divs(comp); | |||
1130 | comp = isl_map_coalesce(comp); | |||
1131 | ||||
1132 | isl_map_free(qc); | |||
1133 | ||||
1134 | return comp; | |||
1135 | } | |||
1136 | ||||
1137 | /* Compute the transitive closure of "map" incrementally by | |||
1138 | * computing | |||
1139 | * | |||
1140 | * map_i^+ \cup qc^+ | |||
1141 | * | |||
1142 | * or | |||
1143 | * | |||
1144 | * map_i^+ \cup ((id \cup map_i^) \circ qc^+) | |||
1145 | * | |||
1146 | * or | |||
1147 | * | |||
1148 | * map_i^+ \cup (qc^+ \circ (id \cup map_i^)) | |||
1149 | * | |||
1150 | * depending on whether left or right are NULL. | |||
1151 | */ | |||
1152 | static __isl_give isl_map *compute_incremental( | |||
1153 | __isl_take isl_space *dim, __isl_keep isl_map *map, | |||
1154 | int i, __isl_take isl_map *qc, int *left, int *right, int *exact) | |||
1155 | { | |||
1156 | isl_map *map_i; | |||
1157 | isl_map *tc; | |||
1158 | isl_map *rtc = NULL((void*)0); | |||
1159 | ||||
1160 | if (!map) | |||
1161 | goto error; | |||
1162 | isl_assert(map->ctx, left || right, goto error)do { if (left || right) break; do { isl_handle_error(map-> ctx, isl_error_unknown, "Assertion \"" "left || right" "\" failed" , "/tmp/buildd/llvm-toolchain-snapshot-3.7~svn239931/polly/lib/External/isl/isl_transitive_closure.c" , 1162); goto error; } while (0); } while (0); | |||
1163 | ||||
1164 | map_i = isl_map_from_basic_map(isl_basic_map_copy(map->p[i])); | |||
1165 | tc = construct_projected_component(isl_space_copy(dim), map_i, | |||
1166 | exact, 1); | |||
1167 | isl_map_free(map_i); | |||
1168 | ||||
1169 | if (*exact) | |||
1170 | qc = isl_map_transitive_closure(qc, exact); | |||
1171 | ||||
1172 | if (!*exact) { | |||
1173 | isl_space_free(dim); | |||
1174 | isl_map_free(tc); | |||
1175 | isl_map_free(qc); | |||
1176 | return isl_map_universe(isl_map_get_space(map)); | |||
1177 | } | |||
1178 | ||||
1179 | if (!left || !right) | |||
1180 | rtc = isl_map_union(isl_map_copy(tc), | |||
1181 | isl_map_identity(isl_map_get_space(tc))); | |||
1182 | if (!right) | |||
1183 | qc = isl_map_apply_range(rtc, qc); | |||
1184 | if (!left) | |||
1185 | qc = isl_map_apply_range(qc, rtc); | |||
1186 | qc = isl_map_union(tc, qc); | |||
1187 | ||||
1188 | isl_space_free(dim); | |||
1189 | ||||
1190 | return qc; | |||
1191 | error: | |||
1192 | isl_space_free(dim); | |||
1193 | isl_map_free(qc); | |||
1194 | return NULL((void*)0); | |||
1195 | } | |||
1196 | ||||
1197 | /* Given a map "map", try to find a basic map such that | |||
1198 | * map^+ can be computed as | |||
1199 | * | |||
1200 | * map^+ = map_i^+ \cup | |||
1201 | * \bigcup_j ((map_i^+ \cup Id_C)^+ \circ map_j \circ (map_i^+ \cup Id_C))^+ | |||
1202 | * | |||
1203 | * with C the simple hull of the domain and range of the input map. | |||
1204 | * map_i^ \cup Id_C is computed by allowing the path lengths to be zero | |||
1205 | * and by intersecting domain and range with C. | |||
1206 | * Of course, we need to check that this is actually equal to map_i^ \cup Id_C. | |||
1207 | * Also, we only use the incremental computation if all the transitive | |||
1208 | * closures are exact and if the number of basic maps in the union, | |||
1209 | * after computing the integer divisions, is smaller than the number | |||
1210 | * of basic maps in the input map. | |||
1211 | */ | |||
1212 | static int incemental_on_entire_domain(__isl_keep isl_space *dim, | |||
1213 | __isl_keep isl_map *map, | |||
1214 | isl_setisl_map **dom, isl_setisl_map **ran, int *left, int *right, | |||
1215 | __isl_give isl_map **res) | |||
1216 | { | |||
1217 | int i; | |||
1218 | isl_setisl_map *C; | |||
1219 | unsigned d; | |||
1220 | ||||
1221 | *res = NULL((void*)0); | |||
1222 | ||||
1223 | C = isl_set_union(isl_map_domain(isl_map_copy(map)), | |||
1224 | isl_map_range(isl_map_copy(map))); | |||
1225 | C = isl_set_from_basic_set(isl_set_simple_hull(C)); | |||
1226 | if (!C) | |||
1227 | return -1; | |||
1228 | if (C->n != 1) { | |||
1229 | isl_set_free(C); | |||
1230 | return 0; | |||
1231 | } | |||
1232 | ||||
1233 | d = isl_map_dim(map, isl_dim_in); | |||
1234 | ||||
1235 | for (i = 0; i < map->n; ++i) { | |||
1236 | isl_map *qc; | |||
1237 | int exact_i, spurious; | |||
1238 | int j; | |||
1239 | dom[i] = isl_set_from_basic_set(isl_basic_map_domain( | |||
1240 | isl_basic_map_copy(map->p[i]))); | |||
1241 | ran[i] = isl_set_from_basic_set(isl_basic_map_range( | |||
1242 | isl_basic_map_copy(map->p[i]))); | |||
1243 | qc = q_closure(isl_space_copy(dim), isl_set_copy(C), | |||
1244 | map->p[i], &exact_i); | |||
1245 | if (!qc) | |||
1246 | goto error; | |||
1247 | if (!exact_i) { | |||
1248 | isl_map_free(qc); | |||
1249 | continue; | |||
1250 | } | |||
1251 | spurious = has_spurious_elements(qc, dom[i], ran[i]); | |||
1252 | if (spurious) { | |||
1253 | isl_map_free(qc); | |||
1254 | if (spurious < 0) | |||
1255 | goto error; | |||
1256 | continue; | |||
1257 | } | |||
1258 | qc = isl_map_project_out(qc, isl_dim_in, d, 1); | |||
1259 | qc = isl_map_project_out(qc, isl_dim_out, d, 1); | |||
1260 | qc = isl_map_compute_divs(qc); | |||
1261 | for (j = 0; j < map->n; ++j) | |||
1262 | left[j] = right[j] = 1; | |||
1263 | qc = compose(map, i, qc, left, right); | |||
1264 | if (!qc) | |||
1265 | goto error; | |||
1266 | if (qc->n >= map->n) { | |||
1267 | isl_map_free(qc); | |||
1268 | continue; | |||
1269 | } | |||
1270 | *res = compute_incremental(isl_space_copy(dim), map, i, qc, | |||
1271 | left, right, &exact_i); | |||
1272 | if (!*res) | |||
1273 | goto error; | |||
1274 | if (exact_i) | |||
1275 | break; | |||
1276 | isl_map_free(*res); | |||
1277 | *res = NULL((void*)0); | |||
1278 | } | |||
1279 | ||||
1280 | isl_set_free(C); | |||
1281 | ||||
1282 | return *res != NULL((void*)0); | |||
1283 | error: | |||
1284 | isl_set_free(C); | |||
1285 | return -1; | |||
1286 | } | |||
1287 | ||||
1288 | /* Try and compute the transitive closure of "map" as | |||
1289 | * | |||
1290 | * map^+ = map_i^+ \cup | |||
1291 | * \bigcup_j ((map_i^+ \cup Id_C)^+ \circ map_j \circ (map_i^+ \cup Id_C))^+ | |||
1292 | * | |||
1293 | * with C either the simple hull of the domain and range of the entire | |||
1294 | * map or the simple hull of domain and range of map_i. | |||
1295 | */ | |||
1296 | static __isl_give isl_map *incremental_closure(__isl_take isl_space *dim, | |||
1297 | __isl_keep isl_map *map, int *exact, int project) | |||
1298 | { | |||
1299 | int i; | |||
1300 | isl_setisl_map **dom = NULL((void*)0); | |||
1301 | isl_setisl_map **ran = NULL((void*)0); | |||
1302 | int *left = NULL((void*)0); | |||
1303 | int *right = NULL((void*)0); | |||
1304 | isl_setisl_map *C; | |||
1305 | unsigned d; | |||
1306 | isl_map *res = NULL((void*)0); | |||
1307 | ||||
1308 | if (!project) | |||
1309 | return construct_projected_component(dim, map, exact, project); | |||
1310 | ||||
1311 | if (!map) | |||
1312 | goto error; | |||
1313 | if (map->n <= 1) | |||
1314 | return construct_projected_component(dim, map, exact, project); | |||
1315 | ||||
1316 | d = isl_map_dim(map, isl_dim_in); | |||
1317 | ||||
1318 | dom = isl_calloc_array(map->ctx, isl_set *, map->n)((isl_map * *)isl_calloc_or_die(map->ctx, map->n, sizeof (isl_map *))); | |||
1319 | ran = isl_calloc_array(map->ctx, isl_set *, map->n)((isl_map * *)isl_calloc_or_die(map->ctx, map->n, sizeof (isl_map *))); | |||
1320 | left = isl_calloc_array(map->ctx, int, map->n)((int *)isl_calloc_or_die(map->ctx, map->n, sizeof(int) )); | |||
1321 | right = isl_calloc_array(map->ctx, int, map->n)((int *)isl_calloc_or_die(map->ctx, map->n, sizeof(int) )); | |||
1322 | if (!ran || !dom || !left || !right) | |||
1323 | goto error; | |||
1324 | ||||
1325 | if (incemental_on_entire_domain(dim, map, dom, ran, left, right, &res) < 0) | |||
1326 | goto error; | |||
1327 | ||||
1328 | for (i = 0; !res && i < map->n; ++i) { | |||
1329 | isl_map *qc; | |||
1330 | int exact_i, spurious, comp; | |||
1331 | if (!dom[i]) | |||
1332 | dom[i] = isl_set_from_basic_set( | |||
1333 | isl_basic_map_domain( | |||
1334 | isl_basic_map_copy(map->p[i]))); | |||
1335 | if (!dom[i]) | |||
1336 | goto error; | |||
1337 | if (!ran[i]) | |||
1338 | ran[i] = isl_set_from_basic_set( | |||
1339 | isl_basic_map_range( | |||
1340 | isl_basic_map_copy(map->p[i]))); | |||
1341 | if (!ran[i]) | |||
1342 | goto error; | |||
1343 | C = isl_set_union(isl_set_copy(dom[i]), | |||
1344 | isl_set_copy(ran[i])); | |||
1345 | C = isl_set_from_basic_set(isl_set_simple_hull(C)); | |||
1346 | if (!C) | |||
1347 | goto error; | |||
1348 | if (C->n != 1) { | |||
1349 | isl_set_free(C); | |||
1350 | continue; | |||
1351 | } | |||
1352 | comp = composability(C, i, dom, ran, left, right, map); | |||
1353 | if (!comp || comp < 0) { | |||
1354 | isl_set_free(C); | |||
1355 | if (comp < 0) | |||
1356 | goto error; | |||
1357 | continue; | |||
1358 | } | |||
1359 | qc = q_closure(isl_space_copy(dim), C, map->p[i], &exact_i); | |||
1360 | if (!qc) | |||
1361 | goto error; | |||
1362 | if (!exact_i) { | |||
1363 | isl_map_free(qc); | |||
1364 | continue; | |||
1365 | } | |||
1366 | spurious = has_spurious_elements(qc, dom[i], ran[i]); | |||
1367 | if (spurious) { | |||
1368 | isl_map_free(qc); | |||
1369 | if (spurious < 0) | |||
1370 | goto error; | |||
1371 | continue; | |||
1372 | } | |||
1373 | qc = isl_map_project_out(qc, isl_dim_in, d, 1); | |||
1374 | qc = isl_map_project_out(qc, isl_dim_out, d, 1); | |||
1375 | qc = isl_map_compute_divs(qc); | |||
1376 | qc = compose(map, i, qc, (comp & LEFT2) ? left : NULL((void*)0), | |||
1377 | (comp & RIGHT1) ? right : NULL((void*)0)); | |||
1378 | if (!qc) | |||
1379 | goto error; | |||
1380 | if (qc->n >= map->n) { | |||
1381 | isl_map_free(qc); | |||
1382 | continue; | |||
1383 | } | |||
1384 | res = compute_incremental(isl_space_copy(dim), map, i, qc, | |||
1385 | (comp & LEFT2) ? left : NULL((void*)0), | |||
1386 | (comp & RIGHT1) ? right : NULL((void*)0), &exact_i); | |||
1387 | if (!res) | |||
1388 | goto error; | |||
1389 | if (exact_i) | |||
1390 | break; | |||
1391 | isl_map_free(res); | |||
1392 | res = NULL((void*)0); | |||
1393 | } | |||
1394 | ||||
1395 | for (i = 0; i < map->n; ++i) { | |||
1396 | isl_set_free(dom[i]); | |||
1397 | isl_set_free(ran[i]); | |||
1398 | } | |||
1399 | free(dom); | |||
1400 | free(ran); | |||
1401 | free(left); | |||
1402 | free(right); | |||
1403 | ||||
1404 | if (res) { | |||
1405 | isl_space_free(dim); | |||
1406 | return res; | |||
1407 | } | |||
1408 | ||||
1409 | return construct_projected_component(dim, map, exact, project); | |||
1410 | error: | |||
1411 | if (dom) | |||
1412 | for (i = 0; i < map->n; ++i) | |||
1413 | isl_set_free(dom[i]); | |||
1414 | free(dom); | |||
1415 | if (ran) | |||
1416 | for (i = 0; i < map->n; ++i) | |||
1417 | isl_set_free(ran[i]); | |||
1418 | free(ran); | |||
1419 | free(left); | |||
1420 | free(right); | |||
1421 | isl_space_free(dim); | |||
1422 | return NULL((void*)0); | |||
1423 | } | |||
1424 | ||||
1425 | /* Given an array of sets "set", add "dom" at position "pos" | |||
1426 | * and search for elements at earlier positions that overlap with "dom". | |||
1427 | * If any can be found, then merge all of them, together with "dom", into | |||
1428 | * a single set and assign the union to the first in the array, | |||
1429 | * which becomes the new group leader for all groups involved in the merge. | |||
1430 | * During the search, we only consider group leaders, i.e., those with | |||
1431 | * group[i] = i, as the other sets have already been combined | |||
1432 | * with one of the group leaders. | |||
1433 | */ | |||
1434 | static int merge(isl_setisl_map **set, int *group, __isl_take isl_setisl_map *dom, int pos) | |||
1435 | { | |||
1436 | int i; | |||
1437 | ||||
1438 | group[pos] = pos; | |||
1439 | set[pos] = isl_set_copy(dom); | |||
1440 | ||||
1441 | for (i = pos - 1; i >= 0; --i) { | |||
1442 | int o; | |||
1443 | ||||
1444 | if (group[i] != i) | |||
1445 | continue; | |||
1446 | ||||
1447 | o = isl_set_overlaps(set[i], dom); | |||
1448 | if (o < 0) | |||
1449 | goto error; | |||
1450 | if (!o) | |||
1451 | continue; | |||
1452 | ||||
1453 | set[i] = isl_set_union(set[i], set[group[pos]]); | |||
1454 | set[group[pos]] = NULL((void*)0); | |||
1455 | if (!set[i]) | |||
1456 | goto error; | |||
1457 | group[group[pos]] = i; | |||
1458 | group[pos] = i; | |||
1459 | } | |||
1460 | ||||
1461 | isl_set_free(dom); | |||
1462 | return 0; | |||
1463 | error: | |||
1464 | isl_set_free(dom); | |||
1465 | return -1; | |||
1466 | } | |||
1467 | ||||
1468 | /* Replace each entry in the n by n grid of maps by the cross product | |||
1469 | * with the relation { [i] -> [i + 1] }. | |||
1470 | */ | |||
1471 | static int add_length(__isl_keep isl_map *map, isl_map ***grid, int n) | |||
1472 | { | |||
1473 | int i, j, k; | |||
1474 | isl_space *dim; | |||
1475 | isl_basic_map *bstep; | |||
1476 | isl_map *step; | |||
1477 | unsigned nparam; | |||
1478 | ||||
1479 | if (!map) | |||
1480 | return -1; | |||
1481 | ||||
1482 | dim = isl_map_get_space(map); | |||
1483 | nparam = isl_space_dim(dim, isl_dim_param); | |||
1484 | dim = isl_space_drop_dims(dim, isl_dim_in, 0, isl_space_dim(dim, isl_dim_in)); | |||
1485 | dim = isl_space_drop_dims(dim, isl_dim_out, 0, isl_space_dim(dim, isl_dim_out)); | |||
1486 | dim = isl_space_add_dims(dim, isl_dim_in, 1); | |||
1487 | dim = isl_space_add_dims(dim, isl_dim_out, 1); | |||
1488 | bstep = isl_basic_map_alloc_space(dim, 0, 1, 0); | |||
1489 | k = isl_basic_map_alloc_equality(bstep); | |||
1490 | if (k < 0) { | |||
1491 | isl_basic_map_free(bstep); | |||
1492 | return -1; | |||
1493 | } | |||
1494 | isl_seq_clr(bstep->eq[k], 1 + isl_basic_map_total_dim(bstep)); | |||
1495 | isl_int_set_si(bstep->eq[k][0], 1)impz_set_si(bstep->eq[k][0],1); | |||
1496 | isl_int_set_si(bstep->eq[k][1 + nparam], 1)impz_set_si(bstep->eq[k][1 + nparam],1); | |||
1497 | isl_int_set_si(bstep->eq[k][1 + nparam + 1], -1)impz_set_si(bstep->eq[k][1 + nparam + 1],-1); | |||
1498 | bstep = isl_basic_map_finalize(bstep); | |||
1499 | step = isl_map_from_basic_map(bstep); | |||
1500 | ||||
1501 | for (i = 0; i < n; ++i) | |||
1502 | for (j = 0; j < n; ++j) | |||
1503 | grid[i][j] = isl_map_product(grid[i][j], | |||
1504 | isl_map_copy(step)); | |||
1505 | ||||
1506 | isl_map_free(step); | |||
1507 | ||||
1508 | return 0; | |||
1509 | } | |||
1510 | ||||
1511 | /* The core of the Floyd-Warshall algorithm. | |||
1512 | * Updates the given n x x matrix of relations in place. | |||
1513 | * | |||
1514 | * The algorithm iterates over all vertices. In each step, the whole | |||
1515 | * matrix is updated to include all paths that go to the current vertex, | |||
1516 | * possibly stay there a while (including passing through earlier vertices) | |||
1517 | * and then come back. At the start of each iteration, the diagonal | |||
1518 | * element corresponding to the current vertex is replaced by its | |||
1519 | * transitive closure to account for all indirect paths that stay | |||
1520 | * in the current vertex. | |||
1521 | */ | |||
1522 | static void floyd_warshall_iterate(isl_map ***grid, int n, int *exact) | |||
1523 | { | |||
1524 | int r, p, q; | |||
1525 | ||||
1526 | for (r = 0; r < n; ++r) { | |||
1527 | int r_exact; | |||
1528 | grid[r][r] = isl_map_transitive_closure(grid[r][r], | |||
1529 | (exact && *exact) ? &r_exact : NULL((void*)0)); | |||
1530 | if (exact && *exact && !r_exact) | |||
| ||||
1531 | *exact = 0; | |||
1532 | ||||
1533 | for (p = 0; p < n; ++p) | |||
1534 | for (q = 0; q < n; ++q) { | |||
1535 | isl_map *loop; | |||
1536 | if (p == r && q == r) | |||
1537 | continue; | |||
1538 | loop = isl_map_apply_range( | |||
1539 | isl_map_copy(grid[p][r]), | |||
1540 | isl_map_copy(grid[r][q])); | |||
1541 | grid[p][q] = isl_map_union(grid[p][q], loop); | |||
1542 | loop = isl_map_apply_range( | |||
1543 | isl_map_copy(grid[p][r]), | |||
1544 | isl_map_apply_range( | |||
1545 | isl_map_copy(grid[r][r]), | |||
1546 | isl_map_copy(grid[r][q]))); | |||
1547 | grid[p][q] = isl_map_union(grid[p][q], loop); | |||
1548 | grid[p][q] = isl_map_coalesce(grid[p][q]); | |||
1549 | } | |||
1550 | } | |||
1551 | } | |||
1552 | ||||
1553 | /* Given a partition of the domains and ranges of the basic maps in "map", | |||
1554 | * apply the Floyd-Warshall algorithm with the elements in the partition | |||
1555 | * as vertices. | |||
1556 | * | |||
1557 | * In particular, there are "n" elements in the partition and "group" is | |||
1558 | * an array of length 2 * map->n with entries in [0,n-1]. | |||
1559 | * | |||
1560 | * We first construct a matrix of relations based on the partition information, | |||
1561 | * apply Floyd-Warshall on this matrix of relations and then take the | |||
1562 | * union of all entries in the matrix as the final result. | |||
1563 | * | |||
1564 | * If we are actually computing the power instead of the transitive closure, | |||
1565 | * i.e., when "project" is not set, then the result should have the | |||
1566 | * path lengths encoded as the difference between an extra pair of | |||
1567 | * coordinates. We therefore apply the nested transitive closures | |||
1568 | * to relations that include these lengths. In particular, we replace | |||
1569 | * the input relation by the cross product with the unit length relation | |||
1570 | * { [i] -> [i + 1] }. | |||
1571 | */ | |||
1572 | static __isl_give isl_map *floyd_warshall_with_groups(__isl_take isl_space *dim, | |||
1573 | __isl_keep isl_map *map, int *exact, int project, int *group, int n) | |||
1574 | { | |||
1575 | int i, j, k; | |||
1576 | isl_map ***grid = NULL((void*)0); | |||
1577 | isl_map *app; | |||
1578 | ||||
1579 | if (!map) | |||
1580 | goto error; | |||
1581 | ||||
1582 | if (n == 1) { | |||
1583 | free(group); | |||
1584 | return incremental_closure(dim, map, exact, project); | |||
1585 | } | |||
1586 | ||||
1587 | grid = isl_calloc_array(map->ctx, isl_map **, n)((isl_map ** *)isl_calloc_or_die(map->ctx, n, sizeof(isl_map **))); | |||
1588 | if (!grid) | |||
1589 | goto error; | |||
1590 | for (i = 0; i < n; ++i) { | |||
1591 | grid[i] = isl_calloc_array(map->ctx, isl_map *, n)((isl_map * *)isl_calloc_or_die(map->ctx, n, sizeof(isl_map *))); | |||
1592 | if (!grid[i]) | |||
1593 | goto error; | |||
1594 | for (j = 0; j < n; ++j) | |||
1595 | grid[i][j] = isl_map_empty(isl_map_get_space(map)); | |||
1596 | } | |||
1597 | ||||
1598 | for (k = 0; k < map->n; ++k) { | |||
1599 | i = group[2 * k]; | |||
1600 | j = group[2 * k + 1]; | |||
1601 | grid[i][j] = isl_map_union(grid[i][j], | |||
1602 | isl_map_from_basic_map( | |||
1603 | isl_basic_map_copy(map->p[k]))); | |||
1604 | } | |||
1605 | ||||
1606 | if (!project && add_length(map, grid, n) < 0) | |||
1607 | goto error; | |||
1608 | ||||
1609 | floyd_warshall_iterate(grid, n, exact); | |||
1610 | ||||
1611 | app = isl_map_empty(isl_map_get_space(map)); | |||
1612 | ||||
1613 | for (i = 0; i < n; ++i) { | |||
1614 | for (j = 0; j < n; ++j) | |||
1615 | app = isl_map_union(app, grid[i][j]); | |||
1616 | free(grid[i]); | |||
1617 | } | |||
1618 | free(grid); | |||
1619 | ||||
1620 | free(group); | |||
1621 | isl_space_free(dim); | |||
1622 | ||||
1623 | return app; | |||
1624 | error: | |||
1625 | if (grid) | |||
1626 | for (i = 0; i < n; ++i) { | |||
1627 | if (!grid[i]) | |||
1628 | continue; | |||
1629 | for (j = 0; j < n; ++j) | |||
1630 | isl_map_free(grid[i][j]); | |||
1631 | free(grid[i]); | |||
1632 | } | |||
1633 | free(grid); | |||
1634 | free(group); | |||
1635 | isl_space_free(dim); | |||
1636 | return NULL((void*)0); | |||
1637 | } | |||
1638 | ||||
1639 | /* Partition the domains and ranges of the n basic relations in list | |||
1640 | * into disjoint cells. | |||
1641 | * | |||
1642 | * To find the partition, we simply consider all of the domains | |||
1643 | * and ranges in turn and combine those that overlap. | |||
1644 | * "set" contains the partition elements and "group" indicates | |||
1645 | * to which partition element a given domain or range belongs. | |||
1646 | * The domain of basic map i corresponds to element 2 * i in these arrays, | |||
1647 | * while the domain corresponds to element 2 * i + 1. | |||
1648 | * During the construction group[k] is either equal to k, | |||
1649 | * in which case set[k] contains the union of all the domains and | |||
1650 | * ranges in the corresponding group, or is equal to some l < k, | |||
1651 | * with l another domain or range in the same group. | |||
1652 | */ | |||
1653 | static int *setup_groups(isl_ctx *ctx, __isl_keep isl_basic_map **list, int n, | |||
1654 | isl_setisl_map ***set, int *n_group) | |||
1655 | { | |||
1656 | int i; | |||
1657 | int *group = NULL((void*)0); | |||
1658 | int g; | |||
1659 | ||||
1660 | *set = isl_calloc_array(ctx, isl_set *, 2 * n)((isl_map * *)isl_calloc_or_die(ctx, 2 * n, sizeof(isl_map *) )); | |||
1661 | group = isl_alloc_array(ctx, int, 2 * n)((int *)isl_malloc_or_die(ctx, (2 * n)*sizeof(int))); | |||
1662 | ||||
1663 | if (!*set || !group) | |||
1664 | goto error; | |||
1665 | ||||
1666 | for (i = 0; i < n; ++i) { | |||
1667 | isl_setisl_map *dom; | |||
1668 | dom = isl_set_from_basic_set(isl_basic_map_domain( | |||
1669 | isl_basic_map_copy(list[i]))); | |||
1670 | if (merge(*set, group, dom, 2 * i) < 0) | |||
1671 | goto error; | |||
1672 | dom = isl_set_from_basic_set(isl_basic_map_range( | |||
1673 | isl_basic_map_copy(list[i]))); | |||
1674 | if (merge(*set, group, dom, 2 * i + 1) < 0) | |||
1675 | goto error; | |||
1676 | } | |||
1677 | ||||
1678 | g = 0; | |||
1679 | for (i = 0; i < 2 * n; ++i) | |||
1680 | if (group[i] == i) { | |||
1681 | if (g != i) { | |||
1682 | (*set)[g] = (*set)[i]; | |||
1683 | (*set)[i] = NULL((void*)0); | |||
1684 | } | |||
1685 | group[i] = g++; | |||
1686 | } else | |||
1687 | group[i] = group[group[i]]; | |||
1688 | ||||
1689 | *n_group = g; | |||
1690 | ||||
1691 | return group; | |||
1692 | error: | |||
1693 | if (*set) { | |||
1694 | for (i = 0; i < 2 * n; ++i) | |||
1695 | isl_set_free((*set)[i]); | |||
1696 | free(*set); | |||
1697 | *set = NULL((void*)0); | |||
1698 | } | |||
1699 | free(group); | |||
1700 | return NULL((void*)0); | |||
1701 | } | |||
1702 | ||||
1703 | /* Check if the domains and ranges of the basic maps in "map" can | |||
1704 | * be partitioned, and if so, apply Floyd-Warshall on the elements | |||
1705 | * of the partition. Note that we also apply this algorithm | |||
1706 | * if we want to compute the power, i.e., when "project" is not set. | |||
1707 | * However, the results are unlikely to be exact since the recursive | |||
1708 | * calls inside the Floyd-Warshall algorithm typically result in | |||
1709 | * non-linear path lengths quite quickly. | |||
1710 | */ | |||
1711 | static __isl_give isl_map *floyd_warshall(__isl_take isl_space *dim, | |||
1712 | __isl_keep isl_map *map, int *exact, int project) | |||
1713 | { | |||
1714 | int i; | |||
1715 | isl_setisl_map **set = NULL((void*)0); | |||
1716 | int *group = NULL((void*)0); | |||
1717 | int n; | |||
1718 | ||||
1719 | if (!map) | |||
1720 | goto error; | |||
1721 | if (map->n <= 1) | |||
1722 | return incremental_closure(dim, map, exact, project); | |||
1723 | ||||
1724 | group = setup_groups(map->ctx, map->p, map->n, &set, &n); | |||
1725 | if (!group) | |||
1726 | goto error; | |||
1727 | ||||
1728 | for (i = 0; i < 2 * map->n; ++i) | |||
1729 | isl_set_free(set[i]); | |||
1730 | ||||
1731 | free(set); | |||
1732 | ||||
1733 | return floyd_warshall_with_groups(dim, map, exact, project, group, n); | |||
1734 | error: | |||
1735 | isl_space_free(dim); | |||
1736 | return NULL((void*)0); | |||
1737 | } | |||
1738 | ||||
1739 | /* Structure for representing the nodes of the graph of which | |||
1740 | * strongly connected components are being computed. | |||
1741 | * | |||
1742 | * list contains the actual nodes | |||
1743 | * check_closed is set if we may have used the fact that | |||
1744 | * a pair of basic maps can be interchanged | |||
1745 | */ | |||
1746 | struct isl_tc_follows_data { | |||
1747 | isl_basic_map **list; | |||
1748 | int check_closed; | |||
1749 | }; | |||
1750 | ||||
1751 | /* Check whether in the computation of the transitive closure | |||
1752 | * "list[i]" (R_1) should follow (or be part of the same component as) | |||
1753 | * "list[j]" (R_2). | |||
1754 | * | |||
1755 | * That is check whether | |||
1756 | * | |||
1757 | * R_1 \circ R_2 | |||
1758 | * | |||
1759 | * is a subset of | |||
1760 | * | |||
1761 | * R_2 \circ R_1 | |||
1762 | * | |||
1763 | * If so, then there is no reason for R_1 to immediately follow R_2 | |||
1764 | * in any path. | |||
1765 | * | |||
1766 | * *check_closed is set if the subset relation holds while | |||
1767 | * R_1 \circ R_2 is not empty. | |||
1768 | */ | |||
1769 | static isl_bool basic_map_follows(int i, int j, void *user) | |||
1770 | { | |||
1771 | struct isl_tc_follows_data *data = user; | |||
1772 | struct isl_map *map12 = NULL((void*)0); | |||
1773 | struct isl_map *map21 = NULL((void*)0); | |||
1774 | isl_bool subset; | |||
1775 | ||||
1776 | if (!isl_space_tuple_is_equal(data->list[i]->dim, isl_dim_in, | |||
1777 | data->list[j]->dim, isl_dim_out)) | |||
1778 | return isl_bool_false; | |||
1779 | ||||
1780 | map21 = isl_map_from_basic_map( | |||
1781 | isl_basic_map_apply_range( | |||
1782 | isl_basic_map_copy(data->list[j]), | |||
1783 | isl_basic_map_copy(data->list[i]))); | |||
1784 | subset = isl_map_is_empty(map21); | |||
1785 | if (subset < 0) | |||
1786 | goto error; | |||
1787 | if (subset) { | |||
1788 | isl_map_free(map21); | |||
1789 | return isl_bool_false; | |||
1790 | } | |||
1791 | ||||
1792 | if (!isl_space_tuple_is_equal(data->list[i]->dim, isl_dim_in, | |||
1793 | data->list[i]->dim, isl_dim_out) || | |||
1794 | !isl_space_tuple_is_equal(data->list[j]->dim, isl_dim_in, | |||
1795 | data->list[j]->dim, isl_dim_out)) { | |||
1796 | isl_map_free(map21); | |||
1797 | return isl_bool_true; | |||
1798 | } | |||
1799 | ||||
1800 | map12 = isl_map_from_basic_map( | |||
1801 | isl_basic_map_apply_range( | |||
1802 | isl_basic_map_copy(data->list[i]), | |||
1803 | isl_basic_map_copy(data->list[j]))); | |||
1804 | ||||
1805 | subset = isl_map_is_subset(map21, map12); | |||
1806 | ||||
1807 | isl_map_free(map12); | |||
1808 | isl_map_free(map21); | |||
1809 | ||||
1810 | if (subset) | |||
1811 | data->check_closed = 1; | |||
1812 | ||||
1813 | return subset < 0 ? isl_bool_error : !subset; | |||
1814 | error: | |||
1815 | isl_map_free(map21); | |||
1816 | return isl_bool_error; | |||
1817 | } | |||
1818 | ||||
1819 | /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D | |||
1820 | * and a dimension specification (Z^{n+1} -> Z^{n+1}), | |||
1821 | * construct a map that is an overapproximation of the map | |||
1822 | * that takes an element from the dom R \times Z to an | |||
1823 | * element from ran R \times Z, such that the first n coordinates of the | |||
1824 | * difference between them is a sum of differences between images | |||
1825 | * and pre-images in one of the R_i and such that the last coordinate | |||
1826 | * is equal to the number of steps taken. | |||
1827 | * If "project" is set, then these final coordinates are not included, | |||
1828 | * i.e., a relation of type Z^n -> Z^n is returned. | |||
1829 | * That is, let | |||
1830 | * | |||
1831 | * \Delta_i = { y - x | (x, y) in R_i } | |||
1832 | * | |||
1833 | * then the constructed map is an overapproximation of | |||
1834 | * | |||
1835 | * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : | |||
1836 | * d = (\sum_i k_i \delta_i, \sum_i k_i) and | |||
1837 | * x in dom R and x + d in ran R } | |||
1838 | * | |||
1839 | * or | |||
1840 | * | |||
1841 | * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : | |||
1842 | * d = (\sum_i k_i \delta_i) and | |||
1843 | * x in dom R and x + d in ran R } | |||
1844 | * | |||
1845 | * if "project" is set. | |||
1846 | * | |||
1847 | * We first split the map into strongly connected components, perform | |||
1848 | * the above on each component and then join the results in the correct | |||
1849 | * order, at each join also taking in the union of both arguments | |||
1850 | * to allow for paths that do not go through one of the two arguments. | |||
1851 | */ | |||
1852 | static __isl_give isl_map *construct_power_components(__isl_take isl_space *dim, | |||
1853 | __isl_keep isl_map *map, int *exact, int project) | |||
1854 | { | |||
1855 | int i, n, c; | |||
1856 | struct isl_map *path = NULL((void*)0); | |||
1857 | struct isl_tc_follows_data data; | |||
1858 | struct isl_tarjan_graph *g = NULL((void*)0); | |||
1859 | int *orig_exact; | |||
1860 | int local_exact; | |||
1861 | ||||
1862 | if (!map) | |||
1863 | goto error; | |||
1864 | if (map->n <= 1) | |||
1865 | return floyd_warshall(dim, map, exact, project); | |||
1866 | ||||
1867 | data.list = map->p; | |||
1868 | data.check_closed = 0; | |||
1869 | g = isl_tarjan_graph_init(map->ctx, map->n, &basic_map_follows, &data); | |||
1870 | if (!g) | |||
1871 | goto error; | |||
1872 | ||||
1873 | orig_exact = exact; | |||
1874 | if (data.check_closed && !exact) | |||
1875 | exact = &local_exact; | |||
1876 | ||||
1877 | c = 0; | |||
1878 | i = 0; | |||
1879 | n = map->n; | |||
1880 | if (project) | |||
1881 | path = isl_map_empty(isl_map_get_space(map)); | |||
1882 | else | |||
1883 | path = isl_map_empty(isl_space_copy(dim)); | |||
1884 | path = anonymize(path); | |||
1885 | while (n) { | |||
1886 | struct isl_map *comp; | |||
1887 | isl_map *path_comp, *path_comb; | |||
1888 | comp = isl_map_alloc_space(isl_map_get_space(map), n, 0); | |||
1889 | while (g->order[i] != -1) { | |||
1890 | comp = isl_map_add_basic_map(comp, | |||
1891 | isl_basic_map_copy(map->p[g->order[i]])); | |||
1892 | --n; | |||
1893 | ++i; | |||
1894 | } | |||
1895 | path_comp = floyd_warshall(isl_space_copy(dim), | |||
1896 | comp, exact, project); | |||
1897 | path_comp = anonymize(path_comp); | |||
1898 | path_comb = isl_map_apply_range(isl_map_copy(path), | |||
1899 | isl_map_copy(path_comp)); | |||
1900 | path = isl_map_union(path, path_comp); | |||
1901 | path = isl_map_union(path, path_comb); | |||
1902 | isl_map_free(comp); | |||
1903 | ++i; | |||
1904 | ++c; | |||
1905 | } | |||
1906 | ||||
1907 | if (c > 1 && data.check_closed && !*exact) { | |||
1908 | int closed; | |||
1909 | ||||
1910 | closed = isl_map_is_transitively_closed(path); | |||
1911 | if (closed < 0) | |||
1912 | goto error; | |||
1913 | if (!closed) { | |||
1914 | isl_tarjan_graph_free(g); | |||
1915 | isl_map_free(path); | |||
1916 | return floyd_warshall(dim, map, orig_exact, project); | |||
1917 | } | |||
1918 | } | |||
1919 | ||||
1920 | isl_tarjan_graph_free(g); | |||
1921 | isl_space_free(dim); | |||
1922 | ||||
1923 | return path; | |||
1924 | error: | |||
1925 | isl_tarjan_graph_free(g); | |||
1926 | isl_space_free(dim); | |||
1927 | isl_map_free(path); | |||
1928 | return NULL((void*)0); | |||
1929 | } | |||
1930 | ||||
1931 | /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D, | |||
1932 | * construct a map that is an overapproximation of the map | |||
1933 | * that takes an element from the space D to another | |||
1934 | * element from the same space, such that the difference between | |||
1935 | * them is a strictly positive sum of differences between images | |||
1936 | * and pre-images in one of the R_i. | |||
1937 | * The number of differences in the sum is equated to parameter "param". | |||
1938 | * That is, let | |||
1939 | * | |||
1940 | * \Delta_i = { y - x | (x, y) in R_i } | |||
1941 | * | |||
1942 | * then the constructed map is an overapproximation of | |||
1943 | * | |||
1944 | * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : | |||
1945 | * d = \sum_i k_i \delta_i and k = \sum_i k_i > 0 } | |||
1946 | * or | |||
1947 | * | |||
1948 | * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : | |||
1949 | * d = \sum_i k_i \delta_i and \sum_i k_i > 0 } | |||
1950 | * | |||
1951 | * if "project" is set. | |||
1952 | * | |||
1953 | * If "project" is not set, then | |||
1954 | * we construct an extended mapping with an extra coordinate | |||
1955 | * that indicates the number of steps taken. In particular, | |||
1956 | * the difference in the last coordinate is equal to the number | |||
1957 | * of steps taken to move from a domain element to the corresponding | |||
1958 | * image element(s). | |||
1959 | */ | |||
1960 | static __isl_give isl_map *construct_power(__isl_keep isl_map *map, | |||
1961 | int *exact, int project) | |||
1962 | { | |||
1963 | struct isl_map *app = NULL((void*)0); | |||
1964 | isl_space *dim = NULL((void*)0); | |||
1965 | ||||
1966 | if (!map) | |||
1967 | return NULL((void*)0); | |||
1968 | ||||
1969 | dim = isl_map_get_space(map); | |||
1970 | ||||
1971 | dim = isl_space_add_dims(dim, isl_dim_in, 1); | |||
1972 | dim = isl_space_add_dims(dim, isl_dim_out, 1); | |||
1973 | ||||
1974 | app = construct_power_components(isl_space_copy(dim), map, | |||
1975 | exact, project); | |||
1976 | ||||
1977 | isl_space_free(dim); | |||
1978 | ||||
1979 | return app; | |||
1980 | } | |||
1981 | ||||
1982 | /* Compute the positive powers of "map", or an overapproximation. | |||
1983 | * If the result is exact, then *exact is set to 1. | |||
1984 | * | |||
1985 | * If project is set, then we are actually interested in the transitive | |||
1986 | * closure, so we can use a more relaxed exactness check. | |||
1987 | * The lengths of the paths are also projected out instead of being | |||
1988 | * encoded as the difference between an extra pair of final coordinates. | |||
1989 | */ | |||
1990 | static __isl_give isl_map *map_power(__isl_take isl_map *map, | |||
1991 | int *exact, int project) | |||
1992 | { | |||
1993 | struct isl_map *app = NULL((void*)0); | |||
1994 | ||||
1995 | if (exact) | |||
1996 | *exact = 1; | |||
1997 | ||||
1998 | if (!map) | |||
1999 | return NULL((void*)0); | |||
2000 | ||||
2001 | isl_assert(map->ctx,do { if (isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out )) break; do { isl_handle_error(map->ctx, isl_error_unknown , "Assertion \"" "isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out)" "\" failed", "/tmp/buildd/llvm-toolchain-snapshot-3.7~svn239931/polly/lib/External/isl/isl_transitive_closure.c" , 2003); goto error; } while (0); } while (0) | |||
2002 | isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out),do { if (isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out )) break; do { isl_handle_error(map->ctx, isl_error_unknown , "Assertion \"" "isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out)" "\" failed", "/tmp/buildd/llvm-toolchain-snapshot-3.7~svn239931/polly/lib/External/isl/isl_transitive_closure.c" , 2003); goto error; } while (0); } while (0) | |||
2003 | goto error)do { if (isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out )) break; do { isl_handle_error(map->ctx, isl_error_unknown , "Assertion \"" "isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out)" "\" failed", "/tmp/buildd/llvm-toolchain-snapshot-3.7~svn239931/polly/lib/External/isl/isl_transitive_closure.c" , 2003); goto error; } while (0); } while (0); | |||
2004 | ||||
2005 | app = construct_power(map, exact, project); | |||
2006 | ||||
2007 | isl_map_free(map); | |||
2008 | return app; | |||
2009 | error: | |||
2010 | isl_map_free(map); | |||
2011 | isl_map_free(app); | |||
2012 | return NULL((void*)0); | |||
2013 | } | |||
2014 | ||||
2015 | /* Compute the positive powers of "map", or an overapproximation. | |||
2016 | * The result maps the exponent to a nested copy of the corresponding power. | |||
2017 | * If the result is exact, then *exact is set to 1. | |||
2018 | * map_power constructs an extended relation with the path lengths | |||
2019 | * encoded as the difference between the final coordinates. | |||
2020 | * In the final step, this difference is equated to an extra parameter | |||
2021 | * and made positive. The extra coordinates are subsequently projected out | |||
2022 | * and the parameter is turned into the domain of the result. | |||
2023 | */ | |||
2024 | __isl_give isl_map *isl_map_power(__isl_take isl_map *map, int *exact) | |||
2025 | { | |||
2026 | isl_space *target_dim; | |||
2027 | isl_space *dim; | |||
2028 | isl_map *diff; | |||
2029 | unsigned d; | |||
2030 | unsigned param; | |||
2031 | ||||
2032 | if (!map) | |||
2033 | return NULL((void*)0); | |||
2034 | ||||
2035 | d = isl_map_dim(map, isl_dim_in); | |||
2036 | param = isl_map_dim(map, isl_dim_param); | |||
2037 | ||||
2038 | map = isl_map_compute_divs(map); | |||
2039 | map = isl_map_coalesce(map); | |||
2040 | ||||
2041 | if (isl_map_plain_is_empty(map)) { | |||
2042 | map = isl_map_from_range(isl_map_wrap(map)); | |||
2043 | map = isl_map_add_dims(map, isl_dim_in, 1); | |||
2044 | map = isl_map_set_dim_name(map, isl_dim_in, 0, "k"); | |||
2045 | return map; | |||
2046 | } | |||
2047 | ||||
2048 | target_dim = isl_map_get_space(map); | |||
2049 | target_dim = isl_space_from_range(isl_space_wrap(target_dim)); | |||
2050 | target_dim = isl_space_add_dims(target_dim, isl_dim_in, 1); | |||
2051 | target_dim = isl_space_set_dim_name(target_dim, isl_dim_in, 0, "k"); | |||
2052 | ||||
2053 | map = map_power(map, exact, 0); | |||
2054 | ||||
2055 | map = isl_map_add_dims(map, isl_dim_param, 1); | |||
2056 | dim = isl_map_get_space(map); | |||
2057 | diff = equate_parameter_to_length(dim, param); | |||
2058 | map = isl_map_intersect(map, diff); | |||
2059 | map = isl_map_project_out(map, isl_dim_in, d, 1); | |||
2060 | map = isl_map_project_out(map, isl_dim_out, d, 1); | |||
2061 | map = isl_map_from_range(isl_map_wrap(map)); | |||
2062 | map = isl_map_move_dims(map, isl_dim_in, 0, isl_dim_param, param, 1); | |||
2063 | ||||
2064 | map = isl_map_reset_space(map, target_dim); | |||
2065 | ||||
2066 | return map; | |||
2067 | } | |||
2068 | ||||
2069 | /* Compute a relation that maps each element in the range of the input | |||
2070 | * relation to the lengths of all paths composed of edges in the input | |||
2071 | * relation that end up in the given range element. | |||
2072 | * The result may be an overapproximation, in which case *exact is set to 0. | |||
2073 | * The resulting relation is very similar to the power relation. | |||
2074 | * The difference are that the domain has been projected out, the | |||
2075 | * range has become the domain and the exponent is the range instead | |||
2076 | * of a parameter. | |||
2077 | */ | |||
2078 | __isl_give isl_map *isl_map_reaching_path_lengths(__isl_take isl_map *map, | |||
2079 | int *exact) | |||
2080 | { | |||
2081 | isl_space *dim; | |||
2082 | isl_map *diff; | |||
2083 | unsigned d; | |||
2084 | unsigned param; | |||
2085 | ||||
2086 | if (!map) | |||
2087 | return NULL((void*)0); | |||
2088 | ||||
2089 | d = isl_map_dim(map, isl_dim_in); | |||
2090 | param = isl_map_dim(map, isl_dim_param); | |||
2091 | ||||
2092 | map = isl_map_compute_divs(map); | |||
2093 | map = isl_map_coalesce(map); | |||
2094 | ||||
2095 | if (isl_map_plain_is_empty(map)) { | |||
2096 | if (exact) | |||
2097 | *exact = 1; | |||
2098 | map = isl_map_project_out(map, isl_dim_out, 0, d); | |||
2099 | map = isl_map_add_dims(map, isl_dim_out, 1); | |||
2100 | return map; | |||
2101 | } | |||
2102 | ||||
2103 | map = map_power(map, exact, 0); | |||
2104 | ||||
2105 | map = isl_map_add_dims(map, isl_dim_param, 1); | |||
2106 | dim = isl_map_get_space(map); | |||
2107 | diff = equate_parameter_to_length(dim, param); | |||
2108 | map = isl_map_intersect(map, diff); | |||
2109 | map = isl_map_project_out(map, isl_dim_in, 0, d + 1); | |||
2110 | map = isl_map_project_out(map, isl_dim_out, d, 1); | |||
2111 | map = isl_map_reverse(map); | |||
2112 | map = isl_map_move_dims(map, isl_dim_out, 0, isl_dim_param, param, 1); | |||
2113 | ||||
2114 | return map; | |||
2115 | } | |||
2116 | ||||
2117 | /* Check whether equality i of bset is a pure stride constraint | |||
2118 | * on a single dimensions, i.e., of the form | |||
2119 | * | |||
2120 | * v = k e | |||
2121 | * | |||
2122 | * with k a constant and e an existentially quantified variable. | |||
2123 | */ | |||
2124 | static int is_eq_stride(__isl_keep isl_basic_setisl_basic_map *bset, int i) | |||
2125 | { | |||
2126 | unsigned nparam; | |||
2127 | unsigned d; | |||
2128 | unsigned n_div; | |||
2129 | int pos1; | |||
2130 | int pos2; | |||
2131 | ||||
2132 | if (!bset) | |||
2133 | return -1; | |||
2134 | ||||
2135 | if (!isl_int_is_zero(bset->eq[i][0])(impz_sgn(bset->eq[i][0]) == 0)) | |||
2136 | return 0; | |||
2137 | ||||
2138 | nparam = isl_basic_set_dim(bset, isl_dim_param); | |||
2139 | d = isl_basic_set_dim(bset, isl_dim_set); | |||
2140 | n_div = isl_basic_set_dim(bset, isl_dim_div); | |||
2141 | ||||
2142 | if (isl_seq_first_non_zero(bset->eq[i] + 1, nparam) != -1) | |||
2143 | return 0; | |||
2144 | pos1 = isl_seq_first_non_zero(bset->eq[i] + 1 + nparam, d); | |||
2145 | if (pos1 == -1) | |||
2146 | return 0; | |||
2147 | if (isl_seq_first_non_zero(bset->eq[i] + 1 + nparam + pos1 + 1, | |||
2148 | d - pos1 - 1) != -1) | |||
2149 | return 0; | |||
2150 | ||||
2151 | pos2 = isl_seq_first_non_zero(bset->eq[i] + 1 + nparam + d, n_div); | |||
2152 | if (pos2 == -1) | |||
2153 | return 0; | |||
2154 | if (isl_seq_first_non_zero(bset->eq[i] + 1 + nparam + d + pos2 + 1, | |||
2155 | n_div - pos2 - 1) != -1) | |||
2156 | return 0; | |||
2157 | if (!isl_int_is_one(bset->eq[i][1 + nparam + pos1])(impz_cmp_si(bset->eq[i][1 + nparam + pos1],1) == 0) && | |||
2158 | !isl_int_is_negone(bset->eq[i][1 + nparam + pos1])(impz_cmp_si(bset->eq[i][1 + nparam + pos1],-1) == 0)) | |||
2159 | return 0; | |||
2160 | ||||
2161 | return 1; | |||
2162 | } | |||
2163 | ||||
2164 | /* Given a map, compute the smallest superset of this map that is of the form | |||
2165 | * | |||
2166 | * { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p } | |||
2167 | * | |||
2168 | * (where p ranges over the (non-parametric) dimensions), | |||
2169 | * compute the transitive closure of this map, i.e., | |||
2170 | * | |||
2171 | * { i -> j : exists k > 0: | |||
2172 | * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } | |||
2173 | * | |||
2174 | * and intersect domain and range of this transitive closure with | |||
2175 | * the given domain and range. | |||
2176 | * | |||
2177 | * If with_id is set, then try to include as much of the identity mapping | |||
2178 | * as possible, by computing | |||
2179 | * | |||
2180 | * { i -> j : exists k >= 0: | |||
2181 | * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } | |||
2182 | * | |||
2183 | * instead (i.e., allow k = 0). | |||
2184 | * | |||
2185 | * In practice, we compute the difference set | |||
2186 | * | |||
2187 | * delta = { j - i | i -> j in map }, | |||
2188 | * | |||
2189 | * look for stride constraint on the individual dimensions and compute | |||
2190 | * (constant) lower and upper bounds for each individual dimension, | |||
2191 | * adding a constraint for each bound not equal to infinity. | |||
2192 | */ | |||
2193 | static __isl_give isl_map *box_closure_on_domain(__isl_take isl_map *map, | |||
2194 | __isl_take isl_setisl_map *dom, __isl_take isl_setisl_map *ran, int with_id) | |||
2195 | { | |||
2196 | int i; | |||
2197 | int k; | |||
2198 | unsigned d; | |||
2199 | unsigned nparam; | |||
2200 | unsigned total; | |||
2201 | isl_space *dim; | |||
2202 | isl_setisl_map *delta; | |||
2203 | isl_map *app = NULL((void*)0); | |||
2204 | isl_basic_setisl_basic_map *aff = NULL((void*)0); | |||
2205 | isl_basic_map *bmap = NULL((void*)0); | |||
2206 | isl_vec *obj = NULL((void*)0); | |||
2207 | isl_int opt; | |||
2208 | ||||
2209 | isl_int_init(opt)opt = mp_int_alloc(); | |||
2210 | ||||
2211 | delta = isl_map_deltas(isl_map_copy(map)); | |||
2212 | ||||
2213 | aff = isl_set_affine_hull(isl_set_copy(delta)); | |||
2214 | if (!aff) | |||
2215 | goto error; | |||
2216 | dim = isl_map_get_space(map); | |||
2217 | d = isl_space_dim(dim, isl_dim_in); | |||
2218 | nparam = isl_space_dim(dim, isl_dim_param); | |||
2219 | total = isl_space_dim(dim, isl_dim_all); | |||
2220 | bmap = isl_basic_map_alloc_space(dim, | |||
2221 | aff->n_div + 1, aff->n_div, 2 * d + 1); | |||
2222 | for (i = 0; i < aff->n_div + 1; ++i) { | |||
2223 | k = isl_basic_map_alloc_div(bmap); | |||
2224 | if (k < 0) | |||
2225 | goto error; | |||
2226 | isl_int_set_si(bmap->div[k][0], 0)impz_set_si(bmap->div[k][0],0); | |||
2227 | } | |||
2228 | for (i = 0; i < aff->n_eq; ++i) { | |||
2229 | if (!is_eq_stride(aff, i)) | |||
2230 | continue; | |||
2231 | k = isl_basic_map_alloc_equality(bmap); | |||
2232 | if (k < 0) | |||
2233 | goto error; | |||
2234 | isl_seq_clr(bmap->eq[k], 1 + nparam); | |||
2235 | isl_seq_cpy(bmap->eq[k] + 1 + nparam + d, | |||
2236 | aff->eq[i] + 1 + nparam, d); | |||
2237 | isl_seq_neg(bmap->eq[k] + 1 + nparam, | |||
2238 | aff->eq[i] + 1 + nparam, d); | |||
2239 | isl_seq_cpy(bmap->eq[k] + 1 + nparam + 2 * d, | |||
2240 | aff->eq[i] + 1 + nparam + d, aff->n_div); | |||
2241 | isl_int_set_si(bmap->eq[k][1 + total + aff->n_div], 0)impz_set_si(bmap->eq[k][1 + total + aff->n_div],0); | |||
2242 | } | |||
2243 | obj = isl_vec_alloc(map->ctx, 1 + nparam + d); | |||
2244 | if (!obj) | |||
2245 | goto error; | |||
2246 | isl_seq_clr(obj->el, 1 + nparam + d); | |||
2247 | for (i = 0; i < d; ++ i) { | |||
2248 | enum isl_lp_result res; | |||
2249 | ||||
2250 | isl_int_set_si(obj->el[1 + nparam + i], 1)impz_set_si(obj->el[1 + nparam + i],1); | |||
2251 | ||||
2252 | res = isl_set_solve_lp(delta, 0, obj->el, map->ctx->one, &opt, | |||
2253 | NULL((void*)0), NULL((void*)0)); | |||
2254 | if (res == isl_lp_error) | |||
2255 | goto error; | |||
2256 | if (res == isl_lp_ok) { | |||
2257 | k = isl_basic_map_alloc_inequality(bmap); | |||
2258 | if (k < 0) | |||
2259 | goto error; | |||
2260 | isl_seq_clr(bmap->ineq[k], | |||
2261 | 1 + nparam + 2 * d + bmap->n_div); | |||
2262 | isl_int_set_si(bmap->ineq[k][1 + nparam + i], -1)impz_set_si(bmap->ineq[k][1 + nparam + i],-1); | |||
2263 | isl_int_set_si(bmap->ineq[k][1 + nparam + d + i], 1)impz_set_si(bmap->ineq[k][1 + nparam + d + i],1); | |||
2264 | isl_int_neg(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div], opt)impz_neg(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div] ,opt); | |||
2265 | } | |||
2266 | ||||
2267 | res = isl_set_solve_lp(delta, 1, obj->el, map->ctx->one, &opt, | |||
2268 | NULL((void*)0), NULL((void*)0)); | |||
2269 | if (res == isl_lp_error) | |||
2270 | goto error; | |||
2271 | if (res == isl_lp_ok) { | |||
2272 | k = isl_basic_map_alloc_inequality(bmap); | |||
2273 | if (k < 0) | |||
2274 | goto error; | |||
2275 | isl_seq_clr(bmap->ineq[k], | |||
2276 | 1 + nparam + 2 * d + bmap->n_div); | |||
2277 | isl_int_set_si(bmap->ineq[k][1 + nparam + i], 1)impz_set_si(bmap->ineq[k][1 + nparam + i],1); | |||
2278 | isl_int_set_si(bmap->ineq[k][1 + nparam + d + i], -1)impz_set_si(bmap->ineq[k][1 + nparam + d + i],-1); | |||
2279 | isl_int_set(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div], opt)impz_set(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div] ,opt); | |||
2280 | } | |||
2281 | ||||
2282 | isl_int_set_si(obj->el[1 + nparam + i], 0)impz_set_si(obj->el[1 + nparam + i],0); | |||
2283 | } | |||
2284 | k = isl_basic_map_alloc_inequality(bmap); | |||
2285 | if (k < 0) | |||
2286 | goto error; | |||
2287 | isl_seq_clr(bmap->ineq[k], | |||
2288 | 1 + nparam + 2 * d + bmap->n_div); | |||
2289 | if (!with_id) | |||
2290 | isl_int_set_si(bmap->ineq[k][0], -1)impz_set_si(bmap->ineq[k][0],-1); | |||
2291 | isl_int_set_si(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div], 1)impz_set_si(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div ],1); | |||
2292 | ||||
2293 | app = isl_map_from_domain_and_range(dom, ran); | |||
2294 | ||||
2295 | isl_vec_free(obj); | |||
2296 | isl_basic_set_free(aff); | |||
2297 | isl_map_free(map); | |||
2298 | bmap = isl_basic_map_finalize(bmap); | |||
2299 | isl_set_free(delta); | |||
2300 | isl_int_clear(opt)mp_int_free(opt); | |||
2301 | ||||
2302 | map = isl_map_from_basic_map(bmap); | |||
2303 | map = isl_map_intersect(map, app); | |||
2304 | ||||
2305 | return map; | |||
2306 | error: | |||
2307 | isl_vec_free(obj); | |||
2308 | isl_basic_map_free(bmap); | |||
2309 | isl_basic_set_free(aff); | |||
2310 | isl_set_free(dom); | |||
2311 | isl_set_free(ran); | |||
2312 | isl_map_free(map); | |||
2313 | isl_set_free(delta); | |||
2314 | isl_int_clear(opt)mp_int_free(opt); | |||
2315 | return NULL((void*)0); | |||
2316 | } | |||
2317 | ||||
2318 | /* Given a map, compute the smallest superset of this map that is of the form | |||
2319 | * | |||
2320 | * { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p } | |||
2321 | * | |||
2322 | * (where p ranges over the (non-parametric) dimensions), | |||
2323 | * compute the transitive closure of this map, i.e., | |||
2324 | * | |||
2325 | * { i -> j : exists k > 0: | |||
2326 | * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } | |||
2327 | * | |||
2328 | * and intersect domain and range of this transitive closure with | |||
2329 | * domain and range of the original map. | |||
2330 | */ | |||
2331 | static __isl_give isl_map *box_closure(__isl_take isl_map *map) | |||
2332 | { | |||
2333 | isl_setisl_map *domain; | |||
2334 | isl_setisl_map *range; | |||
2335 | ||||
2336 | domain = isl_map_domain(isl_map_copy(map)); | |||
2337 | domain = isl_set_coalesce(domain); | |||
2338 | range = isl_map_range(isl_map_copy(map)); | |||
2339 | range = isl_set_coalesce(range); | |||
2340 | ||||
2341 | return box_closure_on_domain(map, domain, range, 0); | |||
2342 | } | |||
2343 | ||||
2344 | /* Given a map, compute the smallest superset of this map that is of the form | |||
2345 | * | |||
2346 | * { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p } | |||
2347 | * | |||
2348 | * (where p ranges over the (non-parametric) dimensions), | |||
2349 | * compute the transitive and partially reflexive closure of this map, i.e., | |||
2350 | * | |||
2351 | * { i -> j : exists k >= 0: | |||
2352 | * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } | |||
2353 | * | |||
2354 | * and intersect domain and range of this transitive closure with | |||
2355 | * the given domain. | |||
2356 | */ | |||
2357 | static __isl_give isl_map *box_closure_with_identity(__isl_take isl_map *map, | |||
2358 | __isl_take isl_setisl_map *dom) | |||
2359 | { | |||
2360 | return box_closure_on_domain(map, dom, isl_set_copy(dom), 1); | |||
2361 | } | |||
2362 | ||||
2363 | /* Check whether app is the transitive closure of map. | |||
2364 | * In particular, check that app is acyclic and, if so, | |||
2365 | * check that | |||
2366 | * | |||
2367 | * app \subset (map \cup (map \circ app)) | |||
2368 | */ | |||
2369 | static int check_exactness_omega(__isl_keep isl_map *map, | |||
2370 | __isl_keep isl_map *app) | |||
2371 | { | |||
2372 | isl_setisl_map *delta; | |||
2373 | int i; | |||
2374 | int is_empty, is_exact; | |||
2375 | unsigned d; | |||
2376 | isl_map *test; | |||
2377 | ||||
2378 | delta = isl_map_deltas(isl_map_copy(app)); | |||
2379 | d = isl_set_dim(delta, isl_dim_set); | |||
2380 | for (i = 0; i < d; ++i) | |||
2381 | delta = isl_set_fix_si(delta, isl_dim_set, i, 0); | |||
2382 | is_empty = isl_set_is_empty(delta); | |||
2383 | isl_set_free(delta); | |||
2384 | if (is_empty < 0) | |||
2385 | return -1; | |||
2386 | if (!is_empty) | |||
2387 | return 0; | |||
2388 | ||||
2389 | test = isl_map_apply_range(isl_map_copy(app), isl_map_copy(map)); | |||
2390 | test = isl_map_union(test, isl_map_copy(map)); | |||
2391 | is_exact = isl_map_is_subset(app, test); | |||
2392 | isl_map_free(test); | |||
2393 | ||||
2394 | return is_exact; | |||
2395 | } | |||
2396 | ||||
2397 | /* Check if basic map M_i can be combined with all the other | |||
2398 | * basic maps such that | |||
2399 | * | |||
2400 | * (\cup_j M_j)^+ | |||
2401 | * | |||
2402 | * can be computed as | |||
2403 | * | |||
2404 | * M_i \cup (\cup_{j \ne i} M_i^* \circ M_j \circ M_i^*)^+ | |||
2405 | * | |||
2406 | * In particular, check if we can compute a compact representation | |||
2407 | * of | |||
2408 | * | |||
2409 | * M_i^* \circ M_j \circ M_i^* | |||
2410 | * | |||
2411 | * for each j != i. | |||
2412 | * Let M_i^? be an extension of M_i^+ that allows paths | |||
2413 | * of length zero, i.e., the result of box_closure(., 1). | |||
2414 | * The criterion, as proposed by Kelly et al., is that | |||
2415 | * id = M_i^? - M_i^+ can be represented as a basic map | |||
2416 | * and that | |||
2417 | * | |||
2418 | * id \circ M_j \circ id = M_j | |||
2419 | * | |||
2420 | * for each j != i. | |||
2421 | * | |||
2422 | * If this function returns 1, then tc and qc are set to | |||
2423 | * M_i^+ and M_i^?, respectively. | |||
2424 | */ | |||
2425 | static int can_be_split_off(__isl_keep isl_map *map, int i, | |||
2426 | __isl_give isl_map **tc, __isl_give isl_map **qc) | |||
2427 | { | |||
2428 | isl_map *map_i, *id = NULL((void*)0); | |||
2429 | int j = -1; | |||
2430 | isl_setisl_map *C; | |||
2431 | ||||
2432 | *tc = NULL((void*)0); | |||
2433 | *qc = NULL((void*)0); | |||
2434 | ||||
2435 | C = isl_set_union(isl_map_domain(isl_map_copy(map)), | |||
2436 | isl_map_range(isl_map_copy(map))); | |||
2437 | C = isl_set_from_basic_set(isl_set_simple_hull(C)); | |||
2438 | if (!C) | |||
2439 | goto error; | |||
2440 | ||||
2441 | map_i = isl_map_from_basic_map(isl_basic_map_copy(map->p[i])); | |||
2442 | *tc = box_closure(isl_map_copy(map_i)); | |||
2443 | *qc = box_closure_with_identity(map_i, C); | |||
2444 | id = isl_map_subtract(isl_map_copy(*qc), isl_map_copy(*tc)); | |||
2445 | ||||
2446 | if (!id || !*qc) | |||
2447 | goto error; | |||
2448 | if (id->n != 1 || (*qc)->n != 1) | |||
2449 | goto done; | |||
2450 | ||||
2451 | for (j = 0; j < map->n; ++j) { | |||
2452 | isl_map *map_j, *test; | |||
2453 | int is_ok; | |||
2454 | ||||
2455 | if (i == j) | |||
2456 | continue; | |||
2457 | map_j = isl_map_from_basic_map( | |||
2458 | isl_basic_map_copy(map->p[j])); | |||
2459 | test = isl_map_apply_range(isl_map_copy(id), | |||
2460 | isl_map_copy(map_j)); | |||
2461 | test = isl_map_apply_range(test, isl_map_copy(id)); | |||
2462 | is_ok = isl_map_is_equal(test, map_j); | |||
2463 | isl_map_free(map_j); | |||
2464 | isl_map_free(test); | |||
2465 | if (is_ok < 0) | |||
2466 | goto error; | |||
2467 | if (!is_ok) | |||
2468 | break; | |||
2469 | } | |||
2470 | ||||
2471 | done: | |||
2472 | isl_map_free(id); | |||
2473 | if (j == map->n) | |||
2474 | return 1; | |||
2475 | ||||
2476 | isl_map_free(*qc); | |||
2477 | isl_map_free(*tc); | |||
2478 | *qc = NULL((void*)0); | |||
2479 | *tc = NULL((void*)0); | |||
2480 | ||||
2481 | return 0; | |||
2482 | error: | |||
2483 | isl_map_free(id); | |||
2484 | isl_map_free(*qc); | |||
2485 | isl_map_free(*tc); | |||
2486 | *qc = NULL((void*)0); | |||
2487 | *tc = NULL((void*)0); | |||
2488 | return -1; | |||
2489 | } | |||
2490 | ||||
2491 | static __isl_give isl_map *box_closure_with_check(__isl_take isl_map *map, | |||
2492 | int *exact) | |||
2493 | { | |||
2494 | isl_map *app; | |||
2495 | ||||
2496 | app = box_closure(isl_map_copy(map)); | |||
2497 | if (exact) | |||
2498 | *exact = check_exactness_omega(map, app); | |||
2499 | ||||
2500 | isl_map_free(map); | |||
2501 | return app; | |||
2502 | } | |||
2503 | ||||
2504 | /* Compute an overapproximation of the transitive closure of "map" | |||
2505 | * using a variation of the algorithm from | |||
2506 | * "Transitive Closure of Infinite Graphs and its Applications" | |||
2507 | * by Kelly et al. | |||
2508 | * | |||
2509 | * We first check whether we can can split of any basic map M_i and | |||
2510 | * compute | |||
2511 | * | |||
2512 | * (\cup_j M_j)^+ | |||
2513 | * | |||
2514 | * as | |||
2515 | * | |||
2516 | * M_i \cup (\cup_{j \ne i} M_i^* \circ M_j \circ M_i^*)^+ | |||
2517 | * | |||
2518 | * using a recursive call on the remaining map. | |||
2519 | * | |||
2520 | * If not, we simply call box_closure on the whole map. | |||
2521 | */ | |||
2522 | static __isl_give isl_map *transitive_closure_omega(__isl_take isl_map *map, | |||
2523 | int *exact) | |||
2524 | { | |||
2525 | int i, j; | |||
2526 | int exact_i; | |||
2527 | isl_map *app; | |||
2528 | ||||
2529 | if (!map) | |||
2530 | return NULL((void*)0); | |||
2531 | if (map->n == 1) | |||
2532 | return box_closure_with_check(map, exact); | |||
2533 | ||||
2534 | for (i = 0; i < map->n; ++i) { | |||
2535 | int ok; | |||
2536 | isl_map *qc, *tc; | |||
2537 | ok = can_be_split_off(map, i, &tc, &qc); | |||
2538 | if (ok < 0) | |||
2539 | goto error; | |||
2540 | if (!ok) | |||
2541 | continue; | |||
2542 | ||||
2543 | app = isl_map_alloc_space(isl_map_get_space(map), map->n - 1, 0); | |||
2544 | ||||
2545 | for (j = 0; j < map->n; ++j) { | |||
2546 | if (j == i) | |||
2547 | continue; | |||
2548 | app = isl_map_add_basic_map(app, | |||
2549 | isl_basic_map_copy(map->p[j])); | |||
2550 | } | |||
2551 | ||||
2552 | app = isl_map_apply_range(isl_map_copy(qc), app); | |||
2553 | app = isl_map_apply_range(app, qc); | |||
2554 | ||||
2555 | app = isl_map_union(tc, transitive_closure_omega(app, NULL((void*)0))); | |||
2556 | exact_i = check_exactness_omega(map, app); | |||
2557 | if (exact_i == 1) { | |||
2558 | if (exact) | |||
2559 | *exact = exact_i; | |||
2560 | isl_map_free(map); | |||
2561 | return app; | |||
2562 | } | |||
2563 | isl_map_free(app); | |||
2564 | if (exact_i < 0) | |||
2565 | goto error; | |||
2566 | } | |||
2567 | ||||
2568 | return box_closure_with_check(map, exact); | |||
2569 | error: | |||
2570 | isl_map_free(map); | |||
2571 | return NULL((void*)0); | |||
2572 | } | |||
2573 | ||||
2574 | /* Compute the transitive closure of "map", or an overapproximation. | |||
2575 | * If the result is exact, then *exact is set to 1. | |||
2576 | * Simply use map_power to compute the powers of map, but tell | |||
2577 | * it to project out the lengths of the paths instead of equating | |||
2578 | * the length to a parameter. | |||
2579 | */ | |||
2580 | __isl_give isl_map *isl_map_transitive_closure(__isl_take isl_map *map, | |||
2581 | int *exact) | |||
2582 | { | |||
2583 | isl_space *target_dim; | |||
2584 | int closed; | |||
2585 | ||||
2586 | if (!map) | |||
2587 | goto error; | |||
2588 | ||||
2589 | if (map->ctx->opt->closure == ISL_CLOSURE_BOX1) | |||
2590 | return transitive_closure_omega(map, exact); | |||
2591 | ||||
2592 | map = isl_map_compute_divs(map); | |||
2593 | map = isl_map_coalesce(map); | |||
2594 | closed = isl_map_is_transitively_closed(map); | |||
2595 | if (closed < 0) | |||
2596 | goto error; | |||
2597 | if (closed) { | |||
2598 | if (exact) | |||
2599 | *exact = 1; | |||
2600 | return map; | |||
2601 | } | |||
2602 | ||||
2603 | target_dim = isl_map_get_space(map); | |||
2604 | map = map_power(map, exact, 1); | |||
2605 | map = isl_map_reset_space(map, target_dim); | |||
2606 | ||||
2607 | return map; | |||
2608 | error: | |||
2609 | isl_map_free(map); | |||
2610 | return NULL((void*)0); | |||
2611 | } | |||
2612 | ||||
2613 | static isl_stat inc_count(__isl_take isl_map *map, void *user) | |||
2614 | { | |||
2615 | int *n = user; | |||
2616 | ||||
2617 | *n += map->n; | |||
2618 | ||||
2619 | isl_map_free(map); | |||
2620 | ||||
2621 | return isl_stat_ok; | |||
2622 | } | |||
2623 | ||||
2624 | static isl_stat collect_basic_map(__isl_take isl_map *map, void *user) | |||
2625 | { | |||
2626 | int i; | |||
2627 | isl_basic_map ***next = user; | |||
2628 | ||||
2629 | for (i = 0; i < map->n; ++i) { | |||
2630 | **next = isl_basic_map_copy(map->p[i]); | |||
2631 | if (!**next) | |||
2632 | goto error; | |||
2633 | (*next)++; | |||
2634 | } | |||
2635 | ||||
2636 | isl_map_free(map); | |||
2637 | return isl_stat_ok; | |||
2638 | error: | |||
2639 | isl_map_free(map); | |||
2640 | return isl_stat_error; | |||
2641 | } | |||
2642 | ||||
2643 | /* Perform Floyd-Warshall on the given list of basic relations. | |||
2644 | * The basic relations may live in different dimensions, | |||
2645 | * but basic relations that get assigned to the diagonal of the | |||
2646 | * grid have domains and ranges of the same dimension and so | |||
2647 | * the standard algorithm can be used because the nested transitive | |||
2648 | * closures are only applied to diagonal elements and because all | |||
2649 | * compositions are peformed on relations with compatible domains and ranges. | |||
2650 | */ | |||
2651 | static __isl_give isl_union_map *union_floyd_warshall_on_list(isl_ctx *ctx, | |||
2652 | __isl_keep isl_basic_map **list, int n, int *exact) | |||
2653 | { | |||
2654 | int i, j, k; | |||
2655 | int n_group; | |||
2656 | int *group = NULL((void*)0); | |||
2657 | isl_setisl_map **set = NULL((void*)0); | |||
2658 | isl_map ***grid = NULL((void*)0); | |||
2659 | isl_union_map *app; | |||
2660 | ||||
2661 | group = setup_groups(ctx, list, n, &set, &n_group); | |||
2662 | if (!group) | |||
2663 | goto error; | |||
2664 | ||||
2665 | grid = isl_calloc_array(ctx, isl_map **, n_group)((isl_map ** *)isl_calloc_or_die(ctx, n_group, sizeof(isl_map **))); | |||
2666 | if (!grid) | |||
2667 | goto error; | |||
2668 | for (i = 0; i < n_group; ++i) { | |||
2669 | grid[i] = isl_calloc_array(ctx, isl_map *, n_group)((isl_map * *)isl_calloc_or_die(ctx, n_group, sizeof(isl_map * ))); | |||
2670 | if (!grid[i]) | |||
2671 | goto error; | |||
2672 | for (j = 0; j < n_group; ++j) { | |||
2673 | isl_space *dim1, *dim2, *dim; | |||
2674 | dim1 = isl_space_reverse(isl_set_get_space(set[i])); | |||
2675 | dim2 = isl_set_get_space(set[j]); | |||
2676 | dim = isl_space_join(dim1, dim2); | |||
2677 | grid[i][j] = isl_map_empty(dim); | |||
2678 | } | |||
2679 | } | |||
2680 | ||||
2681 | for (k = 0; k < n; ++k) { | |||
2682 | i = group[2 * k]; | |||
2683 | j = group[2 * k + 1]; | |||
2684 | grid[i][j] = isl_map_union(grid[i][j], | |||
2685 | isl_map_from_basic_map( | |||
2686 | isl_basic_map_copy(list[k]))); | |||
2687 | } | |||
2688 | ||||
2689 | floyd_warshall_iterate(grid, n_group, exact); | |||
2690 | ||||
2691 | app = isl_union_map_empty(isl_map_get_space(grid[0][0])); | |||
2692 | ||||
2693 | for (i = 0; i < n_group; ++i) { | |||
2694 | for (j = 0; j < n_group; ++j) | |||
2695 | app = isl_union_map_add_map(app, grid[i][j]); | |||
2696 | free(grid[i]); | |||
2697 | } | |||
2698 | free(grid); | |||
2699 | ||||
2700 | for (i = 0; i < 2 * n; ++i) | |||
2701 | isl_set_free(set[i]); | |||
2702 | free(set); | |||
2703 | ||||
2704 | free(group); | |||
2705 | return app; | |||
2706 | error: | |||
2707 | if (grid) | |||
2708 | for (i = 0; i < n_group; ++i) { | |||
2709 | if (!grid[i]) | |||
2710 | continue; | |||
2711 | for (j = 0; j < n_group; ++j) | |||
2712 | isl_map_free(grid[i][j]); | |||
2713 | free(grid[i]); | |||
2714 | } | |||
2715 | free(grid); | |||
2716 | if (set) { | |||
2717 | for (i = 0; i < 2 * n; ++i) | |||
2718 | isl_set_free(set[i]); | |||
2719 | free(set); | |||
2720 | } | |||
2721 | free(group); | |||
2722 | return NULL((void*)0); | |||
2723 | } | |||
2724 | ||||
2725 | /* Perform Floyd-Warshall on the given union relation. | |||
2726 | * The implementation is very similar to that for non-unions. | |||
2727 | * The main difference is that it is applied unconditionally. | |||
2728 | * We first extract a list of basic maps from the union map | |||
2729 | * and then perform the algorithm on this list. | |||
2730 | */ | |||
2731 | static __isl_give isl_union_map *union_floyd_warshall( | |||
2732 | __isl_take isl_union_map *umap, int *exact) | |||
2733 | { | |||
2734 | int i, n; | |||
2735 | isl_ctx *ctx; | |||
2736 | isl_basic_map **list = NULL((void*)0); | |||
2737 | isl_basic_map **next; | |||
2738 | isl_union_map *res; | |||
2739 | ||||
2740 | n = 0; | |||
2741 | if (isl_union_map_foreach_map(umap, inc_count, &n) < 0) | |||
2742 | goto error; | |||
2743 | ||||
2744 | ctx = isl_union_map_get_ctx(umap); | |||
2745 | list = isl_calloc_array(ctx, isl_basic_map *, n)((isl_basic_map * *)isl_calloc_or_die(ctx, n, sizeof(isl_basic_map *))); | |||
2746 | if (!list) | |||
2747 | goto error; | |||
2748 | ||||
2749 | next = list; | |||
2750 | if (isl_union_map_foreach_map(umap, collect_basic_map, &next) < 0) | |||
2751 | goto error; | |||
2752 | ||||
2753 | res = union_floyd_warshall_on_list(ctx, list, n, exact); | |||
2754 | ||||
2755 | if (list) { | |||
2756 | for (i = 0; i < n; ++i) | |||
2757 | isl_basic_map_free(list[i]); | |||
2758 | free(list); | |||
2759 | } | |||
2760 | ||||
2761 | isl_union_map_free(umap); | |||
2762 | return res; | |||
2763 | error: | |||
2764 | if (list) { | |||
2765 | for (i = 0; i < n; ++i) | |||
2766 | isl_basic_map_free(list[i]); | |||
2767 | free(list); | |||
2768 | } | |||
2769 | isl_union_map_free(umap); | |||
2770 | return NULL((void*)0); | |||
2771 | } | |||
2772 | ||||
2773 | /* Decompose the give union relation into strongly connected components. | |||
2774 | * The implementation is essentially the same as that of | |||
2775 | * construct_power_components with the major difference that all | |||
2776 | * operations are performed on union maps. | |||
2777 | */ | |||
2778 | static __isl_give isl_union_map *union_components( | |||
2779 | __isl_take isl_union_map *umap, int *exact) | |||
2780 | { | |||
2781 | int i; | |||
2782 | int n; | |||
2783 | isl_ctx *ctx; | |||
2784 | isl_basic_map **list = NULL((void*)0); | |||
2785 | isl_basic_map **next; | |||
2786 | isl_union_map *path = NULL((void*)0); | |||
2787 | struct isl_tc_follows_data data; | |||
2788 | struct isl_tarjan_graph *g = NULL((void*)0); | |||
2789 | int c, l; | |||
2790 | int recheck = 0; | |||
2791 | ||||
2792 | n = 0; | |||
2793 | if (isl_union_map_foreach_map(umap, inc_count, &n) < 0) | |||
| ||||
2794 | goto error; | |||
2795 | ||||
2796 | if (n == 0) | |||
2797 | return umap; | |||
2798 | if (n <= 1) | |||
2799 | return union_floyd_warshall(umap, exact); | |||
2800 | ||||
2801 | ctx = isl_union_map_get_ctx(umap); | |||
2802 | list = isl_calloc_array(ctx, isl_basic_map *, n)((isl_basic_map * *)isl_calloc_or_die(ctx, n, sizeof(isl_basic_map *))); | |||
2803 | if (!list) | |||
2804 | goto error; | |||
2805 | ||||
2806 | next = list; | |||
2807 | if (isl_union_map_foreach_map(umap, collect_basic_map, &next) < 0) | |||
2808 | goto error; | |||
2809 | ||||
2810 | data.list = list; | |||
2811 | data.check_closed = 0; | |||
2812 | g = isl_tarjan_graph_init(ctx, n, &basic_map_follows, &data); | |||
2813 | if (!g) | |||
2814 | goto error; | |||
2815 | ||||
2816 | c = 0; | |||
2817 | i = 0; | |||
2818 | l = n; | |||
2819 | path = isl_union_map_empty(isl_union_map_get_space(umap)); | |||
2820 | while (l) { | |||
2821 | isl_union_map *comp; | |||
2822 | isl_union_map *path_comp, *path_comb; | |||
2823 | comp = isl_union_map_empty(isl_union_map_get_space(umap)); | |||
2824 | while (g->order[i] != -1) { | |||
2825 | comp = isl_union_map_add_map(comp, | |||
2826 | isl_map_from_basic_map( | |||
2827 | isl_basic_map_copy(list[g->order[i]]))); | |||
2828 | --l; | |||
2829 | ++i; | |||
2830 | } | |||
2831 | path_comp = union_floyd_warshall(comp, exact); | |||
2832 | path_comb = isl_union_map_apply_range(isl_union_map_copy(path), | |||
2833 | isl_union_map_copy(path_comp)); | |||
2834 | path = isl_union_map_union(path, path_comp); | |||
2835 | path = isl_union_map_union(path, path_comb); | |||
2836 | ++i; | |||
2837 | ++c; | |||
2838 | } | |||
2839 | ||||
2840 | if (c > 1 && data.check_closed && !*exact) { | |||
2841 | int closed; | |||
2842 | ||||
2843 | closed = isl_union_map_is_transitively_closed(path); | |||
2844 | if (closed < 0) | |||
2845 | goto error; | |||
2846 | recheck = !closed; | |||
2847 | } | |||
2848 | ||||
2849 | isl_tarjan_graph_free(g); | |||
2850 | ||||
2851 | for (i = 0; i < n; ++i) | |||
2852 | isl_basic_map_free(list[i]); | |||
2853 | free(list); | |||
2854 | ||||
2855 | if (recheck) { | |||
2856 | isl_union_map_free(path); | |||
2857 | return union_floyd_warshall(umap, exact); | |||
2858 | } | |||
2859 | ||||
2860 | isl_union_map_free(umap); | |||
2861 | ||||
2862 | return path; | |||
2863 | error: | |||
2864 | isl_tarjan_graph_free(g); | |||
2865 | if (list) { | |||
2866 | for (i = 0; i < n; ++i) | |||
2867 | isl_basic_map_free(list[i]); | |||
2868 | free(list); | |||
2869 | } | |||
2870 | isl_union_map_free(umap); | |||
2871 | isl_union_map_free(path); | |||
2872 | return NULL((void*)0); | |||
2873 | } | |||
2874 | ||||
2875 | /* Compute the transitive closure of "umap", or an overapproximation. | |||
2876 | * If the result is exact, then *exact is set to 1. | |||
2877 | */ | |||
2878 | __isl_give isl_union_map *isl_union_map_transitive_closure( | |||
2879 | __isl_take isl_union_map *umap, int *exact) | |||
2880 | { | |||
2881 | int closed; | |||
2882 | ||||
2883 | if (!umap) | |||
2884 | return NULL((void*)0); | |||
2885 | ||||
2886 | if (exact) | |||
2887 | *exact = 1; | |||
2888 | ||||
2889 | umap = isl_union_map_compute_divs(umap); | |||
2890 | umap = isl_union_map_coalesce(umap); | |||
2891 | closed = isl_union_map_is_transitively_closed(umap); | |||
2892 | if (closed < 0) | |||
2893 | goto error; | |||
2894 | if (closed) | |||
2895 | return umap; | |||
2896 | umap = union_components(umap, exact); | |||
2897 | return umap; | |||
2898 | error: | |||
2899 | isl_union_map_free(umap); | |||
2900 | return NULL((void*)0); | |||
2901 | } | |||
2902 | ||||
2903 | struct isl_union_power { | |||
2904 | isl_union_map *pow; | |||
2905 | int *exact; | |||
2906 | }; | |||
2907 | ||||
2908 | static isl_stat power(__isl_take isl_map *map, void *user) | |||
2909 | { | |||
2910 | struct isl_union_power *up = user; | |||
2911 | ||||
2912 | map = isl_map_power(map, up->exact); | |||
2913 | up->pow = isl_union_map_from_map(map); | |||
2914 | ||||
2915 | return isl_stat_error; | |||
2916 | } | |||
2917 | ||||
2918 | /* Construct a map [x] -> [x+1], with parameters prescribed by "dim". | |||
2919 | */ | |||
2920 | static __isl_give isl_union_map *increment(__isl_take isl_space *dim) | |||
2921 | { | |||
2922 | int k; | |||
2923 | isl_basic_map *bmap; | |||
2924 | ||||
2925 | dim = isl_space_add_dims(dim, isl_dim_in, 1); | |||
2926 | dim = isl_space_add_dims(dim, isl_dim_out, 1); | |||
2927 | bmap = isl_basic_map_alloc_space(dim, 0, 1, 0); | |||
2928 | k = isl_basic_map_alloc_equality(bmap); | |||
2929 | if (k < 0) | |||
2930 | goto error; | |||
2931 | isl_seq_clr(bmap->eq[k], isl_basic_map_total_dim(bmap)); | |||
2932 | isl_int_set_si(bmap->eq[k][0], 1)impz_set_si(bmap->eq[k][0],1); | |||
2933 | isl_int_set_si(bmap->eq[k][isl_basic_map_offset(bmap, isl_dim_in)], 1)impz_set_si(bmap->eq[k][isl_basic_map_offset(bmap, isl_dim_in )],1); | |||
2934 | isl_int_set_si(bmap->eq[k][isl_basic_map_offset(bmap, isl_dim_out)], -1)impz_set_si(bmap->eq[k][isl_basic_map_offset(bmap, isl_dim_out )],-1); | |||
2935 | return isl_union_map_from_map(isl_map_from_basic_map(bmap)); | |||
2936 | error: | |||
2937 | isl_basic_map_free(bmap); | |||
2938 | return NULL((void*)0); | |||
2939 | } | |||
2940 | ||||
2941 | /* Construct a map [[x]->[y]] -> [y-x], with parameters prescribed by "dim". | |||
2942 | */ | |||
2943 | static __isl_give isl_union_map *deltas_map(__isl_take isl_space *dim) | |||
2944 | { | |||
2945 | isl_basic_map *bmap; | |||
2946 | ||||
2947 | dim = isl_space_add_dims(dim, isl_dim_in, 1); | |||
2948 | dim = isl_space_add_dims(dim, isl_dim_out, 1); | |||
2949 | bmap = isl_basic_map_universe(dim); | |||
2950 | bmap = isl_basic_map_deltas_map(bmap); | |||
2951 | ||||
2952 | return isl_union_map_from_map(isl_map_from_basic_map(bmap)); | |||
2953 | } | |||
2954 | ||||
2955 | /* Compute the positive powers of "map", or an overapproximation. | |||
2956 | * The result maps the exponent to a nested copy of the corresponding power. | |||
2957 | * If the result is exact, then *exact is set to 1. | |||
2958 | */ | |||
2959 | __isl_give isl_union_map *isl_union_map_power(__isl_take isl_union_map *umap, | |||
2960 | int *exact) | |||
2961 | { | |||
2962 | int n; | |||
2963 | isl_union_map *inc; | |||
2964 | isl_union_map *dm; | |||
2965 | ||||
2966 | if (!umap) | |||
2967 | return NULL((void*)0); | |||
2968 | n = isl_union_map_n_map(umap); | |||
2969 | if (n == 0) | |||
2970 | return umap; | |||
2971 | if (n == 1) { | |||
2972 | struct isl_union_power up = { NULL((void*)0), exact }; | |||
2973 | isl_union_map_foreach_map(umap, &power, &up); | |||
2974 | isl_union_map_free(umap); | |||
2975 | return up.pow; | |||
2976 | } | |||
2977 | inc = increment(isl_union_map_get_space(umap)); | |||
2978 | umap = isl_union_map_product(inc, umap); | |||
2979 | umap = isl_union_map_transitive_closure(umap, exact); | |||
2980 | umap = isl_union_map_zip(umap); | |||
2981 | dm = deltas_map(isl_union_map_get_space(umap)); | |||
2982 | umap = isl_union_map_apply_domain(umap, dm); | |||
2983 | ||||
2984 | return umap; | |||
2985 | } | |||
2986 | ||||
2987 | #undef TYPEisl_union_map | |||
2988 | #define TYPEisl_union_map isl_map | |||
2989 | #include "isl_power_templ.c" | |||
2990 | ||||
2991 | #undef TYPEisl_union_map | |||
2992 | #define TYPEisl_union_map isl_union_map | |||
2993 | #include "isl_power_templ.c" |