2 * Copyright 2008-2009 Katholieke Universiteit Leuven
3 * Copyright 2010 INRIA Saclay
5 * Use of this software is governed by the GNU LGPLv2.1 license
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
16 #include <isl_ctx_private.h>
17 #include <isl_map_private.h>
21 #include <isl/stream.h>
23 #include "isl_polynomial_private.h"
24 #include <isl/union_map.h>
25 #include <isl_mat_private.h>
31 /* non-zero if variable represents a min (-1) or a max (1) */
34 struct variable
*next
;
43 static struct vars
*vars_new(struct isl_ctx
*ctx
)
46 v
= isl_alloc_type(ctx
, struct vars
);
55 static void variable_free(struct variable
*var
)
58 struct variable
*next
= var
->next
;
59 isl_mat_free(var
->list
);
60 isl_vec_free(var
->def
);
67 static void vars_free(struct vars
*v
)
75 static void vars_drop(struct vars
*v
, int n
)
86 struct variable
*next
= var
->next
;
87 isl_mat_free(var
->list
);
88 isl_vec_free(var
->def
);
96 static struct variable
*variable_new(struct vars
*v
, const char *name
, int len
,
100 var
= isl_calloc_type(v
->ctx
, struct variable
);
103 var
->name
= strdup(name
);
104 var
->name
[len
] = '\0';
114 static int vars_pos(struct vars
*v
, const char *s
, int len
)
121 for (q
= v
->v
; q
; q
= q
->next
) {
122 if (strncmp(q
->name
, s
, len
) == 0 && q
->name
[len
] == '\0')
129 v
->v
= variable_new(v
, s
, len
, v
->n
);
137 static int vars_add_anon(struct vars
*v
)
139 v
->v
= variable_new(v
, "", 0, v
->n
);
148 static __isl_give isl_basic_map
*set_name(__isl_take isl_basic_map
*bmap
,
149 enum isl_dim_type type
, unsigned pos
, char *name
)
158 prime
= strchr(name
, '\'');
161 bmap
= isl_basic_map_set_dim_name(bmap
, type
, pos
, name
);
168 /* Obtain next token, with some preprocessing.
169 * In particular, evaluate expressions of the form x^y,
170 * with x and y values.
172 static struct isl_token
*next_token(struct isl_stream
*s
)
174 struct isl_token
*tok
, *tok2
;
176 tok
= isl_stream_next_token(s
);
177 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
)
179 if (!isl_stream_eat_if_available(s
, '^'))
181 tok2
= isl_stream_next_token(s
);
182 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
183 isl_stream_error(s
, tok2
, "expecting constant value");
187 isl_int_pow_ui(tok
->u
.v
, tok
->u
.v
, isl_int_get_ui(tok2
->u
.v
));
189 isl_token_free(tok2
);
193 isl_token_free(tok2
);
197 static int accept_cst_factor(struct isl_stream
*s
, isl_int
*f
)
199 struct isl_token
*tok
;
202 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
203 isl_stream_error(s
, tok
, "expecting constant value");
207 isl_int_mul(*f
, *f
, tok
->u
.v
);
211 if (isl_stream_eat_if_available(s
, '*'))
212 return accept_cst_factor(s
, f
);
220 /* Given an affine expression aff, return an affine expression
221 * for aff % d, with d the next token on the stream, which is
222 * assumed to be a constant.
224 * We introduce an integer division q = [aff/d] and the result
225 * is set to aff - d q.
227 static __isl_give isl_vec
*affine_mod(struct isl_stream
*s
,
228 struct vars
*v
, __isl_take isl_vec
*aff
)
230 struct isl_token
*tok
;
231 struct variable
*var
;
235 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
236 isl_stream_error(s
, tok
, "expecting constant value");
240 if (vars_add_anon(v
) < 0)
245 var
->def
= isl_vec_alloc(s
->ctx
, 2 + v
->n
);
248 isl_seq_cpy(var
->def
->el
+ 1, aff
->el
, aff
->size
);
249 isl_int_set_si(var
->def
->el
[1 + aff
->size
], 0);
250 isl_int_set(var
->def
->el
[0], tok
->u
.v
);
252 mod
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
256 isl_seq_cpy(mod
->el
, aff
->el
, aff
->size
);
257 isl_int_neg(mod
->el
[aff
->size
], tok
->u
.v
);
268 static struct isl_vec
*accept_affine(struct isl_stream
*s
, struct vars
*v
);
269 static int read_div_definition(struct isl_stream
*s
, struct vars
*v
);
270 static int read_minmax_definition(struct isl_stream
*s
, struct vars
*v
);
272 static __isl_give isl_vec
*accept_affine_factor(struct isl_stream
*s
,
275 struct isl_token
*tok
= NULL
;
280 isl_stream_error(s
, NULL
, "unexpected EOF");
283 if (tok
->type
== ISL_TOKEN_IDENT
) {
285 int pos
= vars_pos(v
, tok
->u
.s
, -1);
289 isl_stream_error(s
, tok
, "unknown identifier");
293 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
296 isl_seq_clr(aff
->el
, aff
->size
);
297 isl_int_set_si(aff
->el
[1 + pos
], 1);
299 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
300 if (isl_stream_eat_if_available(s
, '*')) {
301 aff
= accept_affine_factor(s
, v
);
302 aff
= isl_vec_scale(aff
, tok
->u
.v
);
304 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
307 isl_seq_clr(aff
->el
, aff
->size
);
308 isl_int_set(aff
->el
[0], tok
->u
.v
);
311 } else if (tok
->type
== '(') {
314 aff
= accept_affine(s
, v
);
317 if (isl_stream_eat(s
, ')'))
319 } else if (tok
->type
== '[' ||
320 tok
->type
== ISL_TOKEN_FLOORD
||
321 tok
->type
== ISL_TOKEN_CEILD
) {
322 int ceil
= tok
->type
== ISL_TOKEN_CEILD
;
323 struct variable
*var
;
324 if (vars_add_anon(v
) < 0)
327 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
330 isl_seq_clr(aff
->el
, aff
->size
);
331 isl_int_set_si(aff
->el
[1 + v
->n
- 1], ceil
? -1 : 1);
332 isl_stream_push_token(s
, tok
);
334 if (read_div_definition(s
, v
) < 0)
337 isl_seq_neg(var
->def
->el
+ 1, var
->def
->el
+ 1,
339 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
340 } else if (tok
->type
== ISL_TOKEN_MIN
|| tok
->type
== ISL_TOKEN_MAX
) {
341 if (vars_add_anon(v
) < 0)
343 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
346 isl_seq_clr(aff
->el
, aff
->size
);
347 isl_int_set_si(aff
->el
[1 + v
->n
- 1], 1);
348 isl_stream_push_token(s
, tok
);
350 if (read_minmax_definition(s
, v
) < 0)
352 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
354 isl_stream_error(s
, tok
, "expecting factor");
357 if (isl_stream_eat_if_available(s
, '%'))
358 return affine_mod(s
, v
, aff
);
359 if (isl_stream_eat_if_available(s
, '*')) {
362 isl_int_set_si(f
, 1);
363 if (accept_cst_factor(s
, &f
) < 0) {
367 aff
= isl_vec_scale(aff
, f
);
379 static struct isl_vec
*accept_affine(struct isl_stream
*s
, struct vars
*v
)
381 struct isl_token
*tok
= NULL
;
385 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
388 isl_seq_clr(aff
->el
, aff
->size
);
393 isl_stream_error(s
, NULL
, "unexpected EOF");
396 if (tok
->type
== '-') {
401 if (tok
->type
== '(' || tok
->type
== '[' ||
402 tok
->type
== ISL_TOKEN_MIN
|| tok
->type
== ISL_TOKEN_MAX
||
403 tok
->type
== ISL_TOKEN_FLOORD
||
404 tok
->type
== ISL_TOKEN_CEILD
||
405 tok
->type
== ISL_TOKEN_IDENT
) {
407 isl_stream_push_token(s
, tok
);
409 aff2
= accept_affine_factor(s
, v
);
411 aff2
= isl_vec_scale(aff2
, s
->ctx
->negone
);
412 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
413 aff
= isl_vec_add(aff
, aff2
);
417 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
419 isl_int_neg(tok
->u
.v
, tok
->u
.v
);
420 if (isl_stream_eat_if_available(s
, '*') ||
421 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
423 aff2
= accept_affine_factor(s
, v
);
424 aff2
= isl_vec_scale(aff2
, tok
->u
.v
);
425 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
426 aff
= isl_vec_add(aff
, aff2
);
430 isl_int_add(aff
->el
[0], aff
->el
[0], tok
->u
.v
);
434 isl_stream_error(s
, tok
, "unexpected isl_token");
435 isl_stream_push_token(s
, tok
);
442 if (tok
&& tok
->type
== '-') {
445 } else if (tok
&& tok
->type
== '+') {
448 } else if (tok
&& tok
->type
== ISL_TOKEN_VALUE
&&
449 isl_int_is_neg(tok
->u
.v
)) {
450 isl_stream_push_token(s
, tok
);
453 isl_stream_push_token(s
, tok
);
465 /* Add any variables in the variable list "v" that are not already in "bmap"
466 * as existentially quantified variables in "bmap".
468 static __isl_give isl_basic_map
*add_divs(__isl_take isl_basic_map
*bmap
,
473 struct variable
*var
;
475 extra
= v
->n
- isl_basic_map_total_dim(bmap
);
480 bmap
= isl_basic_map_extend_dim(bmap
, isl_basic_map_get_dim(bmap
),
481 extra
, 0, 2 * extra
);
483 for (i
= 0; i
< extra
; ++i
)
484 if (isl_basic_map_alloc_div(bmap
) < 0)
487 for (i
= 0, var
= v
->v
; i
< extra
; ++i
, var
= var
->next
) {
488 int k
= bmap
->n_div
- 1 - i
;
490 isl_seq_cpy(bmap
->div
[k
], var
->def
->el
, var
->def
->size
);
491 isl_seq_clr(bmap
->div
[k
] + var
->def
->size
,
492 2 + v
->n
- var
->def
->size
);
494 if (isl_basic_map_add_div_constraints(bmap
, k
) < 0)
500 isl_basic_map_free(bmap
);
504 static __isl_give isl_basic_map
*read_var_def(struct isl_stream
*s
,
505 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
508 isl_basic_map
*def
= NULL
;
513 if (vars_add_anon(v
) < 0)
517 vec
= accept_affine(s
, v
);
521 dim
= isl_basic_map_get_dim(bmap
);
522 def
= isl_basic_map_universe(dim
);
523 def
= add_divs(def
, v
);
524 def
= isl_basic_map_extend_constraints(def
, 1, 0);
525 k
= isl_basic_map_alloc_equality(def
);
527 isl_seq_cpy(def
->eq
[k
], vec
->el
, vec
->size
);
528 isl_int_set_si(def
->eq
[k
][1 + n
- 1], -1);
534 vars_drop(v
, v
->n
- n
);
536 def
= isl_basic_map_simplify(def
);
537 def
= isl_basic_map_finalize(def
);
538 bmap
= isl_basic_map_intersect(bmap
, def
);
541 isl_basic_map_free(bmap
);
542 isl_basic_map_free(def
);
546 static __isl_give isl_basic_map
*read_var_list(struct isl_stream
*s
,
547 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
550 struct isl_token
*tok
;
552 while ((tok
= next_token(s
)) != NULL
) {
555 if (tok
->type
== ISL_TOKEN_IDENT
) {
557 int p
= vars_pos(v
, tok
->u
.s
, -1);
564 bmap
= isl_basic_map_add(bmap
, type
, 1);
565 bmap
= set_name(bmap
, type
, i
, v
->v
->name
);
567 } else if (tok
->type
== ISL_TOKEN_IDENT
||
568 tok
->type
== ISL_TOKEN_VALUE
||
571 if (type
== isl_dim_param
) {
572 isl_stream_error(s
, tok
,
573 "expecting unique identifier");
576 isl_stream_push_token(s
, tok
);
578 bmap
= isl_basic_map_add(bmap
, type
, 1);
579 bmap
= read_var_def(s
, bmap
, type
, v
);
583 tok
= isl_stream_next_token(s
);
584 if (!tok
|| tok
->type
!= ',')
591 isl_stream_push_token(s
, tok
);
596 isl_basic_map_free(bmap
);
600 static __isl_give isl_mat
*accept_affine_list(struct isl_stream
*s
,
605 struct isl_token
*tok
= NULL
;
607 vec
= accept_affine(s
, v
);
608 mat
= isl_mat_from_row_vec(vec
);
613 tok
= isl_stream_next_token(s
);
615 isl_stream_error(s
, NULL
, "unexpected EOF");
618 if (tok
->type
!= ',') {
619 isl_stream_push_token(s
, tok
);
624 vec
= accept_affine(s
, v
);
625 mat
= isl_mat_add_zero_cols(mat
, 1 + v
->n
- isl_mat_cols(mat
));
626 mat
= isl_mat_vec_concat(mat
, vec
);
637 static int read_minmax_definition(struct isl_stream
*s
, struct vars
*v
)
639 struct isl_token
*tok
;
640 struct variable
*var
;
644 tok
= isl_stream_next_token(s
);
647 var
->sign
= tok
->type
== ISL_TOKEN_MIN
? -1 : 1;
650 if (isl_stream_eat(s
, '('))
653 var
->list
= accept_affine_list(s
, v
);
657 if (isl_stream_eat(s
, ')'))
663 static int read_div_definition(struct isl_stream
*s
, struct vars
*v
)
665 struct isl_token
*tok
;
668 struct variable
*var
;
671 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FLOORD
) ||
672 isl_stream_eat_if_available(s
, ISL_TOKEN_CEILD
)) {
674 if (isl_stream_eat(s
, '('))
677 if (isl_stream_eat(s
, '['))
679 if (isl_stream_eat_if_available(s
, '('))
685 aff
= accept_affine(s
, v
);
689 var
->def
= isl_vec_alloc(s
->ctx
, 2 + v
->n
);
695 isl_seq_cpy(var
->def
->el
+ 1, aff
->el
, aff
->size
);
700 if (isl_stream_eat(s
, ','))
703 if (seen_paren
&& isl_stream_eat(s
, ')'))
705 if (isl_stream_eat(s
, '/'))
712 if (tok
->type
!= ISL_TOKEN_VALUE
) {
713 isl_stream_error(s
, tok
, "expected denominator");
714 isl_stream_push_token(s
, tok
);
717 isl_int_set(var
->def
->el
[0], tok
->u
.v
);
721 if (isl_stream_eat(s
, ')'))
724 if (isl_stream_eat(s
, ']'))
731 static struct isl_basic_map
*add_div_definition(struct isl_stream
*s
,
732 struct vars
*v
, struct isl_basic_map
*bmap
, int pos
)
734 struct variable
*var
= v
->v
;
735 unsigned o_out
= isl_basic_map_offset(bmap
, isl_dim_out
) - 1;
737 if (read_div_definition(s
, v
) < 0)
740 if (isl_basic_map_add_div_constraints_var(bmap
, o_out
+ pos
,
746 isl_basic_map_free(bmap
);
750 static struct isl_basic_map
*read_defined_var_list(struct isl_stream
*s
,
751 struct vars
*v
, struct isl_basic_map
*bmap
)
753 struct isl_token
*tok
;
755 while ((tok
= isl_stream_next_token(s
)) != NULL
) {
758 unsigned n_out
= isl_basic_map_dim(bmap
, isl_dim_out
);
760 if (tok
->type
!= ISL_TOKEN_IDENT
)
763 p
= vars_pos(v
, tok
->u
.s
, -1);
767 isl_stream_error(s
, tok
, "expecting unique identifier");
771 bmap
= isl_basic_map_cow(bmap
);
772 bmap
= isl_basic_map_add(bmap
, isl_dim_out
, 1);
773 bmap
= isl_basic_map_extend_dim(bmap
, isl_dim_copy(bmap
->dim
),
777 tok
= isl_stream_next_token(s
);
778 if (tok
&& tok
->type
== '=') {
780 bmap
= add_div_definition(s
, v
, bmap
, n_out
);
781 tok
= isl_stream_next_token(s
);
784 if (!tok
|| tok
->type
!= ',')
790 isl_stream_push_token(s
, tok
);
795 isl_basic_map_free(bmap
);
799 static int next_is_tuple(struct isl_stream
*s
)
801 struct isl_token
*tok
;
804 tok
= isl_stream_next_token(s
);
807 if (tok
->type
== '[') {
808 isl_stream_push_token(s
, tok
);
811 if (tok
->type
!= ISL_TOKEN_IDENT
&& !tok
->is_keyword
) {
812 isl_stream_push_token(s
, tok
);
816 is_tuple
= isl_stream_next_token_is(s
, '[');
818 isl_stream_push_token(s
, tok
);
823 static __isl_give isl_basic_map
*read_tuple(struct isl_stream
*s
,
824 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
);
826 static __isl_give isl_basic_map
*read_nested_tuple(struct isl_stream
*s
,
827 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
829 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
830 if (isl_stream_eat(s
, ISL_TOKEN_TO
))
832 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
833 bmap
= isl_basic_map_from_range(isl_basic_map_wrap(bmap
));
836 isl_basic_map_free(bmap
);
840 static __isl_give isl_basic_map
*read_tuple(struct isl_stream
*s
,
841 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
843 struct isl_token
*tok
;
846 tok
= isl_stream_next_token(s
);
847 if (tok
&& (tok
->type
== ISL_TOKEN_IDENT
|| tok
->is_keyword
)) {
848 name
= strdup(tok
->u
.s
);
852 tok
= isl_stream_next_token(s
);
854 if (!tok
|| tok
->type
!= '[') {
855 isl_stream_error(s
, tok
, "expecting '['");
859 if (type
!= isl_dim_param
&& next_is_tuple(s
)) {
860 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
861 int nparam
= isl_dim_size(dim
, isl_dim_param
);
862 int n_in
= isl_dim_size(dim
, isl_dim_in
);
863 isl_basic_map
*nested
;
864 if (type
== isl_dim_out
)
865 dim
= isl_dim_move(dim
, isl_dim_param
, nparam
,
866 isl_dim_in
, 0, n_in
);
867 nested
= isl_basic_map_alloc_dim(dim
, 0, 0, 0);
868 nested
= read_nested_tuple(s
, nested
, v
);
869 if (type
== isl_dim_in
) {
870 nested
= isl_basic_map_reverse(nested
);
871 bmap
= isl_basic_map_intersect(nested
, bmap
);
874 dim
= isl_dim_range(isl_basic_map_get_dim(nested
));
875 dim
= isl_dim_drop(dim
, isl_dim_param
, nparam
, n_in
);
876 dim
= isl_dim_join(isl_basic_map_get_dim(bmap
), dim
);
877 bset
= isl_basic_map_domain(bmap
);
878 nested
= isl_basic_map_reset_dim(nested
, dim
);
879 bmap
= isl_basic_map_intersect_domain(nested
, bset
);
882 bmap
= read_var_list(s
, bmap
, type
, v
);
883 tok
= isl_stream_next_token(s
);
884 if (!tok
|| tok
->type
!= ']') {
885 isl_stream_error(s
, tok
, "expecting ']'");
891 bmap
= isl_basic_map_set_tuple_name(bmap
, type
, name
);
899 isl_basic_map_free(bmap
);
903 static __isl_give isl_basic_map
*construct_constraint(
904 __isl_take isl_basic_map
*bmap
, enum isl_token_type type
,
905 isl_int
*left
, isl_int
*right
)
913 len
= 1 + isl_basic_map_total_dim(bmap
);
916 k
= isl_basic_map_alloc_inequality(bmap
);
919 if (type
== ISL_TOKEN_LE
)
920 isl_seq_combine(bmap
->ineq
[k
], ctx
->negone
, left
,
923 else if (type
== ISL_TOKEN_GE
)
924 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
927 else if (type
== ISL_TOKEN_LT
) {
928 isl_seq_combine(bmap
->ineq
[k
], ctx
->negone
, left
,
931 isl_int_sub_ui(bmap
->ineq
[k
][0], bmap
->ineq
[k
][0], 1);
932 } else if (type
== ISL_TOKEN_GT
) {
933 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
936 isl_int_sub_ui(bmap
->ineq
[k
][0], bmap
->ineq
[k
][0], 1);
938 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
941 isl_basic_map_inequality_to_equality(bmap
, k
);
946 isl_basic_map_free(bmap
);
950 static int is_comparator(struct isl_token
*tok
)
967 /* Add any variables in the variable list "v" that are not already in "bmap"
968 * as output variables in "bmap".
970 static __isl_give isl_basic_map
*add_lifted_divs(__isl_take isl_basic_map
*bmap
,
975 struct variable
*var
;
977 extra
= v
->n
- isl_basic_map_total_dim(bmap
);
982 bmap
= isl_basic_map_add(bmap
, isl_dim_out
, extra
);
983 bmap
= isl_basic_map_extend_dim(bmap
, isl_basic_map_get_dim(bmap
),
986 for (i
= 0, var
= v
->v
; i
< extra
; ++i
, var
= var
->next
) {
989 var
->def
= isl_vec_zero_extend(var
->def
, 2 + v
->n
);
992 if (isl_basic_map_add_div_constraints_var(bmap
, var
->pos
,
999 isl_basic_map_free(bmap
);
1003 static struct isl_basic_map
*add_constraint(struct isl_stream
*s
,
1004 struct vars
*v
, struct isl_basic_map
*bmap
)
1007 struct isl_token
*tok
= NULL
;
1008 struct isl_mat
*aff1
= NULL
, *aff2
= NULL
;
1010 bmap
= isl_basic_map_cow(bmap
);
1012 aff1
= accept_affine_list(s
, v
);
1015 tok
= isl_stream_next_token(s
);
1016 if (!is_comparator(tok
)) {
1017 isl_stream_error(s
, tok
, "missing operator");
1019 isl_stream_push_token(s
, tok
);
1024 aff2
= accept_affine_list(s
, v
);
1028 aff1
= isl_mat_add_zero_cols(aff1
, aff2
->n_col
- aff1
->n_col
);
1031 bmap
= add_lifted_divs(bmap
, v
);
1032 bmap
= isl_basic_map_extend_constraints(bmap
, 0,
1033 aff1
->n_row
* aff2
->n_row
);
1034 for (i
= 0; i
< aff1
->n_row
; ++i
)
1035 for (j
= 0; j
< aff2
->n_row
; ++j
)
1036 bmap
= construct_constraint(bmap
, tok
->type
,
1037 aff1
->row
[i
], aff2
->row
[j
]);
1038 isl_token_free(tok
);
1042 tok
= isl_stream_next_token(s
);
1043 if (!is_comparator(tok
)) {
1045 isl_stream_push_token(s
, tok
);
1054 isl_token_free(tok
);
1057 isl_basic_map_free(bmap
);
1061 /* Return first variable, starting at n, representing a min or max,
1062 * or NULL if there is no such variable.
1064 static struct variable
*first_minmax(struct vars
*v
, int n
)
1066 struct variable
*first
= NULL
;
1067 struct variable
*var
;
1069 for (var
= v
->v
; var
&& var
->pos
>= n
; var
= var
->next
)
1076 /* Check whether the variable at the given position only occurs in
1077 * inequalities and only with the given sign.
1079 static int all_coefficients_of_sign(__isl_keep isl_map
*map
, int pos
, int sign
)
1086 for (i
= 0; i
< map
->n
; ++i
) {
1087 isl_basic_map
*bmap
= map
->p
[i
];
1089 for (j
= 0; j
< bmap
->n_eq
; ++j
)
1090 if (!isl_int_is_zero(bmap
->eq
[j
][1 + pos
]))
1092 for (j
= 0; j
< bmap
->n_ineq
; ++j
) {
1093 int s
= isl_int_sgn(bmap
->ineq
[j
][1 + pos
]);
1104 /* Given a variable m which represents a min or a max of n expressions
1105 * b_i, add the constraints
1109 * in case of a min (var->sign < 0) and m >= b_i in case of a max.
1111 static __isl_give isl_map
*bound_minmax(__isl_take isl_map
*map
,
1112 struct variable
*var
)
1115 isl_basic_map
*bound
;
1118 total
= isl_map_dim(map
, isl_dim_all
);
1119 bound
= isl_basic_map_alloc_dim(isl_map_get_dim(map
),
1120 0, 0, var
->list
->n_row
);
1122 for (i
= 0; i
< var
->list
->n_row
; ++i
) {
1123 k
= isl_basic_map_alloc_inequality(bound
);
1127 isl_seq_cpy(bound
->ineq
[k
], var
->list
->row
[i
],
1130 isl_seq_neg(bound
->ineq
[k
], var
->list
->row
[i
],
1132 isl_int_set_si(bound
->ineq
[k
][1 + var
->pos
], var
->sign
);
1133 isl_seq_clr(bound
->ineq
[k
] + var
->list
->n_col
,
1134 1 + total
- var
->list
->n_col
);
1137 map
= isl_map_intersect(map
, isl_map_from_basic_map(bound
));
1141 isl_basic_map_free(bound
);
1146 /* Given a variable m which represents a min (or max) of n expressions
1147 * b_i, add constraints that assigns the minimal upper bound to m, i.e.,
1148 * divide the space into cells where one
1149 * of the upper bounds is smaller than all the others and assign
1150 * this upper bound to m.
1152 * In particular, if there are n bounds b_i, then the input map
1153 * is split into n pieces, each with the extra constraints
1156 * b_i <= b_j for j > i
1157 * b_i < b_j for j < i
1159 * in case of a min (var->sign < 0) and similarly in case of a max.
1161 * Note: this function is very similar to set_minimum in isl_tab_pip.c
1162 * Perhaps we should try to merge the two.
1164 static __isl_give isl_map
*set_minmax(__isl_take isl_map
*map
,
1165 struct variable
*var
)
1168 isl_basic_map
*bmap
= NULL
;
1170 isl_map
*split
= NULL
;
1173 ctx
= isl_map_get_ctx(map
);
1174 total
= isl_map_dim(map
, isl_dim_all
);
1175 split
= isl_map_alloc_dim(isl_map_get_dim(map
),
1176 var
->list
->n_row
, ISL_SET_DISJOINT
);
1178 for (i
= 0; i
< var
->list
->n_row
; ++i
) {
1179 bmap
= isl_basic_map_alloc_dim(isl_map_get_dim(map
), 0,
1180 1, var
->list
->n_row
- 1);
1181 k
= isl_basic_map_alloc_equality(bmap
);
1184 isl_seq_cpy(bmap
->eq
[k
], var
->list
->row
[i
], var
->list
->n_col
);
1185 isl_int_set_si(bmap
->eq
[k
][1 + var
->pos
], -1);
1186 for (j
= 0; j
< var
->list
->n_row
; ++j
) {
1189 k
= isl_basic_map_alloc_inequality(bmap
);
1193 isl_seq_combine(bmap
->ineq
[k
],
1194 ctx
->one
, var
->list
->row
[j
],
1195 ctx
->negone
, var
->list
->row
[i
],
1198 isl_seq_combine(bmap
->ineq
[k
],
1199 ctx
->negone
, var
->list
->row
[j
],
1200 ctx
->one
, var
->list
->row
[i
],
1202 isl_seq_clr(bmap
->ineq
[k
] + var
->list
->n_col
,
1203 1 + total
- var
->list
->n_col
);
1205 isl_int_sub_ui(bmap
->ineq
[k
][0],
1206 bmap
->ineq
[k
][0], 1);
1208 bmap
= isl_basic_map_finalize(bmap
);
1209 split
= isl_map_add_basic_map(split
, bmap
);
1212 map
= isl_map_intersect(map
, split
);
1216 isl_basic_map_free(bmap
);
1217 isl_map_free(split
);
1222 /* Plug in the definitions of all min and max expressions.
1223 * If a min expression only appears in inequalities and only
1224 * with a positive coefficient, then we can simply bound
1225 * the variable representing the min by its defining terms
1226 * and similarly for a max expression.
1227 * Otherwise, we have to assign the different terms to the
1228 * variable under the condition that the assigned term is smaller
1229 * than the other terms.
1231 static __isl_give isl_map
*add_minmax(__isl_take isl_map
*map
,
1232 struct vars
*v
, int n
)
1234 struct variable
*var
;
1237 var
= first_minmax(v
, n
);
1240 if (all_coefficients_of_sign(map
, var
->pos
, -var
->sign
))
1241 map
= bound_minmax(map
, var
);
1243 map
= set_minmax(map
, var
);
1250 static isl_map
*read_constraint(struct isl_stream
*s
,
1251 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1260 bmap
= isl_basic_set_unwrap(isl_basic_set_lift(isl_basic_map_wrap(bmap
)));
1261 total
= isl_basic_map_total_dim(bmap
);
1262 while (v
->n
< total
)
1263 if (vars_add_anon(v
) < 0)
1266 bmap
= add_constraint(s
, v
, bmap
);
1267 bmap
= isl_basic_map_simplify(bmap
);
1268 bmap
= isl_basic_map_finalize(bmap
);
1270 map
= isl_map_from_basic_map(bmap
);
1272 map
= add_minmax(map
, v
, n
);
1274 map
= isl_set_unwrap(isl_map_domain(map
));
1276 vars_drop(v
, v
->n
- n
);
1280 isl_basic_map_free(bmap
);
1284 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1285 struct vars
*v
, __isl_take isl_basic_map
*bmap
);
1287 static __isl_give isl_map
*read_exists(struct isl_stream
*s
,
1288 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1291 int seen_paren
= isl_stream_eat_if_available(s
, '(');
1292 isl_map
*map
= NULL
;
1294 bmap
= isl_basic_map_from_domain(isl_basic_map_wrap(bmap
));
1295 bmap
= read_defined_var_list(s
, v
, bmap
);
1297 if (isl_stream_eat(s
, ':'))
1300 map
= read_disjuncts(s
, v
, bmap
);
1301 map
= isl_set_unwrap(isl_map_domain(map
));
1304 vars_drop(v
, v
->n
- n
);
1305 if (seen_paren
&& isl_stream_eat(s
, ')'))
1310 isl_basic_map_free(bmap
);
1315 static __isl_give isl_map
*read_conjunct(struct isl_stream
*s
,
1316 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1320 if (isl_stream_eat_if_available(s
, '(')) {
1321 map
= read_disjuncts(s
, v
, bmap
);
1322 if (isl_stream_eat(s
, ')'))
1327 if (isl_stream_eat_if_available(s
, ISL_TOKEN_EXISTS
))
1328 return read_exists(s
, v
, bmap
);
1330 if (isl_stream_eat_if_available(s
, ISL_TOKEN_TRUE
))
1331 return isl_map_from_basic_map(bmap
);
1333 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FALSE
)) {
1334 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1335 isl_basic_map_free(bmap
);
1336 return isl_map_empty(dim
);
1339 return read_constraint(s
, v
, bmap
);
1345 static __isl_give isl_map
*read_conjuncts(struct isl_stream
*s
,
1346 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1351 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1352 map
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1355 t
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1356 map
= isl_map_subtract(t
, map
);
1359 while (isl_stream_eat_if_available(s
, ISL_TOKEN_AND
)) {
1362 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1363 map_i
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1365 map
= isl_map_subtract(map
, map_i
);
1367 map
= isl_map_intersect(map
, map_i
);
1370 isl_basic_map_free(bmap
);
1374 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1375 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1377 struct isl_map
*map
;
1379 if (isl_stream_next_token_is(s
, '}')) {
1380 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1381 isl_basic_map_free(bmap
);
1382 return isl_map_universe(dim
);
1385 map
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1386 while (isl_stream_eat_if_available(s
, ISL_TOKEN_OR
)) {
1389 map_i
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1390 map
= isl_map_union(map
, map_i
);
1393 isl_basic_map_free(bmap
);
1397 static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map
*bmap
, int pos
)
1399 if (pos
< isl_basic_map_dim(bmap
, isl_dim_out
))
1400 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1401 isl_basic_map_dim(bmap
, isl_dim_in
) + pos
;
1402 pos
-= isl_basic_map_dim(bmap
, isl_dim_out
);
1404 if (pos
< isl_basic_map_dim(bmap
, isl_dim_in
))
1405 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) + pos
;
1406 pos
-= isl_basic_map_dim(bmap
, isl_dim_in
);
1408 if (pos
< isl_basic_map_dim(bmap
, isl_dim_div
))
1409 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1410 isl_basic_map_dim(bmap
, isl_dim_in
) +
1411 isl_basic_map_dim(bmap
, isl_dim_out
) + pos
;
1412 pos
-= isl_basic_map_dim(bmap
, isl_dim_div
);
1414 if (pos
< isl_basic_map_dim(bmap
, isl_dim_param
))
1420 static __isl_give isl_basic_map
*basic_map_read_polylib_constraint(
1421 struct isl_stream
*s
, __isl_take isl_basic_map
*bmap
)
1424 struct isl_token
*tok
;
1434 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
1435 dim
= isl_basic_map_dim(bmap
, isl_dim_out
);
1437 tok
= isl_stream_next_token(s
);
1438 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1439 isl_stream_error(s
, tok
, "expecting coefficient");
1441 isl_stream_push_token(s
, tok
);
1444 if (!tok
->on_new_line
) {
1445 isl_stream_error(s
, tok
, "coefficient should appear on new line");
1446 isl_stream_push_token(s
, tok
);
1450 type
= isl_int_get_si(tok
->u
.v
);
1451 isl_token_free(tok
);
1453 isl_assert(s
->ctx
, type
== 0 || type
== 1, goto error
);
1455 k
= isl_basic_map_alloc_equality(bmap
);
1458 k
= isl_basic_map_alloc_inequality(bmap
);
1464 for (j
= 0; j
< 1 + isl_basic_map_total_dim(bmap
); ++j
) {
1466 tok
= isl_stream_next_token(s
);
1467 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1468 isl_stream_error(s
, tok
, "expecting coefficient");
1470 isl_stream_push_token(s
, tok
);
1473 if (tok
->on_new_line
) {
1474 isl_stream_error(s
, tok
,
1475 "coefficient should not appear on new line");
1476 isl_stream_push_token(s
, tok
);
1479 pos
= polylib_pos_to_isl_pos(bmap
, j
);
1480 isl_int_set(c
[pos
], tok
->u
.v
);
1481 isl_token_free(tok
);
1486 isl_basic_map_free(bmap
);
1490 static __isl_give isl_basic_map
*basic_map_read_polylib(struct isl_stream
*s
,
1494 struct isl_token
*tok
;
1495 struct isl_token
*tok2
;
1498 unsigned in
= 0, out
, local
= 0;
1499 struct isl_basic_map
*bmap
= NULL
;
1504 tok
= isl_stream_next_token(s
);
1506 isl_stream_error(s
, NULL
, "unexpected EOF");
1509 tok2
= isl_stream_next_token(s
);
1511 isl_token_free(tok
);
1512 isl_stream_error(s
, NULL
, "unexpected EOF");
1515 if (tok
->type
!= ISL_TOKEN_VALUE
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1516 isl_stream_push_token(s
, tok2
);
1517 isl_stream_push_token(s
, tok
);
1518 isl_stream_error(s
, NULL
,
1519 "expecting constraint matrix dimensions");
1522 n_row
= isl_int_get_si(tok
->u
.v
);
1523 n_col
= isl_int_get_si(tok2
->u
.v
);
1524 on_new_line
= tok2
->on_new_line
;
1525 isl_token_free(tok2
);
1526 isl_token_free(tok
);
1527 isl_assert(s
->ctx
, !on_new_line
, return NULL
);
1528 isl_assert(s
->ctx
, n_row
>= 0, return NULL
);
1529 isl_assert(s
->ctx
, n_col
>= 2 + nparam
, return NULL
);
1530 tok
= isl_stream_next_token_on_same_line(s
);
1532 if (tok
->type
!= ISL_TOKEN_VALUE
) {
1533 isl_stream_error(s
, tok
,
1534 "expecting number of output dimensions");
1535 isl_stream_push_token(s
, tok
);
1538 out
= isl_int_get_si(tok
->u
.v
);
1539 isl_token_free(tok
);
1541 tok
= isl_stream_next_token_on_same_line(s
);
1542 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1543 isl_stream_error(s
, tok
,
1544 "expecting number of input dimensions");
1546 isl_stream_push_token(s
, tok
);
1549 in
= isl_int_get_si(tok
->u
.v
);
1550 isl_token_free(tok
);
1552 tok
= isl_stream_next_token_on_same_line(s
);
1553 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1554 isl_stream_error(s
, tok
,
1555 "expecting number of existentials");
1557 isl_stream_push_token(s
, tok
);
1560 local
= isl_int_get_si(tok
->u
.v
);
1561 isl_token_free(tok
);
1563 tok
= isl_stream_next_token_on_same_line(s
);
1564 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1565 isl_stream_error(s
, tok
,
1566 "expecting number of parameters");
1568 isl_stream_push_token(s
, tok
);
1571 nparam
= isl_int_get_si(tok
->u
.v
);
1572 isl_token_free(tok
);
1573 if (n_col
!= 1 + out
+ in
+ local
+ nparam
+ 1) {
1574 isl_stream_error(s
, NULL
,
1575 "dimensions don't match");
1579 out
= n_col
- 2 - nparam
;
1580 bmap
= isl_basic_map_alloc(s
->ctx
, nparam
, in
, out
, local
, n_row
, n_row
);
1584 for (i
= 0; i
< local
; ++i
) {
1585 int k
= isl_basic_map_alloc_div(bmap
);
1588 isl_seq_clr(bmap
->div
[k
], 1 + 1 + nparam
+ in
+ out
+ local
);
1591 for (i
= 0; i
< n_row
; ++i
)
1592 bmap
= basic_map_read_polylib_constraint(s
, bmap
);
1594 tok
= isl_stream_next_token_on_same_line(s
);
1596 isl_stream_error(s
, tok
, "unexpected extra token on line");
1597 isl_stream_push_token(s
, tok
);
1601 bmap
= isl_basic_map_simplify(bmap
);
1602 bmap
= isl_basic_map_finalize(bmap
);
1605 isl_basic_map_free(bmap
);
1609 static struct isl_map
*map_read_polylib(struct isl_stream
*s
, int nparam
)
1611 struct isl_token
*tok
;
1612 struct isl_token
*tok2
;
1614 struct isl_map
*map
;
1616 tok
= isl_stream_next_token(s
);
1618 isl_stream_error(s
, NULL
, "unexpected EOF");
1621 tok2
= isl_stream_next_token_on_same_line(s
);
1622 if (tok2
&& tok2
->type
== ISL_TOKEN_VALUE
) {
1623 isl_stream_push_token(s
, tok2
);
1624 isl_stream_push_token(s
, tok
);
1625 return isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1628 isl_stream_error(s
, tok2
, "unexpected token");
1629 isl_stream_push_token(s
, tok2
);
1630 isl_stream_push_token(s
, tok
);
1633 n
= isl_int_get_si(tok
->u
.v
);
1634 isl_token_free(tok
);
1636 isl_assert(s
->ctx
, n
>= 1, return NULL
);
1638 map
= isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1640 for (i
= 1; map
&& i
< n
; ++i
)
1641 map
= isl_map_union(map
,
1642 isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
)));
1647 static int optional_power(struct isl_stream
*s
)
1650 struct isl_token
*tok
;
1652 tok
= isl_stream_next_token(s
);
1655 if (tok
->type
!= '^') {
1656 isl_stream_push_token(s
, tok
);
1659 isl_token_free(tok
);
1660 tok
= isl_stream_next_token(s
);
1661 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1662 isl_stream_error(s
, tok
, "expecting exponent");
1664 isl_stream_push_token(s
, tok
);
1667 pow
= isl_int_get_si(tok
->u
.v
);
1668 isl_token_free(tok
);
1672 static __isl_give isl_div
*read_div(struct isl_stream
*s
,
1673 __isl_take isl_dim
*dim
, struct vars
*v
)
1676 isl_basic_map
*bmap
;
1679 bmap
= isl_basic_map_universe(dim
);
1681 if (vars_add_anon(v
) < 0)
1683 if (read_div_definition(s
, v
) < 0)
1685 bmap
= add_divs(bmap
, v
);
1686 bmap
= isl_basic_map_order_divs(bmap
);
1689 vars_drop(v
, v
->n
- n
);
1691 return isl_basic_map_div(bmap
, bmap
->n_div
- 1);
1693 isl_basic_map_free(bmap
);
1697 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1698 __isl_keep isl_basic_map
*bmap
, struct vars
*v
);
1700 static __isl_give isl_qpolynomial
*read_factor(struct isl_stream
*s
,
1701 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1703 struct isl_qpolynomial
*qp
;
1704 struct isl_token
*tok
;
1706 tok
= next_token(s
);
1708 isl_stream_error(s
, NULL
, "unexpected EOF");
1711 if (tok
->type
== '(') {
1714 isl_token_free(tok
);
1715 qp
= read_term(s
, bmap
, v
);
1718 if (isl_stream_eat(s
, ')'))
1720 pow
= optional_power(s
);
1721 qp
= isl_qpolynomial_pow(qp
, pow
);
1722 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
1723 struct isl_token
*tok2
;
1724 tok2
= isl_stream_next_token(s
);
1725 if (tok2
&& tok2
->type
== '/') {
1726 isl_token_free(tok2
);
1727 tok2
= next_token(s
);
1728 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1729 isl_stream_error(s
, tok2
, "expected denominator");
1730 isl_token_free(tok
);
1731 isl_token_free(tok2
);
1734 qp
= isl_qpolynomial_rat_cst(isl_basic_map_get_dim(bmap
),
1735 tok
->u
.v
, tok2
->u
.v
);
1736 isl_token_free(tok2
);
1738 isl_stream_push_token(s
, tok2
);
1739 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1742 isl_token_free(tok
);
1743 } else if (tok
->type
== ISL_TOKEN_INFTY
) {
1744 isl_token_free(tok
);
1745 qp
= isl_qpolynomial_infty(isl_basic_map_get_dim(bmap
));
1746 } else if (tok
->type
== ISL_TOKEN_NAN
) {
1747 isl_token_free(tok
);
1748 qp
= isl_qpolynomial_nan(isl_basic_map_get_dim(bmap
));
1749 } else if (tok
->type
== ISL_TOKEN_IDENT
) {
1751 int pos
= vars_pos(v
, tok
->u
.s
, -1);
1754 isl_token_free(tok
);
1758 vars_drop(v
, v
->n
- n
);
1759 isl_stream_error(s
, tok
, "unknown identifier");
1760 isl_token_free(tok
);
1763 isl_token_free(tok
);
1764 pow
= optional_power(s
);
1765 qp
= isl_qpolynomial_var_pow(isl_basic_map_get_dim(bmap
), pos
, pow
);
1766 } else if (tok
->type
== '[') {
1770 isl_stream_push_token(s
, tok
);
1771 div
= read_div(s
, isl_basic_map_get_dim(bmap
), v
);
1772 pow
= optional_power(s
);
1773 qp
= isl_qpolynomial_div_pow(div
, pow
);
1774 } else if (tok
->type
== '-') {
1775 struct isl_qpolynomial
*qp2
;
1777 isl_token_free(tok
);
1778 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1780 qp2
= read_factor(s
, bmap
, v
);
1781 qp
= isl_qpolynomial_mul(qp
, qp2
);
1783 isl_stream_error(s
, tok
, "unexpected isl_token");
1784 isl_stream_push_token(s
, tok
);
1788 if (isl_stream_eat_if_available(s
, '*') ||
1789 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
1790 struct isl_qpolynomial
*qp2
;
1792 qp2
= read_factor(s
, bmap
, v
);
1793 qp
= isl_qpolynomial_mul(qp
, qp2
);
1798 isl_qpolynomial_free(qp
);
1802 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1803 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1805 struct isl_token
*tok
;
1806 struct isl_qpolynomial
*qp
;
1808 qp
= read_factor(s
, bmap
, v
);
1811 tok
= next_token(s
);
1815 if (tok
->type
== '+') {
1816 struct isl_qpolynomial
*qp2
;
1818 isl_token_free(tok
);
1819 qp2
= read_factor(s
, bmap
, v
);
1820 qp
= isl_qpolynomial_add(qp
, qp2
);
1821 } else if (tok
->type
== '-') {
1822 struct isl_qpolynomial
*qp2
;
1824 isl_token_free(tok
);
1825 qp2
= read_factor(s
, bmap
, v
);
1826 qp
= isl_qpolynomial_sub(qp
, qp2
);
1827 } else if (tok
->type
== ISL_TOKEN_VALUE
&&
1828 isl_int_is_neg(tok
->u
.v
)) {
1829 struct isl_qpolynomial
*qp2
;
1831 isl_stream_push_token(s
, tok
);
1832 qp2
= read_factor(s
, bmap
, v
);
1833 qp
= isl_qpolynomial_add(qp
, qp2
);
1835 isl_stream_push_token(s
, tok
);
1843 static __isl_give isl_map
*read_optional_disjuncts(struct isl_stream
*s
,
1844 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1846 struct isl_token
*tok
;
1847 struct isl_map
*map
;
1849 tok
= isl_stream_next_token(s
);
1851 isl_stream_error(s
, NULL
, "unexpected EOF");
1854 map
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1855 if (tok
->type
== ':' ||
1856 (tok
->type
== ISL_TOKEN_OR
&& !strcmp(tok
->u
.s
, "|"))) {
1857 isl_token_free(tok
);
1858 map
= isl_map_intersect(map
,
1859 read_disjuncts(s
, v
, isl_basic_map_copy(bmap
)));
1861 isl_stream_push_token(s
, tok
);
1863 isl_basic_map_free(bmap
);
1867 isl_basic_map_free(bmap
);
1871 static struct isl_obj
obj_read_poly(struct isl_stream
*s
,
1872 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1874 struct isl_obj obj
= { isl_obj_pw_qpolynomial
, NULL
};
1875 struct isl_pw_qpolynomial
*pwqp
;
1876 struct isl_qpolynomial
*qp
;
1877 struct isl_map
*map
;
1878 struct isl_set
*set
;
1880 qp
= read_term(s
, bmap
, v
);
1881 map
= read_optional_disjuncts(s
, bmap
, v
);
1882 set
= isl_map_range(map
);
1884 pwqp
= isl_pw_qpolynomial_alloc(set
, qp
);
1886 vars_drop(v
, v
->n
- n
);
1892 static struct isl_obj
obj_read_poly_or_fold(struct isl_stream
*s
,
1893 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1895 struct isl_obj obj
= { isl_obj_pw_qpolynomial_fold
, NULL
};
1896 isl_qpolynomial
*qp
;
1897 isl_qpolynomial_fold
*fold
= NULL
;
1898 isl_pw_qpolynomial_fold
*pwf
;
1902 if (!isl_stream_eat_if_available(s
, ISL_TOKEN_MAX
))
1903 return obj_read_poly(s
, bmap
, v
, n
);
1905 if (isl_stream_eat(s
, '('))
1908 qp
= read_term(s
, bmap
, v
);
1909 fold
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1911 while (isl_stream_eat_if_available(s
, ',')) {
1912 isl_qpolynomial_fold
*fold_i
;
1913 qp
= read_term(s
, bmap
, v
);
1914 fold_i
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1915 fold
= isl_qpolynomial_fold_fold(fold
, fold_i
);
1918 if (isl_stream_eat(s
, ')'))
1921 map
= read_optional_disjuncts(s
, bmap
, v
);
1922 set
= isl_map_range(map
);
1923 pwf
= isl_pw_qpolynomial_fold_alloc(isl_fold_max
, set
, fold
);
1925 vars_drop(v
, v
->n
- n
);
1930 isl_basic_map_free(bmap
);
1931 isl_qpolynomial_fold_free(fold
);
1932 obj
.type
= isl_obj_none
;
1936 static int is_rational(struct isl_stream
*s
)
1938 struct isl_token
*tok
;
1940 tok
= isl_stream_next_token(s
);
1943 if (tok
->type
== ISL_TOKEN_RAT
&& isl_stream_next_token_is(s
, ':')) {
1944 isl_token_free(tok
);
1945 isl_stream_eat(s
, ':');
1949 isl_stream_push_token(s
, tok
);
1954 static struct isl_obj
obj_read_body(struct isl_stream
*s
,
1955 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1957 struct isl_map
*map
= NULL
;
1958 struct isl_token
*tok
;
1959 struct isl_obj obj
= { isl_obj_set
, NULL
};
1963 bmap
= isl_basic_map_set_rational(bmap
);
1965 if (!next_is_tuple(s
))
1966 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1968 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
1971 tok
= isl_stream_next_token(s
);
1972 if (tok
&& tok
->type
== ISL_TOKEN_TO
) {
1973 obj
.type
= isl_obj_map
;
1974 isl_token_free(tok
);
1975 if (!next_is_tuple(s
)) {
1976 bmap
= isl_basic_map_reverse(bmap
);
1977 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1979 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
1983 bmap
= isl_basic_map_reverse(bmap
);
1985 isl_stream_push_token(s
, tok
);
1988 map
= read_optional_disjuncts(s
, bmap
, v
);
1990 vars_drop(v
, v
->n
- n
);
1995 isl_basic_map_free(bmap
);
1996 obj
.type
= isl_obj_none
;
2000 static struct isl_obj
to_union(isl_ctx
*ctx
, struct isl_obj obj
)
2002 if (obj
.type
== isl_obj_map
) {
2003 obj
.v
= isl_union_map_from_map(obj
.v
);
2004 obj
.type
= isl_obj_union_map
;
2005 } else if (obj
.type
== isl_obj_set
) {
2006 obj
.v
= isl_union_set_from_set(obj
.v
);
2007 obj
.type
= isl_obj_union_set
;
2008 } else if (obj
.type
== isl_obj_pw_qpolynomial
) {
2009 obj
.v
= isl_union_pw_qpolynomial_from_pw_qpolynomial(obj
.v
);
2010 obj
.type
= isl_obj_union_pw_qpolynomial
;
2011 } else if (obj
.type
== isl_obj_pw_qpolynomial_fold
) {
2012 obj
.v
= isl_union_pw_qpolynomial_fold_from_pw_qpolynomial_fold(obj
.v
);
2013 obj
.type
= isl_obj_union_pw_qpolynomial_fold
;
2015 isl_assert(ctx
, 0, goto error
);
2018 obj
.type
->free(obj
.v
);
2019 obj
.type
= isl_obj_none
;
2023 static struct isl_obj
obj_add(struct isl_ctx
*ctx
,
2024 struct isl_obj obj1
, struct isl_obj obj2
)
2026 if (obj1
.type
== isl_obj_set
&& obj2
.type
== isl_obj_union_set
)
2027 obj1
= to_union(ctx
, obj1
);
2028 if (obj1
.type
== isl_obj_union_set
&& obj2
.type
== isl_obj_set
)
2029 obj2
= to_union(ctx
, obj2
);
2030 if (obj1
.type
== isl_obj_map
&& obj2
.type
== isl_obj_union_map
)
2031 obj1
= to_union(ctx
, obj1
);
2032 if (obj1
.type
== isl_obj_union_map
&& obj2
.type
== isl_obj_map
)
2033 obj2
= to_union(ctx
, obj2
);
2034 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2035 obj2
.type
== isl_obj_union_pw_qpolynomial
)
2036 obj1
= to_union(ctx
, obj1
);
2037 if (obj1
.type
== isl_obj_union_pw_qpolynomial
&&
2038 obj2
.type
== isl_obj_pw_qpolynomial
)
2039 obj2
= to_union(ctx
, obj2
);
2040 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2041 obj2
.type
== isl_obj_union_pw_qpolynomial_fold
)
2042 obj1
= to_union(ctx
, obj1
);
2043 if (obj1
.type
== isl_obj_union_pw_qpolynomial_fold
&&
2044 obj2
.type
== isl_obj_pw_qpolynomial_fold
)
2045 obj2
= to_union(ctx
, obj2
);
2046 isl_assert(ctx
, obj1
.type
== obj2
.type
, goto error
);
2047 if (obj1
.type
== isl_obj_map
&& !isl_map_has_equal_dim(obj1
.v
, obj2
.v
)) {
2048 obj1
= to_union(ctx
, obj1
);
2049 obj2
= to_union(ctx
, obj2
);
2051 if (obj1
.type
== isl_obj_set
&& !isl_set_has_equal_dim(obj1
.v
, obj2
.v
)) {
2052 obj1
= to_union(ctx
, obj1
);
2053 obj2
= to_union(ctx
, obj2
);
2055 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2056 !isl_pw_qpolynomial_has_equal_dim(obj1
.v
, obj2
.v
)) {
2057 obj1
= to_union(ctx
, obj1
);
2058 obj2
= to_union(ctx
, obj2
);
2060 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2061 !isl_pw_qpolynomial_fold_has_equal_dim(obj1
.v
, obj2
.v
)) {
2062 obj1
= to_union(ctx
, obj1
);
2063 obj2
= to_union(ctx
, obj2
);
2065 obj1
.v
= obj1
.type
->add(obj1
.v
, obj2
.v
);
2068 obj1
.type
->free(obj1
.v
);
2069 obj2
.type
->free(obj2
.v
);
2070 obj1
.type
= isl_obj_none
;
2075 static struct isl_obj
obj_read(struct isl_stream
*s
, int nparam
)
2077 isl_basic_map
*bmap
= NULL
;
2078 struct isl_token
*tok
;
2079 struct vars
*v
= NULL
;
2080 struct isl_obj obj
= { isl_obj_set
, NULL
};
2082 tok
= next_token(s
);
2084 isl_stream_error(s
, NULL
, "unexpected EOF");
2087 if (tok
->type
== ISL_TOKEN_VALUE
) {
2088 struct isl_token
*tok2
;
2089 struct isl_map
*map
;
2091 tok2
= isl_stream_next_token(s
);
2092 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
||
2093 isl_int_is_neg(tok2
->u
.v
)) {
2095 isl_stream_push_token(s
, tok2
);
2096 obj
.type
= isl_obj_int
;
2097 obj
.v
= isl_int_obj_alloc(s
->ctx
, tok
->u
.v
);
2098 isl_token_free(tok
);
2101 isl_stream_push_token(s
, tok2
);
2102 isl_stream_push_token(s
, tok
);
2103 map
= map_read_polylib(s
, nparam
);
2106 if (isl_map_dim(map
, isl_dim_in
) > 0)
2107 obj
.type
= isl_obj_map
;
2111 v
= vars_new(s
->ctx
);
2113 isl_stream_push_token(s
, tok
);
2116 bmap
= isl_basic_map_alloc(s
->ctx
, 0, 0, 0, 0, 0, 0);
2117 if (tok
->type
== '[') {
2118 isl_stream_push_token(s
, tok
);
2119 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2123 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2124 tok
= isl_stream_next_token(s
);
2125 if (!tok
|| tok
->type
!= ISL_TOKEN_TO
) {
2126 isl_stream_error(s
, tok
, "expecting '->'");
2128 isl_stream_push_token(s
, tok
);
2131 isl_token_free(tok
);
2132 tok
= isl_stream_next_token(s
);
2133 } else if (nparam
> 0)
2134 bmap
= isl_basic_map_add(bmap
, isl_dim_param
, nparam
);
2135 if (!tok
|| tok
->type
!= '{') {
2136 isl_stream_error(s
, tok
, "expecting '{'");
2138 isl_stream_push_token(s
, tok
);
2141 isl_token_free(tok
);
2143 tok
= isl_stream_next_token(s
);
2146 else if (tok
->type
== ISL_TOKEN_IDENT
&& !strcmp(tok
->u
.s
, "Sym")) {
2147 isl_token_free(tok
);
2148 if (isl_stream_eat(s
, '='))
2150 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2154 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2155 } else if (tok
->type
== '}') {
2156 obj
.type
= isl_obj_union_set
;
2157 obj
.v
= isl_union_set_empty(isl_basic_map_get_dim(bmap
));
2158 isl_token_free(tok
);
2161 isl_stream_push_token(s
, tok
);
2166 o
= obj_read_body(s
, isl_basic_map_copy(bmap
), v
);
2167 if (o
.type
== isl_obj_none
|| !o
.v
)
2172 obj
= obj_add(s
->ctx
, obj
, o
);
2173 if (obj
.type
== isl_obj_none
|| !obj
.v
)
2176 tok
= isl_stream_next_token(s
);
2177 if (!tok
|| tok
->type
!= ';')
2179 isl_token_free(tok
);
2180 if (isl_stream_next_token_is(s
, '}')) {
2181 tok
= isl_stream_next_token(s
);
2186 if (tok
&& tok
->type
== '}') {
2187 isl_token_free(tok
);
2189 isl_stream_error(s
, tok
, "unexpected isl_token");
2191 isl_token_free(tok
);
2196 isl_basic_map_free(bmap
);
2200 isl_basic_map_free(bmap
);
2201 obj
.type
->free(obj
.v
);
2208 struct isl_obj
isl_stream_read_obj(struct isl_stream
*s
)
2210 return obj_read(s
, -1);
2213 __isl_give isl_map
*isl_stream_read_map(struct isl_stream
*s
, int nparam
)
2217 obj
= obj_read(s
, nparam
);
2219 isl_assert(s
->ctx
, obj
.type
== isl_obj_map
||
2220 obj
.type
== isl_obj_set
, goto error
);
2224 obj
.type
->free(obj
.v
);
2228 __isl_give isl_set
*isl_stream_read_set(struct isl_stream
*s
, int nparam
)
2232 obj
= obj_read(s
, nparam
);
2234 isl_assert(s
->ctx
, obj
.type
== isl_obj_set
, goto error
);
2238 obj
.type
->free(obj
.v
);
2242 __isl_give isl_union_map
*isl_stream_read_union_map(struct isl_stream
*s
)
2246 obj
= obj_read(s
, -1);
2247 if (obj
.type
== isl_obj_map
) {
2248 obj
.type
= isl_obj_union_map
;
2249 obj
.v
= isl_union_map_from_map(obj
.v
);
2251 if (obj
.type
== isl_obj_set
) {
2252 obj
.type
= isl_obj_union_set
;
2253 obj
.v
= isl_union_set_from_set(obj
.v
);
2256 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_map
||
2257 obj
.type
== isl_obj_union_set
, goto error
);
2261 obj
.type
->free(obj
.v
);
2265 __isl_give isl_union_set
*isl_stream_read_union_set(struct isl_stream
*s
)
2269 obj
= obj_read(s
, -1);
2270 if (obj
.type
== isl_obj_set
) {
2271 obj
.type
= isl_obj_union_set
;
2272 obj
.v
= isl_union_set_from_set(obj
.v
);
2275 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_set
, goto error
);
2279 obj
.type
->free(obj
.v
);
2283 static struct isl_basic_map
*basic_map_read(struct isl_stream
*s
, int nparam
)
2286 struct isl_map
*map
;
2287 struct isl_basic_map
*bmap
;
2289 obj
= obj_read(s
, nparam
);
2294 isl_assert(map
->ctx
, map
->n
<= 1, goto error
);
2297 bmap
= isl_basic_map_empty_like_map(map
);
2299 bmap
= isl_basic_map_copy(map
->p
[0]);
2309 __isl_give isl_basic_map
*isl_basic_map_read_from_file(isl_ctx
*ctx
,
2310 FILE *input
, int nparam
)
2312 struct isl_basic_map
*bmap
;
2313 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2316 bmap
= basic_map_read(s
, nparam
);
2321 __isl_give isl_basic_set
*isl_basic_set_read_from_file(isl_ctx
*ctx
,
2322 FILE *input
, int nparam
)
2324 struct isl_basic_map
*bmap
;
2325 bmap
= isl_basic_map_read_from_file(ctx
, input
, nparam
);
2328 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2329 return (struct isl_basic_set
*)bmap
;
2331 isl_basic_map_free(bmap
);
2335 struct isl_basic_map
*isl_basic_map_read_from_str(struct isl_ctx
*ctx
,
2336 const char *str
, int nparam
)
2338 struct isl_basic_map
*bmap
;
2339 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2342 bmap
= basic_map_read(s
, nparam
);
2347 struct isl_basic_set
*isl_basic_set_read_from_str(struct isl_ctx
*ctx
,
2348 const char *str
, int nparam
)
2350 struct isl_basic_map
*bmap
;
2351 bmap
= isl_basic_map_read_from_str(ctx
, str
, nparam
);
2354 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2355 return (struct isl_basic_set
*)bmap
;
2357 isl_basic_map_free(bmap
);
2361 __isl_give isl_map
*isl_map_read_from_file(struct isl_ctx
*ctx
,
2362 FILE *input
, int nparam
)
2364 struct isl_map
*map
;
2365 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2368 map
= isl_stream_read_map(s
, nparam
);
2373 __isl_give isl_map
*isl_map_read_from_str(struct isl_ctx
*ctx
,
2374 const char *str
, int nparam
)
2376 struct isl_map
*map
;
2377 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2380 map
= isl_stream_read_map(s
, nparam
);
2385 __isl_give isl_set
*isl_set_read_from_file(struct isl_ctx
*ctx
,
2386 FILE *input
, int nparam
)
2388 struct isl_map
*map
;
2389 map
= isl_map_read_from_file(ctx
, input
, nparam
);
2392 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2393 return (struct isl_set
*)map
;
2399 struct isl_set
*isl_set_read_from_str(struct isl_ctx
*ctx
,
2400 const char *str
, int nparam
)
2402 struct isl_map
*map
;
2403 map
= isl_map_read_from_str(ctx
, str
, nparam
);
2406 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2407 return (struct isl_set
*)map
;
2413 __isl_give isl_union_map
*isl_union_map_read_from_file(isl_ctx
*ctx
,
2416 isl_union_map
*umap
;
2417 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2420 umap
= isl_stream_read_union_map(s
);
2425 __isl_give isl_union_map
*isl_union_map_read_from_str(struct isl_ctx
*ctx
,
2428 isl_union_map
*umap
;
2429 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2432 umap
= isl_stream_read_union_map(s
);
2437 __isl_give isl_union_set
*isl_union_set_read_from_file(isl_ctx
*ctx
,
2440 isl_union_set
*uset
;
2441 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2444 uset
= isl_stream_read_union_set(s
);
2449 __isl_give isl_union_set
*isl_union_set_read_from_str(struct isl_ctx
*ctx
,
2452 isl_union_set
*uset
;
2453 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2456 uset
= isl_stream_read_union_set(s
);
2461 static __isl_give isl_vec
*isl_vec_read_polylib(struct isl_stream
*s
)
2463 struct isl_vec
*vec
= NULL
;
2464 struct isl_token
*tok
;
2468 tok
= isl_stream_next_token(s
);
2469 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2470 isl_stream_error(s
, tok
, "expecting vector length");
2474 size
= isl_int_get_si(tok
->u
.v
);
2475 isl_token_free(tok
);
2477 vec
= isl_vec_alloc(s
->ctx
, size
);
2479 for (j
= 0; j
< size
; ++j
) {
2480 tok
= isl_stream_next_token(s
);
2481 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2482 isl_stream_error(s
, tok
, "expecting constant value");
2485 isl_int_set(vec
->el
[j
], tok
->u
.v
);
2486 isl_token_free(tok
);
2491 isl_token_free(tok
);
2496 static __isl_give isl_vec
*vec_read(struct isl_stream
*s
)
2498 return isl_vec_read_polylib(s
);
2501 __isl_give isl_vec
*isl_vec_read_from_file(isl_ctx
*ctx
, FILE *input
)
2504 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2512 __isl_give isl_pw_qpolynomial
*isl_stream_read_pw_qpolynomial(
2513 struct isl_stream
*s
)
2517 obj
= obj_read(s
, -1);
2519 isl_assert(s
->ctx
, obj
.type
== isl_obj_pw_qpolynomial
,
2524 obj
.type
->free(obj
.v
);
2528 __isl_give isl_pw_qpolynomial
*isl_pw_qpolynomial_read_from_str(isl_ctx
*ctx
,
2531 isl_pw_qpolynomial
*pwqp
;
2532 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2535 pwqp
= isl_stream_read_pw_qpolynomial(s
);