?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
isl_basic_map_involves_dims: double-check divs
[isl.git] / isl_constraint.c
blob923cf59228ddbcf3612855f60065966204325329
1 /*
2 * Copyright 2008-2009 Katholieke Universiteit Leuven
3 * Copyright 2010 INRIA Saclay
4 *
5 * Use of this software is governed by the GNU LGPLv2.1 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
20 isl_ctx *isl_constraint_get_ctx(__isl_keep isl_constraint *c)
21 {
22 return c ? isl_local_space_get_ctx(c->ls) : NULL;
23 }
24
25 static unsigned n(struct isl_constraint *c, enum isl_dim_type type)
26 {
27 return isl_local_space_dim(c->ls, type);
28 }
29
30 static unsigned offset(struct isl_constraint *c, enum isl_dim_type type)
31 {
32 return isl_local_space_offset(c->ls, type);
33 }
34
35 static unsigned basic_map_offset(__isl_keep isl_basic_map *bmap,
36 enum isl_dim_type type)
37 {
38 return type == isl_dim_div ? 1 + isl_space_dim(bmap->dim, isl_dim_all)
39 : 1 + isl_space_offset(bmap->dim, type);
40 }
41
42 static unsigned basic_set_offset(struct isl_basic_set *bset,
43 enum isl_dim_type type)
44 {
45 isl_space *dim = bset->dim;
46 switch (type) {
47 case isl_dim_param: return 1;
48 case isl_dim_in: return 1 + dim->nparam;
49 case isl_dim_out: return 1 + dim->nparam + dim->n_in;
50 case isl_dim_div: return 1 + dim->nparam + dim->n_in + dim->n_out;
51 default: return 0;
52 }
53 }
54
55 __isl_give isl_constraint *isl_constraint_alloc_vec(int eq,
56 __isl_take isl_local_space *ls, __isl_take isl_vec *v)
57 {
58 isl_constraint *constraint;
59
60 if (!ls || !v)
61 goto error;
62
63 constraint = isl_alloc_type(isl_vec_get_ctx(v), isl_constraint);
64 if (!constraint)
65 goto error;
66
67 constraint->ref = 1;
68 constraint->eq = eq;
69 constraint->ls = ls;
70 constraint->v = v;
71
72 return constraint;
73 error:
74 isl_local_space_free(ls);
75 isl_vec_free(v);
76 return NULL;
77 }
78
79 __isl_give isl_constraint *isl_constraint_alloc(int eq,
80 __isl_take isl_local_space *ls)
81 {
82 isl_ctx *ctx;
83 isl_vec *v;
84
85 if (!ls)
86 return NULL;
87
88 ctx = isl_local_space_get_ctx(ls);
89 v = isl_vec_alloc(ctx, 1 + isl_local_space_dim(ls, isl_dim_all));
90 v = isl_vec_clr(v);
91 return isl_constraint_alloc_vec(eq, ls, v);
92 }
93
94 struct isl_constraint *isl_basic_map_constraint(struct isl_basic_map *bmap,
95 isl_int **line)
96 {
97 int eq;
98 isl_ctx *ctx;
99 isl_vec *v;
100 isl_local_space *ls = NULL;
101 isl_constraint *constraint;
102
103 if (!bmap || !line)
104 goto error;
105
106 eq = line >= bmap->eq;
107
108 ctx = isl_basic_map_get_ctx(bmap);
109 ls = isl_basic_map_get_local_space(bmap);
110 v = isl_vec_alloc(ctx, 1 + isl_local_space_dim(ls, isl_dim_all));
111 if (!v)
112 goto error;
113 isl_seq_cpy(v->el, line[0], v->size);
114 constraint = isl_constraint_alloc_vec(eq, ls, v);
115
116 isl_basic_map_free(bmap);
117 return constraint;
118 error:
119 isl_local_space_free(ls);
120 isl_basic_map_free(bmap);
121 return NULL;
122 }
123
124 struct isl_constraint *isl_basic_set_constraint(struct isl_basic_set *bset,
125 isl_int **line)
126 {
127 return isl_basic_map_constraint((struct isl_basic_map *)bset, line);
128 }
129
130 __isl_give isl_constraint *isl_equality_alloc(__isl_take isl_local_space *ls)
131 {
132 return isl_constraint_alloc(1, ls);
133 }
134
135 __isl_give isl_constraint *isl_inequality_alloc(__isl_take isl_local_space *ls)
136 {
137 return isl_constraint_alloc(0, ls);
138 }
139
140 struct isl_constraint *isl_constraint_dup(struct isl_constraint *c)
141 {
142 if (!c)
143 return NULL;
144
145 return isl_constraint_alloc_vec(c->eq, isl_local_space_copy(c->ls),
146 isl_vec_copy(c->v));
147 }
148
149 struct isl_constraint *isl_constraint_cow(struct isl_constraint *c)
150 {
151 if (!c)
152 return NULL;
153
154 if (c->ref == 1)
155 return c;
156 c->ref--;
157 return isl_constraint_dup(c);
158 }
159
160 struct isl_constraint *isl_constraint_copy(struct isl_constraint *constraint)
161 {
162 if (!constraint)
163 return NULL;
164
165 constraint->ref++;
166 return constraint;
167 }
168
169 void *isl_constraint_free(struct isl_constraint *c)
170 {
171 if (!c)
172 return NULL;
173
174 if (--c->ref > 0)
175 return NULL;
176
177 isl_local_space_free(c->ls);
178 isl_vec_free(c->v);
179 free(c);
180
181 return NULL;
182 }
183
184 int isl_basic_map_foreach_constraint(__isl_keep isl_basic_map *bmap,
185 int (*fn)(__isl_take isl_constraint *c, void *user), void *user)
186 {
187 int i;
188 struct isl_constraint *c;
189
190 if (!bmap)
191 return -1;
192
193 isl_assert(bmap->ctx, ISL_F_ISSET(bmap, ISL_BASIC_MAP_FINAL),
194 return -1);
195
196 for (i = 0; i < bmap->n_eq; ++i) {
197 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
198 &bmap->eq[i]);
199 if (!c)
200 return -1;
201 if (fn(c, user) < 0)
202 return -1;
203 }
204
205 for (i = 0; i < bmap->n_ineq; ++i) {
206 c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
207 &bmap->ineq[i]);
208 if (!c)
209 return -1;
210 if (fn(c, user) < 0)
211 return -1;
212 }
213
214 return 0;
215 }
216
217 int isl_basic_set_foreach_constraint(__isl_keep isl_basic_set *bset,
218 int (*fn)(__isl_take isl_constraint *c, void *user), void *user)
219 {
220 return isl_basic_map_foreach_constraint((isl_basic_map *)bset, fn, user);
221 }
222
223 int isl_constraint_is_equal(struct isl_constraint *constraint1,
224 struct isl_constraint *constraint2)
225 {
226 int equal;
227
228 if (!constraint1 || !constraint2)
229 return 0;
230 if (constraint1->eq != constraint2->eq)
231 return 0;
232 equal = isl_local_space_is_equal(constraint1->ls, constraint2->ls);
233 if (equal < 0 || !equal)
234 return equal;
235 return isl_vec_is_equal(constraint1->v, constraint2->v);
236 }
237
238 struct isl_basic_map *isl_basic_map_add_constraint(
239 struct isl_basic_map *bmap, struct isl_constraint *constraint)
240 {
241 isl_ctx *ctx;
242 isl_space *dim;
243 int equal_space;
244
245 if (!bmap || !constraint)
246 goto error;
247
248 ctx = isl_constraint_get_ctx(constraint);
249 dim = isl_constraint_get_space(constraint);
250 equal_space = isl_space_is_equal(bmap->dim, dim);
251 isl_space_free(dim);
252 isl_assert(ctx, equal_space, goto error);
253
254 bmap = isl_basic_map_intersect(bmap,
255 isl_basic_map_from_constraint(constraint));
256 return bmap;
257 error:
258 isl_basic_map_free(bmap);
259 isl_constraint_free(constraint);
260 return NULL;
261 }
262
263 struct isl_basic_set *isl_basic_set_add_constraint(
264 struct isl_basic_set *bset, struct isl_constraint *constraint)
265 {
266 return (struct isl_basic_set *)
267 isl_basic_map_add_constraint((struct isl_basic_map *)bset,
268 constraint);
269 }
270
271 __isl_give isl_map *isl_map_add_constraint(__isl_take isl_map *map,
272 __isl_take isl_constraint *constraint)
273 {
274 isl_basic_map *bmap;
275
276 bmap = isl_basic_map_from_constraint(constraint);
277 map = isl_map_intersect(map, isl_map_from_basic_map(bmap));
278
279 return map;
280 }
281
282 __isl_give isl_set *isl_set_add_constraint(__isl_take isl_set *set,
283 __isl_take isl_constraint *constraint)
284 {
285 return isl_map_add_constraint(set, constraint);
286 }
287
288 __isl_give isl_space *isl_constraint_get_space(
289 __isl_keep isl_constraint *constraint)
290 {
291 return constraint ? isl_local_space_get_space(constraint->ls) : NULL;
292 }
293
294 int isl_constraint_dim(struct isl_constraint *constraint,
295 enum isl_dim_type type)
296 {
297 if (!constraint)
298 return -1;
299 return n(constraint, type);
300 }
301
302 int isl_constraint_involves_dims(__isl_keep isl_constraint *constraint,
303 enum isl_dim_type type, unsigned first, unsigned n)
304 {
305 int i;
306 isl_ctx *ctx;
307 int *active = NULL;
308 int involves = 0;
309
310 if (!constraint)
311 return -1;
312 if (n == 0)
313 return 0;
314
315 ctx = isl_constraint_get_ctx(constraint);
316 if (first + n > isl_constraint_dim(constraint, type))
317 isl_die(ctx, isl_error_invalid,
318 "range out of bounds", return -1);
319
320 active = isl_local_space_get_active(constraint->ls,
321 constraint->v->el + 1);
322 if (!active)
323 goto error;
324
325 first += isl_local_space_offset(constraint->ls, type) - 1;
326 for (i = 0; i < n; ++i)
327 if (active[first + i]) {
328 involves = 1;
329 break;
330 }
331
332 free(active);
333
334 return involves;
335 error:
336 free(active);
337 return -1;
338 }
339
340 const char *isl_constraint_get_dim_name(__isl_keep isl_constraint *constraint,
341 enum isl_dim_type type, unsigned pos)
342 {
343 return constraint ?
344 isl_local_space_get_dim_name(constraint->ls, type, pos) : NULL;
345 }
346
347 void isl_constraint_get_constant(struct isl_constraint *constraint, isl_int *v)
348 {
349 if (!constraint)
350 return;
351 isl_int_set(*v, constraint->v->el[0]);
352 }
353
354 void isl_constraint_get_coefficient(struct isl_constraint *constraint,
355 enum isl_dim_type type, int pos, isl_int *v)
356 {
357 if (!constraint)
358 return;
359
360 if (pos >= isl_local_space_dim(constraint->ls, type))
361 isl_die(constraint->v->ctx, isl_error_invalid,
362 "position out of bounds", return);
363
364 pos += isl_local_space_offset(constraint->ls, type);
365 isl_int_set(*v, constraint->v->el[pos]);
366 }
367
368 __isl_give isl_aff *isl_constraint_get_div(__isl_keep isl_constraint *constraint,
369 int pos)
370 {
371 if (!constraint)
372 return NULL;
373
374 return isl_local_space_get_div(constraint->ls, pos);
375 }
376
377 __isl_give isl_constraint *isl_constraint_set_constant(
378 __isl_take isl_constraint *constraint, isl_int v)
379 {
380 constraint = isl_constraint_cow(constraint);
381 if (!constraint)
382 return NULL;
383
384 constraint->v = isl_vec_cow(constraint->v);
385 if (!constraint->v)
386 return isl_constraint_free(constraint);
387
388 isl_int_set(constraint->v->el[0], v);
389 return constraint;
390 }
391
392 __isl_give isl_constraint *isl_constraint_set_constant_si(
393 __isl_take isl_constraint *constraint, int v)
394 {
395 constraint = isl_constraint_cow(constraint);
396 if (!constraint)
397 return NULL;
398
399 constraint->v = isl_vec_cow(constraint->v);
400 if (!constraint->v)
401 return isl_constraint_free(constraint);
402
403 isl_int_set_si(constraint->v->el[0], v);
404 return constraint;
405 }
406
407 __isl_give isl_constraint *isl_constraint_set_coefficient(
408 __isl_take isl_constraint *constraint,
409 enum isl_dim_type type, int pos, isl_int v)
410 {
411 constraint = isl_constraint_cow(constraint);
412 if (!constraint)
413 return NULL;
414
415 if (pos >= isl_local_space_dim(constraint->ls, type))
416 isl_die(constraint->v->ctx, isl_error_invalid,
417 "position out of bounds",
418 return isl_constraint_free(constraint));
419
420 constraint = isl_constraint_cow(constraint);
421 if (!constraint)
422 return NULL;
423
424 constraint->v = isl_vec_cow(constraint->v);
425 if (!constraint->v)
426 return isl_constraint_free(constraint);
427
428 pos += isl_local_space_offset(constraint->ls, type);
429 isl_int_set(constraint->v->el[pos], v);
430
431 return constraint;
432 }
433
434 __isl_give isl_constraint *isl_constraint_set_coefficient_si(
435 __isl_take isl_constraint *constraint,
436 enum isl_dim_type type, int pos, int v)
437 {
438 constraint = isl_constraint_cow(constraint);
439 if (!constraint)
440 return NULL;
441
442 if (pos >= isl_local_space_dim(constraint->ls, type))
443 isl_die(constraint->v->ctx, isl_error_invalid,
444 "position out of bounds",
445 return isl_constraint_free(constraint));
446
447 constraint = isl_constraint_cow(constraint);
448 if (!constraint)
449 return NULL;
450
451 constraint->v = isl_vec_cow(constraint->v);
452 if (!constraint->v)
453 return isl_constraint_free(constraint);
454
455 pos += isl_local_space_offset(constraint->ls, type);
456 isl_int_set_si(constraint->v->el[pos], v);
457
458 return constraint;
459 }
460
461 /* Drop any constraint from "bset" that is identical to "constraint".
462 * In particular, this means that the local spaces of "bset" and
463 * "constraint" need to be the same.
464 *
465 * Since the given constraint may actually be a pointer into the bset,
466 * we have to be careful not to reorder the constraints as the user
467 * may be holding on to other constraints from the same bset.
468 * This should be cleaned up when the internal representation of
469 * isl_constraint is changed to use isl_aff.
470 */
471 __isl_give isl_basic_set *isl_basic_set_drop_constraint(
472 __isl_take isl_basic_set *bset, __isl_take isl_constraint *constraint)
473 {
474 int i;
475 unsigned n;
476 isl_int **row;
477 unsigned total;
478 isl_local_space *ls1;
479 int equal;
480
481 if (!bset || !constraint)
482 goto error;
483
484 ls1 = isl_basic_set_get_local_space(bset);
485 equal = isl_local_space_is_equal(ls1, constraint->ls);
486 isl_local_space_free(ls1);
487 if (equal < 0)
488 goto error;
489 if (!equal) {
490 isl_constraint_free(constraint);
491 return bset;
492 }
493
494 if (isl_constraint_is_equality(constraint)) {
495 n = bset->n_eq;
496 row = bset->eq;
497 } else {
498 n = bset->n_ineq;
499 row = bset->ineq;
500 }
501
502 total = isl_constraint_dim(constraint, isl_dim_all);
503 for (i = 0; i < n; ++i)
504 if (isl_seq_eq(row[i], constraint->v->el, 1 + total))
505 isl_seq_clr(row[i], 1 + total);
506
507 isl_constraint_free(constraint);
508 return bset;
509 error:
510 isl_constraint_free(constraint);
511 isl_basic_set_free(bset);
512 return NULL;
513 }
514
515 struct isl_constraint *isl_constraint_negate(struct isl_constraint *constraint)
516 {
517 isl_ctx *ctx;
518
519 constraint = isl_constraint_cow(constraint);
520 if (!constraint)
521 return NULL;
522
523 ctx = isl_constraint_get_ctx(constraint);
524 if (isl_constraint_is_equality(constraint))
525 isl_die(ctx, isl_error_invalid, "cannot negate equality",
526 return isl_constraint_free(constraint));
527 constraint->v = isl_vec_neg(constraint->v);
528 constraint->v = isl_vec_cow(constraint->v);
529 if (!constraint->v)
530 return isl_constraint_free(constraint);
531 isl_int_sub_ui(constraint->v->el[0], constraint->v->el[0], 1);
532 return constraint;
533 }
534
535 int isl_constraint_is_equality(struct isl_constraint *constraint)
536 {
537 if (!constraint)
538 return -1;
539 return constraint->eq;
540 }
541
542 int isl_constraint_is_div_constraint(__isl_keep isl_constraint *constraint)
543 {
544 int i;
545 int n_div;
546
547 if (!constraint)
548 return -1;
549 if (isl_constraint_is_equality(constraint))
550 return 0;
551 n_div = isl_constraint_dim(constraint, isl_dim_div);
552 for (i = 0; i < n_div; ++i) {
553 if (isl_local_space_is_div_constraint(constraint->ls,
554 constraint->v->el, i))
555 return 1;
556 }
557
558 return 0;
559 }
560
561 /* We manually set ISL_BASIC_SET_FINAL instead of calling
562 * isl_basic_map_finalize because we want to keep the position
563 * of the divs and we therefore do not want to throw away redundant divs.
564 * This is arguably a bit fragile.
565 */
566 __isl_give isl_basic_map *isl_basic_map_from_constraint(
567 __isl_take isl_constraint *constraint)
568 {
569 int k;
570 isl_local_space *ls;
571 struct isl_basic_map *bmap;
572 isl_int *c;
573 unsigned total;
574
575 if (!constraint)
576 return NULL;
577
578 ls = isl_local_space_copy(constraint->ls);
579 bmap = isl_basic_map_from_local_space(ls);
580 bmap = isl_basic_map_extend_constraints(bmap, 1, 1);
581 if (isl_constraint_is_equality(constraint)) {
582 k = isl_basic_map_alloc_equality(bmap);
583 if (k < 0)
584 goto error;
585 c = bmap->eq[k];
586 }
587 else {
588 k = isl_basic_map_alloc_inequality(bmap);
589 if (k < 0)
590 goto error;
591 c = bmap->ineq[k];
592 }
593 total = isl_basic_map_total_dim(bmap);
594 isl_seq_cpy(c, constraint->v->el, 1 + total);
595 isl_constraint_free(constraint);
596 if (bmap)
597 ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);
598 return bmap;
599 error:
600 isl_constraint_free(constraint);
601 isl_basic_map_free(bmap);
602 return NULL;
603 }
604
605 struct isl_basic_set *isl_basic_set_from_constraint(
606 struct isl_constraint *constraint)
607 {
608 if (!constraint)
609 return NULL;
610
611 if (isl_constraint_dim(constraint, isl_dim_in) != 0)
612 isl_die(isl_constraint_get_ctx(constraint), isl_error_invalid,
613 "not a set constraint",
614 return isl_constraint_free(constraint));
615 return (isl_basic_set *)isl_basic_map_from_constraint(constraint);
616 }
617
618 int isl_basic_map_has_defining_equality(
619 __isl_keep isl_basic_map *bmap, enum isl_dim_type type, int pos,
620 __isl_give isl_constraint **c)
621 {
622 int i;
623 unsigned offset;
624 unsigned total;
625
626 if (!bmap)
627 return -1;
628 offset = basic_map_offset(bmap, type);
629 total = isl_basic_map_total_dim(bmap);
630 isl_assert(bmap->ctx, pos < isl_basic_map_dim(bmap, type), return -1);
631 for (i = 0; i < bmap->n_eq; ++i)
632 if (!isl_int_is_zero(bmap->eq[i][offset + pos]) &&
633 isl_seq_first_non_zero(bmap->eq[i]+offset+pos+1,
634 1+total-offset-pos-1) == -1) {
635 *c = isl_basic_map_constraint(isl_basic_map_copy(bmap),
636 &bmap->eq[i]);
637 return 1;
638 }
639 return 0;
640 }
641
642 int isl_basic_set_has_defining_equality(
643 __isl_keep isl_basic_set *bset, enum isl_dim_type type, int pos,
644 __isl_give isl_constraint **c)
645 {
646 return isl_basic_map_has_defining_equality((isl_basic_map *)bset,
647 type, pos, c);
648 }
649
650 int isl_basic_set_has_defining_inequalities(
651 struct isl_basic_set *bset, enum isl_dim_type type, int pos,
652 struct isl_constraint **lower,
653 struct isl_constraint **upper)
654 {
655 int i, j;
656 unsigned offset;
657 unsigned total;
658 isl_int m;
659 isl_int **lower_line, **upper_line;
660
661 if (!bset)
662 return -1;
663 offset = basic_set_offset(bset, type);
664 total = isl_basic_set_total_dim(bset);
665 isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type), return -1);
666 isl_int_init(m);
667 for (i = 0; i < bset->n_ineq; ++i) {
668 if (isl_int_is_zero(bset->ineq[i][offset + pos]))
669 continue;
670 if (isl_int_is_one(bset->ineq[i][offset + pos]))
671 continue;
672 if (isl_int_is_negone(bset->ineq[i][offset + pos]))
673 continue;
674 if (isl_seq_first_non_zero(bset->ineq[i]+offset+pos+1,
675 1+total-offset-pos-1) != -1)
676 continue;
677 for (j = i + 1; j < bset->n_ineq; ++j) {
678 if (!isl_seq_is_neg(bset->ineq[i]+1, bset->ineq[j]+1,
679 total))
680 continue;
681 isl_int_add(m, bset->ineq[i][0], bset->ineq[j][0]);
682 if (isl_int_abs_ge(m, bset->ineq[i][offset+pos]))
683 continue;
684
685 if (isl_int_is_pos(bset->ineq[i][offset+pos])) {
686 lower_line = &bset->ineq[i];
687 upper_line = &bset->ineq[j];
688 } else {
689 lower_line = &bset->ineq[j];
690 upper_line = &bset->ineq[i];
691 }
692 *lower = isl_basic_set_constraint(
693 isl_basic_set_copy(bset), lower_line);
694 *upper = isl_basic_set_constraint(
695 isl_basic_set_copy(bset), upper_line);
696 isl_int_clear(m);
697 return 1;
698 }
699 }
700 *lower = NULL;
701 *upper = NULL;
702 isl_int_clear(m);
703 return 0;
704 }
705
706 /* Given two constraints "a" and "b" on the variable at position "abs_pos"
707 * (in "a" and "b"), add a constraint to "bset" that ensures that the
708 * bound implied by "a" is (strictly) larger than the bound implied by "b".
709 *
710 * If both constraints imply lower bounds, then this means that "a" is
711 * active in the result.
712 * If both constraints imply upper bounds, then this means that "b" is
713 * active in the result.
714 */
715 static __isl_give isl_basic_set *add_larger_bound_constraint(
716 __isl_take isl_basic_set *bset, isl_int *a, isl_int *b,
717 unsigned abs_pos, int strict)
718 {
719 int k;
720 isl_int t;
721 unsigned total;
722
723 k = isl_basic_set_alloc_inequality(bset);
724 if (k < 0)
725 goto error;
726
727 total = isl_basic_set_dim(bset, isl_dim_all);
728
729 isl_int_init(t);
730 isl_int_neg(t, b[1 + abs_pos]);
731
732 isl_seq_combine(bset->ineq[k], t, a, a[1 + abs_pos], b, 1 + abs_pos);
733 isl_seq_combine(bset->ineq[k] + 1 + abs_pos,
734 t, a + 1 + abs_pos + 1, a[1 + abs_pos], b + 1 + abs_pos + 1,
735 total - abs_pos);
736
737 if (strict)
738 isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
739
740 isl_int_clear(t);
741
742 return bset;
743 error:
744 isl_basic_set_free(bset);
745 return NULL;
746 }
747
748 /* Add constraints to "context" that ensure that "u" is the smallest
749 * (and therefore active) upper bound on "abs_pos" in "bset" and return
750 * the resulting basic set.
751 */
752 static __isl_give isl_basic_set *set_smallest_upper_bound(
753 __isl_keep isl_basic_set *context,
754 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_upper, int u)
755 {
756 int j;
757
758 context = isl_basic_set_copy(context);
759 context = isl_basic_set_cow(context);
760
761 context = isl_basic_set_extend_constraints(context, 0, n_upper - 1);
762
763 for (j = 0; j < bset->n_ineq; ++j) {
764 if (j == u)
765 continue;
766 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
767 continue;
768 context = add_larger_bound_constraint(context,
769 bset->ineq[j], bset->ineq[u], abs_pos, j > u);
770 }
771
772 context = isl_basic_set_simplify(context);
773 context = isl_basic_set_finalize(context);
774
775 return context;
776 }
777
778 /* Add constraints to "context" that ensure that "u" is the largest
779 * (and therefore active) upper bound on "abs_pos" in "bset" and return
780 * the resulting basic set.
781 */
782 static __isl_give isl_basic_set *set_largest_lower_bound(
783 __isl_keep isl_basic_set *context,
784 __isl_keep isl_basic_set *bset, unsigned abs_pos, int n_lower, int l)
785 {
786 int j;
787
788 context = isl_basic_set_copy(context);
789 context = isl_basic_set_cow(context);
790
791 context = isl_basic_set_extend_constraints(context, 0, n_lower - 1);
792
793 for (j = 0; j < bset->n_ineq; ++j) {
794 if (j == l)
795 continue;
796 if (!isl_int_is_pos(bset->ineq[j][1 + abs_pos]))
797 continue;
798 context = add_larger_bound_constraint(context,
799 bset->ineq[l], bset->ineq[j], abs_pos, j > l);
800 }
801
802 context = isl_basic_set_simplify(context);
803 context = isl_basic_set_finalize(context);
804
805 return context;
806 }
807
808 static int foreach_upper_bound(__isl_keep isl_basic_set *bset,
809 enum isl_dim_type type, unsigned abs_pos,
810 __isl_take isl_basic_set *context, int n_upper,
811 int (*fn)(__isl_take isl_constraint *lower,
812 __isl_take isl_constraint *upper,
813 __isl_take isl_basic_set *bset, void *user), void *user)
814 {
815 isl_basic_set *context_i;
816 isl_constraint *upper = NULL;
817 int i;
818
819 for (i = 0; i < bset->n_ineq; ++i) {
820 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
821 continue;
822
823 context_i = set_smallest_upper_bound(context, bset,
824 abs_pos, n_upper, i);
825 if (isl_basic_set_is_empty(context_i)) {
826 isl_basic_set_free(context_i);
827 continue;
828 }
829 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
830 &bset->ineq[i]);
831 if (!upper || !context_i)
832 goto error;
833 if (fn(NULL, upper, context_i, user) < 0)
834 break;
835 }
836
837 isl_basic_set_free(context);
838
839 if (i < bset->n_ineq)
840 return -1;
841
842 return 0;
843 error:
844 isl_constraint_free(upper);
845 isl_basic_set_free(context_i);
846 isl_basic_set_free(context);
847 return -1;
848 }
849
850 static int foreach_lower_bound(__isl_keep isl_basic_set *bset,
851 enum isl_dim_type type, unsigned abs_pos,
852 __isl_take isl_basic_set *context, int n_lower,
853 int (*fn)(__isl_take isl_constraint *lower,
854 __isl_take isl_constraint *upper,
855 __isl_take isl_basic_set *bset, void *user), void *user)
856 {
857 isl_basic_set *context_i;
858 isl_constraint *lower = NULL;
859 int i;
860
861 for (i = 0; i < bset->n_ineq; ++i) {
862 if (isl_int_is_zero(bset->ineq[i][1 + abs_pos]))
863 continue;
864
865 context_i = set_largest_lower_bound(context, bset,
866 abs_pos, n_lower, i);
867 if (isl_basic_set_is_empty(context_i)) {
868 isl_basic_set_free(context_i);
869 continue;
870 }
871 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
872 &bset->ineq[i]);
873 if (!lower || !context_i)
874 goto error;
875 if (fn(lower, NULL, context_i, user) < 0)
876 break;
877 }
878
879 isl_basic_set_free(context);
880
881 if (i < bset->n_ineq)
882 return -1;
883
884 return 0;
885 error:
886 isl_constraint_free(lower);
887 isl_basic_set_free(context_i);
888 isl_basic_set_free(context);
889 return -1;
890 }
891
892 static int foreach_bound_pair(__isl_keep isl_basic_set *bset,
893 enum isl_dim_type type, unsigned abs_pos,
894 __isl_take isl_basic_set *context, int n_lower, int n_upper,
895 int (*fn)(__isl_take isl_constraint *lower,
896 __isl_take isl_constraint *upper,
897 __isl_take isl_basic_set *bset, void *user), void *user)
898 {
899 isl_basic_set *context_i, *context_j;
900 isl_constraint *lower = NULL;
901 isl_constraint *upper = NULL;
902 int i, j;
903
904 for (i = 0; i < bset->n_ineq; ++i) {
905 if (!isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
906 continue;
907
908 context_i = set_largest_lower_bound(context, bset,
909 abs_pos, n_lower, i);
910 if (isl_basic_set_is_empty(context_i)) {
911 isl_basic_set_free(context_i);
912 continue;
913 }
914
915 for (j = 0; j < bset->n_ineq; ++j) {
916 if (!isl_int_is_neg(bset->ineq[j][1 + abs_pos]))
917 continue;
918
919 context_j = set_smallest_upper_bound(context_i, bset,
920 abs_pos, n_upper, j);
921 context_j = isl_basic_set_extend_constraints(context_j,
922 0, 1);
923 context_j = add_larger_bound_constraint(context_j,
924 bset->ineq[i], bset->ineq[j], abs_pos, 0);
925 context_j = isl_basic_set_simplify(context_j);
926 context_j = isl_basic_set_finalize(context_j);
927 if (isl_basic_set_is_empty(context_j)) {
928 isl_basic_set_free(context_j);
929 continue;
930 }
931 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
932 &bset->ineq[i]);
933 upper = isl_basic_set_constraint(isl_basic_set_copy(bset),
934 &bset->ineq[j]);
935 if (!lower || !upper || !context_j)
936 goto error;
937 if (fn(lower, upper, context_j, user) < 0)
938 break;
939 }
940
941 isl_basic_set_free(context_i);
942
943 if (j < bset->n_ineq)
944 break;
945 }
946
947 isl_basic_set_free(context);
948
949 if (i < bset->n_ineq)
950 return -1;
951
952 return 0;
953 error:
954 isl_constraint_free(lower);
955 isl_constraint_free(upper);
956 isl_basic_set_free(context_i);
957 isl_basic_set_free(context_j);
958 isl_basic_set_free(context);
959 return -1;
960 }
961
962 /* For each pair of lower and upper bounds on the variable "pos"
963 * of type "type", call "fn" with these lower and upper bounds and the
964 * set of constraints on the remaining variables where these bounds
965 * are active, i.e., (stricly) larger/smaller than the other lower/upper bounds.
966 *
967 * If the designated variable is equal to an affine combination of the
968 * other variables then fn is called with both lower and upper
969 * set to the corresponding equality.
970 *
971 * If there is no lower (or upper) bound, then NULL is passed
972 * as the corresponding bound.
973 *
974 * We first check if the variable is involved in any equality.
975 * If not, we count the number of lower and upper bounds and
976 * act accordingly.
977 */
978 int isl_basic_set_foreach_bound_pair(__isl_keep isl_basic_set *bset,
979 enum isl_dim_type type, unsigned pos,
980 int (*fn)(__isl_take isl_constraint *lower,
981 __isl_take isl_constraint *upper,
982 __isl_take isl_basic_set *bset, void *user), void *user)
983 {
984 int i;
985 isl_constraint *lower = NULL;
986 isl_constraint *upper = NULL;
987 isl_basic_set *context = NULL;
988 unsigned abs_pos;
989 int n_lower, n_upper;
990
991 if (!bset)
992 return -1;
993 isl_assert(bset->ctx, pos < isl_basic_set_dim(bset, type), return -1);
994 isl_assert(bset->ctx, type == isl_dim_param || type == isl_dim_set,
995 return -1);
996
997 abs_pos = pos;
998 if (type == isl_dim_set)
999 abs_pos += isl_basic_set_dim(bset, isl_dim_param);
1000
1001 for (i = 0; i < bset->n_eq; ++i) {
1002 if (isl_int_is_zero(bset->eq[i][1 + abs_pos]))
1003 continue;
1004
1005 lower = isl_basic_set_constraint(isl_basic_set_copy(bset),
1006 &bset->eq[i]);
1007 upper = isl_constraint_copy(lower);
1008 context = isl_basic_set_remove_dims(isl_basic_set_copy(bset),
1009 type, pos, 1);
1010 if (!lower || !upper || !context)
1011 goto error;
1012 return fn(lower, upper, context, user);
1013 }
1014
1015 n_lower = 0;
1016 n_upper = 0;
1017 for (i = 0; i < bset->n_ineq; ++i) {
1018 if (isl_int_is_pos(bset->ineq[i][1 + abs_pos]))
1019 n_lower++;
1020 else if (isl_int_is_neg(bset->ineq[i][1 + abs_pos]))
1021 n_upper++;
1022 }
1023
1024 context = isl_basic_set_copy(bset);
1025 context = isl_basic_set_cow(context);
1026 if (!context)
1027 goto error;
1028 for (i = context->n_ineq - 1; i >= 0; --i)
1029 if (!isl_int_is_zero(context->ineq[i][1 + abs_pos]))
1030 isl_basic_set_drop_inequality(context, i);
1031
1032 context = isl_basic_set_drop(context, type, pos, 1);
1033 if (!n_lower && !n_upper)
1034 return fn(NULL, NULL, context, user);
1035 if (!n_lower)
1036 return foreach_upper_bound(bset, type, abs_pos, context, n_upper,
1037 fn, user);
1038 if (!n_upper)
1039 return foreach_lower_bound(bset, type, abs_pos, context, n_lower,
1040 fn, user);
1041 return foreach_bound_pair(bset, type, abs_pos, context, n_lower, n_upper,
1042 fn, user);
1043 error:
1044 isl_constraint_free(lower);
1045 isl_constraint_free(upper);
1046 isl_basic_set_free(context);
1047 return -1;
1048 }
1049
1050 __isl_give isl_aff *isl_constraint_get_bound(
1051 __isl_keep isl_constraint *constraint, enum isl_dim_type type, int pos)
1052 {
1053 isl_aff *aff;
1054 isl_ctx *ctx;
1055
1056 if (!constraint)
1057 return NULL;
1058 ctx = isl_constraint_get_ctx(constraint);
1059 if (pos >= isl_constraint_dim(constraint, type))
1060 isl_die(ctx, isl_error_invalid,
1061 "index out of bounds", return NULL);
1062 if (isl_constraint_dim(constraint, isl_dim_in) != 0)
1063 isl_die(ctx, isl_error_invalid,
1064 "not a set constraint", return NULL);
1065
1066 pos += offset(constraint, type);
1067 if (isl_int_is_zero(constraint->v->el[pos]))
1068 isl_die(ctx, isl_error_invalid,
1069 "constraint does not define a bound on given dimension",
1070 return NULL);
1071
1072 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));
1073 if (!aff)
1074 return NULL;
1075
1076 if (isl_int_is_neg(constraint->v->el[pos]))
1077 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1078 else
1079 isl_seq_neg(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1080 isl_int_set_si(aff->v->el[1 + pos], 0);
1081 isl_int_abs(aff->v->el[0], constraint->v->el[pos]);
1082
1083 return aff;
1084 }
1085
1086 /* For an inequality constraint
1087 *
1088 * f >= 0
1089 *
1090 * or an equality constraint
1091 *
1092 * f = 0
1093 *
1094 * return the affine expression f.
1095 */
1096 __isl_give isl_aff *isl_constraint_get_aff(
1097 __isl_keep isl_constraint *constraint)
1098 {
1099 isl_aff *aff;
1100
1101 if (!constraint)
1102 return NULL;
1103
1104 aff = isl_aff_alloc(isl_local_space_copy(constraint->ls));
1105 if (!aff)
1106 return NULL;
1107
1108 isl_seq_cpy(aff->v->el + 1, constraint->v->el, aff->v->size - 1);
1109 isl_int_set_si(aff->v->el[0], 1);
1110
1111 return aff;
1112 }
1113
1114 /* Construct an equality constraint equating the given affine expression
1115 * to zero.
1116 */
1117 __isl_give isl_constraint *isl_equality_from_aff(__isl_take isl_aff *aff)
1118 {
1119 int k;
1120 isl_local_space *ls;
1121 isl_basic_set *bset;
1122
1123 if (!aff)
1124 return NULL;
1125
1126 ls = isl_aff_get_domain_local_space(aff);
1127 bset = isl_basic_set_from_local_space(ls);
1128 bset = isl_basic_set_extend_constraints(bset, 1, 0);
1129 k = isl_basic_set_alloc_equality(bset);
1130 if (k < 0)
1131 goto error;
1132
1133 isl_seq_cpy(bset->eq[k], aff->v->el + 1, aff->v->size - 1);
1134 isl_aff_free(aff);
1135
1136 return isl_basic_set_constraint(bset, &bset->eq[k]);
1137 error:
1138 isl_aff_free(aff);
1139 isl_basic_set_free(bset);
1140 return NULL;
1141 }
1142
1143 /* Construct an inequality constraint enforcing the given affine expression
1144 * to be non-negative.
1145 */
1146 __isl_give isl_constraint *isl_inequality_from_aff(__isl_take isl_aff *aff)
1147 {
1148 int k;
1149 isl_local_space *ls;
1150 isl_basic_set *bset;
1151
1152 if (!aff)
1153 return NULL;
1154
1155 ls = isl_aff_get_domain_local_space(aff);
1156 bset = isl_basic_set_from_local_space(ls);
1157 bset = isl_basic_set_extend_constraints(bset, 0, 1);
1158 k = isl_basic_set_alloc_inequality(bset);
1159 if (k < 0)
1160 goto error;
1161
1162 isl_seq_cpy(bset->ineq[k], aff->v->el + 1, aff->v->size - 1);
1163 isl_aff_free(aff);
1164
1165 return isl_basic_set_constraint(bset, &bset->ineq[k]);
1166 error:
1167 isl_aff_free(aff);
1168 isl_basic_set_free(bset);
1169 return NULL;
1170 }
Integer set library