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_seq_eq(map->p[i]->ineq[k],
 596                                 map->p[j]->ineq[l], 1 + total))
 597                         break;
 598         isl_int_sub_ui(map->p[i]->ineq[k][0], map->p[i]->ineq[k][0], 1);
 599
 600         if (l >= map->p[j]->n_ineq)
 601                 return 0;
 602
 603         snap = isl_tab_snap(tabs[j]);
 604         tabs[j] = isl_tab_select_facet(tabs[j], map->p[j]->n_eq + l);
 605         if (isl_tab_detect_redundant(tabs[j]) < 0)
 606                 return -1;
 607
 608         changed = can_wrap_in_facet(map, i, j, k, tabs, NULL, ineq_i, NULL, ineq_j);
 609
 610         if (!changed && isl_tab_rollback(tabs[j], snap) < 0)
 611                 return -1;
 612
 613         return changed;
 614 }
 615
 616 /* Check if either i or j has a single cut constraint that can
 617  * be used to wrap in (a facet of) the other basic set.
 618  * if so, replace the pair by their union.
 619  */
 620 static int check_wrap(struct isl_map *map, int i, int j,
 621         struct isl_tab **tabs, int *ineq_i, int *ineq_j)
 622 {
 623         int changed = 0;
 624
 625         if (count(ineq_i, map->p[i]->n_ineq, STATUS_CUT) == 1)
 626                 changed = can_wrap_in_set(map, i, j, tabs, ineq_i, ineq_j);
 627         if (changed)
 628                 return changed;
 629
 630         if (count(ineq_j, map->p[j]->n_ineq, STATUS_CUT) == 1)
 631                 changed = can_wrap_in_set(map, j, i, tabs, ineq_j, ineq_i);
 632         return changed;
 633 }
 634
 635 /* At least one of the basic maps has an equality that is adjacent
 636  * to inequality.  Make sure that only one of the basic maps has
 637  * such an equality and that the other basic map has exactly one
 638  * inequality adjacent to an equality.
 639  * We call the basic map that has the inequality "i" and the basic
 640  * map that has the equality "j".
 641  * If "i" has any "cut" inequality, then relaxing the inequality
 642  * by one would not result in a basic map that contains the other
 643  * basic map.
 644  */
 645 static int check_adj_eq(struct isl_map *map, int i, int j,
 646         struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
 647 {
 648         int changed = 0;
 649         int k;
 650
 651         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ) &&
 652             any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ))
 653                 /* ADJ EQ TOO MANY */
 654                 return 0;
 655
 656         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ))
 657                 return check_adj_eq(map, j, i, tabs,
 658                                         eq_j, ineq_j, eq_i, ineq_i);
 659
 660         /* j has an equality adjacent to an inequality in i */
 661
 662         if (any(ineq_i, map->p[i]->n_ineq, STATUS_CUT))
 663                 /* ADJ EQ CUT */
 664                 return 0;
 665         if (count(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ) != 1 ||
 666             count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_EQ) != 1 ||
 667             any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_EQ) ||
 668             any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
 669             any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ))
 670                 /* ADJ EQ TOO MANY */
 671                 return 0;
 672
 673         for (k = 0; k < map->p[i]->n_ineq ; ++k)
 674                 if (ineq_i[k] == STATUS_ADJ_EQ)
 675                         break;
 676
 677         changed = is_extension(map, i, j, k, tabs, eq_i, ineq_i, eq_j, ineq_j);
 678         if (changed)
 679                 return changed;
 680
 681         changed = can_wrap_in_facet(map, i, j, k, tabs, eq_i, ineq_i, eq_j, ineq_j);
 682
 683         return changed;
 684 }
 685
 686 /* Check if the union of the given pair of basic maps
 687  * can be represented by a single basic map.
 688  * If so, replace the pair by the single basic map and return 1.
 689  * Otherwise, return 0;
 690  *
 691  * We first check the effect of each constraint of one basic map
 692  * on the other basic map.
 693  * The constraint may be
 694  *      redundant       the constraint is redundant in its own
 695  *                      basic map and should be ignore and removed
 696  *                      in the end
 697  *      valid           all (integer) points of the other basic map
 698  *                      satisfy the constraint
 699  *      separate        no (integer) point of the other basic map
 700  *                      satisfies the constraint
 701  *      cut             some but not all points of the other basic map
 702  *                      satisfy the constraint
 703  *      adj_eq          the given constraint is adjacent (on the outside)
 704  *                      to an equality of the other basic map
 705  *      adj_ineq        the given constraint is adjacent (on the outside)
 706  *                      to an inequality of the other basic map
 707  *
 708  * We consider six cases in which we can replace the pair by a single
 709  * basic map.  We ignore all "redundant" constraints.
 710  *
 711  *      1. all constraints of one basic map are valid
 712  *              => the other basic map is a subset and can be removed
 713  *
 714  *      2. all constraints of both basic maps are either "valid" or "cut"
 715  *         and the facets corresponding to the "cut" constraints
 716  *         of one of the basic maps lies entirely inside the other basic map
 717  *              => the pair can be replaced by a basic map consisting
 718  *                 of the valid constraints in both basic maps
 719  *
 720  *      3. there is a single pair of adjacent inequalities
 721  *         (all other constraints are "valid")
 722  *              => the pair can be replaced by a basic map consisting
 723  *                 of the valid constraints in both basic maps
 724  *
 725  *      4. there is a single adjacent pair of an inequality and an equality,
 726  *         the other constraints of the basic map containing the inequality are
 727  *         "valid".  Moreover, if the inequality the basic map is relaxed
 728  *         and then turned into an equality, then resulting facet lies
 729  *         entirely inside the other basic map
 730  *              => the pair can be replaced by the basic map containing
 731  *                 the inequality, with the inequality relaxed.
 732  *
 733  *      5. there is a single adjacent pair of an inequality and an equality,
 734  *         the other constraints of the basic map containing the inequality are
 735  *         "valid".  Moreover, the facets corresponding to both
 736  *         the inequality and the equality can be wrapped around their
 737  *         ridges to include the other basic map
 738  *              => the pair can be replaced by a basic map consisting
 739  *                 of the valid constraints in both basic maps together
 740  *                 with all wrapping constraints
 741  *
 742  *      6. one of the basic maps has a single cut constraint and
 743  *         the other basic map has a constraint adjacent to this constraint.
 744  *         Moreover, the facets corresponding to both constraints
 745  *         can be wrapped around their ridges to include the other basic map
 746  *              => the pair can be replaced by a basic map consisting
 747  *                 of the valid constraints in both basic maps together
 748  *                 with all wrapping constraints
 749  *
 750  * Throughout the computation, we maintain a collection of tableaus
 751  * corresponding to the basic maps.  When the basic maps are dropped
 752  * or combined, the tableaus are modified accordingly.
 753  */
 754 static int coalesce_pair(struct isl_map *map, int i, int j,
 755         struct isl_tab **tabs)
 756 {
 757         int changed = 0;
 758         int *eq_i = NULL;
 759         int *eq_j = NULL;
 760         int *ineq_i = NULL;
 761         int *ineq_j = NULL;
 762
 763         eq_i = eq_status_in(map, i, j, tabs);
 764         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ERROR))
 765                 goto error;
 766         if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_SEPARATE))
 767                 goto done;
 768
 769         eq_j = eq_status_in(map, j, i, tabs);
 770         if (any(eq_j, 2 * map->p[j]->n_eq, STATUS_ERROR))
 771                 goto error;
 772         if (any(eq_j, 2 * map->p[j]->n_eq, STATUS_SEPARATE))
 773                 goto done;
 774
 775         ineq_i = ineq_status_in(map, i, j, tabs);
 776         if (any(ineq_i, map->p[i]->n_ineq, STATUS_ERROR))
 777                 goto error;
 778         if (any(ineq_i, map->p[i]->n_ineq, STATUS_SEPARATE))
 779                 goto done;
 780
 781         ineq_j = ineq_status_in(map, j, i, tabs);
 782         if (any(ineq_j, map->p[j]->n_ineq, STATUS_ERROR))
 783                 goto error;
 784         if (any(ineq_j, map->p[j]->n_ineq, STATUS_SEPARATE))
 785                 goto done;
 786
 787         if (all(eq_i, 2 * map->p[i]->n_eq, STATUS_VALID) &&
 788             all(ineq_i, map->p[i]->n_ineq, STATUS_VALID)) {
 789                 drop(map, j, tabs);
 790                 changed = 1;
 791         } else if (all(eq_j, 2 * map->p[j]->n_eq, STATUS_VALID) &&
 792                    all(ineq_j, map->p[j]->n_ineq, STATUS_VALID)) {
 793                 drop(map, i, tabs);
 794                 changed = 1;
 795         } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_CUT) ||
 796                    any(eq_j, 2 * map->p[j]->n_eq, STATUS_CUT)) {
 797                 /* BAD CUT */
 798         } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_EQ) ||
 799                    any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_EQ)) {
 800                 /* ADJ EQ PAIR */
 801         } else if (any(eq_i, 2 * map->p[i]->n_eq, STATUS_ADJ_INEQ) ||
 802                    any(eq_j, 2 * map->p[j]->n_eq, STATUS_ADJ_INEQ)) {
 803                 changed = check_adj_eq(map, i, j, tabs,
 804                                         eq_i, ineq_i, eq_j, ineq_j);
 805         } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_EQ) ||
 806                    any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_EQ)) {
 807                 /* Can't happen */
 808                 /* BAD ADJ INEQ */
 809         } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
 810                    any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ)) {
 811                 changed = check_adj_ineq(map, i, j, tabs, ineq_i, ineq_j);
 812         } else {
 813                 changed = check_facets(map, i, j, tabs, ineq_i, ineq_j);
 814                 if (!changed)
 815                         changed = check_wrap(map, i, j, tabs, ineq_i, ineq_j);
 816         }
 817
 818 done:
 819         free(eq_i);
 820         free(eq_j);
 821         free(ineq_i);
 822         free(ineq_j);
 823         return changed;
 824 error:
 825         free(eq_i);
 826         free(eq_j);
 827         free(ineq_i);
 828         free(ineq_j);
 829         return -1;
 830 }
 831
 832 static struct isl_map *coalesce(struct isl_map *map, struct isl_tab **tabs)
 833 {
 834         int i, j;
 835
 836         for (i = 0; i < map->n - 1; ++i)
 837                 for (j = i + 1; j < map->n; ++j) {
 838                         int changed;
 839                         changed = coalesce_pair(map, i, j, tabs);
 840                         if (changed < 0)
 841                                 goto error;
 842                         if (changed)
 843                                 return coalesce(map, tabs);
 844                 }
 845         return map;
 846 error:
 847         isl_map_free(map);
 848         return NULL;
 849 }
 850
 851 /* For each pair of basic maps in the map, check if the union of the two
 852  * can be represented by a single basic map.
 853  * If so, replace the pair by the single basic map and start over.
 854  */
 855 struct isl_map *isl_map_coalesce(struct isl_map *map)
 856 {
 857         int i;
 858         unsigned n;
 859         struct isl_tab **tabs = NULL;
 860
 861         if (!map)
 862                 return NULL;
 863
 864         if (map->n <= 1)
 865                 return map;
 866
 867         map = isl_map_align_divs(map);
 868
 869         tabs = isl_calloc_array(map->ctx, struct isl_tab *, map->n);
 870         if (!tabs)
 871                 goto error;
 872
 873         n = map->n;
 874         for (i = 0; i < map->n; ++i) {
 875                 tabs[i] = isl_tab_from_basic_map(map->p[i]);
 876                 if (!tabs[i])
 877                         goto error;
 878                 if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT))
 879                         tabs[i] = isl_tab_detect_implicit_equalities(tabs[i]);
 880                 if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT))
 881                         if (isl_tab_detect_redundant(tabs[i]) < 0)
 882                                 goto error;
 883         }
 884         for (i = map->n - 1; i >= 0; --i)
 885                 if (tabs[i]->empty)
 886                         drop(map, i, tabs);
 887
 888         map = coalesce(map, tabs);
 889
 890         if (map)
 891                 for (i = 0; i < map->n; ++i) {
 892                         map->p[i] = isl_basic_map_update_from_tab(map->p[i],
 893                                                                     tabs[i]);
 894                         map->p[i] = isl_basic_map_finalize(map->p[i]);
 895                         if (!map->p[i])
 896                                 goto error;
 897                         ISL_F_SET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT);
 898                         ISL_F_SET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT);
 899                 }
 900
 901         for (i = 0; i < n; ++i)
 902                 isl_tab_free(tabs[i]);
 903
 904         free(tabs);
 905
 906         return map;
 907 error:
 908         if (tabs)
 909                 for (i = 0; i < n; ++i)
 910                         isl_tab_free(tabs[i]);
 911         free(tabs);
 912         return NULL;
 913 }
 914
 915 /* For each pair of basic sets in the set, check if the union of the two
 916  * can be represented by a single basic set.
 917  * If so, replace the pair by the single basic set and start over.
 918  */
 919 struct isl_set *isl_set_coalesce(struct isl_set *set)
 920 {
 921         return (struct isl_set *)isl_map_coalesce((struct isl_map *)set);
 922 }