1 #include "isl_map_private.h"
5 #define STATUS_ERROR -1
6 #define STATUS_REDUNDANT 1
8 #define STATUS_SEPARATE 3
10 #define STATUS_ADJ_EQ 5
11 #define STATUS_ADJ_INEQ 6
13 static int status_in(isl_int
*ineq
, struct isl_tab
*tab
)
15 enum isl_ineq_type type
= isl_tab_ineq_type(tab
, ineq
);
17 case isl_ineq_error
: return STATUS_ERROR
;
18 case isl_ineq_redundant
: return STATUS_VALID
;
19 case isl_ineq_separate
: return STATUS_SEPARATE
;
20 case isl_ineq_cut
: return STATUS_CUT
;
21 case isl_ineq_adj_eq
: return STATUS_ADJ_EQ
;
22 case isl_ineq_adj_ineq
: return STATUS_ADJ_INEQ
;
26 /* Compute the position of the equalities of basic map "i"
27 * with respect to basic map "j".
28 * The resulting array has twice as many entries as the number
29 * of equalities corresponding to the two inequalties to which
30 * each equality corresponds.
32 static int *eq_status_in(struct isl_map
*map
, int i
, int j
,
33 struct isl_tab
**tabs
)
36 int *eq
= isl_calloc_array(map
->ctx
, int, 2 * map
->p
[i
]->n_eq
);
39 dim
= isl_basic_map_total_dim(map
->p
[i
]);
40 for (k
= 0; k
< map
->p
[i
]->n_eq
; ++k
) {
41 for (l
= 0; l
< 2; ++l
) {
42 isl_seq_neg(map
->p
[i
]->eq
[k
], map
->p
[i
]->eq
[k
], 1+dim
);
43 eq
[2 * k
+ l
] = status_in(map
->p
[i
]->eq
[k
], tabs
[j
]);
44 if (eq
[2 * k
+ l
] == STATUS_ERROR
)
47 if (eq
[2 * k
] == STATUS_SEPARATE
||
48 eq
[2 * k
+ 1] == STATUS_SEPARATE
)
58 /* Compute the position of the inequalities of basic map "i"
59 * with respect to basic map "j".
61 static int *ineq_status_in(struct isl_map
*map
, int i
, int j
,
62 struct isl_tab
**tabs
)
65 unsigned n_eq
= map
->p
[i
]->n_eq
;
66 int *ineq
= isl_calloc_array(map
->ctx
, int, map
->p
[i
]->n_ineq
);
68 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
69 if (isl_tab_is_redundant(tabs
[i
], n_eq
+ k
)) {
70 ineq
[k
] = STATUS_REDUNDANT
;
73 ineq
[k
] = status_in(map
->p
[i
]->ineq
[k
], tabs
[j
]);
74 if (ineq
[k
] == STATUS_ERROR
)
76 if (ineq
[k
] == STATUS_SEPARATE
)
86 static int any(int *con
, unsigned len
, int status
)
90 for (i
= 0; i
< len
; ++i
)
96 static int count(int *con
, unsigned len
, int status
)
101 for (i
= 0; i
< len
; ++i
)
102 if (con
[i
] == status
)
107 static int all(int *con
, unsigned len
, int status
)
111 for (i
= 0; i
< len
; ++i
) {
112 if (con
[i
] == STATUS_REDUNDANT
)
114 if (con
[i
] != status
)
120 static void drop(struct isl_map
*map
, int i
, struct isl_tab
**tabs
)
122 isl_basic_map_free(map
->p
[i
]);
123 isl_tab_free(tabs
[i
]);
125 if (i
!= map
->n
- 1) {
126 map
->p
[i
] = map
->p
[map
->n
- 1];
127 tabs
[i
] = tabs
[map
->n
- 1];
129 tabs
[map
->n
- 1] = NULL
;
133 /* Replace the pair of basic maps i and j but the basic map bounded
134 * by the valid constraints in both basic maps.
136 static int fuse(struct isl_map
*map
, int i
, int j
, struct isl_tab
**tabs
,
137 int *ineq_i
, int *ineq_j
)
140 struct isl_basic_map
*fused
= NULL
;
141 struct isl_tab
*fused_tab
= NULL
;
142 unsigned total
= isl_basic_map_total_dim(map
->p
[i
]);
144 fused
= isl_basic_map_alloc_dim(isl_dim_copy(map
->p
[i
]->dim
),
146 map
->p
[i
]->n_eq
+ map
->p
[j
]->n_eq
,
147 map
->p
[i
]->n_ineq
+ map
->p
[j
]->n_ineq
);
151 for (k
= 0; k
< map
->p
[i
]->n_eq
; ++k
) {
152 int l
= isl_basic_map_alloc_equality(fused
);
153 isl_seq_cpy(fused
->eq
[l
], map
->p
[i
]->eq
[k
], 1 + total
);
156 for (k
= 0; k
< map
->p
[j
]->n_eq
; ++k
) {
157 int l
= isl_basic_map_alloc_equality(fused
);
158 isl_seq_cpy(fused
->eq
[l
], map
->p
[j
]->eq
[k
], 1 + total
);
161 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
162 if (ineq_i
[k
] != STATUS_VALID
)
164 l
= isl_basic_map_alloc_inequality(fused
);
165 isl_seq_cpy(fused
->ineq
[l
], map
->p
[i
]->ineq
[k
], 1 + total
);
168 for (k
= 0; k
< map
->p
[j
]->n_ineq
; ++k
) {
169 if (ineq_j
[k
] != STATUS_VALID
)
171 l
= isl_basic_map_alloc_inequality(fused
);
172 isl_seq_cpy(fused
->ineq
[l
], map
->p
[j
]->ineq
[k
], 1 + total
);
175 for (k
= 0; k
< map
->p
[i
]->n_div
; ++k
) {
176 int l
= isl_basic_map_alloc_div(fused
);
177 isl_seq_cpy(fused
->div
[l
], map
->p
[i
]->div
[k
], 1 + 1 + total
);
180 fused
= isl_basic_map_gauss(fused
, NULL
);
181 ISL_F_SET(fused
, ISL_BASIC_MAP_FINAL
);
182 if (ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_RATIONAL
) &&
183 ISL_F_ISSET(map
->p
[j
], ISL_BASIC_MAP_RATIONAL
))
184 ISL_F_SET(fused
, ISL_BASIC_MAP_RATIONAL
);
186 fused_tab
= isl_tab_from_basic_map(fused
);
187 if (isl_tab_detect_redundant(fused_tab
) < 0)
190 isl_basic_map_free(map
->p
[i
]);
192 isl_tab_free(tabs
[i
]);
198 isl_tab_free(fused_tab
);
199 isl_basic_map_free(fused
);
203 /* Given a pair of basic maps i and j such that all constraints are either
204 * "valid" or "cut", check if the facets corresponding to the "cut"
205 * constraints of i lie entirely within basic map j.
206 * If so, replace the pair by the basic map consisting of the valid
207 * constraints in both basic maps.
209 * To see that we are not introducing any extra points, call the
210 * two basic maps A and B and the resulting map U and let x
211 * be an element of U \setminus ( A \cup B ).
212 * Then there is a pair of cut constraints c_1 and c_2 in A and B such that x
213 * violates them. Let X be the intersection of U with the opposites
214 * of these constraints. Then x \in X.
215 * The facet corresponding to c_1 contains the corresponding facet of A.
216 * This facet is entirely contained in B, so c_2 is valid on the facet.
217 * However, since it is also (part of) a facet of X, -c_2 is also valid
218 * on the facet. This means c_2 is saturated on the facet, so c_1 and
219 * c_2 must be opposites of each other, but then x could not violate
222 static int check_facets(struct isl_map
*map
, int i
, int j
,
223 struct isl_tab
**tabs
, int *ineq_i
, int *ineq_j
)
226 struct isl_tab_undo
*snap
;
227 unsigned n_eq
= map
->p
[i
]->n_eq
;
229 snap
= isl_tab_snap(tabs
[i
]);
231 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
232 if (ineq_i
[k
] != STATUS_CUT
)
234 tabs
[i
] = isl_tab_select_facet(tabs
[i
], n_eq
+ k
);
235 for (l
= 0; l
< map
->p
[j
]->n_ineq
; ++l
) {
237 if (ineq_j
[l
] != STATUS_CUT
)
239 stat
= status_in(map
->p
[j
]->ineq
[l
], tabs
[i
]);
240 if (stat
!= STATUS_VALID
)
243 if (isl_tab_rollback(tabs
[i
], snap
) < 0)
245 if (l
< map
->p
[j
]->n_ineq
)
249 if (k
< map
->p
[i
]->n_ineq
)
252 return fuse(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
255 /* Both basic maps have at least one inequality with and adjacent
256 * (but opposite) inequality in the other basic map.
257 * Check that there are no cut constraints and that there is only
258 * a single pair of adjacent inequalities.
259 * If so, we can replace the pair by a single basic map described
260 * by all but the pair of adjacent inequalities.
261 * Any additional points introduced lie strictly between the two
262 * adjacent hyperplanes and can therefore be integral.
271 * The test for a single pair of adjancent inequalities is important
272 * for avoiding the combination of two basic maps like the following
282 static int check_adj_ineq(struct isl_map
*map
, int i
, int j
,
283 struct isl_tab
**tabs
, int *ineq_i
, int *ineq_j
)
287 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
) ||
288 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_CUT
))
291 else if (count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) == 1 &&
292 count(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
) == 1)
293 changed
= fuse(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
294 /* else ADJ INEQ TOO MANY */
299 /* Check if basic map "i" contains the basic map represented
300 * by the tableau "tab".
302 static int contains(struct isl_map
*map
, int i
, int *ineq_i
,
308 dim
= isl_basic_map_total_dim(map
->p
[i
]);
309 for (k
= 0; k
< map
->p
[i
]->n_eq
; ++k
) {
310 for (l
= 0; l
< 2; ++l
) {
312 isl_seq_neg(map
->p
[i
]->eq
[k
], map
->p
[i
]->eq
[k
], 1+dim
);
313 stat
= status_in(map
->p
[i
]->eq
[k
], tab
);
314 if (stat
!= STATUS_VALID
)
319 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
321 if (ineq_i
[k
] == STATUS_REDUNDANT
)
323 stat
= status_in(map
->p
[i
]->ineq
[k
], tab
);
324 if (stat
!= STATUS_VALID
)
330 /* At least one of the basic maps has an equality that is adjacent
331 * to inequality. Make sure that only one of the basic maps has
332 * such an equality and that the other basic map has exactly one
333 * inequality adjacent to an equality.
334 * We call the basic map that has the inequality "i" and the basic
335 * map that has the equality "j".
336 * If "i" has any "cut" inequality, then relaxing the inequality
337 * by one would not result in a basic map that contains the other
339 * Otherwise, we relax the constraint, compute the corresponding
340 * facet and check whether it is included in the other basic map.
341 * If so, we know that relaxing the constraint extend the basic
342 * map with exactly the other basic map (we already know that this
343 * other basic map is included in the extension, because there
344 * were no "cut" inequalities in "i") and we can replace the
345 * two basic maps by thie extension.
353 static int check_adj_eq(struct isl_map
*map
, int i
, int j
,
354 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
359 struct isl_tab_undo
*snap
, *snap2
;
360 unsigned n_eq
= map
->p
[i
]->n_eq
;
362 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) &&
363 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
))
364 /* ADJ EQ TOO MANY */
367 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
))
368 return check_adj_eq(map
, j
, i
, tabs
,
369 eq_j
, ineq_j
, eq_i
, ineq_i
);
371 /* j has an equality adjacent to an inequality in i */
373 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
))
376 if (count(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
) != 1 ||
377 count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) != 1 ||
378 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
) ||
379 any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
380 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
))
381 /* ADJ EQ TOO MANY */
384 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
)
385 if (ineq_i
[k
] == STATUS_ADJ_EQ
)
388 snap
= isl_tab_snap(tabs
[i
]);
389 tabs
[i
] = isl_tab_relax(tabs
[i
], n_eq
+ k
);
390 snap2
= isl_tab_snap(tabs
[i
]);
391 tabs
[i
] = isl_tab_select_facet(tabs
[i
], n_eq
+ k
);
392 super
= contains(map
, j
, ineq_j
, tabs
[i
]);
394 if (isl_tab_rollback(tabs
[i
], snap2
) < 0)
396 map
->p
[i
] = isl_basic_map_cow(map
->p
[i
]);
399 isl_int_add_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
400 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_FINAL
);
404 if (isl_tab_rollback(tabs
[i
], snap
) < 0)
410 /* Check if the union of the given pair of basic maps
411 * can be represented by a single basic map.
412 * If so, replace the pair by the single basic map and return 1.
413 * Otherwise, return 0;
415 * We first check the effect of each constraint of one basic map
416 * on the other basic map.
417 * The constraint may be
418 * redundant the constraint is redundant in its own
419 * basic map and should be ignore and removed
421 * valid all (integer) points of the other basic map
422 * satisfy the constraint
423 * separate no (integer) point of the other basic map
424 * satisfies the constraint
425 * cut some but not all points of the other basic map
426 * satisfy the constraint
427 * adj_eq the given constraint is adjacent (on the outside)
428 * to an equality of the other basic map
429 * adj_ineq the given constraint is adjacent (on the outside)
430 * to an inequality of the other basic map
432 * We consider four cases in which we can replace the pair by a single
433 * basic map. We ignore all "redundant" constraints.
435 * 1. all constraints of one basic map are valid
436 * => the other basic map is a subset and can be removed
438 * 2. all constraints of both basic maps are either "valid" or "cut"
439 * and the facets corresponding to the "cut" constraints
440 * of one of the basic maps lies entirely inside the other basic map
441 * => the pair can be replaced by a basic map consisting
442 * of the valid constraints in both basic maps
444 * 3. there is a single pair of adjacent inequalities
445 * (all other constraints are "valid")
446 * => the pair can be replaced by a basic map consisting
447 * of the valid constraints in both basic maps
449 * 4. there is a single adjacent pair of an inequality and an equality,
450 * the other constraints of the basic map containing the inequality are
451 * "valid". Moreover, if the inequality the basic map is relaxed
452 * and then turned into an equality, then resulting facet lies
453 * entirely inside the other basic map
454 * => the pair can be replaced by the basic map containing
455 * the inequality, with the inequality relaxed.
457 * Throughout the computation, we maintain a collection of tableaus
458 * corresponding to the basic maps. When the basic maps are dropped
459 * or combined, the tableaus are modified accordingly.
461 static int coalesce_pair(struct isl_map
*map
, int i
, int j
,
462 struct isl_tab
**tabs
)
470 eq_i
= eq_status_in(map
, i
, j
, tabs
);
471 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ERROR
))
473 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_SEPARATE
))
476 eq_j
= eq_status_in(map
, j
, i
, tabs
);
477 if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ERROR
))
479 if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_SEPARATE
))
482 ineq_i
= ineq_status_in(map
, i
, j
, tabs
);
483 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ERROR
))
485 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_SEPARATE
))
488 ineq_j
= ineq_status_in(map
, j
, i
, tabs
);
489 if (any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ERROR
))
491 if (any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_SEPARATE
))
494 if (all(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_VALID
) &&
495 all(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_VALID
)) {
498 } else if (all(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_VALID
) &&
499 all(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_VALID
)) {
502 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_CUT
) ||
503 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_CUT
)) {
505 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_EQ
) ||
506 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_EQ
)) {
508 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) ||
509 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
)) {
510 changed
= check_adj_eq(map
, i
, j
, tabs
,
511 eq_i
, ineq_i
, eq_j
, ineq_j
);
512 } else if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) ||
513 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
)) {
516 } else if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
517 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
)) {
518 changed
= check_adj_ineq(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
520 changed
= check_facets(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
536 static struct isl_map
*coalesce(struct isl_map
*map
, struct isl_tab
**tabs
)
540 for (i
= 0; i
< map
->n
- 1; ++i
)
541 for (j
= i
+ 1; j
< map
->n
; ++j
) {
543 changed
= coalesce_pair(map
, i
, j
, tabs
);
547 return coalesce(map
, tabs
);
555 /* For each pair of basic maps in the map, check if the union of the two
556 * can be represented by a single basic map.
557 * If so, replace the pair by the single basic map and start over.
559 struct isl_map
*isl_map_coalesce(struct isl_map
*map
)
563 struct isl_tab
**tabs
= NULL
;
571 map
= isl_map_align_divs(map
);
573 tabs
= isl_calloc_array(map
->ctx
, struct isl_tab
*, map
->n
);
578 for (i
= 0; i
< map
->n
; ++i
) {
579 tabs
[i
] = isl_tab_from_basic_map(map
->p
[i
]);
582 if (!ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_NO_IMPLICIT
))
583 tabs
[i
] = isl_tab_detect_implicit_equalities(tabs
[i
]);
584 if (!ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_NO_REDUNDANT
))
585 if (isl_tab_detect_redundant(tabs
[i
]) < 0)
588 for (i
= map
->n
- 1; i
>= 0; --i
)
592 map
= coalesce(map
, tabs
);
595 for (i
= 0; i
< map
->n
; ++i
) {
596 map
->p
[i
] = isl_basic_map_update_from_tab(map
->p
[i
],
598 map
->p
[i
] = isl_basic_map_finalize(map
->p
[i
]);
601 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_NO_IMPLICIT
);
602 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_NO_REDUNDANT
);
605 for (i
= 0; i
< n
; ++i
)
606 isl_tab_free(tabs
[i
]);
613 for (i
= 0; i
< n
; ++i
)
614 isl_tab_free(tabs
[i
]);
619 /* For each pair of basic sets in the set, check if the union of the two
620 * can be represented by a single basic set.
621 * If so, replace the pair by the single basic set and start over.
623 struct isl_set
*isl_set_coalesce(struct isl_set
*set
)
625 return (struct isl_set
*)isl_map_coalesce((struct isl_map
*)set
);