isl_local_space.c

   1 /*
   2  * Copyright 2011      INRIA Saclay
   3  * Copyright 2012      Ecole Normale Superieure
   4  *
   5  * Use of this software is governed by the MIT license
   6  *
   7  * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
   8  * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
   9  * 91893 Orsay, France
  10  * and Ecole Normale Superieure, 45 rue d’Ulm, 75230 Paris, France
  11  */
  12
  13 #include <isl_ctx_private.h>
  14 #include <isl_map_private.h>
  15 #include <isl_local_space_private.h>
  16 #include <isl_space_private.h>
  17 #include <isl_mat_private.h>
  18 #include <isl_aff_private.h>
  19 #include <isl/seq.h>
  20
  21 isl_ctx *isl_local_space_get_ctx(__isl_keep isl_local_space *ls)
  22 {
  23         return ls ? ls->dim->ctx : NULL;
  24 }
  25
  26 __isl_give isl_local_space *isl_local_space_alloc_div(__isl_take isl_space *dim,
  27         __isl_take isl_mat *div)
  28 {
  29         isl_ctx *ctx;
  30         isl_local_space *ls = NULL;
  31
  32         if (!dim || !div)
  33                 goto error;
  34
  35         ctx = isl_space_get_ctx(dim);
  36         ls = isl_calloc_type(ctx, struct isl_local_space);
  37         if (!ls)
  38                 goto error;
  39
  40         ls->ref = 1;
  41         ls->dim = dim;
  42         ls->div = div;
  43
  44         return ls;
  45 error:
  46         isl_mat_free(div);
  47         isl_space_free(dim);
  48         isl_local_space_free(ls);
  49         return NULL;
  50 }
  51
  52 __isl_give isl_local_space *isl_local_space_alloc(__isl_take isl_space *dim,
  53         unsigned n_div)
  54 {
  55         isl_ctx *ctx;
  56         isl_mat *div;
  57         unsigned total;
  58
  59         if (!dim)
  60                 return NULL;
  61
  62         total = isl_space_dim(dim, isl_dim_all);
  63
  64         ctx = isl_space_get_ctx(dim);
  65         div = isl_mat_alloc(ctx, n_div, 1 + 1 + total + n_div);
  66         return isl_local_space_alloc_div(dim, div);
  67 }
  68
  69 __isl_give isl_local_space *isl_local_space_from_space(__isl_take isl_space *dim)
  70 {
  71         return isl_local_space_alloc(dim, 0);
  72 }
  73
  74 __isl_give isl_local_space *isl_local_space_copy(__isl_keep isl_local_space *ls)
  75 {
  76         if (!ls)
  77                 return NULL;
  78
  79         ls->ref++;
  80         return ls;
  81 }
  82
  83 __isl_give isl_local_space *isl_local_space_dup(__isl_keep isl_local_space *ls)
  84 {
  85         if (!ls)
  86                 return NULL;
  87
  88         return isl_local_space_alloc_div(isl_space_copy(ls->dim),
  89                                          isl_mat_copy(ls->div));
  90
  91 }
  92
  93 __isl_give isl_local_space *isl_local_space_cow(__isl_take isl_local_space *ls)
  94 {
  95         if (!ls)
  96                 return NULL;
  97
  98         if (ls->ref == 1)
  99                 return ls;
 100         ls->ref--;
 101         return isl_local_space_dup(ls);
 102 }
 103
 104 void *isl_local_space_free(__isl_take isl_local_space *ls)
 105 {
 106         if (!ls)
 107                 return NULL;
 108
 109         if (--ls->ref > 0)
 110                 return NULL;
 111
 112         isl_space_free(ls->dim);
 113         isl_mat_free(ls->div);
 114
 115         free(ls);
 116
 117         return NULL;
 118 }
 119
 120 /* Is the local space that of a set?
 121  */
 122 int isl_local_space_is_set(__isl_keep isl_local_space *ls)
 123 {
 124         return ls ? isl_space_is_set(ls->dim) : -1;
 125 }
 126
 127 /* Return true if the two local spaces are identical, with identical
 128  * expressions for the integer divisions.
 129  */
 130 int isl_local_space_is_equal(__isl_keep isl_local_space *ls1,
 131         __isl_keep isl_local_space *ls2)
 132 {
 133         int equal;
 134
 135         if (!ls1 || !ls2)
 136                 return -1;
 137
 138         equal = isl_space_is_equal(ls1->dim, ls2->dim);
 139         if (equal < 0 || !equal)
 140                 return equal;
 141
 142         if (!isl_local_space_divs_known(ls1))
 143                 return 0;
 144         if (!isl_local_space_divs_known(ls2))
 145                 return 0;
 146
 147         return isl_mat_is_equal(ls1->div, ls2->div);
 148 }
 149
 150 int isl_local_space_dim(__isl_keep isl_local_space *ls,
 151         enum isl_dim_type type)
 152 {
 153         if (!ls)
 154                 return 0;
 155         if (type == isl_dim_div)
 156                 return ls->div->n_row;
 157         if (type == isl_dim_all)
 158                 return isl_space_dim(ls->dim, isl_dim_all) + ls->div->n_row;
 159         return isl_space_dim(ls->dim, type);
 160 }
 161
 162 unsigned isl_local_space_offset(__isl_keep isl_local_space *ls,
 163         enum isl_dim_type type)
 164 {
 165         isl_space *dim;
 166
 167         if (!ls)
 168                 return 0;
 169
 170         dim = ls->dim;
 171         switch (type) {
 172         case isl_dim_cst:       return 0;
 173         case isl_dim_param:     return 1;
 174         case isl_dim_in:        return 1 + dim->nparam;
 175         case isl_dim_out:       return 1 + dim->nparam + dim->n_in;
 176         case isl_dim_div:       return 1 + dim->nparam + dim->n_in + dim->n_out;
 177         default:                return 0;
 178         }
 179 }
 180
 181 /* Does the given dimension have a name?
 182  */
 183 int isl_local_space_has_dim_name(__isl_keep isl_local_space *ls,
 184         enum isl_dim_type type, unsigned pos)
 185 {
 186         return ls ? isl_space_has_dim_name(ls->dim, type, pos) : -1;
 187 }
 188
 189 const char *isl_local_space_get_dim_name(__isl_keep isl_local_space *ls,
 190         enum isl_dim_type type, unsigned pos)
 191 {
 192         return ls ? isl_space_get_dim_name(ls->dim, type, pos) : NULL;
 193 }
 194
 195 int isl_local_space_has_dim_id(__isl_keep isl_local_space *ls,
 196         enum isl_dim_type type, unsigned pos)
 197 {
 198         return ls ? isl_space_has_dim_id(ls->dim, type, pos) : -1;
 199 }
 200
 201 __isl_give isl_id *isl_local_space_get_dim_id(__isl_keep isl_local_space *ls,
 202         enum isl_dim_type type, unsigned pos)
 203 {
 204         return ls ? isl_space_get_dim_id(ls->dim, type, pos) : NULL;
 205 }
 206
 207 __isl_give isl_aff *isl_local_space_get_div(__isl_keep isl_local_space *ls,
 208         int pos)
 209 {
 210         isl_aff *aff;
 211
 212         if (!ls)
 213                 return NULL;
 214
 215         if (pos < 0 || pos >= ls->div->n_row)
 216                 isl_die(isl_local_space_get_ctx(ls), isl_error_invalid,
 217                         "index out of bounds", return NULL);
 218
 219         if (isl_int_is_zero(ls->div->row[pos][0]))
 220                 isl_die(isl_local_space_get_ctx(ls), isl_error_invalid,
 221                         "expression of div unknown", return NULL);
 222
 223         aff = isl_aff_alloc(isl_local_space_copy(ls));
 224         if (!aff)
 225                 return NULL;
 226         isl_seq_cpy(aff->v->el, ls->div->row[pos], aff->v->size);
 227         return aff;
 228 }
 229
 230 __isl_give isl_space *isl_local_space_get_space(__isl_keep isl_local_space *ls)
 231 {
 232         if (!ls)
 233                 return NULL;
 234
 235         return isl_space_copy(ls->dim);
 236 }
 237
 238 __isl_give isl_local_space *isl_local_space_set_dim_name(
 239         __isl_take isl_local_space *ls,
 240         enum isl_dim_type type, unsigned pos, const char *s)
 241 {
 242         ls = isl_local_space_cow(ls);
 243         if (!ls)
 244                 return NULL;
 245         ls->dim = isl_space_set_dim_name(ls->dim, type, pos, s);
 246         if (!ls->dim)
 247                 return isl_local_space_free(ls);
 248
 249         return ls;
 250 }
 251
 252 __isl_give isl_local_space *isl_local_space_set_dim_id(
 253         __isl_take isl_local_space *ls,
 254         enum isl_dim_type type, unsigned pos, __isl_take isl_id *id)
 255 {
 256         ls = isl_local_space_cow(ls);
 257         if (!ls)
 258                 return isl_id_free(id);
 259         ls->dim = isl_space_set_dim_id(ls->dim, type, pos, id);
 260         if (!ls->dim)
 261                 return isl_local_space_free(ls);
 262
 263         return ls;
 264 }
 265
 266 __isl_give isl_local_space *isl_local_space_reset_space(
 267         __isl_take isl_local_space *ls, __isl_take isl_space *dim)
 268 {
 269         ls = isl_local_space_cow(ls);
 270         if (!ls || !dim)
 271                 goto error;
 272
 273         isl_space_free(ls->dim);
 274         ls->dim = dim;
 275
 276         return ls;
 277 error:
 278         isl_local_space_free(ls);
 279         isl_space_free(dim);
 280         return NULL;
 281 }
 282
 283 /* Reorder the columns of the given div definitions according to the
 284  * given reordering.
 285  * The order of the divs themselves is assumed not to change.
 286  */
 287 static __isl_give isl_mat *reorder_divs(__isl_take isl_mat *div,
 288         __isl_take isl_reordering *r)
 289 {
 290         int i, j;
 291         isl_mat *mat;
 292         int extra;
 293
 294         if (!div || !r)
 295                 goto error;
 296
 297         extra = isl_space_dim(r->dim, isl_dim_all) + div->n_row - r->len;
 298         mat = isl_mat_alloc(div->ctx, div->n_row, div->n_col + extra);
 299         if (!mat)
 300                 goto error;
 301
 302         for (i = 0; i < div->n_row; ++i) {
 303                 isl_seq_cpy(mat->row[i], div->row[i], 2);
 304                 isl_seq_clr(mat->row[i] + 2, mat->n_col - 2);
 305                 for (j = 0; j < r->len; ++j)
 306                         isl_int_set(mat->row[i][2 + r->pos[j]],
 307                                     div->row[i][2 + j]);
 308         }
 309
 310         isl_reordering_free(r);
 311         isl_mat_free(div);
 312         return mat;
 313 error:
 314         isl_reordering_free(r);
 315         isl_mat_free(div);
 316         return NULL;
 317 }
 318
 319 /* Reorder the dimensions of "ls" according to the given reordering.
 320  * The reordering r is assumed to have been extended with the local
 321  * variables, leaving them in the same order.
 322  */
 323 __isl_give isl_local_space *isl_local_space_realign(
 324         __isl_take isl_local_space *ls, __isl_take isl_reordering *r)
 325 {
 326         ls = isl_local_space_cow(ls);
 327         if (!ls || !r)
 328                 goto error;
 329
 330         ls->div = reorder_divs(ls->div, isl_reordering_copy(r));
 331         if (!ls->div)
 332                 goto error;
 333
 334         ls = isl_local_space_reset_space(ls, isl_space_copy(r->dim));
 335
 336         isl_reordering_free(r);
 337         return ls;
 338 error:
 339         isl_local_space_free(ls);
 340         isl_reordering_free(r);
 341         return NULL;
 342 }
 343
 344 __isl_give isl_local_space *isl_local_space_add_div(
 345         __isl_take isl_local_space *ls, __isl_take isl_vec *div)
 346 {
 347         ls = isl_local_space_cow(ls);
 348         if (!ls || !div)
 349                 goto error;
 350
 351         if (ls->div->n_col != div->size)
 352                 isl_die(isl_local_space_get_ctx(ls), isl_error_invalid,
 353                         "incompatible dimensions", goto error);
 354
 355         ls->div = isl_mat_add_zero_cols(ls->div, 1);
 356         ls->div = isl_mat_add_rows(ls->div, 1);
 357         if (!ls->div)
 358                 goto error;
 359
 360         isl_seq_cpy(ls->div->row[ls->div->n_row - 1], div->el, div->size);
 361         isl_int_set_si(ls->div->row[ls->div->n_row - 1][div->size], 0);
 362
 363         isl_vec_free(div);
 364         return ls;
 365 error:
 366         isl_local_space_free(ls);
 367         isl_vec_free(div);
 368         return NULL;
 369 }
 370
 371 __isl_give isl_local_space *isl_local_space_replace_divs(
 372         __isl_take isl_local_space *ls, __isl_take isl_mat *div)
 373 {
 374         ls = isl_local_space_cow(ls);
 375
 376         if (!ls || !div)
 377                 goto error;
 378
 379         isl_mat_free(ls->div);
 380         ls->div = div;
 381         return ls;
 382 error:
 383         isl_mat_free(div);
 384         isl_local_space_free(ls);
 385         return NULL;
 386 }
 387
 388 /* Copy row "s" of "src" to row "d" of "dst", applying the expansion
 389  * defined by "exp".
 390  */
 391 static void expand_row(__isl_keep isl_mat *dst, int d,
 392         __isl_keep isl_mat *src, int s, int *exp)
 393 {
 394         int i;
 395         unsigned c = src->n_col - src->n_row;
 396
 397         isl_seq_cpy(dst->row[d], src->row[s], c);
 398         isl_seq_clr(dst->row[d] + c, dst->n_col - c);
 399
 400         for (i = 0; i < s; ++i)
 401                 isl_int_set(dst->row[d][c + exp[i]], src->row[s][c + i]);
 402 }
 403
 404 /* Compare (known) divs.
 405  * Return non-zero if at least one of the two divs is unknown.
 406  * In particular, if both divs are unknown, we respect their
 407  * current order.  Otherwise, we sort the known div after the unknown
 408  * div only if the known div depends on the unknown div.
 409  */
 410 static int cmp_row(isl_int *row_i, isl_int *row_j, int i, int j,
 411         unsigned n_row, unsigned n_col)
 412 {
 413         int li, lj;
 414         int unknown_i, unknown_j;
 415
 416         unknown_i = isl_int_is_zero(row_i[0]);
 417         unknown_j = isl_int_is_zero(row_j[0]);
 418
 419         if (unknown_i && unknown_j)
 420                 return i - j;
 421
 422         if (unknown_i)
 423                 li = n_col - n_row + i;
 424         else
 425                 li = isl_seq_last_non_zero(row_i, n_col);
 426         if (unknown_j)
 427                 lj = n_col - n_row + j;
 428         else
 429                 lj = isl_seq_last_non_zero(row_j, n_col);
 430
 431         if (li != lj)
 432                 return li - lj;
 433
 434         return isl_seq_cmp(row_i, row_j, n_col);
 435 }
 436
 437 /* Call cmp_row for divs in a matrix.
 438  */
 439 static int mat_cmp_row(__isl_keep isl_mat *div, int i, int j)
 440 {
 441         return cmp_row(div->row[i], div->row[j], i, j, div->n_row, div->n_col);
 442 }
 443
 444 /* Call cmp_row for divs in a basic map.
 445  */
 446 static int bmap_cmp_row(__isl_keep isl_basic_map *bmap, int i, int j,
 447         unsigned total)
 448 {
 449         return cmp_row(bmap->div[i], bmap->div[j], i, j, bmap->n_div, total);
 450 }
 451
 452 /* Sort the divs in "bmap".
 453  *
 454  * We first make sure divs are placed after divs on which they depend.
 455  * Then we perform a simple insertion sort based on the same ordering
 456  * that is used in isl_merge_divs.
 457  */
 458 __isl_give isl_basic_map *isl_basic_map_sort_divs(
 459         __isl_take isl_basic_map *bmap)
 460 {
 461         int i, j;
 462         unsigned total;
 463
 464         bmap = isl_basic_map_order_divs(bmap);
 465         if (!bmap)
 466                 return NULL;
 467         if (bmap->n_div <= 1)
 468                 return bmap;
 469
 470         total = 2 + isl_basic_map_total_dim(bmap);
 471         for (i = 1; i < bmap->n_div; ++i) {
 472                 for (j = i - 1; j >= 0; --j) {
 473                         if (bmap_cmp_row(bmap, j, j + 1, total) <= 0)
 474                                 break;
 475                         isl_basic_map_swap_div(bmap, j, j + 1);
 476                 }
 477         }
 478
 479         return bmap;
 480 }
 481
 482 /* Sort the divs in the basic maps of "map".
 483  */
 484 __isl_give isl_map *isl_map_sort_divs(__isl_take isl_map *map)
 485 {
 486         return isl_map_inline_foreach_basic_map(map, &isl_basic_map_sort_divs);
 487 }
 488
 489 /* Combine the two lists of divs into a single list.
 490  * For each row i in div1, exp1[i] is set to the position of the corresponding
 491  * row in the result.  Similarly for div2 and exp2.
 492  * This function guarantees
 493  *      exp1[i] >= i
 494  *      exp1[i+1] > exp1[i]
 495  * For optimal merging, the two input list should have been sorted.
 496  */
 497 __isl_give isl_mat *isl_merge_divs(__isl_keep isl_mat *div1,
 498         __isl_keep isl_mat *div2, int *exp1, int *exp2)
 499 {
 500         int i, j, k;
 501         isl_mat *div = NULL;
 502         unsigned d;
 503
 504         if (!div1 || !div2)
 505                 return NULL;
 506
 507         d = div1->n_col - div1->n_row;
 508         div = isl_mat_alloc(div1->ctx, 1 + div1->n_row + div2->n_row,
 509                                 d + div1->n_row + div2->n_row);
 510         if (!div)
 511                 return NULL;
 512
 513         for (i = 0, j = 0, k = 0; i < div1->n_row && j < div2->n_row; ++k) {
 514                 int cmp;
 515
 516                 expand_row(div, k, div1, i, exp1);
 517                 expand_row(div, k + 1, div2, j, exp2);
 518
 519                 cmp = mat_cmp_row(div, k, k + 1);
 520                 if (cmp == 0) {
 521                         exp1[i++] = k;
 522                         exp2[j++] = k;
 523                 } else if (cmp < 0) {
 524                         exp1[i++] = k;
 525                 } else {
 526                         exp2[j++] = k;
 527                         isl_seq_cpy(div->row[k], div->row[k + 1], div->n_col);
 528                 }
 529         }
 530         for (; i < div1->n_row; ++i, ++k) {
 531                 expand_row(div, k, div1, i, exp1);
 532                 exp1[i] = k;
 533         }
 534         for (; j < div2->n_row; ++j, ++k) {
 535                 expand_row(div, k, div2, j, exp2);
 536                 exp2[j] = k;
 537         }
 538
 539         div->n_row = k;
 540         div->n_col = d + k;
 541
 542         return div;
 543 }
 544
 545 /* Construct a local space that contains all the divs in either
 546  * "ls1" or "ls2".
 547  */
 548 __isl_give isl_local_space *isl_local_space_intersect(
 549         __isl_take isl_local_space *ls1, __isl_take isl_local_space *ls2)
 550 {
 551         isl_ctx *ctx;
 552         int *exp1 = NULL;
 553         int *exp2 = NULL;
 554         isl_mat *div;
 555
 556         if (!ls1 || !ls2)
 557                 goto error;
 558
 559         ctx = isl_local_space_get_ctx(ls1);
 560         if (!isl_space_is_equal(ls1->dim, ls2->dim))
 561                 isl_die(ctx, isl_error_invalid,
 562                         "spaces should be identical", goto error);
 563
 564         if (ls2->div->n_row == 0) {
 565                 isl_local_space_free(ls2);
 566                 return ls1;
 567         }
 568
 569         if (ls1->div->n_row == 0) {
 570                 isl_local_space_free(ls1);
 571                 return ls2;
 572         }
 573
 574         exp1 = isl_alloc_array(ctx, int, ls1->div->n_row);
 575         exp2 = isl_alloc_array(ctx, int, ls2->div->n_row);
 576         if (!exp1 || !exp2)
 577                 goto error;
 578
 579         div = isl_merge_divs(ls1->div, ls2->div, exp1, exp2);
 580         if (!div)
 581                 goto error;
 582
 583         free(exp1);
 584         free(exp2);
 585         isl_local_space_free(ls2);
 586         isl_mat_free(ls1->div);
 587         ls1->div = div;
 588
 589         return ls1;
 590 error:
 591         free(exp1);
 592         free(exp2);
 593         isl_local_space_free(ls1);
 594         isl_local_space_free(ls2);
 595         return NULL;
 596 }
 597
 598 int isl_local_space_divs_known(__isl_keep isl_local_space *ls)
 599 {
 600         int i;
 601
 602         if (!ls)
 603                 return -1;
 604
 605         for (i = 0; i < ls->div->n_row; ++i)
 606                 if (isl_int_is_zero(ls->div->row[i][0]))
 607                         return 0;
 608
 609         return 1;
 610 }
 611
 612 __isl_give isl_local_space *isl_local_space_domain(
 613         __isl_take isl_local_space *ls)
 614 {
 615         ls = isl_local_space_drop_dims(ls, isl_dim_out,
 616                                         0, isl_local_space_dim(ls, isl_dim_out));
 617         ls = isl_local_space_cow(ls);
 618         if (!ls)
 619                 return NULL;
 620         ls->dim = isl_space_domain(ls->dim);
 621         if (!ls->dim)
 622                 return isl_local_space_free(ls);
 623         return ls;
 624 }
 625
 626 __isl_give isl_local_space *isl_local_space_range(
 627         __isl_take isl_local_space *ls)
 628 {
 629         ls = isl_local_space_drop_dims(ls, isl_dim_in,
 630                                         0, isl_local_space_dim(ls, isl_dim_in));
 631         ls = isl_local_space_cow(ls);
 632         if (!ls)
 633                 return NULL;
 634
 635         ls->dim = isl_space_range(ls->dim);
 636         if (!ls->dim)
 637                 return isl_local_space_free(ls);
 638         return ls;
 639 }
 640
 641 /* Construct a local space for a map that has the given local
 642  * space as domain and that has a zero-dimensional range.
 643  */
 644 __isl_give isl_local_space *isl_local_space_from_domain(
 645         __isl_take isl_local_space *ls)
 646 {
 647         ls = isl_local_space_cow(ls);
 648         if (!ls)
 649                 return NULL;
 650         ls->dim = isl_space_from_domain(ls->dim);
 651         if (!ls->dim)
 652                 return isl_local_space_free(ls);
 653         return ls;
 654 }
 655
 656 __isl_give isl_local_space *isl_local_space_add_dims(
 657         __isl_take isl_local_space *ls, enum isl_dim_type type, unsigned n)
 658 {
 659         int pos;
 660
 661         if (!ls)
 662                 return NULL;
 663         pos = isl_local_space_dim(ls, type);
 664         return isl_local_space_insert_dims(ls, type, pos, n);
 665 }
 666
 667 /* Remove common factor of non-constant terms and denominator.
 668  */
 669 static void normalize_div(__isl_keep isl_local_space *ls, int div)
 670 {
 671         isl_ctx *ctx = ls->div->ctx;
 672         unsigned total = ls->div->n_col - 2;
 673
 674         isl_seq_gcd(ls->div->row[div] + 2, total, &ctx->normalize_gcd);
 675         isl_int_gcd(ctx->normalize_gcd,
 676                     ctx->normalize_gcd, ls->div->row[div][0]);
 677         if (isl_int_is_one(ctx->normalize_gcd))
 678                 return;
 679
 680         isl_seq_scale_down(ls->div->row[div] + 2, ls->div->row[div] + 2,
 681                             ctx->normalize_gcd, total);
 682         isl_int_divexact(ls->div->row[div][0], ls->div->row[div][0],
 683                             ctx->normalize_gcd);
 684         isl_int_fdiv_q(ls->div->row[div][1], ls->div->row[div][1],
 685                             ctx->normalize_gcd);
 686 }
 687
 688 /* Exploit the equalities in "eq" to simplify the expressions of
 689  * the integer divisions in "ls".
 690  * The integer divisions in "ls" are assumed to appear as regular
 691  * dimensions in "eq".
 692  */
 693 __isl_give isl_local_space *isl_local_space_substitute_equalities(
 694         __isl_take isl_local_space *ls, __isl_take isl_basic_set *eq)
 695 {
 696         int i, j, k;
 697         unsigned total;
 698         unsigned n_div;
 699
 700         ls = isl_local_space_cow(ls);
 701         if (!ls || !eq)
 702                 goto error;
 703
 704         total = isl_space_dim(eq->dim, isl_dim_all);
 705         if (isl_local_space_dim(ls, isl_dim_all) != total)
 706                 isl_die(isl_local_space_get_ctx(ls), isl_error_invalid,
 707                         "dimensions don't match", goto error);
 708         total++;
 709         n_div = eq->n_div;
 710         for (i = 0; i < eq->n_eq; ++i) {
 711                 j = isl_seq_last_non_zero(eq->eq[i], total + n_div);
 712                 if (j < 0 || j == 0 || j >= total)
 713                         continue;
 714
 715                 for (k = 0; k < ls->div->n_row; ++k) {
 716                         if (isl_int_is_zero(ls->div->row[k][1 + j]))
 717                                 continue;
 718                         isl_seq_elim(ls->div->row[k] + 1, eq->eq[i], j, total,
 719                                         &ls->div->row[k][0]);
 720                         normalize_div(ls, k);
 721                 }
 722         }
 723
 724         isl_basic_set_free(eq);
 725         return ls;
 726 error:
 727         isl_basic_set_free(eq);
 728         isl_local_space_free(ls);
 729         return NULL;
 730 }
 731
 732 /* Plug in "subs" for dimension "type", "pos" in the integer divisions
 733  * of "ls".
 734  *
 735  * Let i be the dimension to replace and let "subs" be of the form
 736  *
 737  *      f/d
 738  *
 739  * Any integer division with a non-zero coefficient for i,
 740  *
 741  *      floor((a i + g)/m)
 742  *
 743  * is replaced by
 744  *
 745  *      floor((a f + d g)/(m d))
 746  */
 747 __isl_give isl_local_space *isl_local_space_substitute(
 748         __isl_take isl_local_space *ls,
 749         enum isl_dim_type type, unsigned pos, __isl_keep isl_aff *subs)
 750 {
 751         int i;
 752         isl_int v;
 753
 754         ls = isl_local_space_cow(ls);
 755         if (!ls || !subs)
 756                 return isl_local_space_free(ls);
 757
 758         if (!isl_space_is_equal(ls->dim, subs->ls->dim))
 759                 isl_die(isl_local_space_get_ctx(ls), isl_error_invalid,
 760                         "spaces don't match", return isl_local_space_free(ls));
 761         if (isl_local_space_dim(subs->ls, isl_dim_div) != 0)
 762                 isl_die(isl_local_space_get_ctx(ls), isl_error_unsupported,
 763                         "cannot handle divs yet",
 764                         return isl_local_space_free(ls));
 765
 766         pos += isl_local_space_offset(ls, type);
 767
 768         isl_int_init(v);
 769         for (i = 0; i < ls->div->n_row; ++i) {
 770                 if (isl_int_is_zero(ls->div->row[i][1 + pos]))
 771                         continue;
 772                 isl_int_set(v, ls->div->row[i][1 + pos]);
 773                 isl_int_set_si(ls->div->row[i][1 + pos], 0);
 774                 isl_seq_combine(ls->div->row[i] + 1,
 775                                 subs->v->el[0], ls->div->row[i] + 1,
 776                                 v, subs->v->el + 1, subs->v->size - 1);
 777                 isl_int_mul(ls->div->row[i][0],
 778                             ls->div->row[i][0], subs->v->el[0]);
 779                 normalize_div(ls, i);
 780         }
 781         isl_int_clear(v);
 782
 783         return ls;
 784 }
 785
 786 int isl_local_space_is_named_or_nested(__isl_keep isl_local_space *ls,
 787         enum isl_dim_type type)
 788 {
 789         if (!ls)
 790                 return -1;
 791         return isl_space_is_named_or_nested(ls->dim, type);
 792 }
 793
 794 __isl_give isl_local_space *isl_local_space_drop_dims(
 795         __isl_take isl_local_space *ls,
 796         enum isl_dim_type type, unsigned first, unsigned n)
 797 {
 798         isl_ctx *ctx;
 799
 800         if (!ls)
 801                 return NULL;
 802         if (n == 0 && !isl_local_space_is_named_or_nested(ls, type))
 803                 return ls;
 804
 805         ctx = isl_local_space_get_ctx(ls);
 806         if (first + n > isl_local_space_dim(ls, type))
 807                 isl_die(ctx, isl_error_invalid, "range out of bounds",
 808                         return isl_local_space_free(ls));
 809
 810         ls = isl_local_space_cow(ls);
 811         if (!ls)
 812                 return NULL;
 813
 814         if (type == isl_dim_div) {
 815                 ls->div = isl_mat_drop_rows(ls->div, first, n);
 816         } else {
 817                 ls->dim = isl_space_drop_dims(ls->dim, type, first, n);
 818                 if (!ls->dim)
 819                         return isl_local_space_free(ls);
 820         }
 821
 822         first += 1 + isl_local_space_offset(ls, type);
 823         ls->div = isl_mat_drop_cols(ls->div, first, n);
 824         if (!ls->div)
 825                 return isl_local_space_free(ls);
 826
 827         return ls;
 828 }
 829
 830 __isl_give isl_local_space *isl_local_space_insert_dims(
 831         __isl_take isl_local_space *ls,
 832         enum isl_dim_type type, unsigned first, unsigned n)
 833 {
 834         isl_ctx *ctx;
 835
 836         if (!ls)
 837                 return NULL;
 838         if (n == 0 && !isl_local_space_is_named_or_nested(ls, type))
 839                 return ls;
 840
 841         ctx = isl_local_space_get_ctx(ls);
 842         if (first > isl_local_space_dim(ls, type))
 843                 isl_die(ctx, isl_error_invalid, "position out of bounds",
 844                         return isl_local_space_free(ls));
 845
 846         ls = isl_local_space_cow(ls);
 847         if (!ls)
 848                 return NULL;
 849
 850         if (type == isl_dim_div) {
 851                 ls->div = isl_mat_insert_zero_rows(ls->div, first, n);
 852         } else {
 853                 ls->dim = isl_space_insert_dims(ls->dim, type, first, n);
 854                 if (!ls->dim)
 855                         return isl_local_space_free(ls);
 856         }
 857
 858         first += 1 + isl_local_space_offset(ls, type);
 859         ls->div = isl_mat_insert_zero_cols(ls->div, first, n);
 860         if (!ls->div)
 861                 return isl_local_space_free(ls);
 862
 863         return ls;
 864 }
 865
 866 /* Check if the constraints pointed to by "constraint" is a div
 867  * constraint corresponding to div "div" in "ls".
 868  *
 869  * That is, if div = floor(f/m), then check if the constraint is
 870  *
 871  *              f - m d >= 0
 872  * or
 873  *              -(f-(m-1)) + m d >= 0
 874  */
 875 int isl_local_space_is_div_constraint(__isl_keep isl_local_space *ls,
 876         isl_int *constraint, unsigned div)
 877 {
 878         unsigned pos;
 879
 880         if (!ls)
 881                 return -1;
 882
 883         if (isl_int_is_zero(ls->div->row[div][0]))
 884                 return 0;
 885
 886         pos = isl_local_space_offset(ls, isl_dim_div) + div;
 887
 888         if (isl_int_eq(constraint[pos], ls->div->row[div][0])) {
 889                 int neg;
 890                 isl_int_sub(ls->div->row[div][1],
 891                                 ls->div->row[div][1], ls->div->row[div][0]);
 892                 isl_int_add_ui(ls->div->row[div][1], ls->div->row[div][1], 1);
 893                 neg = isl_seq_is_neg(constraint, ls->div->row[div]+1, pos);
 894                 isl_int_sub_ui(ls->div->row[div][1], ls->div->row[div][1], 1);
 895                 isl_int_add(ls->div->row[div][1],
 896                                 ls->div->row[div][1], ls->div->row[div][0]);
 897                 if (!neg)
 898                         return 0;
 899                 if (isl_seq_first_non_zero(constraint+pos+1,
 900                                             ls->div->n_row-div-1) != -1)
 901                         return 0;
 902         } else if (isl_int_abs_eq(constraint[pos], ls->div->row[div][0])) {
 903                 if (!isl_seq_eq(constraint, ls->div->row[div]+1, pos))
 904                         return 0;
 905                 if (isl_seq_first_non_zero(constraint+pos+1,
 906                                             ls->div->n_row-div-1) != -1)
 907                         return 0;
 908         } else
 909                 return 0;
 910
 911         return 1;
 912 }
 913
 914 /*
 915  * Set active[i] to 1 if the dimension at position i is involved
 916  * in the linear expression l.
 917  */
 918 int *isl_local_space_get_active(__isl_keep isl_local_space *ls, isl_int *l)
 919 {
 920         int i, j;
 921         isl_ctx *ctx;
 922         int *active = NULL;
 923         unsigned total;
 924         unsigned offset;
 925
 926         ctx = isl_local_space_get_ctx(ls);
 927         total = isl_local_space_dim(ls, isl_dim_all);
 928         active = isl_calloc_array(ctx, int, total);
 929         if (!active)
 930                 return NULL;
 931
 932         for (i = 0; i < total; ++i)
 933                 active[i] = !isl_int_is_zero(l[i]);
 934
 935         offset = isl_local_space_offset(ls, isl_dim_div) - 1;
 936         for (i = ls->div->n_row - 1; i >= 0; --i) {
 937                 if (!active[offset + i])
 938                         continue;
 939                 for (j = 0; j < total; ++j)
 940                         active[j] |= !isl_int_is_zero(ls->div->row[i][2 + j]);
 941         }
 942
 943         return active;
 944 }
 945
 946 /* Given a local space "ls" of a set, create a local space
 947  * for the lift of the set.  In particular, the result
 948  * is of the form [dim -> local[..]], with ls->div->n_row variables in the
 949  * range of the wrapped map.
 950  */
 951 __isl_give isl_local_space *isl_local_space_lift(
 952         __isl_take isl_local_space *ls)
 953 {
 954         ls = isl_local_space_cow(ls);
 955         if (!ls)
 956                 return NULL;
 957
 958         ls->dim = isl_space_lift(ls->dim, ls->div->n_row);
 959         ls->div = isl_mat_drop_rows(ls->div, 0, ls->div->n_row);
 960         if (!ls->dim || !ls->div)
 961                 return isl_local_space_free(ls);
 962
 963         return ls;
 964 }
 965
 966 /* Construct a basic map that maps a set living in local space "ls"
 967  * to the corresponding lifted local space.
 968  */
 969 __isl_give isl_basic_map *isl_local_space_lifting(
 970         __isl_take isl_local_space *ls)
 971 {
 972         isl_basic_map *lifting;
 973         isl_basic_set *bset;
 974
 975         if (!ls)
 976                 return NULL;
 977         if (!isl_local_space_is_set(ls))
 978                 isl_die(isl_local_space_get_ctx(ls), isl_error_invalid,
 979                         "lifting only defined on set spaces",
 980                         return isl_local_space_free(ls));
 981
 982         bset = isl_basic_set_from_local_space(ls);
 983         lifting = isl_basic_set_unwrap(isl_basic_set_lift(bset));
 984         lifting = isl_basic_map_domain_map(lifting);
 985         lifting = isl_basic_map_reverse(lifting);
 986
 987         return lifting;
 988 }