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