isl_tab_rollback: avoid double free on error path
[platform/upstream/isl.git] / isl_transitive_closure.c
1 /*
2  * Copyright 2010      INRIA Saclay
3  *
4  * Use of this software is governed by the GNU LGPLv2.1 license
5  *
6  * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
7  * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
8  * 91893 Orsay, France 
9  */
10
11 #include "isl_map.h"
12 #include "isl_map_private.h"
13 #include "isl_seq.h"
14 #include <isl_lp.h>
15
16 int isl_map_is_transitively_closed(__isl_keep isl_map *map)
17 {
18         isl_map *map2;
19         int closed;
20
21         map2 = isl_map_apply_range(isl_map_copy(map), isl_map_copy(map));
22         closed = isl_map_is_subset(map2, map);
23         isl_map_free(map2);
24
25         return closed;
26 }
27  
28 /* Given a map that represents a path with the length of the path
29  * encoded as the difference between the last output coordindate
30  * and the last input coordinate, set this length to either
31  * exactly "length" (if "exactly" is set) or at least "length"
32  * (if "exactly" is not set).
33  */
34 static __isl_give isl_map *set_path_length(__isl_take isl_map *map,
35         int exactly, int length)
36 {
37         struct isl_dim *dim;
38         struct isl_basic_map *bmap;
39         unsigned d;
40         unsigned nparam;
41         int k;
42         isl_int *c;
43
44         if (!map)
45                 return NULL;
46
47         dim = isl_map_get_dim(map);
48         d = isl_dim_size(dim, isl_dim_in);
49         nparam = isl_dim_size(dim, isl_dim_param);
50         bmap = isl_basic_map_alloc_dim(dim, 0, 1, 1);
51         if (exactly) {
52                 k = isl_basic_map_alloc_equality(bmap);
53                 c = bmap->eq[k];
54         } else {
55                 k = isl_basic_map_alloc_inequality(bmap);
56                 c = bmap->ineq[k];
57         }
58         if (k < 0)
59                 goto error;
60         isl_seq_clr(c, 1 + isl_basic_map_total_dim(bmap));
61         isl_int_set_si(c[0], -length);
62         isl_int_set_si(c[1 + nparam + d - 1], -1);
63         isl_int_set_si(c[1 + nparam + d + d - 1], 1);
64
65         bmap = isl_basic_map_finalize(bmap);
66         map = isl_map_intersect(map, isl_map_from_basic_map(bmap));
67
68         return map;
69 error:
70         isl_basic_map_free(bmap);
71         isl_map_free(map);
72         return NULL;
73 }
74
75 /* Check whether the overapproximation of the power of "map" is exactly
76  * the power of "map".  Let R be "map" and A_k the overapproximation.
77  * The approximation is exact if
78  *
79  *      A_1 = R
80  *      A_k = A_{k-1} \circ R                   k >= 2
81  *
82  * Since A_k is known to be an overapproximation, we only need to check
83  *
84  *      A_1 \subset R
85  *      A_k \subset A_{k-1} \circ R             k >= 2
86  *
87  * In practice, "app" has an extra input and output coordinate
88  * to encode the length of the path.  So, we first need to add
89  * this coordinate to "map" and set the length of the path to
90  * one.
91  */
92 static int check_power_exactness(__isl_take isl_map *map,
93         __isl_take isl_map *app)
94 {
95         int exact;
96         isl_map *app_1;
97         isl_map *app_2;
98
99         map = isl_map_add(map, isl_dim_in, 1);
100         map = isl_map_add(map, isl_dim_out, 1);
101         map = set_path_length(map, 1, 1);
102
103         app_1 = set_path_length(isl_map_copy(app), 1, 1);
104
105         exact = isl_map_is_subset(app_1, map);
106         isl_map_free(app_1);
107
108         if (!exact || exact < 0) {
109                 isl_map_free(app);
110                 isl_map_free(map);
111                 return exact;
112         }
113
114         app_1 = set_path_length(isl_map_copy(app), 0, 1);
115         app_2 = set_path_length(app, 0, 2);
116         app_1 = isl_map_apply_range(map, app_1);
117
118         exact = isl_map_is_subset(app_2, app_1);
119
120         isl_map_free(app_1);
121         isl_map_free(app_2);
122
123         return exact;
124 }
125
126 /* Check whether the overapproximation of the power of "map" is exactly
127  * the power of "map", possibly after projecting out the power (if "project"
128  * is set).
129  *
130  * If "project" is set and if "steps" can only result in acyclic paths,
131  * then we check
132  *
133  *      A = R \cup (A \circ R)
134  *
135  * where A is the overapproximation with the power projected out, i.e.,
136  * an overapproximation of the transitive closure.
137  * More specifically, since A is known to be an overapproximation, we check
138  *
139  *      A \subset R \cup (A \circ R)
140  *
141  * Otherwise, we check if the power is exact.
142  *
143  * Note that "app" has an extra input and output coordinate to encode
144  * the length of the part.  If we are only interested in the transitive
145  * closure, then we can simply project out these coordinates first.
146  */
147 static int check_exactness(__isl_take isl_map *map, __isl_take isl_map *app,
148         int project)
149 {
150         isl_map *test;
151         int exact;
152         unsigned d;
153
154         if (!project)
155                 return check_power_exactness(map, app);
156
157         d = isl_map_dim(map, isl_dim_in);
158         app = set_path_length(app, 0, 1);
159         app = isl_map_project_out(app, isl_dim_in, d, 1);
160         app = isl_map_project_out(app, isl_dim_out, d, 1);
161
162         test = isl_map_apply_range(isl_map_copy(map), isl_map_copy(app));
163         test = isl_map_union(test, isl_map_copy(map));
164
165         exact = isl_map_is_subset(app, test);
166
167         isl_map_free(app);
168         isl_map_free(test);
169
170         isl_map_free(map);
171
172         return exact;
173 }
174
175 /*
176  * The transitive closure implementation is based on the paper
177  * "Computing the Transitive Closure of a Union of Affine Integer
178  * Tuple Relations" by Anna Beletska, Denis Barthou, Wlodzimierz Bielecki and
179  * Albert Cohen.
180  */
181
182 /* Given a set of n offsets v_i (the rows of "steps"), construct a relation
183  * of the given dimension specification (Z^{n+1} -> Z^{n+1})
184  * that maps an element x to any element that can be reached
185  * by taking a non-negative number of steps along any of
186  * the extended offsets v'_i = [v_i 1].
187  * That is, construct
188  *
189  * { [x] -> [y] : exists k_i >= 0, y = x + \sum_i k_i v'_i }
190  *
191  * For any element in this relation, the number of steps taken
192  * is equal to the difference in the final coordinates.
193  */
194 static __isl_give isl_map *path_along_steps(__isl_take isl_dim *dim,
195         __isl_keep isl_mat *steps)
196 {
197         int i, j, k;
198         struct isl_basic_map *path = NULL;
199         unsigned d;
200         unsigned n;
201         unsigned nparam;
202
203         if (!dim || !steps)
204                 goto error;
205
206         d = isl_dim_size(dim, isl_dim_in);
207         n = steps->n_row;
208         nparam = isl_dim_size(dim, isl_dim_param);
209
210         path = isl_basic_map_alloc_dim(isl_dim_copy(dim), n, d, n);
211
212         for (i = 0; i < n; ++i) {
213                 k = isl_basic_map_alloc_div(path);
214                 if (k < 0)
215                         goto error;
216                 isl_assert(steps->ctx, i == k, goto error);
217                 isl_int_set_si(path->div[k][0], 0);
218         }
219
220         for (i = 0; i < d; ++i) {
221                 k = isl_basic_map_alloc_equality(path);
222                 if (k < 0)
223                         goto error;
224                 isl_seq_clr(path->eq[k], 1 + isl_basic_map_total_dim(path));
225                 isl_int_set_si(path->eq[k][1 + nparam + i], 1);
226                 isl_int_set_si(path->eq[k][1 + nparam + d + i], -1);
227                 if (i == d - 1)
228                         for (j = 0; j < n; ++j)
229                                 isl_int_set_si(path->eq[k][1 + nparam + 2 * d + j], 1);
230                 else
231                         for (j = 0; j < n; ++j)
232                                 isl_int_set(path->eq[k][1 + nparam + 2 * d + j],
233                                             steps->row[j][i]);
234         }
235
236         for (i = 0; i < n; ++i) {
237                 k = isl_basic_map_alloc_inequality(path);
238                 if (k < 0)
239                         goto error;
240                 isl_seq_clr(path->ineq[k], 1 + isl_basic_map_total_dim(path));
241                 isl_int_set_si(path->ineq[k][1 + nparam + 2 * d + i], 1);
242         }
243
244         isl_dim_free(dim);
245
246         path = isl_basic_map_simplify(path);
247         path = isl_basic_map_finalize(path);
248         return isl_map_from_basic_map(path);
249 error:
250         isl_dim_free(dim);
251         isl_basic_map_free(path);
252         return NULL;
253 }
254
255 #define IMPURE          0
256 #define PURE_PARAM      1
257 #define PURE_VAR        2
258 #define MIXED           3
259
260 /* Check whether the parametric constant term of constraint c is never
261  * positive in "bset".
262  */
263 static int parametric_constant_never_positive(__isl_keep isl_basic_set *bset,
264         isl_int *c, int *div_purity)
265 {
266         unsigned d;
267         unsigned n_div;
268         unsigned nparam;
269         int i;
270         int k;
271         int empty;
272
273         n_div = isl_basic_set_dim(bset, isl_dim_div);
274         d = isl_basic_set_dim(bset, isl_dim_set);
275         nparam = isl_basic_set_dim(bset, isl_dim_param);
276
277         bset = isl_basic_set_copy(bset);
278         bset = isl_basic_set_cow(bset);
279         bset = isl_basic_set_extend_constraints(bset, 0, 1);
280         k = isl_basic_set_alloc_inequality(bset);
281         if (k < 0)
282                 goto error;
283         isl_seq_clr(bset->ineq[k], 1 + isl_basic_set_total_dim(bset));
284         isl_seq_cpy(bset->ineq[k], c, 1 + nparam);
285         for (i = 0; i < n_div; ++i) {
286                 if (div_purity[i] != PURE_PARAM)
287                         continue;
288                 isl_int_set(bset->ineq[k][1 + nparam + d + i],
289                             c[1 + nparam + d + i]);
290         }
291         isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
292         empty = isl_basic_set_is_empty(bset);
293         isl_basic_set_free(bset);
294
295         return empty;
296 error:
297         isl_basic_set_free(bset);
298         return -1;
299 }
300
301 /* Return PURE_PARAM if only the coefficients of the parameters are non-zero.
302  * Return PURE_VAR if only the coefficients of the set variables are non-zero.
303  * Return MIXED if only the coefficients of the parameters and the set
304  *      variables are non-zero and if moreover the parametric constant
305  *      can never attain positive values.
306  * Return IMPURE otherwise.
307  */
308 static int purity(__isl_keep isl_basic_set *bset, isl_int *c, int *div_purity,
309         int eq)
310 {
311         unsigned d;
312         unsigned n_div;
313         unsigned nparam;
314         int empty;
315         int i;
316         int p = 0, v = 0;
317
318         n_div = isl_basic_set_dim(bset, isl_dim_div);
319         d = isl_basic_set_dim(bset, isl_dim_set);
320         nparam = isl_basic_set_dim(bset, isl_dim_param);
321
322         for (i = 0; i < n_div; ++i) {
323                 if (isl_int_is_zero(c[1 + nparam + d + i]))
324                         continue;
325                 switch (div_purity[i]) {
326                 case PURE_PARAM: p = 1; break;
327                 case PURE_VAR: v = 1; break;
328                 default: return IMPURE;
329                 }
330         }
331         if (!p && isl_seq_first_non_zero(c + 1, nparam) == -1)
332                 return PURE_VAR;
333         if (!v && isl_seq_first_non_zero(c + 1 + nparam, d) == -1)
334                 return PURE_PARAM;
335
336         empty = parametric_constant_never_positive(bset, c, div_purity);
337         if (eq && empty >= 0 && !empty) {
338                 isl_seq_neg(c, c, 1 + nparam + d + n_div);
339                 empty = parametric_constant_never_positive(bset, c, div_purity);
340         }
341
342         return empty < 0 ? -1 : empty ? MIXED : IMPURE;
343 }
344
345 /* Return an array of integers indicating the type of each div in bset.
346  * If the div is (recursively) defined in terms of only the parameters,
347  * then the type is PURE_PARAM.
348  * If the div is (recursively) defined in terms of only the set variables,
349  * then the type is PURE_VAR.
350  * Otherwise, the type is IMPURE.
351  */
352 static __isl_give int *get_div_purity(__isl_keep isl_basic_set *bset)
353 {
354         int i, j;
355         int *div_purity;
356         unsigned d;
357         unsigned n_div;
358         unsigned nparam;
359
360         if (!bset)
361                 return NULL;
362
363         n_div = isl_basic_set_dim(bset, isl_dim_div);
364         d = isl_basic_set_dim(bset, isl_dim_set);
365         nparam = isl_basic_set_dim(bset, isl_dim_param);
366
367         div_purity = isl_alloc_array(bset->ctx, int, n_div);
368         if (!div_purity)
369                 return NULL;
370
371         for (i = 0; i < bset->n_div; ++i) {
372                 int p = 0, v = 0;
373                 if (isl_int_is_zero(bset->div[i][0])) {
374                         div_purity[i] = IMPURE;
375                         continue;
376                 }
377                 if (isl_seq_first_non_zero(bset->div[i] + 2, nparam) != -1)
378                         p = 1;
379                 if (isl_seq_first_non_zero(bset->div[i] + 2 + nparam, d) != -1)
380                         v = 1;
381                 for (j = 0; j < i; ++j) {
382                         if (isl_int_is_zero(bset->div[i][2 + nparam + d + j]))
383                                 continue;
384                         switch (div_purity[j]) {
385                         case PURE_PARAM: p = 1; break;
386                         case PURE_VAR: v = 1; break;
387                         default: p = v = 1; break;
388                         }
389                 }
390                 div_purity[i] = v ? p ? IMPURE : PURE_VAR : PURE_PARAM;
391         }
392
393         return div_purity;
394 }
395
396 /* Given a path with the as yet unconstrained length at position "pos",
397  * check if setting the length to zero results in only the identity
398  * mapping.
399  */
400 int empty_path_is_identity(__isl_keep isl_basic_map *path, unsigned pos)
401 {
402         isl_basic_map *test = NULL;
403         isl_basic_map *id = NULL;
404         int k;
405         int is_id;
406
407         test = isl_basic_map_copy(path);
408         test = isl_basic_map_extend_constraints(test, 1, 0);
409         k = isl_basic_map_alloc_equality(test);
410         if (k < 0)
411                 goto error;
412         isl_seq_clr(test->eq[k], 1 + isl_basic_map_total_dim(test));
413         isl_int_set_si(test->eq[k][pos], 1);
414         id = isl_basic_map_identity(isl_dim_domain(isl_basic_map_get_dim(path)));
415         is_id = isl_basic_map_is_equal(test, id);
416         isl_basic_map_free(test);
417         isl_basic_map_free(id);
418         return is_id;
419 error:
420         isl_basic_map_free(test);
421         return -1;
422 }
423
424 __isl_give isl_basic_map *add_delta_constraints(__isl_take isl_basic_map *path,
425         __isl_keep isl_basic_set *delta, unsigned off, unsigned nparam,
426         unsigned d, int *div_purity, int eq)
427 {
428         int i, k;
429         int n = eq ? delta->n_eq : delta->n_ineq;
430         isl_int **delta_c = eq ? delta->eq : delta->ineq;
431         unsigned n_div;
432
433         n_div = isl_basic_set_dim(delta, isl_dim_div);
434
435         for (i = 0; i < n; ++i) {
436                 isl_int *path_c;
437                 int p = purity(delta, delta_c[i], div_purity, eq);
438                 if (p < 0)
439                         goto error;
440                 if (p == IMPURE)
441                         continue;
442                 if (eq && p != MIXED) {
443                         k = isl_basic_map_alloc_equality(path);
444                         path_c = path->eq[k];
445                 } else {
446                         k = isl_basic_map_alloc_inequality(path);
447                         path_c = path->ineq[k];
448                 }
449                 if (k < 0)
450                         goto error;
451                 isl_seq_clr(path_c, 1 + isl_basic_map_total_dim(path));
452                 if (p == PURE_VAR) {
453                         isl_seq_cpy(path_c + off,
454                                     delta_c[i] + 1 + nparam, d);
455                         isl_int_set(path_c[off + d], delta_c[i][0]);
456                 } else if (p == PURE_PARAM) {
457                         isl_seq_cpy(path_c, delta_c[i], 1 + nparam);
458                 } else {
459                         isl_seq_cpy(path_c + off,
460                                     delta_c[i] + 1 + nparam, d);
461                         isl_seq_cpy(path_c, delta_c[i], 1 + nparam);
462                 }
463                 isl_seq_cpy(path_c + off - n_div,
464                             delta_c[i] + 1 + nparam + d, n_div);
465         }
466
467         return path;
468 error:
469         isl_basic_map_free(path);
470         return NULL;
471 }
472
473 /* Given a set of offsets "delta", construct a relation of the
474  * given dimension specification (Z^{n+1} -> Z^{n+1}) that
475  * is an overapproximation of the relations that
476  * maps an element x to any element that can be reached
477  * by taking a non-negative number of steps along any of
478  * the elements in "delta".
479  * That is, construct an approximation of
480  *
481  *      { [x] -> [y] : exists f \in \delta, k \in Z :
482  *                                      y = x + k [f, 1] and k >= 0 }
483  *
484  * For any element in this relation, the number of steps taken
485  * is equal to the difference in the final coordinates.
486  *
487  * In particular, let delta be defined as
488  *
489  *      \delta = [p] -> { [x] : A x + a >= and B p + b >= 0 and
490  *                              C x + C'p + c >= 0 and
491  *                              D x + D'p + d >= 0 }
492  *
493  * where the constraints C x + C'p + c >= 0 are such that the parametric
494  * constant term of each constraint j, "C_j x + C'_j p + c_j",
495  * can never attain positive values, then the relation is constructed as
496  *
497  *      { [x] -> [y] : exists [f, k] \in Z^{n+1} : y = x + f and
498  *                      A f + k a >= 0 and B p + b >= 0 and
499  *                      C f + C'p + c >= 0 and k >= 1 }
500  *      union { [x] -> [x] }
501  *
502  * If the zero-length paths happen to correspond exactly to the identity
503  * mapping, then we return
504  *
505  *      { [x] -> [y] : exists [f, k] \in Z^{n+1} : y = x + f and
506  *                      A f + k a >= 0 and B p + b >= 0 and
507  *                      C f + C'p + c >= 0 and k >= 0 }
508  *
509  * instead.
510  *
511  * Existentially quantified variables in \delta are handled by
512  * classifying them as independent of the parameters, purely
513  * parameter dependent and others.  Constraints containing
514  * any of the other existentially quantified variables are removed.
515  * This is safe, but leads to an additional overapproximation.
516  */
517 static __isl_give isl_map *path_along_delta(__isl_take isl_dim *dim,
518         __isl_take isl_basic_set *delta)
519 {
520         isl_basic_map *path = NULL;
521         unsigned d;
522         unsigned n_div;
523         unsigned nparam;
524         unsigned off;
525         int i, k;
526         int is_id;
527         int *div_purity = NULL;
528
529         if (!delta)
530                 goto error;
531         n_div = isl_basic_set_dim(delta, isl_dim_div);
532         d = isl_basic_set_dim(delta, isl_dim_set);
533         nparam = isl_basic_set_dim(delta, isl_dim_param);
534         path = isl_basic_map_alloc_dim(isl_dim_copy(dim), n_div + d + 1,
535                         d + 1 + delta->n_eq, delta->n_eq + delta->n_ineq + 1);
536         off = 1 + nparam + 2 * (d + 1) + n_div;
537
538         for (i = 0; i < n_div + d + 1; ++i) {
539                 k = isl_basic_map_alloc_div(path);
540                 if (k < 0)
541                         goto error;
542                 isl_int_set_si(path->div[k][0], 0);
543         }
544
545         for (i = 0; i < d + 1; ++i) {
546                 k = isl_basic_map_alloc_equality(path);
547                 if (k < 0)
548                         goto error;
549                 isl_seq_clr(path->eq[k], 1 + isl_basic_map_total_dim(path));
550                 isl_int_set_si(path->eq[k][1 + nparam + i], 1);
551                 isl_int_set_si(path->eq[k][1 + nparam + d + 1 + i], -1);
552                 isl_int_set_si(path->eq[k][off + i], 1);
553         }
554
555         div_purity = get_div_purity(delta);
556         if (!div_purity)
557                 goto error;
558
559         path = add_delta_constraints(path, delta, off, nparam, d, div_purity, 1);
560         path = add_delta_constraints(path, delta, off, nparam, d, div_purity, 0);
561
562         is_id = empty_path_is_identity(path, off + d);
563         if (is_id < 0)
564                 goto error;
565
566         k = isl_basic_map_alloc_inequality(path);
567         if (k < 0)
568                 goto error;
569         isl_seq_clr(path->ineq[k], 1 + isl_basic_map_total_dim(path));
570         if (!is_id)
571                 isl_int_set_si(path->ineq[k][0], -1);
572         isl_int_set_si(path->ineq[k][off + d], 1);
573                         
574         free(div_purity);
575         isl_basic_set_free(delta);
576         path = isl_basic_map_finalize(path);
577         if (is_id) {
578                 isl_dim_free(dim);
579                 return isl_map_from_basic_map(path);
580         }
581         return isl_basic_map_union(path,
582                                 isl_basic_map_identity(isl_dim_domain(dim)));
583 error:
584         free(div_purity);
585         isl_dim_free(dim);
586         isl_basic_set_free(delta);
587         isl_basic_map_free(path);
588         return NULL;
589 }
590
591 /* Given a dimenion specification Z^{n+1} -> Z^{n+1} and a parameter "param",
592  * construct a map that equates the parameter to the difference
593  * in the final coordinates and imposes that this difference is positive.
594  * That is, construct
595  *
596  *      { [x,x_s] -> [y,y_s] : k = y_s - x_s > 0 }
597  */
598 static __isl_give isl_map *equate_parameter_to_length(__isl_take isl_dim *dim,
599         unsigned param)
600 {
601         struct isl_basic_map *bmap;
602         unsigned d;
603         unsigned nparam;
604         int k;
605
606         d = isl_dim_size(dim, isl_dim_in);
607         nparam = isl_dim_size(dim, isl_dim_param);
608         bmap = isl_basic_map_alloc_dim(dim, 0, 1, 1);
609         k = isl_basic_map_alloc_equality(bmap);
610         if (k < 0)
611                 goto error;
612         isl_seq_clr(bmap->eq[k], 1 + isl_basic_map_total_dim(bmap));
613         isl_int_set_si(bmap->eq[k][1 + param], -1);
614         isl_int_set_si(bmap->eq[k][1 + nparam + d - 1], -1);
615         isl_int_set_si(bmap->eq[k][1 + nparam + d + d - 1], 1);
616
617         k = isl_basic_map_alloc_inequality(bmap);
618         if (k < 0)
619                 goto error;
620         isl_seq_clr(bmap->ineq[k], 1 + isl_basic_map_total_dim(bmap));
621         isl_int_set_si(bmap->ineq[k][1 + param], 1);
622         isl_int_set_si(bmap->ineq[k][0], -1);
623
624         bmap = isl_basic_map_finalize(bmap);
625         return isl_map_from_basic_map(bmap);
626 error:
627         isl_basic_map_free(bmap);
628         return NULL;
629 }
630
631 /* Check whether "path" is acyclic, where the last coordinates of domain
632  * and range of path encode the number of steps taken.
633  * That is, check whether
634  *
635  *      { d | d = y - x and (x,y) in path }
636  *
637  * does not contain any element with positive last coordinate (positive length)
638  * and zero remaining coordinates (cycle).
639  */
640 static int is_acyclic(__isl_take isl_map *path)
641 {
642         int i;
643         int acyclic;
644         unsigned dim;
645         struct isl_set *delta;
646
647         delta = isl_map_deltas(path);
648         dim = isl_set_dim(delta, isl_dim_set);
649         for (i = 0; i < dim; ++i) {
650                 if (i == dim -1)
651                         delta = isl_set_lower_bound_si(delta, isl_dim_set, i, 1);
652                 else
653                         delta = isl_set_fix_si(delta, isl_dim_set, i, 0);
654         }
655
656         acyclic = isl_set_is_empty(delta);
657         isl_set_free(delta);
658
659         return acyclic;
660 }
661
662 /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D
663  * and a dimension specification (Z^{n+1} -> Z^{n+1}),
664  * construct a map that is an overapproximation of the map
665  * that takes an element from the space D \times Z to another
666  * element from the same space, such that the first n coordinates of the
667  * difference between them is a sum of differences between images
668  * and pre-images in one of the R_i and such that the last coordinate
669  * is equal to the number of steps taken.
670  * That is, let
671  *
672  *      \Delta_i = { y - x | (x, y) in R_i }
673  *
674  * then the constructed map is an overapproximation of
675  *
676  *      { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i :
677  *                              d = (\sum_i k_i \delta_i, \sum_i k_i) }
678  *
679  * The elements of the singleton \Delta_i's are collected as the
680  * rows of the steps matrix.  For all these \Delta_i's together,
681  * a single path is constructed.
682  * For each of the other \Delta_i's, we compute an overapproximation
683  * of the paths along elements of \Delta_i.
684  * Since each of these paths performs an addition, composition is
685  * symmetric and we can simply compose all resulting paths in any order.
686  */
687 static __isl_give isl_map *construct_extended_path(__isl_take isl_dim *dim,
688         __isl_keep isl_map *map, int *project)
689 {
690         struct isl_mat *steps = NULL;
691         struct isl_map *path = NULL;
692         unsigned d;
693         int i, j, n;
694
695         d = isl_map_dim(map, isl_dim_in);
696
697         path = isl_map_identity(isl_dim_domain(isl_dim_copy(dim)));
698
699         steps = isl_mat_alloc(map->ctx, map->n, d);
700         if (!steps)
701                 goto error;
702
703         n = 0;
704         for (i = 0; i < map->n; ++i) {
705                 struct isl_basic_set *delta;
706
707                 delta = isl_basic_map_deltas(isl_basic_map_copy(map->p[i]));
708
709                 for (j = 0; j < d; ++j) {
710                         int fixed;
711
712                         fixed = isl_basic_set_fast_dim_is_fixed(delta, j,
713                                                             &steps->row[n][j]);
714                         if (fixed < 0) {
715                                 isl_basic_set_free(delta);
716                                 goto error;
717                         }
718                         if (!fixed)
719                                 break;
720                 }
721
722
723                 if (j < d) {
724                         path = isl_map_apply_range(path,
725                                 path_along_delta(isl_dim_copy(dim), delta));
726                         path = isl_map_coalesce(path);
727                 } else {
728                         isl_basic_set_free(delta);
729                         ++n;
730                 }
731         }
732
733         if (n > 0) {
734                 steps->n_row = n;
735                 path = isl_map_apply_range(path,
736                                 path_along_steps(isl_dim_copy(dim), steps));
737         }
738
739         if (project && *project) {
740                 *project = is_acyclic(isl_map_copy(path));
741                 if (*project < 0)
742                         goto error;
743         }
744
745         isl_dim_free(dim);
746         isl_mat_free(steps);
747         return path;
748 error:
749         isl_dim_free(dim);
750         isl_mat_free(steps);
751         isl_map_free(path);
752         return NULL;
753 }
754
755 static int isl_set_overlaps(__isl_keep isl_set *set1, __isl_keep isl_set *set2)
756 {
757         isl_set *i;
758         int no_overlap;
759
760         i = isl_set_intersect(isl_set_copy(set1), isl_set_copy(set2));
761         no_overlap = isl_set_is_empty(i);
762         isl_set_free(i);
763
764         return no_overlap < 0 ? -1 : !no_overlap;
765 }
766
767 /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D
768  * and a dimension specification (Z^{n+1} -> Z^{n+1}),
769  * construct a map that is an overapproximation of the map
770  * that takes an element from the dom R \times Z to an
771  * element from ran R \times Z, such that the first n coordinates of the
772  * difference between them is a sum of differences between images
773  * and pre-images in one of the R_i and such that the last coordinate
774  * is equal to the number of steps taken.
775  * That is, let
776  *
777  *      \Delta_i = { y - x | (x, y) in R_i }
778  *
779  * then the constructed map is an overapproximation of
780  *
781  *      { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i :
782  *                              d = (\sum_i k_i \delta_i, \sum_i k_i) and
783  *                              x in dom R and x + d in ran R and
784  *                              \sum_i k_i >= 1 }
785  */
786 static __isl_give isl_map *construct_component(__isl_take isl_dim *dim,
787         __isl_keep isl_map *map, int *exact, int project)
788 {
789         struct isl_set *domain = NULL;
790         struct isl_set *range = NULL;
791         struct isl_map *app = NULL;
792         struct isl_map *path = NULL;
793
794         domain = isl_map_domain(isl_map_copy(map));
795         domain = isl_set_coalesce(domain);
796         range = isl_map_range(isl_map_copy(map));
797         range = isl_set_coalesce(range);
798         if (!isl_set_overlaps(domain, range)) {
799                 isl_set_free(domain);
800                 isl_set_free(range);
801                 isl_dim_free(dim);
802
803                 map = isl_map_copy(map);
804                 map = isl_map_add(map, isl_dim_in, 1);
805                 map = isl_map_add(map, isl_dim_out, 1);
806                 map = set_path_length(map, 1, 1);
807                 return map;
808         }
809         app = isl_map_from_domain_and_range(domain, range);
810         app = isl_map_add(app, isl_dim_in, 1);
811         app = isl_map_add(app, isl_dim_out, 1);
812
813         path = construct_extended_path(isl_dim_copy(dim), map,
814                                         exact && *exact ? &project : NULL);
815         app = isl_map_intersect(app, path);
816
817         if (exact && *exact &&
818             (*exact = check_exactness(isl_map_copy(map), isl_map_copy(app),
819                                       project)) < 0)
820                 goto error;
821
822         isl_dim_free(dim);
823         app = set_path_length(app, 0, 1);
824         return app;
825 error:
826         isl_dim_free(dim);
827         isl_map_free(app);
828         return NULL;
829 }
830
831 /* Call construct_component and, if "project" is set, project out
832  * the final coordinates.
833  */
834 static __isl_give isl_map *construct_projected_component(
835         __isl_take isl_dim *dim,
836         __isl_keep isl_map *map, int *exact, int project)
837 {
838         isl_map *app;
839         unsigned d;
840
841         if (!dim)
842                 return NULL;
843         d = isl_dim_size(dim, isl_dim_in);
844
845         app = construct_component(dim, map, exact, project);
846         if (project) {
847                 app = isl_map_project_out(app, isl_dim_in, d - 1, 1);
848                 app = isl_map_project_out(app, isl_dim_out, d - 1, 1);
849         }
850         return app;
851 }
852
853 /* Compute an extended version, i.e., with path lengths, of
854  * an overapproximation of the transitive closure of "bmap"
855  * with path lengths greater than or equal to zero and with
856  * domain and range equal to "dom".
857  */
858 static __isl_give isl_map *q_closure(__isl_take isl_dim *dim,
859         __isl_take isl_set *dom, __isl_keep isl_basic_map *bmap, int *exact)
860 {
861         int project = 1;
862         isl_map *path;
863         isl_map *map;
864         isl_map *app;
865
866         dom = isl_set_add(dom, isl_dim_set, 1);
867         app = isl_map_from_domain_and_range(dom, isl_set_copy(dom));
868         map = isl_map_from_basic_map(isl_basic_map_copy(bmap));
869         path = construct_extended_path(dim, map, &project);
870         app = isl_map_intersect(app, path);
871
872         if ((*exact = check_exactness(map, isl_map_copy(app), project)) < 0)
873                 goto error;
874
875         return app;
876 error:
877         isl_map_free(app);
878         return NULL;
879 }
880
881 /* Check whether qc has any elements of length at least one
882  * with domain and/or range outside of dom and ran.
883  */
884 static int has_spurious_elements(__isl_keep isl_map *qc,
885         __isl_keep isl_set *dom, __isl_keep isl_set *ran)
886 {
887         isl_set *s;
888         int subset;
889         unsigned d;
890
891         if (!qc || !dom || !ran)
892                 return -1;
893
894         d = isl_map_dim(qc, isl_dim_in);
895
896         qc = isl_map_copy(qc);
897         qc = set_path_length(qc, 0, 1);
898         qc = isl_map_project_out(qc, isl_dim_in, d - 1, 1);
899         qc = isl_map_project_out(qc, isl_dim_out, d - 1, 1);
900
901         s = isl_map_domain(isl_map_copy(qc));
902         subset = isl_set_is_subset(s, dom);
903         isl_set_free(s);
904         if (subset < 0)
905                 goto error;
906         if (!subset) {
907                 isl_map_free(qc);
908                 return 1;
909         }
910
911         s = isl_map_range(qc);
912         subset = isl_set_is_subset(s, ran);
913         isl_set_free(s);
914
915         return subset < 0 ? -1 : !subset;
916 error:
917         isl_map_free(qc);
918         return -1;
919 }
920
921 #define LEFT    2
922 #define RIGHT   1
923
924 /* For each basic map in "map", except i, check whether it combines
925  * with the transitive closure that is reflexive on C combines
926  * to the left and to the right.
927  *
928  * In particular, if
929  *
930  *      dom map_j \subseteq C
931  *
932  * then right[j] is set to 1.  Otherwise, if
933  *
934  *      ran map_i \cap dom map_j = \emptyset
935  *
936  * then right[j] is set to 0.  Otherwise, composing to the right
937  * is impossible.
938  *
939  * Similar, for composing to the left, we have if
940  *
941  *      ran map_j \subseteq C
942  *
943  * then left[j] is set to 1.  Otherwise, if
944  *
945  *      dom map_i \cap ran map_j = \emptyset
946  *
947  * then left[j] is set to 0.  Otherwise, composing to the left
948  * is impossible.
949  *
950  * The return value is or'd with LEFT if composing to the left
951  * is possible and with RIGHT if composing to the right is possible.
952  */
953 static int composability(__isl_keep isl_set *C, int i,
954         isl_set **dom, isl_set **ran, int *left, int *right,
955         __isl_keep isl_map *map)
956 {
957         int j;
958         int ok;
959
960         ok = LEFT | RIGHT;
961         for (j = 0; j < map->n && ok; ++j) {
962                 int overlaps, subset;
963                 if (j == i)
964                         continue;
965
966                 if (ok & RIGHT) {
967                         if (!dom[j])
968                                 dom[j] = isl_set_from_basic_set(
969                                         isl_basic_map_domain(
970                                                 isl_basic_map_copy(map->p[j])));
971                         if (!dom[j])
972                                 return -1;
973                         overlaps = isl_set_overlaps(ran[i], dom[j]);
974                         if (overlaps < 0)
975                                 return -1;
976                         if (!overlaps)
977                                 right[j] = 0;
978                         else {
979                                 subset = isl_set_is_subset(dom[j], C);
980                                 if (subset < 0)
981                                         return -1;
982                                 if (subset)
983                                         right[j] = 1;
984                                 else
985                                         ok &= ~RIGHT;
986                         }
987                 }
988
989                 if (ok & LEFT) {
990                         if (!ran[j])
991                                 ran[j] = isl_set_from_basic_set(
992                                         isl_basic_map_range(
993                                                 isl_basic_map_copy(map->p[j])));
994                         if (!ran[j])
995                                 return -1;
996                         overlaps = isl_set_overlaps(dom[i], ran[j]);
997                         if (overlaps < 0)
998                                 return -1;
999                         if (!overlaps)
1000                                 left[j] = 0;
1001                         else {
1002                                 subset = isl_set_is_subset(ran[j], C);
1003                                 if (subset < 0)
1004                                         return -1;
1005                                 if (subset)
1006                                         left[j] = 1;
1007                                 else
1008                                         ok &= ~LEFT;
1009                         }
1010                 }
1011         }
1012
1013         return ok;
1014 }
1015
1016 /* Return a map that is a union of the basic maps in "map", except i,
1017  * composed to left and right with qc based on the entries of "left"
1018  * and "right".
1019  */
1020 static __isl_give isl_map *compose(__isl_keep isl_map *map, int i,
1021         __isl_take isl_map *qc, int *left, int *right)
1022 {
1023         int j;
1024         isl_map *comp;
1025
1026         comp = isl_map_empty(isl_map_get_dim(map));
1027         for (j = 0; j < map->n; ++j) {
1028                 isl_map *map_j;
1029
1030                 if (j == i)
1031                         continue;
1032
1033                 map_j = isl_map_from_basic_map(isl_basic_map_copy(map->p[j]));
1034                 if (left && left[j])
1035                         map_j = isl_map_apply_range(map_j, isl_map_copy(qc));
1036                 if (right && right[j])
1037                         map_j = isl_map_apply_range(isl_map_copy(qc), map_j);
1038                 comp = isl_map_union(comp, map_j);
1039         }
1040
1041         comp = isl_map_compute_divs(comp);
1042         comp = isl_map_coalesce(comp);
1043
1044         isl_map_free(qc);
1045
1046         return comp;
1047 }
1048
1049 /* Compute the transitive closure of "map" incrementally by
1050  * computing
1051  *
1052  *      map_i^+ \cup qc^+
1053  *
1054  * or
1055  *
1056  *      map_i^+ \cup ((id \cup map_i^) \circ qc^+)
1057  *
1058  * or
1059  *
1060  *      map_i^+ \cup (qc^+ \circ (id \cup map_i^))
1061  *
1062  * depending on whether left or right are NULL.
1063  */
1064 static __isl_give isl_map *compute_incremental(
1065         __isl_take isl_dim *dim, __isl_keep isl_map *map,
1066         int i, __isl_take isl_map *qc, int *left, int *right, int *exact)
1067 {
1068         isl_map *map_i;
1069         isl_map *tc;
1070         isl_map *rtc = NULL;
1071
1072         if (!map)
1073                 goto error;
1074         isl_assert(map->ctx, left || right, goto error);
1075
1076         map_i = isl_map_from_basic_map(isl_basic_map_copy(map->p[i]));
1077         tc = construct_projected_component(isl_dim_copy(dim), map_i,
1078                                                 exact, 1);
1079         isl_map_free(map_i);
1080
1081         if (*exact)
1082                 qc = isl_map_transitive_closure(qc, exact);
1083
1084         if (!*exact) {
1085                 isl_dim_free(dim);
1086                 isl_map_free(tc);
1087                 isl_map_free(qc);
1088                 return isl_map_universe(isl_map_get_dim(map));
1089         }
1090
1091         if (!left || !right)
1092                 rtc = isl_map_union(isl_map_copy(tc),
1093                         isl_map_identity(isl_dim_domain(isl_map_get_dim(tc))));
1094         if (!right)
1095                 qc = isl_map_apply_range(rtc, qc);
1096         if (!left)
1097                 qc = isl_map_apply_range(qc, rtc);
1098         qc = isl_map_union(tc, qc);
1099
1100         isl_dim_free(dim);
1101
1102         return qc;
1103 error:
1104         isl_dim_free(dim);
1105         isl_map_free(qc);
1106         return NULL;
1107 }
1108
1109 /* Given a map "map", try to find a basic map such that
1110  * map^+ can be computed as
1111  *
1112  * map^+ = map_i^+ \cup
1113  *    \bigcup_j ((map_i^+ \cup Id_C)^+ \circ map_j \circ (map_i^+ \cup Id_C))^+
1114  *
1115  * with C the simple hull of the domain and range of the input map.
1116  * map_i^ \cup Id_C is computed by allowing the path lengths to be zero
1117  * and by intersecting domain and range with C.
1118  * Of course, we need to check that this is actually equal to map_i^ \cup Id_C.
1119  * Also, we only use the incremental computation if all the transitive
1120  * closures are exact and if the number of basic maps in the union,
1121  * after computing the integer divisions, is smaller than the number
1122  * of basic maps in the input map.
1123  */
1124 static int incemental_on_entire_domain(__isl_keep isl_dim *dim,
1125         __isl_keep isl_map *map,
1126         isl_set **dom, isl_set **ran, int *left, int *right,
1127         __isl_give isl_map **res)
1128 {
1129         int i;
1130         isl_set *C;
1131         unsigned d;
1132
1133         *res = NULL;
1134
1135         C = isl_set_union(isl_map_domain(isl_map_copy(map)),
1136                           isl_map_range(isl_map_copy(map)));
1137         C = isl_set_from_basic_set(isl_set_simple_hull(C));
1138         if (!C)
1139                 return -1;
1140         if (C->n != 1) {
1141                 isl_set_free(C);
1142                 return 0;
1143         }
1144
1145         d = isl_map_dim(map, isl_dim_in);
1146
1147         for (i = 0; i < map->n; ++i) {
1148                 isl_map *qc;
1149                 int exact_i, spurious;
1150                 int j;
1151                 dom[i] = isl_set_from_basic_set(isl_basic_map_domain(
1152                                         isl_basic_map_copy(map->p[i])));
1153                 ran[i] = isl_set_from_basic_set(isl_basic_map_range(
1154                                         isl_basic_map_copy(map->p[i])));
1155                 qc = q_closure(isl_dim_copy(dim), isl_set_copy(C),
1156                                 map->p[i], &exact_i);
1157                 if (!qc)
1158                         goto error;
1159                 if (!exact_i) {
1160                         isl_map_free(qc);
1161                         continue;
1162                 }
1163                 spurious = has_spurious_elements(qc, dom[i], ran[i]);
1164                 if (spurious) {
1165                         isl_map_free(qc);
1166                         if (spurious < 0)
1167                                 goto error;
1168                         continue;
1169                 }
1170                 qc = isl_map_project_out(qc, isl_dim_in, d, 1);
1171                 qc = isl_map_project_out(qc, isl_dim_out, d, 1);
1172                 qc = isl_map_compute_divs(qc);
1173                 for (j = 0; j < map->n; ++j)
1174                         left[j] = right[j] = 1;
1175                 qc = compose(map, i, qc, left, right);
1176                 if (!qc)
1177                         goto error;
1178                 if (qc->n >= map->n) {
1179                         isl_map_free(qc);
1180                         continue;
1181                 }
1182                 *res = compute_incremental(isl_dim_copy(dim), map, i, qc,
1183                                 left, right, &exact_i);
1184                 if (!*res)
1185                         goto error;
1186                 if (exact_i)
1187                         break;
1188                 isl_map_free(*res);
1189                 *res = NULL;
1190         }
1191
1192         isl_set_free(C);
1193
1194         return *res != NULL;
1195 error:
1196         isl_set_free(C);
1197         return -1;
1198 }
1199
1200 /* Try and compute the transitive closure of "map" as
1201  *
1202  * map^+ = map_i^+ \cup
1203  *    \bigcup_j ((map_i^+ \cup Id_C)^+ \circ map_j \circ (map_i^+ \cup Id_C))^+
1204  *
1205  * with C either the simple hull of the domain and range of the entire
1206  * map or the simple hull of domain and range of map_i.
1207  */
1208 static __isl_give isl_map *incremental_closure(__isl_take isl_dim *dim,
1209         __isl_keep isl_map *map, int *exact, int project)
1210 {
1211         int i;
1212         isl_set **dom = NULL;
1213         isl_set **ran = NULL;
1214         int *left = NULL;
1215         int *right = NULL;
1216         isl_set *C;
1217         unsigned d;
1218         isl_map *res = NULL;
1219
1220         if (!project)
1221                 return construct_projected_component(dim, map, exact, project);
1222
1223         if (!map)
1224                 goto error;
1225         if (map->n <= 1)
1226                 return construct_projected_component(dim, map, exact, project);
1227
1228         d = isl_map_dim(map, isl_dim_in);
1229
1230         dom = isl_calloc_array(map->ctx, isl_set *, map->n);
1231         ran = isl_calloc_array(map->ctx, isl_set *, map->n);
1232         left = isl_calloc_array(map->ctx, int, map->n);
1233         right = isl_calloc_array(map->ctx, int, map->n);
1234         if (!ran || !dom || !left || !right)
1235                 goto error;
1236
1237         if (incemental_on_entire_domain(dim, map, dom, ran, left, right, &res) < 0)
1238                 goto error;
1239
1240         for (i = 0; !res && i < map->n; ++i) {
1241                 isl_map *qc;
1242                 int exact_i, spurious, comp;
1243                 if (!dom[i])
1244                         dom[i] = isl_set_from_basic_set(
1245                                         isl_basic_map_domain(
1246                                                 isl_basic_map_copy(map->p[i])));
1247                 if (!dom[i])
1248                         goto error;
1249                 if (!ran[i])
1250                         ran[i] = isl_set_from_basic_set(
1251                                         isl_basic_map_range(
1252                                                 isl_basic_map_copy(map->p[i])));
1253                 if (!ran[i])
1254                         goto error;
1255                 C = isl_set_union(isl_set_copy(dom[i]),
1256                                       isl_set_copy(ran[i]));
1257                 C = isl_set_from_basic_set(isl_set_simple_hull(C));
1258                 if (!C)
1259                         goto error;
1260                 if (C->n != 1) {
1261                         isl_set_free(C);
1262                         continue;
1263                 }
1264                 comp = composability(C, i, dom, ran, left, right, map);
1265                 if (!comp || comp < 0) {
1266                         isl_set_free(C);
1267                         if (comp < 0)
1268                                 goto error;
1269                         continue;
1270                 }
1271                 qc = q_closure(isl_dim_copy(dim), C, map->p[i], &exact_i);
1272                 if (!qc)
1273                         goto error;
1274                 if (!exact_i) {
1275                         isl_map_free(qc);
1276                         continue;
1277                 }
1278                 spurious = has_spurious_elements(qc, dom[i], ran[i]);
1279                 if (spurious) {
1280                         isl_map_free(qc);
1281                         if (spurious < 0)
1282                                 goto error;
1283                         continue;
1284                 }
1285                 qc = isl_map_project_out(qc, isl_dim_in, d, 1);
1286                 qc = isl_map_project_out(qc, isl_dim_out, d, 1);
1287                 qc = isl_map_compute_divs(qc);
1288                 qc = compose(map, i, qc, (comp & LEFT) ? left : NULL,
1289                                 (comp & RIGHT) ? right : NULL);
1290                 if (!qc)
1291                         goto error;
1292                 if (qc->n >= map->n) {
1293                         isl_map_free(qc);
1294                         continue;
1295                 }
1296                 res = compute_incremental(isl_dim_copy(dim), map, i, qc,
1297                                 (comp & LEFT) ? left : NULL,
1298                                 (comp & RIGHT) ? right : NULL, &exact_i);
1299                 if (!res)
1300                         goto error;
1301                 if (exact_i)
1302                         break;
1303                 isl_map_free(res);
1304                 res = NULL;
1305         }
1306
1307         for (i = 0; i < map->n; ++i) {
1308                 isl_set_free(dom[i]);
1309                 isl_set_free(ran[i]);
1310         }
1311         free(dom);
1312         free(ran);
1313         free(left);
1314         free(right);
1315
1316         if (res) {
1317                 isl_dim_free(dim);
1318                 return res;
1319         }
1320
1321         return construct_projected_component(dim, map, exact, project);
1322 error:
1323         if (dom)
1324                 for (i = 0; i < map->n; ++i)
1325                         isl_set_free(dom[i]);
1326         free(dom);
1327         if (ran)
1328                 for (i = 0; i < map->n; ++i)
1329                         isl_set_free(ran[i]);
1330         free(ran);
1331         free(left);
1332         free(right);
1333         isl_dim_free(dim);
1334         return NULL;
1335 }
1336
1337 /* Given an array of sets "set", add "dom" at position "pos"
1338  * and search for elements at earlier positions that overlap with "dom".
1339  * If any can be found, then merge all of them, together with "dom", into
1340  * a single set and assign the union to the first in the array,
1341  * which becomes the new group leader for all groups involved in the merge.
1342  * During the search, we only consider group leaders, i.e., those with
1343  * group[i] = i, as the other sets have already been combined
1344  * with one of the group leaders.
1345  */
1346 static int merge(isl_set **set, int *group, __isl_take isl_set *dom, int pos)
1347 {
1348         int i;
1349
1350         group[pos] = pos;
1351         set[pos] = isl_set_copy(dom);
1352
1353         for (i = pos - 1; i >= 0; --i) {
1354                 int o;
1355
1356                 if (group[i] != i)
1357                         continue;
1358
1359                 o = isl_set_overlaps(set[i], dom);
1360                 if (o < 0)
1361                         goto error;
1362                 if (!o)
1363                         continue;
1364
1365                 set[i] = isl_set_union(set[i], set[group[pos]]);
1366                 if (!set[i])
1367                         goto error;
1368                 set[group[pos]] = NULL;
1369                 group[group[pos]] = i;
1370                 group[pos] = i;
1371         }
1372
1373         isl_set_free(dom);
1374         return 0;
1375 error:
1376         isl_set_free(dom);
1377         return -1;
1378 }
1379
1380 /* Given a partition of the domains and ranges of the basic maps in "map",
1381  * apply the Floyd-Warshall algorithm with the elements in the partition
1382  * as vertices.
1383  *
1384  * In particular, there are "n" elements in the partition and "group" is
1385  * an array of length 2 * map->n with entries in [0,n-1].
1386  *
1387  * We first construct a matrix of relations based on the partition information,
1388  * apply Floyd-Warshall on this matrix of relations and then take the
1389  * union of all entries in the matrix as the final result.
1390  *
1391  * The algorithm iterates over all vertices.  In each step, the whole
1392  * matrix is updated to include all paths that go to the current vertex,
1393  * possibly stay there a while (including passing through earlier vertices)
1394  * and then come back.  At the start of each iteration, the diagonal
1395  * element corresponding to the current vertex is replaced by its
1396  * transitive closure to account for all indirect paths that stay
1397  * in the current vertex.
1398  */
1399 static __isl_give isl_map *floyd_warshall_with_groups(__isl_take isl_dim *dim,
1400         __isl_keep isl_map *map, int *exact, int project, int *group, int n)
1401 {
1402         int i, j, k;
1403         int r, p, q;
1404         isl_map ***grid = NULL;
1405         isl_map *app;
1406
1407         if (!map)
1408                 goto error;
1409
1410         if (n == 1) {
1411                 free(group);
1412                 return incremental_closure(dim, map, exact, project);
1413         }
1414
1415         grid = isl_calloc_array(map->ctx, isl_map **, n);
1416         if (!grid)
1417                 goto error;
1418         for (i = 0; i < n; ++i) {
1419                 grid[i] = isl_calloc_array(map->ctx, isl_map *, n);
1420                 if (!grid[i])
1421                         goto error;
1422                 for (j = 0; j < n; ++j)
1423                         grid[i][j] = isl_map_empty(isl_map_get_dim(map));
1424         }
1425
1426         for (k = 0; k < map->n; ++k) {
1427                 i = group[2 * k];
1428                 j = group[2 * k + 1];
1429                 grid[i][j] = isl_map_union(grid[i][j],
1430                                 isl_map_from_basic_map(
1431                                         isl_basic_map_copy(map->p[k])));
1432         }
1433
1434         for (r = 0; r < n; ++r) {
1435                 int r_exact;
1436                 grid[r][r] = isl_map_transitive_closure(grid[r][r],
1437                                 (exact && *exact) ? &r_exact : NULL);
1438                 if (exact && *exact && !r_exact)
1439                         *exact = 0;
1440
1441                 for (p = 0; p < n; ++p)
1442                         for (q = 0; q < n; ++q) {
1443                                 isl_map *loop;
1444                                 if (p == r && q == r)
1445                                         continue;
1446                                 loop = isl_map_apply_range(
1447                                                 isl_map_copy(grid[p][r]),
1448                                                 isl_map_copy(grid[r][q]));
1449                                 grid[p][q] = isl_map_union(grid[p][q], loop);
1450                                 loop = isl_map_apply_range(
1451                                                 isl_map_copy(grid[p][r]),
1452                                         isl_map_apply_range(
1453                                                 isl_map_copy(grid[r][r]),
1454                                                 isl_map_copy(grid[r][q])));
1455                                 grid[p][q] = isl_map_union(grid[p][q], loop);
1456                                 grid[p][q] = isl_map_coalesce(grid[p][q]);
1457                         }
1458         }
1459
1460         app = isl_map_empty(isl_map_get_dim(map));
1461
1462         for (i = 0; i < n; ++i) {
1463                 for (j = 0; j < n; ++j)
1464                         app = isl_map_union(app, grid[i][j]);
1465                 free(grid[i]);
1466         }
1467         free(grid);
1468
1469         free(group);
1470         isl_dim_free(dim);
1471
1472         return app;
1473 error:
1474         if (grid)
1475                 for (i = 0; i < n; ++i) {
1476                         if (!grid[i])
1477                                 continue;
1478                         for (j = 0; j < n; ++j)
1479                                 isl_map_free(grid[i][j]);
1480                         free(grid[i]);
1481                 }
1482         free(grid);
1483         free(group);
1484         isl_dim_free(dim);
1485         return NULL;
1486 }
1487
1488 /* Check if the domains and ranges of the basic maps in "map" can
1489  * be partitioned, and if so, apply Floyd-Warshall on the elements
1490  * of the partition.  Note that we can only apply this algorithm
1491  * if we want to compute the transitive closure, i.e., when "project"
1492  * is set.  If we want to compute the power, we need to keep track
1493  * of the lengths and the recursive calls inside the Floyd-Warshall
1494  * would result in non-linear lengths.
1495  *
1496  * To find the partition, we simply consider all of the domains
1497  * and ranges in turn and combine those that overlap.
1498  * "set" contains the partition elements and "group" indicates
1499  * to which partition element a given domain or range belongs.
1500  * The domain of basic map i corresponds to element 2 * i in these arrays,
1501  * while the domain corresponds to element 2 * i + 1.
1502  * During the construction group[k] is either equal to k,
1503  * in which case set[k] contains the union of all the domains and
1504  * ranges in the corresponding group, or is equal to some l < k,
1505  * with l another domain or range in the same group.
1506  */
1507 static __isl_give isl_map *floyd_warshall(__isl_take isl_dim *dim,
1508         __isl_keep isl_map *map, int *exact, int project)
1509 {
1510         int i;
1511         isl_set **set = NULL;
1512         int *group = NULL;
1513         int n;
1514
1515         if (!map)
1516                 goto error;
1517         if (!project || map->n <= 1)
1518                 return incremental_closure(dim, map, exact, project);
1519
1520         set = isl_calloc_array(map->ctx, isl_set *, 2 * map->n);
1521         group = isl_alloc_array(map->ctx, int, 2 * map->n);
1522
1523         if (!set || !group)
1524                 goto error;
1525
1526         for (i = 0; i < map->n; ++i) {
1527                 isl_set *dom;
1528                 dom = isl_set_from_basic_set(isl_basic_map_domain(
1529                                 isl_basic_map_copy(map->p[i])));
1530                 if (merge(set, group, dom, 2 * i) < 0)
1531                         goto error;
1532                 dom = isl_set_from_basic_set(isl_basic_map_range(
1533                                 isl_basic_map_copy(map->p[i])));
1534                 if (merge(set, group, dom, 2 * i + 1) < 0)
1535                         goto error;
1536         }
1537
1538         n = 0;
1539         for (i = 0; i < 2 * map->n; ++i)
1540                 if (group[i] == i)
1541                         group[i] = n++;
1542                 else
1543                         group[i] = group[group[i]];
1544
1545         for (i = 0; i < 2 * map->n; ++i)
1546                 isl_set_free(set[i]);
1547
1548         free(set);
1549
1550         return floyd_warshall_with_groups(dim, map, exact, project, group, n);
1551 error:
1552         for (i = 0; i < 2 * map->n; ++i)
1553                 isl_set_free(set[i]);
1554         free(set);
1555         free(group);
1556         isl_dim_free(dim);
1557         return NULL;
1558 }
1559
1560 /* Structure for representing the nodes in the graph being traversed
1561  * using Tarjan's algorithm.
1562  * index represents the order in which nodes are visited.
1563  * min_index is the index of the root of a (sub)component.
1564  * on_stack indicates whether the node is currently on the stack.
1565  */
1566 struct basic_map_sort_node {
1567         int index;
1568         int min_index;
1569         int on_stack;
1570 };
1571 /* Structure for representing the graph being traversed
1572  * using Tarjan's algorithm.
1573  * len is the number of nodes
1574  * node is an array of nodes
1575  * stack contains the nodes on the path from the root to the current node
1576  * sp is the stack pointer
1577  * index is the index of the last node visited
1578  * order contains the elements of the components separated by -1
1579  * op represents the current position in order
1580  *
1581  * check_closed is set if we may have used the fact that
1582  * a pair of basic maps can be interchanged
1583  */
1584 struct basic_map_sort {
1585         int len;
1586         struct basic_map_sort_node *node;
1587         int *stack;
1588         int sp;
1589         int index;
1590         int *order;
1591         int op;
1592         int check_closed;
1593 };
1594
1595 static void basic_map_sort_free(struct basic_map_sort *s)
1596 {
1597         if (!s)
1598                 return;
1599         free(s->node);
1600         free(s->stack);
1601         free(s->order);
1602         free(s);
1603 }
1604
1605 static struct basic_map_sort *basic_map_sort_alloc(struct isl_ctx *ctx, int len)
1606 {
1607         struct basic_map_sort *s;
1608         int i;
1609
1610         s = isl_calloc_type(ctx, struct basic_map_sort);
1611         if (!s)
1612                 return NULL;
1613         s->len = len;
1614         s->node = isl_alloc_array(ctx, struct basic_map_sort_node, len);
1615         if (!s->node)
1616                 goto error;
1617         for (i = 0; i < len; ++i)
1618                 s->node[i].index = -1;
1619         s->stack = isl_alloc_array(ctx, int, len);
1620         if (!s->stack)
1621                 goto error;
1622         s->order = isl_alloc_array(ctx, int, 2 * len);
1623         if (!s->order)
1624                 goto error;
1625
1626         s->sp = 0;
1627         s->index = 0;
1628         s->op = 0;
1629
1630         s->check_closed = 0;
1631
1632         return s;
1633 error:
1634         basic_map_sort_free(s);
1635         return NULL;
1636 }
1637
1638 /* Check whether in the computation of the transitive closure
1639  * "bmap1" (R_1) should follow (or be part of the same component as)
1640  * "bmap2" (R_2).
1641  *
1642  * That is check whether
1643  *
1644  *      R_1 \circ R_2
1645  *
1646  * is a subset of
1647  *
1648  *      R_2 \circ R_1
1649  *
1650  * If so, then there is no reason for R_1 to immediately follow R_2
1651  * in any path.
1652  *
1653  * *check_closed is set if the subset relation holds while
1654  * R_1 \circ R_2 is not empty.
1655  */
1656 static int basic_map_follows(__isl_keep isl_basic_map *bmap1,
1657         __isl_keep isl_basic_map *bmap2, int *check_closed)
1658 {
1659         struct isl_map *map12 = NULL;
1660         struct isl_map *map21 = NULL;
1661         int subset;
1662
1663         map21 = isl_map_from_basic_map(
1664                         isl_basic_map_apply_range(
1665                                 isl_basic_map_copy(bmap2),
1666                                 isl_basic_map_copy(bmap1)));
1667         subset = isl_map_is_empty(map21);
1668         if (subset < 0)
1669                 goto error;
1670         if (subset) {
1671                 isl_map_free(map21);
1672                 return 0;
1673         }
1674
1675         map12 = isl_map_from_basic_map(
1676                         isl_basic_map_apply_range(
1677                                 isl_basic_map_copy(bmap1),
1678                                 isl_basic_map_copy(bmap2)));
1679
1680         subset = isl_map_is_subset(map21, map12);
1681
1682         isl_map_free(map12);
1683         isl_map_free(map21);
1684
1685         if (subset)
1686                 *check_closed = 1;
1687
1688         return subset < 0 ? -1 : !subset;
1689 error:
1690         isl_map_free(map21);
1691         return -1;
1692 }
1693
1694 /* Perform Tarjan's algorithm for computing the strongly connected components
1695  * in the graph with the disjuncts of "map" as vertices and with an
1696  * edge between any pair of disjuncts such that the first has
1697  * to be applied after the second.
1698  */
1699 static int power_components_tarjan(struct basic_map_sort *s,
1700         __isl_keep isl_map *map, int i)
1701 {
1702         int j;
1703
1704         s->node[i].index = s->index;
1705         s->node[i].min_index = s->index;
1706         s->node[i].on_stack = 1;
1707         s->index++;
1708         s->stack[s->sp++] = i;
1709
1710         for (j = s->len - 1; j >= 0; --j) {
1711                 int f;
1712
1713                 if (j == i)
1714                         continue;
1715                 if (s->node[j].index >= 0 &&
1716                         (!s->node[j].on_stack ||
1717                          s->node[j].index > s->node[i].min_index))
1718                         continue;
1719
1720                 f = basic_map_follows(map->p[i], map->p[j], &s->check_closed);
1721                 if (f < 0)
1722                         return -1;
1723                 if (!f)
1724                         continue;
1725
1726                 if (s->node[j].index < 0) {
1727                         power_components_tarjan(s, map, j);
1728                         if (s->node[j].min_index < s->node[i].min_index)
1729                                 s->node[i].min_index = s->node[j].min_index;
1730                 } else if (s->node[j].index < s->node[i].min_index)
1731                         s->node[i].min_index = s->node[j].index;
1732         }
1733
1734         if (s->node[i].index != s->node[i].min_index)
1735                 return 0;
1736
1737         do {
1738                 j = s->stack[--s->sp];
1739                 s->node[j].on_stack = 0;
1740                 s->order[s->op++] = j;
1741         } while (j != i);
1742         s->order[s->op++] = -1;
1743
1744         return 0;
1745 }
1746
1747 /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D
1748  * and a dimension specification (Z^{n+1} -> Z^{n+1}),
1749  * construct a map that is an overapproximation of the map
1750  * that takes an element from the dom R \times Z to an
1751  * element from ran R \times Z, such that the first n coordinates of the
1752  * difference between them is a sum of differences between images
1753  * and pre-images in one of the R_i and such that the last coordinate
1754  * is equal to the number of steps taken.
1755  * If "project" is set, then these final coordinates are not included,
1756  * i.e., a relation of type Z^n -> Z^n is returned.
1757  * That is, let
1758  *
1759  *      \Delta_i = { y - x | (x, y) in R_i }
1760  *
1761  * then the constructed map is an overapproximation of
1762  *
1763  *      { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i :
1764  *                              d = (\sum_i k_i \delta_i, \sum_i k_i) and
1765  *                              x in dom R and x + d in ran R }
1766  *
1767  * or
1768  *
1769  *      { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i :
1770  *                              d = (\sum_i k_i \delta_i) and
1771  *                              x in dom R and x + d in ran R }
1772  *
1773  * if "project" is set.
1774  *
1775  * We first split the map into strongly connected components, perform
1776  * the above on each component and then join the results in the correct
1777  * order, at each join also taking in the union of both arguments
1778  * to allow for paths that do not go through one of the two arguments.
1779  */
1780 static __isl_give isl_map *construct_power_components(__isl_take isl_dim *dim,
1781         __isl_keep isl_map *map, int *exact, int project)
1782 {
1783         int i, n, c;
1784         struct isl_map *path = NULL;
1785         struct basic_map_sort *s = NULL;
1786         int *orig_exact;
1787         int local_exact;
1788
1789         if (!map)
1790                 goto error;
1791         if (map->n <= 1)
1792                 return floyd_warshall(dim, map, exact, project);
1793
1794         s = basic_map_sort_alloc(map->ctx, map->n);
1795         if (!s)
1796                 goto error;
1797         for (i = map->n - 1; i >= 0; --i) {
1798                 if (s->node[i].index >= 0)
1799                         continue;
1800                 if (power_components_tarjan(s, map, i) < 0)
1801                         goto error;
1802         }
1803
1804         orig_exact = exact;
1805         if (s->check_closed && !exact)
1806                 exact = &local_exact;
1807
1808         c = 0;
1809         i = 0;
1810         n = map->n;
1811         if (project)
1812                 path = isl_map_empty(isl_map_get_dim(map));
1813         else
1814                 path = isl_map_empty(isl_dim_copy(dim));
1815         while (n) {
1816                 struct isl_map *comp;
1817                 isl_map *path_comp, *path_comb;
1818                 comp = isl_map_alloc_dim(isl_map_get_dim(map), n, 0);
1819                 while (s->order[i] != -1) {
1820                         comp = isl_map_add_basic_map(comp,
1821                                     isl_basic_map_copy(map->p[s->order[i]]));
1822                         --n;
1823                         ++i;
1824                 }
1825                 path_comp = floyd_warshall(isl_dim_copy(dim),
1826                                                 comp, exact, project);
1827                 path_comb = isl_map_apply_range(isl_map_copy(path),
1828                                                 isl_map_copy(path_comp));
1829                 path = isl_map_union(path, path_comp);
1830                 path = isl_map_union(path, path_comb);
1831                 isl_map_free(comp);
1832                 ++i;
1833                 ++c;
1834         }
1835
1836         if (c > 1 && s->check_closed && !*exact) {
1837                 int closed;
1838
1839                 closed = isl_map_is_transitively_closed(path);
1840                 if (closed < 0)
1841                         goto error;
1842                 if (!closed) {
1843                         basic_map_sort_free(s);
1844                         isl_map_free(path);
1845                         return floyd_warshall(dim, map, orig_exact, project);
1846                 }
1847         }
1848
1849         basic_map_sort_free(s);
1850         isl_dim_free(dim);
1851
1852         return path;
1853 error:
1854         basic_map_sort_free(s);
1855         isl_dim_free(dim);
1856         isl_map_free(path);
1857         return NULL;
1858 }
1859
1860 /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D,
1861  * construct a map that is an overapproximation of the map
1862  * that takes an element from the space D to another
1863  * element from the same space, such that the difference between
1864  * them is a strictly positive sum of differences between images
1865  * and pre-images in one of the R_i.
1866  * The number of differences in the sum is equated to parameter "param".
1867  * That is, let
1868  *
1869  *      \Delta_i = { y - x | (x, y) in R_i }
1870  *
1871  * then the constructed map is an overapproximation of
1872  *
1873  *      { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i :
1874  *                              d = \sum_i k_i \delta_i and k = \sum_i k_i > 0 }
1875  * or
1876  *
1877  *      { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i :
1878  *                              d = \sum_i k_i \delta_i and \sum_i k_i > 0 }
1879  *
1880  * if "project" is set.
1881  *
1882  * If "project" is not set, then
1883  * we first construct an extended mapping with an extra coordinate
1884  * that indicates the number of steps taken.  In particular,
1885  * the difference in the last coordinate is equal to the number
1886  * of steps taken to move from a domain element to the corresponding
1887  * image element(s).
1888  * In the final step, this difference is equated to the parameter "param"
1889  * and made positive.  The extra coordinates are subsequently projected out.
1890  */
1891 static __isl_give isl_map *construct_power(__isl_keep isl_map *map,
1892         unsigned param, int *exact, int project)
1893 {
1894         struct isl_map *app = NULL;
1895         struct isl_map *diff;
1896         struct isl_dim *dim = NULL;
1897         unsigned d;
1898
1899         if (!map)
1900                 return NULL;
1901
1902         dim = isl_map_get_dim(map);
1903
1904         d = isl_dim_size(dim, isl_dim_in);
1905         dim = isl_dim_add(dim, isl_dim_in, 1);
1906         dim = isl_dim_add(dim, isl_dim_out, 1);
1907
1908         app = construct_power_components(isl_dim_copy(dim), map,
1909                                         exact, project);
1910
1911         if (project) {
1912                 isl_dim_free(dim);
1913         } else {
1914                 diff = equate_parameter_to_length(dim, param);
1915                 app = isl_map_intersect(app, diff);
1916                 app = isl_map_project_out(app, isl_dim_in, d, 1);
1917                 app = isl_map_project_out(app, isl_dim_out, d, 1);
1918         }
1919
1920         return app;
1921 }
1922
1923 /* Compute the positive powers of "map", or an overapproximation.
1924  * The power is given by parameter "param".  If the result is exact,
1925  * then *exact is set to 1.
1926  *
1927  * If project is set, then we are actually interested in the transitive
1928  * closure, so we can use a more relaxed exactness check.
1929  * The lengths of the paths are also projected out instead of being
1930  * equated to "param" (which is then ignored in this case).
1931  */
1932 static __isl_give isl_map *map_power(__isl_take isl_map *map, unsigned param,
1933         int *exact, int project)
1934 {
1935         struct isl_map *app = NULL;
1936
1937         if (exact)
1938                 *exact = 1;
1939
1940         if (!map)
1941                 return NULL;
1942
1943         if (isl_map_fast_is_empty(map))
1944                 return map;
1945
1946         isl_assert(map->ctx, project || param < isl_map_dim(map, isl_dim_param),
1947                 goto error);
1948         isl_assert(map->ctx,
1949                 isl_map_dim(map, isl_dim_in) == isl_map_dim(map, isl_dim_out),
1950                 goto error);
1951
1952         app = construct_power(map, param, exact, project);
1953
1954         isl_map_free(map);
1955         return app;
1956 error:
1957         isl_map_free(map);
1958         isl_map_free(app);
1959         return NULL;
1960 }
1961
1962 /* Compute the positive powers of "map", or an overapproximation.
1963  * The power is given by parameter "param".  If the result is exact,
1964  * then *exact is set to 1.
1965  */
1966 __isl_give isl_map *isl_map_power(__isl_take isl_map *map, unsigned param,
1967         int *exact)
1968 {
1969         map = isl_map_compute_divs(map);
1970         map = isl_map_coalesce(map);
1971         return map_power(map, param, exact, 0);
1972 }
1973
1974 /* Check whether equality i of bset is a pure stride constraint
1975  * on a single dimensions, i.e., of the form
1976  *
1977  *      v = k e
1978  *
1979  * with k a constant and e an existentially quantified variable.
1980  */
1981 static int is_eq_stride(__isl_keep isl_basic_set *bset, int i)
1982 {
1983         int k;
1984         unsigned nparam;
1985         unsigned d;
1986         unsigned n_div;
1987         int pos1;
1988         int pos2;
1989
1990         if (!bset)
1991                 return -1;
1992
1993         if (!isl_int_is_zero(bset->eq[i][0]))
1994                 return 0;
1995
1996         nparam = isl_basic_set_dim(bset, isl_dim_param);
1997         d = isl_basic_set_dim(bset, isl_dim_set);
1998         n_div = isl_basic_set_dim(bset, isl_dim_div);
1999
2000         if (isl_seq_first_non_zero(bset->eq[i] + 1, nparam) != -1)
2001                 return 0;
2002         pos1 = isl_seq_first_non_zero(bset->eq[i] + 1 + nparam, d);
2003         if (pos1 == -1)
2004                 return 0;
2005         if (isl_seq_first_non_zero(bset->eq[i] + 1 + nparam + pos1 + 1, 
2006                                         d - pos1 - 1) != -1)
2007                 return 0;
2008
2009         pos2 = isl_seq_first_non_zero(bset->eq[i] + 1 + nparam + d, n_div);
2010         if (pos2 == -1)
2011                 return 0;
2012         if (isl_seq_first_non_zero(bset->eq[i] + 1 + nparam + d  + pos2 + 1,
2013                                    n_div - pos2 - 1) != -1)
2014                 return 0;
2015         if (!isl_int_is_one(bset->eq[i][1 + nparam + pos1]) &&
2016             !isl_int_is_negone(bset->eq[i][1 + nparam + pos1]))
2017                 return 0;
2018
2019         return 1;
2020 }
2021
2022 /* Given a map, compute the smallest superset of this map that is of the form
2023  *
2024  *      { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p }
2025  *
2026  * (where p ranges over the (non-parametric) dimensions),
2027  * compute the transitive closure of this map, i.e.,
2028  *
2029  *      { i -> j : exists k > 0:
2030  *              k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p }
2031  *
2032  * and intersect domain and range of this transitive closure with
2033  * the given domain and range.
2034  *
2035  * If with_id is set, then try to include as much of the identity mapping
2036  * as possible, by computing
2037  *
2038  *      { i -> j : exists k >= 0:
2039  *              k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p }
2040  *
2041  * instead (i.e., allow k = 0).
2042  *
2043  * In practice, we compute the difference set
2044  *
2045  *      delta  = { j - i | i -> j in map },
2046  *
2047  * look for stride constraint on the individual dimensions and compute
2048  * (constant) lower and upper bounds for each individual dimension,
2049  * adding a constraint for each bound not equal to infinity.
2050  */
2051 static __isl_give isl_map *box_closure_on_domain(__isl_take isl_map *map,
2052         __isl_take isl_set *dom, __isl_take isl_set *ran, int with_id)
2053 {
2054         int i;
2055         int k;
2056         unsigned d;
2057         unsigned nparam;
2058         unsigned total;
2059         isl_dim *dim;
2060         isl_set *delta;
2061         isl_map *app = NULL;
2062         isl_basic_set *aff = NULL;
2063         isl_basic_map *bmap = NULL;
2064         isl_vec *obj = NULL;
2065         isl_int opt;
2066
2067         isl_int_init(opt);
2068
2069         delta = isl_map_deltas(isl_map_copy(map));
2070
2071         aff = isl_set_affine_hull(isl_set_copy(delta));
2072         if (!aff)
2073                 goto error;
2074         dim = isl_map_get_dim(map);
2075         d = isl_dim_size(dim, isl_dim_in);
2076         nparam = isl_dim_size(dim, isl_dim_param);
2077         total = isl_dim_total(dim);
2078         bmap = isl_basic_map_alloc_dim(dim,
2079                                         aff->n_div + 1, aff->n_div, 2 * d + 1);
2080         for (i = 0; i < aff->n_div + 1; ++i) {
2081                 k = isl_basic_map_alloc_div(bmap);
2082                 if (k < 0)
2083                         goto error;
2084                 isl_int_set_si(bmap->div[k][0], 0);
2085         }
2086         for (i = 0; i < aff->n_eq; ++i) {
2087                 if (!is_eq_stride(aff, i))
2088                         continue;
2089                 k = isl_basic_map_alloc_equality(bmap);
2090                 if (k < 0)
2091                         goto error;
2092                 isl_seq_clr(bmap->eq[k], 1 + nparam);
2093                 isl_seq_cpy(bmap->eq[k] + 1 + nparam + d,
2094                                 aff->eq[i] + 1 + nparam, d);
2095                 isl_seq_neg(bmap->eq[k] + 1 + nparam,
2096                                 aff->eq[i] + 1 + nparam, d);
2097                 isl_seq_cpy(bmap->eq[k] + 1 + nparam + 2 * d,
2098                                 aff->eq[i] + 1 + nparam + d, aff->n_div);
2099                 isl_int_set_si(bmap->eq[k][1 + total + aff->n_div], 0);
2100         }
2101         obj = isl_vec_alloc(map->ctx, 1 + nparam + d);
2102         if (!obj)
2103                 goto error;
2104         isl_seq_clr(obj->el, 1 + nparam + d);
2105         for (i = 0; i < d; ++ i) {
2106                 enum isl_lp_result res;
2107
2108                 isl_int_set_si(obj->el[1 + nparam + i], 1);
2109
2110                 res = isl_set_solve_lp(delta, 0, obj->el, map->ctx->one, &opt,
2111                                         NULL, NULL);
2112                 if (res == isl_lp_error)
2113                         goto error;
2114                 if (res == isl_lp_ok) {
2115                         k = isl_basic_map_alloc_inequality(bmap);
2116                         if (k < 0)
2117                                 goto error;
2118                         isl_seq_clr(bmap->ineq[k],
2119                                         1 + nparam + 2 * d + bmap->n_div);
2120                         isl_int_set_si(bmap->ineq[k][1 + nparam + i], -1);
2121                         isl_int_set_si(bmap->ineq[k][1 + nparam + d + i], 1);
2122                         isl_int_neg(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div], opt);
2123                 }
2124
2125                 res = isl_set_solve_lp(delta, 1, obj->el, map->ctx->one, &opt,
2126                                         NULL, NULL);
2127                 if (res == isl_lp_error)
2128                         goto error;
2129                 if (res == isl_lp_ok) {
2130                         k = isl_basic_map_alloc_inequality(bmap);
2131                         if (k < 0)
2132                                 goto error;
2133                         isl_seq_clr(bmap->ineq[k],
2134                                         1 + nparam + 2 * d + bmap->n_div);
2135                         isl_int_set_si(bmap->ineq[k][1 + nparam + i], 1);
2136                         isl_int_set_si(bmap->ineq[k][1 + nparam + d + i], -1);
2137                         isl_int_set(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div], opt);
2138                 }
2139
2140                 isl_int_set_si(obj->el[1 + nparam + i], 0);
2141         }
2142         k = isl_basic_map_alloc_inequality(bmap);
2143         if (k < 0)
2144                 goto error;
2145         isl_seq_clr(bmap->ineq[k],
2146                         1 + nparam + 2 * d + bmap->n_div);
2147         if (!with_id)
2148                 isl_int_set_si(bmap->ineq[k][0], -1);
2149         isl_int_set_si(bmap->ineq[k][1 + nparam + 2 * d + aff->n_div], 1);
2150
2151         app = isl_map_from_domain_and_range(dom, ran);
2152
2153         isl_vec_free(obj);
2154         isl_basic_set_free(aff);
2155         isl_map_free(map);
2156         bmap = isl_basic_map_finalize(bmap);
2157         isl_set_free(delta);
2158         isl_int_clear(opt);
2159
2160         map = isl_map_from_basic_map(bmap);
2161         map = isl_map_intersect(map, app);
2162
2163         return map;
2164 error:
2165         isl_vec_free(obj);
2166         isl_basic_map_free(bmap);
2167         isl_basic_set_free(aff);
2168         isl_set_free(dom);
2169         isl_set_free(ran);
2170         isl_map_free(map);
2171         isl_set_free(delta);
2172         isl_int_clear(opt);
2173         return NULL;
2174 }
2175
2176 /* Given a map, compute the smallest superset of this map that is of the form
2177  *
2178  *      { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p }
2179  *
2180  * (where p ranges over the (non-parametric) dimensions),
2181  * compute the transitive closure of this map, i.e.,
2182  *
2183  *      { i -> j : exists k > 0:
2184  *              k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p }
2185  *
2186  * and intersect domain and range of this transitive closure with
2187  * domain and range of the original map.
2188  */
2189 static __isl_give isl_map *box_closure(__isl_take isl_map *map)
2190 {
2191         isl_set *domain;
2192         isl_set *range;
2193
2194         domain = isl_map_domain(isl_map_copy(map));
2195         domain = isl_set_coalesce(domain);
2196         range = isl_map_range(isl_map_copy(map));
2197         range = isl_set_coalesce(range);
2198
2199         return box_closure_on_domain(map, domain, range, 0);
2200 }
2201
2202 /* Given a map, compute the smallest superset of this map that is of the form
2203  *
2204  *      { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p }
2205  *
2206  * (where p ranges over the (non-parametric) dimensions),
2207  * compute the transitive and partially reflexive closure of this map, i.e.,
2208  *
2209  *      { i -> j : exists k >= 0:
2210  *              k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p }
2211  *
2212  * and intersect domain and range of this transitive closure with
2213  * the given domain.
2214  */
2215 static __isl_give isl_map *box_closure_with_identity(__isl_take isl_map *map,
2216         __isl_take isl_set *dom)
2217 {
2218         return box_closure_on_domain(map, dom, isl_set_copy(dom), 1);
2219 }
2220
2221 /* Check whether app is the transitive closure of map.
2222  * In particular, check that app is acyclic and, if so,
2223  * check that
2224  *
2225  *      app \subset (map \cup (map \circ app))
2226  */
2227 static int check_exactness_omega(__isl_keep isl_map *map,
2228         __isl_keep isl_map *app)
2229 {
2230         isl_set *delta;
2231         int i;
2232         int is_empty, is_exact;
2233         unsigned d;
2234         isl_map *test;
2235
2236         delta = isl_map_deltas(isl_map_copy(app));
2237         d = isl_set_dim(delta, isl_dim_set);
2238         for (i = 0; i < d; ++i)
2239                 delta = isl_set_fix_si(delta, isl_dim_set, i, 0);
2240         is_empty = isl_set_is_empty(delta);
2241         isl_set_free(delta);
2242         if (is_empty < 0)
2243                 return -1;
2244         if (!is_empty)
2245                 return 0;
2246
2247         test = isl_map_apply_range(isl_map_copy(app), isl_map_copy(map));
2248         test = isl_map_union(test, isl_map_copy(map));
2249         is_exact = isl_map_is_subset(app, test);
2250         isl_map_free(test);
2251
2252         return is_exact;
2253 }
2254
2255 /* Check if basic map M_i can be combined with all the other
2256  * basic maps such that
2257  *
2258  *      (\cup_j M_j)^+
2259  *
2260  * can be computed as
2261  *
2262  *      M_i \cup (\cup_{j \ne i} M_i^* \circ M_j \circ M_i^*)^+
2263  *
2264  * In particular, check if we can compute a compact representation
2265  * of
2266  *
2267  *              M_i^* \circ M_j \circ M_i^*
2268  *
2269  * for each j != i.
2270  * Let M_i^? be an extension of M_i^+ that allows paths
2271  * of length zero, i.e., the result of box_closure(., 1).
2272  * The criterion, as proposed by Kelly et al., is that
2273  * id = M_i^? - M_i^+ can be represented as a basic map
2274  * and that
2275  *
2276  *      id \circ M_j \circ id = M_j
2277  *
2278  * for each j != i.
2279  *
2280  * If this function returns 1, then tc and qc are set to
2281  * M_i^+ and M_i^?, respectively.
2282  */
2283 static int can_be_split_off(__isl_keep isl_map *map, int i,
2284         __isl_give isl_map **tc, __isl_give isl_map **qc)
2285 {
2286         isl_map *map_i, *id = NULL;
2287         int j = -1;
2288         isl_set *C;
2289
2290         *tc = NULL;
2291         *qc = NULL;
2292
2293         C = isl_set_union(isl_map_domain(isl_map_copy(map)),
2294                           isl_map_range(isl_map_copy(map)));
2295         C = isl_set_from_basic_set(isl_set_simple_hull(C));
2296         if (!C)
2297                 goto error;
2298
2299         map_i = isl_map_from_basic_map(isl_basic_map_copy(map->p[i]));
2300         *tc = box_closure(isl_map_copy(map_i));
2301         *qc = box_closure_with_identity(map_i, C);
2302         id = isl_map_subtract(isl_map_copy(*qc), isl_map_copy(*tc));
2303
2304         if (!id || !*qc)
2305                 goto error;
2306         if (id->n != 1 || (*qc)->n != 1)
2307                 goto done;
2308
2309         for (j = 0; j < map->n; ++j) {
2310                 isl_map *map_j, *test;
2311                 int is_ok;
2312
2313                 if (i == j)
2314                         continue;
2315                 map_j = isl_map_from_basic_map(
2316                                         isl_basic_map_copy(map->p[j]));
2317                 test = isl_map_apply_range(isl_map_copy(id),
2318                                                 isl_map_copy(map_j));
2319                 test = isl_map_apply_range(test, isl_map_copy(id));
2320                 is_ok = isl_map_is_equal(test, map_j);
2321                 isl_map_free(map_j);
2322                 isl_map_free(test);
2323                 if (is_ok < 0)
2324                         goto error;
2325                 if (!is_ok)
2326                         break;
2327         }
2328
2329 done:
2330         isl_map_free(id);
2331         if (j == map->n)
2332                 return 1;
2333
2334         isl_map_free(*qc);
2335         isl_map_free(*tc);
2336         *qc = NULL;
2337         *tc = NULL;
2338
2339         return 0;
2340 error:
2341         isl_map_free(id);
2342         isl_map_free(*qc);
2343         isl_map_free(*tc);
2344         *qc = NULL;
2345         *tc = NULL;
2346         return -1;
2347 }
2348
2349 static __isl_give isl_map *box_closure_with_check(__isl_take isl_map *map,
2350         int *exact)
2351 {
2352         isl_map *app;
2353
2354         app = box_closure(isl_map_copy(map));
2355         if (exact)
2356                 *exact = check_exactness_omega(map, app);
2357
2358         isl_map_free(map);
2359         return app;
2360 }
2361
2362 /* Compute an overapproximation of the transitive closure of "map"
2363  * using a variation of the algorithm from
2364  * "Transitive Closure of Infinite Graphs and its Applications"
2365  * by Kelly et al.
2366  *
2367  * We first check whether we can can split of any basic map M_i and
2368  * compute
2369  *
2370  *      (\cup_j M_j)^+
2371  *
2372  * as
2373  *
2374  *      M_i \cup (\cup_{j \ne i} M_i^* \circ M_j \circ M_i^*)^+
2375  *
2376  * using a recursive call on the remaining map.
2377  *
2378  * If not, we simply call box_closure on the whole map.
2379  */
2380 static __isl_give isl_map *transitive_closure_omega(__isl_take isl_map *map,
2381         int *exact)
2382 {
2383         int i, j;
2384         int exact_i;
2385         isl_map *app;
2386
2387         if (!map)
2388                 return NULL;
2389         if (map->n == 1)
2390                 return box_closure_with_check(map, exact);
2391
2392         for (i = 0; i < map->n; ++i) {
2393                 int ok;
2394                 isl_map *qc, *tc;
2395                 ok = can_be_split_off(map, i, &tc, &qc);
2396                 if (ok < 0)
2397                         goto error;
2398                 if (!ok)
2399                         continue;
2400
2401                 app = isl_map_alloc_dim(isl_map_get_dim(map), map->n - 1, 0);
2402
2403                 for (j = 0; j < map->n; ++j) {
2404                         if (j == i)
2405                                 continue;
2406                         app = isl_map_add_basic_map(app,
2407                                                 isl_basic_map_copy(map->p[j]));
2408                 }
2409
2410                 app = isl_map_apply_range(isl_map_copy(qc), app);
2411                 app = isl_map_apply_range(app, qc);
2412
2413                 app = isl_map_union(tc, transitive_closure_omega(app, NULL));
2414                 exact_i = check_exactness_omega(map, app);
2415                 if (exact_i == 1) {
2416                         if (exact)
2417                                 *exact = exact_i;
2418                         isl_map_free(map);
2419                         return app;
2420                 }
2421                 isl_map_free(app);
2422                 if (exact_i < 0)
2423                         goto error;
2424         }
2425
2426         return box_closure_with_check(map, exact);
2427 error:
2428         isl_map_free(map);
2429         return NULL;
2430 }
2431
2432 /* Compute the transitive closure  of "map", or an overapproximation.
2433  * If the result is exact, then *exact is set to 1.
2434  * Simply use map_power to compute the powers of map, but tell
2435  * it to project out the lengths of the paths instead of equating
2436  * the length to a parameter.
2437  */
2438 __isl_give isl_map *isl_map_transitive_closure(__isl_take isl_map *map,
2439         int *exact)
2440 {
2441         unsigned param;
2442         int closed;
2443
2444         if (!map)
2445                 goto error;
2446
2447         if (map->ctx->opt->closure == ISL_CLOSURE_OMEGA)
2448                 return transitive_closure_omega(map, exact);
2449
2450         map = isl_map_compute_divs(map);
2451         map = isl_map_coalesce(map);
2452         closed = isl_map_is_transitively_closed(map);
2453         if (closed < 0)
2454                 goto error;
2455         if (closed) {
2456                 if (exact)
2457                         *exact = 1;
2458                 return map;
2459         }
2460
2461         param = isl_map_dim(map, isl_dim_param);
2462         map = map_power(map, param, exact, 1);
2463
2464         return map;
2465 error:
2466         isl_map_free(map);
2467         return NULL;
2468 }