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