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 /* Check whether the two basic maps have identical divs in the same order.
 447  */
 448 static int equal_divs(__isl_keep isl_basic_map *bmap1,
 449         __isl_keep isl_basic_map *bmap2)
 450 {
 451         int i;
 452         unsigned total;
 453
 454         if (!isl_basic_map_divs_known(bmap1))
 455                 return 0;
 456         if (!isl_basic_map_divs_known(bmap2))
 457                 return 0;
 458         if (bmap1->n_div != bmap2->n_div)
 459                 return 0;
 460
 461         total = isl_basic_map_total_dim(bmap1);
 462         for (i = 0; i < bmap1->n_div; ++i)
 463                 if (!isl_seq_eq(bmap1->div[i], bmap2->div[i], 2 + total))
 464                         return 0;
 465
 466         return 1;
 467 }
 468
 469 /* Drop any constraint from "bset" that is identical to "constraint".
 470  * In particular, this means that the local spaces of "bset" and
 471  * "constraint" need to be the same.
 472  *
 473  * Since the given constraint may actually be a pointer into the bset,
 474  * we have to be careful not to reorder the constraints as the user
 475  * may be holding on to other constraints from the same bset.
 476  * This should be cleaned up when the internal representation of
 477  * isl_constraint is changed to use isl_aff.
 478  */
 479 __isl_give isl_basic_set *isl_basic_set_drop_constraint(
 480         __isl_take isl_basic_set *bset, __isl_take isl_constraint *constraint)
 481 {
 482         int i;
 483         unsigned n;
 484         isl_int **row;
 485         unsigned total;
 486
 487         if (!bset || !constraint)
 488                 goto error;
 489
 490         if (!isl_dim_equal(bset->dim, constraint->bmap->dim))
 491                 isl_die(bset->ctx, isl_error_invalid,
 492                         "spaces don't match", goto error);
 493
 494         if (bset != constraint->bmap && !equal_divs(bset, constraint->bmap)) {
 495                 isl_constraint_free(constraint);
 496                 return bset;
 497         }
 498
 499         if (isl_constraint_is_equality(constraint)) {
 500                 n = bset->n_eq;
 501                 row = bset->eq;
 502         } else {
 503                 n = bset->n_ineq;
 504                 row = bset->ineq;
 505         }
 506
 507         total = isl_basic_map_total_dim(constraint->bmap);
 508         for (i = 0; i < n; ++i)
 509                 if (isl_seq_eq(row[i], constraint->line[0], 1 + total))
 510                         isl_seq_clr(row[i], 1 + total);
 511
 512         isl_constraint_free(constraint);
 513         return bset;
 514 error:
 515         isl_constraint_free(constraint);
 516         isl_basic_set_free(bset);
 517         return NULL;
 518 }
 519
 520 struct isl_constraint *isl_constraint_negate(struct isl_constraint *constraint)
 521 {
 522         unsigned total;
 523
 524         if (!constraint)
 525                 return NULL;
 526
 527         isl_assert(constraint->ctx, !isl_constraint_is_equality(constraint),
 528                         goto error);
 529         isl_assert(constraint->ctx, constraint->bmap->ref == 1, goto error);
 530         total = isl_basic_map_total_dim(constraint->bmap);
 531         isl_seq_neg(constraint->line[0], constraint->line[0], 1 + total);
 532         isl_int_sub_ui(constraint->line[0][0], constraint->line[0][0], 1);
 533         ISL_F_CLR(constraint->bmap, ISL_BASIC_MAP_NORMALIZED);
 534         return constraint;
 535 error:
 536         isl_constraint_free(constraint);
 537         return NULL;
 538 }
 539
 540 int isl_constraint_is_equality(struct isl_constraint *constraint)
 541 {
 542         if (!constraint)
 543                 return -1;
 544         return constraint->line >= constraint->bmap->eq;
 545 }
 546
 547 int isl_constraint_is_div_constraint(__isl_keep isl_constraint *constraint)
 548 {
 549         int i;
 550
 551         if (!constraint)
 552                 return -1;
 553         if (isl_constraint_is_equality(constraint))
 554                 return 0;
 555         for (i = 0; i < constraint->bmap->n_div; ++i) {
 556                 if (isl_int_is_zero(constraint->bmap->div[i][0]))
 557                         continue;
 558                 if (isl_basic_map_is_div_constraint(constraint->bmap,
 559                                         constraint->line[0], i))
 560                         return 1;
 561         }
 562
 563         return 0;
 564 }
 565
 566 /* We manually set ISL_BASIC_SET_FINAL instead of calling
 567  * isl_basic_map_finalize because we want to keep the position
 568  * of the divs and we therefore do not want to throw away redundant divs.
 569  * This is arguably a bit fragile.
 570  */
 571 __isl_give isl_basic_map *isl_basic_map_from_constraint(
 572         __isl_take isl_constraint *constraint)
 573 {
 574         int k;
 575         struct isl_basic_map *bmap;
 576         isl_int *c;
 577         unsigned total;
 578
 579         if (!constraint)
 580                 return NULL;
 581
 582         if (constraint->bmap->n_eq == 1 && constraint->bmap->n_ineq == 0) {
 583                 bmap = isl_basic_map_copy(constraint->bmap);
 584                 isl_constraint_free(constraint);
 585                 return bmap;
 586         }
 587
 588         bmap = isl_basic_map_universe_like(constraint->bmap);
 589         bmap = isl_basic_map_align_divs(bmap, constraint->bmap);
 590         bmap = isl_basic_map_cow(bmap);
 591         bmap = isl_basic_map_extend_constraints(bmap, 1, 1);
 592         if (isl_constraint_is_equality(constraint)) {
 593                 k = isl_basic_map_alloc_equality(bmap);
 594                 if (k < 0)
 595                         goto error;
 596                 c = bmap->eq[k];
 597         }
 598         else {
 599                 k = isl_basic_map_alloc_inequality(bmap);
 600                 if (k < 0)
 601                         goto error;
 602                 c = bmap->ineq[k];
 603         }
 604         total = isl_basic_map_total_dim(bmap);
 605         isl_seq_cpy(c, constraint->line[0], 1 + total);
 606         isl_constraint_free(constraint);
 607         if (bmap)
 608                 ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);
 609         return bmap;
 610 error:
 611         isl_constraint_free(constraint);
 612         isl_basic_map_free(bmap);
 613         return NULL;
 614 }
 615
 616 struct isl_basic_set *isl_basic_set_from_constraint(
 617         struct isl_constraint *constraint)
 618 {
 619         if (!constraint)
 620                 return NULL;
 621
 622         isl_assert(constraint->ctx,n(constraint, isl_dim_in) == 0, goto error);
 623         return (isl_basic_set *)isl_basic_map_from_constraint(constraint);
 624 error:
 625         isl_constraint_free(constraint);
 626         return NULL;
 627 }
 628
 629 int isl_basic_map_has_defining_equality(
 630         __isl_keep isl_basic_map *bmap, enum isl_dim_type type, int pos,
 631         __isl_give isl_constraint **c)
 632 {
 633         int i;
 634         unsigned offset;
 635         unsigned total;
 636
 637         if (!bmap)
 638                 return -1;
 639         offset = basic_map_offset(bmap, type);
 640         total = isl_basic_map_total_dim(bmap);
 641         isl_assert(bmap->ctx, pos < isl_basic_map_dim(bmap, type), return -1);
 642         for (i = 0; i < bmap->n_eq; ++i)
 643                 if (!isl_int_is_zero(bmap->eq[i][offset + pos]) &&
 644                     isl_seq_first_non_zero(bmap->eq[i]+offset+pos+1,
 645                                            1+total-offset-pos-1) == -1) {
 646                         *c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
 647                                                                 &bmap->eq[i]);
 648                         return 1;
 649                 }
 650         return 0;
 651 }
 652
 653 int isl_basic_set_has_defining_equality(
 654         __isl_keep isl_basic_set *bset, enum isl_dim_type type, int pos,
 655         __isl_give isl_constraint **c)
 656 {
 657         return isl_basic_map_has_defining_equality((isl_basic_map *)bset,
 658                                                     type, pos, c);
 659 }
 660
 661 int isl_basic_set_has_defining_inequalities(
 662         struct isl_basic_set *bset, enum isl_dim_type type, int pos,
 663         struct isl_constraint **lower,
 664         struct isl_constraint **upper)
 665 {
 666         int i, j;
 667         unsigned offset;
 668         unsigned total;
 669         isl_int m;
 670         isl_int **lower_line, **upper_line;
 671
 672         if (!bset)
 673                 return -1;
 674         offset = basic_set_offset(bset, type);
 675         total = isl_basic_set_total_dim(bset);
 676         isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type), return -1);
 677         isl_int_init(m);
 678         for (i = 0; i < bset->n_ineq; ++i) {
 679                 if (isl_int_is_zero(bset->ineq[i][offset + pos]))
 680                         continue;
 681                 if (isl_int_is_one(bset->ineq[i][offset + pos]))
 682                         continue;
 683                 if (isl_int_is_negone(bset->ineq[i][offset + pos]))
 684                         continue;
 685                 if (isl_seq_first_non_zero(bset->ineq[i]+offset+pos+1,
 686                                                 1+total-offset-pos-1) != -1)
 687                         continue;
 688                 for (j = i + 1; j < bset->n_ineq; ++j) {
 689                         if (!isl_seq_is_neg(bset->ineq[i]+1, bset->ineq[j]+1,
 690                                             total))
 691                                 continue;
 692                         isl_int_add(m, bset->ineq[i][0], bset->ineq[j][0]);
 693                         if (isl_int_abs_ge(m, bset->ineq[i][offset+pos]))
 694                                 continue;
 695
 696                         if (isl_int_is_pos(bset->ineq[i][offset+pos])) {
 697                                 lower_line = &bset->ineq[i];
 698                                 upper_line = &bset->ineq[j];
 699                         } else {
 700                                 lower_line = &bset->ineq[j];
 701                                 upper_line = &bset->ineq[i];
 702                         }
 703                         *lower = isl_basic_set_constraint(
 704                                         isl_basic_set_copy(bset), lower_line);
 705                         *upper = isl_basic_set_constraint(
 706                                         isl_basic_set_copy(bset), upper_line);
 707                         isl_int_clear(m);
 708                         return 1;
 709                 }
 710         }
 711         *lower = NULL;
 712         *upper = NULL;
 713         isl_int_clear(m);
 714         return 0;
 715 }
 716
 717 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
 718  * (in "a" and "b"), add a constraint to "bset" that ensures that the
 719  * bound implied by "a" is (strictly) larger than the bound implied by "b".
 720  *
 721  * If both constraints imply lower bounds, then this means that "a" is
 722  * active in the result.
 723  * If both constraints imply upper bounds, then this means that "b" is
 724  * active in the result.
 725  */
 726 static __isl_give isl_basic_set *add_larger_bound_constraint(
 727         __isl_take isl_basic_set *bset, isl_int *a, isl_int *b,
 728         unsigned abs_pos, int strict)
 729 {
 730         int k;
 731         isl_int t;
 732         unsigned total;
 733
 734         k = isl_basic_set_alloc_inequality(bset);
 735         if (k < 0)
 736                 goto error;
 737
 738         total = isl_basic_set_dim(bset, isl_dim_all);
 739
 740         isl_int_init(t);
 741         isl_int_neg(t, b[1 + abs_pos]);
 742
 743         isl_seq_combine(bset->ineq[k], t, a, a[1 + abs_pos], b, 1 + abs_pos);
 744         isl_seq_combine(bset->ineq[k] + 1 + abs_pos,
 745                 t, a + 1 + abs_pos + 1, a[1 + abs_pos], b + 1 + abs_pos + 1,
 746                 total - abs_pos);
 747
 748         if (strict)
 749                 isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
 750
 751         isl_int_clear(t);
 752
 753         return bset;
 754 error:
 755         isl_basic_set_free(bset);
 756         return NULL;
 757 }
 758
 759 /* Add constraints to "context" that ensure that "u" is the smallest
 760  * (and therefore active) upper bound on "abs_pos" in "bset" and return
 761  * the resulting basic set.
 762  */
 763 static __isl_give isl_basic_set *set_smallest_upper_bound(
 764         __isl_keep isl_basic_set *context,
 765         __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_upper, int u)
 766 {
 767         int j;
 768
 769         context = isl_basic_set_copy(context);
 770         context = isl_basic_set_cow(context);
 771
 772         context = isl_basic_set_extend_constraints(context, 0, n_upper - 1);
 773
 774         for (j = 0; j < bset->n_ineq; ++j) {
 775                 if (j == u)
 776                         continue;
 777                 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
 778                         continue;
 779                 context = add_larger_bound_constraint(context,
 780                         bset->ineq[j], bset->ineq[u], abs_pos, j > u);
 781         }
 782
 783         context = isl_basic_set_simplify(context);
 784         context = isl_basic_set_finalize(context);
 785
 786         return context;
 787 }
 788
 789 /* Add constraints to "context" that ensure that "u" is the largest
 790  * (and therefore active) upper bound on "abs_pos" in "bset" and return
 791  * the resulting basic set.
 792  */
 793 static __isl_give isl_basic_set *set_largest_lower_bound(
 794         __isl_keep isl_basic_set *context,
 795         __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_lower, int l)
 796 {
 797         int j;
 798
 799         context = isl_basic_set_copy(context);
 800         context = isl_basic_set_cow(context);
 801
 802         context = isl_basic_set_extend_constraints(context, 0, n_lower - 1);
 803
 804         for (j = 0; j < bset->n_ineq; ++j) {
 805                 if (j == l)
 806                         continue;
 807                 if (!isl_int_is_pos(bset->ineq[j][1 + abs_pos]))
 808                         continue;
 809                 context = add_larger_bound_constraint(context,
 810                         bset->ineq[l], bset->ineq[j], abs_pos, j > l);
 811         }
 812
 813         context = isl_basic_set_simplify(context);
 814         context = isl_basic_set_finalize(context);
 815
 816         return context;
 817 }
 818
 819 static int foreach_upper_bound(__isl_keep isl_basic_set *bset,
 820         enum isl_dim_type type, unsigned abs_pos,
 821         __isl_take isl_basic_set *context, int n_upper,
 822         int (*fn)(__isl_take isl_constraint *lower,
 823                   __isl_take isl_constraint *upper,
 824                   __isl_take isl_basic_set *bset, void *user), void *user)
 825 {
 826         isl_basic_set *context_i;
 827         isl_constraint *upper = NULL;
 828         int i;
 829
 830         for (i = 0; i < bset->n_ineq; ++i) {
 831                 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
 832                         continue;
 833
 834                 context_i = set_smallest_upper_bound(context, bset,
 835                                                         abs_pos, n_upper, i);
 836                 if (isl_basic_set_is_empty(context_i)) {
 837                         isl_basic_set_free(context_i);
 838                         continue;
 839                 }
 840                 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
 841                                                 &bset->ineq[i]);
 842                 if (!upper || !context_i)
 843                         goto error;
 844                 if (fn(NULL, upper, context_i, user) < 0)
 845                         break;
 846         }
 847
 848         isl_basic_set_free(context);
 849
 850         if (i < bset->n_ineq)
 851                 return -1;
 852
 853         return 0;
 854 error:
 855         isl_constraint_free(upper);
 856         isl_basic_set_free(context_i);
 857         isl_basic_set_free(context);
 858         return -1;
 859 }
 860
 861 static int foreach_lower_bound(__isl_keep isl_basic_set *bset,
 862         enum isl_dim_type type, unsigned abs_pos,
 863         __isl_take isl_basic_set *context, int n_lower,
 864         int (*fn)(__isl_take isl_constraint *lower,
 865                   __isl_take isl_constraint *upper,
 866                   __isl_take isl_basic_set *bset, void *user), void *user)
 867 {
 868         isl_basic_set *context_i;
 869         isl_constraint *lower = NULL;
 870         int i;
 871
 872         for (i = 0; i < bset->n_ineq; ++i) {
 873                 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
 874                         continue;
 875
 876                 context_i = set_largest_lower_bound(context, bset,
 877                                                         abs_pos, n_lower, i);
 878                 if (isl_basic_set_is_empty(context_i)) {
 879                         isl_basic_set_free(context_i);
 880                         continue;
 881                 }
 882                 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
 883                                                 &bset->ineq[i]);
 884                 if (!lower || !context_i)
 885                         goto error;
 886                 if (fn(lower, NULL, context_i, user) < 0)
 887                         break;
 888         }
 889
 890         isl_basic_set_free(context);
 891
 892         if (i < bset->n_ineq)
 893                 return -1;
 894
 895         return 0;
 896 error:
 897         isl_constraint_free(lower);
 898         isl_basic_set_free(context_i);
 899         isl_basic_set_free(context);
 900         return -1;
 901 }
 902
 903 static int foreach_bound_pair(__isl_keep isl_basic_set *bset,
 904         enum isl_dim_type type, unsigned abs_pos,
 905         __isl_take isl_basic_set *context, int n_lower, int n_upper,
 906         int (*fn)(__isl_take isl_constraint *lower,
 907                   __isl_take isl_constraint *upper,
 908                   __isl_take isl_basic_set *bset, void *user), void *user)
 909 {
 910         isl_basic_set *context_i, *context_j;
 911         isl_constraint *lower = NULL;
 912         isl_constraint *upper = NULL;
 913         int i, j;
 914
 915         for (i = 0; i < bset->n_ineq; ++i) {
 916                 if (!isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
 917                         continue;
 918
 919                 context_i = set_largest_lower_bound(context, bset,
 920                                                         abs_pos, n_lower, i);
 921                 if (isl_basic_set_is_empty(context_i)) {
 922                         isl_basic_set_free(context_i);
 923                         continue;
 924                 }
 925
 926                 for (j = 0; j < bset->n_ineq; ++j) {
 927                         if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
 928                                 continue;
 929
 930                         context_j = set_smallest_upper_bound(context_i, bset,
 931                                                             abs_pos, n_upper, j);
 932                         context_j = isl_basic_set_extend_constraints(context_j,
 933                                                                         0, 1);
 934                         context_j = add_larger_bound_constraint(context_j,
 935                                 bset->ineq[i], bset->ineq[j], abs_pos, 0);
 936                         context_j = isl_basic_set_simplify(context_j);
 937                         context_j = isl_basic_set_finalize(context_j);
 938                         if (isl_basic_set_is_empty(context_j)) {
 939                                 isl_basic_set_free(context_j);
 940                                 continue;
 941                         }
 942                         lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
 943                                                         &bset->ineq[i]);
 944                         upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
 945                                                         &bset->ineq[j]);
 946                         if (!lower || !upper || !context_j)
 947                                 goto error;
 948                         if (fn(lower, upper, context_j, user) < 0)
 949                                 break;
 950                 }
 951
 952                 isl_basic_set_free(context_i);
 953
 954                 if (j < bset->n_ineq)
 955                         break;
 956         }
 957
 958         isl_basic_set_free(context);
 959
 960         if (i < bset->n_ineq)
 961                 return -1;
 962
 963         return 0;
 964 error:
 965         isl_constraint_free(lower);
 966         isl_constraint_free(upper);
 967         isl_basic_set_free(context_i);
 968         isl_basic_set_free(context_j);
 969         isl_basic_set_free(context);
 970         return -1;
 971 }
 972
 973 /* For each pair of lower and upper bounds on the variable "pos"
 974  * of type "type", call "fn" with these lower and upper bounds and the
 975  * set of constraints on the remaining variables where these bounds
 976  * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
 977  *
 978  * If the designated variable is equal to an affine combination of the
 979  * other variables then fn is called with both lower and upper
 980  * set to the corresponding equality.
 981  *
 982  * If there is no lower (or upper) bound, then NULL is passed
 983  * as the corresponding bound.
 984  *
 985  * We first check if the variable is involved in any equality.
 986  * If not, we count the number of lower and upper bounds and
 987  * act accordingly.
 988  */
 989 int isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set *bset,
 990         enum isl_dim_type type, unsigned pos,
 991         int (*fn)(__isl_take isl_constraint *lower,
 992                   __isl_take isl_constraint *upper,
 993                   __isl_take isl_basic_set *bset, void *user), void *user)
 994 {
 995         int i;
 996         isl_constraint *lower = NULL;
 997         isl_constraint *upper = NULL;
 998         isl_basic_set *context = NULL;
 999         unsigned abs_pos;
1000         int n_lower, n_upper;
1001
1002         if (!bset)
1003                 return -1;
1004         isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type), return -1);
1005         isl_assert(bset->ctx, type == isl_dim_param || type == isl_dim_set,
1006                 return -1);
1007
1008         abs_pos = pos;
1009         if (type == isl_dim_set)
1010                 abs_pos += isl_basic_set_dim(bset, isl_dim_param);
1011
1012         for (i = 0; i < bset->n_eq; ++i) {
1013                 if (isl_int_is_zero(bset->eq[i][1 + abs_pos]))
1014                         continue;
1015
1016                 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1017                                                 &bset->eq[i]);
1018                 upper = isl_constraint_copy(lower);
1019                 context = isl_basic_set_remove_dims(isl_basic_set_copy(bset),
1020                                         type, pos, 1);
1021                 if (!lower || !upper || !context)
1022                         goto error;
1023                 return fn(lower, upper, context, user);
1024         }
1025
1026         n_lower = 0;
1027         n_upper = 0;
1028         for (i = 0; i < bset->n_ineq; ++i) {
1029                 if (isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
1030                         n_lower++;
1031                 else if (isl_int_is_neg(bset->ineq[i][1 + abs_pos]))
1032                         n_upper++;
1033         }
1034
1035         context = isl_basic_set_copy(bset);
1036         context = isl_basic_set_cow(context);
1037         if (!context)
1038                 goto error;
1039         for (i = context->n_ineq - 1; i >= 0; --i)
1040                 if (!isl_int_is_zero(context->ineq[i][1 + abs_pos]))
1041                         isl_basic_set_drop_inequality(context, i);
1042
1043         context = isl_basic_set_drop(context, type, pos, 1);
1044         if (!n_lower && !n_upper)
1045                 return fn(NULL, NULL, context, user);
1046         if (!n_lower)
1047                 return foreach_upper_bound(bset, type, abs_pos, context, n_upper,
1048                                                 fn, user);
1049         if (!n_upper)
1050                 return foreach_lower_bound(bset, type, abs_pos, context, n_lower,
1051                                                 fn, user);
1052         return foreach_bound_pair(bset, type, abs_pos, context, n_lower, n_upper,
1053                                         fn, user);
1054 error:
1055         isl_constraint_free(lower);
1056         isl_constraint_free(upper);
1057         isl_basic_set_free(context);
1058         return -1;
1059 }
1060
1061 __isl_give isl_aff *isl_constraint_get_bound(
1062         __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
1063 {
1064         isl_aff *aff;
1065         isl_local_space *ls;
1066
1067         if (!constraint)
1068                 return NULL;
1069         if (pos >= isl_basic_set_dim(constraint->bmap, type))
1070                 isl_die(constraint->ctx, isl_error_invalid,
1071                         "index out of bounds", return NULL);
1072         if (!isl_basic_map_may_be_set(constraint->bmap))
1073                 isl_die(constraint->ctx, isl_error_invalid,
1074                         "not a set constraint", return NULL);
1075
1076         pos += offset(constraint, type);
1077         if (isl_int_is_zero(constraint->line[0][pos]))
1078                 isl_die(constraint->ctx, isl_error_invalid,
1079                         "constraint does not define a bound on given dimension",
1080                         return NULL);
1081
1082         ls = isl_basic_set_get_local_space(constraint->bmap);
1083         aff = isl_aff_alloc(ls);
1084         if (!aff)
1085                 return NULL;
1086
1087         if (isl_int_is_neg(constraint->line[0][pos]))
1088                 isl_seq_cpy(aff->v->el + 1, constraint->line[0],
1089                             aff->v->size - 1);
1090         else
1091                 isl_seq_neg(aff->v->el + 1, constraint->line[0],
1092                             aff->v->size - 1);
1093         isl_int_set_si(aff->v->el[1 + pos], 0);
1094         isl_int_abs(aff->v->el[0], constraint->line[0][pos]);
1095
1096         return aff;
1097 }
1098
1099 /* For an inequality constraint
1100  *
1101  *      f >= 0
1102  *
1103  * or an equality constraint
1104  *
1105  *      f = 0
1106  *
1107  * return the affine expression f.
1108  */
1109 __isl_give isl_aff *isl_constraint_get_aff(
1110         __isl_keep isl_constraint *constraint)
1111 {
1112         isl_aff *aff;
1113         isl_local_space *ls;
1114
1115         if (!constraint)
1116                 return NULL;
1117
1118         ls = isl_basic_set_get_local_space(constraint->bmap);
1119         aff = isl_aff_alloc(ls);
1120         if (!aff)
1121                 return NULL;
1122
1123         isl_seq_cpy(aff->v->el + 1, constraint->line[0], aff->v->size - 1);
1124         isl_int_set_si(aff->v->el[0], 1);
1125
1126         return aff;
1127 }
1128
1129 /* Construct an equality constraint equating the given affine expression
1130  * to zero.
1131  */
1132 __isl_give isl_constraint *isl_equality_from_aff(__isl_take isl_aff *aff)
1133 {
1134         int k;
1135         isl_basic_set *bset;
1136
1137         if (!aff)
1138                 return NULL;
1139
1140         bset = isl_basic_set_from_local_space(isl_aff_get_local_space(aff));
1141         bset = isl_basic_set_extend_constraints(bset, 1, 0);
1142         k = isl_basic_set_alloc_equality(bset);
1143         if (k < 0)
1144                 goto error;
1145
1146         isl_seq_cpy(bset->eq[k], aff->v->el + 1, aff->v->size - 1);
1147         isl_aff_free(aff);
1148
1149         return isl_basic_set_constraint(bset, &bset->eq[k]);
1150 error:
1151         isl_aff_free(aff);
1152         isl_basic_set_free(bset);
1153         return NULL;
1154 }
1155
1156 /* Construct an inequality constraint enforcing the given affine expression
1157  * to be non-negative.
1158  */
1159 __isl_give isl_constraint *isl_inequality_from_aff(__isl_take isl_aff *aff)
1160 {
1161         int k;
1162         isl_basic_set *bset;
1163
1164         if (!aff)
1165                 return NULL;
1166
1167         bset = isl_basic_set_from_local_space(isl_aff_get_local_space(aff));
1168         bset = isl_basic_set_extend_constraints(bset, 0, 1);
1169         k = isl_basic_set_alloc_inequality(bset);
1170         if (k < 0)
1171                 goto error;
1172
1173         isl_seq_cpy(bset->ineq[k], aff->v->el + 1, aff->v->size - 1);
1174         isl_aff_free(aff);
1175
1176         return isl_basic_set_constraint(bset, &bset->ineq[k]);
1177 error:
1178         isl_aff_free(aff);
1179         isl_basic_set_free(bset);
1180         return NULL;
1181 }