?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
isl_scheduler.c: non_neg_lexmin: improve documentation
[isl.git] / isl_constraint.c
blob92a6bb89a3ad9074fa45ad320a4661437c523663
1 /*
2 * Copyright 2008-2009 Katholieke Universiteit Leuven
3 * Copyright 2010 INRIA Saclay
4 *
5 * Use of this software is governed by the MIT license
6 *
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
11 */
12
13 #include <isl_map_private.h>
14 #include <isl_constraint_private.h>
15 #include <isl_space_private.h>
16 #include <isl_seq.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>
21 #include <isl/deprecated/constraint_int.h>
22
23 #include <bset_to_bmap.c>
24 #include <bset_from_bmap.c>
25
26 #undef BASE
27 #define BASE constraint
28
29 #include <isl_list_templ.c>
30
31 isl_ctx *isl_constraint_get_ctx(__isl_keep isl_constraint *c)
32 {
33 return c ? isl_local_space_get_ctx(c->ls) : NULL;
34 }
35
36 static unsigned n(struct isl_constraint *c, enum isl_dim_type type)
37 {
38 return isl_local_space_dim(c->ls, type);
39 }
40
41 static unsigned offset(struct isl_constraint *c, enum isl_dim_type type)
42 {
43 return isl_local_space_offset(c->ls, type);
44 }
45
46 static unsigned basic_map_offset(__isl_keep isl_basic_map *bmap,
47 enum isl_dim_type type)
48 {
49 return type == isl_dim_div ? 1 + isl_space_dim(bmap->dim, isl_dim_all)
50 : 1 + isl_space_offset(bmap->dim, type);
51 }
52
53 static unsigned basic_set_offset(struct isl_basic_set *bset,
54 enum isl_dim_type type)
55 {
56 isl_space *dim = bset->dim;
57 switch (type) {
58 case isl_dim_param: return 1;
59 case isl_dim_in: return 1 + dim->nparam;
60 case isl_dim_out: return 1 + dim->nparam + dim->n_in;
61 case isl_dim_div: return 1 + dim->nparam + dim->n_in + dim->n_out;
62 default: return 0;
63 }
64 }
65
66 __isl_give isl_constraint *isl_constraint_alloc_vec(int eq,
67 __isl_take isl_local_space *ls, __isl_take isl_vec *v)
68 {
69 isl_constraint *constraint;
70
71 if (!ls || !v)
72 goto error;
73
74 constraint = isl_alloc_type(isl_vec_get_ctx(v), isl_constraint);
75 if (!constraint)
76 goto error;
77
78 constraint->ref = 1;
79 constraint->eq = eq;
80 constraint->ls = ls;
81 constraint->v = v;
82
83 return constraint;
84 error:
85 isl_local_space_free(ls);
86 isl_vec_free(v);
87 return NULL;
88 }
89
90 __isl_give isl_constraint *isl_constraint_alloc(int eq,
91 __isl_take isl_local_space *ls)
92 {
93 isl_ctx *ctx;
94 isl_vec *v;
95
96 if (!ls)
97 return NULL;
98
99 ctx = isl_local_space_get_ctx(ls);
100 v = isl_vec_alloc(ctx, 1 + isl_local_space_dim(ls, isl_dim_all));
101 v = isl_vec_clr(v);
102 return isl_constraint_alloc_vec(eq, ls, v);
103 }
104
105 struct isl_constraint *isl_basic_map_constraint(struct isl_basic_map *bmap,
106 isl_int **line)
107 {
108 int eq;
109 isl_ctx *ctx;
110 isl_vec *v;
111 isl_local_space *ls = NULL;
112 isl_constraint *constraint;
113
114 if (!bmap || !line)
115 goto error;
116
117 eq = line >= bmap->eq;
118
119 ctx = isl_basic_map_get_ctx(bmap);
120 ls = isl_basic_map_get_local_space(bmap);
121 v = isl_vec_alloc(ctx, 1 + isl_local_space_dim(ls, isl_dim_all));
122 if (!v)
123 goto error;
124 isl_seq_cpy(v->el, line[0], v->size);
125 constraint = isl_constraint_alloc_vec(eq, ls, v);
126
127 isl_basic_map_free(bmap);
128 return constraint;
129 error:
130 isl_local_space_free(ls);
131 isl_basic_map_free(bmap);
132 return NULL;
133 }
134
135 struct isl_constraint *isl_basic_set_constraint(struct isl_basic_set *bset,
136 isl_int **line)
137 {
138 return isl_basic_map_constraint(bset_to_bmap(bset), line);
139 }
140
141 __isl_give isl_constraint *isl_constraint_alloc_equality(
142 __isl_take isl_local_space *ls)
143 {
144 return isl_constraint_alloc(1, ls);
145 }
146
147 __isl_give isl_constraint *isl_constraint_alloc_inequality(
148 __isl_take isl_local_space *ls)
149 {
150 return isl_constraint_alloc(0, ls);
151 }
152
153 struct isl_constraint *isl_constraint_dup(struct isl_constraint *c)
154 {
155 if (!c)
156 return NULL;
157
158 return isl_constraint_alloc_vec(c->eq, isl_local_space_copy(c->ls),
159 isl_vec_copy(c->v));
160 }
161
162 struct isl_constraint *isl_constraint_cow(struct isl_constraint *c)
163 {
164 if (!c)
165 return NULL;
166
167 if (c->ref == 1)
168 return c;
169 c->ref--;
170 return isl_constraint_dup(c);
171 }
172
173 struct isl_constraint *isl_constraint_copy(struct isl_constraint *constraint)
174 {
175 if (!constraint)
176 return NULL;
177
178 constraint->ref++;
179 return constraint;
180 }
181
182 __isl_null isl_constraint *isl_constraint_free(__isl_take isl_constraint *c)
183 {
184 if (!c)
185 return NULL;
186
187 if (--c->ref > 0)
188 return NULL;
189
190 isl_local_space_free(c->ls);
191 isl_vec_free(c->v);
192 free(c);
193
194 return NULL;
195 }
196
197 /* Return the number of constraints in "bmap", i.e., the
198 * number of times isl_basic_map_foreach_constraint will
199 * call the callback.
200 */
201 int isl_basic_map_n_constraint(__isl_keep isl_basic_map *bmap)
202 {
203 if (!bmap)
204 return -1;
205
206 return bmap->n_eq + bmap->n_ineq;
207 }
208
209 /* Return the number of constraints in "bset", i.e., the
210 * number of times isl_basic_set_foreach_constraint will
211 * call the callback.
212 */
213 int isl_basic_set_n_constraint(__isl_keep isl_basic_set *bset)
214 {
215 return isl_basic_map_n_constraint(bset);
216 }
217
218 isl_stat isl_basic_map_foreach_constraint(__isl_keep isl_basic_map *bmap,
219 isl_stat (*fn)(__isl_take isl_constraint *c, void *user), void *user)
220 {
221 int i;
222 struct isl_constraint *c;
223
224 if (!bmap)
225 return isl_stat_error;
226
227 isl_assert(bmap->ctx, ISL_F_ISSET(bmap, ISL_BASIC_MAP_FINAL),
228 return isl_stat_error);
229
230 for (i = 0; i < bmap->n_eq; ++i) {
231 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
232 &bmap->eq[i]);
233 if (!c)
234 return isl_stat_error;
235 if (fn(c, user) < 0)
236 return isl_stat_error;
237 }
238
239 for (i = 0; i < bmap->n_ineq; ++i) {
240 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
241 &bmap->ineq[i]);
242 if (!c)
243 return isl_stat_error;
244 if (fn(c, user) < 0)
245 return isl_stat_error;
246 }
247
248 return isl_stat_ok;
249 }
250
251 isl_stat isl_basic_set_foreach_constraint(__isl_keep isl_basic_set *bset,
252 isl_stat (*fn)(__isl_take isl_constraint *c, void *user), void *user)
253 {
254 return isl_basic_map_foreach_constraint(bset_to_bmap(bset), fn, user);
255 }
256
257 /* Add the constraint to the list that "user" points to, if it is not
258 * a div constraint.
259 */
260 static isl_stat collect_constraint(__isl_take isl_constraint *constraint,
261 void *user)
262 {
263 isl_constraint_list **list = user;
264
265 if (isl_constraint_is_div_constraint(constraint))
266 isl_constraint_free(constraint);
267 else
268 *list = isl_constraint_list_add(*list, constraint);
269
270 return isl_stat_ok;
271 }
272
273 /* Return a list of constraints that, when combined, are equivalent
274 * to "bmap". The input is required to have only known divs.
275 *
276 * There is no need to include the div constraints as they are
277 * implied by the div expressions.
278 */
279 __isl_give isl_constraint_list *isl_basic_map_get_constraint_list(
280 __isl_keep isl_basic_map *bmap)
281 {
282 int n;
283 int known;
284 isl_ctx *ctx;
285 isl_constraint_list *list;
286
287 known = isl_basic_map_divs_known(bmap);
288 if (known < 0)
289 return NULL;
290 ctx = isl_basic_map_get_ctx(bmap);
291 if (!known)
292 isl_die(ctx, isl_error_invalid,
293 "input involves unknown divs", return NULL);
294
295 n = isl_basic_map_n_constraint(bmap);
296 list = isl_constraint_list_alloc(ctx, n);
297 if (isl_basic_map_foreach_constraint(bmap,
298 &collect_constraint, &list) < 0)
299 list = isl_constraint_list_free(list);
300
301 return list;
302 }
303
304 /* Return a list of constraints that, when combined, are equivalent
305 * to "bset". The input is required to have only known divs.
306 */
307 __isl_give isl_constraint_list *isl_basic_set_get_constraint_list(
308 __isl_keep isl_basic_set *bset)
309 {
310 return isl_basic_map_get_constraint_list(bset);
311 }
312
313 int isl_constraint_is_equal(struct isl_constraint *constraint1,
314 struct isl_constraint *constraint2)
315 {
316 int equal;
317
318 if (!constraint1 || !constraint2)
319 return 0;
320 if (constraint1->eq != constraint2->eq)
321 return 0;
322 equal = isl_local_space_is_equal(constraint1->ls, constraint2->ls);
323 if (equal < 0 || !equal)
324 return equal;
325 return isl_vec_is_equal(constraint1->v, constraint2->v);
326 }
327
328 struct isl_basic_map *isl_basic_map_add_constraint(
329 struct isl_basic_map *bmap, struct isl_constraint *constraint)
330 {
331 isl_ctx *ctx;
332 isl_space *dim;
333 int equal_space;
334
335 if (!bmap || !constraint)
336 goto error;
337
338 ctx = isl_constraint_get_ctx(constraint);
339 dim = isl_constraint_get_space(constraint);
340 equal_space = isl_space_is_equal(bmap->dim, dim);
341 isl_space_free(dim);
342 isl_assert(ctx, equal_space, goto error);
343
344 bmap = isl_basic_map_intersect(bmap,
345 isl_basic_map_from_constraint(constraint));
346 return bmap;
347 error:
348 isl_basic_map_free(bmap);
349 isl_constraint_free(constraint);
350 return NULL;
351 }
352
353 struct isl_basic_set *isl_basic_set_add_constraint(
354 struct isl_basic_set *bset, struct isl_constraint *constraint)
355 {
356 return bset_from_bmap(isl_basic_map_add_constraint(bset_to_bmap(bset),
357 constraint));
358 }
359
360 __isl_give isl_map *isl_map_add_constraint(__isl_take isl_map *map,
361 __isl_take isl_constraint *constraint)
362 {
363 isl_basic_map *bmap;
364
365 bmap = isl_basic_map_from_constraint(constraint);
366 map = isl_map_intersect(map, isl_map_from_basic_map(bmap));
367
368 return map;
369 }
370
371 __isl_give isl_set *isl_set_add_constraint(__isl_take isl_set *set,
372 __isl_take isl_constraint *constraint)
373 {
374 return isl_map_add_constraint(set, constraint);
375 }
376
377 __isl_give isl_space *isl_constraint_get_space(
378 __isl_keep isl_constraint *constraint)
379 {
380 return constraint ? isl_local_space_get_space(constraint->ls) : NULL;
381 }
382
383 __isl_give isl_local_space *isl_constraint_get_local_space(
384 __isl_keep isl_constraint *constraint)
385 {
386 return constraint ? isl_local_space_copy(constraint->ls) : NULL;
387 }
388
389 int isl_constraint_dim(struct isl_constraint *constraint,
390 enum isl_dim_type type)
391 {
392 if (!constraint)
393 return -1;
394 return n(constraint, type);
395 }
396
397 isl_bool isl_constraint_involves_dims(__isl_keep isl_constraint *constraint,
398 enum isl_dim_type type, unsigned first, unsigned n)
399 {
400 int i;
401 isl_ctx *ctx;
402 int *active = NULL;
403 isl_bool involves = isl_bool_false;
404
405 if (!constraint)
406 return isl_bool_error;
407 if (n == 0)
408 return isl_bool_false;
409
410 ctx = isl_constraint_get_ctx(constraint);
411 if (first + n > isl_constraint_dim(constraint, type))
412 isl_die(ctx, isl_error_invalid,
413 "range out of bounds", return isl_bool_error);
414
415 active = isl_local_space_get_active(constraint->ls,
416 constraint->v->el + 1);
417 if (!active)
418 goto error;
419
420 first += isl_local_space_offset(constraint->ls, type) - 1;
421 for (i = 0; i < n; ++i)
422 if (active[first + i]) {
423 involves = isl_bool_true;
424 break;
425 }
426
427 free(active);
428
429 return involves;
430 error:
431 free(active);
432 return isl_bool_error;
433 }
434
435 /* Does the given constraint represent a lower bound on the given
436 * dimension?
437 */
438 isl_bool isl_constraint_is_lower_bound(__isl_keep isl_constraint *constraint,
439 enum isl_dim_type type, unsigned pos)
440 {
441 if (!constraint)
442 return isl_bool_error;
443
444 if (pos >= isl_local_space_dim(constraint->ls, type))
445 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
446 "position out of bounds", return isl_bool_error);
447
448 pos += isl_local_space_offset(constraint->ls, type);
449 return isl_int_is_pos(constraint->v->el[pos]);
450 }
451
452 /* Does the given constraint represent an upper bound on the given
453 * dimension?
454 */
455 isl_bool isl_constraint_is_upper_bound(__isl_keep isl_constraint *constraint,
456 enum isl_dim_type type, unsigned pos)
457 {
458 if (!constraint)
459 return isl_bool_error;
460
461 if (pos >= isl_local_space_dim(constraint->ls, type))
462 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
463 "position out of bounds", return isl_bool_error);
464
465 pos += isl_local_space_offset(constraint->ls, type);
466 return isl_int_is_neg(constraint->v->el[pos]);
467 }
468
469 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint *constraint,
470 enum isl_dim_type type, unsigned pos)
471 {
472 return constraint ?
473 isl_local_space_get_dim_name(constraint->ls, type, pos) : NULL;
474 }
475
476 void isl_constraint_get_constant(__isl_keep isl_constraint *constraint,
477 isl_int *v)
478 {
479 if (!constraint)
480 return;
481 isl_int_set(*v, constraint->v->el[0]);
482 }
483
484 /* Return the constant term of "constraint".
485 */
486 __isl_give isl_val *isl_constraint_get_constant_val(
487 __isl_keep isl_constraint *constraint)
488 {
489 isl_ctx *ctx;
490
491 if (!constraint)
492 return NULL;
493
494 ctx = isl_constraint_get_ctx(constraint);
495 return isl_val_int_from_isl_int(ctx, constraint->v->el[0]);
496 }
497
498 void isl_constraint_get_coefficient(struct isl_constraint *constraint,
499 enum isl_dim_type type, int pos, isl_int *v)
500 {
501 if (!constraint)
502 return;
503
504 if (pos >= isl_local_space_dim(constraint->ls, type))
505 isl_die(constraint->v->ctx, isl_error_invalid,
506 "position out of bounds", return);
507
508 pos += isl_local_space_offset(constraint->ls, type);
509 isl_int_set(*v, constraint->v->el[pos]);
510 }
511
512 /* Return the coefficient of the variable of type "type" at position "pos"
513 * of "constraint".
514 */
515 __isl_give isl_val *isl_constraint_get_coefficient_val(
516 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
517 {
518 isl_ctx *ctx;
519
520 if (!constraint)
521 return NULL;
522
523 ctx = isl_constraint_get_ctx(constraint);
524 if (pos < 0 || pos >= isl_local_space_dim(constraint->ls, type))
525 isl_die(ctx, isl_error_invalid,
526 "position out of bounds", return NULL);
527
528 pos += isl_local_space_offset(constraint->ls, type);
529 return isl_val_int_from_isl_int(ctx, constraint->v->el[pos]);
530 }
531
532 __isl_give isl_aff *isl_constraint_get_div(__isl_keep isl_constraint *constraint,
533 int pos)
534 {
535 if (!constraint)
536 return NULL;
537
538 return isl_local_space_get_div(constraint->ls, pos);
539 }
540
541 __isl_give isl_constraint *isl_constraint_set_constant(
542 __isl_take isl_constraint *constraint, isl_int v)
543 {
544 constraint = isl_constraint_cow(constraint);
545 if (!constraint)
546 return NULL;
547
548 constraint->v = isl_vec_cow(constraint->v);
549 if (!constraint->v)
550 return isl_constraint_free(constraint);
551
552 isl_int_set(constraint->v->el[0], v);
553 return constraint;
554 }
555
556 /* Replace the constant term of "constraint" by "v".
557 */
558 __isl_give isl_constraint *isl_constraint_set_constant_val(
559 __isl_take isl_constraint *constraint, __isl_take isl_val *v)
560 {
561 constraint = isl_constraint_cow(constraint);
562 if (!constraint || !v)
563 goto error;
564 if (!isl_val_is_int(v))
565 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
566 "expecting integer value", goto error);
567 constraint->v = isl_vec_set_element_val(constraint->v, 0, v);
568 if (!constraint->v)
569 constraint = isl_constraint_free(constraint);
570 return constraint;
571 error:
572 isl_val_free(v);
573 return isl_constraint_free(constraint);
574 }
575
576 __isl_give isl_constraint *isl_constraint_set_constant_si(
577 __isl_take isl_constraint *constraint, int v)
578 {
579 constraint = isl_constraint_cow(constraint);
580 if (!constraint)
581 return NULL;
582
583 constraint->v = isl_vec_cow(constraint->v);
584 if (!constraint->v)
585 return isl_constraint_free(constraint);
586
587 isl_int_set_si(constraint->v->el[0], v);
588 return constraint;
589 }
590
591 __isl_give isl_constraint *isl_constraint_set_coefficient(
592 __isl_take isl_constraint *constraint,
593 enum isl_dim_type type, int pos, isl_int v)
594 {
595 constraint = isl_constraint_cow(constraint);
596 if (!constraint)
597 return NULL;
598
599 if (pos >= isl_local_space_dim(constraint->ls, type))
600 isl_die(constraint->v->ctx, isl_error_invalid,
601 "position out of bounds",
602 return isl_constraint_free(constraint));
603
604 constraint = isl_constraint_cow(constraint);
605 if (!constraint)
606 return NULL;
607
608 constraint->v = isl_vec_cow(constraint->v);
609 if (!constraint->v)
610 return isl_constraint_free(constraint);
611
612 pos += isl_local_space_offset(constraint->ls, type);
613 isl_int_set(constraint->v->el[pos], v);
614
615 return constraint;
616 }
617
618 /* Replace the coefficient of the variable of type "type" at position "pos"
619 * of "constraint" by "v".
620 */
621 __isl_give isl_constraint *isl_constraint_set_coefficient_val(
622 __isl_take isl_constraint *constraint,
623 enum isl_dim_type type, int pos, __isl_take isl_val *v)
624 {
625 constraint = isl_constraint_cow(constraint);
626 if (!constraint || !v)
627 goto error;
628 if (!isl_val_is_int(v))
629 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
630 "expecting integer value", goto error);
631
632 if (pos >= isl_local_space_dim(constraint->ls, type))
633 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
634 "position out of bounds", goto error);
635
636 pos += isl_local_space_offset(constraint->ls, type);
637 constraint->v = isl_vec_set_element_val(constraint->v, pos, v);
638 if (!constraint->v)
639 constraint = isl_constraint_free(constraint);
640 return constraint;
641 error:
642 isl_val_free(v);
643 return isl_constraint_free(constraint);
644 }
645
646 __isl_give isl_constraint *isl_constraint_set_coefficient_si(
647 __isl_take isl_constraint *constraint,
648 enum isl_dim_type type, int pos, int v)
649 {
650 constraint = isl_constraint_cow(constraint);
651 if (!constraint)
652 return NULL;
653
654 if (pos >= isl_local_space_dim(constraint->ls, type))
655 isl_die(constraint->v->ctx, isl_error_invalid,
656 "position out of bounds",
657 return isl_constraint_free(constraint));
658
659 constraint = isl_constraint_cow(constraint);
660 if (!constraint)
661 return NULL;
662
663 constraint->v = isl_vec_cow(constraint->v);
664 if (!constraint->v)
665 return isl_constraint_free(constraint);
666
667 pos += isl_local_space_offset(constraint->ls, type);
668 isl_int_set_si(constraint->v->el[pos], v);
669
670 return constraint;
671 }
672
673 struct isl_constraint *isl_constraint_negate(struct isl_constraint *constraint)
674 {
675 isl_ctx *ctx;
676
677 constraint = isl_constraint_cow(constraint);
678 if (!constraint)
679 return NULL;
680
681 ctx = isl_constraint_get_ctx(constraint);
682 if (isl_constraint_is_equality(constraint))
683 isl_die(ctx, isl_error_invalid, "cannot negate equality",
684 return isl_constraint_free(constraint));
685 constraint->v = isl_vec_neg(constraint->v);
686 constraint->v = isl_vec_cow(constraint->v);
687 if (!constraint->v)
688 return isl_constraint_free(constraint);
689 isl_int_sub_ui(constraint->v->el[0], constraint->v->el[0], 1);
690 return constraint;
691 }
692
693 isl_bool isl_constraint_is_equality(struct isl_constraint *constraint)
694 {
695 if (!constraint)
696 return isl_bool_error;
697 return constraint->eq;
698 }
699
700 int isl_constraint_is_div_constraint(__isl_keep isl_constraint *constraint)
701 {
702 int i;
703 int n_div;
704
705 if (!constraint)
706 return -1;
707 if (isl_constraint_is_equality(constraint))
708 return 0;
709 n_div = isl_constraint_dim(constraint, isl_dim_div);
710 for (i = 0; i < n_div; ++i) {
711 isl_bool is_div;
712 is_div = isl_local_space_is_div_constraint(constraint->ls,
713 constraint->v->el, i);
714 if (is_div < 0 || is_div)
715 return is_div;
716 }
717
718 return 0;
719 }
720
721 /* We manually set ISL_BASIC_SET_FINAL instead of calling
722 * isl_basic_map_finalize because we want to keep the position
723 * of the divs and we therefore do not want to throw away redundant divs.
724 * This is arguably a bit fragile.
725 */
726 __isl_give isl_basic_map *isl_basic_map_from_constraint(
727 __isl_take isl_constraint *constraint)
728 {
729 int k;
730 isl_local_space *ls;
731 struct isl_basic_map *bmap;
732 isl_int *c;
733 unsigned total;
734
735 if (!constraint)
736 return NULL;
737
738 ls = isl_local_space_copy(constraint->ls);
739 bmap = isl_basic_map_from_local_space(ls);
740 bmap = isl_basic_map_extend_constraints(bmap, 1, 1);
741 if (isl_constraint_is_equality(constraint)) {
742 k = isl_basic_map_alloc_equality(bmap);
743 if (k < 0)
744 goto error;
745 c = bmap->eq[k];
746 }
747 else {
748 k = isl_basic_map_alloc_inequality(bmap);
749 if (k < 0)
750 goto error;
751 c = bmap->ineq[k];
752 }
753 total = isl_basic_map_total_dim(bmap);
754 isl_seq_cpy(c, constraint->v->el, 1 + total);
755 isl_constraint_free(constraint);
756 if (bmap)
757 ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);
758 return bmap;
759 error:
760 isl_constraint_free(constraint);
761 isl_basic_map_free(bmap);
762 return NULL;
763 }
764
765 __isl_give isl_basic_set *isl_basic_set_from_constraint(
766 __isl_take isl_constraint *constraint)
767 {
768 if (!constraint)
769 return NULL;
770
771 if (isl_constraint_dim(constraint, isl_dim_in) != 0)
772 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
773 "not a set constraint", goto error);
774 return bset_from_bmap(isl_basic_map_from_constraint(constraint));
775 error:
776 isl_constraint_free(constraint);
777 return NULL;
778 }
779
780 /* Is the variable of "type" at position "pos" of "bmap" defined
781 * in terms of earlier dimensions through an equality?
782 *
783 * If so, and if c is not NULL, then return a copy of this equality in *c.
784 */
785 isl_bool isl_basic_map_has_defining_equality(
786 __isl_keep isl_basic_map *bmap, enum isl_dim_type type, int pos,
787 __isl_give isl_constraint **c)
788 {
789 int i;
790 unsigned offset;
791 unsigned total;
792
793 if (!bmap)
794 return isl_bool_error;
795 offset = basic_map_offset(bmap, type);
796 total = isl_basic_map_total_dim(bmap);
797 if (pos >= isl_basic_map_dim(bmap, type))
798 isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid,
799 "invalid position", return isl_bool_error);
800 for (i = 0; i < bmap->n_eq; ++i) {
801 if (isl_int_is_zero(bmap->eq[i][offset + pos]) ||
802 isl_seq_first_non_zero(bmap->eq[i]+offset+pos+1,
803 1+total-offset-pos-1) != -1)
804 continue;
805 if (c)
806 *c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
807 &bmap->eq[i]);
808 return isl_bool_true;
809 }
810 return isl_bool_false;
811 }
812
813 /* Is the variable of "type" at position "pos" of "bset" defined
814 * in terms of earlier dimensions through an equality?
815 *
816 * If so, and if c is not NULL, then return a copy of this equality in *c.
817 */
818 isl_bool isl_basic_set_has_defining_equality(
819 __isl_keep isl_basic_set *bset, enum isl_dim_type type, int pos,
820 __isl_give isl_constraint **c)
821 {
822 return isl_basic_map_has_defining_equality(bset_to_bmap(bset),
823 type, pos, c);
824 }
825
826 isl_bool isl_basic_set_has_defining_inequalities(
827 struct isl_basic_set *bset, enum isl_dim_type type, int pos,
828 struct isl_constraint **lower,
829 struct isl_constraint **upper)
830 {
831 int i, j;
832 unsigned offset;
833 unsigned total;
834 isl_int m;
835 isl_int **lower_line, **upper_line;
836
837 if (!bset)
838 return isl_bool_error;
839 offset = basic_set_offset(bset, type);
840 total = isl_basic_set_total_dim(bset);
841 if (pos >= isl_basic_set_dim(bset, type))
842 isl_die(isl_basic_set_get_ctx(bset), isl_error_invalid,
843 "invalid position", return isl_bool_error);
844 isl_int_init(m);
845 for (i = 0; i < bset->n_ineq; ++i) {
846 if (isl_int_is_zero(bset->ineq[i][offset + pos]))
847 continue;
848 if (isl_int_is_one(bset->ineq[i][offset + pos]))
849 continue;
850 if (isl_int_is_negone(bset->ineq[i][offset + pos]))
851 continue;
852 if (isl_seq_first_non_zero(bset->ineq[i]+offset+pos+1,
853 1+total-offset-pos-1) != -1)
854 continue;
855 for (j = i + 1; j < bset->n_ineq; ++j) {
856 if (!isl_seq_is_neg(bset->ineq[i]+1, bset->ineq[j]+1,
857 total))
858 continue;
859 isl_int_add(m, bset->ineq[i][0], bset->ineq[j][0]);
860 if (isl_int_abs_ge(m, bset->ineq[i][offset+pos]))
861 continue;
862
863 if (isl_int_is_pos(bset->ineq[i][offset+pos])) {
864 lower_line = &bset->ineq[i];
865 upper_line = &bset->ineq[j];
866 } else {
867 lower_line = &bset->ineq[j];
868 upper_line = &bset->ineq[i];
869 }
870 *lower = isl_basic_set_constraint(
871 isl_basic_set_copy(bset), lower_line);
872 *upper = isl_basic_set_constraint(
873 isl_basic_set_copy(bset), upper_line);
874 isl_int_clear(m);
875 return isl_bool_true;
876 }
877 }
878 *lower = NULL;
879 *upper = NULL;
880 isl_int_clear(m);
881 return isl_bool_false;
882 }
883
884 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
885 * (in "a" and "b"), add a constraint to "bset" that ensures that the
886 * bound implied by "a" is (strictly) larger than the bound implied by "b".
887 *
888 * If both constraints imply lower bounds, then this means that "a" is
889 * active in the result.
890 * If both constraints imply upper bounds, then this means that "b" is
891 * active in the result.
892 */
893 static __isl_give isl_basic_set *add_larger_bound_constraint(
894 __isl_take isl_basic_set *bset, isl_int *a, isl_int *b,
895 unsigned abs_pos, int strict)
896 {
897 int k;
898 isl_int t;
899 unsigned total;
900
901 k = isl_basic_set_alloc_inequality(bset);
902 if (k < 0)
903 goto error;
904
905 total = isl_basic_set_dim(bset, isl_dim_all);
906
907 isl_int_init(t);
908 isl_int_neg(t, b[1 + abs_pos]);
909
910 isl_seq_combine(bset->ineq[k], t, a, a[1 + abs_pos], b, 1 + abs_pos);
911 isl_seq_combine(bset->ineq[k] + 1 + abs_pos,
912 t, a + 1 + abs_pos + 1, a[1 + abs_pos], b + 1 + abs_pos + 1,
913 total - abs_pos);
914
915 if (strict)
916 isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
917
918 isl_int_clear(t);
919
920 return bset;
921 error:
922 isl_basic_set_free(bset);
923 return NULL;
924 }
925
926 /* Add constraints to "context" that ensure that "u" is the smallest
927 * (and therefore active) upper bound on "abs_pos" in "bset" and return
928 * the resulting basic set.
929 */
930 static __isl_give isl_basic_set *set_smallest_upper_bound(
931 __isl_keep isl_basic_set *context,
932 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_upper, int u)
933 {
934 int j;
935
936 context = isl_basic_set_copy(context);
937 context = isl_basic_set_cow(context);
938
939 context = isl_basic_set_extend_constraints(context, 0, n_upper - 1);
940
941 for (j = 0; j < bset->n_ineq; ++j) {
942 if (j == u)
943 continue;
944 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
945 continue;
946 context = add_larger_bound_constraint(context,
947 bset->ineq[j], bset->ineq[u], abs_pos, j > u);
948 }
949
950 context = isl_basic_set_simplify(context);
951 context = isl_basic_set_finalize(context);
952
953 return context;
954 }
955
956 /* Add constraints to "context" that ensure that "u" is the largest
957 * (and therefore active) upper bound on "abs_pos" in "bset" and return
958 * the resulting basic set.
959 */
960 static __isl_give isl_basic_set *set_largest_lower_bound(
961 __isl_keep isl_basic_set *context,
962 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_lower, int l)
963 {
964 int j;
965
966 context = isl_basic_set_copy(context);
967 context = isl_basic_set_cow(context);
968
969 context = isl_basic_set_extend_constraints(context, 0, n_lower - 1);
970
971 for (j = 0; j < bset->n_ineq; ++j) {
972 if (j == l)
973 continue;
974 if (!isl_int_is_pos(bset->ineq[j][1 + abs_pos]))
975 continue;
976 context = add_larger_bound_constraint(context,
977 bset->ineq[l], bset->ineq[j], abs_pos, j > l);
978 }
979
980 context = isl_basic_set_simplify(context);
981 context = isl_basic_set_finalize(context);
982
983 return context;
984 }
985
986 static isl_stat foreach_upper_bound(__isl_keep isl_basic_set *bset,
987 enum isl_dim_type type, unsigned abs_pos,
988 __isl_take isl_basic_set *context, int n_upper,
989 isl_stat (*fn)(__isl_take isl_constraint *lower,
990 __isl_take isl_constraint *upper,
991 __isl_take isl_basic_set *bset, void *user), void *user)
992 {
993 isl_basic_set *context_i;
994 isl_constraint *upper = NULL;
995 int i;
996
997 for (i = 0; i < bset->n_ineq; ++i) {
998 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
999 continue;
1000
1001 context_i = set_smallest_upper_bound(context, bset,
1002 abs_pos, n_upper, i);
1003 if (isl_basic_set_is_empty(context_i)) {
1004 isl_basic_set_free(context_i);
1005 continue;
1006 }
1007 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
1008 &bset->ineq[i]);
1009 if (!upper || !context_i)
1010 goto error;
1011 if (fn(NULL, upper, context_i, user) < 0)
1012 break;
1013 }
1014
1015 isl_basic_set_free(context);
1016
1017 if (i < bset->n_ineq)
1018 return isl_stat_error;
1019
1020 return isl_stat_ok;
1021 error:
1022 isl_constraint_free(upper);
1023 isl_basic_set_free(context_i);
1024 isl_basic_set_free(context);
1025 return isl_stat_error;
1026 }
1027
1028 static isl_stat foreach_lower_bound(__isl_keep isl_basic_set *bset,
1029 enum isl_dim_type type, unsigned abs_pos,
1030 __isl_take isl_basic_set *context, int n_lower,
1031 isl_stat (*fn)(__isl_take isl_constraint *lower,
1032 __isl_take isl_constraint *upper,
1033 __isl_take isl_basic_set *bset, void *user), void *user)
1034 {
1035 isl_basic_set *context_i;
1036 isl_constraint *lower = NULL;
1037 int i;
1038
1039 for (i = 0; i < bset->n_ineq; ++i) {
1040 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
1041 continue;
1042
1043 context_i = set_largest_lower_bound(context, bset,
1044 abs_pos, n_lower, i);
1045 if (isl_basic_set_is_empty(context_i)) {
1046 isl_basic_set_free(context_i);
1047 continue;
1048 }
1049 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1050 &bset->ineq[i]);
1051 if (!lower || !context_i)
1052 goto error;
1053 if (fn(lower, NULL, context_i, user) < 0)
1054 break;
1055 }
1056
1057 isl_basic_set_free(context);
1058
1059 if (i < bset->n_ineq)
1060 return isl_stat_error;
1061
1062 return isl_stat_ok;
1063 error:
1064 isl_constraint_free(lower);
1065 isl_basic_set_free(context_i);
1066 isl_basic_set_free(context);
1067 return isl_stat_error;
1068 }
1069
1070 static isl_stat foreach_bound_pair(__isl_keep isl_basic_set *bset,
1071 enum isl_dim_type type, unsigned abs_pos,
1072 __isl_take isl_basic_set *context, int n_lower, int n_upper,
1073 isl_stat (*fn)(__isl_take isl_constraint *lower,
1074 __isl_take isl_constraint *upper,
1075 __isl_take isl_basic_set *bset, void *user), void *user)
1076 {
1077 isl_basic_set *context_i, *context_j;
1078 isl_constraint *lower = NULL;
1079 isl_constraint *upper = NULL;
1080 int i, j;
1081
1082 for (i = 0; i < bset->n_ineq; ++i) {
1083 if (!isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
1084 continue;
1085
1086 context_i = set_largest_lower_bound(context, bset,
1087 abs_pos, n_lower, i);
1088 if (isl_basic_set_is_empty(context_i)) {
1089 isl_basic_set_free(context_i);
1090 continue;
1091 }
1092
1093 for (j = 0; j < bset->n_ineq; ++j) {
1094 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
1095 continue;
1096
1097 context_j = set_smallest_upper_bound(context_i, bset,
1098 abs_pos, n_upper, j);
1099 context_j = isl_basic_set_extend_constraints(context_j,
1100 0, 1);
1101 context_j = add_larger_bound_constraint(context_j,
1102 bset->ineq[i], bset->ineq[j], abs_pos, 0);
1103 context_j = isl_basic_set_simplify(context_j);
1104 context_j = isl_basic_set_finalize(context_j);
1105 if (isl_basic_set_is_empty(context_j)) {
1106 isl_basic_set_free(context_j);
1107 continue;
1108 }
1109 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1110 &bset->ineq[i]);
1111 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
1112 &bset->ineq[j]);
1113 if (!lower || !upper || !context_j)
1114 goto error;
1115 if (fn(lower, upper, context_j, user) < 0)
1116 break;
1117 }
1118
1119 isl_basic_set_free(context_i);
1120
1121 if (j < bset->n_ineq)
1122 break;
1123 }
1124
1125 isl_basic_set_free(context);
1126
1127 if (i < bset->n_ineq)
1128 return isl_stat_error;
1129
1130 return isl_stat_ok;
1131 error:
1132 isl_constraint_free(lower);
1133 isl_constraint_free(upper);
1134 isl_basic_set_free(context_i);
1135 isl_basic_set_free(context_j);
1136 isl_basic_set_free(context);
1137 return isl_stat_error;
1138 }
1139
1140 /* For each pair of lower and upper bounds on the variable "pos"
1141 * of type "type", call "fn" with these lower and upper bounds and the
1142 * set of constraints on the remaining variables where these bounds
1143 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
1144 *
1145 * If the designated variable is equal to an affine combination of the
1146 * other variables then fn is called with both lower and upper
1147 * set to the corresponding equality.
1148 *
1149 * If there is no lower (or upper) bound, then NULL is passed
1150 * as the corresponding bound.
1151 *
1152 * We first check if the variable is involved in any equality.
1153 * If not, we count the number of lower and upper bounds and
1154 * act accordingly.
1155 */
1156 isl_stat isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set *bset,
1157 enum isl_dim_type type, unsigned pos,
1158 isl_stat (*fn)(__isl_take isl_constraint *lower,
1159 __isl_take isl_constraint *upper,
1160 __isl_take isl_basic_set *bset, void *user), void *user)
1161 {
1162 int i;
1163 isl_constraint *lower = NULL;
1164 isl_constraint *upper = NULL;
1165 isl_basic_set *context = NULL;
1166 unsigned abs_pos;
1167 int n_lower, n_upper;
1168
1169 if (!bset)
1170 return isl_stat_error;
1171 isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type),
1172 return isl_stat_error);
1173 isl_assert(bset->ctx, type == isl_dim_param || type == isl_dim_set,
1174 return isl_stat_error);
1175
1176 abs_pos = pos;
1177 if (type == isl_dim_set)
1178 abs_pos += isl_basic_set_dim(bset, isl_dim_param);
1179
1180 for (i = 0; i < bset->n_eq; ++i) {
1181 if (isl_int_is_zero(bset->eq[i][1 + abs_pos]))
1182 continue;
1183
1184 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1185 &bset->eq[i]);
1186 upper = isl_constraint_copy(lower);
1187 context = isl_basic_set_remove_dims(isl_basic_set_copy(bset),
1188 type, pos, 1);
1189 if (!lower || !upper || !context)
1190 goto error;
1191 return fn(lower, upper, context, user);
1192 }
1193
1194 n_lower = 0;
1195 n_upper = 0;
1196 for (i = 0; i < bset->n_ineq; ++i) {
1197 if (isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
1198 n_lower++;
1199 else if (isl_int_is_neg(bset->ineq[i][1 + abs_pos]))
1200 n_upper++;
1201 }
1202
1203 context = isl_basic_set_copy(bset);
1204 context = isl_basic_set_cow(context);
1205 if (!context)
1206 goto error;
1207 for (i = context->n_ineq - 1; i >= 0; --i)
1208 if (!isl_int_is_zero(context->ineq[i][1 + abs_pos]))
1209 isl_basic_set_drop_inequality(context, i);
1210
1211 context = isl_basic_set_drop(context, type, pos, 1);
1212 if (!n_lower && !n_upper)
1213 return fn(NULL, NULL, context, user);
1214 if (!n_lower)
1215 return foreach_upper_bound(bset, type, abs_pos, context, n_upper,
1216 fn, user);
1217 if (!n_upper)
1218 return foreach_lower_bound(bset, type, abs_pos, context, n_lower,
1219 fn, user);
1220 return foreach_bound_pair(bset, type, abs_pos, context, n_lower, n_upper,
1221 fn, user);
1222 error:
1223 isl_constraint_free(lower);
1224 isl_constraint_free(upper);
1225 isl_basic_set_free(context);
1226 return -1;
1227 }
1228
1229 __isl_give isl_aff *isl_constraint_get_bound(
1230 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
1231 {
1232 isl_aff *aff;
1233 isl_ctx *ctx;
1234
1235 if (!constraint)
1236 return NULL;
1237 ctx = isl_constraint_get_ctx(constraint);
1238 if (pos >= isl_constraint_dim(constraint, type))
1239 isl_die(ctx, isl_error_invalid,
1240 "index out of bounds", return NULL);
1241 if (isl_constraint_dim(constraint, isl_dim_in) != 0)
1242 isl_die(ctx, isl_error_invalid,
1243 "not a set constraint", return NULL);
1244
1245 pos += offset(constraint, type);
1246 if (isl_int_is_zero(constraint->v->el[pos]))
1247 isl_die(ctx, isl_error_invalid,
1248 "constraint does not define a bound on given dimension",
1249 return NULL);
1250
1251 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));
1252 if (!aff)
1253 return NULL;
1254
1255 if (isl_int_is_neg(constraint->v->el[pos]))
1256 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1257 else
1258 isl_seq_neg(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1259 isl_int_set_si(aff->v->el[1 + pos], 0);
1260 isl_int_abs(aff->v->el[0], constraint->v->el[pos]);
1261
1262 return aff;
1263 }
1264
1265 /* For an inequality constraint
1266 *
1267 * f >= 0
1268 *
1269 * or an equality constraint
1270 *
1271 * f = 0
1272 *
1273 * return the affine expression f.
1274 */
1275 __isl_give isl_aff *isl_constraint_get_aff(
1276 __isl_keep isl_constraint *constraint)
1277 {
1278 isl_aff *aff;
1279
1280 if (!constraint)
1281 return NULL;
1282
1283 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));
1284 if (!aff)
1285 return NULL;
1286
1287 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1288 isl_int_set_si(aff->v->el[0], 1);
1289
1290 return aff;
1291 }
1292
1293 /* Construct an inequality (eq = 0) or equality (eq = 1) constraint from "aff".
1294 * In particular, construct aff >= 0 or aff = 0.
1295 *
1296 * The denominator of "aff" can be ignored.
1297 */
1298 static __isl_give isl_constraint *isl_constraint_alloc_aff(int eq,
1299 __isl_take isl_aff *aff)
1300 {
1301 isl_local_space *ls;
1302 isl_vec *v;
1303
1304 if (!aff)
1305 return NULL;
1306 ls = isl_aff_get_domain_local_space(aff);
1307 v = isl_vec_drop_els(isl_vec_copy(aff->v), 0, 1);
1308 isl_aff_free(aff);
1309
1310 return isl_constraint_alloc_vec(eq, ls, v);
1311 }
1312
1313 /* Construct an equality constraint equating the given affine expression
1314 * to zero.
1315 */
1316 __isl_give isl_constraint *isl_equality_from_aff(__isl_take isl_aff *aff)
1317 {
1318 return isl_constraint_alloc_aff(1, aff);
1319 }
1320
1321 /* Construct an inequality constraint enforcing the given affine expression
1322 * to be non-negative.
1323 */
1324 __isl_give isl_constraint *isl_inequality_from_aff(__isl_take isl_aff *aff)
1325 {
1326 return isl_constraint_alloc_aff(0, aff);
1327 }
1328
1329 /* Compare two isl_constraints.
1330 *
1331 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1332 * than "c2" and 0 if they are equal.
1333 *
1334 * The order is fairly arbitrary. We do consider constraints that only involve
1335 * earlier dimensions as "smaller".
1336 */
1337 int isl_constraint_plain_cmp(__isl_keep isl_constraint *c1,
1338 __isl_keep isl_constraint *c2)
1339 {
1340 int cmp;
1341 int last1, last2;
1342
1343 if (c1 == c2)
1344 return 0;
1345 if (!c1)
1346 return -1;
1347 if (!c2)
1348 return 1;
1349 cmp = isl_local_space_cmp(c1->ls, c2->ls);
1350 if (cmp != 0)
1351 return cmp;
1352
1353 last1 = isl_seq_last_non_zero(c1->v->el + 1, c1->v->size - 1);
1354 last2 = isl_seq_last_non_zero(c2->v->el + 1, c1->v->size - 1);
1355 if (last1 != last2)
1356 return last1 - last2;
1357
1358 return isl_seq_cmp(c1->v->el, c2->v->el, c1->v->size);
1359 }
1360
1361 /* Compare two constraints based on their final (non-zero) coefficients.
1362 * In particular, the constraint that involves later variables or
1363 * that has a larger coefficient for a shared latest variable
1364 * is considered "greater" than the other constraint.
1365 *
1366 * Return -1 if "c1" is "smaller" than "c2", 1 if "c1" is "greater"
1367 * than "c2" and 0 if they are equal.
1368 *
1369 * If the constraints live in different local spaces, then we cannot
1370 * really compare the constraints so we compare the local spaces instead.
1371 */
1372 int isl_constraint_cmp_last_non_zero(__isl_keep isl_constraint *c1,
1373 __isl_keep isl_constraint *c2)
1374 {
1375 int cmp;
1376 int last1, last2;
1377
1378 if (c1 == c2)
1379 return 0;
1380 if (!c1)
1381 return -1;
1382 if (!c2)
1383 return 1;
1384 cmp = isl_local_space_cmp(c1->ls, c2->ls);
1385 if (cmp != 0)
1386 return cmp;
1387
1388 last1 = isl_seq_last_non_zero(c1->v->el + 1, c1->v->size - 1);
1389 last2 = isl_seq_last_non_zero(c2->v->el + 1, c1->v->size - 1);
1390 if (last1 != last2)
1391 return last1 - last2;
1392 if (last1 == -1)
1393 return 0;
1394 return isl_int_abs_cmp(c1->v->el[1 + last1], c2->v->el[1 + last2]);
1395 }
Integer set library