shared_outer: use isl_bool_not
[isl.git] / isl_constraint.c
blob70bd56836d84c9c04aadf60e341b5f1c7b1be05e
1 /*
2 * Copyright 2008-2009 Katholieke Universiteit Leuven
3 * Copyright 2010 INRIA Saclay
5 * Use of this software is governed by the MIT license
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
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>
22 #include <bset_to_bmap.c>
23 #include <bset_from_bmap.c>
25 #undef BASE
26 #define BASE constraint
28 #include <isl_list_templ.c>
30 isl_ctx *isl_constraint_get_ctx(__isl_keep isl_constraint *c)
32 return c ? isl_local_space_get_ctx(c->ls) : NULL;
35 static unsigned n(struct isl_constraint *c, enum isl_dim_type type)
37 return isl_local_space_dim(c->ls, type);
40 static unsigned offset(struct isl_constraint *c, enum isl_dim_type type)
42 return isl_local_space_offset(c->ls, type);
45 static unsigned basic_map_offset(__isl_keep isl_basic_map *bmap,
46 enum isl_dim_type type)
48 return type == isl_dim_div ? 1 + isl_space_dim(bmap->dim, isl_dim_all)
49 : 1 + isl_space_offset(bmap->dim, type);
52 static unsigned basic_set_offset(struct isl_basic_set *bset,
53 enum isl_dim_type type)
55 isl_space *dim = bset->dim;
56 switch (type) {
57 case isl_dim_param: return 1;
58 case isl_dim_in: return 1 + dim->nparam;
59 case isl_dim_out: return 1 + dim->nparam + dim->n_in;
60 case isl_dim_div: return 1 + dim->nparam + dim->n_in + dim->n_out;
61 default: return 0;
65 __isl_give isl_constraint *isl_constraint_alloc_vec(int eq,
66 __isl_take isl_local_space *ls, __isl_take isl_vec *v)
68 isl_constraint *constraint;
70 if (!ls || !v)
71 goto error;
73 constraint = isl_alloc_type(isl_vec_get_ctx(v), isl_constraint);
74 if (!constraint)
75 goto error;
77 constraint->ref = 1;
78 constraint->eq = eq;
79 constraint->ls = ls;
80 constraint->v = v;
82 return constraint;
83 error:
84 isl_local_space_free(ls);
85 isl_vec_free(v);
86 return NULL;
89 __isl_give isl_constraint *isl_constraint_alloc(int eq,
90 __isl_take isl_local_space *ls)
92 isl_ctx *ctx;
93 isl_vec *v;
95 if (!ls)
96 return NULL;
98 ctx = isl_local_space_get_ctx(ls);
99 v = isl_vec_alloc(ctx, 1 + isl_local_space_dim(ls, isl_dim_all));
100 v = isl_vec_clr(v);
101 return isl_constraint_alloc_vec(eq, ls, v);
104 struct isl_constraint *isl_basic_map_constraint(struct isl_basic_map *bmap,
105 isl_int **line)
107 int eq;
108 isl_ctx *ctx;
109 isl_vec *v;
110 isl_local_space *ls = NULL;
111 isl_constraint *constraint;
113 if (!bmap || !line)
114 goto error;
116 eq = line >= bmap->eq;
118 ctx = isl_basic_map_get_ctx(bmap);
119 ls = isl_basic_map_get_local_space(bmap);
120 v = isl_vec_alloc(ctx, 1 + isl_local_space_dim(ls, isl_dim_all));
121 if (!v)
122 goto error;
123 isl_seq_cpy(v->el, line[0], v->size);
124 constraint = isl_constraint_alloc_vec(eq, ls, v);
126 isl_basic_map_free(bmap);
127 return constraint;
128 error:
129 isl_local_space_free(ls);
130 isl_basic_map_free(bmap);
131 return NULL;
134 struct isl_constraint *isl_basic_set_constraint(struct isl_basic_set *bset,
135 isl_int **line)
137 return isl_basic_map_constraint(bset_to_bmap(bset), line);
140 __isl_give isl_constraint *isl_constraint_alloc_equality(
141 __isl_take isl_local_space *ls)
143 return isl_constraint_alloc(1, ls);
146 __isl_give isl_constraint *isl_constraint_alloc_inequality(
147 __isl_take isl_local_space *ls)
149 return isl_constraint_alloc(0, ls);
152 struct isl_constraint *isl_constraint_dup(struct isl_constraint *c)
154 if (!c)
155 return NULL;
157 return isl_constraint_alloc_vec(c->eq, isl_local_space_copy(c->ls),
158 isl_vec_copy(c->v));
161 struct isl_constraint *isl_constraint_cow(struct isl_constraint *c)
163 if (!c)
164 return NULL;
166 if (c->ref == 1)
167 return c;
168 c->ref--;
169 return isl_constraint_dup(c);
172 struct isl_constraint *isl_constraint_copy(struct isl_constraint *constraint)
174 if (!constraint)
175 return NULL;
177 constraint->ref++;
178 return constraint;
181 __isl_null isl_constraint *isl_constraint_free(__isl_take isl_constraint *c)
183 if (!c)
184 return NULL;
186 if (--c->ref > 0)
187 return NULL;
189 isl_local_space_free(c->ls);
190 isl_vec_free(c->v);
191 free(c);
193 return NULL;
196 /* Return the number of constraints in "bmap", i.e., the
197 * number of times isl_basic_map_foreach_constraint will
198 * call the callback.
200 int isl_basic_map_n_constraint(__isl_keep isl_basic_map *bmap)
202 if (!bmap)
203 return -1;
205 return bmap->n_eq + bmap->n_ineq;
208 /* Return the number of constraints in "bset", i.e., the
209 * number of times isl_basic_set_foreach_constraint will
210 * call the callback.
212 int isl_basic_set_n_constraint(__isl_keep isl_basic_set *bset)
214 return isl_basic_map_n_constraint(bset);
217 isl_stat isl_basic_map_foreach_constraint(__isl_keep isl_basic_map *bmap,
218 isl_stat (*fn)(__isl_take isl_constraint *c, void *user), void *user)
220 int i;
221 struct isl_constraint *c;
223 if (!bmap)
224 return isl_stat_error;
226 isl_assert(bmap->ctx, ISL_F_ISSET(bmap, ISL_BASIC_MAP_FINAL),
227 return isl_stat_error);
229 for (i = 0; i < bmap->n_eq; ++i) {
230 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
231 &bmap->eq[i]);
232 if (!c)
233 return isl_stat_error;
234 if (fn(c, user) < 0)
235 return isl_stat_error;
238 for (i = 0; i < bmap->n_ineq; ++i) {
239 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
240 &bmap->ineq[i]);
241 if (!c)
242 return isl_stat_error;
243 if (fn(c, user) < 0)
244 return isl_stat_error;
247 return isl_stat_ok;
250 isl_stat isl_basic_set_foreach_constraint(__isl_keep isl_basic_set *bset,
251 isl_stat (*fn)(__isl_take isl_constraint *c, void *user), void *user)
253 return isl_basic_map_foreach_constraint(bset_to_bmap(bset), fn, user);
256 /* Add the constraint to the list that "user" points to, if it is not
257 * a div constraint.
259 static isl_stat collect_constraint(__isl_take isl_constraint *constraint,
260 void *user)
262 isl_constraint_list **list = user;
264 if (isl_constraint_is_div_constraint(constraint))
265 isl_constraint_free(constraint);
266 else
267 *list = isl_constraint_list_add(*list, constraint);
269 return isl_stat_ok;
272 /* Return a list of constraints that, when combined, are equivalent
273 * to "bmap". The input is required to have only known divs.
275 * There is no need to include the div constraints as they are
276 * implied by the div expressions.
278 __isl_give isl_constraint_list *isl_basic_map_get_constraint_list(
279 __isl_keep isl_basic_map *bmap)
281 int n;
282 isl_bool known;
283 isl_ctx *ctx;
284 isl_constraint_list *list;
286 known = isl_basic_map_divs_known(bmap);
287 if (known < 0)
288 return NULL;
289 ctx = isl_basic_map_get_ctx(bmap);
290 if (!known)
291 isl_die(ctx, isl_error_invalid,
292 "input involves unknown divs", return NULL);
294 n = isl_basic_map_n_constraint(bmap);
295 list = isl_constraint_list_alloc(ctx, n);
296 if (isl_basic_map_foreach_constraint(bmap,
297 &collect_constraint, &list) < 0)
298 list = isl_constraint_list_free(list);
300 return list;
303 /* Return a list of constraints that, when combined, are equivalent
304 * to "bset". The input is required to have only known divs.
306 __isl_give isl_constraint_list *isl_basic_set_get_constraint_list(
307 __isl_keep isl_basic_set *bset)
309 return isl_basic_map_get_constraint_list(bset);
312 int isl_constraint_is_equal(struct isl_constraint *constraint1,
313 struct isl_constraint *constraint2)
315 int equal;
317 if (!constraint1 || !constraint2)
318 return 0;
319 if (constraint1->eq != constraint2->eq)
320 return 0;
321 equal = isl_local_space_is_equal(constraint1->ls, constraint2->ls);
322 if (equal < 0 || !equal)
323 return equal;
324 return isl_vec_is_equal(constraint1->v, constraint2->v);
327 struct isl_basic_map *isl_basic_map_add_constraint(
328 struct isl_basic_map *bmap, struct isl_constraint *constraint)
330 isl_ctx *ctx;
331 isl_space *space;
332 int equal_space;
334 if (!bmap || !constraint)
335 goto error;
337 ctx = isl_constraint_get_ctx(constraint);
338 space = isl_constraint_get_space(constraint);
339 equal_space = isl_space_is_equal(bmap->dim, space);
340 isl_space_free(space);
341 isl_assert(ctx, equal_space, goto error);
343 bmap = isl_basic_map_intersect(bmap,
344 isl_basic_map_from_constraint(constraint));
345 return bmap;
346 error:
347 isl_basic_map_free(bmap);
348 isl_constraint_free(constraint);
349 return NULL;
352 struct isl_basic_set *isl_basic_set_add_constraint(
353 struct isl_basic_set *bset, struct isl_constraint *constraint)
355 return bset_from_bmap(isl_basic_map_add_constraint(bset_to_bmap(bset),
356 constraint));
359 __isl_give isl_map *isl_map_add_constraint(__isl_take isl_map *map,
360 __isl_take isl_constraint *constraint)
362 isl_basic_map *bmap;
364 bmap = isl_basic_map_from_constraint(constraint);
365 map = isl_map_intersect(map, isl_map_from_basic_map(bmap));
367 return map;
370 __isl_give isl_set *isl_set_add_constraint(__isl_take isl_set *set,
371 __isl_take isl_constraint *constraint)
373 return isl_map_add_constraint(set, constraint);
376 /* Return the space of "constraint".
378 static __isl_keep isl_space *isl_constraint_peek_space(
379 __isl_keep isl_constraint *constraint)
381 return constraint ? isl_local_space_peek_space(constraint->ls) : NULL;
384 __isl_give isl_space *isl_constraint_get_space(
385 __isl_keep isl_constraint *constraint)
387 return constraint ? isl_local_space_get_space(constraint->ls) : NULL;
390 __isl_give isl_local_space *isl_constraint_get_local_space(
391 __isl_keep isl_constraint *constraint)
393 return constraint ? isl_local_space_copy(constraint->ls) : NULL;
396 int isl_constraint_dim(__isl_keep isl_constraint *constraint,
397 enum isl_dim_type type)
399 if (!constraint)
400 return -1;
401 return n(constraint, type);
404 isl_bool isl_constraint_involves_dims(__isl_keep isl_constraint *constraint,
405 enum isl_dim_type type, unsigned first, unsigned n)
407 int i;
408 isl_ctx *ctx;
409 int *active = NULL;
410 isl_bool involves = isl_bool_false;
412 if (!constraint)
413 return isl_bool_error;
414 if (n == 0)
415 return isl_bool_false;
417 ctx = isl_constraint_get_ctx(constraint);
418 if (first + n > isl_constraint_dim(constraint, type))
419 isl_die(ctx, isl_error_invalid,
420 "range out of bounds", return isl_bool_error);
422 active = isl_local_space_get_active(constraint->ls,
423 constraint->v->el + 1);
424 if (!active)
425 goto error;
427 first += isl_local_space_offset(constraint->ls, type) - 1;
428 for (i = 0; i < n; ++i)
429 if (active[first + i]) {
430 involves = isl_bool_true;
431 break;
434 free(active);
436 return involves;
437 error:
438 free(active);
439 return isl_bool_error;
442 /* Does the given constraint represent a lower bound on the given
443 * dimension?
445 isl_bool isl_constraint_is_lower_bound(__isl_keep isl_constraint *constraint,
446 enum isl_dim_type type, unsigned pos)
448 if (!constraint)
449 return isl_bool_error;
451 if (pos >= isl_local_space_dim(constraint->ls, type))
452 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
453 "position out of bounds", return isl_bool_error);
455 pos += isl_local_space_offset(constraint->ls, type);
456 return isl_int_is_pos(constraint->v->el[pos]);
459 /* Does the given constraint represent an upper bound on the given
460 * dimension?
462 isl_bool isl_constraint_is_upper_bound(__isl_keep isl_constraint *constraint,
463 enum isl_dim_type type, unsigned pos)
465 if (!constraint)
466 return isl_bool_error;
468 if (pos >= isl_local_space_dim(constraint->ls, type))
469 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
470 "position out of bounds", return isl_bool_error);
472 pos += isl_local_space_offset(constraint->ls, type);
473 return isl_int_is_neg(constraint->v->el[pos]);
476 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint *constraint,
477 enum isl_dim_type type, unsigned pos)
479 return constraint ?
480 isl_local_space_get_dim_name(constraint->ls, type, pos) : NULL;
483 void isl_constraint_get_constant(__isl_keep isl_constraint *constraint,
484 isl_int *v)
486 if (!constraint)
487 return;
488 isl_int_set(*v, constraint->v->el[0]);
491 /* Return the constant term of "constraint".
493 __isl_give isl_val *isl_constraint_get_constant_val(
494 __isl_keep isl_constraint *constraint)
496 isl_ctx *ctx;
498 if (!constraint)
499 return NULL;
501 ctx = isl_constraint_get_ctx(constraint);
502 return isl_val_int_from_isl_int(ctx, constraint->v->el[0]);
505 void isl_constraint_get_coefficient(struct isl_constraint *constraint,
506 enum isl_dim_type type, int pos, isl_int *v)
508 if (!constraint)
509 return;
511 if (pos >= isl_local_space_dim(constraint->ls, type))
512 isl_die(constraint->v->ctx, isl_error_invalid,
513 "position out of bounds", return);
515 pos += isl_local_space_offset(constraint->ls, type);
516 isl_int_set(*v, constraint->v->el[pos]);
519 /* Return the coefficient of the variable of type "type" at position "pos"
520 * of "constraint".
522 __isl_give isl_val *isl_constraint_get_coefficient_val(
523 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
525 isl_ctx *ctx;
527 if (!constraint)
528 return NULL;
530 ctx = isl_constraint_get_ctx(constraint);
531 if (pos < 0 || pos >= isl_local_space_dim(constraint->ls, type))
532 isl_die(ctx, isl_error_invalid,
533 "position out of bounds", return NULL);
535 pos += isl_local_space_offset(constraint->ls, type);
536 return isl_val_int_from_isl_int(ctx, constraint->v->el[pos]);
539 __isl_give isl_aff *isl_constraint_get_div(__isl_keep isl_constraint *constraint,
540 int pos)
542 if (!constraint)
543 return NULL;
545 return isl_local_space_get_div(constraint->ls, pos);
548 __isl_give isl_constraint *isl_constraint_set_constant(
549 __isl_take isl_constraint *constraint, isl_int v)
551 constraint = isl_constraint_cow(constraint);
552 if (!constraint)
553 return NULL;
555 constraint->v = isl_vec_cow(constraint->v);
556 if (!constraint->v)
557 return isl_constraint_free(constraint);
559 isl_int_set(constraint->v->el[0], v);
560 return constraint;
563 /* Replace the constant term of "constraint" by "v".
565 __isl_give isl_constraint *isl_constraint_set_constant_val(
566 __isl_take isl_constraint *constraint, __isl_take isl_val *v)
568 constraint = isl_constraint_cow(constraint);
569 if (!constraint || !v)
570 goto error;
571 if (!isl_val_is_int(v))
572 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
573 "expecting integer value", goto error);
574 constraint->v = isl_vec_set_element_val(constraint->v, 0, v);
575 if (!constraint->v)
576 constraint = isl_constraint_free(constraint);
577 return constraint;
578 error:
579 isl_val_free(v);
580 return isl_constraint_free(constraint);
583 __isl_give isl_constraint *isl_constraint_set_constant_si(
584 __isl_take isl_constraint *constraint, int v)
586 constraint = isl_constraint_cow(constraint);
587 if (!constraint)
588 return NULL;
590 constraint->v = isl_vec_cow(constraint->v);
591 if (!constraint->v)
592 return isl_constraint_free(constraint);
594 isl_int_set_si(constraint->v->el[0], v);
595 return constraint;
598 __isl_give isl_constraint *isl_constraint_set_coefficient(
599 __isl_take isl_constraint *constraint,
600 enum isl_dim_type type, int pos, isl_int v)
602 constraint = isl_constraint_cow(constraint);
603 if (!constraint)
604 return NULL;
606 if (pos >= isl_local_space_dim(constraint->ls, type))
607 isl_die(constraint->v->ctx, isl_error_invalid,
608 "position out of bounds",
609 return isl_constraint_free(constraint));
611 constraint->v = isl_vec_cow(constraint->v);
612 if (!constraint->v)
613 return isl_constraint_free(constraint);
615 pos += isl_local_space_offset(constraint->ls, type);
616 isl_int_set(constraint->v->el[pos], v);
618 return constraint;
621 /* Replace the coefficient of the variable of type "type" at position "pos"
622 * of "constraint" by "v".
624 __isl_give isl_constraint *isl_constraint_set_coefficient_val(
625 __isl_take isl_constraint *constraint,
626 enum isl_dim_type type, int pos, __isl_take isl_val *v)
628 constraint = isl_constraint_cow(constraint);
629 if (!constraint || !v)
630 goto error;
631 if (!isl_val_is_int(v))
632 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
633 "expecting integer value", goto error);
635 if (pos >= isl_local_space_dim(constraint->ls, type))
636 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
637 "position out of bounds", goto error);
639 pos += isl_local_space_offset(constraint->ls, type);
640 constraint->v = isl_vec_set_element_val(constraint->v, pos, v);
641 if (!constraint->v)
642 constraint = isl_constraint_free(constraint);
643 return constraint;
644 error:
645 isl_val_free(v);
646 return isl_constraint_free(constraint);
649 __isl_give isl_constraint *isl_constraint_set_coefficient_si(
650 __isl_take isl_constraint *constraint,
651 enum isl_dim_type type, int pos, int v)
653 constraint = isl_constraint_cow(constraint);
654 if (!constraint)
655 return NULL;
657 if (pos >= isl_local_space_dim(constraint->ls, type))
658 isl_die(constraint->v->ctx, isl_error_invalid,
659 "position out of bounds",
660 return isl_constraint_free(constraint));
662 constraint->v = isl_vec_cow(constraint->v);
663 if (!constraint->v)
664 return isl_constraint_free(constraint);
666 pos += isl_local_space_offset(constraint->ls, type);
667 isl_int_set_si(constraint->v->el[pos], v);
669 return constraint;
672 struct isl_constraint *isl_constraint_negate(struct isl_constraint *constraint)
674 isl_ctx *ctx;
676 constraint = isl_constraint_cow(constraint);
677 if (!constraint)
678 return NULL;
680 ctx = isl_constraint_get_ctx(constraint);
681 if (isl_constraint_is_equality(constraint))
682 isl_die(ctx, isl_error_invalid, "cannot negate equality",
683 return isl_constraint_free(constraint));
684 constraint->v = isl_vec_neg(constraint->v);
685 constraint->v = isl_vec_cow(constraint->v);
686 if (!constraint->v)
687 return isl_constraint_free(constraint);
688 isl_int_sub_ui(constraint->v->el[0], constraint->v->el[0], 1);
689 return constraint;
692 isl_bool isl_constraint_is_equality(struct isl_constraint *constraint)
694 if (!constraint)
695 return isl_bool_error;
696 return constraint->eq;
699 int isl_constraint_is_div_constraint(__isl_keep isl_constraint *constraint)
701 int i;
702 int n_div;
704 if (!constraint)
705 return -1;
706 if (isl_constraint_is_equality(constraint))
707 return 0;
708 n_div = isl_constraint_dim(constraint, isl_dim_div);
709 for (i = 0; i < n_div; ++i) {
710 isl_bool is_div;
711 is_div = isl_local_space_is_div_constraint(constraint->ls,
712 constraint->v->el, i);
713 if (is_div < 0 || is_div)
714 return is_div;
717 return 0;
720 /* Is "constraint" an equality that corresponds to integer division "div"?
722 * That is, given an integer division of the form
724 * a = floor((f + c)/m)
726 * is the equality of the form
728 * -f + m d + c' = 0
730 * Note that the constant term is not checked explicitly, but given
731 * that this is a valid equality constraint, the constant c' necessarily
732 * has a value close to -c.
734 isl_bool isl_constraint_is_div_equality(__isl_keep isl_constraint *constraint,
735 unsigned div)
737 isl_bool equality;
739 equality = isl_constraint_is_equality(constraint);
740 if (equality < 0 || !equality)
741 return equality;
742 return isl_local_space_is_div_equality(constraint->ls,
743 constraint->v->el, div);
746 /* We manually set ISL_BASIC_SET_FINAL instead of calling
747 * isl_basic_map_finalize because we want to keep the position
748 * of the divs and we therefore do not want to throw away redundant divs.
749 * This is arguably a bit fragile.
751 __isl_give isl_basic_map *isl_basic_map_from_constraint(
752 __isl_take isl_constraint *constraint)
754 int k;
755 isl_local_space *ls;
756 struct isl_basic_map *bmap;
757 isl_int *c;
758 unsigned total;
760 if (!constraint)
761 return NULL;
763 ls = isl_local_space_copy(constraint->ls);
764 bmap = isl_basic_map_from_local_space(ls);
765 bmap = isl_basic_map_extend_constraints(bmap, 1, 1);
766 if (isl_constraint_is_equality(constraint)) {
767 k = isl_basic_map_alloc_equality(bmap);
768 if (k < 0)
769 goto error;
770 c = bmap->eq[k];
772 else {
773 k = isl_basic_map_alloc_inequality(bmap);
774 if (k < 0)
775 goto error;
776 c = bmap->ineq[k];
778 total = isl_basic_map_total_dim(bmap);
779 isl_seq_cpy(c, constraint->v->el, 1 + total);
780 isl_constraint_free(constraint);
781 if (bmap)
782 ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);
783 return bmap;
784 error:
785 isl_constraint_free(constraint);
786 isl_basic_map_free(bmap);
787 return NULL;
790 __isl_give isl_basic_set *isl_basic_set_from_constraint(
791 __isl_take isl_constraint *constraint)
793 isl_space *space;
795 space = isl_constraint_peek_space(constraint);
796 if (isl_space_check_is_set(space) < 0)
797 goto error;
798 return bset_from_bmap(isl_basic_map_from_constraint(constraint));
799 error:
800 isl_constraint_free(constraint);
801 return NULL;
804 /* Is the variable of "type" at position "pos" of "bmap" defined
805 * in terms of earlier dimensions through an equality?
807 * If so, and if c is not NULL, then return a copy of this equality in *c.
809 isl_bool isl_basic_map_has_defining_equality(
810 __isl_keep isl_basic_map *bmap, enum isl_dim_type type, int pos,
811 __isl_give isl_constraint **c)
813 int i;
814 unsigned offset;
815 unsigned total;
817 if (!bmap)
818 return isl_bool_error;
819 offset = basic_map_offset(bmap, type);
820 total = isl_basic_map_total_dim(bmap);
821 if (pos >= isl_basic_map_dim(bmap, type))
822 isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid,
823 "invalid position", return isl_bool_error);
824 for (i = 0; i < bmap->n_eq; ++i) {
825 if (isl_int_is_zero(bmap->eq[i][offset + pos]) ||
826 isl_seq_first_non_zero(bmap->eq[i]+offset+pos+1,
827 1+total-offset-pos-1) != -1)
828 continue;
829 if (c)
830 *c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
831 &bmap->eq[i]);
832 return isl_bool_true;
834 return isl_bool_false;
837 /* Is the variable of "type" at position "pos" of "bset" defined
838 * in terms of earlier dimensions through an equality?
840 * If so, and if c is not NULL, then return a copy of this equality in *c.
842 isl_bool isl_basic_set_has_defining_equality(
843 __isl_keep isl_basic_set *bset, enum isl_dim_type type, int pos,
844 __isl_give isl_constraint **c)
846 return isl_basic_map_has_defining_equality(bset_to_bmap(bset),
847 type, pos, c);
850 isl_bool isl_basic_set_has_defining_inequalities(
851 struct isl_basic_set *bset, enum isl_dim_type type, int pos,
852 struct isl_constraint **lower,
853 struct isl_constraint **upper)
855 int i, j;
856 unsigned offset;
857 unsigned total;
858 isl_int m;
859 isl_int **lower_line, **upper_line;
861 if (!bset)
862 return isl_bool_error;
863 offset = basic_set_offset(bset, type);
864 total = isl_basic_set_total_dim(bset);
865 if (pos >= isl_basic_set_dim(bset, type))
866 isl_die(isl_basic_set_get_ctx(bset), isl_error_invalid,
867 "invalid position", return isl_bool_error);
868 isl_int_init(m);
869 for (i = 0; i < bset->n_ineq; ++i) {
870 if (isl_int_is_zero(bset->ineq[i][offset + pos]))
871 continue;
872 if (isl_int_is_one(bset->ineq[i][offset + pos]))
873 continue;
874 if (isl_int_is_negone(bset->ineq[i][offset + pos]))
875 continue;
876 if (isl_seq_first_non_zero(bset->ineq[i]+offset+pos+1,
877 1+total-offset-pos-1) != -1)
878 continue;
879 for (j = i + 1; j < bset->n_ineq; ++j) {
880 if (!isl_seq_is_neg(bset->ineq[i]+1, bset->ineq[j]+1,
881 total))
882 continue;
883 isl_int_add(m, bset->ineq[i][0], bset->ineq[j][0]);
884 if (isl_int_abs_ge(m, bset->ineq[i][offset+pos]))
885 continue;
887 if (isl_int_is_pos(bset->ineq[i][offset+pos])) {
888 lower_line = &bset->ineq[i];
889 upper_line = &bset->ineq[j];
890 } else {
891 lower_line = &bset->ineq[j];
892 upper_line = &bset->ineq[i];
894 *lower = isl_basic_set_constraint(
895 isl_basic_set_copy(bset), lower_line);
896 *upper = isl_basic_set_constraint(
897 isl_basic_set_copy(bset), upper_line);
898 isl_int_clear(m);
899 return isl_bool_true;
902 *lower = NULL;
903 *upper = NULL;
904 isl_int_clear(m);
905 return isl_bool_false;
908 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
909 * (in "a" and "b"), add a constraint to "bset" that ensures that the
910 * bound implied by "a" is (strictly) larger than the bound implied by "b".
912 * If both constraints imply lower bounds, then this means that "a" is
913 * active in the result.
914 * If both constraints imply upper bounds, then this means that "b" is
915 * active in the result.
917 static __isl_give isl_basic_set *add_larger_bound_constraint(
918 __isl_take isl_basic_set *bset, isl_int *a, isl_int *b,
919 unsigned abs_pos, int strict)
921 int k;
922 isl_int t;
923 unsigned total;
925 k = isl_basic_set_alloc_inequality(bset);
926 if (k < 0)
927 goto error;
929 total = isl_basic_set_dim(bset, isl_dim_all);
931 isl_int_init(t);
932 isl_int_neg(t, b[1 + abs_pos]);
934 isl_seq_combine(bset->ineq[k], t, a, a[1 + abs_pos], b, 1 + abs_pos);
935 isl_seq_combine(bset->ineq[k] + 1 + abs_pos,
936 t, a + 1 + abs_pos + 1, a[1 + abs_pos], b + 1 + abs_pos + 1,
937 total - abs_pos);
939 if (strict)
940 isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
942 isl_int_clear(t);
944 return bset;
945 error:
946 isl_basic_set_free(bset);
947 return NULL;
950 /* Add constraints to "context" that ensure that "u" is the smallest
951 * (and therefore active) upper bound on "abs_pos" in "bset" and return
952 * the resulting basic set.
954 static __isl_give isl_basic_set *set_smallest_upper_bound(
955 __isl_keep isl_basic_set *context,
956 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_upper, int u)
958 int j;
960 context = isl_basic_set_copy(context);
961 context = isl_basic_set_cow(context);
963 context = isl_basic_set_extend_constraints(context, 0, n_upper - 1);
965 for (j = 0; j < bset->n_ineq; ++j) {
966 if (j == u)
967 continue;
968 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
969 continue;
970 context = add_larger_bound_constraint(context,
971 bset->ineq[j], bset->ineq[u], abs_pos, j > u);
974 context = isl_basic_set_simplify(context);
975 context = isl_basic_set_finalize(context);
977 return context;
980 /* Add constraints to "context" that ensure that "u" is the largest
981 * (and therefore active) upper bound on "abs_pos" in "bset" and return
982 * the resulting basic set.
984 static __isl_give isl_basic_set *set_largest_lower_bound(
985 __isl_keep isl_basic_set *context,
986 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_lower, int l)
988 int j;
990 context = isl_basic_set_copy(context);
991 context = isl_basic_set_cow(context);
993 context = isl_basic_set_extend_constraints(context, 0, n_lower - 1);
995 for (j = 0; j < bset->n_ineq; ++j) {
996 if (j == l)
997 continue;
998 if (!isl_int_is_pos(bset->ineq[j][1 + abs_pos]))
999 continue;
1000 context = add_larger_bound_constraint(context,
1001 bset->ineq[l], bset->ineq[j], abs_pos, j > l);
1004 context = isl_basic_set_simplify(context);
1005 context = isl_basic_set_finalize(context);
1007 return context;
1010 static isl_stat foreach_upper_bound(__isl_keep isl_basic_set *bset,
1011 enum isl_dim_type type, unsigned abs_pos,
1012 __isl_take isl_basic_set *context, int n_upper,
1013 isl_stat (*fn)(__isl_take isl_constraint *lower,
1014 __isl_take isl_constraint *upper,
1015 __isl_take isl_basic_set *bset, void *user), void *user)
1017 isl_basic_set *context_i;
1018 isl_constraint *upper = NULL;
1019 int i;
1021 for (i = 0; i < bset->n_ineq; ++i) {
1022 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
1023 continue;
1025 context_i = set_smallest_upper_bound(context, bset,
1026 abs_pos, n_upper, i);
1027 if (isl_basic_set_is_empty(context_i)) {
1028 isl_basic_set_free(context_i);
1029 continue;
1031 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
1032 &bset->ineq[i]);
1033 if (!upper || !context_i)
1034 goto error;
1035 if (fn(NULL, upper, context_i, user) < 0)
1036 break;
1039 isl_basic_set_free(context);
1041 if (i < bset->n_ineq)
1042 return isl_stat_error;
1044 return isl_stat_ok;
1045 error:
1046 isl_constraint_free(upper);
1047 isl_basic_set_free(context_i);
1048 isl_basic_set_free(context);
1049 return isl_stat_error;
1052 static isl_stat foreach_lower_bound(__isl_keep isl_basic_set *bset,
1053 enum isl_dim_type type, unsigned abs_pos,
1054 __isl_take isl_basic_set *context, int n_lower,
1055 isl_stat (*fn)(__isl_take isl_constraint *lower,
1056 __isl_take isl_constraint *upper,
1057 __isl_take isl_basic_set *bset, void *user), void *user)
1059 isl_basic_set *context_i;
1060 isl_constraint *lower = NULL;
1061 int i;
1063 for (i = 0; i < bset->n_ineq; ++i) {
1064 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
1065 continue;
1067 context_i = set_largest_lower_bound(context, bset,
1068 abs_pos, n_lower, i);
1069 if (isl_basic_set_is_empty(context_i)) {
1070 isl_basic_set_free(context_i);
1071 continue;
1073 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1074 &bset->ineq[i]);
1075 if (!lower || !context_i)
1076 goto error;
1077 if (fn(lower, NULL, context_i, user) < 0)
1078 break;
1081 isl_basic_set_free(context);
1083 if (i < bset->n_ineq)
1084 return isl_stat_error;
1086 return isl_stat_ok;
1087 error:
1088 isl_constraint_free(lower);
1089 isl_basic_set_free(context_i);
1090 isl_basic_set_free(context);
1091 return isl_stat_error;
1094 static isl_stat foreach_bound_pair(__isl_keep isl_basic_set *bset,
1095 enum isl_dim_type type, unsigned abs_pos,
1096 __isl_take isl_basic_set *context, int n_lower, int n_upper,
1097 isl_stat (*fn)(__isl_take isl_constraint *lower,
1098 __isl_take isl_constraint *upper,
1099 __isl_take isl_basic_set *bset, void *user), void *user)
1101 isl_basic_set *context_i, *context_j;
1102 isl_constraint *lower = NULL;
1103 isl_constraint *upper = NULL;
1104 int i, j;
1106 for (i = 0; i < bset->n_ineq; ++i) {
1107 if (!isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
1108 continue;
1110 context_i = set_largest_lower_bound(context, bset,
1111 abs_pos, n_lower, i);
1112 if (isl_basic_set_is_empty(context_i)) {
1113 isl_basic_set_free(context_i);
1114 continue;
1117 for (j = 0; j < bset->n_ineq; ++j) {
1118 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
1119 continue;
1121 context_j = set_smallest_upper_bound(context_i, bset,
1122 abs_pos, n_upper, j);
1123 context_j = isl_basic_set_extend_constraints(context_j,
1124 0, 1);
1125 context_j = add_larger_bound_constraint(context_j,
1126 bset->ineq[i], bset->ineq[j], abs_pos, 0);
1127 context_j = isl_basic_set_simplify(context_j);
1128 context_j = isl_basic_set_finalize(context_j);
1129 if (isl_basic_set_is_empty(context_j)) {
1130 isl_basic_set_free(context_j);
1131 continue;
1133 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1134 &bset->ineq[i]);
1135 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
1136 &bset->ineq[j]);
1137 if (!lower || !upper || !context_j)
1138 goto error;
1139 if (fn(lower, upper, context_j, user) < 0)
1140 break;
1143 isl_basic_set_free(context_i);
1145 if (j < bset->n_ineq)
1146 break;
1149 isl_basic_set_free(context);
1151 if (i < bset->n_ineq)
1152 return isl_stat_error;
1154 return isl_stat_ok;
1155 error:
1156 isl_constraint_free(lower);
1157 isl_constraint_free(upper);
1158 isl_basic_set_free(context_i);
1159 isl_basic_set_free(context_j);
1160 isl_basic_set_free(context);
1161 return isl_stat_error;
1164 /* For each pair of lower and upper bounds on the variable "pos"
1165 * of type "type", call "fn" with these lower and upper bounds and the
1166 * set of constraints on the remaining variables where these bounds
1167 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1169 * If the designated variable is equal to an affine combination of the
1170 * other variables then fn is called with both lower and upper
1171 * set to the corresponding equality.
1173 * If there is no lower (or upper) bound, then NULL is passed
1174 * as the corresponding bound.
1176 * We first check if the variable is involved in any equality.
1177 * If not, we count the number of lower and upper bounds and
1178 * act accordingly.
1180 isl_stat isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set *bset,
1181 enum isl_dim_type type, unsigned pos,
1182 isl_stat (*fn)(__isl_take isl_constraint *lower,
1183 __isl_take isl_constraint *upper,
1184 __isl_take isl_basic_set *bset, void *user), void *user)
1186 int i;
1187 isl_constraint *lower = NULL;
1188 isl_constraint *upper = NULL;
1189 isl_basic_set *context = NULL;
1190 unsigned abs_pos;
1191 int n_lower, n_upper;
1193 if (!bset)
1194 return isl_stat_error;
1195 isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type),
1196 return isl_stat_error);
1197 isl_assert(bset->ctx, type == isl_dim_param || type == isl_dim_set,
1198 return isl_stat_error);
1200 abs_pos = pos;
1201 if (type == isl_dim_set)
1202 abs_pos += isl_basic_set_dim(bset, isl_dim_param);
1204 for (i = 0; i < bset->n_eq; ++i) {
1205 if (isl_int_is_zero(bset->eq[i][1 + abs_pos]))
1206 continue;
1208 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1209 &bset->eq[i]);
1210 upper = isl_constraint_copy(lower);
1211 context = isl_basic_set_remove_dims(isl_basic_set_copy(bset),
1212 type, pos, 1);
1213 if (!lower || !upper || !context)
1214 goto error;
1215 return fn(lower, upper, context, user);
1218 n_lower = 0;
1219 n_upper = 0;
1220 for (i = 0; i < bset->n_ineq; ++i) {
1221 if (isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
1222 n_lower++;
1223 else if (isl_int_is_neg(bset->ineq[i][1 + abs_pos]))
1224 n_upper++;
1227 context = isl_basic_set_copy(bset);
1228 context = isl_basic_set_cow(context);
1229 if (!context)
1230 goto error;
1231 for (i = context->n_ineq - 1; i >= 0; --i)
1232 if (!isl_int_is_zero(context->ineq[i][1 + abs_pos]))
1233 isl_basic_set_drop_inequality(context, i);
1235 context = isl_basic_set_drop(context, type, pos, 1);
1236 if (!n_lower && !n_upper)
1237 return fn(NULL, NULL, context, user);
1238 if (!n_lower)
1239 return foreach_upper_bound(bset, type, abs_pos, context, n_upper,
1240 fn, user);
1241 if (!n_upper)
1242 return foreach_lower_bound(bset, type, abs_pos, context, n_lower,
1243 fn, user);
1244 return foreach_bound_pair(bset, type, abs_pos, context, n_lower, n_upper,
1245 fn, user);
1246 error:
1247 isl_constraint_free(lower);
1248 isl_constraint_free(upper);
1249 isl_basic_set_free(context);
1250 return isl_stat_error;
1253 __isl_give isl_aff *isl_constraint_get_bound(
1254 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
1256 isl_space *space;
1257 isl_aff *aff;
1258 isl_ctx *ctx;
1260 if (!constraint)
1261 return NULL;
1262 ctx = isl_constraint_get_ctx(constraint);
1263 if (pos >= isl_constraint_dim(constraint, type))
1264 isl_die(ctx, isl_error_invalid,
1265 "index out of bounds", return NULL);
1266 space = isl_constraint_peek_space(constraint);
1267 if (isl_space_check_is_set(space) < 0)
1268 return NULL;
1270 pos += offset(constraint, type);
1271 if (isl_int_is_zero(constraint->v->el[pos]))
1272 isl_die(ctx, isl_error_invalid,
1273 "constraint does not define a bound on given dimension",
1274 return NULL);
1276 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));
1277 if (!aff)
1278 return NULL;
1280 if (isl_int_is_neg(constraint->v->el[pos]))
1281 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1282 else
1283 isl_seq_neg(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1284 isl_int_set_si(aff->v->el[1 + pos], 0);
1285 isl_int_abs(aff->v->el[0], constraint->v->el[pos]);
1287 return aff;
1290 /* For an inequality constraint
1292 * f >= 0
1294 * or an equality constraint
1296 * f = 0
1298 * return the affine expression f.
1300 __isl_give isl_aff *isl_constraint_get_aff(
1301 __isl_keep isl_constraint *constraint)
1303 isl_aff *aff;
1305 if (!constraint)
1306 return NULL;
1308 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));
1309 if (!aff)
1310 return NULL;
1312 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1313 isl_int_set_si(aff->v->el[0], 1);
1315 return aff;
1318 /* Construct an inequality (eq = 0) or equality (eq = 1) constraint from "aff".
1319 * In particular, construct aff >= 0 or aff = 0.
1321 * The denominator of "aff" can be ignored.
1323 static __isl_give isl_constraint *isl_constraint_alloc_aff(int eq,
1324 __isl_take isl_aff *aff)
1326 isl_local_space *ls;
1327 isl_vec *v;
1329 if (!aff)
1330 return NULL;
1331 ls = isl_aff_get_domain_local_space(aff);
1332 v = isl_vec_drop_els(isl_vec_copy(aff->v), 0, 1);
1333 isl_aff_free(aff);
1335 return isl_constraint_alloc_vec(eq, ls, v);
1338 /* Construct an equality constraint equating the given affine expression
1339 * to zero.
1341 __isl_give isl_constraint *isl_equality_from_aff(__isl_take isl_aff *aff)
1343 return isl_constraint_alloc_aff(1, aff);
1346 /* Construct an inequality constraint enforcing the given affine expression
1347 * to be non-negative.
1349 __isl_give isl_constraint *isl_inequality_from_aff(__isl_take isl_aff *aff)
1351 return isl_constraint_alloc_aff(0, aff);
1354 /* Compare two isl_constraints.
1356 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1357 * than "c2" and 0 if they are equal.
1359 * The order is fairly arbitrary. We do consider constraints that only involve
1360 * earlier dimensions as "smaller".
1362 int isl_constraint_plain_cmp(__isl_keep isl_constraint *c1,
1363 __isl_keep isl_constraint *c2)
1365 int cmp;
1366 int last1, last2;
1368 if (c1 == c2)
1369 return 0;
1370 if (!c1)
1371 return -1;
1372 if (!c2)
1373 return 1;
1374 cmp = isl_local_space_cmp(c1->ls, c2->ls);
1375 if (cmp != 0)
1376 return cmp;
1378 last1 = isl_seq_last_non_zero(c1->v->el + 1, c1->v->size - 1);
1379 last2 = isl_seq_last_non_zero(c2->v->el + 1, c1->v->size - 1);
1380 if (last1 != last2)
1381 return last1 - last2;
1383 return isl_seq_cmp(c1->v->el, c2->v->el, c1->v->size);
1386 /* Compare two constraints based on their final (non-zero) coefficients.
1387 * In particular, the constraint that involves later variables or
1388 * that has a larger coefficient for a shared latest variable
1389 * is considered "greater" than the other constraint.
1391 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1392 * than "c2" and 0 if they are equal.
1394 * If the constraints live in different local spaces, then we cannot
1395 * really compare the constraints so we compare the local spaces instead.
1397 int isl_constraint_cmp_last_non_zero(__isl_keep isl_constraint *c1,
1398 __isl_keep isl_constraint *c2)
1400 int cmp;
1401 int last1, last2;
1403 if (c1 == c2)
1404 return 0;
1405 if (!c1)
1406 return -1;
1407 if (!c2)
1408 return 1;
1409 cmp = isl_local_space_cmp(c1->ls, c2->ls);
1410 if (cmp != 0)
1411 return cmp;
1413 last1 = isl_seq_last_non_zero(c1->v->el + 1, c1->v->size - 1);
1414 last2 = isl_seq_last_non_zero(c2->v->el + 1, c1->v->size - 1);
1415 if (last1 != last2)
1416 return last1 - last2;
1417 if (last1 == -1)
1418 return 0;
1419 return isl_int_abs_cmp(c1->v->el[1 + last1], c2->v->el[1 + last2]);