1 #include "isl_map_private.h"
4 #define STATUS_ERROR -1
5 #define STATUS_REDUNDANT 1
7 #define STATUS_SEPARATE 3
9 #define STATUS_ADJ_EQ 5
10 #define STATUS_ADJ_INEQ 6
12 static int status_in(isl_int *ineq, struct isl_tab *tab)
14 enum isl_ineq_type type = isl_tab_ineq_type(tab, ineq);
16 case isl_ineq_error: return STATUS_ERROR;
17 case isl_ineq_redundant: return STATUS_VALID;
18 case isl_ineq_separate: return STATUS_SEPARATE;
19 case isl_ineq_cut: return STATUS_CUT;
20 case isl_ineq_adj_eq: return STATUS_ADJ_EQ;
21 case isl_ineq_adj_ineq: return STATUS_ADJ_INEQ;
25 /* Compute the position of the equalities of basic map "i"
26 * with respect to basic map "j".
27 * The resulting array has twice as many entries as the number
28 * of equalities corresponding to the two inequalties to which
29 * each equality corresponds.
31 static int *eq_status_in(struct isl_map *map, int i, int j,
32 struct isl_tab **tabs)
35 int *eq = isl_calloc_array(map->ctx, int, 2 * map->p[i]->n_eq);
38 dim = isl_basic_map_total_dim(map->p[i]);
39 for (k = 0; k < map->p[i]->n_eq; ++k) {
40 for (l = 0; l < 2; ++l) {
41 isl_seq_neg(map->p[i]->eq[k], map->p[i]->eq[k], 1+dim);
42 eq[2 * k + l] = status_in(map->p[i]->eq[k], tabs[j]);
43 if (eq[2 * k + l] == STATUS_ERROR)
46 if (eq[2 * k] == STATUS_SEPARATE ||
47 eq[2 * k + 1] == STATUS_SEPARATE)
57 /* Compute the position of the inequalities of basic map "i"
58 * with respect to basic map "j".
60 static int *ineq_status_in(struct isl_map *map, int i, int j,
61 struct isl_tab **tabs)
64 unsigned n_eq = map->p[i]->n_eq;
65 int *ineq = isl_calloc_array(map->ctx, int, map->p[i]->n_ineq);
67 for (k = 0; k < map->p[i]->n_ineq; ++k) {
68 if (isl_tab_is_redundant(tabs[i], n_eq + k)) {
69 ineq[k] = STATUS_REDUNDANT;
72 ineq[k] = status_in(map->p[i]->ineq[k], tabs[j]);
73 if (ineq[k] == STATUS_ERROR)
75 if (ineq[k] == STATUS_SEPARATE)
85 static int any(int *con, unsigned len, int status)
89 for (i = 0; i < len ; ++i)
95 static int count(int *con, unsigned len, int status)
100 for (i = 0; i < len ; ++i)
101 if (con[i] == status)
106 static int all(int *con, unsigned len, int status)
110 for (i = 0; i < len ; ++i) {
111 if (con[i] == STATUS_REDUNDANT)
113 if (con[i] != status)
119 static void drop(struct isl_map *map, int i, struct isl_tab **tabs)
121 isl_basic_map_free(map->p[i]);
122 isl_tab_free(tabs[i]);
124 if (i != map->n - 1) {
125 map->p[i] = map->p[map->n - 1];
126 tabs[i] = tabs[map->n - 1];
128 tabs[map->n - 1] = NULL;
132 /* Replace the pair of basic maps i and j but the basic map bounded
133 * by the valid constraints in both basic maps.
135 static int fuse(struct isl_map *map, int i, int j, struct isl_tab **tabs,
136 int *ineq_i, int *ineq_j)
139 struct isl_basic_map *fused = NULL;
140 struct isl_tab *fused_tab = NULL;
141 unsigned total = isl_basic_map_total_dim(map->p[i]);
143 fused = isl_basic_map_alloc_dim(isl_dim_copy(map->p[i]->dim),
145 map->p[i]->n_eq + map->p[j]->n_eq,
146 map->p[i]->n_ineq + map->p[j]->n_ineq);
150 for (k = 0; k < map->p[i]->n_eq; ++k) {
151 int l = isl_basic_map_alloc_equality(fused);
152 isl_seq_cpy(fused->eq[l], map->p[i]->eq[k], 1 + total);
155 for (k = 0; k < map->p[j]->n_eq; ++k) {
156 int l = isl_basic_map_alloc_equality(fused);
157 isl_seq_cpy(fused->eq[l], map->p[j]->eq[k], 1 + total);
160 for (k = 0; k < map->p[i]->n_ineq; ++k) {
161 if (ineq_i[k] != STATUS_VALID)
163 l = isl_basic_map_alloc_inequality(fused);
164 isl_seq_cpy(fused->ineq[l], map->p[i]->ineq[k], 1 + total);
167 for (k = 0; k < map->p[j]->n_ineq; ++k) {
168 if (ineq_j[k] != STATUS_VALID)
170 l = isl_basic_map_alloc_inequality(fused);
171 isl_seq_cpy(fused->ineq[l], map->p[j]->ineq[k], 1 + total);
174 for (k = 0; k < map->p[i]->n_div; ++k) {
175 int l = isl_basic_map_alloc_div(fused);
176 isl_seq_cpy(fused->div[l], map->p[i]->div[k], 1 + 1 + total);
179 fused = isl_basic_map_gauss(fused, NULL);
180 ISL_F_SET(fused, ISL_BASIC_MAP_FINAL);
182 fused_tab = isl_tab_from_basic_map(fused);
183 fused_tab = isl_tab_detect_redundant(fused_tab);
187 isl_basic_map_free(map->p[i]);
189 isl_tab_free(tabs[i]);
195 isl_basic_map_free(fused);
199 /* Given a pair of basic maps i and j such that all constraints are either
200 * "valid" or "cut", check if the facets corresponding to the "cut"
201 * constraints of i lie entirely within basic map j.
202 * If so, replace the pair by the basic map consisting of the valid
203 * constraints in both basic maps.
205 * To see that we are not introducing any extra points, call the
206 * two basic maps A and B and the resulting map U and let x
207 * be an element of U \setminus ( A \cup B ).
208 * Then there is a pair of cut constraints c_1 and c_2 in A and B such that x
209 * violates them. Let X be the intersection of U with the opposites
210 * of these constraints. Then x \in X.
211 * The facet corresponding to c_1 contains the corresponding facet of A.
212 * This facet is entirely contained in B, so c_2 is valid on the facet.
213 * However, since it is also (part of) a facet of X, -c_2 is also valid
214 * on the facet. This means c_2 is saturated on the facet, so c_1 and
215 * c_2 must be opposites of each other, but then x could not violate
218 static int check_facets(struct isl_map *map, int i, int j,
219 struct isl_tab **tabs, int *ineq_i, int *ineq_j)
222 struct isl_tab_undo *snap;
223 unsigned n_eq = map->p[i]->n_eq;
225 snap = isl_tab_snap(tabs[i]);
227 for (k = 0; k < map->p[i]->n_ineq; ++k) {
228 if (ineq_i[k] != STATUS_CUT)
230 tabs[i] = isl_tab_select_facet(tabs[i], n_eq + k);
231 for (l = 0; l < map->p[j]->n_ineq; ++l) {
233 if (ineq_j[l] != STATUS_CUT)
235 stat = status_in(map->p[j]->ineq[l], tabs[i]);
236 if (stat != STATUS_VALID)
239 isl_tab_rollback(tabs[i], snap);
240 if (l < map->p[j]->n_ineq)
244 if (k < map->p[i]->n_ineq)
247 return fuse(map, i, j, tabs, ineq_i, ineq_j);
250 /* Both basic maps have at least one inequality with and adjacent
251 * (but opposite) inequality in the other basic map.
252 * Check that there are no cut constraints and that there is only
253 * a single pair of adjacent inequalities.
254 * If so, we can replace the pair by a single basic map described
255 * by all but the pair of adjacent inequalities.
256 * Any additional points introduced lie strictly between the two
257 * adjacent hyperplanes and can therefore be integral.
266 * The test for a single pair of adjancent inequalities is important
267 * for avoiding the combination of two basic maps like the following
277 static int check_adj_ineq(struct isl_map *map, int i, int j,
278 struct isl_tab **tabs, int *ineq_i, int *ineq_j)
282 if (any(ineq_i, map->p[i]->n_ineq, STATUS_CUT) ||
283 any(ineq_j, map->p[j]->n_ineq, STATUS_CUT))
286 else if (count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) == 1 &&
287 count(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ) == 1)
288 changed = fuse(map, i, j, tabs, ineq_i, ineq_j);
289 /* else ADJ INEQ TOO MANY */
294 /* Check if basic map "i" contains the basic map represented
295 * by the tableau "tab".
297 static int contains(struct isl_map *map, int i, int *ineq_i,
303 dim = isl_basic_map_total_dim(map->p[i]);
304 for (k = 0; k < map->p[i]->n_eq; ++k) {
305 for (l = 0; l < 2; ++l) {
307 isl_seq_neg(map->p[i]->eq[k], map->p[i]->eq[k], 1+dim);
308 stat = status_in(map->p[i]->eq[k], tab);
309 if (stat != STATUS_VALID)
314 for (k = 0; k < map->p[i]->n_ineq; ++k) {
316 if (ineq_i[k] == STATUS_REDUNDANT)
318 stat = status_in(map->p[i]->ineq[k], tab);
319 if (stat != STATUS_VALID)
325 /* At least one of the basic maps has an equality that is adjacent
326 * to inequality. Make sure that only one of the basic maps has
327 * such an equality and that the other basic map has exactly one
328 * inequality adjacent to an equality.
329 * We call the basic map that has the inequality "i" and the basic
330 * map that has the equality "j".
331 * If "i" has any "cut" inequality, then relaxing the inequality
332 * by one would not result in a basic map that contains the other
334 * Otherwise, we relax the constraint, compute the corresponding
335 * facet and check whether it is included in the other basic map.
336 * If so, we know that relaxing the constraint extend the basic
337 * map with exactly the other basic map (we already know that this
338 * other basic map is included in the extension, because there
339 * were no "cut" inequalities in "i") and we can replace the
340 * two basic maps by thie extension.
348 static int check_adj_eq(struct isl_map *map, int i, int j,
349 struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
354 struct isl_tab_undo *snap, *snap2;
355 unsigned n_eq = map->p[i]->n_eq;
357 if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ) &&
358 any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ))
359 /* ADJ EQ TOO MANY */
362 if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ))
363 return check_adj_eq(map, j, i, tabs,
364 eq_j, ineq_j, eq_i, ineq_i);
366 /* j has an equality adjacent to an inequality in i */
368 if (any(ineq_i, map->p[i]->n_ineq, STATUS_CUT))
371 if (count(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ) != 1 ||
372 count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_EQ) != 1 ||
373 any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_EQ) ||
374 any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
375 any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ))
376 /* ADJ EQ TOO MANY */
379 for (k = 0; k < map->p[i]->n_ineq ; ++k)
380 if (ineq_i[k] == STATUS_ADJ_EQ)
383 snap = isl_tab_snap(tabs[i]);
384 tabs[i] = isl_tab_relax(tabs[i], n_eq + k);
385 snap2 = isl_tab_snap(tabs[i]);
386 tabs[i] = isl_tab_select_facet(tabs[i], n_eq + k);
387 super = contains(map, j, ineq_j, tabs[i]);
389 isl_tab_rollback(tabs[i], snap2);
390 map->p[i] = isl_basic_map_cow(map->p[i]);
393 isl_int_add_ui(map->p[i]->ineq[k][0], map->p[i]->ineq[k][0], 1);
394 ISL_F_SET(map->p[i], ISL_BASIC_MAP_FINAL);
398 isl_tab_rollback(tabs[i], snap);
403 /* Check if the union of the given pair of basic maps
404 * can be represented by a single basic map.
405 * If so, replace the pair by the single basic map and return 1.
406 * Otherwise, return 0;
408 * We first check the effect of each constraint of one basic map
409 * on the other basic map.
410 * The constraint may be
411 * redundant the constraint is redundant in its own
412 * basic map and should be ignore and removed
414 * valid all (integer) points of the other basic map
415 * satisfy the constraint
416 * separate no (integer) point of the other basic map
417 * satisfies the constraint
418 * cut some but not all points of the other basic map
419 * satisfy the constraint
420 * adj_eq the given constraint is adjacent (on the outside)
421 * to an equality of the other basic map
422 * adj_ineq the given constraint is adjacent (on the outside)
423 * to an inequality of the other basic map
425 * We consider four cases in which we can replace the pair by a single
426 * basic map. We ignore all "redundant" constraints.
428 * 1. all constraints of one basic map are valid
429 * => the other basic map is a subset and can be removed
431 * 2. all constraints of both basic maps are either "valid" or "cut"
432 * and the facets corresponding to the "cut" constraints
433 * of one of the basic maps lies entirely inside the other basic map
434 * => the pair can be replaced by a basic map consisting
435 * of the valid constraints in both basic maps
437 * 3. there is a single pair of adjacent inequalities
438 * (all other constraints are "valid")
439 * => the pair can be replaced by a basic map consisting
440 * of the valid constraints in both basic maps
442 * 4. there is a single adjacent pair of an inequality and an equality,
443 * the other constraints of the basic map containing the inequality are
444 * "valid". Moreover, if the inequality the basic map is relaxed
445 * and then turned into an equality, then resulting facet lies
446 * entirely inside the other basic map
447 * => the pair can be replaced by the basic map containing
448 * the inequality, with the inequality relaxed.
450 * Throughout the computation, we maintain a collection of tableaus
451 * corresponding to the basic maps. When the basic maps are dropped
452 * or combined, the tableaus are modified accordingly.
454 static int coalesce_pair(struct isl_map *map, int i, int j,
455 struct isl_tab **tabs)
463 eq_i = eq_status_in(map, i, j, tabs);
464 if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ERROR))
466 if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_SEPARATE))
469 eq_j = eq_status_in(map, j, i, tabs);
470 if (any(eq_j, 2 * map->p[j]->n_eq, STATUS_ERROR))
472 if (any(eq_j, 2 * map->p[j]->n_eq, STATUS_SEPARATE))
475 ineq_i = ineq_status_in(map, i, j, tabs);
476 if (any(ineq_i, map->p[i]->n_ineq, STATUS_ERROR))
478 if (any(ineq_i, map->p[i]->n_ineq, STATUS_SEPARATE))
481 ineq_j = ineq_status_in(map, j, i, tabs);
482 if (any(ineq_j, map->p[j]->n_ineq, STATUS_ERROR))
484 if (any(ineq_j, map->p[j]->n_ineq, STATUS_SEPARATE))
487 if (all(eq_i, 2 * map->p[i]->n_eq, STATUS_VALID) &&
488 all(ineq_i, map->p[i]->n_ineq, STATUS_VALID)) {
491 } else if (all(eq_j, 2 * map->p[j]->n_eq, STATUS_VALID) &&
492 all(ineq_j, map->p[j]->n_ineq, STATUS_VALID)) {
495 } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_CUT) ||
496 any(eq_j, 2 * map->p[j]->n_eq, STATUS_CUT)) {
498 } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_EQ) ||
499 any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_EQ)) {
501 } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ) ||
502 any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ)) {
503 changed = check_adj_eq(map, i, j, tabs,
504 eq_i, ineq_i, eq_j, ineq_j);
505 } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_EQ) ||
506 any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_EQ)) {
509 } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
510 any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ)) {
511 changed = check_adj_ineq(map, i, j, tabs, ineq_i, ineq_j);
513 changed = check_facets(map, i, j, tabs, ineq_i, ineq_j);
529 static struct isl_map *coalesce(struct isl_map *map, struct isl_tab **tabs)
533 for (i = 0; i < map->n - 1; ++i)
534 for (j = i + 1; j < map->n; ++j) {
536 changed = coalesce_pair(map, i, j, tabs);
540 return coalesce(map, tabs);
548 /* For each pair of basic maps in the map, check if the union of the two
549 * can be represented by a single basic map.
550 * If so, replace the pair by the single basic map and start over.
552 struct isl_map *isl_map_coalesce(struct isl_map *map)
556 struct isl_tab **tabs = NULL;
564 map = isl_map_align_divs(map);
566 tabs = isl_calloc_array(map->ctx, struct isl_tab *, map->n);
571 for (i = 0; i < map->n; ++i) {
572 tabs[i] = isl_tab_from_basic_map(map->p[i]);
575 if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT))
576 tabs[i] = isl_tab_detect_equalities(tabs[i]);
577 if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT))
578 tabs[i] = isl_tab_detect_redundant(tabs[i]);
580 for (i = map->n - 1; i >= 0; --i)
584 map = coalesce(map, tabs);
587 for (i = 0; i < map->n; ++i) {
588 map->p[i] = isl_basic_map_update_from_tab(map->p[i],
590 map->p[i] = isl_basic_map_finalize(map->p[i]);
593 ISL_F_SET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT);
594 ISL_F_SET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT);
597 for (i = 0; i < n; ++i)
598 isl_tab_free(tabs[i]);
605 for (i = 0; i < n; ++i)
606 isl_tab_free(tabs[i]);
611 /* For each pair of basic sets in the set, check if the union of the two
612 * can be represented by a single basic set.
613 * If so, replace the pair by the single basic set and start over.
615 struct isl_set *isl_set_coalesce(struct isl_set *set)
617 (struct isl_set *)isl_map_coalesce((struct isl_map *)set);