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