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