1372 lines · c
1/*2 * Copyright 2008-2009 Katholieke Universiteit Leuven3 * Copyright 2010 INRIA Saclay4 *5 * Use of this software is governed by the MIT license6 *7 * Written by Sven Verdoolaege, K.U.Leuven, Departement8 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium9 * 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#include <isl_val_private.h>20#include <isl_vec_private.h>21 22#include <bset_to_bmap.c>23#include <bset_from_bmap.c>24 25#undef EL_BASE26#define EL_BASE constraint27 28#include <isl_list_templ.c>29 30isl_ctx *isl_constraint_get_ctx(__isl_keep isl_constraint *c)31{32 return c ? isl_local_space_get_ctx(c->ls) : NULL;33}34 35static isl_size n(__isl_keep isl_constraint *c, enum isl_dim_type type)36{37 return isl_local_space_dim(c->ls, type);38}39 40static unsigned offset(__isl_keep isl_constraint *c, enum isl_dim_type type)41{42 return isl_local_space_offset(c->ls, type);43}44 45__isl_give isl_constraint *isl_constraint_alloc_vec(int eq,46 __isl_take isl_local_space *ls, __isl_take isl_vec *v)47{48 isl_constraint *constraint;49 50 if (!ls || !v)51 goto error;52 53 constraint = isl_alloc_type(isl_vec_get_ctx(v), isl_constraint);54 if (!constraint)55 goto error;56 57 constraint->ref = 1;58 constraint->eq = eq;59 constraint->ls = ls;60 constraint->v = v;61 62 return constraint;63error:64 isl_local_space_free(ls);65 isl_vec_free(v);66 return NULL;67}68 69__isl_give isl_constraint *isl_constraint_alloc(int eq,70 __isl_take isl_local_space *ls)71{72 isl_size dim;73 isl_ctx *ctx;74 isl_vec *v;75 76 dim = isl_local_space_dim(ls, isl_dim_all);77 if (dim < 0)78 ls = isl_local_space_free(ls);79 if (!ls)80 return NULL;81 82 ctx = isl_local_space_get_ctx(ls);83 v = isl_vec_alloc(ctx, 1 + dim);84 v = isl_vec_clr(v);85 return isl_constraint_alloc_vec(eq, ls, v);86}87 88__isl_give isl_constraint *isl_basic_map_constraint(89 __isl_take isl_basic_map *bmap, isl_int **line)90{91 int eq;92 isl_size dim;93 isl_ctx *ctx;94 isl_vec *v;95 isl_local_space *ls = NULL;96 isl_constraint *constraint;97 98 if (!bmap || !line)99 goto error;100 101 eq = line >= bmap->eq;102 103 ctx = isl_basic_map_get_ctx(bmap);104 ls = isl_basic_map_get_local_space(bmap);105 dim = isl_local_space_dim(ls, isl_dim_all);106 if (dim < 0)107 goto error;108 v = isl_vec_alloc(ctx, 1 + dim);109 if (!v)110 goto error;111 isl_seq_cpy(v->el, line[0], v->size);112 constraint = isl_constraint_alloc_vec(eq, ls, v);113 114 isl_basic_map_free(bmap);115 return constraint;116error:117 isl_local_space_free(ls);118 isl_basic_map_free(bmap);119 return NULL;120}121 122__isl_give isl_constraint *isl_basic_set_constraint(123 __isl_take isl_basic_set *bset, isl_int **line)124{125 return isl_basic_map_constraint(bset_to_bmap(bset), line);126}127 128__isl_give isl_constraint *isl_constraint_alloc_equality(129 __isl_take isl_local_space *ls)130{131 return isl_constraint_alloc(1, ls);132}133 134__isl_give isl_constraint *isl_constraint_alloc_inequality(135 __isl_take isl_local_space *ls)136{137 return isl_constraint_alloc(0, ls);138}139 140__isl_give isl_constraint *isl_constraint_dup(__isl_keep 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__isl_give isl_constraint *isl_constraint_cow(__isl_take 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__isl_give isl_constraint *isl_constraint_copy(161 __isl_keep isl_constraint *constraint)162{163 if (!constraint)164 return NULL;165 166 constraint->ref++;167 return constraint;168}169 170__isl_null isl_constraint *isl_constraint_free(__isl_take isl_constraint *c)171{172 if (!c)173 return NULL;174 175 if (--c->ref > 0)176 return NULL;177 178 isl_local_space_free(c->ls);179 isl_vec_free(c->v);180 free(c);181 182 return NULL;183}184 185/* Return the number of constraints in "bmap", i.e., the186 * number of times isl_basic_map_foreach_constraint will187 * call the callback.188 */189isl_size isl_basic_map_n_constraint(__isl_keep isl_basic_map *bmap)190{191 if (!bmap)192 return isl_size_error;193 194 return bmap->n_eq + bmap->n_ineq;195}196 197/* Return the number of constraints in "bset", i.e., the198 * number of times isl_basic_set_foreach_constraint will199 * call the callback.200 */201isl_size isl_basic_set_n_constraint(__isl_keep isl_basic_set *bset)202{203 return isl_basic_map_n_constraint(bset);204}205 206isl_stat isl_basic_map_foreach_constraint(__isl_keep isl_basic_map *bmap,207 isl_stat (*fn)(__isl_take isl_constraint *c, void *user), void *user)208{209 int i;210 struct isl_constraint *c;211 212 if (!bmap)213 return isl_stat_error;214 215 isl_assert(bmap->ctx, ISL_F_ISSET(bmap, ISL_BASIC_MAP_FINAL),216 return isl_stat_error);217 218 for (i = 0; i < bmap->n_eq; ++i) {219 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),220 &bmap->eq[i]);221 if (!c)222 return isl_stat_error;223 if (fn(c, user) < 0)224 return isl_stat_error;225 }226 227 for (i = 0; i < bmap->n_ineq; ++i) {228 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),229 &bmap->ineq[i]);230 if (!c)231 return isl_stat_error;232 if (fn(c, user) < 0)233 return isl_stat_error;234 }235 236 return isl_stat_ok;237}238 239isl_stat isl_basic_set_foreach_constraint(__isl_keep isl_basic_set *bset,240 isl_stat (*fn)(__isl_take isl_constraint *c, void *user), void *user)241{242 return isl_basic_map_foreach_constraint(bset_to_bmap(bset), fn, user);243}244 245/* Add the constraint to the list that "user" points to, if it is not246 * a div constraint.247 */248static isl_stat collect_constraint(__isl_take isl_constraint *constraint,249 void *user)250{251 isl_constraint_list **list = user;252 isl_bool is_div;253 254 is_div = isl_constraint_is_div_constraint(constraint);255 if (is_div < 0 || is_div)256 isl_constraint_free(constraint);257 else258 *list = isl_constraint_list_add(*list, constraint);259 260 return is_div < 0 ? isl_stat_error : isl_stat_ok;261}262 263/* Return a list of constraints that, when combined, are equivalent264 * to "bmap". The input is required to have only known divs.265 *266 * There is no need to include the div constraints as they are267 * implied by the div expressions.268 */269__isl_give isl_constraint_list *isl_basic_map_get_constraint_list(270 __isl_keep isl_basic_map *bmap)271{272 isl_size n;273 isl_bool known;274 isl_ctx *ctx;275 isl_constraint_list *list;276 277 known = isl_basic_map_divs_known(bmap);278 if (known < 0)279 return NULL;280 ctx = isl_basic_map_get_ctx(bmap);281 if (!known)282 isl_die(ctx, isl_error_invalid,283 "input involves unknown divs", return NULL);284 285 n = isl_basic_map_n_constraint(bmap);286 if (n < 0)287 return NULL;288 list = isl_constraint_list_alloc(ctx, n);289 if (isl_basic_map_foreach_constraint(bmap,290 &collect_constraint, &list) < 0)291 list = isl_constraint_list_free(list);292 293 return list;294}295 296/* Return a list of constraints that, when combined, are equivalent297 * to "bset". The input is required to have only known divs.298 */299__isl_give isl_constraint_list *isl_basic_set_get_constraint_list(300 __isl_keep isl_basic_set *bset)301{302 return isl_basic_map_get_constraint_list(bset);303}304 305int isl_constraint_is_equal(__isl_keep isl_constraint *constraint1,306 __isl_keep isl_constraint *constraint2)307{308 int equal;309 310 if (!constraint1 || !constraint2)311 return 0;312 if (constraint1->eq != constraint2->eq)313 return 0;314 equal = isl_local_space_is_equal(constraint1->ls, constraint2->ls);315 if (equal < 0 || !equal)316 return equal;317 return isl_vec_is_equal(constraint1->v, constraint2->v);318}319 320__isl_give isl_basic_map *isl_basic_map_add_constraint(321 __isl_take isl_basic_map *bmap, __isl_take isl_constraint *constraint)322{323 isl_ctx *ctx;324 isl_space *space;325 int equal_space;326 327 if (!bmap || !constraint)328 goto error;329 330 ctx = isl_constraint_get_ctx(constraint);331 space = isl_constraint_get_space(constraint);332 equal_space = isl_space_is_equal(bmap->dim, space);333 isl_space_free(space);334 isl_assert(ctx, equal_space, goto error);335 336 bmap = isl_basic_map_intersect(bmap,337 isl_basic_map_from_constraint(constraint));338 return bmap;339error:340 isl_basic_map_free(bmap);341 isl_constraint_free(constraint);342 return NULL;343}344 345__isl_give isl_basic_set *isl_basic_set_add_constraint(346 __isl_take isl_basic_set *bset, __isl_take isl_constraint *constraint)347{348 return bset_from_bmap(isl_basic_map_add_constraint(bset_to_bmap(bset),349 constraint));350}351 352__isl_give isl_map *isl_map_add_constraint(__isl_take isl_map *map,353 __isl_take isl_constraint *constraint)354{355 isl_basic_map *bmap;356 357 bmap = isl_basic_map_from_constraint(constraint);358 map = isl_map_intersect(map, isl_map_from_basic_map(bmap));359 360 return map;361}362 363__isl_give isl_set *isl_set_add_constraint(__isl_take isl_set *set,364 __isl_take isl_constraint *constraint)365{366 return isl_map_add_constraint(set, constraint);367}368 369/* Return the space of "constraint".370 */371static __isl_keep isl_space *isl_constraint_peek_space(372 __isl_keep isl_constraint *constraint)373{374 return constraint ? isl_local_space_peek_space(constraint->ls) : NULL;375}376 377__isl_give isl_space *isl_constraint_get_space(378 __isl_keep isl_constraint *constraint)379{380 return constraint ? isl_local_space_get_space(constraint->ls) : NULL;381}382 383__isl_give isl_local_space *isl_constraint_get_local_space(384 __isl_keep isl_constraint *constraint)385{386 return constraint ? isl_local_space_copy(constraint->ls) : NULL;387}388 389isl_size isl_constraint_dim(__isl_keep isl_constraint *constraint,390 enum isl_dim_type type)391{392 if (!constraint)393 return isl_size_error;394 return n(constraint, type);395}396 397#undef TYPE398#define TYPE isl_constraint399static400#include "check_type_range_templ.c"401 402isl_bool isl_constraint_involves_dims(__isl_keep isl_constraint *constraint,403 enum isl_dim_type type, unsigned first, unsigned n)404{405 int i;406 int *active = NULL;407 isl_bool involves = isl_bool_false;408 409 if (!constraint)410 return isl_bool_error;411 if (n == 0)412 return isl_bool_false;413 414 if (isl_constraint_check_range(constraint, type, first, n) < 0)415 return isl_bool_error;416 417 active = isl_local_space_get_active(constraint->ls,418 constraint->v->el + 1);419 if (!active)420 goto error;421 422 first += isl_local_space_offset(constraint->ls, type) - 1;423 for (i = 0; i < n; ++i)424 if (active[first + i]) {425 involves = isl_bool_true;426 break;427 }428 429 free(active);430 431 return involves;432error:433 free(active);434 return isl_bool_error;435}436 437/* Does the given constraint represent a lower bound on the given438 * dimension?439 */440isl_bool isl_constraint_is_lower_bound(__isl_keep isl_constraint *constraint,441 enum isl_dim_type type, unsigned pos)442{443 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)444 return isl_bool_error;445 446 pos += isl_local_space_offset(constraint->ls, type);447 return isl_bool_ok(isl_int_is_pos(constraint->v->el[pos]));448}449 450/* Does the given constraint represent an upper bound on the given451 * dimension?452 */453isl_bool isl_constraint_is_upper_bound(__isl_keep isl_constraint *constraint,454 enum isl_dim_type type, unsigned pos)455{456 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)457 return isl_bool_error;458 459 pos += isl_local_space_offset(constraint->ls, type);460 return isl_bool_ok(isl_int_is_neg(constraint->v->el[pos]));461}462 463const char *isl_constraint_get_dim_name(__isl_keep isl_constraint *constraint,464 enum isl_dim_type type, unsigned pos)465{466 return constraint ?467 isl_local_space_get_dim_name(constraint->ls, type, pos) : NULL;468}469 470void isl_constraint_get_constant(__isl_keep isl_constraint *constraint,471 isl_int *v)472{473 if (!constraint)474 return;475 isl_int_set(*v, constraint->v->el[0]);476}477 478/* Return the constant term of "constraint".479 */480__isl_give isl_val *isl_constraint_get_constant_val(481 __isl_keep isl_constraint *constraint)482{483 isl_ctx *ctx;484 485 if (!constraint)486 return NULL;487 488 ctx = isl_constraint_get_ctx(constraint);489 return isl_val_int_from_isl_int(ctx, constraint->v->el[0]);490}491 492void isl_constraint_get_coefficient(__isl_keep isl_constraint *constraint,493 enum isl_dim_type type, int pos, isl_int *v)494{495 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)496 return;497 498 pos += isl_local_space_offset(constraint->ls, type);499 isl_int_set(*v, constraint->v->el[pos]);500}501 502/* Return the coefficient of the variable of type "type" at position "pos"503 * of "constraint".504 */505__isl_give isl_val *isl_constraint_get_coefficient_val(506 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)507{508 isl_ctx *ctx;509 510 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)511 return NULL;512 513 ctx = isl_constraint_get_ctx(constraint);514 pos += isl_local_space_offset(constraint->ls, type);515 return isl_val_int_from_isl_int(ctx, constraint->v->el[pos]);516}517 518__isl_give isl_aff *isl_constraint_get_div(__isl_keep isl_constraint *constraint,519 int pos)520{521 if (!constraint)522 return NULL;523 524 return isl_local_space_get_div(constraint->ls, pos);525}526 527__isl_give isl_constraint *isl_constraint_set_constant(528 __isl_take isl_constraint *constraint, isl_int v)529{530 constraint = isl_constraint_cow(constraint);531 if (!constraint)532 return NULL;533 534 constraint->v = isl_vec_cow(constraint->v);535 if (!constraint->v)536 return isl_constraint_free(constraint);537 538 isl_int_set(constraint->v->el[0], v);539 return constraint;540}541 542/* Replace the constant term of "constraint" by "v".543 */544__isl_give isl_constraint *isl_constraint_set_constant_val(545 __isl_take isl_constraint *constraint, __isl_take isl_val *v)546{547 constraint = isl_constraint_cow(constraint);548 if (!constraint || !v)549 goto error;550 if (!isl_val_is_int(v))551 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,552 "expecting integer value", goto error);553 constraint->v = isl_vec_set_element_val(constraint->v, 0, v);554 if (!constraint->v)555 constraint = isl_constraint_free(constraint);556 return constraint;557error:558 isl_val_free(v);559 return isl_constraint_free(constraint);560}561 562__isl_give isl_constraint *isl_constraint_set_constant_si(563 __isl_take isl_constraint *constraint, int v)564{565 constraint = isl_constraint_cow(constraint);566 if (!constraint)567 return NULL;568 569 constraint->v = isl_vec_cow(constraint->v);570 if (!constraint->v)571 return isl_constraint_free(constraint);572 573 isl_int_set_si(constraint->v->el[0], v);574 return constraint;575}576 577/* Replace the coefficient of the variable of type "type" at position "pos"578 * of "constraint" by "v".579 */580__isl_give isl_constraint *isl_constraint_set_coefficient_val(581 __isl_take isl_constraint *constraint,582 enum isl_dim_type type, int pos, __isl_take isl_val *v)583{584 constraint = isl_constraint_cow(constraint);585 if (!constraint || !v)586 goto error;587 if (!isl_val_is_int(v))588 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,589 "expecting integer value", goto error);590 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)591 goto error;592 593 pos += isl_local_space_offset(constraint->ls, type);594 constraint->v = isl_vec_set_element_val(constraint->v, pos, v);595 if (!constraint->v)596 constraint = isl_constraint_free(constraint);597 return constraint;598error:599 isl_val_free(v);600 return isl_constraint_free(constraint);601}602 603__isl_give isl_constraint *isl_constraint_set_coefficient_si(604 __isl_take isl_constraint *constraint,605 enum isl_dim_type type, int pos, int v)606{607 constraint = isl_constraint_cow(constraint);608 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)609 return isl_constraint_free(constraint);610 611 constraint->v = isl_vec_cow(constraint->v);612 if (!constraint->v)613 return isl_constraint_free(constraint);614 615 pos += isl_local_space_offset(constraint->ls, type);616 isl_int_set_si(constraint->v->el[pos], v);617 618 return constraint;619}620 621__isl_give isl_constraint *isl_constraint_negate(622 __isl_take isl_constraint *constraint)623{624 isl_ctx *ctx;625 626 constraint = isl_constraint_cow(constraint);627 if (!constraint)628 return NULL;629 630 ctx = isl_constraint_get_ctx(constraint);631 if (isl_constraint_is_equality(constraint))632 isl_die(ctx, isl_error_invalid, "cannot negate equality",633 return isl_constraint_free(constraint));634 constraint->v = isl_vec_neg(constraint->v);635 constraint->v = isl_vec_cow(constraint->v);636 if (!constraint->v)637 return isl_constraint_free(constraint);638 isl_int_sub_ui(constraint->v->el[0], constraint->v->el[0], 1);639 return constraint;640}641 642isl_bool isl_constraint_is_equality(struct isl_constraint *constraint)643{644 if (!constraint)645 return isl_bool_error;646 return isl_bool_ok(constraint->eq);647}648 649isl_bool isl_constraint_is_div_constraint(__isl_keep isl_constraint *constraint)650{651 int i;652 isl_size n_div;653 654 if (!constraint)655 return isl_bool_error;656 if (isl_constraint_is_equality(constraint))657 return isl_bool_false;658 n_div = isl_constraint_dim(constraint, isl_dim_div);659 if (n_div < 0)660 return isl_bool_error;661 for (i = 0; i < n_div; ++i) {662 isl_bool is_div;663 is_div = isl_local_space_is_div_constraint(constraint->ls,664 constraint->v->el, i);665 if (is_div < 0 || is_div)666 return is_div;667 }668 669 return isl_bool_false;670}671 672/* Is "constraint" an equality that corresponds to integer division "div"?673 *674 * That is, given an integer division of the form675 *676 * a = floor((f + c)/m)677 *678 * is the equality of the form679 *680 * -f + m d + c' = 0681 * ?682 * Note that the constant term is not checked explicitly, but given683 * that this is a valid equality constraint, the constant c' necessarily684 * has a value close to -c.685 */686isl_bool isl_constraint_is_div_equality(__isl_keep isl_constraint *constraint,687 unsigned div)688{689 isl_bool equality;690 691 equality = isl_constraint_is_equality(constraint);692 if (equality < 0 || !equality)693 return equality;694 return isl_local_space_is_div_equality(constraint->ls,695 constraint->v->el, div);696}697 698/* We manually set ISL_BASIC_SET_FINAL instead of calling699 * isl_basic_map_finalize because we want to keep the position700 * of the divs and we therefore do not want to throw away redundant divs.701 * This is arguably a bit fragile.702 */703__isl_give isl_basic_map *isl_basic_map_from_constraint(704 __isl_take isl_constraint *constraint)705{706 int k;707 isl_local_space *ls;708 struct isl_basic_map *bmap;709 isl_int *c;710 isl_size total;711 712 if (!constraint)713 return NULL;714 715 ls = isl_local_space_copy(constraint->ls);716 bmap = isl_basic_map_from_local_space(ls);717 bmap = isl_basic_map_extend_constraints(bmap, 1, 1);718 if (isl_constraint_is_equality(constraint)) {719 k = isl_basic_map_alloc_equality(bmap);720 if (k < 0)721 goto error;722 c = bmap->eq[k];723 }724 else {725 k = isl_basic_map_alloc_inequality(bmap);726 if (k < 0)727 goto error;728 c = bmap->ineq[k];729 }730 total = isl_basic_map_dim(bmap, isl_dim_all);731 if (total < 0)732 goto error;733 isl_seq_cpy(c, constraint->v->el, 1 + total);734 isl_constraint_free(constraint);735 if (bmap)736 ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);737 return bmap;738error:739 isl_constraint_free(constraint);740 isl_basic_map_free(bmap);741 return NULL;742}743 744__isl_give isl_basic_set *isl_basic_set_from_constraint(745 __isl_take isl_constraint *constraint)746{747 isl_space *space;748 749 space = isl_constraint_peek_space(constraint);750 if (isl_space_check_is_set(space) < 0)751 goto error;752 return bset_from_bmap(isl_basic_map_from_constraint(constraint));753error:754 isl_constraint_free(constraint);755 return NULL;756}757 758/* Is the variable of "type" at position "pos" of "bmap" defined759 * in terms of earlier dimensions through an equality?760 *761 * If so, and if c is not NULL, then return a copy of this equality in *c.762 */763isl_bool isl_basic_map_has_defining_equality(764 __isl_keep isl_basic_map *bmap, enum isl_dim_type type, int pos,765 __isl_give isl_constraint **c)766{767 int i;768 unsigned offset;769 isl_size total;770 771 if (isl_basic_map_check_range(bmap, type, pos, 1) < 0)772 return isl_bool_error;773 offset = isl_basic_map_offset(bmap, type);774 total = isl_basic_map_dim(bmap, isl_dim_all);775 if (total < 0)776 return isl_bool_error;777 for (i = 0; i < bmap->n_eq; ++i) {778 if (isl_int_is_zero(bmap->eq[i][offset + pos]) ||779 isl_seq_first_non_zero(bmap->eq[i]+offset+pos+1,780 1+total-offset-pos-1) != -1)781 continue;782 if (c)783 *c = isl_basic_map_constraint(isl_basic_map_copy(bmap),784 &bmap->eq[i]);785 return isl_bool_true;786 }787 return isl_bool_false;788}789 790/* Is the variable of "type" at position "pos" of "bset" defined791 * in terms of earlier dimensions through an equality?792 *793 * If so, and if c is not NULL, then return a copy of this equality in *c.794 */795isl_bool isl_basic_set_has_defining_equality(796 __isl_keep isl_basic_set *bset, enum isl_dim_type type, int pos,797 __isl_give isl_constraint **c)798{799 return isl_basic_map_has_defining_equality(bset_to_bmap(bset),800 type, pos, c);801}802 803isl_bool isl_basic_set_has_defining_inequalities(804 struct isl_basic_set *bset, enum isl_dim_type type, int pos,805 struct isl_constraint **lower,806 struct isl_constraint **upper)807{808 int i, j;809 unsigned offset;810 isl_size total;811 isl_int m;812 isl_int **lower_line, **upper_line;813 814 if (isl_basic_set_check_range(bset, type, pos, 1) < 0)815 return isl_bool_error;816 offset = isl_basic_set_offset(bset, type);817 total = isl_basic_set_dim(bset, isl_dim_all);818 if (total < 0)819 return isl_bool_error;820 isl_int_init(m);821 for (i = 0; i < bset->n_ineq; ++i) {822 if (isl_int_is_zero(bset->ineq[i][offset + pos]))823 continue;824 if (isl_int_is_one(bset->ineq[i][offset + pos]))825 continue;826 if (isl_int_is_negone(bset->ineq[i][offset + pos]))827 continue;828 if (isl_seq_first_non_zero(bset->ineq[i]+offset+pos+1,829 1+total-offset-pos-1) != -1)830 continue;831 for (j = i + 1; j < bset->n_ineq; ++j) {832 if (!isl_seq_is_neg(bset->ineq[i]+1, bset->ineq[j]+1,833 total))834 continue;835 isl_int_add(m, bset->ineq[i][0], bset->ineq[j][0]);836 if (isl_int_abs_ge(m, bset->ineq[i][offset+pos]))837 continue;838 839 if (isl_int_is_pos(bset->ineq[i][offset+pos])) {840 lower_line = &bset->ineq[i];841 upper_line = &bset->ineq[j];842 } else {843 lower_line = &bset->ineq[j];844 upper_line = &bset->ineq[i];845 }846 *lower = isl_basic_set_constraint(847 isl_basic_set_copy(bset), lower_line);848 *upper = isl_basic_set_constraint(849 isl_basic_set_copy(bset), upper_line);850 isl_int_clear(m);851 return isl_bool_true;852 }853 }854 *lower = NULL;855 *upper = NULL;856 isl_int_clear(m);857 return isl_bool_false;858}859 860/* Given two constraints "a" and "b" on the variable at position "abs_pos"861 * (in "a" and "b"), add a constraint to "bset" that ensures that the862 * bound implied by "a" is (strictly) larger than the bound implied by "b".863 *864 * If both constraints imply lower bounds, then this means that "a" is865 * active in the result.866 * If both constraints imply upper bounds, then this means that "b" is867 * active in the result.868 */869static __isl_give isl_basic_set *add_larger_bound_constraint(870 __isl_take isl_basic_set *bset, isl_int *a, isl_int *b,871 unsigned abs_pos, int strict)872{873 int k;874 isl_int t;875 isl_size total;876 877 total = isl_basic_set_dim(bset, isl_dim_all);878 if (total < 0)879 return isl_basic_set_free(bset);880 k = isl_basic_set_alloc_inequality(bset);881 if (k < 0)882 goto error;883 884 isl_int_init(t);885 isl_int_neg(t, b[1 + abs_pos]);886 887 isl_seq_combine(bset->ineq[k], t, a, a[1 + abs_pos], b, 1 + abs_pos);888 isl_seq_combine(bset->ineq[k] + 1 + abs_pos,889 t, a + 1 + abs_pos + 1, a[1 + abs_pos], b + 1 + abs_pos + 1,890 total - abs_pos);891 892 if (strict)893 isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);894 895 isl_int_clear(t);896 897 return bset;898error:899 isl_basic_set_free(bset);900 return NULL;901}902 903/* Add constraints to "context" that ensure that "u" is the smallest904 * (and therefore active) upper bound on "abs_pos" in "bset" and return905 * the resulting basic set.906 */907static __isl_give isl_basic_set *set_smallest_upper_bound(908 __isl_keep isl_basic_set *context,909 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_upper, int u)910{911 int j;912 913 context = isl_basic_set_copy(context);914 context = isl_basic_set_cow(context);915 916 context = isl_basic_set_extend_constraints(context, 0, n_upper - 1);917 918 for (j = 0; j < bset->n_ineq; ++j) {919 if (j == u)920 continue;921 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))922 continue;923 context = add_larger_bound_constraint(context,924 bset->ineq[j], bset->ineq[u], abs_pos, j > u);925 }926 927 context = isl_basic_set_simplify(context);928 context = isl_basic_set_finalize(context);929 930 return context;931}932 933/* Add constraints to "context" that ensure that "u" is the largest934 * (and therefore active) upper bound on "abs_pos" in "bset" and return935 * the resulting basic set.936 */937static __isl_give isl_basic_set *set_largest_lower_bound(938 __isl_keep isl_basic_set *context,939 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_lower, int l)940{941 int j;942 943 context = isl_basic_set_copy(context);944 context = isl_basic_set_cow(context);945 946 context = isl_basic_set_extend_constraints(context, 0, n_lower - 1);947 948 for (j = 0; j < bset->n_ineq; ++j) {949 if (j == l)950 continue;951 if (!isl_int_is_pos(bset->ineq[j][1 + abs_pos]))952 continue;953 context = add_larger_bound_constraint(context,954 bset->ineq[l], bset->ineq[j], abs_pos, j > l);955 }956 957 context = isl_basic_set_simplify(context);958 context = isl_basic_set_finalize(context);959 960 return context;961}962 963static isl_stat foreach_upper_bound(__isl_keep isl_basic_set *bset,964 enum isl_dim_type type, unsigned abs_pos,965 __isl_take isl_basic_set *context, int n_upper,966 isl_stat (*fn)(__isl_take isl_constraint *lower,967 __isl_take isl_constraint *upper,968 __isl_take isl_basic_set *bset, void *user), void *user)969{970 isl_basic_set *context_i;971 isl_constraint *upper = NULL;972 int i;973 974 for (i = 0; i < bset->n_ineq; ++i) {975 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))976 continue;977 978 context_i = set_smallest_upper_bound(context, bset,979 abs_pos, n_upper, i);980 if (isl_basic_set_is_empty(context_i)) {981 isl_basic_set_free(context_i);982 continue;983 }984 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),985 &bset->ineq[i]);986 if (!upper || !context_i)987 goto error;988 if (fn(NULL, upper, context_i, user) < 0)989 break;990 }991 992 isl_basic_set_free(context);993 994 if (i < bset->n_ineq)995 return isl_stat_error;996 997 return isl_stat_ok;998error:999 isl_constraint_free(upper);1000 isl_basic_set_free(context_i);1001 isl_basic_set_free(context);1002 return isl_stat_error;1003}1004 1005static isl_stat foreach_lower_bound(__isl_keep isl_basic_set *bset,1006 enum isl_dim_type type, unsigned abs_pos,1007 __isl_take isl_basic_set *context, int n_lower,1008 isl_stat (*fn)(__isl_take isl_constraint *lower,1009 __isl_take isl_constraint *upper,1010 __isl_take isl_basic_set *bset, void *user), void *user)1011{1012 isl_basic_set *context_i;1013 isl_constraint *lower = NULL;1014 int i;1015 1016 for (i = 0; i < bset->n_ineq; ++i) {1017 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))1018 continue;1019 1020 context_i = set_largest_lower_bound(context, bset,1021 abs_pos, n_lower, i);1022 if (isl_basic_set_is_empty(context_i)) {1023 isl_basic_set_free(context_i);1024 continue;1025 }1026 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),1027 &bset->ineq[i]);1028 if (!lower || !context_i)1029 goto error;1030 if (fn(lower, NULL, context_i, user) < 0)1031 break;1032 }1033 1034 isl_basic_set_free(context);1035 1036 if (i < bset->n_ineq)1037 return isl_stat_error;1038 1039 return isl_stat_ok;1040error:1041 isl_constraint_free(lower);1042 isl_basic_set_free(context_i);1043 isl_basic_set_free(context);1044 return isl_stat_error;1045}1046 1047static isl_stat foreach_bound_pair(__isl_keep isl_basic_set *bset,1048 enum isl_dim_type type, unsigned abs_pos,1049 __isl_take isl_basic_set *context, int n_lower, int n_upper,1050 isl_stat (*fn)(__isl_take isl_constraint *lower,1051 __isl_take isl_constraint *upper,1052 __isl_take isl_basic_set *bset, void *user), void *user)1053{1054 isl_basic_set *context_i, *context_j;1055 isl_constraint *lower = NULL;1056 isl_constraint *upper = NULL;1057 int i, j;1058 1059 for (i = 0; i < bset->n_ineq; ++i) {1060 if (!isl_int_is_pos(bset->ineq[i][1 + abs_pos]))1061 continue;1062 1063 context_i = set_largest_lower_bound(context, bset,1064 abs_pos, n_lower, i);1065 if (isl_basic_set_is_empty(context_i)) {1066 isl_basic_set_free(context_i);1067 continue;1068 }1069 1070 for (j = 0; j < bset->n_ineq; ++j) {1071 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))1072 continue;1073 1074 context_j = set_smallest_upper_bound(context_i, bset,1075 abs_pos, n_upper, j);1076 context_j = isl_basic_set_extend_constraints(context_j,1077 0, 1);1078 context_j = add_larger_bound_constraint(context_j,1079 bset->ineq[i], bset->ineq[j], abs_pos, 0);1080 context_j = isl_basic_set_simplify(context_j);1081 context_j = isl_basic_set_finalize(context_j);1082 if (isl_basic_set_is_empty(context_j)) {1083 isl_basic_set_free(context_j);1084 continue;1085 }1086 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),1087 &bset->ineq[i]);1088 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),1089 &bset->ineq[j]);1090 if (!lower || !upper || !context_j)1091 goto error;1092 if (fn(lower, upper, context_j, user) < 0)1093 break;1094 }1095 1096 isl_basic_set_free(context_i);1097 1098 if (j < bset->n_ineq)1099 break;1100 }1101 1102 isl_basic_set_free(context);1103 1104 if (i < bset->n_ineq)1105 return isl_stat_error;1106 1107 return isl_stat_ok;1108error:1109 isl_constraint_free(lower);1110 isl_constraint_free(upper);1111 isl_basic_set_free(context_i);1112 isl_basic_set_free(context_j);1113 isl_basic_set_free(context);1114 return isl_stat_error;1115}1116 1117/* For each pair of lower and upper bounds on the variable "pos"1118 * of type "type", call "fn" with these lower and upper bounds and the1119 * set of constraints on the remaining variables where these bounds1120 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.1121 *1122 * If the designated variable is equal to an affine combination of the1123 * other variables then fn is called with both lower and upper1124 * set to the corresponding equality.1125 *1126 * If there is no lower (or upper) bound, then NULL is passed1127 * as the corresponding bound.1128 *1129 * We first check if the variable is involved in any equality.1130 * If not, we count the number of lower and upper bounds and1131 * act accordingly.1132 */1133isl_stat isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set *bset,1134 enum isl_dim_type type, unsigned pos,1135 isl_stat (*fn)(__isl_take isl_constraint *lower,1136 __isl_take isl_constraint *upper,1137 __isl_take isl_basic_set *bset, void *user), void *user)1138{1139 int i;1140 isl_constraint *lower = NULL;1141 isl_constraint *upper = NULL;1142 isl_basic_set *context = NULL;1143 unsigned abs_pos;1144 int n_lower, n_upper;1145 isl_size off;1146 1147 if (isl_basic_set_check_range(bset, type, pos, 1) < 0)1148 return isl_stat_error;1149 isl_assert(bset->ctx, type == isl_dim_param || type == isl_dim_set,1150 return isl_stat_error);1151 1152 off = isl_basic_set_var_offset(bset, type);1153 if (off < 0)1154 return isl_stat_error;1155 abs_pos = off + pos;1156 1157 for (i = 0; i < bset->n_eq; ++i) {1158 if (isl_int_is_zero(bset->eq[i][1 + abs_pos]))1159 continue;1160 1161 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),1162 &bset->eq[i]);1163 upper = isl_constraint_copy(lower);1164 context = isl_basic_set_remove_dims(isl_basic_set_copy(bset),1165 type, pos, 1);1166 if (!lower || !upper || !context)1167 goto error;1168 return fn(lower, upper, context, user);1169 }1170 1171 n_lower = 0;1172 n_upper = 0;1173 for (i = 0; i < bset->n_ineq; ++i) {1174 if (isl_int_is_pos(bset->ineq[i][1 + abs_pos]))1175 n_lower++;1176 else if (isl_int_is_neg(bset->ineq[i][1 + abs_pos]))1177 n_upper++;1178 }1179 1180 context = isl_basic_set_copy(bset);1181 context = isl_basic_set_cow(context);1182 if (!context)1183 goto error;1184 for (i = context->n_ineq - 1; i >= 0; --i)1185 if (!isl_int_is_zero(context->ineq[i][1 + abs_pos]))1186 isl_basic_set_drop_inequality(context, i);1187 1188 context = isl_basic_set_drop(context, type, pos, 1);1189 if (!n_lower && !n_upper)1190 return fn(NULL, NULL, context, user);1191 if (!n_lower)1192 return foreach_upper_bound(bset, type, abs_pos, context, n_upper,1193 fn, user);1194 if (!n_upper)1195 return foreach_lower_bound(bset, type, abs_pos, context, n_lower,1196 fn, user);1197 return foreach_bound_pair(bset, type, abs_pos, context, n_lower, n_upper,1198 fn, user);1199error:1200 isl_constraint_free(lower);1201 isl_constraint_free(upper);1202 isl_basic_set_free(context);1203 return isl_stat_error;1204}1205 1206__isl_give isl_aff *isl_constraint_get_bound(1207 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)1208{1209 isl_space *space;1210 isl_aff *aff;1211 isl_ctx *ctx;1212 1213 if (isl_constraint_check_range(constraint, type, pos, 1) < 0)1214 return NULL;1215 space = isl_constraint_peek_space(constraint);1216 if (isl_space_check_is_set(space) < 0)1217 return NULL;1218 1219 ctx = isl_constraint_get_ctx(constraint);1220 pos += offset(constraint, type);1221 if (isl_int_is_zero(constraint->v->el[pos]))1222 isl_die(ctx, isl_error_invalid,1223 "constraint does not define a bound on given dimension",1224 return NULL);1225 1226 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));1227 if (!aff)1228 return NULL;1229 1230 if (isl_int_is_neg(constraint->v->el[pos]))1231 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);1232 else1233 isl_seq_neg(aff->v->el + 1, constraint->v->el, aff->v->size - 1);1234 isl_int_set_si(aff->v->el[1 + pos], 0);1235 isl_int_abs(aff->v->el[0], constraint->v->el[pos]);1236 aff = isl_aff_normalize(aff);1237 1238 return aff;1239}1240 1241/* For an inequality constraint1242 *1243 * f >= 01244 *1245 * or an equality constraint1246 *1247 * f = 01248 *1249 * return the affine expression f.1250 */1251__isl_give isl_aff *isl_constraint_get_aff(1252 __isl_keep isl_constraint *constraint)1253{1254 isl_aff *aff;1255 1256 if (!constraint)1257 return NULL;1258 1259 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));1260 if (!aff)1261 return NULL;1262 1263 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);1264 isl_int_set_si(aff->v->el[0], 1);1265 1266 return aff;1267}1268 1269/* Construct an inequality (eq = 0) or equality (eq = 1) constraint from "aff".1270 * In particular, construct aff >= 0 or aff = 0.1271 *1272 * The denominator of "aff" can be ignored.1273 */1274static __isl_give isl_constraint *isl_constraint_alloc_aff(int eq,1275 __isl_take isl_aff *aff)1276{1277 isl_local_space *ls;1278 isl_vec *v;1279 1280 if (!aff)1281 return NULL;1282 ls = isl_aff_get_domain_local_space(aff);1283 v = isl_vec_drop_els(isl_vec_copy(aff->v), 0, 1);1284 isl_aff_free(aff);1285 1286 return isl_constraint_alloc_vec(eq, ls, v);1287}1288 1289/* Construct an equality constraint equating the given affine expression1290 * to zero.1291 */1292__isl_give isl_constraint *isl_equality_from_aff(__isl_take isl_aff *aff)1293{1294 return isl_constraint_alloc_aff(1, aff);1295}1296 1297/* Construct an inequality constraint enforcing the given affine expression1298 * to be non-negative.1299 */1300__isl_give isl_constraint *isl_inequality_from_aff(__isl_take isl_aff *aff)1301{1302 return isl_constraint_alloc_aff(0, aff);1303}1304 1305/* Compare two isl_constraints.1306 *1307 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"1308 * than "c2" and 0 if they are equal.1309 *1310 * The order is fairly arbitrary. We do consider constraints that only involve1311 * earlier dimensions as "smaller".1312 */1313int isl_constraint_plain_cmp(__isl_keep isl_constraint *c1,1314 __isl_keep isl_constraint *c2)1315{1316 int cmp;1317 int last1, last2;1318 1319 if (c1 == c2)1320 return 0;1321 if (!c1)1322 return -1;1323 if (!c2)1324 return 1;1325 cmp = isl_local_space_cmp(c1->ls, c2->ls);1326 if (cmp != 0)1327 return cmp;1328 1329 last1 = isl_seq_last_non_zero(c1->v->el + 1, c1->v->size - 1);1330 last2 = isl_seq_last_non_zero(c2->v->el + 1, c1->v->size - 1);1331 if (last1 != last2)1332 return last1 - last2;1333 1334 return isl_seq_cmp(c1->v->el, c2->v->el, c1->v->size);1335}1336 1337/* Compare two constraints based on their final (non-zero) coefficients.1338 * In particular, the constraint that involves later variables or1339 * that has a larger coefficient for a shared latest variable1340 * is considered "greater" than the other constraint.1341 *1342 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"1343 * than "c2" and 0 if they are equal.1344 *1345 * If the constraints live in different local spaces, then we cannot1346 * really compare the constraints so we compare the local spaces instead.1347 */1348int isl_constraint_cmp_last_non_zero(__isl_keep isl_constraint *c1,1349 __isl_keep isl_constraint *c2)1350{1351 int cmp;1352 int last1, last2;1353 1354 if (c1 == c2)1355 return 0;1356 if (!c1)1357 return -1;1358 if (!c2)1359 return 1;1360 cmp = isl_local_space_cmp(c1->ls, c2->ls);1361 if (cmp != 0)1362 return cmp;1363 1364 last1 = isl_seq_last_non_zero(c1->v->el + 1, c1->v->size - 1);1365 last2 = isl_seq_last_non_zero(c2->v->el + 1, c1->v->size - 1);1366 if (last1 != last2)1367 return last1 - last2;1368 if (last1 == -1)1369 return 0;1370 return isl_int_abs_cmp(c1->v->el[1 + last1], c2->v->el[1 + last2]);1371}1372