isl_constraint.c

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