nexmon – Blame information for rev 1

Subversion Repositories:
Rev:
Rev Author Line No. Line
1 office 1 /*
2 * Copyright 2008-2009 Katholieke Universiteit Leuven
3 *
4 * Use of this software is governed by the GNU LGPLv2.1 license
5 *
6 * Written by Sven Verdoolaege, K.U.Leuven, Departement
7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
8 */
9  
10 #include <isl_ctx_private.h>
11 #include <isl_map_private.h>
12 #include <isl/seq.h>
13 #include <isl/set.h>
14 #include <isl/lp.h>
15 #include <isl/map.h>
16 #include "isl_equalities.h"
17 #include "isl_sample.h"
18 #include "isl_tab.h"
19 #include <isl_mat_private.h>
20  
21 struct isl_basic_map *isl_basic_map_implicit_equalities(
22 struct isl_basic_map *bmap)
23 {
24 struct isl_tab *tab;
25  
26 if (!bmap)
27 return bmap;
28  
29 bmap = isl_basic_map_gauss(bmap, NULL);
30 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
31 return bmap;
32 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_NO_IMPLICIT))
33 return bmap;
34 if (bmap->n_ineq <= 1)
35 return bmap;
36  
37 tab = isl_tab_from_basic_map(bmap, 0);
38 if (isl_tab_detect_implicit_equalities(tab) < 0)
39 goto error;
40 bmap = isl_basic_map_update_from_tab(bmap, tab);
41 isl_tab_free(tab);
42 bmap = isl_basic_map_gauss(bmap, NULL);
43 ISL_F_SET(bmap, ISL_BASIC_MAP_NO_IMPLICIT);
44 return bmap;
45 error:
46 isl_tab_free(tab);
47 isl_basic_map_free(bmap);
48 return NULL;
49 }
50  
51 struct isl_basic_set *isl_basic_set_implicit_equalities(
52 struct isl_basic_set *bset)
53 {
54 return (struct isl_basic_set *)
55 isl_basic_map_implicit_equalities((struct isl_basic_map*)bset);
56 }
57  
58 struct isl_map *isl_map_implicit_equalities(struct isl_map *map)
59 {
60 int i;
61  
62 if (!map)
63 return map;
64  
65 for (i = 0; i < map->n; ++i) {
66 map->p[i] = isl_basic_map_implicit_equalities(map->p[i]);
67 if (!map->p[i])
68 goto error;
69 }
70  
71 return map;
72 error:
73 isl_map_free(map);
74 return NULL;
75 }
76  
77 /* Make eq[row][col] of both bmaps equal so we can add the row
78 * add the column to the common matrix.
79 * Note that because of the echelon form, the columns of row row
80 * after column col are zero.
81 */
82 static void set_common_multiple(
83 struct isl_basic_set *bset1, struct isl_basic_set *bset2,
84 unsigned row, unsigned col)
85 {
86 isl_int m, c;
87  
88 if (isl_int_eq(bset1->eq[row][col], bset2->eq[row][col]))
89 return;
90  
91 isl_int_init(c);
92 isl_int_init(m);
93 isl_int_lcm(m, bset1->eq[row][col], bset2->eq[row][col]);
94 isl_int_divexact(c, m, bset1->eq[row][col]);
95 isl_seq_scale(bset1->eq[row], bset1->eq[row], c, col+1);
96 isl_int_divexact(c, m, bset2->eq[row][col]);
97 isl_seq_scale(bset2->eq[row], bset2->eq[row], c, col+1);
98 isl_int_clear(c);
99 isl_int_clear(m);
100 }
101  
102 /* Delete a given equality, moving all the following equalities one up.
103 */
104 static void delete_row(struct isl_basic_set *bset, unsigned row)
105 {
106 isl_int *t;
107 int r;
108  
109 t = bset->eq[row];
110 bset->n_eq--;
111 for (r = row; r < bset->n_eq; ++r)
112 bset->eq[r] = bset->eq[r+1];
113 bset->eq[bset->n_eq] = t;
114 }
115  
116 /* Make first row entries in column col of bset1 identical to
117 * those of bset2, using the fact that entry bset1->eq[row][col]=a
118 * is non-zero. Initially, these elements of bset1 are all zero.
119 * For each row i < row, we set
120 * A[i] = a * A[i] + B[i][col] * A[row]
121 * B[i] = a * B[i]
122 * so that
123 * A[i][col] = B[i][col] = a * old(B[i][col])
124 */
125 static void construct_column(
126 struct isl_basic_set *bset1, struct isl_basic_set *bset2,
127 unsigned row, unsigned col)
128 {
129 int r;
130 isl_int a;
131 isl_int b;
132 unsigned total;
133  
134 isl_int_init(a);
135 isl_int_init(b);
136 total = 1 + isl_basic_set_n_dim(bset1);
137 for (r = 0; r < row; ++r) {
138 if (isl_int_is_zero(bset2->eq[r][col]))
139 continue;
140 isl_int_gcd(b, bset2->eq[r][col], bset1->eq[row][col]);
141 isl_int_divexact(a, bset1->eq[row][col], b);
142 isl_int_divexact(b, bset2->eq[r][col], b);
143 isl_seq_combine(bset1->eq[r], a, bset1->eq[r],
144 b, bset1->eq[row], total);
145 isl_seq_scale(bset2->eq[r], bset2->eq[r], a, total);
146 }
147 isl_int_clear(a);
148 isl_int_clear(b);
149 delete_row(bset1, row);
150 }
151  
152 /* Make first row entries in column col of bset1 identical to
153 * those of bset2, using only these entries of the two matrices.
154 * Let t be the last row with different entries.
155 * For each row i < t, we set
156 * A[i] = (A[t][col]-B[t][col]) * A[i] + (B[i][col]-A[i][col) * A[t]
157 * B[i] = (A[t][col]-B[t][col]) * B[i] + (B[i][col]-A[i][col) * B[t]
158 * so that
159 * A[i][col] = B[i][col] = old(A[t][col]*B[i][col]-A[i][col]*B[t][col])
160 */
161 static int transform_column(
162 struct isl_basic_set *bset1, struct isl_basic_set *bset2,
163 unsigned row, unsigned col)
164 {
165 int i, t;
166 isl_int a, b, g;
167 unsigned total;
168  
169 for (t = row-1; t >= 0; --t)
170 if (isl_int_ne(bset1->eq[t][col], bset2->eq[t][col]))
171 break;
172 if (t < 0)
173 return 0;
174  
175 total = 1 + isl_basic_set_n_dim(bset1);
176 isl_int_init(a);
177 isl_int_init(b);
178 isl_int_init(g);
179 isl_int_sub(b, bset1->eq[t][col], bset2->eq[t][col]);
180 for (i = 0; i < t; ++i) {
181 isl_int_sub(a, bset2->eq[i][col], bset1->eq[i][col]);
182 isl_int_gcd(g, a, b);
183 isl_int_divexact(a, a, g);
184 isl_int_divexact(g, b, g);
185 isl_seq_combine(bset1->eq[i], g, bset1->eq[i], a, bset1->eq[t],
186 total);
187 isl_seq_combine(bset2->eq[i], g, bset2->eq[i], a, bset2->eq[t],
188 total);
189 }
190 isl_int_clear(a);
191 isl_int_clear(b);
192 isl_int_clear(g);
193 delete_row(bset1, t);
194 delete_row(bset2, t);
195 return 1;
196 }
197  
198 /* The implementation is based on Section 5.2 of Michael Karr,
199 * "Affine Relationships Among Variables of a Program",
200 * except that the echelon form we use starts from the last column
201 * and that we are dealing with integer coefficients.
202 */
203 static struct isl_basic_set *affine_hull(
204 struct isl_basic_set *bset1, struct isl_basic_set *bset2)
205 {
206 unsigned total;
207 int col;
208 int row;
209  
210 if (!bset1 || !bset2)
211 goto error;
212  
213 total = 1 + isl_basic_set_n_dim(bset1);
214  
215 row = 0;
216 for (col = total-1; col >= 0; --col) {
217 int is_zero1 = row >= bset1->n_eq ||
218 isl_int_is_zero(bset1->eq[row][col]);
219 int is_zero2 = row >= bset2->n_eq ||
220 isl_int_is_zero(bset2->eq[row][col]);
221 if (!is_zero1 && !is_zero2) {
222 set_common_multiple(bset1, bset2, row, col);
223 ++row;
224 } else if (!is_zero1 && is_zero2) {
225 construct_column(bset1, bset2, row, col);
226 } else if (is_zero1 && !is_zero2) {
227 construct_column(bset2, bset1, row, col);
228 } else {
229 if (transform_column(bset1, bset2, row, col))
230 --row;
231 }
232 }
233 isl_assert(bset1->ctx, row == bset1->n_eq, goto error);
234 isl_basic_set_free(bset2);
235 bset1 = isl_basic_set_normalize_constraints(bset1);
236 return bset1;
237 error:
238 isl_basic_set_free(bset1);
239 isl_basic_set_free(bset2);
240 return NULL;
241 }
242  
243 /* Find an integer point in the set represented by "tab"
244 * that lies outside of the equality "eq" e(x) = 0.
245 * If "up" is true, look for a point satisfying e(x) - 1 >= 0.
246 * Otherwise, look for a point satisfying -e(x) - 1 >= 0 (i.e., e(x) <= -1).
247 * The point, if found, is returned.
248 * If no point can be found, a zero-length vector is returned.
249 *
250 * Before solving an ILP problem, we first check if simply
251 * adding the normal of the constraint to one of the known
252 * integer points in the basic set represented by "tab"
253 * yields another point inside the basic set.
254 *
255 * The caller of this function ensures that the tableau is bounded or
256 * that tab->basis and tab->n_unbounded have been set appropriately.
257 */
258 static struct isl_vec *outside_point(struct isl_tab *tab, isl_int *eq, int up)
259 {
260 struct isl_ctx *ctx;
261 struct isl_vec *sample = NULL;
262 struct isl_tab_undo *snap;
263 unsigned dim;
264  
265 if (!tab)
266 return NULL;
267 ctx = tab->mat->ctx;
268  
269 dim = tab->n_var;
270 sample = isl_vec_alloc(ctx, 1 + dim);
271 if (!sample)
272 return NULL;
273 isl_int_set_si(sample->el[0], 1);
274 isl_seq_combine(sample->el + 1,
275 ctx->one, tab->bmap->sample->el + 1,
276 up ? ctx->one : ctx->negone, eq + 1, dim);
277 if (isl_basic_map_contains(tab->bmap, sample))
278 return sample;
279 isl_vec_free(sample);
280 sample = NULL;
281  
282 snap = isl_tab_snap(tab);
283  
284 if (!up)
285 isl_seq_neg(eq, eq, 1 + dim);
286 isl_int_sub_ui(eq[0], eq[0], 1);
287  
288 if (isl_tab_extend_cons(tab, 1) < 0)
289 goto error;
290 if (isl_tab_add_ineq(tab, eq) < 0)
291 goto error;
292  
293 sample = isl_tab_sample(tab);
294  
295 isl_int_add_ui(eq[0], eq[0], 1);
296 if (!up)
297 isl_seq_neg(eq, eq, 1 + dim);
298  
299 if (sample && isl_tab_rollback(tab, snap) < 0)
300 goto error;
301  
302 return sample;
303 error:
304 isl_vec_free(sample);
305 return NULL;
306 }
307  
308 struct isl_basic_set *isl_basic_set_recession_cone(struct isl_basic_set *bset)
309 {
310 int i;
311  
312 bset = isl_basic_set_cow(bset);
313 if (!bset)
314 return NULL;
315 isl_assert(bset->ctx, bset->n_div == 0, goto error);
316  
317 for (i = 0; i < bset->n_eq; ++i)
318 isl_int_set_si(bset->eq[i][0], 0);
319  
320 for (i = 0; i < bset->n_ineq; ++i)
321 isl_int_set_si(bset->ineq[i][0], 0);
322  
323 ISL_F_CLR(bset, ISL_BASIC_SET_NO_IMPLICIT);
324 return isl_basic_set_implicit_equalities(bset);
325 error:
326 isl_basic_set_free(bset);
327 return NULL;
328 }
329  
330 __isl_give isl_set *isl_set_recession_cone(__isl_take isl_set *set)
331 {
332 int i;
333  
334 if (!set)
335 return NULL;
336 if (set->n == 0)
337 return set;
338  
339 set = isl_set_remove_divs(set);
340 set = isl_set_cow(set);
341 if (!set)
342 return NULL;
343  
344 for (i = 0; i < set->n; ++i) {
345 set->p[i] = isl_basic_set_recession_cone(set->p[i]);
346 if (!set->p[i])
347 goto error;
348 }
349  
350 return set;
351 error:
352 isl_set_free(set);
353 return NULL;
354 }
355  
356 /* Move "sample" to a point that is one up (or down) from the original
357 * point in dimension "pos".
358 */
359 static void adjacent_point(__isl_keep isl_vec *sample, int pos, int up)
360 {
361 if (up)
362 isl_int_add_ui(sample->el[1 + pos], sample->el[1 + pos], 1);
363 else
364 isl_int_sub_ui(sample->el[1 + pos], sample->el[1 + pos], 1);
365 }
366  
367 /* Check if any points that are adjacent to "sample" also belong to "bset".
368 * If so, add them to "hull" and return the updated hull.
369 *
370 * Before checking whether and adjacent point belongs to "bset", we first
371 * check whether it already belongs to "hull" as this test is typically
372 * much cheaper.
373 */
374 static __isl_give isl_basic_set *add_adjacent_points(
375 __isl_take isl_basic_set *hull, __isl_take isl_vec *sample,
376 __isl_keep isl_basic_set *bset)
377 {
378 int i, up;
379 int dim;
380  
381 if (!sample)
382 goto error;
383  
384 dim = isl_basic_set_dim(hull, isl_dim_set);
385  
386 for (i = 0; i < dim; ++i) {
387 for (up = 0; up <= 1; ++up) {
388 int contains;
389 isl_basic_set *point;
390  
391 adjacent_point(sample, i, up);
392 contains = isl_basic_set_contains(hull, sample);
393 if (contains < 0)
394 goto error;
395 if (contains) {
396 adjacent_point(sample, i, !up);
397 continue;
398 }
399 contains = isl_basic_set_contains(bset, sample);
400 if (contains < 0)
401 goto error;
402 if (contains) {
403 point = isl_basic_set_from_vec(
404 isl_vec_copy(sample));
405 hull = affine_hull(hull, point);
406 }
407 adjacent_point(sample, i, !up);
408 if (contains)
409 break;
410 }
411 }
412  
413 isl_vec_free(sample);
414  
415 return hull;
416 error:
417 isl_vec_free(sample);
418 isl_basic_set_free(hull);
419 return NULL;
420 }
421  
422 /* Extend an initial (under-)approximation of the affine hull of basic
423 * set represented by the tableau "tab"
424 * by looking for points that do not satisfy one of the equalities
425 * in the current approximation and adding them to that approximation
426 * until no such points can be found any more.
427 *
428 * The caller of this function ensures that "tab" is bounded or
429 * that tab->basis and tab->n_unbounded have been set appropriately.
430 *
431 * "bset" may be either NULL or the basic set represented by "tab".
432 * If "bset" is not NULL, we check for any point we find if any
433 * of its adjacent points also belong to "bset".
434 */
435 static __isl_give isl_basic_set *extend_affine_hull(struct isl_tab *tab,
436 __isl_take isl_basic_set *hull, __isl_keep isl_basic_set *bset)
437 {
438 int i, j;
439 unsigned dim;
440  
441 if (!tab || !hull)
442 goto error;
443  
444 dim = tab->n_var;
445  
446 if (isl_tab_extend_cons(tab, 2 * dim + 1) < 0)
447 goto error;
448  
449 for (i = 0; i < dim; ++i) {
450 struct isl_vec *sample;
451 struct isl_basic_set *point;
452 for (j = 0; j < hull->n_eq; ++j) {
453 sample = outside_point(tab, hull->eq[j], 1);
454 if (!sample)
455 goto error;
456 if (sample->size > 0)
457 break;
458 isl_vec_free(sample);
459 sample = outside_point(tab, hull->eq[j], 0);
460 if (!sample)
461 goto error;
462 if (sample->size > 0)
463 break;
464 isl_vec_free(sample);
465  
466 if (isl_tab_add_eq(tab, hull->eq[j]) < 0)
467 goto error;
468 }
469 if (j == hull->n_eq)
470 break;
471 if (tab->samples)
472 tab = isl_tab_add_sample(tab, isl_vec_copy(sample));
473 if (!tab)
474 goto error;
475 if (bset)
476 hull = add_adjacent_points(hull, isl_vec_copy(sample),
477 bset);
478 point = isl_basic_set_from_vec(sample);
479 hull = affine_hull(hull, point);
480 if (!hull)
481 return NULL;
482 }
483  
484 return hull;
485 error:
486 isl_basic_set_free(hull);
487 return NULL;
488 }
489  
490 /* Drop all constraints in bset that involve any of the dimensions
491 * first to first+n-1.
492 */
493 __isl_give isl_basic_set *isl_basic_set_drop_constraints_involving(
494 __isl_take isl_basic_set *bset, unsigned first, unsigned n)
495 {
496 int i;
497  
498 if (n == 0)
499 return bset;
500  
501 bset = isl_basic_set_cow(bset);
502  
503 if (!bset)
504 return NULL;
505  
506 for (i = bset->n_eq - 1; i >= 0; --i) {
507 if (isl_seq_first_non_zero(bset->eq[i] + 1 + first, n) == -1)
508 continue;
509 isl_basic_set_drop_equality(bset, i);
510 }
511  
512 for (i = bset->n_ineq - 1; i >= 0; --i) {
513 if (isl_seq_first_non_zero(bset->ineq[i] + 1 + first, n) == -1)
514 continue;
515 isl_basic_set_drop_inequality(bset, i);
516 }
517  
518 return bset;
519 }
520  
521 /* Construct an initial underapproximatino of the hull of "bset"
522 * from "sample" and any of its adjacent points that also belong to "bset".
523 */
524 static __isl_give isl_basic_set *initialize_hull(__isl_keep isl_basic_set *bset,
525 __isl_take isl_vec *sample)
526 {
527 isl_basic_set *hull;
528  
529 hull = isl_basic_set_from_vec(isl_vec_copy(sample));
530 hull = add_adjacent_points(hull, sample, bset);
531  
532 return hull;
533 }
534  
535 /* Look for all equalities satisfied by the integer points in bset,
536 * which is assumed to be bounded.
537 *
538 * The equalities are obtained by successively looking for
539 * a point that is affinely independent of the points found so far.
540 * In particular, for each equality satisfied by the points so far,
541 * we check if there is any point on a hyperplane parallel to the
542 * corresponding hyperplane shifted by at least one (in either direction).
543 */
544 static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset)
545 {
546 struct isl_vec *sample = NULL;
547 struct isl_basic_set *hull;
548 struct isl_tab *tab = NULL;
549 unsigned dim;
550  
551 if (isl_basic_set_plain_is_empty(bset))
552 return bset;
553  
554 dim = isl_basic_set_n_dim(bset);
555  
556 if (bset->sample && bset->sample->size == 1 + dim) {
557 int contains = isl_basic_set_contains(bset, bset->sample);
558 if (contains < 0)
559 goto error;
560 if (contains) {
561 if (dim == 0)
562 return bset;
563 sample = isl_vec_copy(bset->sample);
564 } else {
565 isl_vec_free(bset->sample);
566 bset->sample = NULL;
567 }
568 }
569  
570 tab = isl_tab_from_basic_set(bset, 1);
571 if (!tab)
572 goto error;
573 if (tab->empty) {
574 isl_tab_free(tab);
575 isl_vec_free(sample);
576 return isl_basic_set_set_to_empty(bset);
577 }
578  
579 if (!sample) {
580 struct isl_tab_undo *snap;
581 snap = isl_tab_snap(tab);
582 sample = isl_tab_sample(tab);
583 if (isl_tab_rollback(tab, snap) < 0)
584 goto error;
585 isl_vec_free(tab->bmap->sample);
586 tab->bmap->sample = isl_vec_copy(sample);
587 }
588  
589 if (!sample)
590 goto error;
591 if (sample->size == 0) {
592 isl_tab_free(tab);
593 isl_vec_free(sample);
594 return isl_basic_set_set_to_empty(bset);
595 }
596  
597 hull = initialize_hull(bset, sample);
598  
599 hull = extend_affine_hull(tab, hull, bset);
600 isl_basic_set_free(bset);
601 isl_tab_free(tab);
602  
603 return hull;
604 error:
605 isl_vec_free(sample);
606 isl_tab_free(tab);
607 isl_basic_set_free(bset);
608 return NULL;
609 }
610  
611 /* Given an unbounded tableau and an integer point satisfying the tableau,
612 * construct an initial affine hull containing the recession cone
613 * shifted to the given point.
614 *
615 * The unbounded directions are taken from the last rows of the basis,
616 * which is assumed to have been initialized appropriately.
617 */
618 static __isl_give isl_basic_set *initial_hull(struct isl_tab *tab,
619 __isl_take isl_vec *vec)
620 {
621 int i;
622 int k;
623 struct isl_basic_set *bset = NULL;
624 struct isl_ctx *ctx;
625 unsigned dim;
626  
627 if (!vec || !tab)
628 return NULL;
629 ctx = vec->ctx;
630 isl_assert(ctx, vec->size != 0, goto error);
631  
632 bset = isl_basic_set_alloc(ctx, 0, vec->size - 1, 0, vec->size - 1, 0);
633 if (!bset)
634 goto error;
635 dim = isl_basic_set_n_dim(bset) - tab->n_unbounded;
636 for (i = 0; i < dim; ++i) {
637 k = isl_basic_set_alloc_equality(bset);
638 if (k < 0)
639 goto error;
640 isl_seq_cpy(bset->eq[k] + 1, tab->basis->row[1 + i] + 1,
641 vec->size - 1);
642 isl_seq_inner_product(bset->eq[k] + 1, vec->el +1,
643 vec->size - 1, &bset->eq[k][0]);
644 isl_int_neg(bset->eq[k][0], bset->eq[k][0]);
645 }
646 bset->sample = vec;
647 bset = isl_basic_set_gauss(bset, NULL);
648  
649 return bset;
650 error:
651 isl_basic_set_free(bset);
652 isl_vec_free(vec);
653 return NULL;
654 }
655  
656 /* Given a tableau of a set and a tableau of the corresponding
657 * recession cone, detect and add all equalities to the tableau.
658 * If the tableau is bounded, then we can simply keep the
659 * tableau in its state after the return from extend_affine_hull.
660 * However, if the tableau is unbounded, then
661 * isl_tab_set_initial_basis_with_cone will add some additional
662 * constraints to the tableau that have to be removed again.
663 * In this case, we therefore rollback to the state before
664 * any constraints were added and then add the equalities back in.
665 */
666 struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab,
667 struct isl_tab *tab_cone)
668 {
669 int j;
670 struct isl_vec *sample;
671 struct isl_basic_set *hull;
672 struct isl_tab_undo *snap;
673  
674 if (!tab || !tab_cone)
675 goto error;
676  
677 snap = isl_tab_snap(tab);
678  
679 isl_mat_free(tab->basis);
680 tab->basis = NULL;
681  
682 isl_assert(tab->mat->ctx, tab->bmap, goto error);
683 isl_assert(tab->mat->ctx, tab->samples, goto error);
684 isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, goto error);
685 isl_assert(tab->mat->ctx, tab->n_sample > tab->n_outside, goto error);
686  
687 if (isl_tab_set_initial_basis_with_cone(tab, tab_cone) < 0)
688 goto error;
689  
690 sample = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
691 if (!sample)
692 goto error;
693  
694 isl_seq_cpy(sample->el, tab->samples->row[tab->n_outside], sample->size);
695  
696 isl_vec_free(tab->bmap->sample);
697 tab->bmap->sample = isl_vec_copy(sample);
698  
699 if (tab->n_unbounded == 0)
700 hull = isl_basic_set_from_vec(isl_vec_copy(sample));
701 else
702 hull = initial_hull(tab, isl_vec_copy(sample));
703  
704 for (j = tab->n_outside + 1; j < tab->n_sample; ++j) {
705 isl_seq_cpy(sample->el, tab->samples->row[j], sample->size);
706 hull = affine_hull(hull,
707 isl_basic_set_from_vec(isl_vec_copy(sample)));
708 }
709  
710 isl_vec_free(sample);
711  
712 hull = extend_affine_hull(tab, hull, NULL);
713 if (!hull)
714 goto error;
715  
716 if (tab->n_unbounded == 0) {
717 isl_basic_set_free(hull);
718 return tab;
719 }
720  
721 if (isl_tab_rollback(tab, snap) < 0)
722 goto error;
723  
724 if (hull->n_eq > tab->n_zero) {
725 for (j = 0; j < hull->n_eq; ++j) {
726 isl_seq_normalize(tab->mat->ctx, hull->eq[j], 1 + tab->n_var);
727 if (isl_tab_add_eq(tab, hull->eq[j]) < 0)
728 goto error;
729 }
730 }
731  
732 isl_basic_set_free(hull);
733  
734 return tab;
735 error:
736 isl_tab_free(tab);
737 return NULL;
738 }
739  
740 /* Compute the affine hull of "bset", where "cone" is the recession cone
741 * of "bset".
742 *
743 * We first compute a unimodular transformation that puts the unbounded
744 * directions in the last dimensions. In particular, we take a transformation
745 * that maps all equalities to equalities (in HNF) on the first dimensions.
746 * Let x be the original dimensions and y the transformed, with y_1 bounded
747 * and y_2 unbounded.
748 *
749 * [ y_1 ] [ y_1 ] [ Q_1 ]
750 * x = U [ y_2 ] [ y_2 ] = [ Q_2 ] x
751 *
752 * Let's call the input basic set S. We compute S' = preimage(S, U)
753 * and drop the final dimensions including any constraints involving them.
754 * This results in set S''.
755 * Then we compute the affine hull A'' of S''.
756 * Let F y_1 >= g be the constraint system of A''. In the transformed
757 * space the y_2 are unbounded, so we can add them back without any constraints,
758 * resulting in
759 *
760 * [ y_1 ]
761 * [ F 0 ] [ y_2 ] >= g
762 * or
763 * [ Q_1 ]
764 * [ F 0 ] [ Q_2 ] x >= g
765 * or
766 * F Q_1 x >= g
767 *
768 * The affine hull in the original space is then obtained as
769 * A = preimage(A'', Q_1).
770 */
771 static struct isl_basic_set *affine_hull_with_cone(struct isl_basic_set *bset,
772 struct isl_basic_set *cone)
773 {
774 unsigned total;
775 unsigned cone_dim;
776 struct isl_basic_set *hull;
777 struct isl_mat *M, *U, *Q;
778  
779 if (!bset || !cone)
780 goto error;
781  
782 total = isl_basic_set_total_dim(cone);
783 cone_dim = total - cone->n_eq;
784  
785 M = isl_mat_sub_alloc6(bset->ctx, cone->eq, 0, cone->n_eq, 1, total);
786 M = isl_mat_left_hermite(M, 0, &U, &Q);
787 if (!M)
788 goto error;
789 isl_mat_free(M);
790  
791 U = isl_mat_lin_to_aff(U);
792 bset = isl_basic_set_preimage(bset, isl_mat_copy(U));
793  
794 bset = isl_basic_set_drop_constraints_involving(bset, total - cone_dim,
795 cone_dim);
796 bset = isl_basic_set_drop_dims(bset, total - cone_dim, cone_dim);
797  
798 Q = isl_mat_lin_to_aff(Q);
799 Q = isl_mat_drop_rows(Q, 1 + total - cone_dim, cone_dim);
800  
801 if (bset && bset->sample && bset->sample->size == 1 + total)
802 bset->sample = isl_mat_vec_product(isl_mat_copy(Q), bset->sample);
803  
804 hull = uset_affine_hull_bounded(bset);
805  
806 if (!hull)
807 isl_mat_free(U);
808 else {
809 struct isl_vec *sample = isl_vec_copy(hull->sample);
810 U = isl_mat_drop_cols(U, 1 + total - cone_dim, cone_dim);
811 if (sample && sample->size > 0)
812 sample = isl_mat_vec_product(U, sample);
813 else
814 isl_mat_free(U);
815 hull = isl_basic_set_preimage(hull, Q);
816 if (hull) {
817 isl_vec_free(hull->sample);
818 hull->sample = sample;
819 } else
820 isl_vec_free(sample);
821 }
822  
823 isl_basic_set_free(cone);
824  
825 return hull;
826 error:
827 isl_basic_set_free(bset);
828 isl_basic_set_free(cone);
829 return NULL;
830 }
831  
832 /* Look for all equalities satisfied by the integer points in bset,
833 * which is assumed not to have any explicit equalities.
834 *
835 * The equalities are obtained by successively looking for
836 * a point that is affinely independent of the points found so far.
837 * In particular, for each equality satisfied by the points so far,
838 * we check if there is any point on a hyperplane parallel to the
839 * corresponding hyperplane shifted by at least one (in either direction).
840 *
841 * Before looking for any outside points, we first compute the recession
842 * cone. The directions of this recession cone will always be part
843 * of the affine hull, so there is no need for looking for any points
844 * in these directions.
845 * In particular, if the recession cone is full-dimensional, then
846 * the affine hull is simply the whole universe.
847 */
848 static struct isl_basic_set *uset_affine_hull(struct isl_basic_set *bset)
849 {
850 struct isl_basic_set *cone;
851  
852 if (isl_basic_set_plain_is_empty(bset))
853 return bset;
854  
855 cone = isl_basic_set_recession_cone(isl_basic_set_copy(bset));
856 if (!cone)
857 goto error;
858 if (cone->n_eq == 0) {
859 struct isl_basic_set *hull;
860 isl_basic_set_free(cone);
861 hull = isl_basic_set_universe_like(bset);
862 isl_basic_set_free(bset);
863 return hull;
864 }
865  
866 if (cone->n_eq < isl_basic_set_total_dim(cone))
867 return affine_hull_with_cone(bset, cone);
868  
869 isl_basic_set_free(cone);
870 return uset_affine_hull_bounded(bset);
871 error:
872 isl_basic_set_free(bset);
873 return NULL;
874 }
875  
876 /* Look for all equalities satisfied by the integer points in bmap
877 * that are independent of the equalities already explicitly available
878 * in bmap.
879 *
880 * We first remove all equalities already explicitly available,
881 * then look for additional equalities in the reduced space
882 * and then transform the result to the original space.
883 * The original equalities are _not_ added to this set. This is
884 * the responsibility of the calling function.
885 * The resulting basic set has all meaning about the dimensions removed.
886 * In particular, dimensions that correspond to existential variables
887 * in bmap and that are found to be fixed are not removed.
888 */
889 static struct isl_basic_set *equalities_in_underlying_set(
890 struct isl_basic_map *bmap)
891 {
892 struct isl_mat *T1 = NULL;
893 struct isl_mat *T2 = NULL;
894 struct isl_basic_set *bset = NULL;
895 struct isl_basic_set *hull = NULL;
896  
897 bset = isl_basic_map_underlying_set(bmap);
898 if (!bset)
899 return NULL;
900 if (bset->n_eq)
901 bset = isl_basic_set_remove_equalities(bset, &T1, &T2);
902 if (!bset)
903 goto error;
904  
905 hull = uset_affine_hull(bset);
906 if (!T2)
907 return hull;
908  
909 if (!hull) {
910 isl_mat_free(T1);
911 isl_mat_free(T2);
912 } else {
913 struct isl_vec *sample = isl_vec_copy(hull->sample);
914 if (sample && sample->size > 0)
915 sample = isl_mat_vec_product(T1, sample);
916 else
917 isl_mat_free(T1);
918 hull = isl_basic_set_preimage(hull, T2);
919 if (hull) {
920 isl_vec_free(hull->sample);
921 hull->sample = sample;
922 } else
923 isl_vec_free(sample);
924 }
925  
926 return hull;
927 error:
928 isl_mat_free(T2);
929 isl_basic_set_free(bset);
930 isl_basic_set_free(hull);
931 return NULL;
932 }
933  
934 /* Detect and make explicit all equalities satisfied by the (integer)
935 * points in bmap.
936 */
937 struct isl_basic_map *isl_basic_map_detect_equalities(
938 struct isl_basic_map *bmap)
939 {
940 int i, j;
941 struct isl_basic_set *hull = NULL;
942  
943 if (!bmap)
944 return NULL;
945 if (bmap->n_ineq == 0)
946 return bmap;
947 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
948 return bmap;
949 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_ALL_EQUALITIES))
950 return bmap;
951 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
952 return isl_basic_map_implicit_equalities(bmap);
953  
954 hull = equalities_in_underlying_set(isl_basic_map_copy(bmap));
955 if (!hull)
956 goto error;
957 if (ISL_F_ISSET(hull, ISL_BASIC_SET_EMPTY)) {
958 isl_basic_set_free(hull);
959 return isl_basic_map_set_to_empty(bmap);
960 }
961 bmap = isl_basic_map_extend_space(bmap, isl_space_copy(bmap->dim), 0,
962 hull->n_eq, 0);
963 for (i = 0; i < hull->n_eq; ++i) {
964 j = isl_basic_map_alloc_equality(bmap);
965 if (j < 0)
966 goto error;
967 isl_seq_cpy(bmap->eq[j], hull->eq[i],
968 1 + isl_basic_set_total_dim(hull));
969 }
970 isl_vec_free(bmap->sample);
971 bmap->sample = isl_vec_copy(hull->sample);
972 isl_basic_set_free(hull);
973 ISL_F_SET(bmap, ISL_BASIC_MAP_NO_IMPLICIT | ISL_BASIC_MAP_ALL_EQUALITIES);
974 bmap = isl_basic_map_simplify(bmap);
975 return isl_basic_map_finalize(bmap);
976 error:
977 isl_basic_set_free(hull);
978 isl_basic_map_free(bmap);
979 return NULL;
980 }
981  
982 __isl_give isl_basic_set *isl_basic_set_detect_equalities(
983 __isl_take isl_basic_set *bset)
984 {
985 return (isl_basic_set *)
986 isl_basic_map_detect_equalities((isl_basic_map *)bset);
987 }
988  
989 __isl_give isl_map *isl_map_inline_foreach_basic_map(__isl_take isl_map *map,
990 __isl_give isl_basic_map *(*fn)(__isl_take isl_basic_map *bmap))
991 {
992 struct isl_basic_map *bmap;
993 int i;
994  
995 if (!map)
996 return NULL;
997  
998 for (i = 0; i < map->n; ++i) {
999 bmap = isl_basic_map_copy(map->p[i]);
1000 bmap = fn(bmap);
1001 if (!bmap)
1002 goto error;
1003 isl_basic_map_free(map->p[i]);
1004 map->p[i] = bmap;
1005 }
1006  
1007 return map;
1008 error:
1009 isl_map_free(map);
1010 return NULL;
1011 }
1012  
1013 __isl_give isl_map *isl_map_detect_equalities(__isl_take isl_map *map)
1014 {
1015 return isl_map_inline_foreach_basic_map(map,
1016 &isl_basic_map_detect_equalities);
1017 }
1018  
1019 __isl_give isl_set *isl_set_detect_equalities(__isl_take isl_set *set)
1020 {
1021 return (isl_set *)isl_map_detect_equalities((isl_map *)set);
1022 }
1023  
1024 /* After computing the rational affine hull (by detecting the implicit
1025 * equalities), we compute the additional equalities satisfied by
1026 * the integer points (if any) and add the original equalities back in.
1027 */
1028 struct isl_basic_map *isl_basic_map_affine_hull(struct isl_basic_map *bmap)
1029 {
1030 bmap = isl_basic_map_detect_equalities(bmap);
1031 bmap = isl_basic_map_cow(bmap);
1032 if (bmap)
1033 isl_basic_map_free_inequality(bmap, bmap->n_ineq);
1034 bmap = isl_basic_map_finalize(bmap);
1035 return bmap;
1036 }
1037  
1038 struct isl_basic_set *isl_basic_set_affine_hull(struct isl_basic_set *bset)
1039 {
1040 return (struct isl_basic_set *)
1041 isl_basic_map_affine_hull((struct isl_basic_map *)bset);
1042 }
1043  
1044 struct isl_basic_map *isl_map_affine_hull(struct isl_map *map)
1045 {
1046 int i;
1047 struct isl_basic_map *model = NULL;
1048 struct isl_basic_map *hull = NULL;
1049 struct isl_set *set;
1050  
1051 map = isl_map_detect_equalities(map);
1052 map = isl_map_align_divs(map);
1053  
1054 if (!map)
1055 return NULL;
1056  
1057 if (map->n == 0) {
1058 hull = isl_basic_map_empty_like_map(map);
1059 isl_map_free(map);
1060 return hull;
1061 }
1062  
1063 model = isl_basic_map_copy(map->p[0]);
1064 set = isl_map_underlying_set(map);
1065 set = isl_set_cow(set);
1066 if (!set)
1067 goto error;
1068  
1069 for (i = 0; i < set->n; ++i) {
1070 set->p[i] = isl_basic_set_cow(set->p[i]);
1071 set->p[i] = isl_basic_set_affine_hull(set->p[i]);
1072 set->p[i] = isl_basic_set_gauss(set->p[i], NULL);
1073 if (!set->p[i])
1074 goto error;
1075 }
1076 set = isl_set_remove_empty_parts(set);
1077 if (set->n == 0) {
1078 hull = isl_basic_map_empty_like(model);
1079 isl_basic_map_free(model);
1080 } else {
1081 struct isl_basic_set *bset;
1082 while (set->n > 1) {
1083 set->p[0] = affine_hull(set->p[0], set->p[--set->n]);
1084 if (!set->p[0])
1085 goto error;
1086 }
1087 bset = isl_basic_set_copy(set->p[0]);
1088 hull = isl_basic_map_overlying_set(bset, model);
1089 }
1090 isl_set_free(set);
1091 hull = isl_basic_map_simplify(hull);
1092 return isl_basic_map_finalize(hull);
1093 error:
1094 isl_basic_map_free(model);
1095 isl_set_free(set);
1096 return NULL;
1097 }
1098  
1099 struct isl_basic_set *isl_set_affine_hull(struct isl_set *set)
1100 {
1101 return (struct isl_basic_set *)
1102 isl_map_affine_hull((struct isl_map *)set);
1103 }