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