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