2 * Copyright 2008-2009 Katholieke Universiteit Leuven
3 * Copyright 2010 INRIA Saclay
4 * Copyright 2012-2013 Ecole Normale Superieure
5 * Copyright 2014 INRIA Rocquencourt
7 * Use of this software is governed by the MIT license
9 * Written by Sven Verdoolaege, K.U.Leuven, Departement
10 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
11 * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
12 * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
13 * and Ecole Normale Superieure, 45 rue d’Ulm, 75230 Paris, France
14 * and Inria Paris - Rocquencourt, Domaine de Voluceau - Rocquencourt,
15 * B.P. 105 - 78153 Le Chesnay, France
18 #include "isl_map_private.h"
20 #include <isl/options.h>
22 #include <isl_mat_private.h>
23 #include <isl_local_space_private.h>
24 #include <isl_vec_private.h>
26 #define STATUS_ERROR -1
27 #define STATUS_REDUNDANT 1
28 #define STATUS_VALID 2
29 #define STATUS_SEPARATE 3
31 #define STATUS_ADJ_EQ 5
32 #define STATUS_ADJ_INEQ 6
34 static int status_in(isl_int
*ineq
, struct isl_tab
*tab
)
36 enum isl_ineq_type type
= isl_tab_ineq_type(tab
, ineq
);
39 case isl_ineq_error
: return STATUS_ERROR
;
40 case isl_ineq_redundant
: return STATUS_VALID
;
41 case isl_ineq_separate
: return STATUS_SEPARATE
;
42 case isl_ineq_cut
: return STATUS_CUT
;
43 case isl_ineq_adj_eq
: return STATUS_ADJ_EQ
;
44 case isl_ineq_adj_ineq
: return STATUS_ADJ_INEQ
;
48 /* Compute the position of the equalities of basic map "bmap_i"
49 * with respect to the basic map represented by "tab_j".
50 * The resulting array has twice as many entries as the number
51 * of equalities corresponding to the two inequalties to which
52 * each equality corresponds.
54 static int *eq_status_in(__isl_keep isl_basic_map
*bmap_i
,
55 struct isl_tab
*tab_j
)
58 int *eq
= isl_calloc_array(bmap_i
->ctx
, int, 2 * bmap_i
->n_eq
);
64 dim
= isl_basic_map_total_dim(bmap_i
);
65 for (k
= 0; k
< bmap_i
->n_eq
; ++k
) {
66 for (l
= 0; l
< 2; ++l
) {
67 isl_seq_neg(bmap_i
->eq
[k
], bmap_i
->eq
[k
], 1+dim
);
68 eq
[2 * k
+ l
] = status_in(bmap_i
->eq
[k
], tab_j
);
69 if (eq
[2 * k
+ l
] == STATUS_ERROR
)
72 if (eq
[2 * k
] == STATUS_SEPARATE
||
73 eq
[2 * k
+ 1] == STATUS_SEPARATE
)
83 /* Compute the position of the inequalities of basic map "bmap_i"
84 * (also represented by "tab_i", if not NULL) with respect to the basic map
85 * represented by "tab_j".
87 static int *ineq_status_in(__isl_keep isl_basic_map
*bmap_i
,
88 struct isl_tab
*tab_i
, struct isl_tab
*tab_j
)
91 unsigned n_eq
= bmap_i
->n_eq
;
92 int *ineq
= isl_calloc_array(bmap_i
->ctx
, int, bmap_i
->n_ineq
);
97 for (k
= 0; k
< bmap_i
->n_ineq
; ++k
) {
98 if (tab_i
&& isl_tab_is_redundant(tab_i
, n_eq
+ k
)) {
99 ineq
[k
] = STATUS_REDUNDANT
;
102 ineq
[k
] = status_in(bmap_i
->ineq
[k
], tab_j
);
103 if (ineq
[k
] == STATUS_ERROR
)
105 if (ineq
[k
] == STATUS_SEPARATE
)
115 static int any(int *con
, unsigned len
, int status
)
119 for (i
= 0; i
< len
; ++i
)
120 if (con
[i
] == status
)
125 static int count(int *con
, unsigned len
, int status
)
130 for (i
= 0; i
< len
; ++i
)
131 if (con
[i
] == status
)
136 static int all(int *con
, unsigned len
, int status
)
140 for (i
= 0; i
< len
; ++i
) {
141 if (con
[i
] == STATUS_REDUNDANT
)
143 if (con
[i
] != status
)
149 static void drop(struct isl_map
*map
, int i
, struct isl_tab
**tabs
)
151 isl_basic_map_free(map
->p
[i
]);
152 isl_tab_free(tabs
[i
]);
154 if (i
!= map
->n
- 1) {
155 map
->p
[i
] = map
->p
[map
->n
- 1];
156 tabs
[i
] = tabs
[map
->n
- 1];
158 tabs
[map
->n
- 1] = NULL
;
162 /* Exchange the basic maps in positions i and j, along with their tabs.
164 static void exchange(__isl_keep isl_map
*map
, int i
, int j
,
165 struct isl_tab
**tabs
)
171 map
->p
[i
] = map
->p
[j
];
178 /* Replace the pair of basic maps i and j by the basic map bounded
179 * by the valid constraints in both basic maps and the constraints
180 * in extra (if not NULL).
181 * Place the fused basic map in the position that is the smallest of i and j.
183 * If "detect_equalities" is set, then look for equalities encoded
184 * as pairs of inequalities.
186 static int fuse(struct isl_map
*map
, int i
, int j
,
187 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
,
188 __isl_keep isl_mat
*extra
, int detect_equalities
)
191 struct isl_basic_map
*fused
= NULL
;
192 struct isl_tab
*fused_tab
= NULL
;
193 unsigned total
= isl_basic_map_total_dim(map
->p
[i
]);
194 unsigned extra_rows
= extra
? extra
->n_row
: 0;
197 return fuse(map
, j
, i
, tabs
, eq_j
, ineq_j
, eq_i
, ineq_i
,
198 extra
, detect_equalities
);
200 fused
= isl_basic_map_alloc_space(isl_space_copy(map
->p
[i
]->dim
),
202 map
->p
[i
]->n_eq
+ map
->p
[j
]->n_eq
,
203 map
->p
[i
]->n_ineq
+ map
->p
[j
]->n_ineq
+ extra_rows
);
207 for (k
= 0; k
< map
->p
[i
]->n_eq
; ++k
) {
208 if (eq_i
&& (eq_i
[2 * k
] != STATUS_VALID
||
209 eq_i
[2 * k
+ 1] != STATUS_VALID
))
211 l
= isl_basic_map_alloc_equality(fused
);
214 isl_seq_cpy(fused
->eq
[l
], map
->p
[i
]->eq
[k
], 1 + total
);
217 for (k
= 0; k
< map
->p
[j
]->n_eq
; ++k
) {
218 if (eq_j
&& (eq_j
[2 * k
] != STATUS_VALID
||
219 eq_j
[2 * k
+ 1] != STATUS_VALID
))
221 l
= isl_basic_map_alloc_equality(fused
);
224 isl_seq_cpy(fused
->eq
[l
], map
->p
[j
]->eq
[k
], 1 + total
);
227 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
228 if (ineq_i
[k
] != STATUS_VALID
)
230 l
= isl_basic_map_alloc_inequality(fused
);
233 isl_seq_cpy(fused
->ineq
[l
], map
->p
[i
]->ineq
[k
], 1 + total
);
236 for (k
= 0; k
< map
->p
[j
]->n_ineq
; ++k
) {
237 if (ineq_j
[k
] != STATUS_VALID
)
239 l
= isl_basic_map_alloc_inequality(fused
);
242 isl_seq_cpy(fused
->ineq
[l
], map
->p
[j
]->ineq
[k
], 1 + total
);
245 for (k
= 0; k
< map
->p
[i
]->n_div
; ++k
) {
246 int l
= isl_basic_map_alloc_div(fused
);
249 isl_seq_cpy(fused
->div
[l
], map
->p
[i
]->div
[k
], 1 + 1 + total
);
252 for (k
= 0; k
< extra_rows
; ++k
) {
253 l
= isl_basic_map_alloc_inequality(fused
);
256 isl_seq_cpy(fused
->ineq
[l
], extra
->row
[k
], 1 + total
);
259 if (detect_equalities
)
260 fused
= isl_basic_map_detect_inequality_pairs(fused
, NULL
);
261 fused
= isl_basic_map_gauss(fused
, NULL
);
262 ISL_F_SET(fused
, ISL_BASIC_MAP_FINAL
);
263 if (ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_RATIONAL
) &&
264 ISL_F_ISSET(map
->p
[j
], ISL_BASIC_MAP_RATIONAL
))
265 ISL_F_SET(fused
, ISL_BASIC_MAP_RATIONAL
);
267 fused_tab
= isl_tab_from_basic_map(fused
, 0);
268 if (isl_tab_detect_redundant(fused_tab
) < 0)
271 isl_basic_map_free(map
->p
[i
]);
273 isl_tab_free(tabs
[i
]);
279 isl_tab_free(fused_tab
);
280 isl_basic_map_free(fused
);
284 /* Given a pair of basic maps i and j such that all constraints are either
285 * "valid" or "cut", check if the facets corresponding to the "cut"
286 * constraints of i lie entirely within basic map j.
287 * If so, replace the pair by the basic map consisting of the valid
288 * constraints in both basic maps.
289 * Checking whether the facet lies entirely within basic map j
290 * is performed by checking whether the constraints of basic map j
291 * are valid for the facet. These tests are performed on a rational
292 * tableau to avoid the theoretical possibility that a constraint
293 * that was considered to be a cut constraint for the entire basic map i
294 * happens to be considered to be a valid constraint for the facet,
295 * even though it cuts off the same rational points.
297 * To see that we are not introducing any extra points, call the
298 * two basic maps A and B and the resulting map U and let x
299 * be an element of U \setminus ( A \cup B ).
300 * A line connecting x with an element of A \cup B meets a facet F
301 * of either A or B. Assume it is a facet of B and let c_1 be
302 * the corresponding facet constraint. We have c_1(x) < 0 and
303 * so c_1 is a cut constraint. This implies that there is some
304 * (possibly rational) point x' satisfying the constraints of A
305 * and the opposite of c_1 as otherwise c_1 would have been marked
306 * valid for A. The line connecting x and x' meets a facet of A
307 * in a (possibly rational) point that also violates c_1, but this
308 * is impossible since all cut constraints of B are valid for all
310 * In case F is a facet of A rather than B, then we can apply the
311 * above reasoning to find a facet of B separating x from A \cup B first.
313 static int check_facets(struct isl_map
*map
, int i
, int j
,
314 struct isl_tab
**tabs
, int *ineq_i
, int *ineq_j
)
317 struct isl_tab_undo
*snap
, *snap2
;
318 unsigned n_eq
= map
->p
[i
]->n_eq
;
320 snap
= isl_tab_snap(tabs
[i
]);
321 if (isl_tab_mark_rational(tabs
[i
]) < 0)
323 snap2
= isl_tab_snap(tabs
[i
]);
325 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
326 if (ineq_i
[k
] != STATUS_CUT
)
328 if (isl_tab_select_facet(tabs
[i
], n_eq
+ k
) < 0)
330 for (l
= 0; l
< map
->p
[j
]->n_ineq
; ++l
) {
332 if (ineq_j
[l
] != STATUS_CUT
)
334 stat
= status_in(map
->p
[j
]->ineq
[l
], tabs
[i
]);
335 if (stat
!= STATUS_VALID
)
338 if (isl_tab_rollback(tabs
[i
], snap2
) < 0)
340 if (l
< map
->p
[j
]->n_ineq
)
344 if (k
< map
->p
[i
]->n_ineq
) {
345 if (isl_tab_rollback(tabs
[i
], snap
) < 0)
349 return fuse(map
, i
, j
, tabs
, NULL
, ineq_i
, NULL
, ineq_j
, NULL
, 0);
352 /* Check if basic map "i" contains the basic map represented
353 * by the tableau "tab".
355 static int contains(struct isl_map
*map
, int i
, int *ineq_i
,
361 dim
= isl_basic_map_total_dim(map
->p
[i
]);
362 for (k
= 0; k
< map
->p
[i
]->n_eq
; ++k
) {
363 for (l
= 0; l
< 2; ++l
) {
365 isl_seq_neg(map
->p
[i
]->eq
[k
], map
->p
[i
]->eq
[k
], 1+dim
);
366 stat
= status_in(map
->p
[i
]->eq
[k
], tab
);
367 if (stat
!= STATUS_VALID
)
372 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
) {
374 if (ineq_i
[k
] == STATUS_REDUNDANT
)
376 stat
= status_in(map
->p
[i
]->ineq
[k
], tab
);
377 if (stat
!= STATUS_VALID
)
383 /* Basic map "i" has an inequality (say "k") that is adjacent
384 * to some inequality of basic map "j". All the other inequalities
386 * Check if basic map "j" forms an extension of basic map "i".
388 * Note that this function is only called if some of the equalities or
389 * inequalities of basic map "j" do cut basic map "i". The function is
390 * correct even if there are no such cut constraints, but in that case
391 * the additional checks performed by this function are overkill.
393 * In particular, we replace constraint k, say f >= 0, by constraint
394 * f <= -1, add the inequalities of "j" that are valid for "i"
395 * and check if the result is a subset of basic map "j".
396 * If so, then we know that this result is exactly equal to basic map "j"
397 * since all its constraints are valid for basic map "j".
398 * By combining the valid constraints of "i" (all equalities and all
399 * inequalities except "k") and the valid constraints of "j" we therefore
400 * obtain a basic map that is equal to their union.
401 * In this case, there is no need to perform a rollback of the tableau
402 * since it is going to be destroyed in fuse().
408 * |_______| _ |_________\
420 static int is_adj_ineq_extension(__isl_keep isl_map
*map
, int i
, int j
,
421 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
424 struct isl_tab_undo
*snap
;
425 unsigned n_eq
= map
->p
[i
]->n_eq
;
426 unsigned total
= isl_basic_map_total_dim(map
->p
[i
]);
429 if (isl_tab_extend_cons(tabs
[i
], 1 + map
->p
[j
]->n_ineq
) < 0)
432 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
)
433 if (ineq_i
[k
] == STATUS_ADJ_INEQ
)
435 if (k
>= map
->p
[i
]->n_ineq
)
436 isl_die(isl_map_get_ctx(map
), isl_error_internal
,
437 "ineq_i should have exactly one STATUS_ADJ_INEQ",
440 snap
= isl_tab_snap(tabs
[i
]);
442 if (isl_tab_unrestrict(tabs
[i
], n_eq
+ k
) < 0)
445 isl_seq_neg(map
->p
[i
]->ineq
[k
], map
->p
[i
]->ineq
[k
], 1 + total
);
446 isl_int_sub_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
447 r
= isl_tab_add_ineq(tabs
[i
], map
->p
[i
]->ineq
[k
]);
448 isl_seq_neg(map
->p
[i
]->ineq
[k
], map
->p
[i
]->ineq
[k
], 1 + total
);
449 isl_int_sub_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
453 for (k
= 0; k
< map
->p
[j
]->n_ineq
; ++k
) {
454 if (ineq_j
[k
] != STATUS_VALID
)
456 if (isl_tab_add_ineq(tabs
[i
], map
->p
[j
]->ineq
[k
]) < 0)
460 if (contains(map
, j
, ineq_j
, tabs
[i
]))
461 return fuse(map
, i
, j
, tabs
, eq_i
, ineq_i
, eq_j
, ineq_j
,
464 if (isl_tab_rollback(tabs
[i
], snap
) < 0)
471 /* Both basic maps have at least one inequality with and adjacent
472 * (but opposite) inequality in the other basic map.
473 * Check that there are no cut constraints and that there is only
474 * a single pair of adjacent inequalities.
475 * If so, we can replace the pair by a single basic map described
476 * by all but the pair of adjacent inequalities.
477 * Any additional points introduced lie strictly between the two
478 * adjacent hyperplanes and can therefore be integral.
487 * The test for a single pair of adjancent inequalities is important
488 * for avoiding the combination of two basic maps like the following
498 * If there are some cut constraints on one side, then we may
499 * still be able to fuse the two basic maps, but we need to perform
500 * some additional checks in is_adj_ineq_extension.
502 static int check_adj_ineq(struct isl_map
*map
, int i
, int j
,
503 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
505 int count_i
, count_j
;
508 count_i
= count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
);
509 count_j
= count(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
);
511 if (count_i
!= 1 && count_j
!= 1)
514 cut_i
= any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_CUT
) ||
515 any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
);
516 cut_j
= any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_CUT
) ||
517 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_CUT
);
519 if (!cut_i
&& !cut_j
&& count_i
== 1 && count_j
== 1)
520 return fuse(map
, i
, j
, tabs
, NULL
, ineq_i
, NULL
, ineq_j
,
523 if (count_i
== 1 && !cut_i
)
524 return is_adj_ineq_extension(map
, i
, j
, tabs
,
525 eq_i
, ineq_i
, eq_j
, ineq_j
);
527 if (count_j
== 1 && !cut_j
)
528 return is_adj_ineq_extension(map
, j
, i
, tabs
,
529 eq_j
, ineq_j
, eq_i
, ineq_i
);
534 /* Basic map "i" has an inequality "k" that is adjacent to some equality
535 * of basic map "j". All the other inequalities are valid for "j".
536 * Check if basic map "j" forms an extension of basic map "i".
538 * In particular, we relax constraint "k", compute the corresponding
539 * facet and check whether it is included in the other basic map.
540 * If so, we know that relaxing the constraint extends the basic
541 * map with exactly the other basic map (we already know that this
542 * other basic map is included in the extension, because there
543 * were no "cut" inequalities in "i") and we can replace the
544 * two basic maps by this extension.
545 * Place this extension in the position that is the smallest of i and j.
553 static int is_adj_eq_extension(struct isl_map
*map
, int i
, int j
, int k
,
554 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
558 struct isl_tab_undo
*snap
, *snap2
;
559 unsigned n_eq
= map
->p
[i
]->n_eq
;
561 if (isl_tab_is_equality(tabs
[i
], n_eq
+ k
))
564 snap
= isl_tab_snap(tabs
[i
]);
565 if (isl_tab_relax(tabs
[i
], n_eq
+ k
) < 0)
567 snap2
= isl_tab_snap(tabs
[i
]);
568 if (isl_tab_select_facet(tabs
[i
], n_eq
+ k
) < 0)
570 super
= contains(map
, j
, ineq_j
, tabs
[i
]);
572 if (isl_tab_rollback(tabs
[i
], snap2
) < 0)
574 map
->p
[i
] = isl_basic_map_cow(map
->p
[i
]);
577 isl_int_add_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
578 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_FINAL
);
580 exchange(map
, i
, j
, tabs
);
587 if (isl_tab_rollback(tabs
[i
], snap
) < 0)
593 /* Data structure that keeps track of the wrapping constraints
594 * and of information to bound the coefficients of those constraints.
596 * bound is set if we want to apply a bound on the coefficients
597 * mat contains the wrapping constraints
598 * max is the bound on the coefficients (if bound is set)
606 /* Update wraps->max to be greater than or equal to the coefficients
607 * in the equalities and inequalities of bmap that can be removed if we end up
610 static void wraps_update_max(struct isl_wraps
*wraps
,
611 __isl_keep isl_basic_map
*bmap
, int *eq
, int *ineq
)
615 unsigned total
= isl_basic_map_total_dim(bmap
);
619 for (k
= 0; k
< bmap
->n_eq
; ++k
) {
620 if (eq
[2 * k
] == STATUS_VALID
&&
621 eq
[2 * k
+ 1] == STATUS_VALID
)
623 isl_seq_abs_max(bmap
->eq
[k
] + 1, total
, &max_k
);
624 if (isl_int_abs_gt(max_k
, wraps
->max
))
625 isl_int_set(wraps
->max
, max_k
);
628 for (k
= 0; k
< bmap
->n_ineq
; ++k
) {
629 if (ineq
[k
] == STATUS_VALID
|| ineq
[k
] == STATUS_REDUNDANT
)
631 isl_seq_abs_max(bmap
->ineq
[k
] + 1, total
, &max_k
);
632 if (isl_int_abs_gt(max_k
, wraps
->max
))
633 isl_int_set(wraps
->max
, max_k
);
636 isl_int_clear(max_k
);
639 /* Initialize the isl_wraps data structure.
640 * If we want to bound the coefficients of the wrapping constraints,
641 * we set wraps->max to the largest coefficient
642 * in the equalities and inequalities that can be removed if we end up
645 static void wraps_init(struct isl_wraps
*wraps
, __isl_take isl_mat
*mat
,
646 __isl_keep isl_map
*map
, int i
, int j
,
647 int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
655 ctx
= isl_mat_get_ctx(mat
);
656 wraps
->bound
= isl_options_get_coalesce_bounded_wrapping(ctx
);
659 isl_int_init(wraps
->max
);
660 isl_int_set_si(wraps
->max
, 0);
661 wraps_update_max(wraps
, map
->p
[i
], eq_i
, ineq_i
);
662 wraps_update_max(wraps
, map
->p
[j
], eq_j
, ineq_j
);
665 /* Free the contents of the isl_wraps data structure.
667 static void wraps_free(struct isl_wraps
*wraps
)
669 isl_mat_free(wraps
->mat
);
671 isl_int_clear(wraps
->max
);
674 /* Is the wrapping constraint in row "row" allowed?
676 * If wraps->bound is set, we check that none of the coefficients
677 * is greater than wraps->max.
679 static int allow_wrap(struct isl_wraps
*wraps
, int row
)
686 for (i
= 1; i
< wraps
->mat
->n_col
; ++i
)
687 if (isl_int_abs_gt(wraps
->mat
->row
[row
][i
], wraps
->max
))
693 /* For each non-redundant constraint in "bmap" (as determined by "tab"),
694 * wrap the constraint around "bound" such that it includes the whole
695 * set "set" and append the resulting constraint to "wraps".
696 * "wraps" is assumed to have been pre-allocated to the appropriate size.
697 * wraps->n_row is the number of actual wrapped constraints that have
699 * If any of the wrapping problems results in a constraint that is
700 * identical to "bound", then this means that "set" is unbounded in such
701 * way that no wrapping is possible. If this happens then wraps->n_row
703 * Similarly, if we want to bound the coefficients of the wrapping
704 * constraints and a newly added wrapping constraint does not
705 * satisfy the bound, then wraps->n_row is also reset to zero.
707 static int add_wraps(struct isl_wraps
*wraps
, __isl_keep isl_basic_map
*bmap
,
708 struct isl_tab
*tab
, isl_int
*bound
, __isl_keep isl_set
*set
)
712 unsigned total
= isl_basic_map_total_dim(bmap
);
714 w
= wraps
->mat
->n_row
;
716 for (l
= 0; l
< bmap
->n_ineq
; ++l
) {
717 if (isl_seq_is_neg(bound
, bmap
->ineq
[l
], 1 + total
))
719 if (isl_seq_eq(bound
, bmap
->ineq
[l
], 1 + total
))
721 if (isl_tab_is_redundant(tab
, bmap
->n_eq
+ l
))
724 isl_seq_cpy(wraps
->mat
->row
[w
], bound
, 1 + total
);
725 if (!isl_set_wrap_facet(set
, wraps
->mat
->row
[w
], bmap
->ineq
[l
]))
727 if (isl_seq_eq(wraps
->mat
->row
[w
], bound
, 1 + total
))
729 if (!allow_wrap(wraps
, w
))
733 for (l
= 0; l
< bmap
->n_eq
; ++l
) {
734 if (isl_seq_is_neg(bound
, bmap
->eq
[l
], 1 + total
))
736 if (isl_seq_eq(bound
, bmap
->eq
[l
], 1 + total
))
739 isl_seq_cpy(wraps
->mat
->row
[w
], bound
, 1 + total
);
740 isl_seq_neg(wraps
->mat
->row
[w
+ 1], bmap
->eq
[l
], 1 + total
);
741 if (!isl_set_wrap_facet(set
, wraps
->mat
->row
[w
],
742 wraps
->mat
->row
[w
+ 1]))
744 if (isl_seq_eq(wraps
->mat
->row
[w
], bound
, 1 + total
))
746 if (!allow_wrap(wraps
, w
))
750 isl_seq_cpy(wraps
->mat
->row
[w
], bound
, 1 + total
);
751 if (!isl_set_wrap_facet(set
, wraps
->mat
->row
[w
], bmap
->eq
[l
]))
753 if (isl_seq_eq(wraps
->mat
->row
[w
], bound
, 1 + total
))
755 if (!allow_wrap(wraps
, w
))
760 wraps
->mat
->n_row
= w
;
763 wraps
->mat
->n_row
= 0;
767 /* Check if the constraints in "wraps" from "first" until the last
768 * are all valid for the basic set represented by "tab".
769 * If not, wraps->n_row is set to zero.
771 static int check_wraps(__isl_keep isl_mat
*wraps
, int first
,
776 for (i
= first
; i
< wraps
->n_row
; ++i
) {
777 enum isl_ineq_type type
;
778 type
= isl_tab_ineq_type(tab
, wraps
->row
[i
]);
779 if (type
== isl_ineq_error
)
781 if (type
== isl_ineq_redundant
)
790 /* Return a set that corresponds to the non-redundant constraints
791 * (as recorded in tab) of bmap.
793 * It's important to remove the redundant constraints as some
794 * of the other constraints may have been modified after the
795 * constraints were marked redundant.
796 * In particular, a constraint may have been relaxed.
797 * Redundant constraints are ignored when a constraint is relaxed
798 * and should therefore continue to be ignored ever after.
799 * Otherwise, the relaxation might be thwarted by some of
802 * Update the underlying set to ensure that the dimension doesn't change.
803 * Otherwise the integer divisions could get dropped if the tab
804 * turns out to be empty.
806 static __isl_give isl_set
*set_from_updated_bmap(__isl_keep isl_basic_map
*bmap
,
811 bmap
= isl_basic_map_copy(bmap
);
812 bset
= isl_basic_map_underlying_set(bmap
);
813 bset
= isl_basic_set_cow(bset
);
814 bset
= isl_basic_set_update_from_tab(bset
, tab
);
815 return isl_set_from_basic_set(bset
);
818 /* Given a basic set i with a constraint k that is adjacent to
819 * basic set j, check if we can wrap
820 * both the facet corresponding to k and basic map j
821 * around their ridges to include the other set.
822 * If so, replace the pair of basic sets by their union.
824 * All constraints of i (except k) are assumed to be valid for j.
825 * This means that there is no real need to wrap the ridges of
826 * the faces of basic map i around basic map j but since we do,
827 * we have to check that the resulting wrapping constraints are valid for i.
836 static int can_wrap_in_facet(struct isl_map
*map
, int i
, int j
, int k
,
837 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
840 struct isl_wraps wraps
;
842 struct isl_set
*set_i
= NULL
;
843 struct isl_set
*set_j
= NULL
;
844 struct isl_vec
*bound
= NULL
;
845 unsigned total
= isl_basic_map_total_dim(map
->p
[i
]);
846 struct isl_tab_undo
*snap
;
849 set_i
= set_from_updated_bmap(map
->p
[i
], tabs
[i
]);
850 set_j
= set_from_updated_bmap(map
->p
[j
], tabs
[j
]);
851 mat
= isl_mat_alloc(map
->ctx
, 2 * (map
->p
[i
]->n_eq
+ map
->p
[j
]->n_eq
) +
852 map
->p
[i
]->n_ineq
+ map
->p
[j
]->n_ineq
,
854 wraps_init(&wraps
, mat
, map
, i
, j
, eq_i
, ineq_i
, eq_j
, ineq_j
);
855 bound
= isl_vec_alloc(map
->ctx
, 1 + total
);
856 if (!set_i
|| !set_j
|| !wraps
.mat
|| !bound
)
859 isl_seq_cpy(bound
->el
, map
->p
[i
]->ineq
[k
], 1 + total
);
860 isl_int_add_ui(bound
->el
[0], bound
->el
[0], 1);
862 isl_seq_cpy(wraps
.mat
->row
[0], bound
->el
, 1 + total
);
863 wraps
.mat
->n_row
= 1;
865 if (add_wraps(&wraps
, map
->p
[j
], tabs
[j
], bound
->el
, set_i
) < 0)
867 if (!wraps
.mat
->n_row
)
870 snap
= isl_tab_snap(tabs
[i
]);
872 if (isl_tab_select_facet(tabs
[i
], map
->p
[i
]->n_eq
+ k
) < 0)
874 if (isl_tab_detect_redundant(tabs
[i
]) < 0)
877 isl_seq_neg(bound
->el
, map
->p
[i
]->ineq
[k
], 1 + total
);
879 n
= wraps
.mat
->n_row
;
880 if (add_wraps(&wraps
, map
->p
[i
], tabs
[i
], bound
->el
, set_j
) < 0)
883 if (isl_tab_rollback(tabs
[i
], snap
) < 0)
885 if (check_wraps(wraps
.mat
, n
, tabs
[i
]) < 0)
887 if (!wraps
.mat
->n_row
)
890 changed
= fuse(map
, i
, j
, tabs
, eq_i
, ineq_i
, eq_j
, ineq_j
,
910 /* Given a pair of basic maps i and j such that j sticks out
911 * of i at n cut constraints, each time by at most one,
912 * try to compute wrapping constraints and replace the two
913 * basic maps by a single basic map.
914 * The other constraints of i are assumed to be valid for j.
916 * For each cut constraint t(x) >= 0 of i, we add the relaxed version
917 * t(x) + 1 >= 0, along with wrapping constraints for all constraints
918 * of basic map j that bound the part of basic map j that sticks out
919 * of the cut constraint.
920 * In particular, we first intersect basic map j with t(x) + 1 = 0.
921 * If the result is empty, then t(x) >= 0 was actually a valid constraint
922 * (with respect to the integer points), so we add t(x) >= 0 instead.
923 * Otherwise, we wrap the constraints of basic map j that are not
924 * redundant in this intersection over the union of the two basic maps.
926 * If any wrapping fails, i.e., if we cannot wrap to touch
927 * the union, then we give up.
928 * Otherwise, the pair of basic maps is replaced by their union.
930 static int wrap_in_facets(struct isl_map
*map
, int i
, int j
,
931 int *cuts
, int n
, struct isl_tab
**tabs
,
932 int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
935 struct isl_wraps wraps
;
938 unsigned total
= isl_basic_map_total_dim(map
->p
[i
]);
941 struct isl_tab_undo
*snap
;
943 if (isl_tab_extend_cons(tabs
[j
], 1) < 0)
946 max_wrap
= 1 + 2 * map
->p
[j
]->n_eq
+ map
->p
[j
]->n_ineq
;
949 set
= isl_set_union(set_from_updated_bmap(map
->p
[i
], tabs
[i
]),
950 set_from_updated_bmap(map
->p
[j
], tabs
[j
]));
951 mat
= isl_mat_alloc(map
->ctx
, max_wrap
, 1 + total
);
952 wraps_init(&wraps
, mat
, map
, i
, j
, eq_i
, ineq_i
, eq_j
, ineq_j
);
953 if (!set
|| !wraps
.mat
)
956 snap
= isl_tab_snap(tabs
[j
]);
958 wraps
.mat
->n_row
= 0;
960 for (k
= 0; k
< n
; ++k
) {
961 w
= wraps
.mat
->n_row
++;
962 isl_seq_cpy(wraps
.mat
->row
[w
],
963 map
->p
[i
]->ineq
[cuts
[k
]], 1 + total
);
964 isl_int_add_ui(wraps
.mat
->row
[w
][0], wraps
.mat
->row
[w
][0], 1);
965 if (isl_tab_add_eq(tabs
[j
], wraps
.mat
->row
[w
]) < 0)
967 if (isl_tab_detect_redundant(tabs
[j
]) < 0)
971 isl_int_sub_ui(wraps
.mat
->row
[w
][0],
972 wraps
.mat
->row
[w
][0], 1);
973 else if (add_wraps(&wraps
, map
->p
[j
], tabs
[j
],
974 wraps
.mat
->row
[w
], set
) < 0)
977 if (isl_tab_rollback(tabs
[j
], snap
) < 0)
980 if (!wraps
.mat
->n_row
)
985 changed
= fuse(map
, i
, j
, tabs
,
986 eq_i
, ineq_i
, eq_j
, ineq_j
, wraps
.mat
, 0);
998 /* Given two basic sets i and j such that i has no cut equalities,
999 * check if relaxing all the cut inequalities of i by one turns
1000 * them into valid constraint for j and check if we can wrap in
1001 * the bits that are sticking out.
1002 * If so, replace the pair by their union.
1004 * We first check if all relaxed cut inequalities of i are valid for j
1005 * and then try to wrap in the intersections of the relaxed cut inequalities
1008 * During this wrapping, we consider the points of j that lie at a distance
1009 * of exactly 1 from i. In particular, we ignore the points that lie in
1010 * between this lower-dimensional space and the basic map i.
1011 * We can therefore only apply this to integer maps.
1037 * Wrapping can fail if the result of wrapping one of the facets
1038 * around its edges does not produce any new facet constraint.
1039 * In particular, this happens when we try to wrap in unbounded sets.
1041 * _______________________________________________________________________
1045 * |_| |_________________________________________________________________
1048 * The following is not an acceptable result of coalescing the above two
1049 * sets as it includes extra integer points.
1050 * _______________________________________________________________________
1055 * \______________________________________________________________________
1057 static int can_wrap_in_set(struct isl_map
*map
, int i
, int j
,
1058 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
1065 if (ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_RATIONAL
) ||
1066 ISL_F_ISSET(map
->p
[j
], ISL_BASIC_MAP_RATIONAL
))
1069 n
= count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
);
1073 cuts
= isl_alloc_array(map
->ctx
, int, n
);
1077 for (k
= 0, m
= 0; m
< n
; ++k
) {
1078 enum isl_ineq_type type
;
1080 if (ineq_i
[k
] != STATUS_CUT
)
1083 isl_int_add_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
1084 type
= isl_tab_ineq_type(tabs
[j
], map
->p
[i
]->ineq
[k
]);
1085 isl_int_sub_ui(map
->p
[i
]->ineq
[k
][0], map
->p
[i
]->ineq
[k
][0], 1);
1086 if (type
== isl_ineq_error
)
1088 if (type
!= isl_ineq_redundant
)
1095 changed
= wrap_in_facets(map
, i
, j
, cuts
, n
, tabs
,
1096 eq_i
, ineq_i
, eq_j
, ineq_j
);
1106 /* Check if either i or j has only cut inequalities that can
1107 * be used to wrap in (a facet of) the other basic set.
1108 * if so, replace the pair by their union.
1110 static int check_wrap(struct isl_map
*map
, int i
, int j
,
1111 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
1115 if (!any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_CUT
))
1116 changed
= can_wrap_in_set(map
, i
, j
, tabs
,
1117 eq_i
, ineq_i
, eq_j
, ineq_j
);
1121 if (!any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_CUT
))
1122 changed
= can_wrap_in_set(map
, j
, i
, tabs
,
1123 eq_j
, ineq_j
, eq_i
, ineq_i
);
1127 /* At least one of the basic maps has an equality that is adjacent
1128 * to inequality. Make sure that only one of the basic maps has
1129 * such an equality and that the other basic map has exactly one
1130 * inequality adjacent to an equality.
1131 * We call the basic map that has the inequality "i" and the basic
1132 * map that has the equality "j".
1133 * If "i" has any "cut" (in)equality, then relaxing the inequality
1134 * by one would not result in a basic map that contains the other
1137 static int check_adj_eq(struct isl_map
*map
, int i
, int j
,
1138 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
1143 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) &&
1144 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
))
1145 /* ADJ EQ TOO MANY */
1148 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
))
1149 return check_adj_eq(map
, j
, i
, tabs
,
1150 eq_j
, ineq_j
, eq_i
, ineq_i
);
1152 /* j has an equality adjacent to an inequality in i */
1154 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_CUT
))
1156 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_CUT
))
1159 if (count(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) != 1 ||
1160 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
) ||
1161 any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
1162 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
))
1163 /* ADJ EQ TOO MANY */
1166 for (k
= 0; k
< map
->p
[i
]->n_ineq
; ++k
)
1167 if (ineq_i
[k
] == STATUS_ADJ_EQ
)
1170 changed
= is_adj_eq_extension(map
, i
, j
, k
, tabs
,
1171 eq_i
, ineq_i
, eq_j
, ineq_j
);
1175 if (count(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
) != 1)
1178 changed
= can_wrap_in_facet(map
, i
, j
, k
, tabs
, eq_i
, ineq_i
, eq_j
, ineq_j
);
1183 /* The two basic maps lie on adjacent hyperplanes. In particular,
1184 * basic map "i" has an equality that lies parallel to basic map "j".
1185 * Check if we can wrap the facets around the parallel hyperplanes
1186 * to include the other set.
1188 * We perform basically the same operations as can_wrap_in_facet,
1189 * except that we don't need to select a facet of one of the sets.
1195 * If there is more than one equality of "i" adjacent to an equality of "j",
1196 * then the result will satisfy one or more equalities that are a linear
1197 * combination of these equalities. These will be encoded as pairs
1198 * of inequalities in the wrapping constraints and need to be made
1201 static int check_eq_adj_eq(struct isl_map
*map
, int i
, int j
,
1202 struct isl_tab
**tabs
, int *eq_i
, int *ineq_i
, int *eq_j
, int *ineq_j
)
1206 int detect_equalities
= 0;
1207 struct isl_wraps wraps
;
1209 struct isl_set
*set_i
= NULL
;
1210 struct isl_set
*set_j
= NULL
;
1211 struct isl_vec
*bound
= NULL
;
1212 unsigned total
= isl_basic_map_total_dim(map
->p
[i
]);
1214 if (count(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_EQ
) != 1)
1215 detect_equalities
= 1;
1217 for (k
= 0; k
< 2 * map
->p
[i
]->n_eq
; ++k
)
1218 if (eq_i
[k
] == STATUS_ADJ_EQ
)
1221 set_i
= set_from_updated_bmap(map
->p
[i
], tabs
[i
]);
1222 set_j
= set_from_updated_bmap(map
->p
[j
], tabs
[j
]);
1223 mat
= isl_mat_alloc(map
->ctx
, 2 * (map
->p
[i
]->n_eq
+ map
->p
[j
]->n_eq
) +
1224 map
->p
[i
]->n_ineq
+ map
->p
[j
]->n_ineq
,
1226 wraps_init(&wraps
, mat
, map
, i
, j
, eq_i
, ineq_i
, eq_j
, ineq_j
);
1227 bound
= isl_vec_alloc(map
->ctx
, 1 + total
);
1228 if (!set_i
|| !set_j
|| !wraps
.mat
|| !bound
)
1232 isl_seq_neg(bound
->el
, map
->p
[i
]->eq
[k
/ 2], 1 + total
);
1234 isl_seq_cpy(bound
->el
, map
->p
[i
]->eq
[k
/ 2], 1 + total
);
1235 isl_int_add_ui(bound
->el
[0], bound
->el
[0], 1);
1237 isl_seq_cpy(wraps
.mat
->row
[0], bound
->el
, 1 + total
);
1238 wraps
.mat
->n_row
= 1;
1240 if (add_wraps(&wraps
, map
->p
[j
], tabs
[j
], bound
->el
, set_i
) < 0)
1242 if (!wraps
.mat
->n_row
)
1245 isl_int_sub_ui(bound
->el
[0], bound
->el
[0], 1);
1246 isl_seq_neg(bound
->el
, bound
->el
, 1 + total
);
1248 isl_seq_cpy(wraps
.mat
->row
[wraps
.mat
->n_row
], bound
->el
, 1 + total
);
1251 if (add_wraps(&wraps
, map
->p
[i
], tabs
[i
], bound
->el
, set_j
) < 0)
1253 if (!wraps
.mat
->n_row
)
1256 changed
= fuse(map
, i
, j
, tabs
, eq_i
, ineq_i
, eq_j
, ineq_j
, wraps
.mat
,
1260 error
: changed
= -1;
1265 isl_set_free(set_i
);
1266 isl_set_free(set_j
);
1267 isl_vec_free(bound
);
1272 /* Check if the union of the given pair of basic maps
1273 * can be represented by a single basic map.
1274 * If so, replace the pair by the single basic map and return 1.
1275 * Otherwise, return 0;
1276 * The two basic maps are assumed to live in the same local space.
1278 * We first check the effect of each constraint of one basic map
1279 * on the other basic map.
1280 * The constraint may be
1281 * redundant the constraint is redundant in its own
1282 * basic map and should be ignore and removed
1284 * valid all (integer) points of the other basic map
1285 * satisfy the constraint
1286 * separate no (integer) point of the other basic map
1287 * satisfies the constraint
1288 * cut some but not all points of the other basic map
1289 * satisfy the constraint
1290 * adj_eq the given constraint is adjacent (on the outside)
1291 * to an equality of the other basic map
1292 * adj_ineq the given constraint is adjacent (on the outside)
1293 * to an inequality of the other basic map
1295 * We consider seven cases in which we can replace the pair by a single
1296 * basic map. We ignore all "redundant" constraints.
1298 * 1. all constraints of one basic map are valid
1299 * => the other basic map is a subset and can be removed
1301 * 2. all constraints of both basic maps are either "valid" or "cut"
1302 * and the facets corresponding to the "cut" constraints
1303 * of one of the basic maps lies entirely inside the other basic map
1304 * => the pair can be replaced by a basic map consisting
1305 * of the valid constraints in both basic maps
1307 * 3. there is a single pair of adjacent inequalities
1308 * (all other constraints are "valid")
1309 * => the pair can be replaced by a basic map consisting
1310 * of the valid constraints in both basic maps
1312 * 4. one basic map has a single adjacent inequality, while the other
1313 * constraints are "valid". The other basic map has some
1314 * "cut" constraints, but replacing the adjacent inequality by
1315 * its opposite and adding the valid constraints of the other
1316 * basic map results in a subset of the other basic map
1317 * => the pair can be replaced by a basic map consisting
1318 * of the valid constraints in both basic maps
1320 * 5. there is a single adjacent pair of an inequality and an equality,
1321 * the other constraints of the basic map containing the inequality are
1322 * "valid". Moreover, if the inequality the basic map is relaxed
1323 * and then turned into an equality, then resulting facet lies
1324 * entirely inside the other basic map
1325 * => the pair can be replaced by the basic map containing
1326 * the inequality, with the inequality relaxed.
1328 * 6. there is a single adjacent pair of an inequality and an equality,
1329 * the other constraints of the basic map containing the inequality are
1330 * "valid". Moreover, the facets corresponding to both
1331 * the inequality and the equality can be wrapped around their
1332 * ridges to include the other basic map
1333 * => the pair can be replaced by a basic map consisting
1334 * of the valid constraints in both basic maps together
1335 * with all wrapping constraints
1337 * 7. one of the basic maps extends beyond the other by at most one.
1338 * Moreover, the facets corresponding to the cut constraints and
1339 * the pieces of the other basic map at offset one from these cut
1340 * constraints can be wrapped around their ridges to include
1341 * the union of the two basic maps
1342 * => the pair can be replaced by a basic map consisting
1343 * of the valid constraints in both basic maps together
1344 * with all wrapping constraints
1346 * 8. the two basic maps live in adjacent hyperplanes. In principle
1347 * such sets can always be combined through wrapping, but we impose
1348 * that there is only one such pair, to avoid overeager coalescing.
1350 * Throughout the computation, we maintain a collection of tableaus
1351 * corresponding to the basic maps. When the basic maps are dropped
1352 * or combined, the tableaus are modified accordingly.
1354 static int coalesce_local_pair(__isl_keep isl_map
*map
, int i
, int j
,
1355 struct isl_tab
**tabs
)
1363 eq_i
= eq_status_in(map
->p
[i
], tabs
[j
]);
1364 if (map
->p
[i
]->n_eq
&& !eq_i
)
1366 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ERROR
))
1368 if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_SEPARATE
))
1371 eq_j
= eq_status_in(map
->p
[j
], tabs
[i
]);
1372 if (map
->p
[j
]->n_eq
&& !eq_j
)
1374 if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ERROR
))
1376 if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_SEPARATE
))
1379 ineq_i
= ineq_status_in(map
->p
[i
], tabs
[i
], tabs
[j
]);
1380 if (map
->p
[i
]->n_ineq
&& !ineq_i
)
1382 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ERROR
))
1384 if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_SEPARATE
))
1387 ineq_j
= ineq_status_in(map
->p
[j
], tabs
[j
], tabs
[i
]);
1388 if (map
->p
[j
]->n_ineq
&& !ineq_j
)
1390 if (any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ERROR
))
1392 if (any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_SEPARATE
))
1395 if (all(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_VALID
) &&
1396 all(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_VALID
)) {
1399 } else if (all(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_VALID
) &&
1400 all(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_VALID
)) {
1403 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_EQ
)) {
1404 changed
= check_eq_adj_eq(map
, i
, j
, tabs
,
1405 eq_i
, ineq_i
, eq_j
, ineq_j
);
1406 } else if (any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_EQ
)) {
1407 changed
= check_eq_adj_eq(map
, j
, i
, tabs
,
1408 eq_j
, ineq_j
, eq_i
, ineq_i
);
1409 } else if (any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_ADJ_INEQ
) ||
1410 any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_ADJ_INEQ
)) {
1411 changed
= check_adj_eq(map
, i
, j
, tabs
,
1412 eq_i
, ineq_i
, eq_j
, ineq_j
);
1413 } else if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_EQ
) ||
1414 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_EQ
)) {
1417 } else if (any(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_ADJ_INEQ
) ||
1418 any(ineq_j
, map
->p
[j
]->n_ineq
, STATUS_ADJ_INEQ
)) {
1419 changed
= check_adj_ineq(map
, i
, j
, tabs
,
1420 eq_i
, ineq_i
, eq_j
, ineq_j
);
1422 if (!any(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_CUT
) &&
1423 !any(eq_j
, 2 * map
->p
[j
]->n_eq
, STATUS_CUT
))
1424 changed
= check_facets(map
, i
, j
, tabs
, ineq_i
, ineq_j
);
1426 changed
= check_wrap(map
, i
, j
, tabs
,
1427 eq_i
, ineq_i
, eq_j
, ineq_j
);
1444 /* Do the two basic maps live in the same local space, i.e.,
1445 * do they have the same (known) divs?
1446 * If either basic map has any unknown divs, then we can only assume
1447 * that they do not live in the same local space.
1449 static int same_divs(__isl_keep isl_basic_map
*bmap1
,
1450 __isl_keep isl_basic_map
*bmap2
)
1456 if (!bmap1
|| !bmap2
)
1458 if (bmap1
->n_div
!= bmap2
->n_div
)
1461 if (bmap1
->n_div
== 0)
1464 known
= isl_basic_map_divs_known(bmap1
);
1465 if (known
< 0 || !known
)
1467 known
= isl_basic_map_divs_known(bmap2
);
1468 if (known
< 0 || !known
)
1471 total
= isl_basic_map_total_dim(bmap1
);
1472 for (i
= 0; i
< bmap1
->n_div
; ++i
)
1473 if (!isl_seq_eq(bmap1
->div
[i
], bmap2
->div
[i
], 2 + total
))
1479 /* Given two basic maps "i" and "j", where the divs of "i" form a subset
1480 * of those of "j", check if basic map "j" is a subset of basic map "i"
1481 * and, if so, drop basic map "j".
1483 * We first expand the divs of basic map "i" to match those of basic map "j",
1484 * using the divs and expansion computed by the caller.
1485 * Then we check if all constraints of the expanded "i" are valid for "j".
1487 static int coalesce_subset(__isl_keep isl_map
*map
, int i
, int j
,
1488 struct isl_tab
**tabs
, __isl_keep isl_mat
*div
, int *exp
)
1490 isl_basic_map
*bmap
;
1495 bmap
= isl_basic_map_copy(map
->p
[i
]);
1496 bmap
= isl_basic_set_expand_divs(bmap
, isl_mat_copy(div
), exp
);
1501 eq_i
= eq_status_in(bmap
, tabs
[j
]);
1502 if (bmap
->n_eq
&& !eq_i
)
1504 if (any(eq_i
, 2 * bmap
->n_eq
, STATUS_ERROR
))
1506 if (any(eq_i
, 2 * bmap
->n_eq
, STATUS_SEPARATE
))
1509 ineq_i
= ineq_status_in(bmap
, NULL
, tabs
[j
]);
1510 if (bmap
->n_ineq
&& !ineq_i
)
1512 if (any(ineq_i
, bmap
->n_ineq
, STATUS_ERROR
))
1514 if (any(ineq_i
, bmap
->n_ineq
, STATUS_SEPARATE
))
1517 if (all(eq_i
, 2 * map
->p
[i
]->n_eq
, STATUS_VALID
) &&
1518 all(ineq_i
, map
->p
[i
]->n_ineq
, STATUS_VALID
)) {
1524 isl_basic_map_free(bmap
);
1529 isl_basic_map_free(bmap
);
1535 /* Check if the basic map "j" is a subset of basic map "i",
1536 * assuming that "i" has fewer divs that "j".
1537 * If not, then we change the order.
1539 * If the two basic maps have the same number of divs, then
1540 * they must necessarily be different. Otherwise, we would have
1541 * called coalesce_local_pair. We therefore don't try anything
1544 * We first check if the divs of "i" are all known and form a subset
1545 * of those of "j". If so, we pass control over to coalesce_subset.
1547 static int check_coalesce_subset(__isl_keep isl_map
*map
, int i
, int j
,
1548 struct isl_tab
**tabs
)
1551 isl_mat
*div_i
, *div_j
, *div
;
1557 if (map
->p
[i
]->n_div
== map
->p
[j
]->n_div
)
1559 if (map
->p
[j
]->n_div
< map
->p
[i
]->n_div
)
1560 return check_coalesce_subset(map
, j
, i
, tabs
);
1562 known
= isl_basic_map_divs_known(map
->p
[i
]);
1563 if (known
< 0 || !known
)
1566 ctx
= isl_map_get_ctx(map
);
1568 div_i
= isl_basic_map_get_divs(map
->p
[i
]);
1569 div_j
= isl_basic_map_get_divs(map
->p
[j
]);
1571 if (!div_i
|| !div_j
)
1574 exp1
= isl_alloc_array(ctx
, int, div_i
->n_row
);
1575 exp2
= isl_alloc_array(ctx
, int, div_j
->n_row
);
1576 if ((div_i
->n_row
&& !exp1
) || (div_j
->n_row
&& !exp2
))
1579 div
= isl_merge_divs(div_i
, div_j
, exp1
, exp2
);
1583 if (div
->n_row
== div_j
->n_row
)
1584 subset
= coalesce_subset(map
, i
, j
, tabs
, div
, exp1
);
1590 isl_mat_free(div_i
);
1591 isl_mat_free(div_j
);
1598 isl_mat_free(div_i
);
1599 isl_mat_free(div_j
);
1605 /* Check if the union of the given pair of basic maps
1606 * can be represented by a single basic map.
1607 * If so, replace the pair by the single basic map and return 1.
1608 * Otherwise, return 0;
1610 * We first check if the two basic maps live in the same local space.
1611 * If so, we do the complete check. Otherwise, we check if one is
1612 * an obvious subset of the other.
1614 static int coalesce_pair(__isl_keep isl_map
*map
, int i
, int j
,
1615 struct isl_tab
**tabs
)
1619 same
= same_divs(map
->p
[i
], map
->p
[j
]);
1623 return coalesce_local_pair(map
, i
, j
, tabs
);
1625 return check_coalesce_subset(map
, i
, j
, tabs
);
1628 static struct isl_map
*coalesce(struct isl_map
*map
, struct isl_tab
**tabs
)
1632 for (i
= map
->n
- 2; i
>= 0; --i
)
1634 for (j
= i
+ 1; j
< map
->n
; ++j
) {
1636 changed
= coalesce_pair(map
, i
, j
, tabs
);
1648 /* For each pair of basic maps in the map, check if the union of the two
1649 * can be represented by a single basic map.
1650 * If so, replace the pair by the single basic map and start over.
1652 * Since we are constructing the tableaus of the basic maps anyway,
1653 * we exploit them to detect implicit equalities and redundant constraints.
1654 * This also helps the coalescing as it can ignore the redundant constraints.
1655 * In order to avoid confusion, we make all implicit equalities explicit
1656 * in the basic maps. We don't call isl_basic_map_gauss, though,
1657 * as that may affect the number of constraints.
1658 * This means that we have to call isl_basic_map_gauss at the end
1659 * of the computation to ensure that the basic maps are not left
1660 * in an unexpected state.
1662 struct isl_map
*isl_map_coalesce(struct isl_map
*map
)
1666 struct isl_tab
**tabs
= NULL
;
1668 map
= isl_map_remove_empty_parts(map
);
1675 map
= isl_map_sort_divs(map
);
1676 map
= isl_map_cow(map
);
1681 tabs
= isl_calloc_array(map
->ctx
, struct isl_tab
*, map
->n
);
1686 for (i
= 0; i
< map
->n
; ++i
) {
1687 tabs
[i
] = isl_tab_from_basic_map(map
->p
[i
], 0);
1690 if (!ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_NO_IMPLICIT
))
1691 if (isl_tab_detect_implicit_equalities(tabs
[i
]) < 0)
1693 map
->p
[i
] = isl_tab_make_equalities_explicit(tabs
[i
],
1697 if (!ISL_F_ISSET(map
->p
[i
], ISL_BASIC_MAP_NO_REDUNDANT
))
1698 if (isl_tab_detect_redundant(tabs
[i
]) < 0)
1701 for (i
= map
->n
- 1; i
>= 0; --i
)
1705 map
= coalesce(map
, tabs
);
1708 for (i
= 0; i
< map
->n
; ++i
) {
1709 map
->p
[i
] = isl_basic_map_update_from_tab(map
->p
[i
],
1711 map
->p
[i
] = isl_basic_map_gauss(map
->p
[i
], NULL
);
1712 map
->p
[i
] = isl_basic_map_finalize(map
->p
[i
]);
1715 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_NO_IMPLICIT
);
1716 ISL_F_SET(map
->p
[i
], ISL_BASIC_MAP_NO_REDUNDANT
);
1719 for (i
= 0; i
< n
; ++i
)
1720 isl_tab_free(tabs
[i
]);
1727 for (i
= 0; i
< n
; ++i
)
1728 isl_tab_free(tabs
[i
]);
1734 /* For each pair of basic sets in the set, check if the union of the two
1735 * can be represented by a single basic set.
1736 * If so, replace the pair by the single basic set and start over.
1738 struct isl_set
*isl_set_coalesce(struct isl_set
*set
)
1740 return (struct isl_set
*)isl_map_coalesce((struct isl_map
*)set
);