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>
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>
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 __isl_give isl_constraint
*isl_constraint_alloc_vec(int eq
,
46 __isl_take isl_local_space
*ls
, __isl_take isl_vec
*v
)
48 isl_constraint
*constraint
;
53 constraint
= isl_alloc_type(isl_vec_get_ctx(v
), isl_constraint
);
64 isl_local_space_free(ls
);
69 __isl_give isl_constraint
*isl_constraint_alloc(int eq
,
70 __isl_take isl_local_space
*ls
)
78 ctx
= isl_local_space_get_ctx(ls
);
79 v
= isl_vec_alloc(ctx
, 1 + isl_local_space_dim(ls
, isl_dim_all
));
81 return isl_constraint_alloc_vec(eq
, ls
, v
);
84 struct isl_constraint
*isl_basic_map_constraint(struct isl_basic_map
*bmap
,
90 isl_local_space
*ls
= NULL
;
91 isl_constraint
*constraint
;
96 eq
= line
>= bmap
->eq
;
98 ctx
= isl_basic_map_get_ctx(bmap
);
99 ls
= isl_basic_map_get_local_space(bmap
);
100 v
= isl_vec_alloc(ctx
, 1 + isl_local_space_dim(ls
, isl_dim_all
));
103 isl_seq_cpy(v
->el
, line
[0], v
->size
);
104 constraint
= isl_constraint_alloc_vec(eq
, ls
, v
);
106 isl_basic_map_free(bmap
);
109 isl_local_space_free(ls
);
110 isl_basic_map_free(bmap
);
114 struct isl_constraint
*isl_basic_set_constraint(struct isl_basic_set
*bset
,
117 return isl_basic_map_constraint(bset_to_bmap(bset
), line
);
120 __isl_give isl_constraint
*isl_constraint_alloc_equality(
121 __isl_take isl_local_space
*ls
)
123 return isl_constraint_alloc(1, ls
);
126 __isl_give isl_constraint
*isl_constraint_alloc_inequality(
127 __isl_take isl_local_space
*ls
)
129 return isl_constraint_alloc(0, ls
);
132 struct isl_constraint
*isl_constraint_dup(struct isl_constraint
*c
)
137 return isl_constraint_alloc_vec(c
->eq
, isl_local_space_copy(c
->ls
),
141 struct isl_constraint
*isl_constraint_cow(struct isl_constraint
*c
)
149 return isl_constraint_dup(c
);
152 struct isl_constraint
*isl_constraint_copy(struct isl_constraint
*constraint
)
161 __isl_null isl_constraint
*isl_constraint_free(__isl_take isl_constraint
*c
)
169 isl_local_space_free(c
->ls
);
176 /* Return the number of constraints in "bmap", i.e., the
177 * number of times isl_basic_map_foreach_constraint will
180 int isl_basic_map_n_constraint(__isl_keep isl_basic_map
*bmap
)
185 return bmap
->n_eq
+ bmap
->n_ineq
;
188 /* Return the number of constraints in "bset", i.e., the
189 * number of times isl_basic_set_foreach_constraint will
192 int isl_basic_set_n_constraint(__isl_keep isl_basic_set
*bset
)
194 return isl_basic_map_n_constraint(bset
);
197 isl_stat
isl_basic_map_foreach_constraint(__isl_keep isl_basic_map
*bmap
,
198 isl_stat (*fn
)(__isl_take isl_constraint
*c
, void *user
), void *user
)
201 struct isl_constraint
*c
;
204 return isl_stat_error
;
206 isl_assert(bmap
->ctx
, ISL_F_ISSET(bmap
, ISL_BASIC_MAP_FINAL
),
207 return isl_stat_error
);
209 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
210 c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
213 return isl_stat_error
;
215 return isl_stat_error
;
218 for (i
= 0; i
< bmap
->n_ineq
; ++i
) {
219 c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
222 return isl_stat_error
;
224 return isl_stat_error
;
230 isl_stat
isl_basic_set_foreach_constraint(__isl_keep isl_basic_set
*bset
,
231 isl_stat (*fn
)(__isl_take isl_constraint
*c
, void *user
), void *user
)
233 return isl_basic_map_foreach_constraint(bset_to_bmap(bset
), fn
, user
);
236 /* Add the constraint to the list that "user" points to, if it is not
239 static isl_stat
collect_constraint(__isl_take isl_constraint
*constraint
,
242 isl_constraint_list
**list
= user
;
245 is_div
= isl_constraint_is_div_constraint(constraint
);
246 if (is_div
< 0 || is_div
)
247 isl_constraint_free(constraint
);
249 *list
= isl_constraint_list_add(*list
, constraint
);
251 return is_div
< 0 ? isl_stat_error
: isl_stat_ok
;
254 /* Return a list of constraints that, when combined, are equivalent
255 * to "bmap". The input is required to have only known divs.
257 * There is no need to include the div constraints as they are
258 * implied by the div expressions.
260 __isl_give isl_constraint_list
*isl_basic_map_get_constraint_list(
261 __isl_keep isl_basic_map
*bmap
)
266 isl_constraint_list
*list
;
268 known
= isl_basic_map_divs_known(bmap
);
271 ctx
= isl_basic_map_get_ctx(bmap
);
273 isl_die(ctx
, isl_error_invalid
,
274 "input involves unknown divs", return NULL
);
276 n
= isl_basic_map_n_constraint(bmap
);
277 list
= isl_constraint_list_alloc(ctx
, n
);
278 if (isl_basic_map_foreach_constraint(bmap
,
279 &collect_constraint
, &list
) < 0)
280 list
= isl_constraint_list_free(list
);
285 /* Return a list of constraints that, when combined, are equivalent
286 * to "bset". The input is required to have only known divs.
288 __isl_give isl_constraint_list
*isl_basic_set_get_constraint_list(
289 __isl_keep isl_basic_set
*bset
)
291 return isl_basic_map_get_constraint_list(bset
);
294 int isl_constraint_is_equal(struct isl_constraint
*constraint1
,
295 struct isl_constraint
*constraint2
)
299 if (!constraint1
|| !constraint2
)
301 if (constraint1
->eq
!= constraint2
->eq
)
303 equal
= isl_local_space_is_equal(constraint1
->ls
, constraint2
->ls
);
304 if (equal
< 0 || !equal
)
306 return isl_vec_is_equal(constraint1
->v
, constraint2
->v
);
309 struct isl_basic_map
*isl_basic_map_add_constraint(
310 struct isl_basic_map
*bmap
, struct isl_constraint
*constraint
)
316 if (!bmap
|| !constraint
)
319 ctx
= isl_constraint_get_ctx(constraint
);
320 space
= isl_constraint_get_space(constraint
);
321 equal_space
= isl_space_is_equal(bmap
->dim
, space
);
322 isl_space_free(space
);
323 isl_assert(ctx
, equal_space
, goto error
);
325 bmap
= isl_basic_map_intersect(bmap
,
326 isl_basic_map_from_constraint(constraint
));
329 isl_basic_map_free(bmap
);
330 isl_constraint_free(constraint
);
334 struct isl_basic_set
*isl_basic_set_add_constraint(
335 struct isl_basic_set
*bset
, struct isl_constraint
*constraint
)
337 return bset_from_bmap(isl_basic_map_add_constraint(bset_to_bmap(bset
),
341 __isl_give isl_map
*isl_map_add_constraint(__isl_take isl_map
*map
,
342 __isl_take isl_constraint
*constraint
)
346 bmap
= isl_basic_map_from_constraint(constraint
);
347 map
= isl_map_intersect(map
, isl_map_from_basic_map(bmap
));
352 __isl_give isl_set
*isl_set_add_constraint(__isl_take isl_set
*set
,
353 __isl_take isl_constraint
*constraint
)
355 return isl_map_add_constraint(set
, constraint
);
358 /* Return the space of "constraint".
360 static __isl_keep isl_space
*isl_constraint_peek_space(
361 __isl_keep isl_constraint
*constraint
)
363 return constraint
? isl_local_space_peek_space(constraint
->ls
) : NULL
;
366 __isl_give isl_space
*isl_constraint_get_space(
367 __isl_keep isl_constraint
*constraint
)
369 return constraint
? isl_local_space_get_space(constraint
->ls
) : NULL
;
372 __isl_give isl_local_space
*isl_constraint_get_local_space(
373 __isl_keep isl_constraint
*constraint
)
375 return constraint
? isl_local_space_copy(constraint
->ls
) : NULL
;
378 int isl_constraint_dim(__isl_keep isl_constraint
*constraint
,
379 enum isl_dim_type type
)
383 return n(constraint
, type
);
387 #define TYPE isl_constraint
389 #include "check_type_range_templ.c"
391 isl_bool
isl_constraint_involves_dims(__isl_keep isl_constraint
*constraint
,
392 enum isl_dim_type type
, unsigned first
, unsigned n
)
396 isl_bool involves
= isl_bool_false
;
399 return isl_bool_error
;
401 return isl_bool_false
;
403 if (isl_constraint_check_range(constraint
, type
, first
, n
) < 0)
404 return isl_bool_error
;
406 active
= isl_local_space_get_active(constraint
->ls
,
407 constraint
->v
->el
+ 1);
411 first
+= isl_local_space_offset(constraint
->ls
, type
) - 1;
412 for (i
= 0; i
< n
; ++i
)
413 if (active
[first
+ i
]) {
414 involves
= isl_bool_true
;
423 return isl_bool_error
;
426 /* Does the given constraint represent a lower bound on the given
429 isl_bool
isl_constraint_is_lower_bound(__isl_keep isl_constraint
*constraint
,
430 enum isl_dim_type type
, unsigned pos
)
432 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
433 return isl_bool_error
;
435 pos
+= isl_local_space_offset(constraint
->ls
, type
);
436 return isl_int_is_pos(constraint
->v
->el
[pos
]);
439 /* Does the given constraint represent an upper bound on the given
442 isl_bool
isl_constraint_is_upper_bound(__isl_keep isl_constraint
*constraint
,
443 enum isl_dim_type type
, unsigned pos
)
445 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
446 return isl_bool_error
;
448 pos
+= isl_local_space_offset(constraint
->ls
, type
);
449 return isl_int_is_neg(constraint
->v
->el
[pos
]);
452 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint
*constraint
,
453 enum isl_dim_type type
, unsigned pos
)
456 isl_local_space_get_dim_name(constraint
->ls
, type
, pos
) : NULL
;
459 void isl_constraint_get_constant(__isl_keep isl_constraint
*constraint
,
464 isl_int_set(*v
, constraint
->v
->el
[0]);
467 /* Return the constant term of "constraint".
469 __isl_give isl_val
*isl_constraint_get_constant_val(
470 __isl_keep isl_constraint
*constraint
)
477 ctx
= isl_constraint_get_ctx(constraint
);
478 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[0]);
481 void isl_constraint_get_coefficient(struct isl_constraint
*constraint
,
482 enum isl_dim_type type
, int pos
, isl_int
*v
)
484 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
487 pos
+= isl_local_space_offset(constraint
->ls
, type
);
488 isl_int_set(*v
, constraint
->v
->el
[pos
]);
491 /* Return the coefficient of the variable of type "type" at position "pos"
494 __isl_give isl_val
*isl_constraint_get_coefficient_val(
495 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
499 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
502 ctx
= isl_constraint_get_ctx(constraint
);
503 pos
+= isl_local_space_offset(constraint
->ls
, type
);
504 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[pos
]);
507 __isl_give isl_aff
*isl_constraint_get_div(__isl_keep isl_constraint
*constraint
,
513 return isl_local_space_get_div(constraint
->ls
, pos
);
516 __isl_give isl_constraint
*isl_constraint_set_constant(
517 __isl_take isl_constraint
*constraint
, isl_int v
)
519 constraint
= isl_constraint_cow(constraint
);
523 constraint
->v
= isl_vec_cow(constraint
->v
);
525 return isl_constraint_free(constraint
);
527 isl_int_set(constraint
->v
->el
[0], v
);
531 /* Replace the constant term of "constraint" by "v".
533 __isl_give isl_constraint
*isl_constraint_set_constant_val(
534 __isl_take isl_constraint
*constraint
, __isl_take isl_val
*v
)
536 constraint
= isl_constraint_cow(constraint
);
537 if (!constraint
|| !v
)
539 if (!isl_val_is_int(v
))
540 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
541 "expecting integer value", goto error
);
542 constraint
->v
= isl_vec_set_element_val(constraint
->v
, 0, v
);
544 constraint
= isl_constraint_free(constraint
);
548 return isl_constraint_free(constraint
);
551 __isl_give isl_constraint
*isl_constraint_set_constant_si(
552 __isl_take isl_constraint
*constraint
, int v
)
554 constraint
= isl_constraint_cow(constraint
);
558 constraint
->v
= isl_vec_cow(constraint
->v
);
560 return isl_constraint_free(constraint
);
562 isl_int_set_si(constraint
->v
->el
[0], v
);
566 __isl_give isl_constraint
*isl_constraint_set_coefficient(
567 __isl_take isl_constraint
*constraint
,
568 enum isl_dim_type type
, int pos
, isl_int v
)
570 constraint
= isl_constraint_cow(constraint
);
571 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
572 return isl_constraint_free(constraint
);
574 constraint
->v
= isl_vec_cow(constraint
->v
);
576 return isl_constraint_free(constraint
);
578 pos
+= isl_local_space_offset(constraint
->ls
, type
);
579 isl_int_set(constraint
->v
->el
[pos
], v
);
584 /* Replace the coefficient of the variable of type "type" at position "pos"
585 * of "constraint" by "v".
587 __isl_give isl_constraint
*isl_constraint_set_coefficient_val(
588 __isl_take isl_constraint
*constraint
,
589 enum isl_dim_type type
, int pos
, __isl_take isl_val
*v
)
591 constraint
= isl_constraint_cow(constraint
);
592 if (!constraint
|| !v
)
594 if (!isl_val_is_int(v
))
595 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
596 "expecting integer value", goto error
);
597 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
600 pos
+= isl_local_space_offset(constraint
->ls
, type
);
601 constraint
->v
= isl_vec_set_element_val(constraint
->v
, pos
, v
);
603 constraint
= isl_constraint_free(constraint
);
607 return isl_constraint_free(constraint
);
610 __isl_give isl_constraint
*isl_constraint_set_coefficient_si(
611 __isl_take isl_constraint
*constraint
,
612 enum isl_dim_type type
, int pos
, int v
)
614 constraint
= isl_constraint_cow(constraint
);
615 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
616 return isl_constraint_free(constraint
);
618 constraint
->v
= isl_vec_cow(constraint
->v
);
620 return isl_constraint_free(constraint
);
622 pos
+= isl_local_space_offset(constraint
->ls
, type
);
623 isl_int_set_si(constraint
->v
->el
[pos
], v
);
628 struct isl_constraint
*isl_constraint_negate(struct isl_constraint
*constraint
)
632 constraint
= isl_constraint_cow(constraint
);
636 ctx
= isl_constraint_get_ctx(constraint
);
637 if (isl_constraint_is_equality(constraint
))
638 isl_die(ctx
, isl_error_invalid
, "cannot negate equality",
639 return isl_constraint_free(constraint
));
640 constraint
->v
= isl_vec_neg(constraint
->v
);
641 constraint
->v
= isl_vec_cow(constraint
->v
);
643 return isl_constraint_free(constraint
);
644 isl_int_sub_ui(constraint
->v
->el
[0], constraint
->v
->el
[0], 1);
648 isl_bool
isl_constraint_is_equality(struct isl_constraint
*constraint
)
651 return isl_bool_error
;
652 return constraint
->eq
;
655 isl_bool
isl_constraint_is_div_constraint(__isl_keep isl_constraint
*constraint
)
661 return isl_bool_error
;
662 if (isl_constraint_is_equality(constraint
))
663 return isl_bool_false
;
664 n_div
= isl_constraint_dim(constraint
, isl_dim_div
);
665 for (i
= 0; i
< n_div
; ++i
) {
667 is_div
= isl_local_space_is_div_constraint(constraint
->ls
,
668 constraint
->v
->el
, i
);
669 if (is_div
< 0 || is_div
)
673 return isl_bool_false
;
676 /* Is "constraint" an equality that corresponds to integer division "div"?
678 * That is, given an integer division of the form
680 * a = floor((f + c)/m)
682 * is the equality of the form
686 * Note that the constant term is not checked explicitly, but given
687 * that this is a valid equality constraint, the constant c' necessarily
688 * has a value close to -c.
690 isl_bool
isl_constraint_is_div_equality(__isl_keep isl_constraint
*constraint
,
695 equality
= isl_constraint_is_equality(constraint
);
696 if (equality
< 0 || !equality
)
698 return isl_local_space_is_div_equality(constraint
->ls
,
699 constraint
->v
->el
, div
);
702 /* We manually set ISL_BASIC_SET_FINAL instead of calling
703 * isl_basic_map_finalize because we want to keep the position
704 * of the divs and we therefore do not want to throw away redundant divs.
705 * This is arguably a bit fragile.
707 __isl_give isl_basic_map
*isl_basic_map_from_constraint(
708 __isl_take isl_constraint
*constraint
)
712 struct isl_basic_map
*bmap
;
719 ls
= isl_local_space_copy(constraint
->ls
);
720 bmap
= isl_basic_map_from_local_space(ls
);
721 bmap
= isl_basic_map_extend_constraints(bmap
, 1, 1);
722 if (isl_constraint_is_equality(constraint
)) {
723 k
= isl_basic_map_alloc_equality(bmap
);
729 k
= isl_basic_map_alloc_inequality(bmap
);
734 total
= isl_basic_map_total_dim(bmap
);
735 isl_seq_cpy(c
, constraint
->v
->el
, 1 + total
);
736 isl_constraint_free(constraint
);
738 ISL_F_SET(bmap
, ISL_BASIC_SET_FINAL
);
741 isl_constraint_free(constraint
);
742 isl_basic_map_free(bmap
);
746 __isl_give isl_basic_set
*isl_basic_set_from_constraint(
747 __isl_take isl_constraint
*constraint
)
751 space
= isl_constraint_peek_space(constraint
);
752 if (isl_space_check_is_set(space
) < 0)
754 return bset_from_bmap(isl_basic_map_from_constraint(constraint
));
756 isl_constraint_free(constraint
);
760 /* Is the variable of "type" at position "pos" of "bmap" defined
761 * in terms of earlier dimensions through an equality?
763 * If so, and if c is not NULL, then return a copy of this equality in *c.
765 isl_bool
isl_basic_map_has_defining_equality(
766 __isl_keep isl_basic_map
*bmap
, enum isl_dim_type type
, int pos
,
767 __isl_give isl_constraint
**c
)
773 if (isl_basic_map_check_range(bmap
, type
, pos
, 1) < 0)
774 return isl_bool_error
;
775 offset
= isl_basic_map_offset(bmap
, type
);
776 total
= isl_basic_map_total_dim(bmap
);
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)
783 *c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
785 return isl_bool_true
;
787 return isl_bool_false
;
790 /* Is the variable of "type" at position "pos" of "bset" defined
791 * in terms of earlier dimensions through an equality?
793 * If so, and if c is not NULL, then return a copy of this equality in *c.
795 isl_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
)
799 return isl_basic_map_has_defining_equality(bset_to_bmap(bset
),
803 isl_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
)
812 isl_int
**lower_line
, **upper_line
;
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_total_dim(bset
);
819 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
820 if (isl_int_is_zero(bset
->ineq
[i
][offset
+ pos
]))
822 if (isl_int_is_one(bset
->ineq
[i
][offset
+ pos
]))
824 if (isl_int_is_negone(bset
->ineq
[i
][offset
+ pos
]))
826 if (isl_seq_first_non_zero(bset
->ineq
[i
]+offset
+pos
+1,
827 1+total
-offset
-pos
-1) != -1)
829 for (j
= i
+ 1; j
< bset
->n_ineq
; ++j
) {
830 if (!isl_seq_is_neg(bset
->ineq
[i
]+1, bset
->ineq
[j
]+1,
833 isl_int_add(m
, bset
->ineq
[i
][0], bset
->ineq
[j
][0]);
834 if (isl_int_abs_ge(m
, bset
->ineq
[i
][offset
+pos
]))
837 if (isl_int_is_pos(bset
->ineq
[i
][offset
+pos
])) {
838 lower_line
= &bset
->ineq
[i
];
839 upper_line
= &bset
->ineq
[j
];
841 lower_line
= &bset
->ineq
[j
];
842 upper_line
= &bset
->ineq
[i
];
844 *lower
= isl_basic_set_constraint(
845 isl_basic_set_copy(bset
), lower_line
);
846 *upper
= isl_basic_set_constraint(
847 isl_basic_set_copy(bset
), upper_line
);
849 return isl_bool_true
;
855 return isl_bool_false
;
858 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
859 * (in "a" and "b"), add a constraint to "bset" that ensures that the
860 * bound implied by "a" is (strictly) larger than the bound implied by "b".
862 * If both constraints imply lower bounds, then this means that "a" is
863 * active in the result.
864 * If both constraints imply upper bounds, then this means that "b" is
865 * active in the result.
867 static __isl_give isl_basic_set
*add_larger_bound_constraint(
868 __isl_take isl_basic_set
*bset
, isl_int
*a
, isl_int
*b
,
869 unsigned abs_pos
, int strict
)
875 k
= isl_basic_set_alloc_inequality(bset
);
879 total
= isl_basic_set_dim(bset
, isl_dim_all
);
882 isl_int_neg(t
, b
[1 + abs_pos
]);
884 isl_seq_combine(bset
->ineq
[k
], t
, a
, a
[1 + abs_pos
], b
, 1 + abs_pos
);
885 isl_seq_combine(bset
->ineq
[k
] + 1 + abs_pos
,
886 t
, a
+ 1 + abs_pos
+ 1, a
[1 + abs_pos
], b
+ 1 + abs_pos
+ 1,
890 isl_int_sub_ui(bset
->ineq
[k
][0], bset
->ineq
[k
][0], 1);
896 isl_basic_set_free(bset
);
900 /* Add constraints to "context" that ensure that "u" is the smallest
901 * (and therefore active) upper bound on "abs_pos" in "bset" and return
902 * the resulting basic set.
904 static __isl_give isl_basic_set
*set_smallest_upper_bound(
905 __isl_keep isl_basic_set
*context
,
906 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_upper
, int u
)
910 context
= isl_basic_set_copy(context
);
911 context
= isl_basic_set_cow(context
);
913 context
= isl_basic_set_extend_constraints(context
, 0, n_upper
- 1);
915 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
918 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
920 context
= add_larger_bound_constraint(context
,
921 bset
->ineq
[j
], bset
->ineq
[u
], abs_pos
, j
> u
);
924 context
= isl_basic_set_simplify(context
);
925 context
= isl_basic_set_finalize(context
);
930 /* Add constraints to "context" that ensure that "u" is the largest
931 * (and therefore active) upper bound on "abs_pos" in "bset" and return
932 * the resulting basic set.
934 static __isl_give isl_basic_set
*set_largest_lower_bound(
935 __isl_keep isl_basic_set
*context
,
936 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_lower
, int l
)
940 context
= isl_basic_set_copy(context
);
941 context
= isl_basic_set_cow(context
);
943 context
= isl_basic_set_extend_constraints(context
, 0, n_lower
- 1);
945 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
948 if (!isl_int_is_pos(bset
->ineq
[j
][1 + abs_pos
]))
950 context
= add_larger_bound_constraint(context
,
951 bset
->ineq
[l
], bset
->ineq
[j
], abs_pos
, j
> l
);
954 context
= isl_basic_set_simplify(context
);
955 context
= isl_basic_set_finalize(context
);
960 static isl_stat
foreach_upper_bound(__isl_keep isl_basic_set
*bset
,
961 enum isl_dim_type type
, unsigned abs_pos
,
962 __isl_take isl_basic_set
*context
, int n_upper
,
963 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
964 __isl_take isl_constraint
*upper
,
965 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
967 isl_basic_set
*context_i
;
968 isl_constraint
*upper
= NULL
;
971 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
972 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
975 context_i
= set_smallest_upper_bound(context
, bset
,
976 abs_pos
, n_upper
, i
);
977 if (isl_basic_set_is_empty(context_i
)) {
978 isl_basic_set_free(context_i
);
981 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
983 if (!upper
|| !context_i
)
985 if (fn(NULL
, upper
, context_i
, user
) < 0)
989 isl_basic_set_free(context
);
991 if (i
< bset
->n_ineq
)
992 return isl_stat_error
;
996 isl_constraint_free(upper
);
997 isl_basic_set_free(context_i
);
998 isl_basic_set_free(context
);
999 return isl_stat_error
;
1002 static isl_stat
foreach_lower_bound(__isl_keep isl_basic_set
*bset
,
1003 enum isl_dim_type type
, unsigned abs_pos
,
1004 __isl_take isl_basic_set
*context
, int n_lower
,
1005 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1006 __isl_take isl_constraint
*upper
,
1007 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1009 isl_basic_set
*context_i
;
1010 isl_constraint
*lower
= NULL
;
1013 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1014 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1017 context_i
= set_largest_lower_bound(context
, bset
,
1018 abs_pos
, n_lower
, i
);
1019 if (isl_basic_set_is_empty(context_i
)) {
1020 isl_basic_set_free(context_i
);
1023 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1025 if (!lower
|| !context_i
)
1027 if (fn(lower
, NULL
, context_i
, user
) < 0)
1031 isl_basic_set_free(context
);
1033 if (i
< bset
->n_ineq
)
1034 return isl_stat_error
;
1038 isl_constraint_free(lower
);
1039 isl_basic_set_free(context_i
);
1040 isl_basic_set_free(context
);
1041 return isl_stat_error
;
1044 static isl_stat
foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1045 enum isl_dim_type type
, unsigned abs_pos
,
1046 __isl_take isl_basic_set
*context
, int n_lower
, int n_upper
,
1047 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1048 __isl_take isl_constraint
*upper
,
1049 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1051 isl_basic_set
*context_i
, *context_j
;
1052 isl_constraint
*lower
= NULL
;
1053 isl_constraint
*upper
= NULL
;
1056 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1057 if (!isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1060 context_i
= set_largest_lower_bound(context
, bset
,
1061 abs_pos
, n_lower
, i
);
1062 if (isl_basic_set_is_empty(context_i
)) {
1063 isl_basic_set_free(context_i
);
1067 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
1068 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
1071 context_j
= set_smallest_upper_bound(context_i
, bset
,
1072 abs_pos
, n_upper
, j
);
1073 context_j
= isl_basic_set_extend_constraints(context_j
,
1075 context_j
= add_larger_bound_constraint(context_j
,
1076 bset
->ineq
[i
], bset
->ineq
[j
], abs_pos
, 0);
1077 context_j
= isl_basic_set_simplify(context_j
);
1078 context_j
= isl_basic_set_finalize(context_j
);
1079 if (isl_basic_set_is_empty(context_j
)) {
1080 isl_basic_set_free(context_j
);
1083 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1085 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1087 if (!lower
|| !upper
|| !context_j
)
1089 if (fn(lower
, upper
, context_j
, user
) < 0)
1093 isl_basic_set_free(context_i
);
1095 if (j
< bset
->n_ineq
)
1099 isl_basic_set_free(context
);
1101 if (i
< bset
->n_ineq
)
1102 return isl_stat_error
;
1106 isl_constraint_free(lower
);
1107 isl_constraint_free(upper
);
1108 isl_basic_set_free(context_i
);
1109 isl_basic_set_free(context_j
);
1110 isl_basic_set_free(context
);
1111 return isl_stat_error
;
1114 /* For each pair of lower and upper bounds on the variable "pos"
1115 * of type "type", call "fn" with these lower and upper bounds and the
1116 * set of constraints on the remaining variables where these bounds
1117 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1119 * If the designated variable is equal to an affine combination of the
1120 * other variables then fn is called with both lower and upper
1121 * set to the corresponding equality.
1123 * If there is no lower (or upper) bound, then NULL is passed
1124 * as the corresponding bound.
1126 * We first check if the variable is involved in any equality.
1127 * If not, we count the number of lower and upper bounds and
1130 isl_stat
isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1131 enum isl_dim_type type
, unsigned pos
,
1132 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1133 __isl_take isl_constraint
*upper
,
1134 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1137 isl_constraint
*lower
= NULL
;
1138 isl_constraint
*upper
= NULL
;
1139 isl_basic_set
*context
= NULL
;
1141 int n_lower
, n_upper
;
1144 if (isl_basic_set_check_range(bset
, type
, pos
, 1) < 0)
1145 return isl_stat_error
;
1146 isl_assert(bset
->ctx
, type
== isl_dim_param
|| type
== isl_dim_set
,
1147 return isl_stat_error
);
1149 off
= isl_basic_set_var_offset(bset
, type
);
1151 return isl_stat_error
;
1152 abs_pos
= off
+ pos
;
1154 for (i
= 0; i
< bset
->n_eq
; ++i
) {
1155 if (isl_int_is_zero(bset
->eq
[i
][1 + abs_pos
]))
1158 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1160 upper
= isl_constraint_copy(lower
);
1161 context
= isl_basic_set_remove_dims(isl_basic_set_copy(bset
),
1163 if (!lower
|| !upper
|| !context
)
1165 return fn(lower
, upper
, context
, user
);
1170 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1171 if (isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1173 else if (isl_int_is_neg(bset
->ineq
[i
][1 + abs_pos
]))
1177 context
= isl_basic_set_copy(bset
);
1178 context
= isl_basic_set_cow(context
);
1181 for (i
= context
->n_ineq
- 1; i
>= 0; --i
)
1182 if (!isl_int_is_zero(context
->ineq
[i
][1 + abs_pos
]))
1183 isl_basic_set_drop_inequality(context
, i
);
1185 context
= isl_basic_set_drop(context
, type
, pos
, 1);
1186 if (!n_lower
&& !n_upper
)
1187 return fn(NULL
, NULL
, context
, user
);
1189 return foreach_upper_bound(bset
, type
, abs_pos
, context
, n_upper
,
1192 return foreach_lower_bound(bset
, type
, abs_pos
, context
, n_lower
,
1194 return foreach_bound_pair(bset
, type
, abs_pos
, context
, n_lower
, n_upper
,
1197 isl_constraint_free(lower
);
1198 isl_constraint_free(upper
);
1199 isl_basic_set_free(context
);
1200 return isl_stat_error
;
1203 __isl_give isl_aff
*isl_constraint_get_bound(
1204 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
1210 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
1212 space
= isl_constraint_peek_space(constraint
);
1213 if (isl_space_check_is_set(space
) < 0)
1216 ctx
= isl_constraint_get_ctx(constraint
);
1217 pos
+= offset(constraint
, type
);
1218 if (isl_int_is_zero(constraint
->v
->el
[pos
]))
1219 isl_die(ctx
, isl_error_invalid
,
1220 "constraint does not define a bound on given dimension",
1223 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
1227 if (isl_int_is_neg(constraint
->v
->el
[pos
]))
1228 isl_seq_cpy(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1230 isl_seq_neg(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1231 isl_int_set_si(aff
->v
->el
[1 + pos
], 0);
1232 isl_int_abs(aff
->v
->el
[0], constraint
->v
->el
[pos
]);
1237 /* For an inequality constraint
1241 * or an equality constraint
1245 * return the affine expression f.
1247 __isl_give isl_aff
*isl_constraint_get_aff(
1248 __isl_keep isl_constraint
*constraint
)
1255 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
1259 isl_seq_cpy(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1260 isl_int_set_si(aff
->v
->el
[0], 1);
1265 /* Construct an inequality (eq = 0) or equality (eq = 1) constraint from "aff".
1266 * In particular, construct aff >= 0 or aff = 0.
1268 * The denominator of "aff" can be ignored.
1270 static __isl_give isl_constraint
*isl_constraint_alloc_aff(int eq
,
1271 __isl_take isl_aff
*aff
)
1273 isl_local_space
*ls
;
1278 ls
= isl_aff_get_domain_local_space(aff
);
1279 v
= isl_vec_drop_els(isl_vec_copy(aff
->v
), 0, 1);
1282 return isl_constraint_alloc_vec(eq
, ls
, v
);
1285 /* Construct an equality constraint equating the given affine expression
1288 __isl_give isl_constraint
*isl_equality_from_aff(__isl_take isl_aff
*aff
)
1290 return isl_constraint_alloc_aff(1, aff
);
1293 /* Construct an inequality constraint enforcing the given affine expression
1294 * to be non-negative.
1296 __isl_give isl_constraint
*isl_inequality_from_aff(__isl_take isl_aff
*aff
)
1298 return isl_constraint_alloc_aff(0, aff
);
1301 /* Compare two isl_constraints.
1303 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1304 * than "c2" and 0 if they are equal.
1306 * The order is fairly arbitrary. We do consider constraints that only involve
1307 * earlier dimensions as "smaller".
1309 int isl_constraint_plain_cmp(__isl_keep isl_constraint
*c1
,
1310 __isl_keep isl_constraint
*c2
)
1321 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
1325 last1
= isl_seq_last_non_zero(c1
->v
->el
+ 1, c1
->v
->size
- 1);
1326 last2
= isl_seq_last_non_zero(c2
->v
->el
+ 1, c1
->v
->size
- 1);
1328 return last1
- last2
;
1330 return isl_seq_cmp(c1
->v
->el
, c2
->v
->el
, c1
->v
->size
);
1333 /* Compare two constraints based on their final (non-zero) coefficients.
1334 * In particular, the constraint that involves later variables or
1335 * that has a larger coefficient for a shared latest variable
1336 * is considered "greater" than the other constraint.
1338 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1339 * than "c2" and 0 if they are equal.
1341 * If the constraints live in different local spaces, then we cannot
1342 * really compare the constraints so we compare the local spaces instead.
1344 int isl_constraint_cmp_last_non_zero(__isl_keep isl_constraint
*c1
,
1345 __isl_keep isl_constraint
*c2
)
1356 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
1360 last1
= isl_seq_last_non_zero(c1
->v
->el
+ 1, c1
->v
->size
- 1);
1361 last2
= isl_seq_last_non_zero(c2
->v
->el
+ 1, c1
->v
->size
- 1);
1363 return last1
- last2
;
1366 return isl_int_abs_cmp(c1
->v
->el
[1 + last1
], c2
->v
->el
[1 + last2
]);