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