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