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 dim
= isl_constraint_get_space(constraint
);
339 equal_space
= isl_space_is_equal(bmap
->dim
, dim
);
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(struct 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
= isl_constraint_cow(constraint
);
607 constraint
->v
= isl_vec_cow(constraint
->v
);
609 return isl_constraint_free(constraint
);
611 pos
+= isl_local_space_offset(constraint
->ls
, type
);
612 isl_int_set(constraint
->v
->el
[pos
], v
);
617 /* Replace the coefficient of the variable of type "type" at position "pos"
618 * of "constraint" by "v".
620 __isl_give isl_constraint
*isl_constraint_set_coefficient_val(
621 __isl_take isl_constraint
*constraint
,
622 enum isl_dim_type type
, int pos
, __isl_take isl_val
*v
)
624 constraint
= isl_constraint_cow(constraint
);
625 if (!constraint
|| !v
)
627 if (!isl_val_is_int(v
))
628 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
629 "expecting integer value", goto error
);
631 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
632 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
633 "position out of bounds", goto error
);
635 pos
+= isl_local_space_offset(constraint
->ls
, type
);
636 constraint
->v
= isl_vec_set_element_val(constraint
->v
, pos
, v
);
638 constraint
= isl_constraint_free(constraint
);
642 return isl_constraint_free(constraint
);
645 __isl_give isl_constraint
*isl_constraint_set_coefficient_si(
646 __isl_take isl_constraint
*constraint
,
647 enum isl_dim_type type
, int pos
, int v
)
649 constraint
= isl_constraint_cow(constraint
);
653 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
654 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
655 "position out of bounds",
656 return isl_constraint_free(constraint
));
658 constraint
= isl_constraint_cow(constraint
);
662 constraint
->v
= isl_vec_cow(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
);
672 struct isl_constraint
*isl_constraint_negate(struct isl_constraint
*constraint
)
676 constraint
= isl_constraint_cow(constraint
);
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
);
687 return isl_constraint_free(constraint
);
688 isl_int_sub_ui(constraint
->v
->el
[0], constraint
->v
->el
[0], 1);
692 isl_bool
isl_constraint_is_equality(struct isl_constraint
*constraint
)
695 return isl_bool_error
;
696 return constraint
->eq
;
699 int isl_constraint_is_div_constraint(__isl_keep isl_constraint
*constraint
)
706 if (isl_constraint_is_equality(constraint
))
708 n_div
= isl_constraint_dim(constraint
, isl_dim_div
);
709 for (i
= 0; i
< n_div
; ++i
) {
711 is_div
= isl_local_space_is_div_constraint(constraint
->ls
,
712 constraint
->v
->el
, i
);
713 if (is_div
< 0 || is_div
)
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
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
,
739 equality
= isl_constraint_is_equality(constraint
);
740 if (equality
< 0 || !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
)
756 struct isl_basic_map
*bmap
;
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
);
773 k
= isl_basic_map_alloc_inequality(bmap
);
778 total
= isl_basic_map_total_dim(bmap
);
779 isl_seq_cpy(c
, constraint
->v
->el
, 1 + total
);
780 isl_constraint_free(constraint
);
782 ISL_F_SET(bmap
, ISL_BASIC_SET_FINAL
);
785 isl_constraint_free(constraint
);
786 isl_basic_map_free(bmap
);
790 __isl_give isl_basic_set
*isl_basic_set_from_constraint(
791 __isl_take isl_constraint
*constraint
)
796 if (isl_constraint_dim(constraint
, isl_dim_in
) != 0)
797 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
798 "not a set constraint", goto error
);
799 return bset_from_bmap(isl_basic_map_from_constraint(constraint
));
801 isl_constraint_free(constraint
);
805 /* Is the variable of "type" at position "pos" of "bmap" defined
806 * in terms of earlier dimensions through an equality?
808 * If so, and if c is not NULL, then return a copy of this equality in *c.
810 isl_bool
isl_basic_map_has_defining_equality(
811 __isl_keep isl_basic_map
*bmap
, enum isl_dim_type type
, int pos
,
812 __isl_give isl_constraint
**c
)
819 return isl_bool_error
;
820 offset
= basic_map_offset(bmap
, type
);
821 total
= isl_basic_map_total_dim(bmap
);
822 if (pos
>= isl_basic_map_dim(bmap
, type
))
823 isl_die(isl_basic_map_get_ctx(bmap
), isl_error_invalid
,
824 "invalid position", return isl_bool_error
);
825 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
826 if (isl_int_is_zero(bmap
->eq
[i
][offset
+ pos
]) ||
827 isl_seq_first_non_zero(bmap
->eq
[i
]+offset
+pos
+1,
828 1+total
-offset
-pos
-1) != -1)
831 *c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
833 return isl_bool_true
;
835 return isl_bool_false
;
838 /* Is the variable of "type" at position "pos" of "bset" defined
839 * in terms of earlier dimensions through an equality?
841 * If so, and if c is not NULL, then return a copy of this equality in *c.
843 isl_bool
isl_basic_set_has_defining_equality(
844 __isl_keep isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
845 __isl_give isl_constraint
**c
)
847 return isl_basic_map_has_defining_equality(bset_to_bmap(bset
),
851 isl_bool
isl_basic_set_has_defining_inequalities(
852 struct isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
853 struct isl_constraint
**lower
,
854 struct isl_constraint
**upper
)
860 isl_int
**lower_line
, **upper_line
;
863 return isl_bool_error
;
864 offset
= basic_set_offset(bset
, type
);
865 total
= isl_basic_set_total_dim(bset
);
866 if (pos
>= isl_basic_set_dim(bset
, type
))
867 isl_die(isl_basic_set_get_ctx(bset
), isl_error_invalid
,
868 "invalid position", return isl_bool_error
);
870 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
871 if (isl_int_is_zero(bset
->ineq
[i
][offset
+ pos
]))
873 if (isl_int_is_one(bset
->ineq
[i
][offset
+ pos
]))
875 if (isl_int_is_negone(bset
->ineq
[i
][offset
+ pos
]))
877 if (isl_seq_first_non_zero(bset
->ineq
[i
]+offset
+pos
+1,
878 1+total
-offset
-pos
-1) != -1)
880 for (j
= i
+ 1; j
< bset
->n_ineq
; ++j
) {
881 if (!isl_seq_is_neg(bset
->ineq
[i
]+1, bset
->ineq
[j
]+1,
884 isl_int_add(m
, bset
->ineq
[i
][0], bset
->ineq
[j
][0]);
885 if (isl_int_abs_ge(m
, bset
->ineq
[i
][offset
+pos
]))
888 if (isl_int_is_pos(bset
->ineq
[i
][offset
+pos
])) {
889 lower_line
= &bset
->ineq
[i
];
890 upper_line
= &bset
->ineq
[j
];
892 lower_line
= &bset
->ineq
[j
];
893 upper_line
= &bset
->ineq
[i
];
895 *lower
= isl_basic_set_constraint(
896 isl_basic_set_copy(bset
), lower_line
);
897 *upper
= isl_basic_set_constraint(
898 isl_basic_set_copy(bset
), upper_line
);
900 return isl_bool_true
;
906 return isl_bool_false
;
909 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
910 * (in "a" and "b"), add a constraint to "bset" that ensures that the
911 * bound implied by "a" is (strictly) larger than the bound implied by "b".
913 * If both constraints imply lower bounds, then this means that "a" is
914 * active in the result.
915 * If both constraints imply upper bounds, then this means that "b" is
916 * active in the result.
918 static __isl_give isl_basic_set
*add_larger_bound_constraint(
919 __isl_take isl_basic_set
*bset
, isl_int
*a
, isl_int
*b
,
920 unsigned abs_pos
, int strict
)
926 k
= isl_basic_set_alloc_inequality(bset
);
930 total
= isl_basic_set_dim(bset
, isl_dim_all
);
933 isl_int_neg(t
, b
[1 + abs_pos
]);
935 isl_seq_combine(bset
->ineq
[k
], t
, a
, a
[1 + abs_pos
], b
, 1 + abs_pos
);
936 isl_seq_combine(bset
->ineq
[k
] + 1 + abs_pos
,
937 t
, a
+ 1 + abs_pos
+ 1, a
[1 + abs_pos
], b
+ 1 + abs_pos
+ 1,
941 isl_int_sub_ui(bset
->ineq
[k
][0], bset
->ineq
[k
][0], 1);
947 isl_basic_set_free(bset
);
951 /* Add constraints to "context" that ensure that "u" is the smallest
952 * (and therefore active) upper bound on "abs_pos" in "bset" and return
953 * the resulting basic set.
955 static __isl_give isl_basic_set
*set_smallest_upper_bound(
956 __isl_keep isl_basic_set
*context
,
957 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_upper
, int u
)
961 context
= isl_basic_set_copy(context
);
962 context
= isl_basic_set_cow(context
);
964 context
= isl_basic_set_extend_constraints(context
, 0, n_upper
- 1);
966 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
969 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
971 context
= add_larger_bound_constraint(context
,
972 bset
->ineq
[j
], bset
->ineq
[u
], abs_pos
, j
> u
);
975 context
= isl_basic_set_simplify(context
);
976 context
= isl_basic_set_finalize(context
);
981 /* Add constraints to "context" that ensure that "u" is the largest
982 * (and therefore active) upper bound on "abs_pos" in "bset" and return
983 * the resulting basic set.
985 static __isl_give isl_basic_set
*set_largest_lower_bound(
986 __isl_keep isl_basic_set
*context
,
987 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_lower
, int l
)
991 context
= isl_basic_set_copy(context
);
992 context
= isl_basic_set_cow(context
);
994 context
= isl_basic_set_extend_constraints(context
, 0, n_lower
- 1);
996 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
999 if (!isl_int_is_pos(bset
->ineq
[j
][1 + abs_pos
]))
1001 context
= add_larger_bound_constraint(context
,
1002 bset
->ineq
[l
], bset
->ineq
[j
], abs_pos
, j
> l
);
1005 context
= isl_basic_set_simplify(context
);
1006 context
= isl_basic_set_finalize(context
);
1011 static isl_stat
foreach_upper_bound(__isl_keep isl_basic_set
*bset
,
1012 enum isl_dim_type type
, unsigned abs_pos
,
1013 __isl_take isl_basic_set
*context
, int n_upper
,
1014 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1015 __isl_take isl_constraint
*upper
,
1016 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1018 isl_basic_set
*context_i
;
1019 isl_constraint
*upper
= NULL
;
1022 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1023 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1026 context_i
= set_smallest_upper_bound(context
, bset
,
1027 abs_pos
, n_upper
, i
);
1028 if (isl_basic_set_is_empty(context_i
)) {
1029 isl_basic_set_free(context_i
);
1032 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1034 if (!upper
|| !context_i
)
1036 if (fn(NULL
, upper
, context_i
, user
) < 0)
1040 isl_basic_set_free(context
);
1042 if (i
< bset
->n_ineq
)
1043 return isl_stat_error
;
1047 isl_constraint_free(upper
);
1048 isl_basic_set_free(context_i
);
1049 isl_basic_set_free(context
);
1050 return isl_stat_error
;
1053 static isl_stat
foreach_lower_bound(__isl_keep isl_basic_set
*bset
,
1054 enum isl_dim_type type
, unsigned abs_pos
,
1055 __isl_take isl_basic_set
*context
, int n_lower
,
1056 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1057 __isl_take isl_constraint
*upper
,
1058 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1060 isl_basic_set
*context_i
;
1061 isl_constraint
*lower
= NULL
;
1064 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1065 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1068 context_i
= set_largest_lower_bound(context
, bset
,
1069 abs_pos
, n_lower
, i
);
1070 if (isl_basic_set_is_empty(context_i
)) {
1071 isl_basic_set_free(context_i
);
1074 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1076 if (!lower
|| !context_i
)
1078 if (fn(lower
, NULL
, context_i
, user
) < 0)
1082 isl_basic_set_free(context
);
1084 if (i
< bset
->n_ineq
)
1085 return isl_stat_error
;
1089 isl_constraint_free(lower
);
1090 isl_basic_set_free(context_i
);
1091 isl_basic_set_free(context
);
1092 return isl_stat_error
;
1095 static isl_stat
foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1096 enum isl_dim_type type
, unsigned abs_pos
,
1097 __isl_take isl_basic_set
*context
, int n_lower
, int n_upper
,
1098 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1099 __isl_take isl_constraint
*upper
,
1100 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1102 isl_basic_set
*context_i
, *context_j
;
1103 isl_constraint
*lower
= NULL
;
1104 isl_constraint
*upper
= NULL
;
1107 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1108 if (!isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1111 context_i
= set_largest_lower_bound(context
, bset
,
1112 abs_pos
, n_lower
, i
);
1113 if (isl_basic_set_is_empty(context_i
)) {
1114 isl_basic_set_free(context_i
);
1118 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
1119 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
1122 context_j
= set_smallest_upper_bound(context_i
, bset
,
1123 abs_pos
, n_upper
, j
);
1124 context_j
= isl_basic_set_extend_constraints(context_j
,
1126 context_j
= add_larger_bound_constraint(context_j
,
1127 bset
->ineq
[i
], bset
->ineq
[j
], abs_pos
, 0);
1128 context_j
= isl_basic_set_simplify(context_j
);
1129 context_j
= isl_basic_set_finalize(context_j
);
1130 if (isl_basic_set_is_empty(context_j
)) {
1131 isl_basic_set_free(context_j
);
1134 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1136 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1138 if (!lower
|| !upper
|| !context_j
)
1140 if (fn(lower
, upper
, context_j
, user
) < 0)
1144 isl_basic_set_free(context_i
);
1146 if (j
< bset
->n_ineq
)
1150 isl_basic_set_free(context
);
1152 if (i
< bset
->n_ineq
)
1153 return isl_stat_error
;
1157 isl_constraint_free(lower
);
1158 isl_constraint_free(upper
);
1159 isl_basic_set_free(context_i
);
1160 isl_basic_set_free(context_j
);
1161 isl_basic_set_free(context
);
1162 return isl_stat_error
;
1165 /* For each pair of lower and upper bounds on the variable "pos"
1166 * of type "type", call "fn" with these lower and upper bounds and the
1167 * set of constraints on the remaining variables where these bounds
1168 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1170 * If the designated variable is equal to an affine combination of the
1171 * other variables then fn is called with both lower and upper
1172 * set to the corresponding equality.
1174 * If there is no lower (or upper) bound, then NULL is passed
1175 * as the corresponding bound.
1177 * We first check if the variable is involved in any equality.
1178 * If not, we count the number of lower and upper bounds and
1181 isl_stat
isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1182 enum isl_dim_type type
, unsigned pos
,
1183 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1184 __isl_take isl_constraint
*upper
,
1185 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1188 isl_constraint
*lower
= NULL
;
1189 isl_constraint
*upper
= NULL
;
1190 isl_basic_set
*context
= NULL
;
1192 int n_lower
, n_upper
;
1195 return isl_stat_error
;
1196 isl_assert(bset
->ctx
, pos
< isl_basic_set_dim(bset
, type
),
1197 return isl_stat_error
);
1198 isl_assert(bset
->ctx
, type
== isl_dim_param
|| type
== isl_dim_set
,
1199 return isl_stat_error
);
1202 if (type
== isl_dim_set
)
1203 abs_pos
+= isl_basic_set_dim(bset
, isl_dim_param
);
1205 for (i
= 0; i
< bset
->n_eq
; ++i
) {
1206 if (isl_int_is_zero(bset
->eq
[i
][1 + abs_pos
]))
1209 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1211 upper
= isl_constraint_copy(lower
);
1212 context
= isl_basic_set_remove_dims(isl_basic_set_copy(bset
),
1214 if (!lower
|| !upper
|| !context
)
1216 return fn(lower
, upper
, context
, user
);
1221 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1222 if (isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1224 else if (isl_int_is_neg(bset
->ineq
[i
][1 + abs_pos
]))
1228 context
= isl_basic_set_copy(bset
);
1229 context
= isl_basic_set_cow(context
);
1232 for (i
= context
->n_ineq
- 1; i
>= 0; --i
)
1233 if (!isl_int_is_zero(context
->ineq
[i
][1 + abs_pos
]))
1234 isl_basic_set_drop_inequality(context
, i
);
1236 context
= isl_basic_set_drop(context
, type
, pos
, 1);
1237 if (!n_lower
&& !n_upper
)
1238 return fn(NULL
, NULL
, context
, user
);
1240 return foreach_upper_bound(bset
, type
, abs_pos
, context
, n_upper
,
1243 return foreach_lower_bound(bset
, type
, abs_pos
, context
, n_lower
,
1245 return foreach_bound_pair(bset
, type
, abs_pos
, context
, n_lower
, n_upper
,
1248 isl_constraint_free(lower
);
1249 isl_constraint_free(upper
);
1250 isl_basic_set_free(context
);
1254 __isl_give isl_aff
*isl_constraint_get_bound(
1255 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
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 if (isl_constraint_dim(constraint
, isl_dim_in
) != 0)
1267 isl_die(ctx
, isl_error_invalid
,
1268 "not a set constraint", 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",
1276 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
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);
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
]);
1290 /* For an inequality constraint
1294 * or an equality constraint
1298 * return the affine expression f.
1300 __isl_give isl_aff
*isl_constraint_get_aff(
1301 __isl_keep isl_constraint
*constraint
)
1308 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
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);
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
;
1331 ls
= isl_aff_get_domain_local_space(aff
);
1332 v
= isl_vec_drop_els(isl_vec_copy(aff
->v
), 0, 1);
1335 return isl_constraint_alloc_vec(eq
, ls
, v
);
1338 /* Construct an equality constraint equating the given affine expression
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
)
1374 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
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);
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
)
1409 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
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);
1416 return last1
- last2
;
1419 return isl_int_abs_cmp(c1
->v
->el
[1 + last1
], c2
->v
->el
[1 + last2
]);