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