isl_constraint.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_constraint_private.h>
  15 #include <isl_dim_private.h>
  16 #include <isl_div_private.h>
  17 #include <isl/seq.h>
  18 #include <isl_aff_private.h>
  19
  20 isl_ctx *isl_constraint_get_ctx(__isl_keep isl_constraint *c)
  21 {
  22         return c ? c->ctx : NULL;
  23 }
  24
  25 static unsigned n(struct isl_constraint *c, enum isl_dim_type type)
  26 {
  27         return isl_basic_map_dim(c->bmap, type);
  28 }
  29
  30 static unsigned offset(struct isl_constraint *c, enum isl_dim_type type)
  31 {
  32         struct isl_dim *dim = c->bmap->dim;
  33         switch (type) {
  34         case isl_dim_param:     return 1;
  35         case isl_dim_in:        return 1 + dim->nparam;
  36         case isl_dim_out:       return 1 + dim->nparam + dim->n_in;
  37         case isl_dim_div:       return 1 + dim->nparam + dim->n_in + dim->n_out;
  38         default:                return 0;
  39         }
  40 }
  41
  42 static unsigned basic_map_offset(__isl_keep isl_basic_map *bmap,
  43                                                         enum isl_dim_type type)
  44 {
  45         return type == isl_dim_div ? 1 + isl_dim_total(bmap->dim)
  46                                    : 1 + isl_dim_offset(bmap->dim, type);
  47 }
  48
  49 static unsigned basic_set_offset(struct isl_basic_set *bset,
  50                                                         enum isl_dim_type type)
  51 {
  52         struct isl_dim *dim = bset->dim;
  53         switch (type) {
  54         case isl_dim_param:     return 1;
  55         case isl_dim_in:        return 1 + dim->nparam;
  56         case isl_dim_out:       return 1 + dim->nparam + dim->n_in;
  57         case isl_dim_div:       return 1 + dim->nparam + dim->n_in + dim->n_out;
  58         default:                return 0;
  59         }
  60 }
  61
  62 struct isl_constraint *isl_basic_map_constraint(struct isl_basic_map *bmap,
  63         isl_int **line)
  64 {
  65         struct isl_constraint *constraint;
  66
  67         if (!bmap || !line)
  68                 goto error;
  69
  70         constraint = isl_alloc_type(bmap->ctx, struct isl_constraint);
  71         if (!constraint)
  72                 goto error;
  73
  74         constraint->ctx = bmap->ctx;
  75         isl_ctx_ref(constraint->ctx);
  76         constraint->ref = 1;
  77         constraint->bmap = bmap;
  78         constraint->line = line;
  79
  80         return constraint;
  81 error:
  82         isl_basic_map_free(bmap);
  83         return NULL;
  84 }
  85
  86 struct isl_constraint *isl_basic_set_constraint(struct isl_basic_set *bset,
  87         isl_int **line)
  88 {
  89         return isl_basic_map_constraint((struct isl_basic_map *)bset, line);
  90 }
  91
  92 struct isl_constraint *isl_equality_alloc(struct isl_dim *dim)
  93 {
  94         struct isl_basic_map *bmap;
  95
  96         if (!dim)
  97                 return NULL;
  98
  99         bmap = isl_basic_map_alloc_dim(dim, 0, 1, 0);
 100         if (!bmap)
 101                 return NULL;
 102
 103         isl_basic_map_alloc_equality(bmap);
 104         isl_seq_clr(bmap->eq[0], 1 + isl_basic_map_total_dim(bmap));
 105         return isl_basic_map_constraint(bmap, &bmap->eq[0]);
 106 }
 107
 108 struct isl_constraint *isl_inequality_alloc(struct isl_dim *dim)
 109 {
 110         struct isl_basic_map *bmap;
 111
 112         if (!dim)
 113                 return NULL;
 114
 115         bmap = isl_basic_map_alloc_dim(dim, 0, 0, 1);
 116         if (!bmap)
 117                 return NULL;
 118
 119         isl_basic_map_alloc_inequality(bmap);
 120         isl_seq_clr(bmap->ineq[0], 1 + isl_basic_map_total_dim(bmap));
 121         return isl_basic_map_constraint(bmap, &bmap->ineq[0]);
 122 }
 123
 124 struct isl_constraint *isl_constraint_dup(struct isl_constraint *c)
 125 {
 126         struct isl_basic_map *bmap;
 127         int i;
 128         int eq;
 129
 130         if (!c)
 131                 return NULL;
 132
 133         eq = c->line < c->bmap->eq + c->bmap->n_eq;
 134         i = eq ? c->line - c->bmap->eq : c->line - c->bmap->ineq;
 135         bmap = isl_basic_map_copy(c->bmap);
 136         if (!bmap)
 137                 return NULL;
 138         return isl_basic_map_constraint(bmap, eq ? bmap->eq + i : bmap->ineq + i);
 139 }
 140
 141 struct isl_constraint *isl_constraint_cow(struct isl_constraint *c)
 142 {
 143         if (!c)
 144                 return NULL;
 145
 146         if (c->ref == 1)
 147                 return c;
 148         c->ref--;
 149         return isl_constraint_dup(c);
 150 }
 151
 152 struct isl_constraint *isl_constraint_copy(struct isl_constraint *constraint)
 153 {
 154         if (!constraint)
 155                 return NULL;
 156
 157         constraint->ref++;
 158         return constraint;
 159 }
 160
 161 void isl_constraint_free(struct isl_constraint *c)
 162 {
 163         if (!c)
 164                 return;
 165
 166         if (--c->ref > 0)
 167                 return;
 168
 169         isl_basic_map_free(c->bmap);
 170         isl_ctx_deref(c->ctx);
 171         free(c);
 172 }
 173
 174 int isl_basic_map_foreach_constraint(__isl_keep isl_basic_map *bmap,
 175         int (*fn)(__isl_take isl_constraint *c, void *user), void *user)
 176 {
 177         int i;
 178         struct isl_constraint *c;
 179
 180         if (!bmap)
 181                 return -1;
 182
 183         isl_assert(bmap->ctx, ISL_F_ISSET(bmap, ISL_BASIC_MAP_FINAL),
 184                         return -1);
 185
 186         for (i = 0; i < bmap->n_eq; ++i) {
 187                 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
 188                                                 &bmap->eq[i]);
 189                 if (!c)
 190                         return -1;
 191                 if (fn(c, user) < 0)
 192                         return -1;
 193         }
 194
 195         for (i = 0; i < bmap->n_ineq; ++i) {
 196                 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
 197                                                 &bmap->ineq[i]);
 198                 if (!c)
 199                         return -1;
 200                 if (fn(c, user) < 0)
 201                         return -1;
 202         }
 203
 204         return 0;
 205 }
 206
 207 int isl_basic_set_foreach_constraint(__isl_keep isl_basic_set *bset,
 208         int (*fn)(__isl_take isl_constraint *c, void *user), void *user)
 209 {
 210         return isl_basic_map_foreach_constraint((isl_basic_map *)bset, fn, user);
 211 }
 212
 213 int isl_constraint_is_equal(struct isl_constraint *constraint1,
 214         struct isl_constraint *constraint2)
 215 {
 216         if (!constraint1 || !constraint2)
 217                 return 0;
 218         return constraint1->bmap == constraint2->bmap &&
 219                constraint1->line == constraint2->line;
 220 }
 221
 222 struct isl_basic_map *isl_basic_map_add_constraint(
 223         struct isl_basic_map *bmap, struct isl_constraint *constraint)
 224 {
 225         if (!bmap || !constraint)
 226                 goto error;
 227
 228         isl_assert(constraint->ctx,
 229                 isl_dim_equal(bmap->dim, constraint->bmap->dim), goto error);
 230
 231         bmap = isl_basic_map_intersect(bmap,
 232                                 isl_basic_map_from_constraint(constraint));
 233         return bmap;
 234 error:
 235         isl_basic_map_free(bmap);
 236         isl_constraint_free(constraint);
 237         return NULL;
 238 }
 239
 240 struct isl_basic_set *isl_basic_set_add_constraint(
 241         struct isl_basic_set *bset, struct isl_constraint *constraint)
 242 {
 243         return (struct isl_basic_set *)
 244                 isl_basic_map_add_constraint((struct isl_basic_map *)bset,
 245                                                 constraint);
 246 }
 247
 248 __isl_give isl_map *isl_map_add_constraint(__isl_take isl_map *map,
 249         __isl_take isl_constraint *constraint)
 250 {
 251         isl_basic_map *bmap;
 252
 253         bmap = isl_basic_map_from_constraint(constraint);
 254         map = isl_map_intersect(map, isl_map_from_basic_map(bmap));
 255
 256         return map;
 257 }
 258
 259 __isl_give isl_set *isl_set_add_constraint(__isl_take isl_set *set,
 260         __isl_take isl_constraint *constraint)
 261 {
 262         return isl_map_add_constraint(set, constraint);
 263 }
 264
 265 __isl_give isl_dim *isl_constraint_get_dim(
 266         __isl_keep isl_constraint *constraint)
 267 {
 268         return constraint ? isl_basic_map_get_dim(constraint->bmap) : NULL;
 269 }
 270
 271 int isl_constraint_dim(struct isl_constraint *constraint,
 272         enum isl_dim_type type)
 273 {
 274         if (!constraint)
 275                 return -1;
 276         return n(constraint, type);
 277 }
 278
 279 int isl_constraint_involves_dims(__isl_keep isl_constraint *constraint,
 280         enum isl_dim_type type, unsigned first, unsigned n)
 281 {
 282         if (!constraint)
 283                 return -1;
 284
 285         if (first + n > isl_basic_set_dim(constraint->bmap, type))
 286                 isl_die(constraint->ctx, isl_error_invalid,
 287                         "index out of bounds", return -1);
 288
 289         first += isl_basic_map_offset(constraint->bmap, type);
 290
 291         if (isl_seq_first_non_zero(constraint->line[0] + first, n) >= 0)
 292                 return 1;
 293
 294         return 0;
 295 }
 296
 297 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint *constraint,
 298         enum isl_dim_type type, unsigned pos)
 299 {
 300         return constraint ?
 301             isl_basic_map_get_dim_name(constraint->bmap, type, pos) : NULL;
 302 }
 303
 304 void isl_constraint_get_constant(struct isl_constraint *constraint, isl_int *v)
 305 {
 306         if (!constraint)
 307                 return;
 308         isl_int_set(*v, constraint->line[0][0]);
 309 }
 310
 311 void isl_constraint_get_coefficient(struct isl_constraint *constraint,
 312         enum isl_dim_type type, int pos, isl_int *v)
 313 {
 314         if (!constraint)
 315                 return;
 316
 317         isl_assert(constraint->ctx, pos < n(constraint, type), return);
 318         isl_int_set(*v, constraint->line[0][offset(constraint, type) + pos]);
 319 }
 320
 321 struct isl_div *isl_constraint_div(struct isl_constraint *constraint, int pos)
 322 {
 323         if (!constraint)
 324                 return NULL;
 325
 326         isl_assert(constraint->ctx, pos < n(constraint, isl_dim_div),
 327                         return NULL);
 328         isl_assert(constraint->ctx,
 329                 !isl_int_is_zero(constraint->bmap->div[pos][0]), return NULL);
 330         return isl_basic_map_div(isl_basic_map_copy(constraint->bmap), pos);
 331 }
 332
 333 void isl_constraint_set_constant(struct isl_constraint *constraint, isl_int v)
 334 {
 335         if (!constraint)
 336                 return;
 337         isl_int_set(constraint->line[0][0], v);
 338 }
 339
 340 void isl_constraint_set_constant_si(__isl_keep isl_constraint *constraint,
 341         int v)
 342 {
 343         if (!constraint)
 344                 return;
 345         isl_int_set_si(constraint->line[0][0], v);
 346 }
 347
 348 void isl_constraint_set_coefficient(struct isl_constraint *constraint,
 349         enum isl_dim_type type, int pos, isl_int v)
 350 {
 351         if (!constraint)
 352                 return;
 353
 354         isl_assert(constraint->ctx, pos < n(constraint, type), return);
 355         isl_int_set(constraint->line[0][offset(constraint, type) + pos], v);
 356 }
 357
 358 void isl_constraint_set_coefficient_si(__isl_keep isl_constraint *constraint,
 359         enum isl_dim_type type, int pos, int v)
 360 {
 361         if (!constraint)
 362                 return;
 363
 364         isl_assert(constraint->ctx, pos < n(constraint, type), return);
 365         isl_int_set_si(constraint->line[0][offset(constraint, type) + pos], v);
 366 }
 367
 368
 369 /* Check whether the two basic maps have identical divs in the same order.
 370  */
 371 static int equal_divs(__isl_keep isl_basic_map *bmap1,
 372         __isl_keep isl_basic_map *bmap2)
 373 {
 374         int i;
 375         unsigned total;
 376
 377         if (!isl_basic_map_divs_known(bmap1))
 378                 return 0;
 379         if (!isl_basic_map_divs_known(bmap2))
 380                 return 0;
 381         if (bmap1->n_div != bmap2->n_div)
 382                 return 0;
 383
 384         total = isl_basic_map_total_dim(bmap1);
 385         for (i = 0; i < bmap1->n_div; ++i)
 386                 if (!isl_seq_eq(bmap1->div[i], bmap2->div[i], 2 + total))
 387                         return 0;
 388
 389         return 1;
 390 }
 391
 392 /* Drop any constraint from "bset" that is identical to "constraint".
 393  * In particular, this means that the local spaces of "bset" and
 394  * "constraint" need to be the same.
 395  *
 396  * Since the given constraint may actually be a pointer into the bset,
 397  * we have to be careful not to reorder the constraints as the user
 398  * may be holding on to other constraints from the same bset.
 399  * This should be cleaned up when the internal representation of
 400  * isl_constraint is changed to use isl_aff.
 401  */
 402 __isl_give isl_basic_set *isl_basic_set_drop_constraint(
 403         __isl_take isl_basic_set *bset, __isl_take isl_constraint *constraint)
 404 {
 405         int i;
 406         unsigned n;
 407         isl_int **row;
 408         unsigned total;
 409
 410         if (!bset || !constraint)
 411                 goto error;
 412
 413         if (!isl_dim_equal(bset->dim, constraint->bmap->dim))
 414                 isl_die(bset->ctx, isl_error_invalid,
 415                         "spaces don't match", goto error);
 416
 417         if (bset != constraint->bmap && !equal_divs(bset, constraint->bmap)) {
 418                 isl_constraint_free(constraint);
 419                 return bset;
 420         }
 421
 422         if (isl_constraint_is_equality(constraint)) {
 423                 n = bset->n_eq;
 424                 row = bset->eq;
 425         } else {
 426                 n = bset->n_ineq;
 427                 row = bset->ineq;
 428         }
 429
 430         total = isl_basic_map_total_dim(constraint->bmap);
 431         for (i = 0; i < n; ++i)
 432                 if (isl_seq_eq(row[i], constraint->line[0], 1 + total))
 433                         isl_seq_clr(row[i], 1 + total);
 434
 435         isl_constraint_free(constraint);
 436         return bset;
 437 error:
 438         isl_constraint_free(constraint);
 439         isl_basic_set_free(bset);
 440         return NULL;
 441 }
 442
 443 struct isl_constraint *isl_constraint_negate(struct isl_constraint *constraint)
 444 {
 445         unsigned total;
 446
 447         if (!constraint)
 448                 return NULL;
 449
 450         isl_assert(constraint->ctx, !isl_constraint_is_equality(constraint),
 451                         goto error);
 452         isl_assert(constraint->ctx, constraint->bmap->ref == 1, goto error);
 453         total = isl_basic_map_total_dim(constraint->bmap);
 454         isl_seq_neg(constraint->line[0], constraint->line[0], 1 + total);
 455         isl_int_sub_ui(constraint->line[0][0], constraint->line[0][0], 1);
 456         ISL_F_CLR(constraint->bmap, ISL_BASIC_MAP_NORMALIZED);
 457         return constraint;
 458 error:
 459         isl_constraint_free(constraint);
 460         return NULL;
 461 }
 462
 463 int isl_constraint_is_equality(struct isl_constraint *constraint)
 464 {
 465         if (!constraint)
 466                 return -1;
 467         return constraint->line >= constraint->bmap->eq;
 468 }
 469
 470 int isl_constraint_is_div_constraint(__isl_keep isl_constraint *constraint)
 471 {
 472         int i;
 473
 474         if (!constraint)
 475                 return -1;
 476         if (isl_constraint_is_equality(constraint))
 477                 return 0;
 478         for (i = 0; i < constraint->bmap->n_div; ++i) {
 479                 if (isl_int_is_zero(constraint->bmap->div[i][0]))
 480                         continue;
 481                 if (isl_basic_map_is_div_constraint(constraint->bmap,
 482                                         constraint->line[0], i))
 483                         return 1;
 484         }
 485
 486         return 0;
 487 }
 488
 489 /* We manually set ISL_BASIC_SET_FINAL instead of calling
 490  * isl_basic_map_finalize because we want to keep the position
 491  * of the divs and we therefore do not want to throw away redundant divs.
 492  * This is arguably a bit fragile.
 493  */
 494 __isl_give isl_basic_map *isl_basic_map_from_constraint(
 495         __isl_take isl_constraint *constraint)
 496 {
 497         int k;
 498         struct isl_basic_map *bmap;
 499         isl_int *c;
 500         unsigned total;
 501
 502         if (!constraint)
 503                 return NULL;
 504
 505         if (constraint->bmap->n_eq == 1 && constraint->bmap->n_ineq == 0) {
 506                 bmap = isl_basic_map_copy(constraint->bmap);
 507                 isl_constraint_free(constraint);
 508                 return bmap;
 509         }
 510
 511         bmap = isl_basic_map_universe_like(constraint->bmap);
 512         bmap = isl_basic_map_align_divs(bmap, constraint->bmap);
 513         bmap = isl_basic_map_cow(bmap);
 514         bmap = isl_basic_map_extend_constraints(bmap, 1, 1);
 515         if (isl_constraint_is_equality(constraint)) {
 516                 k = isl_basic_map_alloc_equality(bmap);
 517                 if (k < 0)
 518                         goto error;
 519                 c = bmap->eq[k];
 520         }
 521         else {
 522                 k = isl_basic_map_alloc_inequality(bmap);
 523                 if (k < 0)
 524                         goto error;
 525                 c = bmap->ineq[k];
 526         }
 527         total = isl_basic_map_total_dim(bmap);
 528         isl_seq_cpy(c, constraint->line[0], 1 + total);
 529         isl_constraint_free(constraint);
 530         if (bmap)
 531                 ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);
 532         return bmap;
 533 error:
 534         isl_constraint_free(constraint);
 535         isl_basic_map_free(bmap);
 536         return NULL;
 537 }
 538
 539 struct isl_basic_set *isl_basic_set_from_constraint(
 540         struct isl_constraint *constraint)
 541 {
 542         if (!constraint)
 543                 return NULL;
 544
 545         isl_assert(constraint->ctx,n(constraint, isl_dim_in) == 0, goto error);
 546         return (isl_basic_set *)isl_basic_map_from_constraint(constraint);
 547 error:
 548         isl_constraint_free(constraint);
 549         return NULL;
 550 }
 551
 552 int isl_basic_map_has_defining_equality(
 553         __isl_keep isl_basic_map *bmap, enum isl_dim_type type, int pos,
 554         __isl_give isl_constraint **c)
 555 {
 556         int i;
 557         unsigned offset;
 558         unsigned total;
 559
 560         if (!bmap)
 561                 return -1;
 562         offset = basic_map_offset(bmap, type);
 563         total = isl_basic_map_total_dim(bmap);
 564         isl_assert(bmap->ctx, pos < isl_basic_map_dim(bmap, type), return -1);
 565         for (i = 0; i < bmap->n_eq; ++i)
 566                 if (!isl_int_is_zero(bmap->eq[i][offset + pos]) &&
 567                     isl_seq_first_non_zero(bmap->eq[i]+offset+pos+1,
 568                                            1+total-offset-pos-1) == -1) {
 569                         *c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
 570                                                                 &bmap->eq[i]);
 571                         return 1;
 572                 }
 573         return 0;
 574 }
 575
 576 int isl_basic_set_has_defining_equality(
 577         __isl_keep isl_basic_set *bset, enum isl_dim_type type, int pos,
 578         __isl_give isl_constraint **c)
 579 {
 580         return isl_basic_map_has_defining_equality((isl_basic_map *)bset,
 581                                                     type, pos, c);
 582 }
 583
 584 int isl_basic_set_has_defining_inequalities(
 585         struct isl_basic_set *bset, enum isl_dim_type type, int pos,
 586         struct isl_constraint **lower,
 587         struct isl_constraint **upper)
 588 {
 589         int i, j;
 590         unsigned offset;
 591         unsigned total;
 592         isl_int m;
 593         isl_int **lower_line, **upper_line;
 594
 595         if (!bset)
 596                 return -1;
 597         offset = basic_set_offset(bset, type);
 598         total = isl_basic_set_total_dim(bset);
 599         isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type), return -1);
 600         isl_int_init(m);
 601         for (i = 0; i < bset->n_ineq; ++i) {
 602                 if (isl_int_is_zero(bset->ineq[i][offset + pos]))
 603                         continue;
 604                 if (isl_int_is_one(bset->ineq[i][offset + pos]))
 605                         continue;
 606                 if (isl_int_is_negone(bset->ineq[i][offset + pos]))
 607                         continue;
 608                 if (isl_seq_first_non_zero(bset->ineq[i]+offset+pos+1,
 609                                                 1+total-offset-pos-1) != -1)
 610                         continue;
 611                 for (j = i + 1; j < bset->n_ineq; ++j) {
 612                         if (!isl_seq_is_neg(bset->ineq[i]+1, bset->ineq[j]+1,
 613                                             total))
 614                                 continue;
 615                         isl_int_add(m, bset->ineq[i][0], bset->ineq[j][0]);
 616                         if (isl_int_abs_ge(m, bset->ineq[i][offset+pos]))
 617                                 continue;
 618
 619                         if (isl_int_is_pos(bset->ineq[i][offset+pos])) {
 620                                 lower_line = &bset->ineq[i];
 621                                 upper_line = &bset->ineq[j];
 622                         } else {
 623                                 lower_line = &bset->ineq[j];
 624                                 upper_line = &bset->ineq[i];
 625                         }
 626                         *lower = isl_basic_set_constraint(
 627                                         isl_basic_set_copy(bset), lower_line);
 628                         *upper = isl_basic_set_constraint(
 629                                         isl_basic_set_copy(bset), upper_line);
 630                         isl_int_clear(m);
 631                         return 1;
 632                 }
 633         }
 634         *lower = NULL;
 635         *upper = NULL;
 636         isl_int_clear(m);
 637         return 0;
 638 }
 639
 640 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
 641  * (in "a" and "b"), add a constraint to "bset" that ensures that the
 642  * bound implied by "a" is (strictly) larger than the bound implied by "b".
 643  *
 644  * If both constraints imply lower bounds, then this means that "a" is
 645  * active in the result.
 646  * If both constraints imply upper bounds, then this means that "b" is
 647  * active in the result.
 648  */
 649 static __isl_give isl_basic_set *add_larger_bound_constraint(
 650         __isl_take isl_basic_set *bset, isl_int *a, isl_int *b,
 651         unsigned abs_pos, int strict)
 652 {
 653         int k;
 654         isl_int t;
 655         unsigned total;
 656
 657         k = isl_basic_set_alloc_inequality(bset);
 658         if (k < 0)
 659                 goto error;
 660
 661         total = isl_basic_set_dim(bset, isl_dim_all);
 662
 663         isl_int_init(t);
 664         isl_int_neg(t, b[1 + abs_pos]);
 665
 666         isl_seq_combine(bset->ineq[k], t, a, a[1 + abs_pos], b, 1 + abs_pos);
 667         isl_seq_combine(bset->ineq[k] + 1 + abs_pos,
 668                 t, a + 1 + abs_pos + 1, a[1 + abs_pos], b + 1 + abs_pos + 1,
 669                 total - abs_pos);
 670
 671         if (strict)
 672                 isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
 673
 674         isl_int_clear(t);
 675
 676         return bset;
 677 error:
 678         isl_basic_set_free(bset);
 679         return NULL;
 680 }
 681
 682 /* Add constraints to "context" that ensure that "u" is the smallest
 683  * (and therefore active) upper bound on "abs_pos" in "bset" and return
 684  * the resulting basic set.
 685  */
 686 static __isl_give isl_basic_set *set_smallest_upper_bound(
 687         __isl_keep isl_basic_set *context,
 688         __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_upper, int u)
 689 {
 690         int j;
 691
 692         context = isl_basic_set_copy(context);
 693         context = isl_basic_set_cow(context);
 694
 695         context = isl_basic_set_extend_constraints(context, 0, n_upper - 1);
 696
 697         for (j = 0; j < bset->n_ineq; ++j) {
 698                 if (j == u)
 699                         continue;
 700                 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
 701                         continue;
 702                 context = add_larger_bound_constraint(context,
 703                         bset->ineq[j], bset->ineq[u], abs_pos, j > u);
 704         }
 705
 706         context = isl_basic_set_simplify(context);
 707         context = isl_basic_set_finalize(context);
 708
 709         return context;
 710 }
 711
 712 /* Add constraints to "context" that ensure that "u" is the largest
 713  * (and therefore active) upper bound on "abs_pos" in "bset" and return
 714  * the resulting basic set.
 715  */
 716 static __isl_give isl_basic_set *set_largest_lower_bound(
 717         __isl_keep isl_basic_set *context,
 718         __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_lower, int l)
 719 {
 720         int j;
 721
 722         context = isl_basic_set_copy(context);
 723         context = isl_basic_set_cow(context);
 724
 725         context = isl_basic_set_extend_constraints(context, 0, n_lower - 1);
 726
 727         for (j = 0; j < bset->n_ineq; ++j) {
 728                 if (j == l)
 729                         continue;
 730                 if (!isl_int_is_pos(bset->ineq[j][1 + abs_pos]))
 731                         continue;
 732                 context = add_larger_bound_constraint(context,
 733                         bset->ineq[l], bset->ineq[j], abs_pos, j > l);
 734         }
 735
 736         context = isl_basic_set_simplify(context);
 737         context = isl_basic_set_finalize(context);
 738
 739         return context;
 740 }
 741
 742 static int foreach_upper_bound(__isl_keep isl_basic_set *bset,
 743         enum isl_dim_type type, unsigned abs_pos,
 744         __isl_take isl_basic_set *context, int n_upper,
 745         int (*fn)(__isl_take isl_constraint *lower,
 746                   __isl_take isl_constraint *upper,
 747                   __isl_take isl_basic_set *bset, void *user), void *user)
 748 {
 749         isl_basic_set *context_i;
 750         isl_constraint *upper = NULL;
 751         int i;
 752
 753         for (i = 0; i < bset->n_ineq; ++i) {
 754                 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
 755                         continue;
 756
 757                 context_i = set_smallest_upper_bound(context, bset,
 758                                                         abs_pos, n_upper, i);
 759                 if (isl_basic_set_is_empty(context_i)) {
 760                         isl_basic_set_free(context_i);
 761                         continue;
 762                 }
 763                 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
 764                                                 &bset->ineq[i]);
 765                 if (!upper || !context_i)
 766                         goto error;
 767                 if (fn(NULL, upper, context_i, user) < 0)
 768                         break;
 769         }
 770
 771         isl_basic_set_free(context);
 772
 773         if (i < bset->n_ineq)
 774                 return -1;
 775
 776         return 0;
 777 error:
 778         isl_constraint_free(upper);
 779         isl_basic_set_free(context_i);
 780         isl_basic_set_free(context);
 781         return -1;
 782 }
 783
 784 static int foreach_lower_bound(__isl_keep isl_basic_set *bset,
 785         enum isl_dim_type type, unsigned abs_pos,
 786         __isl_take isl_basic_set *context, int n_lower,
 787         int (*fn)(__isl_take isl_constraint *lower,
 788                   __isl_take isl_constraint *upper,
 789                   __isl_take isl_basic_set *bset, void *user), void *user)
 790 {
 791         isl_basic_set *context_i;
 792         isl_constraint *lower = NULL;
 793         int i;
 794
 795         for (i = 0; i < bset->n_ineq; ++i) {
 796                 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
 797                         continue;
 798
 799                 context_i = set_largest_lower_bound(context, bset,
 800                                                         abs_pos, n_lower, i);
 801                 if (isl_basic_set_is_empty(context_i)) {
 802                         isl_basic_set_free(context_i);
 803                         continue;
 804                 }
 805                 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
 806                                                 &bset->ineq[i]);
 807                 if (!lower || !context_i)
 808                         goto error;
 809                 if (fn(lower, NULL, context_i, user) < 0)
 810                         break;
 811         }
 812
 813         isl_basic_set_free(context);
 814
 815         if (i < bset->n_ineq)
 816                 return -1;
 817
 818         return 0;
 819 error:
 820         isl_constraint_free(lower);
 821         isl_basic_set_free(context_i);
 822         isl_basic_set_free(context);
 823         return -1;
 824 }
 825
 826 static int foreach_bound_pair(__isl_keep isl_basic_set *bset,
 827         enum isl_dim_type type, unsigned abs_pos,
 828         __isl_take isl_basic_set *context, int n_lower, int n_upper,
 829         int (*fn)(__isl_take isl_constraint *lower,
 830                   __isl_take isl_constraint *upper,
 831                   __isl_take isl_basic_set *bset, void *user), void *user)
 832 {
 833         isl_basic_set *context_i, *context_j;
 834         isl_constraint *lower = NULL;
 835         isl_constraint *upper = NULL;
 836         int i, j;
 837
 838         for (i = 0; i < bset->n_ineq; ++i) {
 839                 if (!isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
 840                         continue;
 841
 842                 context_i = set_largest_lower_bound(context, bset,
 843                                                         abs_pos, n_lower, i);
 844                 if (isl_basic_set_is_empty(context_i)) {
 845                         isl_basic_set_free(context_i);
 846                         continue;
 847                 }
 848
 849                 for (j = 0; j < bset->n_ineq; ++j) {
 850                         if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
 851                                 continue;
 852
 853                         context_j = set_smallest_upper_bound(context_i, bset,
 854                                                             abs_pos, n_upper, j);
 855                         context_j = isl_basic_set_extend_constraints(context_j,
 856                                                                         0, 1);
 857                         context_j = add_larger_bound_constraint(context_j,
 858                                 bset->ineq[i], bset->ineq[j], abs_pos, 0);
 859                         context_j = isl_basic_set_simplify(context_j);
 860                         context_j = isl_basic_set_finalize(context_j);
 861                         if (isl_basic_set_is_empty(context_j)) {
 862                                 isl_basic_set_free(context_j);
 863                                 continue;
 864                         }
 865                         lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
 866                                                         &bset->ineq[i]);
 867                         upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
 868                                                         &bset->ineq[j]);
 869                         if (!lower || !upper || !context_j)
 870                                 goto error;
 871                         if (fn(lower, upper, context_j, user) < 0)
 872                                 break;
 873                 }
 874
 875                 isl_basic_set_free(context_i);
 876
 877                 if (j < bset->n_ineq)
 878                         break;
 879         }
 880
 881         isl_basic_set_free(context);
 882
 883         if (i < bset->n_ineq)
 884                 return -1;
 885
 886         return 0;
 887 error:
 888         isl_constraint_free(lower);
 889         isl_constraint_free(upper);
 890         isl_basic_set_free(context_i);
 891         isl_basic_set_free(context_j);
 892         isl_basic_set_free(context);
 893         return -1;
 894 }
 895
 896 /* For each pair of lower and upper bounds on the variable "pos"
 897  * of type "type", call "fn" with these lower and upper bounds and the
 898  * set of constraints on the remaining variables where these bounds
 899  * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
 900  *
 901  * If the designated variable is equal to an affine combination of the
 902  * other variables then fn is called with both lower and upper
 903  * set to the corresponding equality.
 904  *
 905  * If there is no lower (or upper) bound, then NULL is passed
 906  * as the corresponding bound.
 907  *
 908  * We first check if the variable is involved in any equality.
 909  * If not, we count the number of lower and upper bounds and
 910  * act accordingly.
 911  */
 912 int isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set *bset,
 913         enum isl_dim_type type, unsigned pos,
 914         int (*fn)(__isl_take isl_constraint *lower,
 915                   __isl_take isl_constraint *upper,
 916                   __isl_take isl_basic_set *bset, void *user), void *user)
 917 {
 918         int i;
 919         isl_constraint *lower = NULL;
 920         isl_constraint *upper = NULL;
 921         isl_basic_set *context = NULL;
 922         unsigned abs_pos;
 923         int n_lower, n_upper;
 924
 925         if (!bset)
 926                 return -1;
 927         isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type), return -1);
 928         isl_assert(bset->ctx, type == isl_dim_param || type == isl_dim_set,
 929                 return -1);
 930
 931         abs_pos = pos;
 932         if (type == isl_dim_set)
 933                 abs_pos += isl_basic_set_dim(bset, isl_dim_param);
 934
 935         for (i = 0; i < bset->n_eq; ++i) {
 936                 if (isl_int_is_zero(bset->eq[i][1 + abs_pos]))
 937                         continue;
 938
 939                 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
 940                                                 &bset->eq[i]);
 941                 upper = isl_constraint_copy(lower);
 942                 context = isl_basic_set_remove_dims(isl_basic_set_copy(bset),
 943                                         type, pos, 1);
 944                 if (!lower || !upper || !context)
 945                         goto error;
 946                 return fn(lower, upper, context, user);
 947         }
 948
 949         n_lower = 0;
 950         n_upper = 0;
 951         for (i = 0; i < bset->n_ineq; ++i) {
 952                 if (isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
 953                         n_lower++;
 954                 else if (isl_int_is_neg(bset->ineq[i][1 + abs_pos]))
 955                         n_upper++;
 956         }
 957
 958         context = isl_basic_set_copy(bset);
 959         context = isl_basic_set_cow(context);
 960         if (!context)
 961                 goto error;
 962         for (i = context->n_ineq - 1; i >= 0; --i)
 963                 if (!isl_int_is_zero(context->ineq[i][1 + abs_pos]))
 964                         isl_basic_set_drop_inequality(context, i);
 965
 966         context = isl_basic_set_drop(context, type, pos, 1);
 967         if (!n_lower && !n_upper)
 968                 return fn(NULL, NULL, context, user);
 969         if (!n_lower)
 970                 return foreach_upper_bound(bset, type, abs_pos, context, n_upper,
 971                                                 fn, user);
 972         if (!n_upper)
 973                 return foreach_lower_bound(bset, type, abs_pos, context, n_lower,
 974                                                 fn, user);
 975         return foreach_bound_pair(bset, type, abs_pos, context, n_lower, n_upper,
 976                                         fn, user);
 977 error:
 978         isl_constraint_free(lower);
 979         isl_constraint_free(upper);
 980         isl_basic_set_free(context);
 981         return -1;
 982 }
 983
 984 __isl_give isl_aff *isl_constraint_get_bound(
 985         __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
 986 {
 987         isl_aff *aff;
 988         isl_local_space *ls;
 989
 990         if (!constraint)
 991                 return NULL;
 992         if (pos >= isl_basic_set_dim(constraint->bmap, type))
 993                 isl_die(constraint->ctx, isl_error_invalid,
 994                         "index out of bounds", return NULL);
 995         if (!isl_basic_map_may_be_set(constraint->bmap))
 996                 isl_die(constraint->ctx, isl_error_invalid,
 997                         "not a set constraint", return NULL);
 998
 999         pos += offset(constraint, type);
1000         if (isl_int_is_zero(constraint->line[0][pos]))
1001                 isl_die(constraint->ctx, isl_error_invalid,
1002                         "constraint does not define a bound on given dimension",
1003                         return NULL);
1004
1005         ls = isl_basic_set_get_local_space(constraint->bmap);
1006         aff = isl_aff_alloc(ls);
1007         if (!aff)
1008                 return NULL;
1009
1010         if (isl_int_is_neg(constraint->line[0][pos]))
1011                 isl_seq_cpy(aff->v->el + 1, constraint->line[0],
1012                             aff->v->size - 1);
1013         else
1014                 isl_seq_neg(aff->v->el + 1, constraint->line[0],
1015                             aff->v->size - 1);
1016         isl_int_set_si(aff->v->el[1 + pos], 0);
1017         isl_int_abs(aff->v->el[0], constraint->line[0][pos]);
1018
1019         return aff;
1020 }
1021
1022 /* For an inequality constraint
1023  *
1024  *      f >= 0
1025  *
1026  * or an equality constraint
1027  *
1028  *      f = 0
1029  *
1030  * return the affine expression f.
1031  */
1032 __isl_give isl_aff *isl_constraint_get_aff(
1033         __isl_keep isl_constraint *constraint)
1034 {
1035         isl_aff *aff;
1036         isl_local_space *ls;
1037
1038         if (!constraint)
1039                 return NULL;
1040
1041         ls = isl_basic_set_get_local_space(constraint->bmap);
1042         aff = isl_aff_alloc(ls);
1043         if (!aff)
1044                 return NULL;
1045
1046         isl_seq_cpy(aff->v->el + 1, constraint->line[0], aff->v->size - 1);
1047         isl_int_set_si(aff->v->el[0], 1);
1048
1049         return aff;
1050 }
1051
1052 /* Construct an equality constraint equating the given affine expression
1053  * to zero.
1054  */
1055 __isl_give isl_constraint *isl_equality_from_aff(__isl_take isl_aff *aff)
1056 {
1057         int k;
1058         isl_basic_set *bset;
1059
1060         if (!aff)
1061                 return NULL;
1062
1063         bset = isl_basic_set_from_local_space(isl_aff_get_local_space(aff));
1064         bset = isl_basic_set_extend_constraints(bset, 1, 0);
1065         k = isl_basic_set_alloc_equality(bset);
1066         if (k < 0)
1067                 goto error;
1068
1069         isl_seq_cpy(bset->eq[k], aff->v->el + 1, aff->v->size - 1);
1070         isl_aff_free(aff);
1071
1072         return isl_basic_set_constraint(bset, &bset->eq[k]);
1073 error:
1074         isl_aff_free(aff);
1075         isl_basic_set_free(bset);
1076         return NULL;
1077 }
1078
1079 /* Construct an inequality constraint enforcing the given affine expression
1080  * to be non-negative.
1081  */
1082 __isl_give isl_constraint *isl_inequality_from_aff(__isl_take isl_aff *aff)
1083 {
1084         int k;
1085         isl_basic_set *bset;
1086
1087         if (!aff)
1088                 return NULL;
1089
1090         bset = isl_basic_set_from_local_space(isl_aff_get_local_space(aff));
1091         bset = isl_basic_set_extend_constraints(bset, 0, 1);
1092         k = isl_basic_set_alloc_inequality(bset);
1093         if (k < 0)
1094                 goto error;
1095
1096         isl_seq_cpy(bset->ineq[k], aff->v->el + 1, aff->v->size - 1);
1097         isl_aff_free(aff);
1098
1099         return isl_basic_set_constraint(bset, &bset->ineq[k]);
1100 error:
1101         isl_aff_free(aff);
1102         isl_basic_set_free(bset);
1103         return NULL;
1104 }