isl_coalesce.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  * Copyright 2010      INRIA Saclay
   4  *
   5  * Use of this software is governed by the GNU LGPLv2.1 license
   6  *
   7  * Written by Sven Verdoolaege, K.U.Leuven, Departement
   8  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
   9  * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
  10  * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
  11  */
  12
  13 #include "isl_map_private.h"
  14 #include "isl_seq.h"
  15 #include "isl_tab.h"
  16
  17 #define STATUS_ERROR            -1
  18 #define STATUS_REDUNDANT         1
  19 #define STATUS_VALID             2
  20 #define STATUS_SEPARATE          3
  21 #define STATUS_CUT               4
  22 #define STATUS_ADJ_EQ            5
  23 #define STATUS_ADJ_INEQ          6
  24
  25 static int status_in(isl_int *ineq, struct isl_tab *tab)
  26 {
  27         enum isl_ineq_type type = isl_tab_ineq_type(tab, ineq);
  28         switch (type) {
  29         case isl_ineq_error:            return STATUS_ERROR;
  30         case isl_ineq_redundant:        return STATUS_VALID;
  31         case isl_ineq_separate:         return STATUS_SEPARATE;
  32         case isl_ineq_cut:              return STATUS_CUT;
  33         case isl_ineq_adj_eq:           return STATUS_ADJ_EQ;
  34         case isl_ineq_adj_ineq:         return STATUS_ADJ_INEQ;
  35         }
  36 }
  37
  38 /* Compute the position of the equalities of basic map "i"
  39  * with respect to basic map "j".
  40  * The resulting array has twice as many entries as the number
  41  * of equalities corresponding to the two inequalties to which
  42  * each equality corresponds.
  43  */
  44 static int *eq_status_in(struct isl_map *map, int i, int j,
  45         struct isl_tab **tabs)
  46 {
  47         int k, l;
  48         int *eq = isl_calloc_array(map->ctx, int, 2 * map->p[i]->n_eq);
  49         unsigned dim;
  50
  51         dim = isl_basic_map_total_dim(map->p[i]);
  52         for (k = 0; k < map->p[i]->n_eq; ++k) {
  53                 for (l = 0; l < 2; ++l) {
  54                         isl_seq_neg(map->p[i]->eq[k], map->p[i]->eq[k], 1+dim);
  55                         eq[2 * k + l] = status_in(map->p[i]->eq[k], tabs[j]);
  56                         if (eq[2 * k + l] == STATUS_ERROR)
  57                                 goto error;
  58                 }
  59                 if (eq[2 * k] == STATUS_SEPARATE ||
  60                     eq[2 * k + 1] == STATUS_SEPARATE)
  61                         break;
  62         }
  63
  64         return eq;
  65 error:
  66         free(eq);
  67         return NULL;
  68 }
  69
  70 /* Compute the position of the inequalities of basic map "i"
  71  * with respect to basic map "j".
  72  */
  73 static int *ineq_status_in(struct isl_map *map, int i, int j,
  74         struct isl_tab **tabs)
  75 {
  76         int k;
  77         unsigned n_eq = map->p[i]->n_eq;
  78         int *ineq = isl_calloc_array(map->ctx, int, map->p[i]->n_ineq);
  79
  80         for (k = 0; k < map->p[i]->n_ineq; ++k) {
  81                 if (isl_tab_is_redundant(tabs[i], n_eq + k)) {
  82                         ineq[k] = STATUS_REDUNDANT;
  83                         continue;
  84                 }
  85                 ineq[k] = status_in(map->p[i]->ineq[k], tabs[j]);
  86                 if (ineq[k] == STATUS_ERROR)
  87                         goto error;
  88                 if (ineq[k] == STATUS_SEPARATE)
  89                         break;
  90         }
  91
  92         return ineq;
  93 error:
  94         free(ineq);
  95         return NULL;
  96 }
  97
  98 static int any(int *con, unsigned len, int status)
  99 {
 100         int i;
 101
 102         for (i = 0; i < len ; ++i)
 103                 if (con[i] == status)
 104                         return 1;
 105         return 0;
 106 }
 107
 108 static int count(int *con, unsigned len, int status)
 109 {
 110         int i;
 111         int c = 0;
 112
 113         for (i = 0; i < len ; ++i)
 114                 if (con[i] == status)
 115                         c++;
 116         return c;
 117 }
 118
 119 static int all(int *con, unsigned len, int status)
 120 {
 121         int i;
 122
 123         for (i = 0; i < len ; ++i) {
 124                 if (con[i] == STATUS_REDUNDANT)
 125                         continue;
 126                 if (con[i] != status)
 127                         return 0;
 128         }
 129         return 1;
 130 }
 131
 132 static void drop(struct isl_map *map, int i, struct isl_tab **tabs)
 133 {
 134         isl_basic_map_free(map->p[i]);
 135         isl_tab_free(tabs[i]);
 136
 137         if (i != map->n - 1) {
 138                 map->p[i] = map->p[map->n - 1];
 139                 tabs[i] = tabs[map->n - 1];
 140         }
 141         tabs[map->n - 1] = NULL;
 142         map->n--;
 143 }
 144
 145 /* Replace the pair of basic maps i and j by the basic map bounded
 146  * by the valid constraints in both basic maps and the constraint
 147  * in extra (if not NULL).
 148  */
 149 static int fuse(struct isl_map *map, int i, int j,
 150         struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j,
 151         __isl_keep isl_mat *extra)
 152 {
 153         int k, l;
 154         struct isl_basic_map *fused = NULL;
 155         struct isl_tab *fused_tab = NULL;
 156         unsigned total = isl_basic_map_total_dim(map->p[i]);
 157         unsigned extra_rows = extra ? extra->n_row : 0;
 158
 159         fused = isl_basic_map_alloc_dim(isl_dim_copy(map->p[i]->dim),
 160                         map->p[i]->n_div,
 161                         map->p[i]->n_eq + map->p[j]->n_eq,
 162                         map->p[i]->n_ineq + map->p[j]->n_ineq + extra_rows);
 163         if (!fused)
 164                 goto error;
 165
 166         for (k = 0; k < map->p[i]->n_eq; ++k) {
 167                 if (eq_i && (eq_i[2 * k] != STATUS_VALID ||
 168                              eq_i[2 * k + 1] != STATUS_VALID))
 169                 l = isl_basic_map_alloc_equality(fused);
 170                 if (l < 0)
 171                         goto error;
 172                 isl_seq_cpy(fused->eq[l], map->p[i]->eq[k], 1 + total);
 173         }
 174
 175         for (k = 0; k < map->p[j]->n_eq; ++k) {
 176                 if (eq_j && (eq_j[2 * k] != STATUS_VALID ||
 177                              eq_j[2 * k + 1] != STATUS_VALID))
 178                         continue;
 179                 l = isl_basic_map_alloc_equality(fused);
 180                 if (l < 0)
 181                         goto error;
 182                 isl_seq_cpy(fused->eq[l], map->p[j]->eq[k], 1 + total);
 183         }
 184
 185         for (k = 0; k < map->p[i]->n_ineq; ++k) {
 186                 if (ineq_i[k] != STATUS_VALID)
 187                         continue;
 188                 l = isl_basic_map_alloc_inequality(fused);
 189                 if (l < 0)
 190                         goto error;
 191                 isl_seq_cpy(fused->ineq[l], map->p[i]->ineq[k], 1 + total);
 192         }
 193
 194         for (k = 0; k < map->p[j]->n_ineq; ++k) {
 195                 if (ineq_j[k] != STATUS_VALID)
 196                         continue;
 197                 l = isl_basic_map_alloc_inequality(fused);
 198                 if (l < 0)
 199                         goto error;
 200                 isl_seq_cpy(fused->ineq[l], map->p[j]->ineq[k], 1 + total);
 201         }
 202
 203         for (k = 0; k < extra_rows; ++k) {
 204                 l = isl_basic_map_alloc_inequality(fused);
 205                 if (l < 0)
 206                         goto error;
 207                 isl_seq_cpy(fused->ineq[l], extra->row[k], 1 + total);
 208         }
 209
 210         fused = isl_basic_map_gauss(fused, NULL);
 211         ISL_F_SET(fused, ISL_BASIC_MAP_FINAL);
 212         if (ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_RATIONAL) &&
 213             ISL_F_ISSET(map->p[j], ISL_BASIC_MAP_RATIONAL))
 214                 ISL_F_SET(fused, ISL_BASIC_MAP_RATIONAL);
 215
 216         fused_tab = isl_tab_from_basic_map(fused);
 217         if (isl_tab_detect_redundant(fused_tab) < 0)
 218                 goto error;
 219
 220         isl_basic_map_free(map->p[i]);
 221         map->p[i] = fused;
 222         isl_tab_free(tabs[i]);
 223         tabs[i] = fused_tab;
 224         drop(map, j, tabs);
 225
 226         return 1;
 227 error:
 228         isl_tab_free(fused_tab);
 229         isl_basic_map_free(fused);
 230         return -1;
 231 }
 232
 233 /* Given a pair of basic maps i and j such that all constraints are either
 234  * "valid" or "cut", check if the facets corresponding to the "cut"
 235  * constraints of i lie entirely within basic map j.
 236  * If so, replace the pair by the basic map consisting of the valid
 237  * constraints in both basic maps.
 238  *
 239  * To see that we are not introducing any extra points, call the
 240  * two basic maps A and B and the resulting map U and let x
 241  * be an element of U \setminus ( A \cup B ).
 242  * Then there is a pair of cut constraints c_1 and c_2 in A and B such that x
 243  * violates them.  Let X be the intersection of U with the opposites
 244  * of these constraints.  Then x \in X.
 245  * The facet corresponding to c_1 contains the corresponding facet of A.
 246  * This facet is entirely contained in B, so c_2 is valid on the facet.
 247  * However, since it is also (part of) a facet of X, -c_2 is also valid
 248  * on the facet.  This means c_2 is saturated on the facet, so c_1 and
 249  * c_2 must be opposites of each other, but then x could not violate
 250  * both of them.
 251  */
 252 static int check_facets(struct isl_map *map, int i, int j,
 253         struct isl_tab **tabs, int *ineq_i, int *ineq_j)
 254 {
 255         int k, l;
 256         struct isl_tab_undo *snap;
 257         unsigned n_eq = map->p[i]->n_eq;
 258
 259         snap = isl_tab_snap(tabs[i]);
 260
 261         for (k = 0; k < map->p[i]->n_ineq; ++k) {
 262                 if (ineq_i[k] != STATUS_CUT)
 263                         continue;
 264                 tabs[i] = isl_tab_select_facet(tabs[i], n_eq + k);
 265                 for (l = 0; l < map->p[j]->n_ineq; ++l) {
 266                         int stat;
 267                         if (ineq_j[l] != STATUS_CUT)
 268                                 continue;
 269                         stat = status_in(map->p[j]->ineq[l], tabs[i]);
 270                         if (stat != STATUS_VALID)
 271                                 break;
 272                 }
 273                 if (isl_tab_rollback(tabs[i], snap) < 0)
 274                         return -1;
 275                 if (l < map->p[j]->n_ineq)
 276                         break;
 277         }
 278
 279         if (k < map->p[i]->n_ineq)
 280                 /* BAD CUT PAIR */
 281                 return 0;
 282         return fuse(map, i, j, tabs, NULL, ineq_i, NULL, ineq_j, NULL);
 283 }
 284
 285 /* Both basic maps have at least one inequality with and adjacent
 286  * (but opposite) inequality in the other basic map.
 287  * Check that there are no cut constraints and that there is only
 288  * a single pair of adjacent inequalities.
 289  * If so, we can replace the pair by a single basic map described
 290  * by all but the pair of adjacent inequalities.
 291  * Any additional points introduced lie strictly between the two
 292  * adjacent hyperplanes and can therefore be integral.
 293  *
 294  *        ____                    _____
 295  *       /    ||\                /     \
 296  *      /     || \              /       \
 297  *      \     ||  \     =>      \        \
 298  *       \    ||  /              \       /
 299  *        \___||_/                \_____/
 300  *
 301  * The test for a single pair of adjancent inequalities is important
 302  * for avoiding the combination of two basic maps like the following
 303  *
 304  *       /|
 305  *      / |
 306  *     /__|
 307  *         _____
 308  *         |   |
 309  *         |   |
 310  *         |___|
 311  */
 312 static int check_adj_ineq(struct isl_map *map, int i, int j,
 313         struct isl_tab **tabs, int *ineq_i, int *ineq_j)
 314 {
 315         int changed = 0;
 316
 317         if (any(ineq_i, map->p[i]->n_ineq, STATUS_CUT) ||
 318             any(ineq_j, map->p[j]->n_ineq, STATUS_CUT))
 319                 /* ADJ INEQ CUT */
 320                 ;
 321         else if (count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) == 1 &&
 322                  count(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ) == 1)
 323                 changed = fuse(map, i, j, tabs, NULL, ineq_i, NULL, ineq_j, NULL);
 324         /* else ADJ INEQ TOO MANY */
 325
 326         return changed;
 327 }
 328
 329 /* Check if basic map "i" contains the basic map represented
 330  * by the tableau "tab".
 331  */
 332 static int contains(struct isl_map *map, int i, int *ineq_i,
 333         struct isl_tab *tab)
 334 {
 335         int k, l;
 336         unsigned dim;
 337
 338         dim = isl_basic_map_total_dim(map->p[i]);
 339         for (k = 0; k < map->p[i]->n_eq; ++k) {
 340                 for (l = 0; l < 2; ++l) {
 341                         int stat;
 342                         isl_seq_neg(map->p[i]->eq[k], map->p[i]->eq[k], 1+dim);
 343                         stat = status_in(map->p[i]->eq[k], tab);
 344                         if (stat != STATUS_VALID)
 345                                 return 0;
 346                 }
 347         }
 348
 349         for (k = 0; k < map->p[i]->n_ineq; ++k) {
 350                 int stat;
 351                 if (ineq_i[k] == STATUS_REDUNDANT)
 352                         continue;
 353                 stat = status_in(map->p[i]->ineq[k], tab);
 354                 if (stat != STATUS_VALID)
 355                         return 0;
 356         }
 357         return 1;
 358 }
 359
 360 /* Basic map "i" has an inequality "k" that is adjacent to some equality
 361  * of basic map "j".  All the other inequalities are valid for "j".
 362  * Check if basic map "j" forms an extension of basic map "i".
 363  *
 364  * In particular, we relax constraint "k", compute the corresponding
 365  * facet and check whether it is included in the other basic map.
 366  * If so, we know that relaxing the constraint extends the basic
 367  * map with exactly the other basic map (we already know that this
 368  * other basic map is included in the extension, because there
 369  * were no "cut" inequalities in "i") and we can replace the
 370  * two basic maps by thie extension.
 371  *        ____                    _____
 372  *       /    ||                 /     |
 373  *      /     ||                /      |
 374  *      \     ||        =>      \      |
 375  *       \    ||                 \     |
 376  *        \___||                  \____|
 377  */
 378 static int is_extension(struct isl_map *map, int i, int j, int k,
 379         struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
 380 {
 381         int changed = 0;
 382         int super;
 383         struct isl_tab_undo *snap, *snap2;
 384         unsigned n_eq = map->p[i]->n_eq;
 385
 386         snap = isl_tab_snap(tabs[i]);
 387         tabs[i] = isl_tab_relax(tabs[i], n_eq + k);
 388         snap2 = isl_tab_snap(tabs[i]);
 389         tabs[i] = isl_tab_select_facet(tabs[i], n_eq + k);
 390         super = contains(map, j, ineq_j, tabs[i]);
 391         if (super) {
 392                 if (isl_tab_rollback(tabs[i], snap2) < 0)
 393                         return -1;
 394                 map->p[i] = isl_basic_map_cow(map->p[i]);
 395                 if (!map->p[i])
 396                         return -1;
 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);
 399                 drop(map, j, tabs);
 400                 changed = 1;
 401         } else
 402                 if (isl_tab_rollback(tabs[i], snap) < 0)
 403                         return -1;
 404
 405         return changed;
 406 }
 407
 408 /* For each non-redundant constraint in "bmap" (as determined by "tab"),
 409  * wrap the constraint around "bound" such that it includes the whole
 410  * set "set" and append the resulting constraint to "wraps".
 411  * "wraps" is assumed to have been pre-allocated to the appropriate size.
 412  * wraps->n_row is the number of actual wrapped constraints that have
 413  * been added.
 414  * If any of the wrapping problems results in a constraint that is
 415  * identical to "bound", then this means that "set" is unbounded in such
 416  * way that no wrapping is possible.  If this happens then wraps->n_row
 417  * is reset to zero.
 418  */
 419 static int add_wraps(__isl_keep isl_mat *wraps, __isl_keep isl_basic_map *bmap,
 420         struct isl_tab *tab, isl_int *bound, __isl_keep isl_set *set)
 421 {
 422         int l;
 423         int w;
 424         unsigned total = isl_basic_map_total_dim(bmap);
 425
 426         w = wraps->n_row;
 427
 428         for (l = 0; l < bmap->n_ineq; ++l) {
 429                 if (isl_seq_is_neg(bound, bmap->ineq[l], 1 + total))
 430                         continue;
 431                 if (isl_seq_eq(bound, bmap->ineq[l], 1 + total))
 432                         continue;
 433                 if (isl_tab_is_redundant(tab, bmap->n_eq + l))
 434                         continue;
 435
 436                 isl_seq_cpy(wraps->row[w], bound, 1 + total);
 437                 if (!isl_set_wrap_facet(set, wraps->row[w], bmap->ineq[l]))
 438                         return -1;
 439                 if (isl_seq_eq(wraps->row[w], bound, 1 + total))
 440                         goto unbounded;
 441                 ++w;
 442         }
 443         for (l = 0; l < bmap->n_eq; ++l) {
 444                 if (isl_seq_is_neg(bound, bmap->eq[l], 1 + total))
 445                         continue;
 446                 if (isl_seq_eq(bound, bmap->eq[l], 1 + total))
 447                         continue;
 448
 449                 isl_seq_cpy(wraps->row[w], bound, 1 + total);
 450                 isl_seq_neg(wraps->row[w + 1], bmap->eq[l], 1 + total);
 451                 if (!isl_set_wrap_facet(set, wraps->row[w], wraps->row[w + 1]))
 452                         return -1;
 453                 if (isl_seq_eq(wraps->row[w], bound, 1 + total))
 454                         goto unbounded;
 455                 ++w;
 456
 457                 isl_seq_cpy(wraps->row[w], bound, 1 + total);
 458                 if (!isl_set_wrap_facet(set, wraps->row[w], bmap->eq[l]))
 459                         return -1;
 460                 if (isl_seq_eq(wraps->row[w], bound, 1 + total))
 461                         goto unbounded;
 462                 ++w;
 463         }
 464
 465         wraps->n_row = w;
 466         return 0;
 467 unbounded:
 468         wraps->n_row = 0;
 469         return 0;
 470 }
 471
 472 /* Given a basic set i with a constraint k that is adjacent to either the
 473  * whole of basic set j or a facet of basic set j, check if we can wrap
 474  * both the facet corresponding to k and the facet of j (or the whole of j)
 475  * around their ridges to include the other set.
 476  * If so, replace the pair of basic sets by their union.
 477  *
 478  * All constraints of i (except k) are assumed to be valid for j.
 479  *
 480  * In the case where j has a facet adjacent to i, tab[j] is assumed
 481  * to have been restricted to this facet, so that the non-redundant
 482  * constraints in tab[j] are the ridges of the facet.
 483  * Note that for the purpose of wrapping, it does not matter whether
 484  * we wrap the ridges of i aronud the whole of j or just around
 485  * the facet since all the other constraints are assumed to be valid for j.
 486  * In practice, we wrap to include the whole of j.
 487  *        ____                    _____
 488  *       /    |                  /     \
 489  *      /     ||                /      |
 490  *      \     ||        =>      \      |
 491  *       \    ||                 \     |
 492  *        \___||                  \____|
 493  *
 494  */
 495 static int can_wrap_in_facet(struct isl_map *map, int i, int j, int k,
 496         struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
 497 {
 498         int changed = 0;
 499         struct isl_mat *wraps = NULL;
 500         struct isl_set *set_i = NULL;
 501         struct isl_set *set_j = NULL;
 502         struct isl_vec *bound = NULL;
 503         unsigned total = isl_basic_map_total_dim(map->p[i]);
 504         struct isl_tab_undo *snap;
 505
 506         snap = isl_tab_snap(tabs[i]);
 507
 508         set_i = isl_set_from_basic_set(
 509                     isl_basic_map_underlying_set(isl_basic_map_copy(map->p[i])));
 510         set_j = isl_set_from_basic_set(
 511                     isl_basic_map_underlying_set(isl_basic_map_copy(map->p[j])));
 512         wraps = isl_mat_alloc(map->ctx, 2 * (map->p[i]->n_eq + map->p[j]->n_eq) +
 513                                         map->p[i]->n_ineq + map->p[j]->n_ineq,
 514                                         1 + total);
 515         bound = isl_vec_alloc(map->ctx, 1 + total);
 516         if (!set_i || !set_j || !wraps || !bound)
 517                 goto error;
 518
 519         isl_seq_cpy(bound->el, map->p[i]->ineq[k], 1 + total);
 520         isl_int_add_ui(bound->el[0], bound->el[0], 1);
 521
 522         isl_seq_cpy(wraps->row[0], bound->el, 1 + total);
 523         wraps->n_row = 1;
 524
 525         if (add_wraps(wraps, map->p[j], tabs[j], bound->el, set_i) < 0)
 526                 goto error;
 527         if (!wraps->n_row)
 528                 goto unbounded;
 529
 530         tabs[i] = isl_tab_select_facet(tabs[i], map->p[i]->n_eq + k);
 531         if (isl_tab_detect_redundant(tabs[i]) < 0)
 532                 goto error;
 533
 534         isl_seq_neg(bound->el, map->p[i]->ineq[k], 1 + total);
 535
 536         if (add_wraps(wraps, map->p[i], tabs[i], bound->el, set_j) < 0)
 537                 goto error;
 538         if (!wraps->n_row)
 539                 goto unbounded;
 540
 541         changed = fuse(map, i, j, tabs, eq_i, ineq_i, eq_j, ineq_j, wraps);
 542
 543         if (!changed) {
 544 unbounded:
 545                 if (isl_tab_rollback(tabs[i], snap) < 0)
 546                         goto error;
 547         }
 548
 549         isl_mat_free(wraps);
 550
 551         isl_set_free(set_i);
 552         isl_set_free(set_j);
 553
 554         isl_vec_free(bound);
 555
 556         return changed;
 557 error:
 558         isl_vec_free(bound);
 559         isl_mat_free(wraps);
 560         isl_set_free(set_i);
 561         isl_set_free(set_j);
 562         return -1;
 563 }
 564
 565 /* Given two basic sets i and j such that i has exactly one cut constraint,
 566  * check if we can wrap the corresponding facet around its ridges to include
 567  * the other basic set (and nothing else).
 568  * If so, replace the pair by their union.
 569  *
 570  * We first check if j has a facet adjacent to the cut constraint of i.
 571  * If so, we try to wrap in the facet.
 572  *        ____                    _____
 573  *       / ___|_                 /     \
 574  *      / |    |                /      |
 575  *      \ |    |        =>      \      |
 576  *       \|____|                 \     |
 577  *        \___|                   \____/
 578  */
 579 static int can_wrap_in_set(struct isl_map *map, int i, int j,
 580         struct isl_tab **tabs, int *ineq_i, int *ineq_j)
 581 {
 582         int changed = 0;
 583         int k, l;
 584         unsigned total = isl_basic_map_total_dim(map->p[i]);
 585         struct isl_tab_undo *snap;
 586
 587         for (k = 0; k < map->p[i]->n_ineq; ++k)
 588                 if (ineq_i[k] == STATUS_CUT)
 589                         break;
 590
 591         isl_assert(map->ctx, k < map->p[i]->n_ineq, return -1);
 592
 593         isl_int_add_ui(map->p[i]->ineq[k][0], map->p[i]->ineq[k][0], 1);
 594         for (l = 0; l < map->p[j]->n_ineq; ++l) {
 595                 if (isl_tab_is_redundant(tabs[j], map->p[j]->n_eq + l))
 596                         continue;
 597                 if (isl_seq_eq(map->p[i]->ineq[k],
 598                                 map->p[j]->ineq[l], 1 + total))
 599                         break;
 600         }
 601         isl_int_sub_ui(map->p[i]->ineq[k][0], map->p[i]->ineq[k][0], 1);
 602
 603         if (l >= map->p[j]->n_ineq)
 604                 return 0;
 605
 606         snap = isl_tab_snap(tabs[j]);
 607         tabs[j] = isl_tab_select_facet(tabs[j], map->p[j]->n_eq + l);
 608         if (isl_tab_detect_redundant(tabs[j]) < 0)
 609                 return -1;
 610
 611         changed = can_wrap_in_facet(map, i, j, k, tabs, NULL, ineq_i, NULL, ineq_j);
 612
 613         if (!changed && isl_tab_rollback(tabs[j], snap) < 0)
 614                 return -1;
 615
 616         return changed;
 617 }
 618
 619 /* Check if either i or j has a single cut constraint that can
 620  * be used to wrap in (a facet of) the other basic set.
 621  * if so, replace the pair by their union.
 622  */
 623 static int check_wrap(struct isl_map *map, int i, int j,
 624         struct isl_tab **tabs, int *ineq_i, int *ineq_j)
 625 {
 626         int changed = 0;
 627
 628         if (count(ineq_i, map->p[i]->n_ineq, STATUS_CUT) == 1)
 629                 changed = can_wrap_in_set(map, i, j, tabs, ineq_i, ineq_j);
 630         if (changed)
 631                 return changed;
 632
 633         if (count(ineq_j, map->p[j]->n_ineq, STATUS_CUT) == 1)
 634                 changed = can_wrap_in_set(map, j, i, tabs, ineq_j, ineq_i);
 635         return changed;
 636 }
 637
 638 /* At least one of the basic maps has an equality that is adjacent
 639  * to inequality.  Make sure that only one of the basic maps has
 640  * such an equality and that the other basic map has exactly one
 641  * inequality adjacent to an equality.
 642  * We call the basic map that has the inequality "i" and the basic
 643  * map that has the equality "j".
 644  * If "i" has any "cut" inequality, then relaxing the inequality
 645  * by one would not result in a basic map that contains the other
 646  * basic map.
 647  */
 648 static int check_adj_eq(struct isl_map *map, int i, int j,
 649         struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
 650 {
 651         int changed = 0;
 652         int k;
 653
 654         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ) &&
 655             any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ))
 656                 /* ADJ EQ TOO MANY */
 657                 return 0;
 658
 659         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ))
 660                 return check_adj_eq(map, j, i, tabs,
 661                                         eq_j, ineq_j, eq_i, ineq_i);
 662
 663         /* j has an equality adjacent to an inequality in i */
 664
 665         if (any(ineq_i, map->p[i]->n_ineq, STATUS_CUT))
 666                 /* ADJ EQ CUT */
 667                 return 0;
 668         if (count(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ) != 1 ||
 669             count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_EQ) != 1 ||
 670             any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_EQ) ||
 671             any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
 672             any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ))
 673                 /* ADJ EQ TOO MANY */
 674                 return 0;
 675
 676         for (k = 0; k < map->p[i]->n_ineq ; ++k)
 677                 if (ineq_i[k] == STATUS_ADJ_EQ)
 678                         break;
 679
 680         changed = is_extension(map, i, j, k, tabs, eq_i, ineq_i, eq_j, ineq_j);
 681         if (changed)
 682                 return changed;
 683
 684         changed = can_wrap_in_facet(map, i, j, k, tabs, eq_i, ineq_i, eq_j, ineq_j);
 685
 686         return changed;
 687 }
 688
 689 /* Check if the union of the given pair of basic maps
 690  * can be represented by a single basic map.
 691  * If so, replace the pair by the single basic map and return 1.
 692  * Otherwise, return 0;
 693  *
 694  * We first check the effect of each constraint of one basic map
 695  * on the other basic map.
 696  * The constraint may be
 697  *      redundant       the constraint is redundant in its own
 698  *                      basic map and should be ignore and removed
 699  *                      in the end
 700  *      valid           all (integer) points of the other basic map
 701  *                      satisfy the constraint
 702  *      separate        no (integer) point of the other basic map
 703  *                      satisfies the constraint
 704  *      cut             some but not all points of the other basic map
 705  *                      satisfy the constraint
 706  *      adj_eq          the given constraint is adjacent (on the outside)
 707  *                      to an equality of the other basic map
 708  *      adj_ineq        the given constraint is adjacent (on the outside)
 709  *                      to an inequality of the other basic map
 710  *
 711  * We consider six cases in which we can replace the pair by a single
 712  * basic map.  We ignore all "redundant" constraints.
 713  *
 714  *      1. all constraints of one basic map are valid
 715  *              => the other basic map is a subset and can be removed
 716  *
 717  *      2. all constraints of both basic maps are either "valid" or "cut"
 718  *         and the facets corresponding to the "cut" constraints
 719  *         of one of the basic maps lies entirely inside the other basic map
 720  *              => the pair can be replaced by a basic map consisting
 721  *                 of the valid constraints in both basic maps
 722  *
 723  *      3. there is a single pair of adjacent inequalities
 724  *         (all other constraints are "valid")
 725  *              => the pair can be replaced by a basic map consisting
 726  *                 of the valid constraints in both basic maps
 727  *
 728  *      4. there is a single adjacent pair of an inequality and an equality,
 729  *         the other constraints of the basic map containing the inequality are
 730  *         "valid".  Moreover, if the inequality the basic map is relaxed
 731  *         and then turned into an equality, then resulting facet lies
 732  *         entirely inside the other basic map
 733  *              => the pair can be replaced by the basic map containing
 734  *                 the inequality, with the inequality relaxed.
 735  *
 736  *      5. there is a single adjacent pair of an inequality and an equality,
 737  *         the other constraints of the basic map containing the inequality are
 738  *         "valid".  Moreover, the facets corresponding to both
 739  *         the inequality and the equality can be wrapped around their
 740  *         ridges to include the other basic map
 741  *              => the pair can be replaced by a basic map consisting
 742  *                 of the valid constraints in both basic maps together
 743  *                 with all wrapping constraints
 744  *
 745  *      6. one of the basic maps has a single cut constraint and
 746  *         the other basic map has a constraint adjacent to this constraint.
 747  *         Moreover, the facets corresponding to both constraints
 748  *         can be wrapped around their ridges to include the other basic map
 749  *              => the pair can be replaced by a basic map consisting
 750  *                 of the valid constraints in both basic maps together
 751  *                 with all wrapping constraints
 752  *
 753  * Throughout the computation, we maintain a collection of tableaus
 754  * corresponding to the basic maps.  When the basic maps are dropped
 755  * or combined, the tableaus are modified accordingly.
 756  */
 757 static int coalesce_pair(struct isl_map *map, int i, int j,
 758         struct isl_tab **tabs)
 759 {
 760         int changed = 0;
 761         int *eq_i = NULL;
 762         int *eq_j = NULL;
 763         int *ineq_i = NULL;
 764         int *ineq_j = NULL;
 765
 766         eq_i = eq_status_in(map, i, j, tabs);
 767         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ERROR))
 768                 goto error;
 769         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_SEPARATE))
 770                 goto done;
 771
 772         eq_j = eq_status_in(map, j, i, tabs);
 773         if (any(eq_j, 2 * map->p[j]->n_eq, STATUS_ERROR))
 774                 goto error;
 775         if (any(eq_j, 2 * map->p[j]->n_eq, STATUS_SEPARATE))
 776                 goto done;
 777
 778         ineq_i = ineq_status_in(map, i, j, tabs);
 779         if (any(ineq_i, map->p[i]->n_ineq, STATUS_ERROR))
 780                 goto error;
 781         if (any(ineq_i, map->p[i]->n_ineq, STATUS_SEPARATE))
 782                 goto done;
 783
 784         ineq_j = ineq_status_in(map, j, i, tabs);
 785         if (any(ineq_j, map->p[j]->n_ineq, STATUS_ERROR))
 786                 goto error;
 787         if (any(ineq_j, map->p[j]->n_ineq, STATUS_SEPARATE))
 788                 goto done;
 789
 790         if (all(eq_i, 2 * map->p[i]->n_eq, STATUS_VALID) &&
 791             all(ineq_i, map->p[i]->n_ineq, STATUS_VALID)) {
 792                 drop(map, j, tabs);
 793                 changed = 1;
 794         } else if (all(eq_j, 2 * map->p[j]->n_eq, STATUS_VALID) &&
 795                    all(ineq_j, map->p[j]->n_ineq, STATUS_VALID)) {
 796                 drop(map, i, tabs);
 797                 changed = 1;
 798         } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_CUT) ||
 799                    any(eq_j, 2 * map->p[j]->n_eq, STATUS_CUT)) {
 800                 /* BAD CUT */
 801         } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_EQ) ||
 802                    any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_EQ)) {
 803                 /* ADJ EQ PAIR */
 804         } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ) ||
 805                    any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ)) {
 806                 changed = check_adj_eq(map, i, j, tabs,
 807                                         eq_i, ineq_i, eq_j, ineq_j);
 808         } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_EQ) ||
 809                    any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_EQ)) {
 810                 /* Can't happen */
 811                 /* BAD ADJ INEQ */
 812         } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
 813                    any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ)) {
 814                 changed = check_adj_ineq(map, i, j, tabs, ineq_i, ineq_j);
 815         } else {
 816                 changed = check_facets(map, i, j, tabs, ineq_i, ineq_j);
 817                 if (!changed)
 818                         changed = check_wrap(map, i, j, tabs, ineq_i, ineq_j);
 819         }
 820
 821 done:
 822         free(eq_i);
 823         free(eq_j);
 824         free(ineq_i);
 825         free(ineq_j);
 826         return changed;
 827 error:
 828         free(eq_i);
 829         free(eq_j);
 830         free(ineq_i);
 831         free(ineq_j);
 832         return -1;
 833 }
 834
 835 static struct isl_map *coalesce(struct isl_map *map, struct isl_tab **tabs)
 836 {
 837         int i, j;
 838
 839         for (i = 0; i < map->n - 1; ++i)
 840                 for (j = i + 1; j < map->n; ++j) {
 841                         int changed;
 842                         changed = coalesce_pair(map, i, j, tabs);
 843                         if (changed < 0)
 844                                 goto error;
 845                         if (changed)
 846                                 return coalesce(map, tabs);
 847                 }
 848         return map;
 849 error:
 850         isl_map_free(map);
 851         return NULL;
 852 }
 853
 854 /* For each pair of basic maps in the map, check if the union of the two
 855  * can be represented by a single basic map.
 856  * If so, replace the pair by the single basic map and start over.
 857  */
 858 struct isl_map *isl_map_coalesce(struct isl_map *map)
 859 {
 860         int i;
 861         unsigned n;
 862         struct isl_tab **tabs = NULL;
 863
 864         if (!map)
 865                 return NULL;
 866
 867         if (map->n <= 1)
 868                 return map;
 869
 870         map = isl_map_align_divs(map);
 871
 872         tabs = isl_calloc_array(map->ctx, struct isl_tab *, map->n);
 873         if (!tabs)
 874                 goto error;
 875
 876         n = map->n;
 877         for (i = 0; i < map->n; ++i) {
 878                 tabs[i] = isl_tab_from_basic_map(map->p[i]);
 879                 if (!tabs[i])
 880                         goto error;
 881                 if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT))
 882                         tabs[i] = isl_tab_detect_implicit_equalities(tabs[i]);
 883                 if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT))
 884                         if (isl_tab_detect_redundant(tabs[i]) < 0)
 885                                 goto error;
 886         }
 887         for (i = map->n - 1; i >= 0; --i)
 888                 if (tabs[i]->empty)
 889                         drop(map, i, tabs);
 890
 891         map = coalesce(map, tabs);
 892
 893         if (map)
 894                 for (i = 0; i < map->n; ++i) {
 895                         map->p[i] = isl_basic_map_update_from_tab(map->p[i],
 896                                                                     tabs[i]);
 897                         map->p[i] = isl_basic_map_finalize(map->p[i]);
 898                         if (!map->p[i])
 899                                 goto error;
 900                         ISL_F_SET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT);
 901                         ISL_F_SET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT);
 902                 }
 903
 904         for (i = 0; i < n; ++i)
 905                 isl_tab_free(tabs[i]);
 906
 907         free(tabs);
 908
 909         return map;
 910 error:
 911         if (tabs)
 912                 for (i = 0; i < n; ++i)
 913                         isl_tab_free(tabs[i]);
 914         free(tabs);
 915         return NULL;
 916 }
 917
 918 /* For each pair of basic sets in the set, check if the union of the two
 919  * can be represented by a single basic set.
 920  * If so, replace the pair by the single basic set and start over.
 921  */
 922 struct isl_set *isl_set_coalesce(struct isl_set *set)
 923 {
 924         return (struct isl_set *)isl_map_coalesce((struct isl_map *)set);
 925 }