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 isl_size
n(struct isl_constraint
*c
, enum isl_dim_type type
)
37 return isl_local_space_dim(c
->ls
, type
);
40 static unsigned offset(struct isl_constraint
*c
, enum isl_dim_type type
)
42 return isl_local_space_offset(c
->ls
, type
);
45 __isl_give isl_constraint
*isl_constraint_alloc_vec(int eq
,
46 __isl_take isl_local_space
*ls
, __isl_take isl_vec
*v
)
48 isl_constraint
*constraint
;
53 constraint
= isl_alloc_type(isl_vec_get_ctx(v
), isl_constraint
);
64 isl_local_space_free(ls
);
69 __isl_give isl_constraint
*isl_constraint_alloc(int eq
,
70 __isl_take isl_local_space
*ls
)
76 dim
= isl_local_space_dim(ls
, isl_dim_all
);
78 ls
= isl_local_space_free(ls
);
82 ctx
= isl_local_space_get_ctx(ls
);
83 v
= isl_vec_alloc(ctx
, 1 + dim
);
85 return isl_constraint_alloc_vec(eq
, ls
, v
);
88 struct isl_constraint
*isl_basic_map_constraint(struct isl_basic_map
*bmap
,
95 isl_local_space
*ls
= NULL
;
96 isl_constraint
*constraint
;
101 eq
= line
>= bmap
->eq
;
103 ctx
= isl_basic_map_get_ctx(bmap
);
104 ls
= isl_basic_map_get_local_space(bmap
);
105 dim
= isl_local_space_dim(ls
, isl_dim_all
);
108 v
= isl_vec_alloc(ctx
, 1 + dim
);
111 isl_seq_cpy(v
->el
, line
[0], v
->size
);
112 constraint
= isl_constraint_alloc_vec(eq
, ls
, v
);
114 isl_basic_map_free(bmap
);
117 isl_local_space_free(ls
);
118 isl_basic_map_free(bmap
);
122 struct isl_constraint
*isl_basic_set_constraint(struct isl_basic_set
*bset
,
125 return isl_basic_map_constraint(bset_to_bmap(bset
), line
);
128 __isl_give isl_constraint
*isl_constraint_alloc_equality(
129 __isl_take isl_local_space
*ls
)
131 return isl_constraint_alloc(1, ls
);
134 __isl_give isl_constraint
*isl_constraint_alloc_inequality(
135 __isl_take isl_local_space
*ls
)
137 return isl_constraint_alloc(0, ls
);
140 struct isl_constraint
*isl_constraint_dup(struct isl_constraint
*c
)
145 return isl_constraint_alloc_vec(c
->eq
, isl_local_space_copy(c
->ls
),
149 struct isl_constraint
*isl_constraint_cow(struct isl_constraint
*c
)
157 return isl_constraint_dup(c
);
160 struct isl_constraint
*isl_constraint_copy(struct isl_constraint
*constraint
)
169 __isl_null isl_constraint
*isl_constraint_free(__isl_take isl_constraint
*c
)
177 isl_local_space_free(c
->ls
);
184 /* Return the number of constraints in "bmap", i.e., the
185 * number of times isl_basic_map_foreach_constraint will
188 int isl_basic_map_n_constraint(__isl_keep isl_basic_map
*bmap
)
193 return bmap
->n_eq
+ bmap
->n_ineq
;
196 /* Return the number of constraints in "bset", i.e., the
197 * number of times isl_basic_set_foreach_constraint will
200 int isl_basic_set_n_constraint(__isl_keep isl_basic_set
*bset
)
202 return isl_basic_map_n_constraint(bset
);
205 isl_stat
isl_basic_map_foreach_constraint(__isl_keep isl_basic_map
*bmap
,
206 isl_stat (*fn
)(__isl_take isl_constraint
*c
, void *user
), void *user
)
209 struct isl_constraint
*c
;
212 return isl_stat_error
;
214 isl_assert(bmap
->ctx
, ISL_F_ISSET(bmap
, ISL_BASIC_MAP_FINAL
),
215 return isl_stat_error
);
217 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
218 c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
221 return isl_stat_error
;
223 return isl_stat_error
;
226 for (i
= 0; i
< bmap
->n_ineq
; ++i
) {
227 c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
230 return isl_stat_error
;
232 return isl_stat_error
;
238 isl_stat
isl_basic_set_foreach_constraint(__isl_keep isl_basic_set
*bset
,
239 isl_stat (*fn
)(__isl_take isl_constraint
*c
, void *user
), void *user
)
241 return isl_basic_map_foreach_constraint(bset_to_bmap(bset
), fn
, user
);
244 /* Add the constraint to the list that "user" points to, if it is not
247 static isl_stat
collect_constraint(__isl_take isl_constraint
*constraint
,
250 isl_constraint_list
**list
= user
;
253 is_div
= isl_constraint_is_div_constraint(constraint
);
254 if (is_div
< 0 || is_div
)
255 isl_constraint_free(constraint
);
257 *list
= isl_constraint_list_add(*list
, constraint
);
259 return is_div
< 0 ? isl_stat_error
: isl_stat_ok
;
262 /* Return a list of constraints that, when combined, are equivalent
263 * to "bmap". The input is required to have only known divs.
265 * There is no need to include the div constraints as they are
266 * implied by the div expressions.
268 __isl_give isl_constraint_list
*isl_basic_map_get_constraint_list(
269 __isl_keep isl_basic_map
*bmap
)
274 isl_constraint_list
*list
;
276 known
= isl_basic_map_divs_known(bmap
);
279 ctx
= isl_basic_map_get_ctx(bmap
);
281 isl_die(ctx
, isl_error_invalid
,
282 "input involves unknown divs", return NULL
);
284 n
= isl_basic_map_n_constraint(bmap
);
285 list
= isl_constraint_list_alloc(ctx
, n
);
286 if (isl_basic_map_foreach_constraint(bmap
,
287 &collect_constraint
, &list
) < 0)
288 list
= isl_constraint_list_free(list
);
293 /* Return a list of constraints that, when combined, are equivalent
294 * to "bset". The input is required to have only known divs.
296 __isl_give isl_constraint_list
*isl_basic_set_get_constraint_list(
297 __isl_keep isl_basic_set
*bset
)
299 return isl_basic_map_get_constraint_list(bset
);
302 int isl_constraint_is_equal(struct isl_constraint
*constraint1
,
303 struct isl_constraint
*constraint2
)
307 if (!constraint1
|| !constraint2
)
309 if (constraint1
->eq
!= constraint2
->eq
)
311 equal
= isl_local_space_is_equal(constraint1
->ls
, constraint2
->ls
);
312 if (equal
< 0 || !equal
)
314 return isl_vec_is_equal(constraint1
->v
, constraint2
->v
);
317 struct isl_basic_map
*isl_basic_map_add_constraint(
318 struct isl_basic_map
*bmap
, struct isl_constraint
*constraint
)
324 if (!bmap
|| !constraint
)
327 ctx
= isl_constraint_get_ctx(constraint
);
328 space
= isl_constraint_get_space(constraint
);
329 equal_space
= isl_space_is_equal(bmap
->dim
, space
);
330 isl_space_free(space
);
331 isl_assert(ctx
, equal_space
, goto error
);
333 bmap
= isl_basic_map_intersect(bmap
,
334 isl_basic_map_from_constraint(constraint
));
337 isl_basic_map_free(bmap
);
338 isl_constraint_free(constraint
);
342 struct isl_basic_set
*isl_basic_set_add_constraint(
343 struct isl_basic_set
*bset
, struct isl_constraint
*constraint
)
345 return bset_from_bmap(isl_basic_map_add_constraint(bset_to_bmap(bset
),
349 __isl_give isl_map
*isl_map_add_constraint(__isl_take isl_map
*map
,
350 __isl_take isl_constraint
*constraint
)
354 bmap
= isl_basic_map_from_constraint(constraint
);
355 map
= isl_map_intersect(map
, isl_map_from_basic_map(bmap
));
360 __isl_give isl_set
*isl_set_add_constraint(__isl_take isl_set
*set
,
361 __isl_take isl_constraint
*constraint
)
363 return isl_map_add_constraint(set
, constraint
);
366 /* Return the space of "constraint".
368 static __isl_keep isl_space
*isl_constraint_peek_space(
369 __isl_keep isl_constraint
*constraint
)
371 return constraint
? isl_local_space_peek_space(constraint
->ls
) : NULL
;
374 __isl_give isl_space
*isl_constraint_get_space(
375 __isl_keep isl_constraint
*constraint
)
377 return constraint
? isl_local_space_get_space(constraint
->ls
) : NULL
;
380 __isl_give isl_local_space
*isl_constraint_get_local_space(
381 __isl_keep isl_constraint
*constraint
)
383 return constraint
? isl_local_space_copy(constraint
->ls
) : NULL
;
386 isl_size
isl_constraint_dim(__isl_keep isl_constraint
*constraint
,
387 enum isl_dim_type type
)
390 return isl_size_error
;
391 return n(constraint
, type
);
395 #define TYPE isl_constraint
397 #include "check_type_range_templ.c"
399 isl_bool
isl_constraint_involves_dims(__isl_keep isl_constraint
*constraint
,
400 enum isl_dim_type type
, unsigned first
, unsigned n
)
404 isl_bool involves
= isl_bool_false
;
407 return isl_bool_error
;
409 return isl_bool_false
;
411 if (isl_constraint_check_range(constraint
, type
, first
, n
) < 0)
412 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
)
440 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
441 return isl_bool_error
;
443 pos
+= isl_local_space_offset(constraint
->ls
, type
);
444 return isl_int_is_pos(constraint
->v
->el
[pos
]);
447 /* Does the given constraint represent an upper bound on the given
450 isl_bool
isl_constraint_is_upper_bound(__isl_keep isl_constraint
*constraint
,
451 enum isl_dim_type type
, unsigned pos
)
453 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
454 return isl_bool_error
;
456 pos
+= isl_local_space_offset(constraint
->ls
, type
);
457 return isl_int_is_neg(constraint
->v
->el
[pos
]);
460 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint
*constraint
,
461 enum isl_dim_type type
, unsigned pos
)
464 isl_local_space_get_dim_name(constraint
->ls
, type
, pos
) : NULL
;
467 void isl_constraint_get_constant(__isl_keep isl_constraint
*constraint
,
472 isl_int_set(*v
, constraint
->v
->el
[0]);
475 /* Return the constant term of "constraint".
477 __isl_give isl_val
*isl_constraint_get_constant_val(
478 __isl_keep isl_constraint
*constraint
)
485 ctx
= isl_constraint_get_ctx(constraint
);
486 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[0]);
489 void isl_constraint_get_coefficient(struct isl_constraint
*constraint
,
490 enum isl_dim_type type
, int pos
, isl_int
*v
)
492 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
495 pos
+= isl_local_space_offset(constraint
->ls
, type
);
496 isl_int_set(*v
, constraint
->v
->el
[pos
]);
499 /* Return the coefficient of the variable of type "type" at position "pos"
502 __isl_give isl_val
*isl_constraint_get_coefficient_val(
503 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
507 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
510 ctx
= isl_constraint_get_ctx(constraint
);
511 pos
+= isl_local_space_offset(constraint
->ls
, type
);
512 return isl_val_int_from_isl_int(ctx
, constraint
->v
->el
[pos
]);
515 __isl_give isl_aff
*isl_constraint_get_div(__isl_keep isl_constraint
*constraint
,
521 return isl_local_space_get_div(constraint
->ls
, pos
);
524 __isl_give isl_constraint
*isl_constraint_set_constant(
525 __isl_take isl_constraint
*constraint
, isl_int v
)
527 constraint
= isl_constraint_cow(constraint
);
531 constraint
->v
= isl_vec_cow(constraint
->v
);
533 return isl_constraint_free(constraint
);
535 isl_int_set(constraint
->v
->el
[0], v
);
539 /* Replace the constant term of "constraint" by "v".
541 __isl_give isl_constraint
*isl_constraint_set_constant_val(
542 __isl_take isl_constraint
*constraint
, __isl_take isl_val
*v
)
544 constraint
= isl_constraint_cow(constraint
);
545 if (!constraint
|| !v
)
547 if (!isl_val_is_int(v
))
548 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
549 "expecting integer value", goto error
);
550 constraint
->v
= isl_vec_set_element_val(constraint
->v
, 0, v
);
552 constraint
= isl_constraint_free(constraint
);
556 return isl_constraint_free(constraint
);
559 __isl_give isl_constraint
*isl_constraint_set_constant_si(
560 __isl_take isl_constraint
*constraint
, int v
)
562 constraint
= isl_constraint_cow(constraint
);
566 constraint
->v
= isl_vec_cow(constraint
->v
);
568 return isl_constraint_free(constraint
);
570 isl_int_set_si(constraint
->v
->el
[0], v
);
574 __isl_give isl_constraint
*isl_constraint_set_coefficient(
575 __isl_take isl_constraint
*constraint
,
576 enum isl_dim_type type
, int pos
, isl_int v
)
578 constraint
= isl_constraint_cow(constraint
);
579 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
580 return isl_constraint_free(constraint
);
582 constraint
->v
= isl_vec_cow(constraint
->v
);
584 return isl_constraint_free(constraint
);
586 pos
+= isl_local_space_offset(constraint
->ls
, type
);
587 isl_int_set(constraint
->v
->el
[pos
], v
);
592 /* Replace the coefficient of the variable of type "type" at position "pos"
593 * of "constraint" by "v".
595 __isl_give isl_constraint
*isl_constraint_set_coefficient_val(
596 __isl_take isl_constraint
*constraint
,
597 enum isl_dim_type type
, int pos
, __isl_take isl_val
*v
)
599 constraint
= isl_constraint_cow(constraint
);
600 if (!constraint
|| !v
)
602 if (!isl_val_is_int(v
))
603 isl_die(isl_constraint_get_ctx(constraint
), isl_error_invalid
,
604 "expecting integer value", goto error
);
605 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
608 pos
+= isl_local_space_offset(constraint
->ls
, type
);
609 constraint
->v
= isl_vec_set_element_val(constraint
->v
, pos
, v
);
611 constraint
= isl_constraint_free(constraint
);
615 return isl_constraint_free(constraint
);
618 __isl_give isl_constraint
*isl_constraint_set_coefficient_si(
619 __isl_take isl_constraint
*constraint
,
620 enum isl_dim_type type
, int pos
, int v
)
622 constraint
= isl_constraint_cow(constraint
);
623 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
624 return isl_constraint_free(constraint
);
626 constraint
->v
= isl_vec_cow(constraint
->v
);
628 return isl_constraint_free(constraint
);
630 pos
+= isl_local_space_offset(constraint
->ls
, type
);
631 isl_int_set_si(constraint
->v
->el
[pos
], v
);
636 struct isl_constraint
*isl_constraint_negate(struct isl_constraint
*constraint
)
640 constraint
= isl_constraint_cow(constraint
);
644 ctx
= isl_constraint_get_ctx(constraint
);
645 if (isl_constraint_is_equality(constraint
))
646 isl_die(ctx
, isl_error_invalid
, "cannot negate equality",
647 return isl_constraint_free(constraint
));
648 constraint
->v
= isl_vec_neg(constraint
->v
);
649 constraint
->v
= isl_vec_cow(constraint
->v
);
651 return isl_constraint_free(constraint
);
652 isl_int_sub_ui(constraint
->v
->el
[0], constraint
->v
->el
[0], 1);
656 isl_bool
isl_constraint_is_equality(struct isl_constraint
*constraint
)
659 return isl_bool_error
;
660 return constraint
->eq
;
663 isl_bool
isl_constraint_is_div_constraint(__isl_keep isl_constraint
*constraint
)
669 return isl_bool_error
;
670 if (isl_constraint_is_equality(constraint
))
671 return isl_bool_false
;
672 n_div
= isl_constraint_dim(constraint
, isl_dim_div
);
674 return isl_bool_error
;
675 for (i
= 0; i
< n_div
; ++i
) {
677 is_div
= isl_local_space_is_div_constraint(constraint
->ls
,
678 constraint
->v
->el
, i
);
679 if (is_div
< 0 || is_div
)
683 return isl_bool_false
;
686 /* Is "constraint" an equality that corresponds to integer division "div"?
688 * That is, given an integer division of the form
690 * a = floor((f + c)/m)
692 * is the equality of the form
696 * Note that the constant term is not checked explicitly, but given
697 * that this is a valid equality constraint, the constant c' necessarily
698 * has a value close to -c.
700 isl_bool
isl_constraint_is_div_equality(__isl_keep isl_constraint
*constraint
,
705 equality
= isl_constraint_is_equality(constraint
);
706 if (equality
< 0 || !equality
)
708 return isl_local_space_is_div_equality(constraint
->ls
,
709 constraint
->v
->el
, div
);
712 /* We manually set ISL_BASIC_SET_FINAL instead of calling
713 * isl_basic_map_finalize because we want to keep the position
714 * of the divs and we therefore do not want to throw away redundant divs.
715 * This is arguably a bit fragile.
717 __isl_give isl_basic_map
*isl_basic_map_from_constraint(
718 __isl_take isl_constraint
*constraint
)
722 struct isl_basic_map
*bmap
;
729 ls
= isl_local_space_copy(constraint
->ls
);
730 bmap
= isl_basic_map_from_local_space(ls
);
731 bmap
= isl_basic_map_extend_constraints(bmap
, 1, 1);
732 if (isl_constraint_is_equality(constraint
)) {
733 k
= isl_basic_map_alloc_equality(bmap
);
739 k
= isl_basic_map_alloc_inequality(bmap
);
744 total
= isl_basic_map_dim(bmap
, isl_dim_all
);
747 isl_seq_cpy(c
, constraint
->v
->el
, 1 + total
);
748 isl_constraint_free(constraint
);
750 ISL_F_SET(bmap
, ISL_BASIC_SET_FINAL
);
753 isl_constraint_free(constraint
);
754 isl_basic_map_free(bmap
);
758 __isl_give isl_basic_set
*isl_basic_set_from_constraint(
759 __isl_take isl_constraint
*constraint
)
763 space
= isl_constraint_peek_space(constraint
);
764 if (isl_space_check_is_set(space
) < 0)
766 return bset_from_bmap(isl_basic_map_from_constraint(constraint
));
768 isl_constraint_free(constraint
);
772 /* Is the variable of "type" at position "pos" of "bmap" defined
773 * in terms of earlier dimensions through an equality?
775 * If so, and if c is not NULL, then return a copy of this equality in *c.
777 isl_bool
isl_basic_map_has_defining_equality(
778 __isl_keep isl_basic_map
*bmap
, enum isl_dim_type type
, int pos
,
779 __isl_give isl_constraint
**c
)
785 if (isl_basic_map_check_range(bmap
, type
, pos
, 1) < 0)
786 return isl_bool_error
;
787 offset
= isl_basic_map_offset(bmap
, type
);
788 total
= isl_basic_map_dim(bmap
, isl_dim_all
);
790 return isl_bool_error
;
791 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
792 if (isl_int_is_zero(bmap
->eq
[i
][offset
+ pos
]) ||
793 isl_seq_first_non_zero(bmap
->eq
[i
]+offset
+pos
+1,
794 1+total
-offset
-pos
-1) != -1)
797 *c
= isl_basic_map_constraint(isl_basic_map_copy(bmap
),
799 return isl_bool_true
;
801 return isl_bool_false
;
804 /* Is the variable of "type" at position "pos" of "bset" 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_set_has_defining_equality(
810 __isl_keep isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
811 __isl_give isl_constraint
**c
)
813 return isl_basic_map_has_defining_equality(bset_to_bmap(bset
),
817 isl_bool
isl_basic_set_has_defining_inequalities(
818 struct isl_basic_set
*bset
, enum isl_dim_type type
, int pos
,
819 struct isl_constraint
**lower
,
820 struct isl_constraint
**upper
)
826 isl_int
**lower_line
, **upper_line
;
828 if (isl_basic_set_check_range(bset
, type
, pos
, 1) < 0)
829 return isl_bool_error
;
830 offset
= isl_basic_set_offset(bset
, type
);
831 total
= isl_basic_set_dim(bset
, isl_dim_all
);
833 return isl_bool_error
;
835 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
836 if (isl_int_is_zero(bset
->ineq
[i
][offset
+ pos
]))
838 if (isl_int_is_one(bset
->ineq
[i
][offset
+ pos
]))
840 if (isl_int_is_negone(bset
->ineq
[i
][offset
+ pos
]))
842 if (isl_seq_first_non_zero(bset
->ineq
[i
]+offset
+pos
+1,
843 1+total
-offset
-pos
-1) != -1)
845 for (j
= i
+ 1; j
< bset
->n_ineq
; ++j
) {
846 if (!isl_seq_is_neg(bset
->ineq
[i
]+1, bset
->ineq
[j
]+1,
849 isl_int_add(m
, bset
->ineq
[i
][0], bset
->ineq
[j
][0]);
850 if (isl_int_abs_ge(m
, bset
->ineq
[i
][offset
+pos
]))
853 if (isl_int_is_pos(bset
->ineq
[i
][offset
+pos
])) {
854 lower_line
= &bset
->ineq
[i
];
855 upper_line
= &bset
->ineq
[j
];
857 lower_line
= &bset
->ineq
[j
];
858 upper_line
= &bset
->ineq
[i
];
860 *lower
= isl_basic_set_constraint(
861 isl_basic_set_copy(bset
), lower_line
);
862 *upper
= isl_basic_set_constraint(
863 isl_basic_set_copy(bset
), upper_line
);
865 return isl_bool_true
;
871 return isl_bool_false
;
874 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
875 * (in "a" and "b"), add a constraint to "bset" that ensures that the
876 * bound implied by "a" is (strictly) larger than the bound implied by "b".
878 * If both constraints imply lower bounds, then this means that "a" is
879 * active in the result.
880 * If both constraints imply upper bounds, then this means that "b" is
881 * active in the result.
883 static __isl_give isl_basic_set
*add_larger_bound_constraint(
884 __isl_take isl_basic_set
*bset
, isl_int
*a
, isl_int
*b
,
885 unsigned abs_pos
, int strict
)
891 total
= isl_basic_set_dim(bset
, isl_dim_all
);
893 return isl_basic_set_free(bset
);
894 k
= isl_basic_set_alloc_inequality(bset
);
899 isl_int_neg(t
, b
[1 + abs_pos
]);
901 isl_seq_combine(bset
->ineq
[k
], t
, a
, a
[1 + abs_pos
], b
, 1 + abs_pos
);
902 isl_seq_combine(bset
->ineq
[k
] + 1 + abs_pos
,
903 t
, a
+ 1 + abs_pos
+ 1, a
[1 + abs_pos
], b
+ 1 + abs_pos
+ 1,
907 isl_int_sub_ui(bset
->ineq
[k
][0], bset
->ineq
[k
][0], 1);
913 isl_basic_set_free(bset
);
917 /* Add constraints to "context" that ensure that "u" is the smallest
918 * (and therefore active) upper bound on "abs_pos" in "bset" and return
919 * the resulting basic set.
921 static __isl_give isl_basic_set
*set_smallest_upper_bound(
922 __isl_keep isl_basic_set
*context
,
923 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_upper
, int u
)
927 context
= isl_basic_set_copy(context
);
928 context
= isl_basic_set_cow(context
);
930 context
= isl_basic_set_extend_constraints(context
, 0, n_upper
- 1);
932 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
935 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
937 context
= add_larger_bound_constraint(context
,
938 bset
->ineq
[j
], bset
->ineq
[u
], abs_pos
, j
> u
);
941 context
= isl_basic_set_simplify(context
);
942 context
= isl_basic_set_finalize(context
);
947 /* Add constraints to "context" that ensure that "u" is the largest
948 * (and therefore active) upper bound on "abs_pos" in "bset" and return
949 * the resulting basic set.
951 static __isl_give isl_basic_set
*set_largest_lower_bound(
952 __isl_keep isl_basic_set
*context
,
953 __isl_keep isl_basic_set
*bset
, unsigned abs_pos
, int n_lower
, int l
)
957 context
= isl_basic_set_copy(context
);
958 context
= isl_basic_set_cow(context
);
960 context
= isl_basic_set_extend_constraints(context
, 0, n_lower
- 1);
962 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
965 if (!isl_int_is_pos(bset
->ineq
[j
][1 + abs_pos
]))
967 context
= add_larger_bound_constraint(context
,
968 bset
->ineq
[l
], bset
->ineq
[j
], abs_pos
, j
> l
);
971 context
= isl_basic_set_simplify(context
);
972 context
= isl_basic_set_finalize(context
);
977 static isl_stat
foreach_upper_bound(__isl_keep isl_basic_set
*bset
,
978 enum isl_dim_type type
, unsigned abs_pos
,
979 __isl_take isl_basic_set
*context
, int n_upper
,
980 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
981 __isl_take isl_constraint
*upper
,
982 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
984 isl_basic_set
*context_i
;
985 isl_constraint
*upper
= NULL
;
988 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
989 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
992 context_i
= set_smallest_upper_bound(context
, bset
,
993 abs_pos
, n_upper
, i
);
994 if (isl_basic_set_is_empty(context_i
)) {
995 isl_basic_set_free(context_i
);
998 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1000 if (!upper
|| !context_i
)
1002 if (fn(NULL
, upper
, context_i
, user
) < 0)
1006 isl_basic_set_free(context
);
1008 if (i
< bset
->n_ineq
)
1009 return isl_stat_error
;
1013 isl_constraint_free(upper
);
1014 isl_basic_set_free(context_i
);
1015 isl_basic_set_free(context
);
1016 return isl_stat_error
;
1019 static isl_stat
foreach_lower_bound(__isl_keep isl_basic_set
*bset
,
1020 enum isl_dim_type type
, unsigned abs_pos
,
1021 __isl_take isl_basic_set
*context
, int n_lower
,
1022 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1023 __isl_take isl_constraint
*upper
,
1024 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1026 isl_basic_set
*context_i
;
1027 isl_constraint
*lower
= NULL
;
1030 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1031 if (isl_int_is_zero(bset
->ineq
[i
][1 + abs_pos
]))
1034 context_i
= set_largest_lower_bound(context
, bset
,
1035 abs_pos
, n_lower
, i
);
1036 if (isl_basic_set_is_empty(context_i
)) {
1037 isl_basic_set_free(context_i
);
1040 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1042 if (!lower
|| !context_i
)
1044 if (fn(lower
, NULL
, context_i
, user
) < 0)
1048 isl_basic_set_free(context
);
1050 if (i
< bset
->n_ineq
)
1051 return isl_stat_error
;
1055 isl_constraint_free(lower
);
1056 isl_basic_set_free(context_i
);
1057 isl_basic_set_free(context
);
1058 return isl_stat_error
;
1061 static isl_stat
foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1062 enum isl_dim_type type
, unsigned abs_pos
,
1063 __isl_take isl_basic_set
*context
, int n_lower
, int n_upper
,
1064 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1065 __isl_take isl_constraint
*upper
,
1066 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1068 isl_basic_set
*context_i
, *context_j
;
1069 isl_constraint
*lower
= NULL
;
1070 isl_constraint
*upper
= NULL
;
1073 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1074 if (!isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1077 context_i
= set_largest_lower_bound(context
, bset
,
1078 abs_pos
, n_lower
, i
);
1079 if (isl_basic_set_is_empty(context_i
)) {
1080 isl_basic_set_free(context_i
);
1084 for (j
= 0; j
< bset
->n_ineq
; ++j
) {
1085 if (!isl_int_is_neg(bset
->ineq
[j
][1 + abs_pos
]))
1088 context_j
= set_smallest_upper_bound(context_i
, bset
,
1089 abs_pos
, n_upper
, j
);
1090 context_j
= isl_basic_set_extend_constraints(context_j
,
1092 context_j
= add_larger_bound_constraint(context_j
,
1093 bset
->ineq
[i
], bset
->ineq
[j
], abs_pos
, 0);
1094 context_j
= isl_basic_set_simplify(context_j
);
1095 context_j
= isl_basic_set_finalize(context_j
);
1096 if (isl_basic_set_is_empty(context_j
)) {
1097 isl_basic_set_free(context_j
);
1100 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1102 upper
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1104 if (!lower
|| !upper
|| !context_j
)
1106 if (fn(lower
, upper
, context_j
, user
) < 0)
1110 isl_basic_set_free(context_i
);
1112 if (j
< bset
->n_ineq
)
1116 isl_basic_set_free(context
);
1118 if (i
< bset
->n_ineq
)
1119 return isl_stat_error
;
1123 isl_constraint_free(lower
);
1124 isl_constraint_free(upper
);
1125 isl_basic_set_free(context_i
);
1126 isl_basic_set_free(context_j
);
1127 isl_basic_set_free(context
);
1128 return isl_stat_error
;
1131 /* For each pair of lower and upper bounds on the variable "pos"
1132 * of type "type", call "fn" with these lower and upper bounds and the
1133 * set of constraints on the remaining variables where these bounds
1134 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1136 * If the designated variable is equal to an affine combination of the
1137 * other variables then fn is called with both lower and upper
1138 * set to the corresponding equality.
1140 * If there is no lower (or upper) bound, then NULL is passed
1141 * as the corresponding bound.
1143 * We first check if the variable is involved in any equality.
1144 * If not, we count the number of lower and upper bounds and
1147 isl_stat
isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set
*bset
,
1148 enum isl_dim_type type
, unsigned pos
,
1149 isl_stat (*fn
)(__isl_take isl_constraint
*lower
,
1150 __isl_take isl_constraint
*upper
,
1151 __isl_take isl_basic_set
*bset
, void *user
), void *user
)
1154 isl_constraint
*lower
= NULL
;
1155 isl_constraint
*upper
= NULL
;
1156 isl_basic_set
*context
= NULL
;
1158 int n_lower
, n_upper
;
1161 if (isl_basic_set_check_range(bset
, type
, pos
, 1) < 0)
1162 return isl_stat_error
;
1163 isl_assert(bset
->ctx
, type
== isl_dim_param
|| type
== isl_dim_set
,
1164 return isl_stat_error
);
1166 off
= isl_basic_set_var_offset(bset
, type
);
1168 return isl_stat_error
;
1169 abs_pos
= off
+ pos
;
1171 for (i
= 0; i
< bset
->n_eq
; ++i
) {
1172 if (isl_int_is_zero(bset
->eq
[i
][1 + abs_pos
]))
1175 lower
= isl_basic_set_constraint(isl_basic_set_copy(bset
),
1177 upper
= isl_constraint_copy(lower
);
1178 context
= isl_basic_set_remove_dims(isl_basic_set_copy(bset
),
1180 if (!lower
|| !upper
|| !context
)
1182 return fn(lower
, upper
, context
, user
);
1187 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
1188 if (isl_int_is_pos(bset
->ineq
[i
][1 + abs_pos
]))
1190 else if (isl_int_is_neg(bset
->ineq
[i
][1 + abs_pos
]))
1194 context
= isl_basic_set_copy(bset
);
1195 context
= isl_basic_set_cow(context
);
1198 for (i
= context
->n_ineq
- 1; i
>= 0; --i
)
1199 if (!isl_int_is_zero(context
->ineq
[i
][1 + abs_pos
]))
1200 isl_basic_set_drop_inequality(context
, i
);
1202 context
= isl_basic_set_drop(context
, type
, pos
, 1);
1203 if (!n_lower
&& !n_upper
)
1204 return fn(NULL
, NULL
, context
, user
);
1206 return foreach_upper_bound(bset
, type
, abs_pos
, context
, n_upper
,
1209 return foreach_lower_bound(bset
, type
, abs_pos
, context
, n_lower
,
1211 return foreach_bound_pair(bset
, type
, abs_pos
, context
, n_lower
, n_upper
,
1214 isl_constraint_free(lower
);
1215 isl_constraint_free(upper
);
1216 isl_basic_set_free(context
);
1217 return isl_stat_error
;
1220 __isl_give isl_aff
*isl_constraint_get_bound(
1221 __isl_keep isl_constraint
*constraint
, enum isl_dim_type type
, int pos
)
1227 if (isl_constraint_check_range(constraint
, type
, pos
, 1) < 0)
1229 space
= isl_constraint_peek_space(constraint
);
1230 if (isl_space_check_is_set(space
) < 0)
1233 ctx
= isl_constraint_get_ctx(constraint
);
1234 pos
+= offset(constraint
, type
);
1235 if (isl_int_is_zero(constraint
->v
->el
[pos
]))
1236 isl_die(ctx
, isl_error_invalid
,
1237 "constraint does not define a bound on given dimension",
1240 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
1244 if (isl_int_is_neg(constraint
->v
->el
[pos
]))
1245 isl_seq_cpy(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1247 isl_seq_neg(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1248 isl_int_set_si(aff
->v
->el
[1 + pos
], 0);
1249 isl_int_abs(aff
->v
->el
[0], constraint
->v
->el
[pos
]);
1254 /* For an inequality constraint
1258 * or an equality constraint
1262 * return the affine expression f.
1264 __isl_give isl_aff
*isl_constraint_get_aff(
1265 __isl_keep isl_constraint
*constraint
)
1272 aff
= isl_aff_alloc(isl_local_space_copy(constraint
->ls
));
1276 isl_seq_cpy(aff
->v
->el
+ 1, constraint
->v
->el
, aff
->v
->size
- 1);
1277 isl_int_set_si(aff
->v
->el
[0], 1);
1282 /* Construct an inequality (eq = 0) or equality (eq = 1) constraint from "aff".
1283 * In particular, construct aff >= 0 or aff = 0.
1285 * The denominator of "aff" can be ignored.
1287 static __isl_give isl_constraint
*isl_constraint_alloc_aff(int eq
,
1288 __isl_take isl_aff
*aff
)
1290 isl_local_space
*ls
;
1295 ls
= isl_aff_get_domain_local_space(aff
);
1296 v
= isl_vec_drop_els(isl_vec_copy(aff
->v
), 0, 1);
1299 return isl_constraint_alloc_vec(eq
, ls
, v
);
1302 /* Construct an equality constraint equating the given affine expression
1305 __isl_give isl_constraint
*isl_equality_from_aff(__isl_take isl_aff
*aff
)
1307 return isl_constraint_alloc_aff(1, aff
);
1310 /* Construct an inequality constraint enforcing the given affine expression
1311 * to be non-negative.
1313 __isl_give isl_constraint
*isl_inequality_from_aff(__isl_take isl_aff
*aff
)
1315 return isl_constraint_alloc_aff(0, aff
);
1318 /* Compare two isl_constraints.
1320 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1321 * than "c2" and 0 if they are equal.
1323 * The order is fairly arbitrary. We do consider constraints that only involve
1324 * earlier dimensions as "smaller".
1326 int isl_constraint_plain_cmp(__isl_keep isl_constraint
*c1
,
1327 __isl_keep isl_constraint
*c2
)
1338 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
1342 last1
= isl_seq_last_non_zero(c1
->v
->el
+ 1, c1
->v
->size
- 1);
1343 last2
= isl_seq_last_non_zero(c2
->v
->el
+ 1, c1
->v
->size
- 1);
1345 return last1
- last2
;
1347 return isl_seq_cmp(c1
->v
->el
, c2
->v
->el
, c1
->v
->size
);
1350 /* Compare two constraints based on their final (non-zero) coefficients.
1351 * In particular, the constraint that involves later variables or
1352 * that has a larger coefficient for a shared latest variable
1353 * is considered "greater" than the other constraint.
1355 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1356 * than "c2" and 0 if they are equal.
1358 * If the constraints live in different local spaces, then we cannot
1359 * really compare the constraints so we compare the local spaces instead.
1361 int isl_constraint_cmp_last_non_zero(__isl_keep isl_constraint
*c1
,
1362 __isl_keep isl_constraint
*c2
)
1373 cmp
= isl_local_space_cmp(c1
->ls
, c2
->ls
);
1377 last1
= isl_seq_last_non_zero(c1
->v
->el
+ 1, c1
->v
->size
- 1);
1378 last2
= isl_seq_last_non_zero(c2
->v
->el
+ 1, c1
->v
->size
- 1);
1380 return last1
- last2
;
1383 return isl_int_abs_cmp(c1
->v
->el
[1 + last1
], c2
->v
->el
[1 + last2
]);