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 /* Return the space of "constraint".
378 static __isl_keep isl_space
*isl_constraint_peek_space(
379 __isl_keep isl_constraint
*constraint
)
381 return constraint
? isl_local_space_peek_space(constraint
->ls
) : NULL
;
384 __isl_give isl_space
*isl_constraint_get_space(
385 __isl_keep isl_constraint
*constraint
)
387 return constraint
? isl_local_space_get_space(constraint
->ls
) : NULL
;
390 __isl_give isl_local_space
*isl_constraint_get_local_space(
391 __isl_keep isl_constraint
*constraint
)
393 return constraint
? isl_local_space_copy(constraint
->ls
) : NULL
;
396 int isl_constraint_dim(__isl_keep isl_constraint
*constraint
,
397 enum isl_dim_type type
)
401 return n(constraint
, type
);
404 isl_bool
isl_constraint_involves_dims(__isl_keep isl_constraint
*constraint
,
405 enum isl_dim_type type
, unsigned first
, unsigned n
)
410 isl_bool involves
= isl_bool_false
;
413 return isl_bool_error
;
415 return isl_bool_false
;
417 ctx
= isl_constraint_get_ctx(constraint
);
418 if (first
+ n
> isl_constraint_dim(constraint
, type
))
419 isl_die(ctx
, isl_error_invalid
,
420 "range out of bounds", return isl_bool_error
);
422 active
= isl_local_space_get_active(constraint
->ls
,
423 constraint
->v
->el
+ 1);
427 first
+= isl_local_space_offset(constraint
->ls
, type
) - 1;
428 for (i
= 0; i
< n
; ++i
)
429 if (active
[first
+ i
]) {
430 involves
= isl_bool_true
;
439 return isl_bool_error
;
442 /* Does the given constraint represent a lower bound on the given
445 isl_bool
isl_constraint_is_lower_bound(__isl_keep isl_constraint
*constraint
,
446 enum isl_dim_type type
, unsigned pos
)
449 return isl_bool_error
;
451 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
452 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
453 "position out of bounds", return isl_bool_error
);
455 pos
+= isl_local_space_offset(constraint
->ls
, type
);
456 return isl_int_is_pos(constraint
->v
->el
[pos
]);
459 /* Does the given constraint represent an upper bound on the given
462 isl_bool
isl_constraint_is_upper_bound(__isl_keep isl_constraint
*constraint
,
463 enum isl_dim_type type
, unsigned pos
)
466 return isl_bool_error
;
468 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
469 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
470 "position out of bounds", return isl_bool_error
);
472 pos
+= isl_local_space_offset(constraint
->ls
, type
);
473 return isl_int_is_neg(constraint
->v
->el
[pos
]);
476 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint
*constraint
,
477 enum isl_dim_type type
, unsigned pos
)
480 isl_local_space_get_dim_name(constraint
->ls
, type
, pos
) : NULL
;
483 void isl_constraint_get_constant(__isl_keep isl_constraint
*constraint
,
488 isl_int_set(*v
, constraint
->v
->el
[0]);
491 /* Return the constant term of "constraint".
493 __isl_give isl_val
*isl_constraint_get_constant_val(
494 __isl_keep isl_constraint
*constraint
)
501 ctx
= isl_constraint_get_ctx(constraint
);
502 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[0]);
505 void isl_constraint_get_coefficient(struct isl_constraint
*constraint
,
506 enum isl_dim_type type
, int pos
, isl_int
*v
)
511 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
512 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
513 "position out of bounds", return);
515 pos
+= isl_local_space_offset(constraint
->ls
, type
);
516 isl_int_set(*v
, constraint
->v
->el
[pos
]);
519 /* Return the coefficient of the variable of type "type" at position "pos"
522 __isl_give isl_val
*isl_constraint_get_coefficient_val(
523 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
530 ctx
= isl_constraint_get_ctx(constraint
);
531 if (pos
< 0 || pos
>= isl_local_space_dim(constraint
->ls
, type
))
532 isl_die(ctx
, isl_error_invalid
,
533 "position out of bounds", return NULL
);
535 pos
+= isl_local_space_offset(constraint
->ls
, type
);
536 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[pos
]);
539 __isl_give isl_aff
*isl_constraint_get_div(__isl_keep isl_constraint
*constraint
,
545 return isl_local_space_get_div(constraint
->ls
, pos
);
548 __isl_give isl_constraint
*isl_constraint_set_constant(
549 __isl_take isl_constraint
*constraint
, isl_int v
)
551 constraint
= isl_constraint_cow(constraint
);
555 constraint
->v
= isl_vec_cow(constraint
->v
);
557 return isl_constraint_free(constraint
);
559 isl_int_set(constraint
->v
->el
[0], v
);
563 /* Replace the constant term of "constraint" by "v".
565 __isl_give isl_constraint
*isl_constraint_set_constant_val(
566 __isl_take isl_constraint
*constraint
, __isl_take isl_val
*v
)
568 constraint
= isl_constraint_cow(constraint
);
569 if (!constraint
|| !v
)
571 if (!isl_val_is_int(v
))
572 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
573 "expecting integer value", goto error
);
574 constraint
->v
= isl_vec_set_element_val(constraint
->v
, 0, v
);
576 constraint
= isl_constraint_free(constraint
);
580 return isl_constraint_free(constraint
);
583 __isl_give isl_constraint
*isl_constraint_set_constant_si(
584 __isl_take isl_constraint
*constraint
, int v
)
586 constraint
= isl_constraint_cow(constraint
);
590 constraint
->v
= isl_vec_cow(constraint
->v
);
592 return isl_constraint_free(constraint
);
594 isl_int_set_si(constraint
->v
->el
[0], v
);
598 __isl_give isl_constraint
*isl_constraint_set_coefficient(
599 __isl_take isl_constraint
*constraint
,
600 enum isl_dim_type type
, int pos
, isl_int v
)
602 constraint
= isl_constraint_cow(constraint
);
606 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
607 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
608 "position out of bounds",
609 return isl_constraint_free(constraint
));
611 constraint
->v
= isl_vec_cow(constraint
->v
);
613 return isl_constraint_free(constraint
);
615 pos
+= isl_local_space_offset(constraint
->ls
, type
);
616 isl_int_set(constraint
->v
->el
[pos
], v
);
621 /* Replace the coefficient of the variable of type "type" at position "pos"
622 * of "constraint" by "v".
624 __isl_give isl_constraint
*isl_constraint_set_coefficient_val(
625 __isl_take isl_constraint
*constraint
,
626 enum isl_dim_type type
, int pos
, __isl_take isl_val
*v
)
628 constraint
= isl_constraint_cow(constraint
);
629 if (!constraint
|| !v
)
631 if (!isl_val_is_int(v
))
632 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
633 "expecting integer value", goto error
);
635 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
636 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
637 "position out of bounds", goto error
);
639 pos
+= isl_local_space_offset(constraint
->ls
, type
);
640 constraint
->v
= isl_vec_set_element_val(constraint
->v
, pos
, v
);
642 constraint
= isl_constraint_free(constraint
);
646 return isl_constraint_free(constraint
);
649 __isl_give isl_constraint
*isl_constraint_set_coefficient_si(
650 __isl_take isl_constraint
*constraint
,
651 enum isl_dim_type type
, int pos
, int v
)
653 constraint
= isl_constraint_cow(constraint
);
657 if (pos
>= isl_local_space_dim(constraint
->ls
, type
))
658 isl_die(constraint
->v
->ctx
, isl_error_invalid
,
659 "position out of bounds",
660 return isl_constraint_free(constraint
));
662 constraint
->v
= isl_vec_cow(constraint
->v
);
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
)
795 space
= isl_constraint_peek_space(constraint
);
796 if (isl_space_check_is_set(space
) < 0)
798 return bset_from_bmap(isl_basic_map_from_constraint(constraint
));
800 isl_constraint_free(constraint
);
804 /* Is the variable of "type" at position "pos" of "bmap" defined
805 * in terms of earlier dimensions through an equality?
807 * If so, and if c is not NULL, then return a copy of this equality in *c.
809 isl_bool
isl_basic_map_has_defining_equality(
810 __isl_keep isl_basic_map
*bmap
, enum isl_dim_type type
, int pos
,
811 __isl_give isl_constraint
**c
)
818 return isl_bool_error
;
819 offset
= basic_map_offset(bmap
, type
);
820 total
= isl_basic_map_total_dim(bmap
);
821 if (pos
>= isl_basic_map_dim(bmap
, type
))
822 isl_die(isl_basic_map_get_ctx(bmap
), isl_error_invalid
,
823 "invalid position", return isl_bool_error
);
824 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
825 if (isl_int_is_zero(bmap
->eq
[i
][offset
+ pos
]) ||
826 isl_seq_first_non_zero(bmap
->eq
[i
]+offset
+pos
+1,
827 1+total
-offset
-pos
-1) != -1)
830 *c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
832 return isl_bool_true
;
834 return isl_bool_false
;
837 /* Is the variable of "type" at position "pos" of "bset" defined
838 * in terms of earlier dimensions through an equality?
840 * If so, and if c is not NULL, then return a copy of this equality in *c.
842 isl_bool
isl_basic_set_has_defining_equality(
843 __isl_keep isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
844 __isl_give isl_constraint
**c
)
846 return isl_basic_map_has_defining_equality(bset_to_bmap(bset
),
850 isl_bool
isl_basic_set_has_defining_inequalities(
851 struct isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
852 struct isl_constraint
**lower
,
853 struct isl_constraint
**upper
)
859 isl_int
**lower_line
, **upper_line
;
862 return isl_bool_error
;
863 offset
= basic_set_offset(bset
, type
);
864 total
= isl_basic_set_total_dim(bset
);
865 if (pos
>= isl_basic_set_dim(bset
, type
))
866 isl_die(isl_basic_set_get_ctx(bset
), isl_error_invalid
,
867 "invalid position", return isl_bool_error
);
869 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
870 if (isl_int_is_zero(bset
->ineq
[i
][offset
+ pos
]))
872 if (isl_int_is_one(bset
->ineq
[i
][offset
+ pos
]))
874 if (isl_int_is_negone(bset
->ineq
[i
][offset
+ pos
]))
876 if (isl_seq_first_non_zero(bset
->ineq
[i
]+offset
+pos
+1,
877 1+total
-offset
-pos
-1) != -1)
879 for (j
= i
+ 1; j
< bset
->n_ineq
; ++j
) {
880 if (!isl_seq_is_neg(bset
->ineq
[i
]+1, bset
->ineq
[j
]+1,
883 isl_int_add(m
, bset
->ineq
[i
][0], bset
->ineq
[j
][0]);
884 if (isl_int_abs_ge(m
, bset
->ineq
[i
][offset
+pos
]))
887 if (isl_int_is_pos(bset
->ineq
[i
][offset
+pos
])) {
888 lower_line
= &bset
->ineq
[i
];
889 upper_line
= &bset
->ineq
[j
];
891 lower_line
= &bset
->ineq
[j
];
892 upper_line
= &bset
->ineq
[i
];
894 *lower
= isl_basic_set_constraint(
895 isl_basic_set_copy(bset
), lower_line
);
896 *upper
= isl_basic_set_constraint(
897 isl_basic_set_copy(bset
), upper_line
);
899 return isl_bool_true
;
905 return isl_bool_false
;
908 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
909 * (in "a" and "b"), add a constraint to "bset" that ensures that the
910 * bound implied by "a" is (strictly) larger than the bound implied by "b".
912 * If both constraints imply lower bounds, then this means that "a" is
913 * active in the result.
914 * If both constraints imply upper bounds, then this means that "b" is
915 * active in the result.
917 static __isl_give isl_basic_set
*add_larger_bound_constraint(
918 __isl_take isl_basic_set
*bset
, isl_int
*a
, isl_int
*b
,
919 unsigned abs_pos
, int strict
)
925 k
= isl_basic_set_alloc_inequality(bset
);
929 total
= isl_basic_set_dim(bset
, isl_dim_all
);
932 isl_int_neg(t
, b
[1 + abs_pos
]);
934 isl_seq_combine(bset
->ineq
[k
], t
, a
, a
[1 + abs_pos
], b
, 1 + abs_pos
);
935 isl_seq_combine(bset
->ineq
[k
] + 1 + abs_pos
,
936 t
, a
+ 1 + abs_pos
+ 1, a
[1 + abs_pos
], b
+ 1 + abs_pos
+ 1,
940 isl_int_sub_ui(bset
->ineq
[k
][0], bset
->ineq
[k
][0], 1);
946 isl_basic_set_free(bset
);
950 /* Add constraints to "context" that ensure that "u" is the smallest
951 * (and therefore active) upper bound on "abs_pos" in "bset" and return
952 * the resulting basic set.
954 static __isl_give isl_basic_set
*set_smallest_upper_bound(
955 __isl_keep isl_basic_set
*context
,
956 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_upper
, int u
)
960 context
= isl_basic_set_copy(context
);
961 context
= isl_basic_set_cow(context
);
963 context
= isl_basic_set_extend_constraints(context
, 0, n_upper
- 1);
965 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
968 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
970 context
= add_larger_bound_constraint(context
,
971 bset
->ineq
[j
], bset
->ineq
[u
], abs_pos
, j
> u
);
974 context
= isl_basic_set_simplify(context
);
975 context
= isl_basic_set_finalize(context
);
980 /* Add constraints to "context" that ensure that "u" is the largest
981 * (and therefore active) upper bound on "abs_pos" in "bset" and return
982 * the resulting basic set.
984 static __isl_give isl_basic_set
*set_largest_lower_bound(
985 __isl_keep isl_basic_set
*context
,
986 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_lower
, int l
)
990 context
= isl_basic_set_copy(context
);
991 context
= isl_basic_set_cow(context
);
993 context
= isl_basic_set_extend_constraints(context
, 0, n_lower
- 1);
995 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
998 if (!isl_int_is_pos(bset
->ineq
[j
][1 + abs_pos
]))
1000 context
= add_larger_bound_constraint(context
,
1001 bset
->ineq
[l
], bset
->ineq
[j
], abs_pos
, j
> l
);
1004 context
= isl_basic_set_simplify(context
);
1005 context
= isl_basic_set_finalize(context
);
1010 static isl_stat
foreach_upper_bound(__isl_keep isl_basic_set
*bset
,
1011 enum isl_dim_type type
, unsigned abs_pos
,
1012 __isl_take isl_basic_set
*context
, int n_upper
,
1013 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1014 __isl_take isl_constraint
*upper
,
1015 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1017 isl_basic_set
*context_i
;
1018 isl_constraint
*upper
= NULL
;
1021 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1022 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1025 context_i
= set_smallest_upper_bound(context
, bset
,
1026 abs_pos
, n_upper
, i
);
1027 if (isl_basic_set_is_empty(context_i
)) {
1028 isl_basic_set_free(context_i
);
1031 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1033 if (!upper
|| !context_i
)
1035 if (fn(NULL
, upper
, context_i
, user
) < 0)
1039 isl_basic_set_free(context
);
1041 if (i
< bset
->n_ineq
)
1042 return isl_stat_error
;
1046 isl_constraint_free(upper
);
1047 isl_basic_set_free(context_i
);
1048 isl_basic_set_free(context
);
1049 return isl_stat_error
;
1052 static isl_stat
foreach_lower_bound(__isl_keep isl_basic_set
*bset
,
1053 enum isl_dim_type type
, unsigned abs_pos
,
1054 __isl_take isl_basic_set
*context
, int n_lower
,
1055 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1056 __isl_take isl_constraint
*upper
,
1057 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1059 isl_basic_set
*context_i
;
1060 isl_constraint
*lower
= NULL
;
1063 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1064 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1067 context_i
= set_largest_lower_bound(context
, bset
,
1068 abs_pos
, n_lower
, i
);
1069 if (isl_basic_set_is_empty(context_i
)) {
1070 isl_basic_set_free(context_i
);
1073 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1075 if (!lower
|| !context_i
)
1077 if (fn(lower
, NULL
, context_i
, user
) < 0)
1081 isl_basic_set_free(context
);
1083 if (i
< bset
->n_ineq
)
1084 return isl_stat_error
;
1088 isl_constraint_free(lower
);
1089 isl_basic_set_free(context_i
);
1090 isl_basic_set_free(context
);
1091 return isl_stat_error
;
1094 static isl_stat
foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1095 enum isl_dim_type type
, unsigned abs_pos
,
1096 __isl_take isl_basic_set
*context
, int n_lower
, int n_upper
,
1097 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1098 __isl_take isl_constraint
*upper
,
1099 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1101 isl_basic_set
*context_i
, *context_j
;
1102 isl_constraint
*lower
= NULL
;
1103 isl_constraint
*upper
= NULL
;
1106 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1107 if (!isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1110 context_i
= set_largest_lower_bound(context
, bset
,
1111 abs_pos
, n_lower
, i
);
1112 if (isl_basic_set_is_empty(context_i
)) {
1113 isl_basic_set_free(context_i
);
1117 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
1118 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
1121 context_j
= set_smallest_upper_bound(context_i
, bset
,
1122 abs_pos
, n_upper
, j
);
1123 context_j
= isl_basic_set_extend_constraints(context_j
,
1125 context_j
= add_larger_bound_constraint(context_j
,
1126 bset
->ineq
[i
], bset
->ineq
[j
], abs_pos
, 0);
1127 context_j
= isl_basic_set_simplify(context_j
);
1128 context_j
= isl_basic_set_finalize(context_j
);
1129 if (isl_basic_set_is_empty(context_j
)) {
1130 isl_basic_set_free(context_j
);
1133 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1135 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1137 if (!lower
|| !upper
|| !context_j
)
1139 if (fn(lower
, upper
, context_j
, user
) < 0)
1143 isl_basic_set_free(context_i
);
1145 if (j
< bset
->n_ineq
)
1149 isl_basic_set_free(context
);
1151 if (i
< bset
->n_ineq
)
1152 return isl_stat_error
;
1156 isl_constraint_free(lower
);
1157 isl_constraint_free(upper
);
1158 isl_basic_set_free(context_i
);
1159 isl_basic_set_free(context_j
);
1160 isl_basic_set_free(context
);
1161 return isl_stat_error
;
1164 /* For each pair of lower and upper bounds on the variable "pos"
1165 * of type "type", call "fn" with these lower and upper bounds and the
1166 * set of constraints on the remaining variables where these bounds
1167 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1169 * If the designated variable is equal to an affine combination of the
1170 * other variables then fn is called with both lower and upper
1171 * set to the corresponding equality.
1173 * If there is no lower (or upper) bound, then NULL is passed
1174 * as the corresponding bound.
1176 * We first check if the variable is involved in any equality.
1177 * If not, we count the number of lower and upper bounds and
1180 isl_stat
isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1181 enum isl_dim_type type
, unsigned pos
,
1182 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1183 __isl_take isl_constraint
*upper
,
1184 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1187 isl_constraint
*lower
= NULL
;
1188 isl_constraint
*upper
= NULL
;
1189 isl_basic_set
*context
= NULL
;
1191 int n_lower
, n_upper
;
1194 return isl_stat_error
;
1195 isl_assert(bset
->ctx
, pos
< isl_basic_set_dim(bset
, type
),
1196 return isl_stat_error
);
1197 isl_assert(bset
->ctx
, type
== isl_dim_param
|| type
== isl_dim_set
,
1198 return isl_stat_error
);
1201 if (type
== isl_dim_set
)
1202 abs_pos
+= isl_basic_set_dim(bset
, isl_dim_param
);
1204 for (i
= 0; i
< bset
->n_eq
; ++i
) {
1205 if (isl_int_is_zero(bset
->eq
[i
][1 + abs_pos
]))
1208 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1210 upper
= isl_constraint_copy(lower
);
1211 context
= isl_basic_set_remove_dims(isl_basic_set_copy(bset
),
1213 if (!lower
|| !upper
|| !context
)
1215 return fn(lower
, upper
, context
, user
);
1220 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1221 if (isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1223 else if (isl_int_is_neg(bset
->ineq
[i
][1 + abs_pos
]))
1227 context
= isl_basic_set_copy(bset
);
1228 context
= isl_basic_set_cow(context
);
1231 for (i
= context
->n_ineq
- 1; i
>= 0; --i
)
1232 if (!isl_int_is_zero(context
->ineq
[i
][1 + abs_pos
]))
1233 isl_basic_set_drop_inequality(context
, i
);
1235 context
= isl_basic_set_drop(context
, type
, pos
, 1);
1236 if (!n_lower
&& !n_upper
)
1237 return fn(NULL
, NULL
, context
, user
);
1239 return foreach_upper_bound(bset
, type
, abs_pos
, context
, n_upper
,
1242 return foreach_lower_bound(bset
, type
, abs_pos
, context
, n_lower
,
1244 return foreach_bound_pair(bset
, type
, abs_pos
, context
, n_lower
, n_upper
,
1247 isl_constraint_free(lower
);
1248 isl_constraint_free(upper
);
1249 isl_basic_set_free(context
);
1250 return isl_stat_error
;
1253 __isl_give isl_aff
*isl_constraint_get_bound(
1254 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
1262 ctx
= isl_constraint_get_ctx(constraint
);
1263 if (pos
>= isl_constraint_dim(constraint
, type
))
1264 isl_die(ctx
, isl_error_invalid
,
1265 "index out of bounds", return NULL
);
1266 space
= isl_constraint_peek_space(constraint
);
1267 if (isl_space_check_is_set(space
) < 0)
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
]);