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 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
;
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
;
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
;
73 constraint
= isl_alloc_type(isl_vec_get_ctx(v
), isl_constraint
);
84 isl_local_space_free(ls
);
89 __isl_give isl_constraint
*isl_constraint_alloc(int eq
,
90 __isl_take isl_local_space
*ls
)
98 ctx
= isl_local_space_get_ctx(ls
);
99 v
= isl_vec_alloc(ctx
, 1 + isl_local_space_dim(ls
, isl_dim_all
));
101 return isl_constraint_alloc_vec(eq
, ls
, v
);
104 struct isl_constraint
*isl_basic_map_constraint(struct isl_basic_map
*bmap
,
110 isl_local_space
*ls
= NULL
;
111 isl_constraint
*constraint
;
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
));
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
);
129 isl_local_space_free(ls
);
130 isl_basic_map_free(bmap
);
134 struct isl_constraint
*isl_basic_set_constraint(struct isl_basic_set
*bset
,
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
)
157 return isl_constraint_alloc_vec(c
->eq
, isl_local_space_copy(c
->ls
),
161 struct isl_constraint
*isl_constraint_cow(struct isl_constraint
*c
)
169 return isl_constraint_dup(c
);
172 struct isl_constraint
*isl_constraint_copy(struct isl_constraint
*constraint
)
181 __isl_null isl_constraint
*isl_constraint_free(__isl_take isl_constraint
*c
)
189 isl_local_space_free(c
->ls
);
196 /* Return the number of constraints in "bmap", i.e., the
197 * number of times isl_basic_map_foreach_constraint will
200 int isl_basic_map_n_constraint(__isl_keep isl_basic_map
*bmap
)
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
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
)
221 struct isl_constraint
*c
;
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
),
233 return isl_stat_error
;
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
),
242 return isl_stat_error
;
244 return isl_stat_error
;
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
259 static isl_stat
collect_constraint(__isl_take isl_constraint
*constraint
,
262 isl_constraint_list
**list
= user
;
264 if (isl_constraint_is_div_constraint(constraint
))
265 isl_constraint_free(constraint
);
267 *list
= isl_constraint_list_add(*list
, constraint
);
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
)
284 isl_constraint_list
*list
;
286 known
= isl_basic_map_divs_known(bmap
);
289 ctx
= isl_basic_map_get_ctx(bmap
);
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
);
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
)
317 if (!constraint1
|| !constraint2
)
319 if (constraint1
->eq
!= constraint2
->eq
)
321 equal
= isl_local_space_is_equal(constraint1
->ls
, constraint2
->ls
);
322 if (equal
< 0 || !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
)
334 if (!bmap
|| !constraint
)
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
));
347 isl_basic_map_free(bmap
);
348 isl_constraint_free(constraint
);
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
),
359 __isl_give isl_map
*isl_map_add_constraint(__isl_take isl_map
*map
,
360 __isl_take isl_constraint
*constraint
)
364 bmap
= isl_basic_map_from_constraint(constraint
);
365 map
= isl_map_intersect(map
, isl_map_from_basic_map(bmap
));
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 __isl_give isl_space
*isl_constraint_get_space(
377 __isl_keep isl_constraint
*constraint
)
379 return constraint
? isl_local_space_get_space(constraint
->ls
) : NULL
;
382 __isl_give isl_local_space
*isl_constraint_get_local_space(
383 __isl_keep isl_constraint
*constraint
)
385 return constraint
? isl_local_space_copy(constraint
->ls
) : NULL
;
388 int isl_constraint_dim(__isl_keep isl_constraint
*constraint
,
389 enum isl_dim_type type
)
393 return n(constraint
, type
);
396 isl_bool
isl_constraint_involves_dims(__isl_keep isl_constraint
*constraint
,
397 enum isl_dim_type type
, unsigned first
, unsigned n
)
402 isl_bool involves
= isl_bool_false
;
405 return isl_bool_error
;
407 return isl_bool_false
;
409 ctx
= isl_constraint_get_ctx(constraint
);
410 if (first
+ n
> isl_constraint_dim(constraint
, type
))
411 isl_die(ctx
, isl_error_invalid
,
412 "range out of bounds", return isl_bool_error
);
414 active
= isl_local_space_get_active(constraint
->ls
,
415 constraint
->v
->el
+ 1);
419 first
+= isl_local_space_offset(constraint
->ls
, type
) - 1;
420 for (i
= 0; i
< n
; ++i
)
421 if (active
[first
+ i
]) {
422 involves
= isl_bool_true
;
431 return isl_bool_error
;
434 /* Does the given constraint represent a lower bound on the given
437 isl_bool
isl_constraint_is_lower_bound(__isl_keep isl_constraint
*constraint
,
438 enum isl_dim_type type
, unsigned pos
)
441 return isl_bool_error
;
443 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
444 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
445 "position out of bounds", return isl_bool_error
);
447 pos
+= isl_local_space_offset(constraint
->ls
, type
);
448 return isl_int_is_pos(constraint
->v
->el
[pos
]);
451 /* Does the given constraint represent an upper bound on the given
454 isl_bool
isl_constraint_is_upper_bound(__isl_keep isl_constraint
*constraint
,
455 enum isl_dim_type type
, unsigned pos
)
458 return isl_bool_error
;
460 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
461 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
462 "position out of bounds", return isl_bool_error
);
464 pos
+= isl_local_space_offset(constraint
->ls
, type
);
465 return isl_int_is_neg(constraint
->v
->el
[pos
]);
468 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint
*constraint
,
469 enum isl_dim_type type
, unsigned pos
)
472 isl_local_space_get_dim_name(constraint
->ls
, type
, pos
) : NULL
;
475 void isl_constraint_get_constant(__isl_keep isl_constraint
*constraint
,
480 isl_int_set(*v
, constraint
->v
->el
[0]);
483 /* Return the constant term of "constraint".
485 __isl_give isl_val
*isl_constraint_get_constant_val(
486 __isl_keep isl_constraint
*constraint
)
493 ctx
= isl_constraint_get_ctx(constraint
);
494 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[0]);
497 void isl_constraint_get_coefficient(struct isl_constraint
*constraint
,
498 enum isl_dim_type type
, int pos
, isl_int
*v
)
503 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
504 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
505 "position out of bounds", return);
507 pos
+= isl_local_space_offset(constraint
->ls
, type
);
508 isl_int_set(*v
, constraint
->v
->el
[pos
]);
511 /* Return the coefficient of the variable of type "type" at position "pos"
514 __isl_give isl_val
*isl_constraint_get_coefficient_val(
515 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
522 ctx
= isl_constraint_get_ctx(constraint
);
523 if (pos
< 0 || pos
>= isl_local_space_dim(constraint
->ls
, type
))
524 isl_die(ctx
, isl_error_invalid
,
525 "position out of bounds", return NULL
);
527 pos
+= isl_local_space_offset(constraint
->ls
, type
);
528 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[pos
]);
531 __isl_give isl_aff
*isl_constraint_get_div(__isl_keep isl_constraint
*constraint
,
537 return isl_local_space_get_div(constraint
->ls
, pos
);
540 __isl_give isl_constraint
*isl_constraint_set_constant(
541 __isl_take isl_constraint
*constraint
, isl_int v
)
543 constraint
= isl_constraint_cow(constraint
);
547 constraint
->v
= isl_vec_cow(constraint
->v
);
549 return isl_constraint_free(constraint
);
551 isl_int_set(constraint
->v
->el
[0], v
);
555 /* Replace the constant term of "constraint" by "v".
557 __isl_give isl_constraint
*isl_constraint_set_constant_val(
558 __isl_take isl_constraint
*constraint
, __isl_take isl_val
*v
)
560 constraint
= isl_constraint_cow(constraint
);
561 if (!constraint
|| !v
)
563 if (!isl_val_is_int(v
))
564 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
565 "expecting integer value", goto error
);
566 constraint
->v
= isl_vec_set_element_val(constraint
->v
, 0, v
);
568 constraint
= isl_constraint_free(constraint
);
572 return isl_constraint_free(constraint
);
575 __isl_give isl_constraint
*isl_constraint_set_constant_si(
576 __isl_take isl_constraint
*constraint
, int v
)
578 constraint
= isl_constraint_cow(constraint
);
582 constraint
->v
= isl_vec_cow(constraint
->v
);
584 return isl_constraint_free(constraint
);
586 isl_int_set_si(constraint
->v
->el
[0], v
);
590 __isl_give isl_constraint
*isl_constraint_set_coefficient(
591 __isl_take isl_constraint
*constraint
,
592 enum isl_dim_type type
, int pos
, isl_int v
)
594 constraint
= isl_constraint_cow(constraint
);
598 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
599 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
600 "position out of bounds",
601 return isl_constraint_free(constraint
));
603 constraint
->v
= isl_vec_cow(constraint
->v
);
605 return isl_constraint_free(constraint
);
607 pos
+= isl_local_space_offset(constraint
->ls
, type
);
608 isl_int_set(constraint
->v
->el
[pos
], v
);
613 /* Replace the coefficient of the variable of type "type" at position "pos"
614 * of "constraint" by "v".
616 __isl_give isl_constraint
*isl_constraint_set_coefficient_val(
617 __isl_take isl_constraint
*constraint
,
618 enum isl_dim_type type
, int pos
, __isl_take isl_val
*v
)
620 constraint
= isl_constraint_cow(constraint
);
621 if (!constraint
|| !v
)
623 if (!isl_val_is_int(v
))
624 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
625 "expecting integer value", goto error
);
627 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
628 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
629 "position out of bounds", goto error
);
631 pos
+= isl_local_space_offset(constraint
->ls
, type
);
632 constraint
->v
= isl_vec_set_element_val(constraint
->v
, pos
, v
);
634 constraint
= isl_constraint_free(constraint
);
638 return isl_constraint_free(constraint
);
641 __isl_give isl_constraint
*isl_constraint_set_coefficient_si(
642 __isl_take isl_constraint
*constraint
,
643 enum isl_dim_type type
, int pos
, int v
)
645 constraint
= isl_constraint_cow(constraint
);
649 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
650 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
651 "position out of bounds",
652 return isl_constraint_free(constraint
));
654 constraint
->v
= isl_vec_cow(constraint
->v
);
656 return isl_constraint_free(constraint
);
658 pos
+= isl_local_space_offset(constraint
->ls
, type
);
659 isl_int_set_si(constraint
->v
->el
[pos
], v
);
664 struct isl_constraint
*isl_constraint_negate(struct isl_constraint
*constraint
)
668 constraint
= isl_constraint_cow(constraint
);
672 ctx
= isl_constraint_get_ctx(constraint
);
673 if (isl_constraint_is_equality(constraint
))
674 isl_die(ctx
, isl_error_invalid
, "cannot negate equality",
675 return isl_constraint_free(constraint
));
676 constraint
->v
= isl_vec_neg(constraint
->v
);
677 constraint
->v
= isl_vec_cow(constraint
->v
);
679 return isl_constraint_free(constraint
);
680 isl_int_sub_ui(constraint
->v
->el
[0], constraint
->v
->el
[0], 1);
684 isl_bool
isl_constraint_is_equality(struct isl_constraint
*constraint
)
687 return isl_bool_error
;
688 return constraint
->eq
;
691 int isl_constraint_is_div_constraint(__isl_keep isl_constraint
*constraint
)
698 if (isl_constraint_is_equality(constraint
))
700 n_div
= isl_constraint_dim(constraint
, isl_dim_div
);
701 for (i
= 0; i
< n_div
; ++i
) {
703 is_div
= isl_local_space_is_div_constraint(constraint
->ls
,
704 constraint
->v
->el
, i
);
705 if (is_div
< 0 || is_div
)
712 /* Is "constraint" an equality that corresponds to integer division "div"?
714 * That is, given an integer division of the form
716 * a = floor((f + c)/m)
718 * is the equality of the form
722 * Note that the constant term is not checked explicitly, but given
723 * that this is a valid equality constraint, the constant c' necessarily
724 * has a value close to -c.
726 isl_bool
isl_constraint_is_div_equality(__isl_keep isl_constraint
*constraint
,
731 equality
= isl_constraint_is_equality(constraint
);
732 if (equality
< 0 || !equality
)
734 return isl_local_space_is_div_equality(constraint
->ls
,
735 constraint
->v
->el
, div
);
738 /* We manually set ISL_BASIC_SET_FINAL instead of calling
739 * isl_basic_map_finalize because we want to keep the position
740 * of the divs and we therefore do not want to throw away redundant divs.
741 * This is arguably a bit fragile.
743 __isl_give isl_basic_map
*isl_basic_map_from_constraint(
744 __isl_take isl_constraint
*constraint
)
748 struct isl_basic_map
*bmap
;
755 ls
= isl_local_space_copy(constraint
->ls
);
756 bmap
= isl_basic_map_from_local_space(ls
);
757 bmap
= isl_basic_map_extend_constraints(bmap
, 1, 1);
758 if (isl_constraint_is_equality(constraint
)) {
759 k
= isl_basic_map_alloc_equality(bmap
);
765 k
= isl_basic_map_alloc_inequality(bmap
);
770 total
= isl_basic_map_total_dim(bmap
);
771 isl_seq_cpy(c
, constraint
->v
->el
, 1 + total
);
772 isl_constraint_free(constraint
);
774 ISL_F_SET(bmap
, ISL_BASIC_SET_FINAL
);
777 isl_constraint_free(constraint
);
778 isl_basic_map_free(bmap
);
782 __isl_give isl_basic_set
*isl_basic_set_from_constraint(
783 __isl_take isl_constraint
*constraint
)
788 if (isl_constraint_dim(constraint
, isl_dim_in
) != 0)
789 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
790 "not a set constraint", goto error
);
791 return bset_from_bmap(isl_basic_map_from_constraint(constraint
));
793 isl_constraint_free(constraint
);
797 /* Is the variable of "type" at position "pos" of "bmap" defined
798 * in terms of earlier dimensions through an equality?
800 * If so, and if c is not NULL, then return a copy of this equality in *c.
802 isl_bool
isl_basic_map_has_defining_equality(
803 __isl_keep isl_basic_map
*bmap
, enum isl_dim_type type
, int pos
,
804 __isl_give isl_constraint
**c
)
811 return isl_bool_error
;
812 offset
= basic_map_offset(bmap
, type
);
813 total
= isl_basic_map_total_dim(bmap
);
814 if (pos
>= isl_basic_map_dim(bmap
, type
))
815 isl_die(isl_basic_map_get_ctx(bmap
), isl_error_invalid
,
816 "invalid position", return isl_bool_error
);
817 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
818 if (isl_int_is_zero(bmap
->eq
[i
][offset
+ pos
]) ||
819 isl_seq_first_non_zero(bmap
->eq
[i
]+offset
+pos
+1,
820 1+total
-offset
-pos
-1) != -1)
823 *c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
825 return isl_bool_true
;
827 return isl_bool_false
;
830 /* Is the variable of "type" at position "pos" of "bset" defined
831 * in terms of earlier dimensions through an equality?
833 * If so, and if c is not NULL, then return a copy of this equality in *c.
835 isl_bool
isl_basic_set_has_defining_equality(
836 __isl_keep isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
837 __isl_give isl_constraint
**c
)
839 return isl_basic_map_has_defining_equality(bset_to_bmap(bset
),
843 isl_bool
isl_basic_set_has_defining_inequalities(
844 struct isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
845 struct isl_constraint
**lower
,
846 struct isl_constraint
**upper
)
852 isl_int
**lower_line
, **upper_line
;
855 return isl_bool_error
;
856 offset
= basic_set_offset(bset
, type
);
857 total
= isl_basic_set_total_dim(bset
);
858 if (pos
>= isl_basic_set_dim(bset
, type
))
859 isl_die(isl_basic_set_get_ctx(bset
), isl_error_invalid
,
860 "invalid position", return isl_bool_error
);
862 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
863 if (isl_int_is_zero(bset
->ineq
[i
][offset
+ pos
]))
865 if (isl_int_is_one(bset
->ineq
[i
][offset
+ pos
]))
867 if (isl_int_is_negone(bset
->ineq
[i
][offset
+ pos
]))
869 if (isl_seq_first_non_zero(bset
->ineq
[i
]+offset
+pos
+1,
870 1+total
-offset
-pos
-1) != -1)
872 for (j
= i
+ 1; j
< bset
->n_ineq
; ++j
) {
873 if (!isl_seq_is_neg(bset
->ineq
[i
]+1, bset
->ineq
[j
]+1,
876 isl_int_add(m
, bset
->ineq
[i
][0], bset
->ineq
[j
][0]);
877 if (isl_int_abs_ge(m
, bset
->ineq
[i
][offset
+pos
]))
880 if (isl_int_is_pos(bset
->ineq
[i
][offset
+pos
])) {
881 lower_line
= &bset
->ineq
[i
];
882 upper_line
= &bset
->ineq
[j
];
884 lower_line
= &bset
->ineq
[j
];
885 upper_line
= &bset
->ineq
[i
];
887 *lower
= isl_basic_set_constraint(
888 isl_basic_set_copy(bset
), lower_line
);
889 *upper
= isl_basic_set_constraint(
890 isl_basic_set_copy(bset
), upper_line
);
892 return isl_bool_true
;
898 return isl_bool_false
;
901 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
902 * (in "a" and "b"), add a constraint to "bset" that ensures that the
903 * bound implied by "a" is (strictly) larger than the bound implied by "b".
905 * If both constraints imply lower bounds, then this means that "a" is
906 * active in the result.
907 * If both constraints imply upper bounds, then this means that "b" is
908 * active in the result.
910 static __isl_give isl_basic_set
*add_larger_bound_constraint(
911 __isl_take isl_basic_set
*bset
, isl_int
*a
, isl_int
*b
,
912 unsigned abs_pos
, int strict
)
918 k
= isl_basic_set_alloc_inequality(bset
);
922 total
= isl_basic_set_dim(bset
, isl_dim_all
);
925 isl_int_neg(t
, b
[1 + abs_pos
]);
927 isl_seq_combine(bset
->ineq
[k
], t
, a
, a
[1 + abs_pos
], b
, 1 + abs_pos
);
928 isl_seq_combine(bset
->ineq
[k
] + 1 + abs_pos
,
929 t
, a
+ 1 + abs_pos
+ 1, a
[1 + abs_pos
], b
+ 1 + abs_pos
+ 1,
933 isl_int_sub_ui(bset
->ineq
[k
][0], bset
->ineq
[k
][0], 1);
939 isl_basic_set_free(bset
);
943 /* Add constraints to "context" that ensure that "u" is the smallest
944 * (and therefore active) upper bound on "abs_pos" in "bset" and return
945 * the resulting basic set.
947 static __isl_give isl_basic_set
*set_smallest_upper_bound(
948 __isl_keep isl_basic_set
*context
,
949 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_upper
, int u
)
953 context
= isl_basic_set_copy(context
);
954 context
= isl_basic_set_cow(context
);
956 context
= isl_basic_set_extend_constraints(context
, 0, n_upper
- 1);
958 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
961 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
963 context
= add_larger_bound_constraint(context
,
964 bset
->ineq
[j
], bset
->ineq
[u
], abs_pos
, j
> u
);
967 context
= isl_basic_set_simplify(context
);
968 context
= isl_basic_set_finalize(context
);
973 /* Add constraints to "context" that ensure that "u" is the largest
974 * (and therefore active) upper bound on "abs_pos" in "bset" and return
975 * the resulting basic set.
977 static __isl_give isl_basic_set
*set_largest_lower_bound(
978 __isl_keep isl_basic_set
*context
,
979 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_lower
, int l
)
983 context
= isl_basic_set_copy(context
);
984 context
= isl_basic_set_cow(context
);
986 context
= isl_basic_set_extend_constraints(context
, 0, n_lower
- 1);
988 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
991 if (!isl_int_is_pos(bset
->ineq
[j
][1 + abs_pos
]))
993 context
= add_larger_bound_constraint(context
,
994 bset
->ineq
[l
], bset
->ineq
[j
], abs_pos
, j
> l
);
997 context
= isl_basic_set_simplify(context
);
998 context
= isl_basic_set_finalize(context
);
1003 static isl_stat
foreach_upper_bound(__isl_keep isl_basic_set
*bset
,
1004 enum isl_dim_type type
, unsigned abs_pos
,
1005 __isl_take isl_basic_set
*context
, int n_upper
,
1006 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1007 __isl_take isl_constraint
*upper
,
1008 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1010 isl_basic_set
*context_i
;
1011 isl_constraint
*upper
= NULL
;
1014 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1015 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1018 context_i
= set_smallest_upper_bound(context
, bset
,
1019 abs_pos
, n_upper
, i
);
1020 if (isl_basic_set_is_empty(context_i
)) {
1021 isl_basic_set_free(context_i
);
1024 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1026 if (!upper
|| !context_i
)
1028 if (fn(NULL
, upper
, context_i
, user
) < 0)
1032 isl_basic_set_free(context
);
1034 if (i
< bset
->n_ineq
)
1035 return isl_stat_error
;
1039 isl_constraint_free(upper
);
1040 isl_basic_set_free(context_i
);
1041 isl_basic_set_free(context
);
1042 return isl_stat_error
;
1045 static isl_stat
foreach_lower_bound(__isl_keep isl_basic_set
*bset
,
1046 enum isl_dim_type type
, unsigned abs_pos
,
1047 __isl_take isl_basic_set
*context
, int n_lower
,
1048 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1049 __isl_take isl_constraint
*upper
,
1050 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1052 isl_basic_set
*context_i
;
1053 isl_constraint
*lower
= NULL
;
1056 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1057 if (isl_int_is_zero(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
);
1066 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1068 if (!lower
|| !context_i
)
1070 if (fn(lower
, NULL
, context_i
, user
) < 0)
1074 isl_basic_set_free(context
);
1076 if (i
< bset
->n_ineq
)
1077 return isl_stat_error
;
1081 isl_constraint_free(lower
);
1082 isl_basic_set_free(context_i
);
1083 isl_basic_set_free(context
);
1084 return isl_stat_error
;
1087 static isl_stat
foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1088 enum isl_dim_type type
, unsigned abs_pos
,
1089 __isl_take isl_basic_set
*context
, int n_lower
, int n_upper
,
1090 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1091 __isl_take isl_constraint
*upper
,
1092 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1094 isl_basic_set
*context_i
, *context_j
;
1095 isl_constraint
*lower
= NULL
;
1096 isl_constraint
*upper
= NULL
;
1099 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1100 if (!isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1103 context_i
= set_largest_lower_bound(context
, bset
,
1104 abs_pos
, n_lower
, i
);
1105 if (isl_basic_set_is_empty(context_i
)) {
1106 isl_basic_set_free(context_i
);
1110 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
1111 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
1114 context_j
= set_smallest_upper_bound(context_i
, bset
,
1115 abs_pos
, n_upper
, j
);
1116 context_j
= isl_basic_set_extend_constraints(context_j
,
1118 context_j
= add_larger_bound_constraint(context_j
,
1119 bset
->ineq
[i
], bset
->ineq
[j
], abs_pos
, 0);
1120 context_j
= isl_basic_set_simplify(context_j
);
1121 context_j
= isl_basic_set_finalize(context_j
);
1122 if (isl_basic_set_is_empty(context_j
)) {
1123 isl_basic_set_free(context_j
);
1126 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1128 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1130 if (!lower
|| !upper
|| !context_j
)
1132 if (fn(lower
, upper
, context_j
, user
) < 0)
1136 isl_basic_set_free(context_i
);
1138 if (j
< bset
->n_ineq
)
1142 isl_basic_set_free(context
);
1144 if (i
< bset
->n_ineq
)
1145 return isl_stat_error
;
1149 isl_constraint_free(lower
);
1150 isl_constraint_free(upper
);
1151 isl_basic_set_free(context_i
);
1152 isl_basic_set_free(context_j
);
1153 isl_basic_set_free(context
);
1154 return isl_stat_error
;
1157 /* For each pair of lower and upper bounds on the variable "pos"
1158 * of type "type", call "fn" with these lower and upper bounds and the
1159 * set of constraints on the remaining variables where these bounds
1160 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1162 * If the designated variable is equal to an affine combination of the
1163 * other variables then fn is called with both lower and upper
1164 * set to the corresponding equality.
1166 * If there is no lower (or upper) bound, then NULL is passed
1167 * as the corresponding bound.
1169 * We first check if the variable is involved in any equality.
1170 * If not, we count the number of lower and upper bounds and
1173 isl_stat
isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1174 enum isl_dim_type type
, unsigned pos
,
1175 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1176 __isl_take isl_constraint
*upper
,
1177 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1180 isl_constraint
*lower
= NULL
;
1181 isl_constraint
*upper
= NULL
;
1182 isl_basic_set
*context
= NULL
;
1184 int n_lower
, n_upper
;
1187 return isl_stat_error
;
1188 isl_assert(bset
->ctx
, pos
< isl_basic_set_dim(bset
, type
),
1189 return isl_stat_error
);
1190 isl_assert(bset
->ctx
, type
== isl_dim_param
|| type
== isl_dim_set
,
1191 return isl_stat_error
);
1194 if (type
== isl_dim_set
)
1195 abs_pos
+= isl_basic_set_dim(bset
, isl_dim_param
);
1197 for (i
= 0; i
< bset
->n_eq
; ++i
) {
1198 if (isl_int_is_zero(bset
->eq
[i
][1 + abs_pos
]))
1201 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1203 upper
= isl_constraint_copy(lower
);
1204 context
= isl_basic_set_remove_dims(isl_basic_set_copy(bset
),
1206 if (!lower
|| !upper
|| !context
)
1208 return fn(lower
, upper
, context
, user
);
1213 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1214 if (isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1216 else if (isl_int_is_neg(bset
->ineq
[i
][1 + abs_pos
]))
1220 context
= isl_basic_set_copy(bset
);
1221 context
= isl_basic_set_cow(context
);
1224 for (i
= context
->n_ineq
- 1; i
>= 0; --i
)
1225 if (!isl_int_is_zero(context
->ineq
[i
][1 + abs_pos
]))
1226 isl_basic_set_drop_inequality(context
, i
);
1228 context
= isl_basic_set_drop(context
, type
, pos
, 1);
1229 if (!n_lower
&& !n_upper
)
1230 return fn(NULL
, NULL
, context
, user
);
1232 return foreach_upper_bound(bset
, type
, abs_pos
, context
, n_upper
,
1235 return foreach_lower_bound(bset
, type
, abs_pos
, context
, n_lower
,
1237 return foreach_bound_pair(bset
, type
, abs_pos
, context
, n_lower
, n_upper
,
1240 isl_constraint_free(lower
);
1241 isl_constraint_free(upper
);
1242 isl_basic_set_free(context
);
1243 return isl_stat_error
;
1246 __isl_give isl_aff
*isl_constraint_get_bound(
1247 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
1254 ctx
= isl_constraint_get_ctx(constraint
);
1255 if (pos
>= isl_constraint_dim(constraint
, type
))
1256 isl_die(ctx
, isl_error_invalid
,
1257 "index out of bounds", return NULL
);
1258 if (isl_constraint_dim(constraint
, isl_dim_in
) != 0)
1259 isl_die(ctx
, isl_error_invalid
,
1260 "not a set constraint", return NULL
);
1262 pos
+= offset(constraint
, type
);
1263 if (isl_int_is_zero(constraint
->v
->el
[pos
]))
1264 isl_die(ctx
, isl_error_invalid
,
1265 "constraint does not define a bound on given dimension",
1268 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
1272 if (isl_int_is_neg(constraint
->v
->el
[pos
]))
1273 isl_seq_cpy(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1275 isl_seq_neg(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1276 isl_int_set_si(aff
->v
->el
[1 + pos
], 0);
1277 isl_int_abs(aff
->v
->el
[0], constraint
->v
->el
[pos
]);
1282 /* For an inequality constraint
1286 * or an equality constraint
1290 * return the affine expression f.
1292 __isl_give isl_aff
*isl_constraint_get_aff(
1293 __isl_keep isl_constraint
*constraint
)
1300 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
1304 isl_seq_cpy(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1305 isl_int_set_si(aff
->v
->el
[0], 1);
1310 /* Construct an inequality (eq = 0) or equality (eq = 1) constraint from "aff".
1311 * In particular, construct aff >= 0 or aff = 0.
1313 * The denominator of "aff" can be ignored.
1315 static __isl_give isl_constraint
*isl_constraint_alloc_aff(int eq
,
1316 __isl_take isl_aff
*aff
)
1318 isl_local_space
*ls
;
1323 ls
= isl_aff_get_domain_local_space(aff
);
1324 v
= isl_vec_drop_els(isl_vec_copy(aff
->v
), 0, 1);
1327 return isl_constraint_alloc_vec(eq
, ls
, v
);
1330 /* Construct an equality constraint equating the given affine expression
1333 __isl_give isl_constraint
*isl_equality_from_aff(__isl_take isl_aff
*aff
)
1335 return isl_constraint_alloc_aff(1, aff
);
1338 /* Construct an inequality constraint enforcing the given affine expression
1339 * to be non-negative.
1341 __isl_give isl_constraint
*isl_inequality_from_aff(__isl_take isl_aff
*aff
)
1343 return isl_constraint_alloc_aff(0, aff
);
1346 /* Compare two isl_constraints.
1348 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1349 * than "c2" and 0 if they are equal.
1351 * The order is fairly arbitrary. We do consider constraints that only involve
1352 * earlier dimensions as "smaller".
1354 int isl_constraint_plain_cmp(__isl_keep isl_constraint
*c1
,
1355 __isl_keep isl_constraint
*c2
)
1366 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
1370 last1
= isl_seq_last_non_zero(c1
->v
->el
+ 1, c1
->v
->size
- 1);
1371 last2
= isl_seq_last_non_zero(c2
->v
->el
+ 1, c1
->v
->size
- 1);
1373 return last1
- last2
;
1375 return isl_seq_cmp(c1
->v
->el
, c2
->v
->el
, c1
->v
->size
);
1378 /* Compare two constraints based on their final (non-zero) coefficients.
1379 * In particular, the constraint that involves later variables or
1380 * that has a larger coefficient for a shared latest variable
1381 * is considered "greater" than the other constraint.
1383 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1384 * than "c2" and 0 if they are equal.
1386 * If the constraints live in different local spaces, then we cannot
1387 * really compare the constraints so we compare the local spaces instead.
1389 int isl_constraint_cmp_last_non_zero(__isl_keep isl_constraint
*c1
,
1390 __isl_keep isl_constraint
*c2
)
1401 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
1405 last1
= isl_seq_last_non_zero(c1
->v
->el
+ 1, c1
->v
->size
- 1);
1406 last2
= isl_seq_last_non_zero(c2
->v
->el
+ 1, c1
->v
->size
- 1);
1408 return last1
- last2
;
1411 return isl_int_abs_cmp(c1
->v
->el
[1 + last1
], c2
->v
->el
[1 + last2
]);