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