add missing AUTHORS file
[isl.git] / isl_affine_hull.c
bloba1335984acf59223a242ddbc62169b0277452624
1 #include "isl_ctx.h"
2 #include "isl_seq.h"
3 #include "isl_set.h"
4 #include "isl_lp.h"
5 #include "isl_map.h"
6 #include "isl_map_private.h"
7 #include "isl_equalities.h"
8 #include "isl_sample.h"
9 #include "isl_tab.h"
11 struct isl_basic_map *isl_basic_map_implicit_equalities(
12 struct isl_basic_map *bmap)
14 struct isl_tab *tab;
16 if (!bmap)
17 return bmap;
19 bmap = isl_basic_map_gauss(bmap, NULL);
20 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
21 return bmap;
22 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_NO_IMPLICIT))
23 return bmap;
24 if (bmap->n_ineq <= 1)
25 return bmap;
27 tab = isl_tab_from_basic_map(bmap);
28 tab = isl_tab_detect_implicit_equalities(tab);
29 bmap = isl_basic_map_update_from_tab(bmap, tab);
30 isl_tab_free(tab);
31 bmap = isl_basic_map_gauss(bmap, NULL);
32 ISL_F_SET(bmap, ISL_BASIC_MAP_NO_IMPLICIT);
33 return bmap;
36 struct isl_basic_set *isl_basic_set_implicit_equalities(
37 struct isl_basic_set *bset)
39 return (struct isl_basic_set *)
40 isl_basic_map_implicit_equalities((struct isl_basic_map*)bset);
43 struct isl_map *isl_map_implicit_equalities(struct isl_map *map)
45 int i;
47 if (!map)
48 return map;
50 for (i = 0; i < map->n; ++i) {
51 map->p[i] = isl_basic_map_implicit_equalities(map->p[i]);
52 if (!map->p[i])
53 goto error;
56 return map;
57 error:
58 isl_map_free(map);
59 return NULL;
62 /* Make eq[row][col] of both bmaps equal so we can add the row
63 * add the column to the common matrix.
64 * Note that because of the echelon form, the columns of row row
65 * after column col are zero.
67 static void set_common_multiple(
68 struct isl_basic_set *bset1, struct isl_basic_set *bset2,
69 unsigned row, unsigned col)
71 isl_int m, c;
73 if (isl_int_eq(bset1->eq[row][col], bset2->eq[row][col]))
74 return;
76 isl_int_init(c);
77 isl_int_init(m);
78 isl_int_lcm(m, bset1->eq[row][col], bset2->eq[row][col]);
79 isl_int_divexact(c, m, bset1->eq[row][col]);
80 isl_seq_scale(bset1->eq[row], bset1->eq[row], c, col+1);
81 isl_int_divexact(c, m, bset2->eq[row][col]);
82 isl_seq_scale(bset2->eq[row], bset2->eq[row], c, col+1);
83 isl_int_clear(c);
84 isl_int_clear(m);
87 /* Delete a given equality, moving all the following equalities one up.
89 static void delete_row(struct isl_basic_set *bset, unsigned row)
91 isl_int *t;
92 int r;
94 t = bset->eq[row];
95 bset->n_eq--;
96 for (r = row; r < bset->n_eq; ++r)
97 bset->eq[r] = bset->eq[r+1];
98 bset->eq[bset->n_eq] = t;
101 /* Make first row entries in column col of bset1 identical to
102 * those of bset2, using the fact that entry bset1->eq[row][col]=a
103 * is non-zero. Initially, these elements of bset1 are all zero.
104 * For each row i < row, we set
105 * A[i] = a * A[i] + B[i][col] * A[row]
106 * B[i] = a * B[i]
107 * so that
108 * A[i][col] = B[i][col] = a * old(B[i][col])
110 static void construct_column(
111 struct isl_basic_set *bset1, struct isl_basic_set *bset2,
112 unsigned row, unsigned col)
114 int r;
115 isl_int a;
116 isl_int b;
117 unsigned total;
119 isl_int_init(a);
120 isl_int_init(b);
121 total = 1 + isl_basic_set_n_dim(bset1);
122 for (r = 0; r < row; ++r) {
123 if (isl_int_is_zero(bset2->eq[r][col]))
124 continue;
125 isl_int_gcd(b, bset2->eq[r][col], bset1->eq[row][col]);
126 isl_int_divexact(a, bset1->eq[row][col], b);
127 isl_int_divexact(b, bset2->eq[r][col], b);
128 isl_seq_combine(bset1->eq[r], a, bset1->eq[r],
129 b, bset1->eq[row], total);
130 isl_seq_scale(bset2->eq[r], bset2->eq[r], a, total);
132 isl_int_clear(a);
133 isl_int_clear(b);
134 delete_row(bset1, row);
137 /* Make first row entries in column col of bset1 identical to
138 * those of bset2, using only these entries of the two matrices.
139 * Let t be the last row with different entries.
140 * For each row i < t, we set
141 * A[i] = (A[t][col]-B[t][col]) * A[i] + (B[i][col]-A[i][col) * A[t]
142 * B[i] = (A[t][col]-B[t][col]) * B[i] + (B[i][col]-A[i][col) * B[t]
143 * so that
144 * A[i][col] = B[i][col] = old(A[t][col]*B[i][col]-A[i][col]*B[t][col])
146 static int transform_column(
147 struct isl_basic_set *bset1, struct isl_basic_set *bset2,
148 unsigned row, unsigned col)
150 int i, t;
151 isl_int a, b, g;
152 unsigned total;
154 for (t = row-1; t >= 0; --t)
155 if (isl_int_ne(bset1->eq[t][col], bset2->eq[t][col]))
156 break;
157 if (t < 0)
158 return 0;
160 total = 1 + isl_basic_set_n_dim(bset1);
161 isl_int_init(a);
162 isl_int_init(b);
163 isl_int_init(g);
164 isl_int_sub(b, bset1->eq[t][col], bset2->eq[t][col]);
165 for (i = 0; i < t; ++i) {
166 isl_int_sub(a, bset2->eq[i][col], bset1->eq[i][col]);
167 isl_int_gcd(g, a, b);
168 isl_int_divexact(a, a, g);
169 isl_int_divexact(g, b, g);
170 isl_seq_combine(bset1->eq[i], g, bset1->eq[i], a, bset1->eq[t],
171 total);
172 isl_seq_combine(bset2->eq[i], g, bset2->eq[i], a, bset2->eq[t],
173 total);
175 isl_int_clear(a);
176 isl_int_clear(b);
177 isl_int_clear(g);
178 delete_row(bset1, t);
179 delete_row(bset2, t);
180 return 1;
183 /* The implementation is based on Section 5.2 of Michael Karr,
184 * "Affine Relationships Among Variables of a Program",
185 * except that the echelon form we use starts from the last column
186 * and that we are dealing with integer coefficients.
188 static struct isl_basic_set *affine_hull(
189 struct isl_basic_set *bset1, struct isl_basic_set *bset2)
191 unsigned total;
192 int col;
193 int row;
195 total = 1 + isl_basic_set_n_dim(bset1);
197 row = 0;
198 for (col = total-1; col >= 0; --col) {
199 int is_zero1 = row >= bset1->n_eq ||
200 isl_int_is_zero(bset1->eq[row][col]);
201 int is_zero2 = row >= bset2->n_eq ||
202 isl_int_is_zero(bset2->eq[row][col]);
203 if (!is_zero1 && !is_zero2) {
204 set_common_multiple(bset1, bset2, row, col);
205 ++row;
206 } else if (!is_zero1 && is_zero2) {
207 construct_column(bset1, bset2, row, col);
208 } else if (is_zero1 && !is_zero2) {
209 construct_column(bset2, bset1, row, col);
210 } else {
211 if (transform_column(bset1, bset2, row, col))
212 --row;
215 isl_basic_set_free(bset2);
216 isl_assert(bset1->ctx, row == bset1->n_eq, goto error);
217 bset1 = isl_basic_set_normalize_constraints(bset1);
218 return bset1;
219 error:
220 isl_basic_set_free(bset1);
221 return NULL;
224 /* Find an integer point in the set represented by "tab"
225 * that lies outside of the equality "eq" e(x) = 0.
226 * If "up" is true, look for a point satisfying e(x) - 1 >= 0.
227 * Otherwise, look for a point satisfying -e(x) - 1 >= 0 (i.e., e(x) <= -1).
228 * The point, if found, is returned.
229 * If no point can be found, a zero-length vector is returned.
231 * Before solving an ILP problem, we first check if simply
232 * adding the normal of the constraint to one of the known
233 * integer points in the basic set represented by "tab"
234 * yields another point inside the basic set.
236 * The caller of this function ensures that the tableau is bounded or
237 * that tab->basis and tab->n_unbounded have been set appropriately.
239 static struct isl_vec *outside_point(struct isl_tab *tab, isl_int *eq, int up)
241 struct isl_ctx *ctx;
242 struct isl_vec *sample;
243 struct isl_tab_undo *snap;
244 unsigned dim;
245 int k;
247 if (!tab)
248 return NULL;
249 ctx = tab->mat->ctx;
251 dim = tab->n_var;
252 sample = isl_vec_alloc(ctx, 1 + dim);
253 if (!sample)
254 return NULL;
255 isl_int_set_si(sample->el[0], 1);
256 isl_seq_combine(sample->el + 1,
257 ctx->one, tab->bset->sample->el + 1,
258 up ? ctx->one : ctx->negone, eq + 1, dim);
259 if (isl_basic_set_contains(tab->bset, sample))
260 return sample;
261 isl_vec_free(sample);
262 sample = NULL;
264 snap = isl_tab_snap(tab);
266 if (!up)
267 isl_seq_neg(eq, eq, 1 + dim);
268 isl_int_sub_ui(eq[0], eq[0], 1);
270 if (isl_tab_extend_cons(tab, 1) < 0)
271 goto error;
272 tab = isl_tab_add_ineq(tab, eq);
274 sample = isl_tab_sample(tab);
276 isl_int_add_ui(eq[0], eq[0], 1);
277 if (!up)
278 isl_seq_neg(eq, eq, 1 + dim);
280 if (isl_tab_rollback(tab, snap) < 0)
281 goto error;
283 return sample;
284 error:
285 isl_vec_free(sample);
286 return NULL;
289 struct isl_basic_set *isl_basic_set_recession_cone(struct isl_basic_set *bset)
291 int i;
293 bset = isl_basic_set_cow(bset);
294 if (!bset)
295 return NULL;
296 isl_assert(bset->ctx, bset->n_div == 0, goto error);
298 for (i = 0; i < bset->n_eq; ++i)
299 isl_int_set_si(bset->eq[i][0], 0);
301 for (i = 0; i < bset->n_ineq; ++i)
302 isl_int_set_si(bset->ineq[i][0], 0);
304 ISL_F_CLR(bset, ISL_BASIC_SET_NO_IMPLICIT);
305 return isl_basic_set_implicit_equalities(bset);
306 error:
307 isl_basic_set_free(bset);
308 return NULL;
311 /* Extend an initial (under-)approximation of the affine hull of basic
312 * set represented by the tableau "tab"
313 * by looking for points that do not satisfy one of the equalities
314 * in the current approximation and adding them to that approximation
315 * until no such points can be found any more.
317 * The caller of this function ensures that "tab" is bounded or
318 * that tab->basis and tab->n_unbounded have been set appropriately.
320 static struct isl_basic_set *extend_affine_hull(struct isl_tab *tab,
321 struct isl_basic_set *hull)
323 int i, j, k;
324 unsigned dim;
326 if (!tab || !hull)
327 goto error;
329 dim = tab->n_var;
331 if (isl_tab_extend_cons(tab, 2 * dim + 1) < 0)
332 goto error;
334 for (i = 0; i < dim; ++i) {
335 struct isl_vec *sample;
336 struct isl_basic_set *point;
337 for (j = 0; j < hull->n_eq; ++j) {
338 sample = outside_point(tab, hull->eq[j], 1);
339 if (!sample)
340 goto error;
341 if (sample->size > 0)
342 break;
343 isl_vec_free(sample);
344 sample = outside_point(tab, hull->eq[j], 0);
345 if (!sample)
346 goto error;
347 if (sample->size > 0)
348 break;
349 isl_vec_free(sample);
351 tab = isl_tab_add_eq(tab, hull->eq[j]);
352 if (!tab)
353 goto error;
355 if (j == hull->n_eq)
356 break;
357 if (tab->samples)
358 tab = isl_tab_add_sample(tab, isl_vec_copy(sample));
359 if (!tab)
360 goto error;
361 point = isl_basic_set_from_vec(sample);
362 hull = affine_hull(hull, point);
365 return hull;
366 error:
367 isl_basic_set_free(hull);
368 return NULL;
371 /* Drop all constraints in bset that involve any of the dimensions
372 * first to first+n-1.
374 static struct isl_basic_set *drop_constraints_involving
375 (struct isl_basic_set *bset, unsigned first, unsigned n)
377 int i;
379 if (!bset)
380 return NULL;
382 bset = isl_basic_set_cow(bset);
384 for (i = bset->n_eq - 1; i >= 0; --i) {
385 if (isl_seq_first_non_zero(bset->eq[i] + 1 + first, n) == -1)
386 continue;
387 isl_basic_set_drop_equality(bset, i);
390 for (i = bset->n_ineq - 1; i >= 0; --i) {
391 if (isl_seq_first_non_zero(bset->ineq[i] + 1 + first, n) == -1)
392 continue;
393 isl_basic_set_drop_inequality(bset, i);
396 return bset;
399 /* Look for all equalities satisfied by the integer points in bset,
400 * which is assumed to be bounded.
402 * The equalities are obtained by successively looking for
403 * a point that is affinely independent of the points found so far.
404 * In particular, for each equality satisfied by the points so far,
405 * we check if there is any point on a hyperplane parallel to the
406 * corresponding hyperplane shifted by at least one (in either direction).
408 static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset)
410 struct isl_vec *sample = NULL;
411 struct isl_basic_set *hull;
412 struct isl_tab *tab = NULL;
413 unsigned dim;
415 if (isl_basic_set_fast_is_empty(bset))
416 return bset;
418 dim = isl_basic_set_n_dim(bset);
420 if (bset->sample && bset->sample->size == 1 + dim) {
421 int contains = isl_basic_set_contains(bset, bset->sample);
422 if (contains < 0)
423 goto error;
424 if (contains) {
425 if (dim == 0)
426 return bset;
427 sample = isl_vec_copy(bset->sample);
428 } else {
429 isl_vec_free(bset->sample);
430 bset->sample = NULL;
434 tab = isl_tab_from_basic_set(bset);
435 if (!tab)
436 goto error;
437 tab->bset = isl_basic_set_copy(bset);
439 if (!sample) {
440 struct isl_tab_undo *snap;
441 snap = isl_tab_snap(tab);
442 sample = isl_tab_sample(tab);
443 if (isl_tab_rollback(tab, snap) < 0)
444 goto error;
445 isl_vec_free(tab->bset->sample);
446 tab->bset->sample = isl_vec_copy(sample);
449 if (!sample)
450 goto error;
451 if (sample->size == 0) {
452 isl_tab_free(tab);
453 isl_vec_free(sample);
454 return isl_basic_set_set_to_empty(bset);
457 hull = isl_basic_set_from_vec(sample);
459 isl_basic_set_free(bset);
460 hull = extend_affine_hull(tab, hull);
461 isl_tab_free(tab);
463 return hull;
464 error:
465 isl_vec_free(sample);
466 isl_tab_free(tab);
467 isl_basic_set_free(bset);
468 return NULL;
471 /* Given an unbounded tableau and an integer point satisfying the tableau,
472 * construct an intial affine hull containing the recession cone
473 * shifted to the given point.
475 * The unbounded directions are taken from the last rows of the basis,
476 * which is assumed to have been initialized appropriately.
478 static __isl_give isl_basic_set *initial_hull(struct isl_tab *tab,
479 __isl_take isl_vec *vec)
481 int i;
482 int k;
483 struct isl_basic_set *bset = NULL;
484 struct isl_ctx *ctx;
485 unsigned dim;
487 if (!vec || !tab)
488 return NULL;
489 ctx = vec->ctx;
490 isl_assert(ctx, vec->size != 0, goto error);
492 bset = isl_basic_set_alloc(ctx, 0, vec->size - 1, 0, vec->size - 1, 0);
493 if (!bset)
494 goto error;
495 dim = isl_basic_set_n_dim(bset) - tab->n_unbounded;
496 for (i = 0; i < dim; ++i) {
497 k = isl_basic_set_alloc_equality(bset);
498 if (k < 0)
499 goto error;
500 isl_seq_cpy(bset->eq[k] + 1, tab->basis->row[1 + i] + 1,
501 vec->size - 1);
502 isl_seq_inner_product(bset->eq[k] + 1, vec->el +1,
503 vec->size - 1, &bset->eq[k][0]);
504 isl_int_neg(bset->eq[k][0], bset->eq[k][0]);
506 bset->sample = vec;
507 bset = isl_basic_set_gauss(bset, NULL);
509 return bset;
510 error:
511 isl_basic_set_free(bset);
512 isl_vec_free(vec);
513 return NULL;
516 /* Given a tableau of a set and a tableau of the corresponding
517 * recession cone, detect and add all equalities to the tableau.
518 * If the tableau is bounded, then we can simply keep the
519 * tableau in its state after the return from extend_affine_hull.
520 * However, if the tableau is unbounded, then
521 * isl_tab_set_initial_basis_with_cone will add some additional
522 * constraints to the tableau that have to be removed again.
523 * In this case, we therefore rollback to the state before
524 * any constraints were added and then add the eqaulities back in.
526 struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab,
527 struct isl_tab *tab_cone)
529 int j;
530 struct isl_vec *sample;
531 struct isl_basic_set *hull;
532 struct isl_tab_undo *snap;
534 if (!tab || !tab_cone)
535 goto error;
537 snap = isl_tab_snap(tab);
539 isl_mat_free(tab->basis);
540 tab->basis = NULL;
542 isl_assert(tab->mat->ctx, tab->bset, goto error);
543 isl_assert(tab->mat->ctx, tab->samples, goto error);
544 isl_assert(tab->mat->ctx, tab->samples->n_col == 1 + tab->n_var, goto error);
545 isl_assert(tab->mat->ctx, tab->n_sample > tab->n_outside, goto error);
547 if (isl_tab_set_initial_basis_with_cone(tab, tab_cone) < 0)
548 goto error;
550 sample = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
551 if (!sample)
552 goto error;
554 isl_seq_cpy(sample->el, tab->samples->row[tab->n_outside], sample->size);
556 isl_vec_free(tab->bset->sample);
557 tab->bset->sample = isl_vec_copy(sample);
559 if (tab->n_unbounded == 0)
560 hull = isl_basic_set_from_vec(isl_vec_copy(sample));
561 else
562 hull = initial_hull(tab, isl_vec_copy(sample));
564 for (j = tab->n_outside + 1; j < tab->n_sample; ++j) {
565 isl_seq_cpy(sample->el, tab->samples->row[j], sample->size);
566 hull = affine_hull(hull,
567 isl_basic_set_from_vec(isl_vec_copy(sample)));
570 isl_vec_free(sample);
572 hull = extend_affine_hull(tab, hull);
573 if (!hull)
574 goto error;
576 if (tab->n_unbounded == 0) {
577 isl_basic_set_free(hull);
578 return tab;
581 if (isl_tab_rollback(tab, snap) < 0)
582 goto error;
584 if (hull->n_eq > tab->n_zero) {
585 for (j = 0; j < hull->n_eq; ++j) {
586 isl_seq_normalize(tab->mat->ctx, hull->eq[j], 1 + tab->n_var);
587 tab = isl_tab_add_eq(tab, hull->eq[j]);
591 isl_basic_set_free(hull);
593 return tab;
594 error:
595 isl_tab_free(tab);
596 return NULL;
599 /* Compute the affine hull of "bset", where "cone" is the recession cone
600 * of "bset".
602 * We first compute a unimodular transformation that puts the unbounded
603 * directions in the last dimensions. In particular, we take a transformation
604 * that maps all equalities to equalities (in HNF) on the first dimensions.
605 * Let x be the original dimensions and y the transformed, with y_1 bounded
606 * and y_2 unbounded.
608 * [ y_1 ] [ y_1 ] [ Q_1 ]
609 * x = U [ y_2 ] [ y_2 ] = [ Q_2 ] x
611 * Let's call the input basic set S. We compute S' = preimage(S, U)
612 * and drop the final dimensions including any constraints involving them.
613 * This results in set S''.
614 * Then we compute the affine hull A'' of S''.
615 * Let F y_1 >= g be the constraint system of A''. In the transformed
616 * space the y_2 are unbounded, so we can add them back without any constraints,
617 * resulting in
619 * [ y_1 ]
620 * [ F 0 ] [ y_2 ] >= g
621 * or
622 * [ Q_1 ]
623 * [ F 0 ] [ Q_2 ] x >= g
624 * or
625 * F Q_1 x >= g
627 * The affine hull in the original space is then obtained as
628 * A = preimage(A'', Q_1).
630 static struct isl_basic_set *affine_hull_with_cone(struct isl_basic_set *bset,
631 struct isl_basic_set *cone)
633 unsigned total;
634 unsigned cone_dim;
635 struct isl_basic_set *hull;
636 struct isl_mat *M, *U, *Q;
638 if (!bset || !cone)
639 goto error;
641 total = isl_basic_set_total_dim(cone);
642 cone_dim = total - cone->n_eq;
644 M = isl_mat_sub_alloc(bset->ctx, cone->eq, 0, cone->n_eq, 1, total);
645 M = isl_mat_left_hermite(M, 0, &U, &Q);
646 if (!M)
647 goto error;
648 isl_mat_free(M);
650 U = isl_mat_lin_to_aff(U);
651 bset = isl_basic_set_preimage(bset, isl_mat_copy(U));
653 bset = drop_constraints_involving(bset, total - cone_dim, cone_dim);
654 bset = isl_basic_set_drop_dims(bset, total - cone_dim, cone_dim);
656 Q = isl_mat_lin_to_aff(Q);
657 Q = isl_mat_drop_rows(Q, 1 + total - cone_dim, cone_dim);
659 if (bset && bset->sample && bset->sample->size == 1 + total)
660 bset->sample = isl_mat_vec_product(isl_mat_copy(Q), bset->sample);
662 hull = uset_affine_hull_bounded(bset);
664 if (!hull)
665 isl_mat_free(U);
666 else {
667 struct isl_vec *sample = isl_vec_copy(hull->sample);
668 U = isl_mat_drop_cols(U, 1 + total - cone_dim, cone_dim);
669 if (sample && sample->size > 0)
670 sample = isl_mat_vec_product(U, sample);
671 else
672 isl_mat_free(U);
673 hull = isl_basic_set_preimage(hull, Q);
674 isl_vec_free(hull->sample);
675 hull->sample = sample;
678 isl_basic_set_free(cone);
680 return hull;
681 error:
682 isl_basic_set_free(bset);
683 isl_basic_set_free(cone);
684 return NULL;
687 /* Look for all equalities satisfied by the integer points in bset,
688 * which is assumed not to have any explicit equalities.
690 * The equalities are obtained by successively looking for
691 * a point that is affinely independent of the points found so far.
692 * In particular, for each equality satisfied by the points so far,
693 * we check if there is any point on a hyperplane parallel to the
694 * corresponding hyperplane shifted by at least one (in either direction).
696 * Before looking for any outside points, we first compute the recession
697 * cone. The directions of this recession cone will always be part
698 * of the affine hull, so there is no need for looking for any points
699 * in these directions.
700 * In particular, if the recession cone is full-dimensional, then
701 * the affine hull is simply the whole universe.
703 static struct isl_basic_set *uset_affine_hull(struct isl_basic_set *bset)
705 struct isl_basic_set *cone;
707 if (isl_basic_set_fast_is_empty(bset))
708 return bset;
710 cone = isl_basic_set_recession_cone(isl_basic_set_copy(bset));
711 if (!cone)
712 goto error;
713 if (cone->n_eq == 0) {
714 struct isl_basic_set *hull;
715 isl_basic_set_free(cone);
716 hull = isl_basic_set_universe_like(bset);
717 isl_basic_set_free(bset);
718 return hull;
721 if (cone->n_eq < isl_basic_set_total_dim(cone))
722 return affine_hull_with_cone(bset, cone);
724 isl_basic_set_free(cone);
725 return uset_affine_hull_bounded(bset);
726 error:
727 isl_basic_set_free(bset);
728 return NULL;
731 /* Look for all equalities satisfied by the integer points in bmap
732 * that are independent of the equalities already explicitly available
733 * in bmap.
735 * We first remove all equalities already explicitly available,
736 * then look for additional equalities in the reduced space
737 * and then transform the result to the original space.
738 * The original equalities are _not_ added to this set. This is
739 * the responsibility of the calling function.
740 * The resulting basic set has all meaning about the dimensions removed.
741 * In particular, dimensions that correspond to existential variables
742 * in bmap and that are found to be fixed are not removed.
744 static struct isl_basic_set *equalities_in_underlying_set(
745 struct isl_basic_map *bmap)
747 struct isl_mat *T1 = NULL;
748 struct isl_mat *T2 = NULL;
749 struct isl_basic_set *bset = NULL;
750 struct isl_basic_set *hull = NULL;
752 bset = isl_basic_map_underlying_set(bmap);
753 if (!bset)
754 return NULL;
755 if (bset->n_eq)
756 bset = isl_basic_set_remove_equalities(bset, &T1, &T2);
757 if (!bset)
758 goto error;
760 hull = uset_affine_hull(bset);
761 if (!T2)
762 return hull;
764 if (!hull)
765 isl_mat_free(T1);
766 else {
767 struct isl_vec *sample = isl_vec_copy(hull->sample);
768 if (sample && sample->size > 0)
769 sample = isl_mat_vec_product(T1, sample);
770 else
771 isl_mat_free(T1);
772 hull = isl_basic_set_preimage(hull, T2);
773 isl_vec_free(hull->sample);
774 hull->sample = sample;
777 return hull;
778 error:
779 isl_mat_free(T2);
780 isl_basic_set_free(bset);
781 isl_basic_set_free(hull);
782 return NULL;
785 /* Detect and make explicit all equalities satisfied by the (integer)
786 * points in bmap.
788 struct isl_basic_map *isl_basic_map_detect_equalities(
789 struct isl_basic_map *bmap)
791 int i, j;
792 struct isl_basic_set *hull = NULL;
794 if (!bmap)
795 return NULL;
796 if (bmap->n_ineq == 0)
797 return bmap;
798 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
799 return bmap;
800 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_ALL_EQUALITIES))
801 return bmap;
802 if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
803 return isl_basic_map_implicit_equalities(bmap);
805 hull = equalities_in_underlying_set(isl_basic_map_copy(bmap));
806 if (!hull)
807 goto error;
808 if (ISL_F_ISSET(hull, ISL_BASIC_SET_EMPTY)) {
809 isl_basic_set_free(hull);
810 return isl_basic_map_set_to_empty(bmap);
812 bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim), 0,
813 hull->n_eq, 0);
814 for (i = 0; i < hull->n_eq; ++i) {
815 j = isl_basic_map_alloc_equality(bmap);
816 if (j < 0)
817 goto error;
818 isl_seq_cpy(bmap->eq[j], hull->eq[i],
819 1 + isl_basic_set_total_dim(hull));
821 isl_vec_free(bmap->sample);
822 bmap->sample = isl_vec_copy(hull->sample);
823 isl_basic_set_free(hull);
824 ISL_F_SET(bmap, ISL_BASIC_MAP_NO_IMPLICIT | ISL_BASIC_MAP_ALL_EQUALITIES);
825 bmap = isl_basic_map_simplify(bmap);
826 return isl_basic_map_finalize(bmap);
827 error:
828 isl_basic_set_free(hull);
829 isl_basic_map_free(bmap);
830 return NULL;
833 __isl_give isl_basic_set *isl_basic_set_detect_equalities(
834 __isl_take isl_basic_set *bset)
836 return (isl_basic_set *)
837 isl_basic_map_detect_equalities((isl_basic_map *)bset);
840 struct isl_map *isl_map_detect_equalities(struct isl_map *map)
842 struct isl_basic_map *bmap;
843 int i;
845 if (!map)
846 return NULL;
848 for (i = 0; i < map->n; ++i) {
849 bmap = isl_basic_map_copy(map->p[i]);
850 bmap = isl_basic_map_detect_equalities(bmap);
851 if (!bmap)
852 goto error;
853 isl_basic_map_free(map->p[i]);
854 map->p[i] = bmap;
857 return map;
858 error:
859 isl_map_free(map);
860 return NULL;
863 __isl_give isl_set *isl_set_detect_equalities(__isl_take isl_set *set)
865 return (isl_set *)isl_map_detect_equalities((isl_map *)set);
868 /* After computing the rational affine hull (by detecting the implicit
869 * equalities), we compute the additional equalities satisfied by
870 * the integer points (if any) and add the original equalities back in.
872 struct isl_basic_map *isl_basic_map_affine_hull(struct isl_basic_map *bmap)
874 bmap = isl_basic_map_detect_equalities(bmap);
875 bmap = isl_basic_map_cow(bmap);
876 isl_basic_map_free_inequality(bmap, bmap->n_ineq);
877 return bmap;
880 struct isl_basic_set *isl_basic_set_affine_hull(struct isl_basic_set *bset)
882 return (struct isl_basic_set *)
883 isl_basic_map_affine_hull((struct isl_basic_map *)bset);
886 struct isl_basic_map *isl_map_affine_hull(struct isl_map *map)
888 int i;
889 struct isl_basic_map *model = NULL;
890 struct isl_basic_map *hull = NULL;
891 struct isl_set *set;
893 if (!map)
894 return NULL;
896 if (map->n == 0) {
897 hull = isl_basic_map_empty_like_map(map);
898 isl_map_free(map);
899 return hull;
902 map = isl_map_detect_equalities(map);
903 map = isl_map_align_divs(map);
904 if (!map)
905 return NULL;
906 model = isl_basic_map_copy(map->p[0]);
907 set = isl_map_underlying_set(map);
908 set = isl_set_cow(set);
909 if (!set)
910 goto error;
912 for (i = 0; i < set->n; ++i) {
913 set->p[i] = isl_basic_set_cow(set->p[i]);
914 set->p[i] = isl_basic_set_affine_hull(set->p[i]);
915 set->p[i] = isl_basic_set_gauss(set->p[i], NULL);
916 if (!set->p[i])
917 goto error;
919 set = isl_set_remove_empty_parts(set);
920 if (set->n == 0) {
921 hull = isl_basic_map_empty_like(model);
922 isl_basic_map_free(model);
923 } else {
924 struct isl_basic_set *bset;
925 while (set->n > 1) {
926 set->p[0] = affine_hull(set->p[0], set->p[--set->n]);
927 if (!set->p[0])
928 goto error;
930 bset = isl_basic_set_copy(set->p[0]);
931 hull = isl_basic_map_overlying_set(bset, model);
933 isl_set_free(set);
934 hull = isl_basic_map_simplify(hull);
935 return isl_basic_map_finalize(hull);
936 error:
937 isl_basic_map_free(model);
938 isl_set_free(set);
939 return NULL;
942 struct isl_basic_set *isl_set_affine_hull(struct isl_set *set)
944 return (struct isl_basic_set *)
945 isl_map_affine_hull((struct isl_map *)set);