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