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(struct isl_ctx
*ctx
, isl_int
*ineq
, struct isl_tab
*tab
)
14 enum isl_ineq_type type
= isl_tab_ineq_type(ctx
, 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 set "i"
26 * with respect to basic set "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_set
*set
, int i
, int j
,
32 struct isl_tab
**tabs
)
35 int *eq
= isl_calloc_array(set
->ctx
, int, 2 * set
->p
[i
]->n_eq
);
38 dim
= isl_basic_set_total_dim(set
->p
[i
]);
39 for (k
= 0; k
< set
->p
[i
]->n_eq
; ++k
) {
40 for (l
= 0; l
< 2; ++l
) {
41 isl_seq_neg(set
->p
[i
]->eq
[k
], set
->p
[i
]->eq
[k
], 1+dim
);
42 eq
[2 * k
+ l
] = status_in(set
->ctx
, set
->p
[i
]->eq
[k
],
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 set "i"
59 * with respect to basic set "j".
61 static int *ineq_status_in(struct isl_set
*set
, int i
, int j
,
62 struct isl_tab
**tabs
)
65 unsigned n_eq
= set
->p
[i
]->n_eq
;
66 int *ineq
= isl_calloc_array(set
->ctx
, int, set
->p
[i
]->n_ineq
);
68 for (k
= 0; k
< set
->p
[i
]->n_ineq
; ++k
) {
69 if (isl_tab_is_redundant(set
->ctx
, tabs
[i
], n_eq
+ k
)) {
70 ineq
[k
] = STATUS_REDUNDANT
;
73 ineq
[k
] = status_in(set
->ctx
, set
->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_set
*set
, int i
, struct isl_tab
**tabs
)
122 isl_basic_set_free(set
->p
[i
]);
123 isl_tab_free(set
->ctx
, tabs
[i
]);
125 if (i
!= set
->n
- 1) {
126 set
->p
[i
] = set
->p
[set
->n
- 1];
127 tabs
[i
] = tabs
[set
->n
- 1];
129 tabs
[set
->n
- 1] = NULL
;
133 /* Replace the pair of basic sets i and j but the basic set bounded
134 * by the valid constraints in both basic sets.
136 static int fuse(struct isl_set
*set
, int i
, int j
, struct isl_tab
**tabs
,
137 int *ineq_i
, int *ineq_j
)
140 struct isl_basic_set
*fused
= NULL
;
141 struct isl_tab
*fused_tab
= NULL
;
142 unsigned total
= isl_basic_set_total_dim(set
->p
[i
]);
144 fused
= isl_basic_set_alloc_dim(isl_dim_copy(set
->p
[i
]->dim
),
146 set
->p
[i
]->n_eq
+ set
->p
[j
]->n_eq
,
147 set
->p
[i
]->n_ineq
+ set
->p
[j
]->n_ineq
);
151 for (k
= 0; k
< set
->p
[i
]->n_eq
; ++k
) {
152 int l
= isl_basic_set_alloc_equality(fused
);
153 isl_seq_cpy(fused
->eq
[l
], set
->p
[i
]->eq
[k
], 1 + total
);
156 for (k
= 0; k
< set
->p
[j
]->n_eq
; ++k
) {
157 int l
= isl_basic_set_alloc_equality(fused
);
158 isl_seq_cpy(fused
->eq
[l
], set
->p
[j
]->eq
[k
], 1 + total
);
161 for (k
= 0; k
< set
->p
[i
]->n_ineq
; ++k
) {
162 if (ineq_i
[k
] != STATUS_VALID
)
164 l
= isl_basic_set_alloc_inequality(fused
);
165 isl_seq_cpy(fused
->ineq
[l
], set
->p
[i
]->ineq
[k
], 1 + total
);
168 for (k
= 0; k
< set
->p
[j
]->n_ineq
; ++k
) {
169 if (ineq_j
[k
] != STATUS_VALID
)
171 l
= isl_basic_set_alloc_inequality(fused
);
172 isl_seq_cpy(fused
->ineq
[l
], set
->p
[j
]->ineq
[k
], 1 + total
);
175 for (k
= 0; k
< set
->p
[i
]->n_div
; ++k
) {
176 int l
= isl_basic_set_alloc_div(fused
);
177 isl_seq_cpy(fused
->div
[l
], set
->p
[i
]->div
[k
], 1 + 1 + total
);
180 fused
= isl_basic_set_gauss(fused
, NULL
);
181 ISL_F_SET(fused
, ISL_BASIC_SET_FINAL
);
183 fused_tab
= isl_tab_from_basic_set(fused
);
184 fused_tab
= isl_tab_detect_redundant(set
->ctx
, fused_tab
);
188 isl_basic_set_free(set
->p
[i
]);
190 isl_tab_free(set
->ctx
, tabs
[i
]);
196 isl_basic_set_free(fused
);
200 /* Given a pair of basic sets i and j such that all constraints are either
201 * "valid" or "cut", check if the facets corresponding to the "cut"
202 * constraints of i lie entirely within basic set j.
203 * If so, replace the pair by the basic set consisting of the valid
204 * constraints in both basic sets.
206 * To see that we are not introducing any extra points, call the
207 * two basic sets A and B and the resulting set U and let x
208 * be an element of U \setminus ( A \cup B ).
209 * Then there is a pair of cut constraints c_1 and c_2 in A and B such that x
210 * violates them. Let X be the intersection of U with the opposites
211 * of these constraints. Then x \in X.
212 * The facet corresponding to c_1 contains the corresponding facet of A.
213 * This facet is entirely contained in B, so c_2 is valid on the facet.
214 * However, since it is also (part of) a facet of X, -c_2 is also valid
215 * on the facet. This means c_2 is saturated on the facet, so c_1 and
216 * c_2 must be opposites of each other, but then x could not violate
219 static int check_facets(struct isl_set
*set
, int i
, int j
,
220 struct isl_tab
**tabs
, int *ineq_i
, int *ineq_j
)
223 struct isl_tab_undo
*snap
;
224 unsigned n_eq
= set
->p
[i
]->n_eq
;
226 snap
= isl_tab_snap(set
->ctx
, tabs
[i
]);
228 for (k
= 0; k
< set
->p
[i
]->n_ineq
; ++k
) {
229 if (ineq_i
[k
] != STATUS_CUT
)
231 tabs
[i
] = isl_tab_select_facet(set
->ctx
, tabs
[i
], n_eq
+ k
);
232 for (l
= 0; l
< set
->p
[j
]->n_ineq
; ++l
) {
234 if (ineq_j
[l
] != STATUS_CUT
)
236 stat
= status_in(set
->ctx
, set
->p
[j
]->ineq
[l
], tabs
[i
]);
237 if (stat
!= STATUS_VALID
)
240 isl_tab_rollback(set
->ctx
, tabs
[i
], snap
);
241 if (l
< set
->p
[j
]->n_ineq
)
245 if (k
< set
->p
[i
]->n_ineq
)
248 return fuse(set
, i
, j
, tabs
, ineq_i
, ineq_j
);
251 /* Both basic sets have at least one inequality with and adjacent
252 * (but opposite) inequality in the other basic set.
253 * Check that there are no cut constraints and that there is only
254 * a single pair of adjacent inequalities.
255 * If so, we can replace the pair by a single basic set described
256 * by all but the pair of adjacent inequalities.
257 * Any additional points introduced lie strictly between the two
258 * adjacent hyperplanes and can therefore be integral.
267 * The test for a single pair of adjancent inequalities is important
268 * for avoiding the combination of two basic sets like the following
278 static int check_adj_ineq(struct isl_set
*set
, int i
, int j
,
279 struct isl_tab
**tabs
, int *ineq_i
, int *ineq_j
)
283 if (any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_CUT
) ||
284 any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_CUT
))
287 else if (count(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) == 1 &&
288 count(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
) == 1)
289 changed
= fuse(set
, i
, j
, tabs
, ineq_i
, ineq_j
);
290 /* else ADJ INEQ TOO MANY */
295 /* Check if basic set "i" contains the basic set represented
296 * by the tableau "tab".
298 static int contains(struct isl_set
*set
, int i
, int *ineq_i
,
304 dim
= isl_basic_set_total_dim(set
->p
[i
]);
305 for (k
= 0; k
< set
->p
[i
]->n_eq
; ++k
) {
306 for (l
= 0; l
< 2; ++l
) {
308 isl_seq_neg(set
->p
[i
]->eq
[k
], set
->p
[i
]->eq
[k
], 1+dim
);
309 stat
= status_in(set
->ctx
, set
->p
[i
]->eq
[k
], tab
);
310 if (stat
!= STATUS_VALID
)
315 for (k
= 0; k
< set
->p
[i
]->n_ineq
; ++k
) {
317 if (ineq_i
[l
] == STATUS_REDUNDANT
)
319 stat
= status_in(set
->ctx
, set
->p
[i
]->ineq
[k
], tab
);
320 if (stat
!= STATUS_VALID
)
326 /* At least one of the basic sets has an equality that is adjacent
327 * to inequality. Make sure that only one of the basic sets has
328 * such an equality and that the other basic set has exactly one
329 * inequality adjacent to an equality.
330 * We call the basic set that has the inequality "i" and the basic
331 * set that has the equality "j".
332 * If "i" has any "cut" inequality, then relaxing the inequality
333 * by one would not result in a basic set that contains the other
335 * Otherwise, we relax the constraint, compute the corresponding
336 * facet and check whether it is included in the other basic set.
337 * If so, we know that relaxing the constraint extend the basic
338 * set with exactly the other basic set (we already know that this
339 * other basic set is included in the extension, because there
340 * were no "cut" inequalities in "i") and we can replace the
341 * two basic sets by thie extension.
349 static int check_adj_eq(struct isl_set
*set
, int i
, int j
,
350 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
355 struct isl_tab_undo
*snap
, *snap2
;
356 unsigned n_eq
= set
->p
[i
]->n_eq
;
358 if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) &&
359 any(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
))
360 /* ADJ EQ TOO MANY */
363 if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
))
364 return check_adj_eq(set
, j
, i
, tabs
,
365 eq_j
, ineq_j
, eq_i
, ineq_i
);
367 /* j has an equality adjacent to an inequality in i */
369 if (any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_CUT
))
372 if (count(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
) != 1 ||
373 count(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) != 1 ||
374 any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
) ||
375 any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
376 any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
))
377 /* ADJ EQ TOO MANY */
380 for (k
= 0; k
< set
->p
[i
]->n_ineq
; ++k
)
381 if (ineq_i
[k
] == STATUS_ADJ_EQ
)
384 snap
= isl_tab_snap(set
->ctx
, tabs
[i
]);
385 tabs
[i
] = isl_tab_relax(set
->ctx
, tabs
[i
], n_eq
+ k
);
386 snap2
= isl_tab_snap(set
->ctx
, tabs
[i
]);
387 tabs
[i
] = isl_tab_select_facet(set
->ctx
, tabs
[i
], n_eq
+ k
);
388 super
= contains(set
, j
, ineq_j
, tabs
[i
]);
390 isl_tab_rollback(set
->ctx
, tabs
[i
], snap2
);
391 set
->p
[i
] = isl_basic_set_cow(set
->p
[i
]);
394 isl_int_add_ui(set
->p
[i
]->ineq
[k
][0], set
->p
[i
]->ineq
[k
][0], 1);
395 ISL_F_SET(set
->p
[i
], ISL_BASIC_SET_FINAL
);
399 isl_tab_rollback(set
->ctx
, tabs
[i
], snap
);
404 /* Check if the union of the given pair of basic sets
405 * can be represented by a single basic set.
406 * If so, replace the pair by the single basic set and return 1.
407 * Otherwise, return 0;
409 * We first check the effect of each constraint of one basic set
410 * on the other basic set.
411 * The constraint may be
412 * redundant the constraint is redundant in its own
413 * basic set and should be ignore and removed
415 * valid all (integer) points of the other basic set
416 * satisfy the constraint
417 * separate no (integer) point of the other basic set
418 * satisfies the constraint
419 * cut some but not all points of the other basic set
420 * satisfy the constraint
421 * adj_eq the given constraint is adjacent (on the outside)
422 * to an equality of the other basic set
423 * adj_ineq the given constraint is adjacent (on the outside)
424 * to an inequality of the other basic set
426 * We consider four cases in which we can replace the pair by a single
427 * basic set. We ignore all "redundant" constraints.
429 * 1. all constraints of one basic set are valid
430 * => the other basic set is a subset and can be removed
432 * 2. all constraints of both basic sets are either "valid" or "cut"
433 * and the facets corresponding to the "cut" constraints
434 * of one of the basic sets lies entirely inside the other basic set
435 * => the pair can be replaced by a basic set consisting
436 * of the valid constraints in both basic sets
438 * 3. there is a single pair of adjacent inequalities
439 * (all other constraints are "valid")
440 * => the pair can be replaced by a basic set consisting
441 * of the valid constraints in both basic sets
443 * 4. there is a single adjacent pair of an inequality and an equality,
444 * the other constraints of the basic set containing the equality are
445 * "valid". Moreover, if the inequality the basic set is relaxed
446 * and then turned into an equality, then resulting facet lies
447 * entirely inside the other basic set
448 * => the pair can be replaced by the basic set containing
449 * the inequality, with the inequality relaxed.
451 * Throughout the computation, we maintain a collection of tableaus
452 * corresponding to the basic sets. When the basic sets are dropped
453 * or combined, the tableaus are modified accordingly.
455 static int coalesce_pair(struct isl_set
*set
, int i
, int j
,
456 struct isl_tab
**tabs
)
464 eq_i
= eq_status_in(set
, i
, j
, tabs
);
465 if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_ERROR
))
467 if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_SEPARATE
))
470 eq_j
= eq_status_in(set
, j
, i
, tabs
);
471 if (any(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_ERROR
))
473 if (any(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_SEPARATE
))
476 ineq_i
= ineq_status_in(set
, i
, j
, tabs
);
477 if (any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_ERROR
))
479 if (any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_SEPARATE
))
482 ineq_j
= ineq_status_in(set
, j
, i
, tabs
);
483 if (any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_ERROR
))
485 if (any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_SEPARATE
))
488 if (all(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_VALID
) &&
489 all(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_VALID
)) {
492 } else if (all(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_VALID
) &&
493 all(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_VALID
)) {
496 } else if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_CUT
) ||
497 any(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_CUT
)) {
499 } else if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_ADJ_EQ
) ||
500 any(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_ADJ_EQ
)) {
502 } else if (any(eq_i
, 2 * set
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) ||
503 any(eq_j
, 2 * set
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
)) {
504 changed
= check_adj_eq(set
, i
, j
, tabs
,
505 eq_i
, ineq_i
, eq_j
, ineq_j
);
506 } else if (any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) ||
507 any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
)) {
510 } else if (any(ineq_i
, set
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
511 any(ineq_j
, set
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
)) {
512 changed
= check_adj_ineq(set
, i
, j
, tabs
, ineq_i
, ineq_j
);
514 changed
= check_facets(set
, i
, j
, tabs
, ineq_i
, ineq_j
);
530 static struct isl_set
*coalesce(struct isl_set
*set
, struct isl_tab
**tabs
)
534 for (i
= 0; i
< set
->n
- 1; ++i
)
535 for (j
= i
+ 1; j
< set
->n
; ++j
) {
537 changed
= coalesce_pair(set
, i
, j
, tabs
);
541 return coalesce(set
, tabs
);
549 /* For each pair of basic sets in the set, check if the union of the two
550 * can be represented by a single basic set.
551 * If so, replace the pair by the single basic set and start over.
553 struct isl_set
*isl_set_coalesce(struct isl_set
*set
)
558 struct isl_tab
**tabs
= NULL
;
566 set
= isl_set_align_divs(set
);
568 tabs
= isl_calloc_array(set
->ctx
, struct isl_tab
*, set
->n
);
574 for (i
= 0; i
< set
->n
; ++i
) {
575 tabs
[i
] = isl_tab_from_basic_set(set
->p
[i
]);
578 if (!ISL_F_ISSET(set
->p
[i
], ISL_BASIC_SET_NO_IMPLICIT
))
579 tabs
[i
] = isl_tab_detect_equalities(set
->ctx
, tabs
[i
]);
580 if (!ISL_F_ISSET(set
->p
[i
], ISL_BASIC_SET_NO_REDUNDANT
))
581 tabs
[i
] = isl_tab_detect_redundant(set
->ctx
, tabs
[i
]);
583 for (i
= set
->n
- 1; i
>= 0; --i
)
587 set
= coalesce(set
, tabs
);
590 for (i
= 0; i
< set
->n
; ++i
) {
591 set
->p
[i
] = isl_basic_set_update_from_tab(set
->p
[i
],
595 ISL_F_SET(set
->p
[i
], ISL_BASIC_SET_NO_IMPLICIT
);
596 ISL_F_SET(set
->p
[i
], ISL_BASIC_SET_NO_REDUNDANT
);
599 for (i
= 0; i
< n
; ++i
)
600 isl_tab_free(ctx
, tabs
[i
]);
607 for (i
= 0; i
< n
; ++i
)
608 isl_tab_free(ctx
, tabs
[i
]);