?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
add isl_map_copy_basic_map and isl_map_drop_basic_map
[isl.git] / isl_map_simplify.c
blobd1c23d2a16f7c5ebecde3e332e9b1eb70e5a28eb
1 #include "isl_equalities.h"
2 #include "isl_map.h"
3 #include "isl_map_private.h"
4
5 static void swap_equality(struct isl_basic_map *bmap, int a, int b)
6 {
7 isl_int *t = bmap->eq[a];
8 bmap->eq[a] = bmap->eq[b];
9 bmap->eq[b] = t;
10 }
11
12 static void swap_inequality(struct isl_basic_map *bmap, int a, int b)
13 {
14 if (a != b) {
15 isl_int *t = bmap->ineq[a];
16 bmap->ineq[a] = bmap->ineq[b];
17 bmap->ineq[b] = t;
18 }
19 }
20
21 static void set_swap_inequality(struct isl_basic_set *bset, int a, int b)
22 {
23 swap_inequality((struct isl_basic_map *)bset, a, b);
24 }
25
26 static void constraint_drop_vars(isl_int *c, unsigned n, unsigned rem)
27 {
28 isl_seq_cpy(c, c + n, rem);
29 isl_seq_clr(c + rem, n);
30 }
31
32 /* Drop n dimensions starting at first.
33 *
34 * In principle, this frees up some extra variables as the number
35 * of columns remains constant, but we would have to extend
36 * the div array too as the number of rows in this array is assumed
37 * to be equal to extra.
38 */
39 struct isl_basic_set *isl_basic_set_drop_dims(
40 struct isl_basic_set *bset, unsigned first, unsigned n)
41 {
42 int i;
43
44 if (!bset)
45 goto error;
46
47 isl_assert(bset->ctx, first + n <= bset->dim->n_out, goto error);
48
49 if (n == 0)
50 return bset;
51
52 bset = isl_basic_set_cow(bset);
53 if (!bset)
54 return NULL;
55
56 for (i = 0; i < bset->n_eq; ++i)
57 constraint_drop_vars(bset->eq[i]+1+bset->dim->nparam+first, n,
58 (bset->dim->n_out-first-n)+bset->extra);
59
60 for (i = 0; i < bset->n_ineq; ++i)
61 constraint_drop_vars(bset->ineq[i]+1+bset->dim->nparam+first, n,
62 (bset->dim->n_out-first-n)+bset->extra);
63
64 for (i = 0; i < bset->n_div; ++i)
65 constraint_drop_vars(bset->div[i]+1+1+bset->dim->nparam+first, n,
66 (bset->dim->n_out-first-n)+bset->extra);
67
68 bset->dim = isl_dim_drop_outputs(bset->dim, first, n);
69 if (!bset->dim)
70 goto error;
71
72 F_CLR(bset, ISL_BASIC_SET_NORMALIZED);
73 bset = isl_basic_set_simplify(bset);
74 return isl_basic_set_finalize(bset);
75 error:
76 isl_basic_set_free(bset);
77 return NULL;
78 }
79
80 struct isl_set *isl_set_drop_dims(
81 struct isl_set *set, unsigned first, unsigned n)
82 {
83 int i;
84
85 if (!set)
86 goto error;
87
88 isl_assert(set->ctx, first + n <= set->dim->n_out, goto error);
89
90 if (n == 0)
91 return set;
92 set = isl_set_cow(set);
93 if (!set)
94 goto error;
95 set->dim = isl_dim_drop_outputs(set->dim, first, n);
96 if (!set->dim)
97 goto error;
98
99 for (i = 0; i < set->n; ++i) {
100 set->p[i] = isl_basic_set_drop_dims(set->p[i], first, n);
101 if (!set->p[i])
102 goto error;
103 }
104
105 F_CLR(set, ISL_SET_NORMALIZED);
106 return set;
107 error:
108 isl_set_free(set);
109 return NULL;
110 }
111
112 /* Drop n input dimensions starting at first.
113 *
114 * In principle, this frees up some extra variables as the number
115 * of columns remains constant, but we would have to extend
116 * the div array too as the number of rows in this array is assumed
117 * to be equal to extra.
118 */
119 struct isl_basic_map *isl_basic_map_drop_inputs(
120 struct isl_basic_map *bmap, unsigned first, unsigned n)
121 {
122 int i;
123 unsigned nparam;
124 unsigned n_in;
125 unsigned n_out;
126
127 if (!bmap)
128 goto error;
129
130 nparam = isl_basic_map_n_param(bmap);
131 n_in = isl_basic_map_n_in(bmap);
132 n_out = isl_basic_map_n_out(bmap);
133 isl_assert(bmap->ctx, first + n <= n_in, goto error);
134
135 if (n == 0)
136 return bmap;
137
138 bmap = isl_basic_map_cow(bmap);
139 if (!bmap)
140 return NULL;
141
142 for (i = 0; i < bmap->n_eq; ++i)
143 constraint_drop_vars(bmap->eq[i]+1+nparam+first, n,
144 (n_in-first-n)+n_out+bmap->extra);
145
146 for (i = 0; i < bmap->n_ineq; ++i)
147 constraint_drop_vars(bmap->ineq[i]+1+nparam+first, n,
148 (n_in-first-n)+n_out+bmap->extra);
149
150 for (i = 0; i < bmap->n_div; ++i)
151 constraint_drop_vars(bmap->div[i]+1+1+nparam+first, n,
152 (n_in-first-n)+n_out+bmap->extra);
153
154 bmap->dim = isl_dim_drop_inputs(bmap->dim, first, n);
155 if (!bmap->dim)
156 goto error;
157
158 F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
159 bmap = isl_basic_map_simplify(bmap);
160 return isl_basic_map_finalize(bmap);
161 error:
162 isl_basic_map_free(bmap);
163 return NULL;
164 }
165
166 struct isl_map *isl_map_drop_inputs(
167 struct isl_map *map, unsigned first, unsigned n)
168 {
169 int i;
170
171 if (!map)
172 goto error;
173
174 isl_assert(map->ctx, first + n <= map->dim->n_in, goto error);
175
176 if (n == 0)
177 return map;
178 map = isl_map_cow(map);
179 if (!map)
180 goto error;
181 map->dim = isl_dim_drop_inputs(map->dim, first, n);
182 if (!map->dim)
183 goto error;
184
185 for (i = 0; i < map->n; ++i) {
186 map->p[i] = isl_basic_map_drop_inputs(map->p[i], first, n);
187 if (!map->p[i])
188 goto error;
189 }
190 F_CLR(map, ISL_MAP_NORMALIZED);
191
192 return map;
193 error:
194 isl_map_free(map);
195 return NULL;
196 }
197
198 /*
199 * We don't cow, as the div is assumed to be redundant.
200 */
201 static struct isl_basic_map *isl_basic_map_drop_div(
202 struct isl_basic_map *bmap, unsigned div)
203 {
204 int i;
205 unsigned pos;
206
207 if (!bmap)
208 goto error;
209
210 pos = 1 + isl_dim_total(bmap->dim) + div;
211
212 isl_assert(bmap->ctx, div < bmap->n_div, goto error);
213
214 for (i = 0; i < bmap->n_eq; ++i)
215 constraint_drop_vars(bmap->eq[i]+pos, 1, bmap->extra-div-1);
216
217 for (i = 0; i < bmap->n_ineq; ++i) {
218 if (!isl_int_is_zero(bmap->ineq[i][pos])) {
219 isl_basic_map_drop_inequality(bmap, i);
220 --i;
221 continue;
222 }
223 constraint_drop_vars(bmap->ineq[i]+pos, 1, bmap->extra-div-1);
224 }
225
226 for (i = 0; i < bmap->n_div; ++i)
227 constraint_drop_vars(bmap->div[i]+1+pos, 1, bmap->extra-div-1);
228
229 if (div != bmap->n_div - 1) {
230 int j;
231 isl_int *t = bmap->div[div];
232
233 for (j = div; j < bmap->n_div - 1; ++j)
234 bmap->div[j] = bmap->div[j+1];
235
236 bmap->div[bmap->n_div - 1] = t;
237 }
238 F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
239 isl_basic_map_free_div(bmap, 1);
240
241 return bmap;
242 error:
243 isl_basic_map_free(bmap);
244 return NULL;
245 }
246
247 static struct isl_basic_map *normalize_constraints(struct isl_basic_map *bmap)
248 {
249 int i;
250 isl_int gcd;
251 unsigned total = isl_basic_map_total_dim(bmap);
252
253 isl_int_init(gcd);
254 for (i = bmap->n_eq - 1; i >= 0; --i) {
255 isl_seq_gcd(bmap->eq[i]+1, total, &gcd);
256 if (isl_int_is_zero(gcd)) {
257 if (!isl_int_is_zero(bmap->eq[i][0])) {
258 bmap = isl_basic_map_set_to_empty(bmap);
259 break;
260 }
261 isl_basic_map_drop_equality(bmap, i);
262 continue;
263 }
264 if (F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
265 isl_int_gcd(gcd, gcd, bmap->eq[i][0]);
266 if (isl_int_is_one(gcd))
267 continue;
268 if (!isl_int_is_divisible_by(bmap->eq[i][0], gcd)) {
269 bmap = isl_basic_map_set_to_empty(bmap);
270 break;
271 }
272 isl_seq_scale_down(bmap->eq[i], bmap->eq[i], gcd, 1+total);
273 }
274
275 for (i = bmap->n_ineq - 1; i >= 0; --i) {
276 isl_seq_gcd(bmap->ineq[i]+1, total, &gcd);
277 if (isl_int_is_zero(gcd)) {
278 if (isl_int_is_neg(bmap->ineq[i][0])) {
279 bmap = isl_basic_map_set_to_empty(bmap);
280 break;
281 }
282 isl_basic_map_drop_inequality(bmap, i);
283 continue;
284 }
285 if (F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
286 isl_int_gcd(gcd, gcd, bmap->ineq[i][0]);
287 if (isl_int_is_one(gcd))
288 continue;
289 isl_int_fdiv_q(bmap->ineq[i][0], bmap->ineq[i][0], gcd);
290 isl_seq_scale_down(bmap->ineq[i]+1, bmap->ineq[i]+1, gcd, total);
291 }
292 isl_int_clear(gcd);
293
294 return bmap;
295 }
296
297 static void eliminate_div(struct isl_basic_map *bmap, isl_int *eq, unsigned div)
298 {
299 int i;
300 unsigned pos = 1 + isl_dim_total(bmap->dim) + div;
301 unsigned len;
302 len = 1 + isl_basic_map_total_dim(bmap);
303
304 for (i = 0; i < bmap->n_eq; ++i)
305 if (bmap->eq[i] != eq)
306 isl_seq_elim(bmap->eq[i], eq, pos, len, NULL);
307
308 for (i = 0; i < bmap->n_ineq; ++i)
309 isl_seq_elim(bmap->ineq[i], eq, pos, len, NULL);
310
311 /* We need to be careful about circular definitions,
312 * so for now we just remove the definitions of other divs that
313 * depend on this div and (possibly) recompute them later.
314 */
315 for (i = 0; i < bmap->n_div; ++i)
316 if (!isl_int_is_zero(bmap->div[i][0]) &&
317 !isl_int_is_zero(bmap->div[i][1 + pos]))
318 isl_seq_clr(bmap->div[i], 1 + len);
319
320 isl_basic_map_drop_div(bmap, div);
321 }
322
323 /* Elimininate divs based on equalities
324 */
325 static struct isl_basic_map *eliminate_divs_eq(
326 struct isl_basic_map *bmap, int *progress)
327 {
328 int d;
329 int i;
330 int modified = 0;
331 unsigned off;
332
333 if (!bmap)
334 return NULL;
335
336 off = 1 + isl_dim_total(bmap->dim);
337
338 for (d = bmap->n_div - 1; d >= 0 ; --d) {
339 for (i = 0; i < bmap->n_eq; ++i) {
340 if (!isl_int_is_one(bmap->eq[i][off + d]) &&
341 !isl_int_is_negone(bmap->eq[i][off + d]))
342 continue;
343 modified = 1;
344 *progress = 1;
345 eliminate_div(bmap, bmap->eq[i], d);
346 isl_basic_map_drop_equality(bmap, i);
347 break;
348 }
349 }
350 if (modified)
351 return eliminate_divs_eq(bmap, progress);
352 return bmap;
353 }
354
355 /* Elimininate divs based on inequalities
356 */
357 static struct isl_basic_map *eliminate_divs_ineq(
358 struct isl_basic_map *bmap, int *progress)
359 {
360 int d;
361 int i;
362 unsigned off;
363 struct isl_ctx *ctx;
364
365 if (!bmap)
366 return NULL;
367
368 ctx = bmap->ctx;
369 off = 1 + isl_dim_total(bmap->dim);
370
371 for (d = bmap->n_div - 1; d >= 0 ; --d) {
372 for (i = 0; i < bmap->n_eq; ++i)
373 if (!isl_int_is_zero(bmap->eq[i][off + d]))
374 break;
375 if (i < bmap->n_eq)
376 continue;
377 for (i = 0; i < bmap->n_ineq; ++i)
378 if (isl_int_abs_gt(bmap->ineq[i][off + d], ctx->one))
379 break;
380 if (i < bmap->n_ineq)
381 continue;
382 *progress = 1;
383 bmap = isl_basic_map_eliminate_vars(bmap, (off-1)+d, 1);
384 if (F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
385 break;
386 bmap = isl_basic_map_drop_div(bmap, d);
387 if (!bmap)
388 break;
389 }
390 return bmap;
391 }
392
393 static void eliminate_var_using_equality(struct isl_basic_map *bmap,
394 unsigned pos, isl_int *eq, int *progress)
395 {
396 unsigned total;
397 int k;
398 int contains_divs;
399
400 total = isl_basic_map_total_dim(bmap);
401 contains_divs =
402 isl_seq_first_non_zero(eq + 1 + isl_dim_total(bmap->dim),
403 bmap->n_div) != -1;
404 for (k = 0; k < bmap->n_eq; ++k) {
405 if (bmap->eq[k] == eq)
406 continue;
407 if (isl_int_is_zero(bmap->eq[k][1+pos]))
408 continue;
409 if (progress)
410 *progress = 1;
411 isl_seq_elim(bmap->eq[k], eq, 1+pos, 1+total, NULL);
412 }
413
414 for (k = 0; k < bmap->n_ineq; ++k) {
415 if (isl_int_is_zero(bmap->ineq[k][1+pos]))
416 continue;
417 if (progress)
418 *progress = 1;
419 isl_seq_elim(bmap->ineq[k], eq, 1+pos, 1+total, NULL);
420 F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
421 }
422
423 for (k = 0; k < bmap->n_div; ++k) {
424 if (isl_int_is_zero(bmap->div[k][0]))
425 continue;
426 if (isl_int_is_zero(bmap->div[k][1+1+pos]))
427 continue;
428 if (progress)
429 *progress = 1;
430 /* We need to be careful about circular definitions,
431 * so for now we just remove the definition of div k
432 * if the equality contains any divs.
433 */
434 if (contains_divs)
435 isl_seq_clr(bmap->div[k], 1 + total);
436 else
437 isl_seq_elim(bmap->div[k]+1, eq,
438 1+pos, 1+total, &bmap->div[k][0]);
439 F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
440 }
441 }
442
443 struct isl_basic_map *isl_basic_map_gauss(
444 struct isl_basic_map *bmap, int *progress)
445 {
446 int k;
447 int done;
448 int last_var;
449 unsigned total_var;
450 unsigned total;
451
452 if (!bmap)
453 return NULL;
454
455 total = isl_basic_map_total_dim(bmap);
456 total_var = total - bmap->n_div;
457
458 last_var = total - 1;
459 for (done = 0; done < bmap->n_eq; ++done) {
460 for (; last_var >= 0; --last_var) {
461 for (k = done; k < bmap->n_eq; ++k)
462 if (!isl_int_is_zero(bmap->eq[k][1+last_var]))
463 break;
464 if (k < bmap->n_eq)
465 break;
466 }
467 if (last_var < 0)
468 break;
469 if (k != done)
470 swap_equality(bmap, k, done);
471 if (isl_int_is_neg(bmap->eq[done][1+last_var]))
472 isl_seq_neg(bmap->eq[done], bmap->eq[done], 1+total);
473
474 eliminate_var_using_equality(bmap, last_var, bmap->eq[done],
475 progress);
476
477 if (last_var >= total_var &&
478 isl_int_is_zero(bmap->div[last_var - total_var][0])) {
479 unsigned div = last_var - total_var;
480 isl_seq_neg(bmap->div[div]+1, bmap->eq[done], 1+total);
481 isl_int_set_si(bmap->div[div][1+1+last_var], 0);
482 isl_int_set(bmap->div[div][0],
483 bmap->eq[done][1+last_var]);
484 F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
485 }
486 }
487 if (done == bmap->n_eq)
488 return bmap;
489 for (k = done; k < bmap->n_eq; ++k) {
490 if (isl_int_is_zero(bmap->eq[k][0]))
491 continue;
492 return isl_basic_map_set_to_empty(bmap);
493 }
494 isl_basic_map_free_equality(bmap, bmap->n_eq-done);
495 return bmap;
496 }
497
498 struct isl_basic_set *isl_basic_set_gauss(
499 struct isl_basic_set *bset, int *progress)
500 {
501 return (struct isl_basic_set*)isl_basic_map_gauss(
502 (struct isl_basic_map *)bset, progress);
503 }
504
505
506 static unsigned int round_up(unsigned int v)
507 {
508 int old_v = v;
509
510 while (v) {
511 old_v = v;
512 v ^= v & -v;
513 }
514 return old_v << 1;
515 }
516
517 static int hash_index(isl_int ***index, unsigned int size, int bits,
518 struct isl_basic_map *bmap, int k)
519 {
520 int h;
521 unsigned total = isl_basic_map_total_dim(bmap);
522 uint32_t hash = isl_seq_get_hash_bits(bmap->ineq[k]+1, total, bits);
523 for (h = hash; index[h]; h = (h+1) % size)
524 if (&bmap->ineq[k] != index[h] &&
525 isl_seq_eq(bmap->ineq[k]+1, index[h][0]+1, total))
526 break;
527 return h;
528 }
529
530 static int set_hash_index(isl_int ***index, unsigned int size, int bits,
531 struct isl_basic_set *bset, int k)
532 {
533 return hash_index(index, size, bits, (struct isl_basic_map *)bset, k);
534 }
535
536 /* If we can eliminate more than one div, then we need to make
537 * sure we do it from last div to first div, in order not to
538 * change the position of the other divs that still need to
539 * be removed.
540 */
541 static struct isl_basic_map *remove_duplicate_divs(
542 struct isl_basic_map *bmap, int *progress)
543 {
544 unsigned int size;
545 int *index;
546 int *elim_for;
547 int k, l, h;
548 int bits;
549 struct isl_blk eq;
550 unsigned total_var = isl_dim_total(bmap->dim);
551 unsigned total = total_var + bmap->n_div;
552 struct isl_ctx *ctx;
553
554 if (bmap->n_div <= 1)
555 return bmap;
556
557 ctx = bmap->ctx;
558 for (k = bmap->n_div - 1; k >= 0; --k)
559 if (!isl_int_is_zero(bmap->div[k][0]))
560 break;
561 if (k <= 0)
562 return bmap;
563
564 elim_for = isl_calloc_array(ctx, int, bmap->n_div);
565 size = round_up(4 * bmap->n_div / 3 - 1);
566 bits = ffs(size) - 1;
567 index = isl_calloc_array(ctx, int, size);
568 if (!index)
569 return bmap;
570 eq = isl_blk_alloc(ctx, 1+total);
571 if (isl_blk_is_error(eq))
572 goto out;
573
574 isl_seq_clr(eq.data, 1+total);
575 index[isl_seq_get_hash_bits(bmap->div[k], 2+total, bits)] = k + 1;
576 for (--k; k >= 0; --k) {
577 uint32_t hash;
578
579 if (isl_int_is_zero(bmap->div[k][0]))
580 continue;
581
582 hash = isl_seq_get_hash_bits(bmap->div[k], 2+total, bits);
583 for (h = hash; index[h]; h = (h+1) % size)
584 if (isl_seq_eq(bmap->div[k],
585 bmap->div[index[h]-1], 2+total))
586 break;
587 if (index[h]) {
588 *progress = 1;
589 l = index[h] - 1;
590 elim_for[l] = k + 1;
591 }
592 index[h] = k+1;
593 }
594 for (l = bmap->n_div - 1; l >= 0; --l) {
595 if (!elim_for[l])
596 continue;
597 k = elim_for[l] - 1;
598 isl_int_set_si(eq.data[1+total_var+k], -1);
599 isl_int_set_si(eq.data[1+total_var+l], 1);
600 eliminate_div(bmap, eq.data, l);
601 isl_int_set_si(eq.data[1+total_var+k], 0);
602 isl_int_set_si(eq.data[1+total_var+l], 0);
603 }
604
605 isl_blk_free(ctx, eq);
606 out:
607 free(index);
608 free(elim_for);
609 return bmap;
610 }
611
612 /* Normalize divs that appear in equalities.
613 *
614 * In particular, we assume that bmap contains some equalities
615 * of the form
616 *
617 * a x = m * e_i
618 *
619 * and we want to replace the set of e_i by a minimal set and
620 * such that the new e_i have a canonical representation in terms
621 * of the vector x.
622 * If any of the equalities involves more than one divs, then
623 * we currently simply bail out.
624 *
625 * Let us first additionally assume that all equalities involve
626 * a div. The equalities then express modulo constraints on the
627 * remaining variables and we can use "parameter compression"
628 * to find a minimal set of constraints. The result is a transformation
629 *
630 * x = T(x') = x_0 + G x'
631 *
632 * with G a lower-triangular matrix with all elements below the diagonal
633 * non-negative and smaller than the diagonal element on the same row.
634 * We first normalize x_0 by making the same property hold in the affine
635 * T matrix.
636 * The rows i of G with a 1 on the diagonal do not impose any modulo
637 * constraint and simply express x_i = x'_i.
638 * For each of the remaining rows i, we introduce a div and a corresponding
639 * equality. In particular
640 *
641 * g_ii e_j = x_i - g_i(x')
642 *
643 * where each x'_k is replaced either by x_k (if g_kk = 1) or the
644 * corresponding div (if g_kk != 1).
645 *
646 * If there are any equalities not involving any div, then we
647 * first apply a variable compression on the variables x:
648 *
649 * x = C x'' x'' = C_2 x
650 *
651 * and perform the above parameter compression on A C instead of on A.
652 * The resulting compression is then of the form
653 *
654 * x'' = T(x') = x_0 + G x'
655 *
656 * and in constructing the new divs and the corresponding equalities,
657 * we have to replace each x'', i.e., the x'_k with (g_kk = 1),
658 * by the corresponding row from C_2.
659 */
660 static struct isl_basic_map *normalize_divs(
661 struct isl_basic_map *bmap, int *progress)
662 {
663 int i, j, k;
664 int total;
665 int div_eq;
666 struct isl_mat *B;
667 struct isl_vec *d;
668 struct isl_mat *T = NULL;
669 struct isl_mat *C = NULL;
670 struct isl_mat *C2 = NULL;
671 isl_int v;
672 int *pos;
673 int dropped, needed;
674
675 if (!bmap)
676 return NULL;
677
678 if (bmap->n_div == 0)
679 return bmap;
680
681 if (bmap->n_eq == 0)
682 return bmap;
683
684 if (F_ISSET(bmap, ISL_BASIC_MAP_NORMALIZED_DIVS))
685 return bmap;
686
687 total = isl_dim_total(bmap->dim);
688 for (i = 0, j = bmap->n_div-1; i < bmap->n_eq; ++i) {
689 while (j >= 0 && isl_int_is_zero(bmap->eq[i][1 + total + j]))
690 --j;
691 if (j < 0)
692 break;
693 if (isl_seq_first_non_zero(bmap->eq[i] + 1 + total, j) != -1)
694 goto done;
695 }
696 div_eq = i;
697 if (div_eq == 0)
698 return bmap;
699
700 if (div_eq < bmap->n_eq) {
701 B = isl_mat_sub_alloc(bmap->ctx, bmap->eq, div_eq,
702 bmap->n_eq - div_eq, 0, 1 + total);
703 C = isl_mat_variable_compression(bmap->ctx, B, &C2);
704 if (!C || !C2)
705 goto error;
706 if (C->n_col == 0) {
707 bmap = isl_basic_map_set_to_empty(bmap);
708 isl_mat_free(bmap->ctx, C);
709 isl_mat_free(bmap->ctx, C2);
710 goto done;
711 }
712 }
713
714 d = isl_vec_alloc(bmap->ctx, div_eq);
715 if (!d)
716 goto error;
717 for (i = 0, j = bmap->n_div-1; i < div_eq; ++i) {
718 while (j >= 0 && isl_int_is_zero(bmap->eq[i][1 + total + j]))
719 --j;
720 isl_int_set(d->block.data[i], bmap->eq[i][1 + total + j]);
721 }
722 B = isl_mat_sub_alloc(bmap->ctx, bmap->eq, 0, div_eq, 0, 1 + total);
723
724 if (C) {
725 B = isl_mat_product(bmap->ctx, B, C);
726 C = NULL;
727 }
728
729 T = isl_mat_parameter_compression(bmap->ctx, B, d);
730 if (!T)
731 goto error;
732 if (T->n_col == 0) {
733 bmap = isl_basic_map_set_to_empty(bmap);
734 isl_mat_free(bmap->ctx, C2);
735 isl_mat_free(bmap->ctx, T);
736 goto done;
737 }
738 isl_int_init(v);
739 for (i = 0; i < T->n_row - 1; ++i) {
740 isl_int_fdiv_q(v, T->row[1 + i][0], T->row[1 + i][1 + i]);
741 if (isl_int_is_zero(v))
742 continue;
743 isl_mat_col_submul(T, 0, v, 1 + i);
744 }
745 isl_int_clear(v);
746 pos = isl_alloc_array(bmap->ctx, int, T->n_row);
747 /* We have to be careful because dropping equalities may reorder them */
748 dropped = 0;
749 for (j = bmap->n_div - 1; j >= 0; --j) {
750 for (i = 0; i < bmap->n_eq; ++i)
751 if (!isl_int_is_zero(bmap->eq[i][1 + total + j]))
752 break;
753 if (i < bmap->n_eq) {
754 bmap = isl_basic_map_drop_div(bmap, j);
755 isl_basic_map_drop_equality(bmap, i);
756 ++dropped;
757 }
758 }
759 pos[0] = 0;
760 needed = 0;
761 for (i = 1; i < T->n_row; ++i) {
762 if (isl_int_is_one(T->row[i][i]))
763 pos[i] = i;
764 else
765 needed++;
766 }
767 if (needed > dropped) {
768 bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
769 needed, needed, 0);
770 if (!bmap)
771 goto error;
772 }
773 for (i = 1; i < T->n_row; ++i) {
774 if (isl_int_is_one(T->row[i][i]))
775 continue;
776 k = isl_basic_map_alloc_div(bmap);
777 pos[i] = 1 + total + k;
778 isl_seq_clr(bmap->div[k] + 1, 1 + total + bmap->n_div);
779 isl_int_set(bmap->div[k][0], T->row[i][i]);
780 if (C2)
781 isl_seq_cpy(bmap->div[k] + 1, C2->row[i], 1 + total);
782 else
783 isl_int_set_si(bmap->div[k][1 + i], 1);
784 for (j = 0; j < i; ++j) {
785 if (isl_int_is_zero(T->row[i][j]))
786 continue;
787 if (pos[j] < T->n_row && C2)
788 isl_seq_submul(bmap->div[k] + 1, T->row[i][j],
789 C2->row[pos[j]], 1 + total);
790 else
791 isl_int_neg(bmap->div[k][1 + pos[j]],
792 T->row[i][j]);
793 }
794 j = isl_basic_map_alloc_equality(bmap);
795 isl_seq_neg(bmap->eq[j], bmap->div[k]+1, 1+total+bmap->n_div);
796 isl_int_set(bmap->eq[j][pos[i]], bmap->div[k][0]);
797 }
798 free(pos);
799 isl_mat_free(bmap->ctx, C2);
800 isl_mat_free(bmap->ctx, T);
801
802 *progress = 1;
803 done:
804 F_SET(bmap, ISL_BASIC_MAP_NORMALIZED_DIVS);
805
806 return bmap;
807 error:
808 isl_mat_free(bmap->ctx, C);
809 isl_mat_free(bmap->ctx, C2);
810 isl_mat_free(bmap->ctx, T);
811 return bmap;
812 }
813
814 static struct isl_basic_map *remove_duplicate_constraints(
815 struct isl_basic_map *bmap, int *progress)
816 {
817 unsigned int size;
818 isl_int ***index;
819 int k, l, h;
820 int bits;
821 unsigned total = isl_basic_map_total_dim(bmap);
822 isl_int sum;
823
824 if (bmap->n_ineq <= 1)
825 return bmap;
826
827 size = round_up(4 * (bmap->n_ineq+1) / 3 - 1);
828 bits = ffs(size) - 1;
829 index = isl_calloc_array(ctx, isl_int **, size);
830 if (!index)
831 return bmap;
832
833 index[isl_seq_get_hash_bits(bmap->ineq[0]+1, total, bits)] = &bmap->ineq[0];
834 for (k = 1; k < bmap->n_ineq; ++k) {
835 h = hash_index(index, size, bits, bmap, k);
836 if (!index[h]) {
837 index[h] = &bmap->ineq[k];
838 continue;
839 }
840 if (progress)
841 *progress = 1;
842 l = index[h] - &bmap->ineq[0];
843 if (isl_int_lt(bmap->ineq[k][0], bmap->ineq[l][0]))
844 swap_inequality(bmap, k, l);
845 isl_basic_map_drop_inequality(bmap, k);
846 --k;
847 }
848 isl_int_init(sum);
849 for (k = 0; k < bmap->n_ineq-1; ++k) {
850 isl_seq_neg(bmap->ineq[k]+1, bmap->ineq[k]+1, total);
851 h = hash_index(index, size, bits, bmap, k);
852 isl_seq_neg(bmap->ineq[k]+1, bmap->ineq[k]+1, total);
853 if (!index[h])
854 continue;
855 l = index[h] - &bmap->ineq[0];
856 isl_int_add(sum, bmap->ineq[k][0], bmap->ineq[l][0]);
857 if (isl_int_is_pos(sum))
858 continue;
859 if (isl_int_is_zero(sum)) {
860 /* We need to break out of the loop after these
861 * changes since the contents of the hash
862 * will no longer be valid.
863 * Plus, we probably we want to regauss first.
864 */
865 isl_basic_map_drop_inequality(bmap, l);
866 isl_basic_map_inequality_to_equality(bmap, k);
867 } else
868 bmap = isl_basic_map_set_to_empty(bmap);
869 break;
870 }
871 isl_int_clear(sum);
872
873 free(index);
874 return bmap;
875 }
876
877
878 struct isl_basic_map *isl_basic_map_simplify(struct isl_basic_map *bmap)
879 {
880 int progress = 1;
881 if (!bmap)
882 return NULL;
883 while (progress) {
884 progress = 0;
885 bmap = normalize_constraints(bmap);
886 bmap = eliminate_divs_eq(bmap, &progress);
887 bmap = eliminate_divs_ineq(bmap, &progress);
888 bmap = isl_basic_map_gauss(bmap, &progress);
889 /* requires equalities in normal form */
890 bmap = normalize_divs(bmap, &progress);
891 bmap = remove_duplicate_divs(bmap, &progress);
892 bmap = remove_duplicate_constraints(bmap, &progress);
893 }
894 return bmap;
895 }
896
897 struct isl_basic_set *isl_basic_set_simplify(struct isl_basic_set *bset)
898 {
899 return (struct isl_basic_set *)
900 isl_basic_map_simplify((struct isl_basic_map *)bset);
901 }
902
903
904 /* If the only constraints a div d=floor(f/m)
905 * appears in are its two defining constraints
906 *
907 * f - m d >=0
908 * -(f - (m - 1)) + m d >= 0
909 *
910 * then it can safely be removed.
911 */
912 static int div_is_redundant(struct isl_basic_map *bmap, int div)
913 {
914 int i;
915 unsigned pos = 1 + isl_dim_total(bmap->dim) + div;
916
917 for (i = 0; i < bmap->n_eq; ++i)
918 if (!isl_int_is_zero(bmap->eq[i][pos]))
919 return 0;
920
921 for (i = 0; i < bmap->n_ineq; ++i) {
922 if (isl_int_is_zero(bmap->ineq[i][pos]))
923 continue;
924 if (isl_int_eq(bmap->ineq[i][pos], bmap->div[div][0])) {
925 int neg;
926 isl_int_sub(bmap->div[div][1],
927 bmap->div[div][1], bmap->div[div][0]);
928 isl_int_add_ui(bmap->div[div][1], bmap->div[div][1], 1);
929 neg = isl_seq_is_neg(bmap->ineq[i], bmap->div[div]+1, pos);
930 isl_int_sub_ui(bmap->div[div][1], bmap->div[div][1], 1);
931 isl_int_add(bmap->div[div][1],
932 bmap->div[div][1], bmap->div[div][0]);
933 if (!neg)
934 return 0;
935 if (isl_seq_first_non_zero(bmap->ineq[i]+pos+1,
936 bmap->n_div-div-1) != -1)
937 return 0;
938 } else if (isl_int_abs_eq(bmap->ineq[i][pos], bmap->div[div][0])) {
939 if (!isl_seq_eq(bmap->ineq[i], bmap->div[div]+1, pos))
940 return 0;
941 if (isl_seq_first_non_zero(bmap->ineq[i]+pos+1,
942 bmap->n_div-div-1) != -1)
943 return 0;
944 } else
945 return 0;
946 }
947
948 for (i = 0; i < bmap->n_div; ++i)
949 if (!isl_int_is_zero(bmap->div[i][1+pos]))
950 return 0;
951
952 return 1;
953 }
954
955 /*
956 * Remove divs that don't occur in any of the constraints or other divs.
957 * These can arise when dropping some of the variables in a quast
958 * returned by piplib.
959 */
960 static struct isl_basic_map *remove_redundant_divs(struct isl_basic_map *bmap)
961 {
962 int i;
963
964 if (!bmap)
965 return NULL;
966
967 for (i = bmap->n_div-1; i >= 0; --i) {
968 if (!div_is_redundant(bmap, i))
969 continue;
970 bmap = isl_basic_map_drop_div(bmap, i);
971 }
972 return bmap;
973 }
974
975 struct isl_basic_map *isl_basic_map_finalize(struct isl_basic_map *bmap)
976 {
977 bmap = remove_redundant_divs(bmap);
978 if (!bmap)
979 return NULL;
980 F_SET(bmap, ISL_BASIC_SET_FINAL);
981 return bmap;
982 }
983
984 struct isl_basic_set *isl_basic_set_finalize(struct isl_basic_set *bset)
985 {
986 return (struct isl_basic_set *)
987 isl_basic_map_finalize((struct isl_basic_map *)bset);
988 }
989
990 struct isl_set *isl_set_finalize(struct isl_set *set)
991 {
992 int i;
993
994 if (!set)
995 return NULL;
996 for (i = 0; i < set->n; ++i) {
997 set->p[i] = isl_basic_set_finalize(set->p[i]);
998 if (!set->p[i])
999 goto error;
1000 }
1001 return set;
1002 error:
1003 isl_set_free(set);
1004 return NULL;
1005 }
1006
1007 struct isl_map *isl_map_finalize(struct isl_map *map)
1008 {
1009 int i;
1010
1011 if (!map)
1012 return NULL;
1013 for (i = 0; i < map->n; ++i) {
1014 map->p[i] = isl_basic_map_finalize(map->p[i]);
1015 if (!map->p[i])
1016 goto error;
1017 }
1018 F_CLR(map, ISL_MAP_NORMALIZED);
1019 return map;
1020 error:
1021 isl_map_free(map);
1022 return NULL;
1023 }
1024
1025
1026 /* Remove any div that is defined in terms of the given variable.
1027 */
1028 static struct isl_basic_map *remove_dependent_vars(struct isl_basic_map *bmap,
1029 int pos)
1030 {
1031 int i;
1032 unsigned dim = isl_dim_total(bmap->dim);
1033
1034 for (i = 0; i < bmap->n_div; ++i) {
1035 if (isl_int_is_zero(bmap->div[i][0]))
1036 continue;
1037 if (isl_int_is_zero(bmap->div[i][1+1+pos]))
1038 continue;
1039 bmap = isl_basic_map_eliminate_vars(bmap, dim + i, 1);
1040 if (!bmap)
1041 return NULL;
1042 }
1043 return bmap;
1044 }
1045
1046 /* Eliminate the specified variables from the constraints using
1047 * Fourier-Motzkin. The variables themselves are not removed.
1048 */
1049 struct isl_basic_map *isl_basic_map_eliminate_vars(
1050 struct isl_basic_map *bmap, unsigned pos, unsigned n)
1051 {
1052 int d;
1053 int i, j, k;
1054 unsigned total;
1055
1056 if (n == 0)
1057 return bmap;
1058 if (!bmap)
1059 return NULL;
1060 total = isl_basic_map_total_dim(bmap);
1061
1062 bmap = isl_basic_map_cow(bmap);
1063 for (d = pos + n - 1; d >= 0 && d >= pos; --d) {
1064 int n_lower, n_upper;
1065 bmap = remove_dependent_vars(bmap, d);
1066 if (!bmap)
1067 return NULL;
1068 if (d >= total - bmap->n_div)
1069 isl_seq_clr(bmap->div[d-(total-bmap->n_div)], 2+total);
1070 for (i = 0; i < bmap->n_eq; ++i) {
1071 if (isl_int_is_zero(bmap->eq[i][1+d]))
1072 continue;
1073 eliminate_var_using_equality(bmap, d, bmap->eq[i], NULL);
1074 isl_basic_map_drop_equality(bmap, i);
1075 break;
1076 }
1077 if (i < bmap->n_eq)
1078 continue;
1079 n_lower = 0;
1080 n_upper = 0;
1081 for (i = 0; i < bmap->n_ineq; ++i) {
1082 if (isl_int_is_pos(bmap->ineq[i][1+d]))
1083 n_lower++;
1084 else if (isl_int_is_neg(bmap->ineq[i][1+d]))
1085 n_upper++;
1086 }
1087 bmap = isl_basic_map_extend_constraints(bmap,
1088 0, n_lower * n_upper);
1089 for (i = bmap->n_ineq - 1; i >= 0; --i) {
1090 int last;
1091 if (isl_int_is_zero(bmap->ineq[i][1+d]))
1092 continue;
1093 last = -1;
1094 for (j = 0; j < i; ++j) {
1095 if (isl_int_is_zero(bmap->ineq[j][1+d]))
1096 continue;
1097 last = j;
1098 if (isl_int_sgn(bmap->ineq[i][1+d]) ==
1099 isl_int_sgn(bmap->ineq[j][1+d]))
1100 continue;
1101 k = isl_basic_map_alloc_inequality(bmap);
1102 if (k < 0)
1103 goto error;
1104 isl_seq_cpy(bmap->ineq[k], bmap->ineq[i],
1105 1+total);
1106 isl_seq_elim(bmap->ineq[k], bmap->ineq[j],
1107 1+d, 1+total, NULL);
1108 }
1109 isl_basic_map_drop_inequality(bmap, i);
1110 i = last + 1;
1111 }
1112 if (n_lower > 0 && n_upper > 0) {
1113 bmap = normalize_constraints(bmap);
1114 bmap = remove_duplicate_constraints(bmap, NULL);
1115 bmap = isl_basic_map_gauss(bmap, NULL);
1116 bmap = isl_basic_map_convex_hull(bmap);
1117 if (!bmap)
1118 goto error;
1119 if (F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
1120 break;
1121 }
1122 }
1123 F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
1124 return bmap;
1125 error:
1126 isl_basic_map_free(bmap);
1127 return NULL;
1128 }
1129
1130 struct isl_basic_set *isl_basic_set_eliminate_vars(
1131 struct isl_basic_set *bset, unsigned pos, unsigned n)
1132 {
1133 return (struct isl_basic_set *)isl_basic_map_eliminate_vars(
1134 (struct isl_basic_map *)bset, pos, n);
1135 }
1136
1137 static void compute_elimination_index(struct isl_basic_map *bmap, int *elim)
1138 {
1139 int d, i;
1140 unsigned total;
1141
1142 total = isl_dim_total(bmap->dim);
1143 for (d = 0; d < total; ++d)
1144 elim[d] = -1;
1145 for (d = total - 1, i = 0; d >= 0 && i < bmap->n_eq; ++i) {
1146 for (; d >= 0; --d) {
1147 if (isl_int_is_zero(bmap->eq[i][1+d]))
1148 continue;
1149 elim[d] = i;
1150 break;
1151 }
1152 }
1153 }
1154
1155 static void set_compute_elimination_index(struct isl_basic_set *bset, int *elim)
1156 {
1157 return compute_elimination_index((struct isl_basic_map *)bset, elim);
1158 }
1159
1160 static int reduced_using_equalities(isl_int *dst, isl_int *src,
1161 struct isl_basic_map *bmap, int *elim)
1162 {
1163 int d, i;
1164 int copied = 0;
1165 unsigned total;
1166
1167 total = isl_dim_total(bmap->dim);
1168 for (d = total - 1; d >= 0; --d) {
1169 if (isl_int_is_zero(src[1+d]))
1170 continue;
1171 if (elim[d] == -1)
1172 continue;
1173 if (!copied) {
1174 isl_seq_cpy(dst, src, 1 + total);
1175 copied = 1;
1176 }
1177 isl_seq_elim(dst, bmap->eq[elim[d]], 1 + d, 1 + total, NULL);
1178 }
1179 return copied;
1180 }
1181
1182 static int set_reduced_using_equalities(isl_int *dst, isl_int *src,
1183 struct isl_basic_set *bset, int *elim)
1184 {
1185 return reduced_using_equalities(dst, src,
1186 (struct isl_basic_map *)bset, elim);
1187 }
1188
1189 static struct isl_basic_set *isl_basic_set_reduce_using_equalities(
1190 struct isl_basic_set *bset, struct isl_basic_set *context)
1191 {
1192 int i;
1193 int *elim;
1194
1195 if (!bset || !context)
1196 goto error;
1197
1198 bset = isl_basic_set_cow(bset);
1199 if (!bset)
1200 goto error;
1201
1202 elim = isl_alloc_array(ctx, int, isl_basic_set_n_dim(bset));
1203 if (!elim)
1204 goto error;
1205 set_compute_elimination_index(context, elim);
1206 for (i = 0; i < bset->n_eq; ++i)
1207 set_reduced_using_equalities(bset->eq[i], bset->eq[i],
1208 context, elim);
1209 for (i = 0; i < bset->n_ineq; ++i)
1210 set_reduced_using_equalities(bset->ineq[i], bset->ineq[i],
1211 context, elim);
1212 isl_basic_set_free(context);
1213 free(elim);
1214 bset = isl_basic_set_simplify(bset);
1215 bset = isl_basic_set_finalize(bset);
1216 return bset;
1217 error:
1218 isl_basic_set_free(bset);
1219 isl_basic_set_free(context);
1220 return NULL;
1221 }
1222
1223 static struct isl_basic_set *remove_shifted_constraints(
1224 struct isl_basic_set *bset, struct isl_basic_set *context)
1225 {
1226 unsigned int size;
1227 isl_int ***index;
1228 int bits;
1229 int k, h, l;
1230
1231 if (!bset)
1232 return NULL;
1233
1234 size = round_up(4 * (context->n_ineq+1) / 3 - 1);
1235 bits = ffs(size) - 1;
1236 index = isl_calloc_array(ctx, isl_int **, size);
1237 if (!index)
1238 return bset;
1239
1240 for (k = 0; k < context->n_ineq; ++k) {
1241 h = set_hash_index(index, size, bits, context, k);
1242 index[h] = &context->ineq[k];
1243 }
1244 for (k = 0; k < bset->n_ineq; ++k) {
1245 h = set_hash_index(index, size, bits, bset, k);
1246 if (!index[h])
1247 continue;
1248 l = index[h] - &context->ineq[0];
1249 if (isl_int_lt(bset->ineq[k][0], context->ineq[l][0]))
1250 continue;
1251 bset = isl_basic_set_cow(bset);
1252 if (!bset)
1253 goto error;
1254 isl_basic_set_drop_inequality(bset, k);
1255 --k;
1256 }
1257 free(index);
1258 return bset;
1259 error:
1260 free(index);
1261 return bset;
1262 }
1263
1264 static struct isl_basic_set *uset_gist(struct isl_basic_set *bset,
1265 struct isl_basic_set *context);
1266
1267 static struct isl_basic_set *uset_gist_context_eq(struct isl_basic_set *bset,
1268 struct isl_basic_set *context)
1269 {
1270 struct isl_mat *T;
1271 struct isl_mat *T2;
1272 struct isl_ctx *ctx = context->ctx;
1273 struct isl_basic_set *reduced_context;
1274 reduced_context = isl_basic_set_remove_equalities(
1275 isl_basic_set_copy(context), &T, &T2);
1276 if (!reduced_context)
1277 goto error;
1278 bset = isl_basic_set_preimage(ctx, bset, T);
1279 bset = uset_gist(bset, reduced_context);
1280 bset = isl_basic_set_preimage(ctx, bset, T2);
1281 bset = isl_basic_set_reduce_using_equalities(bset, context);
1282 return bset;
1283 error:
1284 isl_basic_set_free(context);
1285 isl_basic_set_free(bset);
1286 return NULL;
1287 }
1288
1289 static struct isl_basic_set *uset_gist_set_eq(struct isl_basic_set *bset,
1290 struct isl_basic_set *context)
1291 {
1292 struct isl_mat *T;
1293 struct isl_mat *T2;
1294 struct isl_ctx *ctx = context->ctx;
1295 struct isl_basic_set *affine_hull = NULL;
1296
1297 affine_hull = isl_basic_set_copy(bset);
1298 affine_hull = isl_basic_set_cow(affine_hull);
1299 if (!affine_hull)
1300 goto error;
1301 isl_basic_set_free_inequality(affine_hull, affine_hull->n_ineq);
1302
1303 bset = isl_basic_set_remove_equalities(bset, &T, &T2);
1304 if (!bset)
1305 goto error;
1306 context = isl_basic_set_preimage(ctx, context, T);
1307 bset = uset_gist(bset, context);
1308 bset = isl_basic_set_preimage(ctx, bset, T2);
1309 bset = isl_basic_set_intersect(bset, affine_hull);
1310 return bset;
1311 error:
1312 isl_basic_set_free(affine_hull);
1313 isl_basic_set_free(context);
1314 isl_basic_set_free(bset);
1315 return NULL;
1316 }
1317
1318 /* Remove all information from bset that is redundant in the context
1319 * of context. In particular, equalities that are linear combinations
1320 * of those in context are removed. Then the inequalities that are
1321 * redundant in the context of the equalities and inequalities of
1322 * context are removed.
1323 */
1324 static struct isl_basic_set *uset_gist(struct isl_basic_set *bset,
1325 struct isl_basic_set *context)
1326 {
1327 int i;
1328 isl_int opt;
1329 struct isl_basic_set *combined;
1330 struct isl_ctx *ctx;
1331
1332 if (!bset || !context)
1333 goto error;
1334
1335 if (context->n_eq > 0)
1336 return uset_gist_context_eq(bset, context);
1337 if (!context->n_ineq)
1338 goto done;
1339 if (bset->n_eq > 0)
1340 return uset_gist_set_eq(bset, context);
1341 bset = remove_shifted_constraints(bset, context);
1342 combined = isl_basic_set_extend_constraints(isl_basic_set_copy(bset),
1343 context->n_eq, context->n_ineq);
1344 context = isl_basic_set_add_constraints(combined, context, 0);
1345 if (!context)
1346 goto error;
1347 ctx = context->ctx;
1348 isl_int_init(opt);
1349 for (i = bset->n_ineq-1; i >= 0; --i) {
1350 int redundant;
1351 set_swap_inequality(context, i, context->n_ineq-1);
1352 context->n_ineq--;
1353 redundant = isl_basic_set_constraint_is_redundant(&context,
1354 context->ineq[context->n_ineq], &opt, NULL);
1355 if (redundant == -1) {
1356 isl_int_clear(opt);
1357 goto error;
1358 }
1359 if (F_ISSET(context, ISL_BASIC_MAP_EMPTY)) {
1360 bset = isl_basic_set_set_to_empty(bset);
1361 break;
1362 }
1363 context->n_ineq++;
1364 set_swap_inequality(context, i, context->n_ineq-1);
1365 if (redundant) {
1366 isl_basic_set_drop_inequality(context, i);
1367 isl_basic_set_drop_inequality(bset, i);
1368 }
1369 }
1370 isl_int_clear(opt);
1371 done:
1372 isl_basic_set_free(context);
1373 return bset;
1374 error:
1375 isl_basic_set_free(context);
1376 isl_basic_set_free(bset);
1377 return NULL;
1378 }
1379
1380 struct isl_basic_map *isl_basic_map_gist(struct isl_basic_map *bmap,
1381 struct isl_basic_map *context)
1382 {
1383 struct isl_basic_set *bset;
1384
1385 if (!bmap || !context)
1386 goto error;
1387
1388 context = isl_basic_map_align_divs(context, bmap);
1389 bmap = isl_basic_map_align_divs(bmap, context);
1390
1391 bset = uset_gist(isl_basic_map_underlying_set(isl_basic_map_copy(bmap)),
1392 isl_basic_map_underlying_set(context));
1393
1394 return isl_basic_map_overlying_set(bset, bmap);
1395 error:
1396 isl_basic_map_free(bmap);
1397 isl_basic_map_free(context);
1398 return NULL;
1399 }
1400
1401 /*
1402 * Assumes context has no implicit divs.
1403 */
1404 struct isl_map *isl_map_gist(struct isl_map *map, struct isl_basic_map *context)
1405 {
1406 int i;
1407
1408 map = isl_map_cow(map);
1409 if (!map || !context)
1410 return NULL;
1411 isl_assert(map->ctx, isl_dim_equal(map->dim, context->dim), goto error);
1412 map = isl_map_compute_divs(map);
1413 for (i = 0; i < map->n; ++i)
1414 context = isl_basic_map_align_divs(context, map->p[i]);
1415 for (i = 0; i < map->n; ++i) {
1416 map->p[i] = isl_basic_map_gist(map->p[i],
1417 isl_basic_map_copy(context));
1418 if (!map->p[i])
1419 goto error;
1420 }
1421 isl_basic_map_free(context);
1422 F_CLR(map, ISL_MAP_NORMALIZED);
1423 return map;
1424 error:
1425 isl_map_free(map);
1426 isl_basic_map_free(context);
1427 return NULL;
1428 }
1429
1430 struct isl_basic_set *isl_basic_set_gist(struct isl_basic_set *bset,
1431 struct isl_basic_set *context)
1432 {
1433 return (struct isl_basic_set *)isl_basic_map_gist(
1434 (struct isl_basic_map *)bset, (struct isl_basic_map *)context);
1435 }
1436
1437 struct isl_set *isl_set_gist(struct isl_set *set, struct isl_basic_set *context)
1438 {
1439 return (struct isl_set *)isl_map_gist((struct isl_map *)set,
1440 (struct isl_basic_map *)context);
1441 }
1442
1443 /* Quick check to see if two basic maps are disjoint.
1444 * In particular, we reduce the equalities and inequalities of
1445 * one basic map in the context of the equalities of the other
1446 * basic map and check if we get a contradiction.
1447 */
1448 int isl_basic_map_fast_is_disjoint(struct isl_basic_map *bmap1,
1449 struct isl_basic_map *bmap2)
1450 {
1451 struct isl_vec *v = NULL;
1452 int *elim = NULL;
1453 unsigned total;
1454 int d, i;
1455
1456 if (!bmap1 || !bmap2)
1457 return -1;
1458 isl_assert(bmap1->ctx, isl_dim_equal(bmap1->dim, bmap2->dim),
1459 return -1);
1460 if (bmap1->n_div || bmap2->n_div)
1461 return 0;
1462 if (!bmap1->n_eq && !bmap2->n_eq)
1463 return 0;
1464
1465 total = isl_dim_total(bmap1->dim);
1466 if (total == 0)
1467 return 0;
1468 v = isl_vec_alloc(bmap1->ctx, 1 + total);
1469 if (!v)
1470 goto error;
1471 elim = isl_alloc_array(bmap1->ctx, int, total);
1472 if (!elim)
1473 goto error;
1474 compute_elimination_index(bmap1, elim);
1475 for (i = 0; i < bmap2->n_eq; ++i) {
1476 int reduced;
1477 reduced = reduced_using_equalities(v->block.data, bmap2->eq[i],
1478 bmap1, elim);
1479 if (reduced && !isl_int_is_zero(v->block.data[0]) &&
1480 isl_seq_first_non_zero(v->block.data + 1, total) == -1)
1481 goto disjoint;
1482 }
1483 for (i = 0; i < bmap2->n_ineq; ++i) {
1484 int reduced;
1485 reduced = reduced_using_equalities(v->block.data,
1486 bmap2->ineq[i], bmap1, elim);
1487 if (reduced && isl_int_is_neg(v->block.data[0]) &&
1488 isl_seq_first_non_zero(v->block.data + 1, total) == -1)
1489 goto disjoint;
1490 }
1491 compute_elimination_index(bmap2, elim);
1492 for (i = 0; i < bmap1->n_ineq; ++i) {
1493 int reduced;
1494 reduced = reduced_using_equalities(v->block.data,
1495 bmap1->ineq[i], bmap2, elim);
1496 if (reduced && isl_int_is_neg(v->block.data[0]) &&
1497 isl_seq_first_non_zero(v->block.data + 1, total) == -1)
1498 goto disjoint;
1499 }
1500 isl_vec_free(bmap1->ctx, v);
1501 free(elim);
1502 return 0;
1503 disjoint:
1504 isl_vec_free(bmap1->ctx, v);
1505 free(elim);
1506 return 1;
1507 error:
1508 isl_vec_free(bmap1->ctx, v);
1509 free(elim);
1510 return -1;
1511 }
1512
1513 int isl_basic_set_fast_is_disjoint(struct isl_basic_set *bset1,
1514 struct isl_basic_set *bset2)
1515 {
1516 return isl_basic_map_fast_is_disjoint((struct isl_basic_map *)bset1,
1517 (struct isl_basic_map *)bset2);
1518 }
1519
1520 int isl_map_fast_is_disjoint(struct isl_map *map1, struct isl_map *map2)
1521 {
1522 int i, j;
1523
1524 if (!map1 || !map2)
1525 return -1;
1526
1527 if (isl_map_fast_is_equal(map1, map2))
1528 return 0;
1529
1530 for (i = 0; i < map1->n; ++i) {
1531 for (j = 0; j < map2->n; ++j) {
1532 int d = isl_basic_map_fast_is_disjoint(map1->p[i],
1533 map2->p[j]);
1534 if (d != 1)
1535 return d;
1536 }
1537 }
1538 return 1;
1539 }
1540
1541 int isl_set_fast_is_disjoint(struct isl_set *set1, struct isl_set *set2)
1542 {
1543 return isl_map_fast_is_disjoint((struct isl_map *)set1,
1544 (struct isl_map *)set2);
1545 }
Integer set library