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

source code of polly/lib/External/isl/isl_constraint.c