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 fused_tab
= isl_tab_detect_redundant(fused_tab
);
191 isl_basic_map_free(map
->p
[i
]);
193 isl_tab_free(tabs
[i
]);
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 isl_tab_rollback(tabs
[i
], snap
);
244 if (l
< map
->p
[j
]->n_ineq
)
248 if (k
< map
->p
[i
]->n_ineq
)
251 return fuse(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
254 /* Both basic maps have at least one inequality with and adjacent
255 * (but opposite) inequality in the other basic map.
256 * Check that there are no cut constraints and that there is only
257 * a single pair of adjacent inequalities.
258 * If so, we can replace the pair by a single basic map described
259 * by all but the pair of adjacent inequalities.
260 * Any additional points introduced lie strictly between the two
261 * adjacent hyperplanes and can therefore be integral.
270 * The test for a single pair of adjancent inequalities is important
271 * for avoiding the combination of two basic maps like the following
281 static int check_adj_ineq(struct isl_map
*map
, int i
, int j
,
282 struct isl_tab
**tabs
, int *ineq_i
, int *ineq_j
)
286 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
) ||
287 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_CUT
))
290 else if (count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) == 1 &&
291 count(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
) == 1)
292 changed
= fuse(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
293 /* else ADJ INEQ TOO MANY */
298 /* Check if basic map "i" contains the basic map represented
299 * by the tableau "tab".
301 static int contains(struct isl_map
*map
, int i
, int *ineq_i
,
307 dim
= isl_basic_map_total_dim(map
->p
[i
]);
308 for (k
= 0; k
< map
->p
[i
]->n_eq
; ++k
) {
309 for (l
= 0; l
< 2; ++l
) {
311 isl_seq_neg(map
->p
[i
]->eq
[k
], map
->p
[i
]->eq
[k
], 1+dim
);
312 stat
= status_in(map
->p
[i
]->eq
[k
], tab
);
313 if (stat
!= STATUS_VALID
)
318 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
320 if (ineq_i
[k
] == STATUS_REDUNDANT
)
322 stat
= status_in(map
->p
[i
]->ineq
[k
], tab
);
323 if (stat
!= STATUS_VALID
)
329 /* At least one of the basic maps has an equality that is adjacent
330 * to inequality. Make sure that only one of the basic maps has
331 * such an equality and that the other basic map has exactly one
332 * inequality adjacent to an equality.
333 * We call the basic map that has the inequality "i" and the basic
334 * map that has the equality "j".
335 * If "i" has any "cut" inequality, then relaxing the inequality
336 * by one would not result in a basic map that contains the other
338 * Otherwise, we relax the constraint, compute the corresponding
339 * facet and check whether it is included in the other basic map.
340 * If so, we know that relaxing the constraint extend the basic
341 * map with exactly the other basic map (we already know that this
342 * other basic map is included in the extension, because there
343 * were no "cut" inequalities in "i") and we can replace the
344 * two basic maps by thie extension.
352 static int check_adj_eq(struct isl_map
*map
, int i
, int j
,
353 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
358 struct isl_tab_undo
*snap
, *snap2
;
359 unsigned n_eq
= map
->p
[i
]->n_eq
;
361 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) &&
362 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
))
363 /* ADJ EQ TOO MANY */
366 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
))
367 return check_adj_eq(map
, j
, i
, tabs
,
368 eq_j
, ineq_j
, eq_i
, ineq_i
);
370 /* j has an equality adjacent to an inequality in i */
372 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
))
375 if (count(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
) != 1 ||
376 count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) != 1 ||
377 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
) ||
378 any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
379 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
))
380 /* ADJ EQ TOO MANY */
383 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
)
384 if (ineq_i
[k
] == STATUS_ADJ_EQ
)
387 snap
= isl_tab_snap(tabs
[i
]);
388 tabs
[i
] = isl_tab_relax(tabs
[i
], n_eq
+ k
);
389 snap2
= isl_tab_snap(tabs
[i
]);
390 tabs
[i
] = isl_tab_select_facet(tabs
[i
], n_eq
+ k
);
391 super
= contains(map
, j
, ineq_j
, tabs
[i
]);
393 isl_tab_rollback(tabs
[i
], snap2
);
394 map
->p
[i
] = isl_basic_map_cow(map
->p
[i
]);
397 isl_int_add_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
398 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_FINAL
);
402 isl_tab_rollback(tabs
[i
], snap
);
407 /* Check if the union of the given pair of basic maps
408 * can be represented by a single basic map.
409 * If so, replace the pair by the single basic map and return 1.
410 * Otherwise, return 0;
412 * We first check the effect of each constraint of one basic map
413 * on the other basic map.
414 * The constraint may be
415 * redundant the constraint is redundant in its own
416 * basic map and should be ignore and removed
418 * valid all (integer) points of the other basic map
419 * satisfy the constraint
420 * separate no (integer) point of the other basic map
421 * satisfies the constraint
422 * cut some but not all points of the other basic map
423 * satisfy the constraint
424 * adj_eq the given constraint is adjacent (on the outside)
425 * to an equality of the other basic map
426 * adj_ineq the given constraint is adjacent (on the outside)
427 * to an inequality of the other basic map
429 * We consider four cases in which we can replace the pair by a single
430 * basic map. We ignore all "redundant" constraints.
432 * 1. all constraints of one basic map are valid
433 * => the other basic map is a subset and can be removed
435 * 2. all constraints of both basic maps are either "valid" or "cut"
436 * and the facets corresponding to the "cut" constraints
437 * of one of the basic maps lies entirely inside the other basic map
438 * => the pair can be replaced by a basic map consisting
439 * of the valid constraints in both basic maps
441 * 3. there is a single pair of adjacent inequalities
442 * (all other constraints are "valid")
443 * => the pair can be replaced by a basic map consisting
444 * of the valid constraints in both basic maps
446 * 4. there is a single adjacent pair of an inequality and an equality,
447 * the other constraints of the basic map containing the inequality are
448 * "valid". Moreover, if the inequality the basic map is relaxed
449 * and then turned into an equality, then resulting facet lies
450 * entirely inside the other basic map
451 * => the pair can be replaced by the basic map containing
452 * the inequality, with the inequality relaxed.
454 * Throughout the computation, we maintain a collection of tableaus
455 * corresponding to the basic maps. When the basic maps are dropped
456 * or combined, the tableaus are modified accordingly.
458 static int coalesce_pair(struct isl_map
*map
, int i
, int j
,
459 struct isl_tab
**tabs
)
467 eq_i
= eq_status_in(map
, i
, j
, tabs
);
468 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ERROR
))
470 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_SEPARATE
))
473 eq_j
= eq_status_in(map
, j
, i
, tabs
);
474 if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ERROR
))
476 if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_SEPARATE
))
479 ineq_i
= ineq_status_in(map
, i
, j
, tabs
);
480 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ERROR
))
482 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_SEPARATE
))
485 ineq_j
= ineq_status_in(map
, j
, i
, tabs
);
486 if (any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ERROR
))
488 if (any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_SEPARATE
))
491 if (all(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_VALID
) &&
492 all(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_VALID
)) {
495 } else if (all(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_VALID
) &&
496 all(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_VALID
)) {
499 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_CUT
) ||
500 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_CUT
)) {
502 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_EQ
) ||
503 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_EQ
)) {
505 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) ||
506 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
)) {
507 changed
= check_adj_eq(map
, i
, j
, tabs
,
508 eq_i
, ineq_i
, eq_j
, ineq_j
);
509 } else if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) ||
510 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
)) {
513 } else if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
514 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
)) {
515 changed
= check_adj_ineq(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
517 changed
= check_facets(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
533 static struct isl_map
*coalesce(struct isl_map
*map
, struct isl_tab
**tabs
)
537 for (i
= 0; i
< map
->n
- 1; ++i
)
538 for (j
= i
+ 1; j
< map
->n
; ++j
) {
540 changed
= coalesce_pair(map
, i
, j
, tabs
);
544 return coalesce(map
, tabs
);
552 /* For each pair of basic maps in the map, check if the union of the two
553 * can be represented by a single basic map.
554 * If so, replace the pair by the single basic map and start over.
556 struct isl_map
*isl_map_coalesce(struct isl_map
*map
)
560 struct isl_tab
**tabs
= NULL
;
568 map
= isl_map_align_divs(map
);
570 tabs
= isl_calloc_array(map
->ctx
, struct isl_tab
*, map
->n
);
575 for (i
= 0; i
< map
->n
; ++i
) {
576 tabs
[i
] = isl_tab_from_basic_map(map
->p
[i
]);
579 if (!ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_NO_IMPLICIT
))
580 tabs
[i
] = isl_tab_detect_equalities(tabs
[i
]);
581 if (!ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_NO_REDUNDANT
))
582 tabs
[i
] = isl_tab_detect_redundant(tabs
[i
]);
584 for (i
= map
->n
- 1; i
>= 0; --i
)
588 map
= coalesce(map
, tabs
);
591 for (i
= 0; i
< map
->n
; ++i
) {
592 map
->p
[i
] = isl_basic_map_update_from_tab(map
->p
[i
],
594 map
->p
[i
] = isl_basic_map_finalize(map
->p
[i
]);
597 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_NO_IMPLICIT
);
598 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_NO_REDUNDANT
);
601 for (i
= 0; i
< n
; ++i
)
602 isl_tab_free(tabs
[i
]);
609 for (i
= 0; i
< n
; ++i
)
610 isl_tab_free(tabs
[i
]);
615 /* For each pair of basic sets in the set, check if the union of the two
616 * can be represented by a single basic set.
617 * If so, replace the pair by the single basic set and start over.
619 struct isl_set
*isl_set_coalesce(struct isl_set
*set
)
621 return (struct isl_set
*)isl_map_coalesce((struct isl_map
*)set
);