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
== ']' &&
585 isl_stream_next_token_is(s
, '[')) {
587 tok
= isl_stream_next_token(s
);
588 } else if (!tok
|| tok
->type
!= ',')
595 isl_stream_push_token(s
, tok
);
600 isl_basic_map_free(bmap
);
604 static __isl_give isl_mat
*accept_affine_list(struct isl_stream
*s
,
609 struct isl_token
*tok
= NULL
;
611 vec
= accept_affine(s
, v
);
612 mat
= isl_mat_from_row_vec(vec
);
617 tok
= isl_stream_next_token(s
);
619 isl_stream_error(s
, NULL
, "unexpected EOF");
622 if (tok
->type
!= ',') {
623 isl_stream_push_token(s
, tok
);
628 vec
= accept_affine(s
, v
);
629 mat
= isl_mat_add_zero_cols(mat
, 1 + v
->n
- isl_mat_cols(mat
));
630 mat
= isl_mat_vec_concat(mat
, vec
);
641 static int read_minmax_definition(struct isl_stream
*s
, struct vars
*v
)
643 struct isl_token
*tok
;
644 struct variable
*var
;
648 tok
= isl_stream_next_token(s
);
651 var
->sign
= tok
->type
== ISL_TOKEN_MIN
? -1 : 1;
654 if (isl_stream_eat(s
, '('))
657 var
->list
= accept_affine_list(s
, v
);
661 if (isl_stream_eat(s
, ')'))
667 static int read_div_definition(struct isl_stream
*s
, struct vars
*v
)
669 struct isl_token
*tok
;
672 struct variable
*var
;
675 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FLOORD
) ||
676 isl_stream_eat_if_available(s
, ISL_TOKEN_CEILD
)) {
678 if (isl_stream_eat(s
, '('))
681 if (isl_stream_eat(s
, '['))
683 if (isl_stream_eat_if_available(s
, '('))
689 aff
= accept_affine(s
, v
);
693 var
->def
= isl_vec_alloc(s
->ctx
, 2 + v
->n
);
699 isl_seq_cpy(var
->def
->el
+ 1, aff
->el
, aff
->size
);
704 if (isl_stream_eat(s
, ','))
707 if (seen_paren
&& isl_stream_eat(s
, ')'))
709 if (isl_stream_eat(s
, '/'))
716 if (tok
->type
!= ISL_TOKEN_VALUE
) {
717 isl_stream_error(s
, tok
, "expected denominator");
718 isl_stream_push_token(s
, tok
);
721 isl_int_set(var
->def
->el
[0], tok
->u
.v
);
725 if (isl_stream_eat(s
, ')'))
728 if (isl_stream_eat(s
, ']'))
735 static struct isl_basic_map
*add_div_definition(struct isl_stream
*s
,
736 struct vars
*v
, struct isl_basic_map
*bmap
, int pos
)
738 struct variable
*var
= v
->v
;
739 unsigned o_out
= isl_basic_map_offset(bmap
, isl_dim_out
) - 1;
741 if (read_div_definition(s
, v
) < 0)
744 if (isl_basic_map_add_div_constraints_var(bmap
, o_out
+ pos
,
750 isl_basic_map_free(bmap
);
754 static struct isl_basic_map
*read_defined_var_list(struct isl_stream
*s
,
755 struct vars
*v
, struct isl_basic_map
*bmap
)
757 struct isl_token
*tok
;
759 while ((tok
= isl_stream_next_token(s
)) != NULL
) {
762 unsigned n_out
= isl_basic_map_dim(bmap
, isl_dim_out
);
764 if (tok
->type
!= ISL_TOKEN_IDENT
)
767 p
= vars_pos(v
, tok
->u
.s
, -1);
771 isl_stream_error(s
, tok
, "expecting unique identifier");
775 bmap
= isl_basic_map_cow(bmap
);
776 bmap
= isl_basic_map_add(bmap
, isl_dim_out
, 1);
777 bmap
= isl_basic_map_extend_dim(bmap
, isl_dim_copy(bmap
->dim
),
781 tok
= isl_stream_next_token(s
);
782 if (tok
&& tok
->type
== '=') {
784 bmap
= add_div_definition(s
, v
, bmap
, n_out
);
785 tok
= isl_stream_next_token(s
);
788 if (!tok
|| tok
->type
!= ',')
794 isl_stream_push_token(s
, tok
);
799 isl_basic_map_free(bmap
);
803 static int next_is_tuple(struct isl_stream
*s
)
805 struct isl_token
*tok
;
808 tok
= isl_stream_next_token(s
);
811 if (tok
->type
== '[') {
812 isl_stream_push_token(s
, tok
);
815 if (tok
->type
!= ISL_TOKEN_IDENT
&& !tok
->is_keyword
) {
816 isl_stream_push_token(s
, tok
);
820 is_tuple
= isl_stream_next_token_is(s
, '[');
822 isl_stream_push_token(s
, tok
);
827 static __isl_give isl_basic_map
*read_tuple(struct isl_stream
*s
,
828 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
);
830 static __isl_give isl_basic_map
*read_nested_tuple(struct isl_stream
*s
,
831 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
833 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
834 if (isl_stream_eat(s
, ISL_TOKEN_TO
))
836 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
837 bmap
= isl_basic_map_from_range(isl_basic_map_wrap(bmap
));
840 isl_basic_map_free(bmap
);
844 static __isl_give isl_basic_map
*read_tuple(struct isl_stream
*s
,
845 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
847 struct isl_token
*tok
;
850 tok
= isl_stream_next_token(s
);
851 if (tok
&& (tok
->type
== ISL_TOKEN_IDENT
|| tok
->is_keyword
)) {
852 name
= strdup(tok
->u
.s
);
856 tok
= isl_stream_next_token(s
);
858 if (!tok
|| tok
->type
!= '[') {
859 isl_stream_error(s
, tok
, "expecting '['");
863 if (type
!= isl_dim_param
&& next_is_tuple(s
)) {
864 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
865 int nparam
= isl_dim_size(dim
, isl_dim_param
);
866 int n_in
= isl_dim_size(dim
, isl_dim_in
);
867 isl_basic_map
*nested
;
868 if (type
== isl_dim_out
)
869 dim
= isl_dim_move(dim
, isl_dim_param
, nparam
,
870 isl_dim_in
, 0, n_in
);
871 nested
= isl_basic_map_alloc_dim(dim
, 0, 0, 0);
872 nested
= read_nested_tuple(s
, nested
, v
);
873 if (type
== isl_dim_in
) {
874 nested
= isl_basic_map_reverse(nested
);
875 bmap
= isl_basic_map_intersect(nested
, bmap
);
878 dim
= isl_dim_range(isl_basic_map_get_dim(nested
));
879 dim
= isl_dim_drop(dim
, isl_dim_param
, nparam
, n_in
);
880 dim
= isl_dim_join(isl_basic_map_get_dim(bmap
), dim
);
881 bset
= isl_basic_map_domain(bmap
);
882 nested
= isl_basic_map_reset_dim(nested
, dim
);
883 bmap
= isl_basic_map_intersect_domain(nested
, bset
);
886 bmap
= read_var_list(s
, bmap
, type
, v
);
887 tok
= isl_stream_next_token(s
);
888 if (!tok
|| tok
->type
!= ']') {
889 isl_stream_error(s
, tok
, "expecting ']'");
895 bmap
= isl_basic_map_set_tuple_name(bmap
, type
, name
);
903 isl_basic_map_free(bmap
);
907 static __isl_give isl_basic_map
*construct_constraint(
908 __isl_take isl_basic_map
*bmap
, enum isl_token_type type
,
909 isl_int
*left
, isl_int
*right
)
917 len
= 1 + isl_basic_map_total_dim(bmap
);
920 k
= isl_basic_map_alloc_inequality(bmap
);
923 if (type
== ISL_TOKEN_LE
)
924 isl_seq_combine(bmap
->ineq
[k
], ctx
->negone
, left
,
927 else if (type
== ISL_TOKEN_GE
)
928 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
931 else if (type
== ISL_TOKEN_LT
) {
932 isl_seq_combine(bmap
->ineq
[k
], ctx
->negone
, left
,
935 isl_int_sub_ui(bmap
->ineq
[k
][0], bmap
->ineq
[k
][0], 1);
936 } else if (type
== ISL_TOKEN_GT
) {
937 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
940 isl_int_sub_ui(bmap
->ineq
[k
][0], bmap
->ineq
[k
][0], 1);
942 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
945 isl_basic_map_inequality_to_equality(bmap
, k
);
950 isl_basic_map_free(bmap
);
954 static int is_comparator(struct isl_token
*tok
)
971 /* Add any variables in the variable list "v" that are not already in "bmap"
972 * as output variables in "bmap".
974 static __isl_give isl_basic_map
*add_lifted_divs(__isl_take isl_basic_map
*bmap
,
979 struct variable
*var
;
981 extra
= v
->n
- isl_basic_map_total_dim(bmap
);
986 bmap
= isl_basic_map_add(bmap
, isl_dim_out
, extra
);
987 bmap
= isl_basic_map_extend_dim(bmap
, isl_basic_map_get_dim(bmap
),
990 for (i
= 0, var
= v
->v
; i
< extra
; ++i
, var
= var
->next
) {
993 var
->def
= isl_vec_zero_extend(var
->def
, 2 + v
->n
);
996 if (isl_basic_map_add_div_constraints_var(bmap
, var
->pos
,
1003 isl_basic_map_free(bmap
);
1007 static struct isl_basic_map
*add_constraint(struct isl_stream
*s
,
1008 struct vars
*v
, struct isl_basic_map
*bmap
)
1011 struct isl_token
*tok
= NULL
;
1012 struct isl_mat
*aff1
= NULL
, *aff2
= NULL
;
1014 bmap
= isl_basic_map_cow(bmap
);
1016 aff1
= accept_affine_list(s
, v
);
1019 tok
= isl_stream_next_token(s
);
1020 if (!is_comparator(tok
)) {
1021 isl_stream_error(s
, tok
, "missing operator");
1023 isl_stream_push_token(s
, tok
);
1028 aff2
= accept_affine_list(s
, v
);
1032 aff1
= isl_mat_add_zero_cols(aff1
, aff2
->n_col
- aff1
->n_col
);
1035 bmap
= add_lifted_divs(bmap
, v
);
1036 bmap
= isl_basic_map_extend_constraints(bmap
, 0,
1037 aff1
->n_row
* aff2
->n_row
);
1038 for (i
= 0; i
< aff1
->n_row
; ++i
)
1039 for (j
= 0; j
< aff2
->n_row
; ++j
)
1040 bmap
= construct_constraint(bmap
, tok
->type
,
1041 aff1
->row
[i
], aff2
->row
[j
]);
1042 isl_token_free(tok
);
1046 tok
= isl_stream_next_token(s
);
1047 if (!is_comparator(tok
)) {
1049 isl_stream_push_token(s
, tok
);
1058 isl_token_free(tok
);
1061 isl_basic_map_free(bmap
);
1065 /* Return first variable, starting at n, representing a min or max,
1066 * or NULL if there is no such variable.
1068 static struct variable
*first_minmax(struct vars
*v
, int n
)
1070 struct variable
*first
= NULL
;
1071 struct variable
*var
;
1073 for (var
= v
->v
; var
&& var
->pos
>= n
; var
= var
->next
)
1080 /* Check whether the variable at the given position only occurs in
1081 * inequalities and only with the given sign.
1083 static int all_coefficients_of_sign(__isl_keep isl_map
*map
, int pos
, int sign
)
1090 for (i
= 0; i
< map
->n
; ++i
) {
1091 isl_basic_map
*bmap
= map
->p
[i
];
1093 for (j
= 0; j
< bmap
->n_eq
; ++j
)
1094 if (!isl_int_is_zero(bmap
->eq
[j
][1 + pos
]))
1096 for (j
= 0; j
< bmap
->n_ineq
; ++j
) {
1097 int s
= isl_int_sgn(bmap
->ineq
[j
][1 + pos
]);
1108 /* Given a variable m which represents a min or a max of n expressions
1109 * b_i, add the constraints
1113 * in case of a min (var->sign < 0) and m >= b_i in case of a max.
1115 static __isl_give isl_map
*bound_minmax(__isl_take isl_map
*map
,
1116 struct variable
*var
)
1119 isl_basic_map
*bound
;
1122 total
= isl_map_dim(map
, isl_dim_all
);
1123 bound
= isl_basic_map_alloc_dim(isl_map_get_dim(map
),
1124 0, 0, var
->list
->n_row
);
1126 for (i
= 0; i
< var
->list
->n_row
; ++i
) {
1127 k
= isl_basic_map_alloc_inequality(bound
);
1131 isl_seq_cpy(bound
->ineq
[k
], var
->list
->row
[i
],
1134 isl_seq_neg(bound
->ineq
[k
], var
->list
->row
[i
],
1136 isl_int_set_si(bound
->ineq
[k
][1 + var
->pos
], var
->sign
);
1137 isl_seq_clr(bound
->ineq
[k
] + var
->list
->n_col
,
1138 1 + total
- var
->list
->n_col
);
1141 map
= isl_map_intersect(map
, isl_map_from_basic_map(bound
));
1145 isl_basic_map_free(bound
);
1150 /* Given a variable m which represents a min (or max) of n expressions
1151 * b_i, add constraints that assigns the minimal upper bound to m, i.e.,
1152 * divide the space into cells where one
1153 * of the upper bounds is smaller than all the others and assign
1154 * this upper bound to m.
1156 * In particular, if there are n bounds b_i, then the input map
1157 * is split into n pieces, each with the extra constraints
1160 * b_i <= b_j for j > i
1161 * b_i < b_j for j < i
1163 * in case of a min (var->sign < 0) and similarly in case of a max.
1165 * Note: this function is very similar to set_minimum in isl_tab_pip.c
1166 * Perhaps we should try to merge the two.
1168 static __isl_give isl_map
*set_minmax(__isl_take isl_map
*map
,
1169 struct variable
*var
)
1172 isl_basic_map
*bmap
= NULL
;
1174 isl_map
*split
= NULL
;
1177 ctx
= isl_map_get_ctx(map
);
1178 total
= isl_map_dim(map
, isl_dim_all
);
1179 split
= isl_map_alloc_dim(isl_map_get_dim(map
),
1180 var
->list
->n_row
, ISL_SET_DISJOINT
);
1182 for (i
= 0; i
< var
->list
->n_row
; ++i
) {
1183 bmap
= isl_basic_map_alloc_dim(isl_map_get_dim(map
), 0,
1184 1, var
->list
->n_row
- 1);
1185 k
= isl_basic_map_alloc_equality(bmap
);
1188 isl_seq_cpy(bmap
->eq
[k
], var
->list
->row
[i
], var
->list
->n_col
);
1189 isl_int_set_si(bmap
->eq
[k
][1 + var
->pos
], -1);
1190 for (j
= 0; j
< var
->list
->n_row
; ++j
) {
1193 k
= isl_basic_map_alloc_inequality(bmap
);
1197 isl_seq_combine(bmap
->ineq
[k
],
1198 ctx
->one
, var
->list
->row
[j
],
1199 ctx
->negone
, var
->list
->row
[i
],
1202 isl_seq_combine(bmap
->ineq
[k
],
1203 ctx
->negone
, var
->list
->row
[j
],
1204 ctx
->one
, var
->list
->row
[i
],
1206 isl_seq_clr(bmap
->ineq
[k
] + var
->list
->n_col
,
1207 1 + total
- var
->list
->n_col
);
1209 isl_int_sub_ui(bmap
->ineq
[k
][0],
1210 bmap
->ineq
[k
][0], 1);
1212 bmap
= isl_basic_map_finalize(bmap
);
1213 split
= isl_map_add_basic_map(split
, bmap
);
1216 map
= isl_map_intersect(map
, split
);
1220 isl_basic_map_free(bmap
);
1221 isl_map_free(split
);
1226 /* Plug in the definitions of all min and max expressions.
1227 * If a min expression only appears in inequalities and only
1228 * with a positive coefficient, then we can simply bound
1229 * the variable representing the min by its defining terms
1230 * and similarly for a max expression.
1231 * Otherwise, we have to assign the different terms to the
1232 * variable under the condition that the assigned term is smaller
1233 * than the other terms.
1235 static __isl_give isl_map
*add_minmax(__isl_take isl_map
*map
,
1236 struct vars
*v
, int n
)
1238 struct variable
*var
;
1241 var
= first_minmax(v
, n
);
1244 if (all_coefficients_of_sign(map
, var
->pos
, -var
->sign
))
1245 map
= bound_minmax(map
, var
);
1247 map
= set_minmax(map
, var
);
1254 static isl_map
*read_constraint(struct isl_stream
*s
,
1255 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1264 bmap
= isl_basic_set_unwrap(isl_basic_set_lift(isl_basic_map_wrap(bmap
)));
1265 total
= isl_basic_map_total_dim(bmap
);
1266 while (v
->n
< total
)
1267 if (vars_add_anon(v
) < 0)
1270 bmap
= add_constraint(s
, v
, bmap
);
1271 bmap
= isl_basic_map_simplify(bmap
);
1272 bmap
= isl_basic_map_finalize(bmap
);
1274 map
= isl_map_from_basic_map(bmap
);
1276 map
= add_minmax(map
, v
, n
);
1278 map
= isl_set_unwrap(isl_map_domain(map
));
1280 vars_drop(v
, v
->n
- n
);
1284 isl_basic_map_free(bmap
);
1288 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1289 struct vars
*v
, __isl_take isl_basic_map
*bmap
);
1291 static __isl_give isl_map
*read_exists(struct isl_stream
*s
,
1292 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1295 int seen_paren
= isl_stream_eat_if_available(s
, '(');
1296 isl_map
*map
= NULL
;
1298 bmap
= isl_basic_map_from_domain(isl_basic_map_wrap(bmap
));
1299 bmap
= read_defined_var_list(s
, v
, bmap
);
1301 if (isl_stream_eat(s
, ':'))
1304 map
= read_disjuncts(s
, v
, bmap
);
1305 map
= isl_set_unwrap(isl_map_domain(map
));
1308 vars_drop(v
, v
->n
- n
);
1309 if (seen_paren
&& isl_stream_eat(s
, ')'))
1314 isl_basic_map_free(bmap
);
1319 static __isl_give isl_map
*read_conjunct(struct isl_stream
*s
,
1320 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1324 if (isl_stream_eat_if_available(s
, '(')) {
1325 map
= read_disjuncts(s
, v
, bmap
);
1326 if (isl_stream_eat(s
, ')'))
1331 if (isl_stream_eat_if_available(s
, ISL_TOKEN_EXISTS
))
1332 return read_exists(s
, v
, bmap
);
1334 if (isl_stream_eat_if_available(s
, ISL_TOKEN_TRUE
))
1335 return isl_map_from_basic_map(bmap
);
1337 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FALSE
)) {
1338 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1339 isl_basic_map_free(bmap
);
1340 return isl_map_empty(dim
);
1343 return read_constraint(s
, v
, bmap
);
1349 static __isl_give isl_map
*read_conjuncts(struct isl_stream
*s
,
1350 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1355 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1356 map
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1359 t
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1360 map
= isl_map_subtract(t
, map
);
1363 while (isl_stream_eat_if_available(s
, ISL_TOKEN_AND
)) {
1366 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1367 map_i
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1369 map
= isl_map_subtract(map
, map_i
);
1371 map
= isl_map_intersect(map
, map_i
);
1374 isl_basic_map_free(bmap
);
1378 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1379 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1381 struct isl_map
*map
;
1383 if (isl_stream_next_token_is(s
, '}')) {
1384 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1385 isl_basic_map_free(bmap
);
1386 return isl_map_universe(dim
);
1389 map
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1390 while (isl_stream_eat_if_available(s
, ISL_TOKEN_OR
)) {
1393 map_i
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1394 map
= isl_map_union(map
, map_i
);
1397 isl_basic_map_free(bmap
);
1401 static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map
*bmap
, int pos
)
1403 if (pos
< isl_basic_map_dim(bmap
, isl_dim_out
))
1404 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1405 isl_basic_map_dim(bmap
, isl_dim_in
) + pos
;
1406 pos
-= isl_basic_map_dim(bmap
, isl_dim_out
);
1408 if (pos
< isl_basic_map_dim(bmap
, isl_dim_in
))
1409 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) + pos
;
1410 pos
-= isl_basic_map_dim(bmap
, isl_dim_in
);
1412 if (pos
< isl_basic_map_dim(bmap
, isl_dim_div
))
1413 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1414 isl_basic_map_dim(bmap
, isl_dim_in
) +
1415 isl_basic_map_dim(bmap
, isl_dim_out
) + pos
;
1416 pos
-= isl_basic_map_dim(bmap
, isl_dim_div
);
1418 if (pos
< isl_basic_map_dim(bmap
, isl_dim_param
))
1424 static __isl_give isl_basic_map
*basic_map_read_polylib_constraint(
1425 struct isl_stream
*s
, __isl_take isl_basic_map
*bmap
)
1428 struct isl_token
*tok
;
1438 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
1439 dim
= isl_basic_map_dim(bmap
, isl_dim_out
);
1441 tok
= isl_stream_next_token(s
);
1442 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1443 isl_stream_error(s
, tok
, "expecting coefficient");
1445 isl_stream_push_token(s
, tok
);
1448 if (!tok
->on_new_line
) {
1449 isl_stream_error(s
, tok
, "coefficient should appear on new line");
1450 isl_stream_push_token(s
, tok
);
1454 type
= isl_int_get_si(tok
->u
.v
);
1455 isl_token_free(tok
);
1457 isl_assert(s
->ctx
, type
== 0 || type
== 1, goto error
);
1459 k
= isl_basic_map_alloc_equality(bmap
);
1462 k
= isl_basic_map_alloc_inequality(bmap
);
1468 for (j
= 0; j
< 1 + isl_basic_map_total_dim(bmap
); ++j
) {
1470 tok
= isl_stream_next_token(s
);
1471 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1472 isl_stream_error(s
, tok
, "expecting coefficient");
1474 isl_stream_push_token(s
, tok
);
1477 if (tok
->on_new_line
) {
1478 isl_stream_error(s
, tok
,
1479 "coefficient should not appear on new line");
1480 isl_stream_push_token(s
, tok
);
1483 pos
= polylib_pos_to_isl_pos(bmap
, j
);
1484 isl_int_set(c
[pos
], tok
->u
.v
);
1485 isl_token_free(tok
);
1490 isl_basic_map_free(bmap
);
1494 static __isl_give isl_basic_map
*basic_map_read_polylib(struct isl_stream
*s
,
1498 struct isl_token
*tok
;
1499 struct isl_token
*tok2
;
1502 unsigned in
= 0, out
, local
= 0;
1503 struct isl_basic_map
*bmap
= NULL
;
1508 tok
= isl_stream_next_token(s
);
1510 isl_stream_error(s
, NULL
, "unexpected EOF");
1513 tok2
= isl_stream_next_token(s
);
1515 isl_token_free(tok
);
1516 isl_stream_error(s
, NULL
, "unexpected EOF");
1519 if (tok
->type
!= ISL_TOKEN_VALUE
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1520 isl_stream_push_token(s
, tok2
);
1521 isl_stream_push_token(s
, tok
);
1522 isl_stream_error(s
, NULL
,
1523 "expecting constraint matrix dimensions");
1526 n_row
= isl_int_get_si(tok
->u
.v
);
1527 n_col
= isl_int_get_si(tok2
->u
.v
);
1528 on_new_line
= tok2
->on_new_line
;
1529 isl_token_free(tok2
);
1530 isl_token_free(tok
);
1531 isl_assert(s
->ctx
, !on_new_line
, return NULL
);
1532 isl_assert(s
->ctx
, n_row
>= 0, return NULL
);
1533 isl_assert(s
->ctx
, n_col
>= 2 + nparam
, return NULL
);
1534 tok
= isl_stream_next_token_on_same_line(s
);
1536 if (tok
->type
!= ISL_TOKEN_VALUE
) {
1537 isl_stream_error(s
, tok
,
1538 "expecting number of output dimensions");
1539 isl_stream_push_token(s
, tok
);
1542 out
= isl_int_get_si(tok
->u
.v
);
1543 isl_token_free(tok
);
1545 tok
= isl_stream_next_token_on_same_line(s
);
1546 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1547 isl_stream_error(s
, tok
,
1548 "expecting number of input dimensions");
1550 isl_stream_push_token(s
, tok
);
1553 in
= isl_int_get_si(tok
->u
.v
);
1554 isl_token_free(tok
);
1556 tok
= isl_stream_next_token_on_same_line(s
);
1557 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1558 isl_stream_error(s
, tok
,
1559 "expecting number of existentials");
1561 isl_stream_push_token(s
, tok
);
1564 local
= isl_int_get_si(tok
->u
.v
);
1565 isl_token_free(tok
);
1567 tok
= isl_stream_next_token_on_same_line(s
);
1568 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1569 isl_stream_error(s
, tok
,
1570 "expecting number of parameters");
1572 isl_stream_push_token(s
, tok
);
1575 nparam
= isl_int_get_si(tok
->u
.v
);
1576 isl_token_free(tok
);
1577 if (n_col
!= 1 + out
+ in
+ local
+ nparam
+ 1) {
1578 isl_stream_error(s
, NULL
,
1579 "dimensions don't match");
1583 out
= n_col
- 2 - nparam
;
1584 bmap
= isl_basic_map_alloc(s
->ctx
, nparam
, in
, out
, local
, n_row
, n_row
);
1588 for (i
= 0; i
< local
; ++i
) {
1589 int k
= isl_basic_map_alloc_div(bmap
);
1592 isl_seq_clr(bmap
->div
[k
], 1 + 1 + nparam
+ in
+ out
+ local
);
1595 for (i
= 0; i
< n_row
; ++i
)
1596 bmap
= basic_map_read_polylib_constraint(s
, bmap
);
1598 tok
= isl_stream_next_token_on_same_line(s
);
1600 isl_stream_error(s
, tok
, "unexpected extra token on line");
1601 isl_stream_push_token(s
, tok
);
1605 bmap
= isl_basic_map_simplify(bmap
);
1606 bmap
= isl_basic_map_finalize(bmap
);
1609 isl_basic_map_free(bmap
);
1613 static struct isl_map
*map_read_polylib(struct isl_stream
*s
, int nparam
)
1615 struct isl_token
*tok
;
1616 struct isl_token
*tok2
;
1618 struct isl_map
*map
;
1620 tok
= isl_stream_next_token(s
);
1622 isl_stream_error(s
, NULL
, "unexpected EOF");
1625 tok2
= isl_stream_next_token_on_same_line(s
);
1626 if (tok2
&& tok2
->type
== ISL_TOKEN_VALUE
) {
1627 isl_stream_push_token(s
, tok2
);
1628 isl_stream_push_token(s
, tok
);
1629 return isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1632 isl_stream_error(s
, tok2
, "unexpected token");
1633 isl_stream_push_token(s
, tok2
);
1634 isl_stream_push_token(s
, tok
);
1637 n
= isl_int_get_si(tok
->u
.v
);
1638 isl_token_free(tok
);
1640 isl_assert(s
->ctx
, n
>= 1, return NULL
);
1642 map
= isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1644 for (i
= 1; map
&& i
< n
; ++i
)
1645 map
= isl_map_union(map
,
1646 isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
)));
1651 static int optional_power(struct isl_stream
*s
)
1654 struct isl_token
*tok
;
1656 tok
= isl_stream_next_token(s
);
1659 if (tok
->type
!= '^') {
1660 isl_stream_push_token(s
, tok
);
1663 isl_token_free(tok
);
1664 tok
= isl_stream_next_token(s
);
1665 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1666 isl_stream_error(s
, tok
, "expecting exponent");
1668 isl_stream_push_token(s
, tok
);
1671 pow
= isl_int_get_si(tok
->u
.v
);
1672 isl_token_free(tok
);
1676 static __isl_give isl_div
*read_div(struct isl_stream
*s
,
1677 __isl_take isl_dim
*dim
, struct vars
*v
)
1680 isl_basic_map
*bmap
;
1683 bmap
= isl_basic_map_universe(dim
);
1685 if (vars_add_anon(v
) < 0)
1687 if (read_div_definition(s
, v
) < 0)
1689 bmap
= add_divs(bmap
, v
);
1690 bmap
= isl_basic_map_order_divs(bmap
);
1693 vars_drop(v
, v
->n
- n
);
1695 return isl_basic_map_div(bmap
, bmap
->n_div
- 1);
1697 isl_basic_map_free(bmap
);
1701 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1702 __isl_keep isl_basic_map
*bmap
, struct vars
*v
);
1704 static __isl_give isl_qpolynomial
*read_factor(struct isl_stream
*s
,
1705 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1707 struct isl_qpolynomial
*qp
;
1708 struct isl_token
*tok
;
1710 tok
= next_token(s
);
1712 isl_stream_error(s
, NULL
, "unexpected EOF");
1715 if (tok
->type
== '(') {
1718 isl_token_free(tok
);
1719 qp
= read_term(s
, bmap
, v
);
1722 if (isl_stream_eat(s
, ')'))
1724 pow
= optional_power(s
);
1725 qp
= isl_qpolynomial_pow(qp
, pow
);
1726 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
1727 struct isl_token
*tok2
;
1728 tok2
= isl_stream_next_token(s
);
1729 if (tok2
&& tok2
->type
== '/') {
1730 isl_token_free(tok2
);
1731 tok2
= next_token(s
);
1732 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1733 isl_stream_error(s
, tok2
, "expected denominator");
1734 isl_token_free(tok
);
1735 isl_token_free(tok2
);
1738 qp
= isl_qpolynomial_rat_cst(isl_basic_map_get_dim(bmap
),
1739 tok
->u
.v
, tok2
->u
.v
);
1740 isl_token_free(tok2
);
1742 isl_stream_push_token(s
, tok2
);
1743 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1746 isl_token_free(tok
);
1747 } else if (tok
->type
== ISL_TOKEN_INFTY
) {
1748 isl_token_free(tok
);
1749 qp
= isl_qpolynomial_infty(isl_basic_map_get_dim(bmap
));
1750 } else if (tok
->type
== ISL_TOKEN_NAN
) {
1751 isl_token_free(tok
);
1752 qp
= isl_qpolynomial_nan(isl_basic_map_get_dim(bmap
));
1753 } else if (tok
->type
== ISL_TOKEN_IDENT
) {
1755 int pos
= vars_pos(v
, tok
->u
.s
, -1);
1758 isl_token_free(tok
);
1762 vars_drop(v
, v
->n
- n
);
1763 isl_stream_error(s
, tok
, "unknown identifier");
1764 isl_token_free(tok
);
1767 isl_token_free(tok
);
1768 pow
= optional_power(s
);
1769 qp
= isl_qpolynomial_var_pow(isl_basic_map_get_dim(bmap
), pos
, pow
);
1770 } else if (tok
->type
== '[') {
1774 isl_stream_push_token(s
, tok
);
1775 div
= read_div(s
, isl_basic_map_get_dim(bmap
), v
);
1776 pow
= optional_power(s
);
1777 qp
= isl_qpolynomial_div_pow(div
, pow
);
1778 } else if (tok
->type
== '-') {
1779 struct isl_qpolynomial
*qp2
;
1781 isl_token_free(tok
);
1782 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1784 qp2
= read_factor(s
, bmap
, v
);
1785 qp
= isl_qpolynomial_mul(qp
, qp2
);
1787 isl_stream_error(s
, tok
, "unexpected isl_token");
1788 isl_stream_push_token(s
, tok
);
1792 if (isl_stream_eat_if_available(s
, '*') ||
1793 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
1794 struct isl_qpolynomial
*qp2
;
1796 qp2
= read_factor(s
, bmap
, v
);
1797 qp
= isl_qpolynomial_mul(qp
, qp2
);
1802 isl_qpolynomial_free(qp
);
1806 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1807 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1809 struct isl_token
*tok
;
1810 struct isl_qpolynomial
*qp
;
1812 qp
= read_factor(s
, bmap
, v
);
1815 tok
= next_token(s
);
1819 if (tok
->type
== '+') {
1820 struct isl_qpolynomial
*qp2
;
1822 isl_token_free(tok
);
1823 qp2
= read_factor(s
, bmap
, v
);
1824 qp
= isl_qpolynomial_add(qp
, qp2
);
1825 } else if (tok
->type
== '-') {
1826 struct isl_qpolynomial
*qp2
;
1828 isl_token_free(tok
);
1829 qp2
= read_factor(s
, bmap
, v
);
1830 qp
= isl_qpolynomial_sub(qp
, qp2
);
1831 } else if (tok
->type
== ISL_TOKEN_VALUE
&&
1832 isl_int_is_neg(tok
->u
.v
)) {
1833 struct isl_qpolynomial
*qp2
;
1835 isl_stream_push_token(s
, tok
);
1836 qp2
= read_factor(s
, bmap
, v
);
1837 qp
= isl_qpolynomial_add(qp
, qp2
);
1839 isl_stream_push_token(s
, tok
);
1847 static __isl_give isl_map
*read_optional_disjuncts(struct isl_stream
*s
,
1848 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1850 struct isl_token
*tok
;
1851 struct isl_map
*map
;
1853 tok
= isl_stream_next_token(s
);
1855 isl_stream_error(s
, NULL
, "unexpected EOF");
1858 map
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1859 if (tok
->type
== ':' ||
1860 (tok
->type
== ISL_TOKEN_OR
&& !strcmp(tok
->u
.s
, "|"))) {
1861 isl_token_free(tok
);
1862 map
= isl_map_intersect(map
,
1863 read_disjuncts(s
, v
, isl_basic_map_copy(bmap
)));
1865 isl_stream_push_token(s
, tok
);
1867 isl_basic_map_free(bmap
);
1871 isl_basic_map_free(bmap
);
1875 static struct isl_obj
obj_read_poly(struct isl_stream
*s
,
1876 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1878 struct isl_obj obj
= { isl_obj_pw_qpolynomial
, NULL
};
1879 struct isl_pw_qpolynomial
*pwqp
;
1880 struct isl_qpolynomial
*qp
;
1881 struct isl_map
*map
;
1882 struct isl_set
*set
;
1884 qp
= read_term(s
, bmap
, v
);
1885 map
= read_optional_disjuncts(s
, bmap
, v
);
1886 set
= isl_map_range(map
);
1888 pwqp
= isl_pw_qpolynomial_alloc(set
, qp
);
1890 vars_drop(v
, v
->n
- n
);
1896 static struct isl_obj
obj_read_poly_or_fold(struct isl_stream
*s
,
1897 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1899 struct isl_obj obj
= { isl_obj_pw_qpolynomial_fold
, NULL
};
1900 isl_qpolynomial
*qp
;
1901 isl_qpolynomial_fold
*fold
= NULL
;
1902 isl_pw_qpolynomial_fold
*pwf
;
1906 if (!isl_stream_eat_if_available(s
, ISL_TOKEN_MAX
))
1907 return obj_read_poly(s
, bmap
, v
, n
);
1909 if (isl_stream_eat(s
, '('))
1912 qp
= read_term(s
, bmap
, v
);
1913 fold
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1915 while (isl_stream_eat_if_available(s
, ',')) {
1916 isl_qpolynomial_fold
*fold_i
;
1917 qp
= read_term(s
, bmap
, v
);
1918 fold_i
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1919 fold
= isl_qpolynomial_fold_fold(fold
, fold_i
);
1922 if (isl_stream_eat(s
, ')'))
1925 map
= read_optional_disjuncts(s
, bmap
, v
);
1926 set
= isl_map_range(map
);
1927 pwf
= isl_pw_qpolynomial_fold_alloc(isl_fold_max
, set
, fold
);
1929 vars_drop(v
, v
->n
- n
);
1934 isl_basic_map_free(bmap
);
1935 isl_qpolynomial_fold_free(fold
);
1936 obj
.type
= isl_obj_none
;
1940 static int is_rational(struct isl_stream
*s
)
1942 struct isl_token
*tok
;
1944 tok
= isl_stream_next_token(s
);
1947 if (tok
->type
== ISL_TOKEN_RAT
&& isl_stream_next_token_is(s
, ':')) {
1948 isl_token_free(tok
);
1949 isl_stream_eat(s
, ':');
1953 isl_stream_push_token(s
, tok
);
1958 static struct isl_obj
obj_read_body(struct isl_stream
*s
,
1959 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1961 struct isl_map
*map
= NULL
;
1962 struct isl_token
*tok
;
1963 struct isl_obj obj
= { isl_obj_set
, NULL
};
1967 bmap
= isl_basic_map_set_rational(bmap
);
1969 if (!next_is_tuple(s
))
1970 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1972 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
1975 tok
= isl_stream_next_token(s
);
1976 if (tok
&& tok
->type
== ISL_TOKEN_TO
) {
1977 obj
.type
= isl_obj_map
;
1978 isl_token_free(tok
);
1979 if (!next_is_tuple(s
)) {
1980 bmap
= isl_basic_map_reverse(bmap
);
1981 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1983 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
1987 bmap
= isl_basic_map_reverse(bmap
);
1989 isl_stream_push_token(s
, tok
);
1992 map
= read_optional_disjuncts(s
, bmap
, v
);
1994 vars_drop(v
, v
->n
- n
);
1999 isl_basic_map_free(bmap
);
2000 obj
.type
= isl_obj_none
;
2004 static struct isl_obj
to_union(isl_ctx
*ctx
, struct isl_obj obj
)
2006 if (obj
.type
== isl_obj_map
) {
2007 obj
.v
= isl_union_map_from_map(obj
.v
);
2008 obj
.type
= isl_obj_union_map
;
2009 } else if (obj
.type
== isl_obj_set
) {
2010 obj
.v
= isl_union_set_from_set(obj
.v
);
2011 obj
.type
= isl_obj_union_set
;
2012 } else if (obj
.type
== isl_obj_pw_qpolynomial
) {
2013 obj
.v
= isl_union_pw_qpolynomial_from_pw_qpolynomial(obj
.v
);
2014 obj
.type
= isl_obj_union_pw_qpolynomial
;
2015 } else if (obj
.type
== isl_obj_pw_qpolynomial_fold
) {
2016 obj
.v
= isl_union_pw_qpolynomial_fold_from_pw_qpolynomial_fold(obj
.v
);
2017 obj
.type
= isl_obj_union_pw_qpolynomial_fold
;
2019 isl_assert(ctx
, 0, goto error
);
2022 obj
.type
->free(obj
.v
);
2023 obj
.type
= isl_obj_none
;
2027 static struct isl_obj
obj_add(struct isl_ctx
*ctx
,
2028 struct isl_obj obj1
, struct isl_obj obj2
)
2030 if (obj1
.type
== isl_obj_set
&& obj2
.type
== isl_obj_union_set
)
2031 obj1
= to_union(ctx
, obj1
);
2032 if (obj1
.type
== isl_obj_union_set
&& obj2
.type
== isl_obj_set
)
2033 obj2
= to_union(ctx
, obj2
);
2034 if (obj1
.type
== isl_obj_map
&& obj2
.type
== isl_obj_union_map
)
2035 obj1
= to_union(ctx
, obj1
);
2036 if (obj1
.type
== isl_obj_union_map
&& obj2
.type
== isl_obj_map
)
2037 obj2
= to_union(ctx
, obj2
);
2038 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2039 obj2
.type
== isl_obj_union_pw_qpolynomial
)
2040 obj1
= to_union(ctx
, obj1
);
2041 if (obj1
.type
== isl_obj_union_pw_qpolynomial
&&
2042 obj2
.type
== isl_obj_pw_qpolynomial
)
2043 obj2
= to_union(ctx
, obj2
);
2044 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2045 obj2
.type
== isl_obj_union_pw_qpolynomial_fold
)
2046 obj1
= to_union(ctx
, obj1
);
2047 if (obj1
.type
== isl_obj_union_pw_qpolynomial_fold
&&
2048 obj2
.type
== isl_obj_pw_qpolynomial_fold
)
2049 obj2
= to_union(ctx
, obj2
);
2050 isl_assert(ctx
, obj1
.type
== obj2
.type
, goto error
);
2051 if (obj1
.type
== isl_obj_map
&& !isl_map_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_set
&& !isl_set_has_equal_dim(obj1
.v
, obj2
.v
)) {
2056 obj1
= to_union(ctx
, obj1
);
2057 obj2
= to_union(ctx
, obj2
);
2059 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2060 !isl_pw_qpolynomial_has_equal_dim(obj1
.v
, obj2
.v
)) {
2061 obj1
= to_union(ctx
, obj1
);
2062 obj2
= to_union(ctx
, obj2
);
2064 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2065 !isl_pw_qpolynomial_fold_has_equal_dim(obj1
.v
, obj2
.v
)) {
2066 obj1
= to_union(ctx
, obj1
);
2067 obj2
= to_union(ctx
, obj2
);
2069 obj1
.v
= obj1
.type
->add(obj1
.v
, obj2
.v
);
2072 obj1
.type
->free(obj1
.v
);
2073 obj2
.type
->free(obj2
.v
);
2074 obj1
.type
= isl_obj_none
;
2079 static struct isl_obj
obj_read(struct isl_stream
*s
, int nparam
)
2081 isl_basic_map
*bmap
= NULL
;
2082 struct isl_token
*tok
;
2083 struct vars
*v
= NULL
;
2084 struct isl_obj obj
= { isl_obj_set
, NULL
};
2086 tok
= next_token(s
);
2088 isl_stream_error(s
, NULL
, "unexpected EOF");
2091 if (tok
->type
== ISL_TOKEN_VALUE
) {
2092 struct isl_token
*tok2
;
2093 struct isl_map
*map
;
2095 tok2
= isl_stream_next_token(s
);
2096 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
||
2097 isl_int_is_neg(tok2
->u
.v
)) {
2099 isl_stream_push_token(s
, tok2
);
2100 obj
.type
= isl_obj_int
;
2101 obj
.v
= isl_int_obj_alloc(s
->ctx
, tok
->u
.v
);
2102 isl_token_free(tok
);
2105 isl_stream_push_token(s
, tok2
);
2106 isl_stream_push_token(s
, tok
);
2107 map
= map_read_polylib(s
, nparam
);
2110 if (isl_map_dim(map
, isl_dim_in
) > 0)
2111 obj
.type
= isl_obj_map
;
2115 v
= vars_new(s
->ctx
);
2117 isl_stream_push_token(s
, tok
);
2120 bmap
= isl_basic_map_alloc(s
->ctx
, 0, 0, 0, 0, 0, 0);
2121 if (tok
->type
== '[') {
2122 isl_stream_push_token(s
, tok
);
2123 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2127 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2128 tok
= isl_stream_next_token(s
);
2129 if (!tok
|| tok
->type
!= ISL_TOKEN_TO
) {
2130 isl_stream_error(s
, tok
, "expecting '->'");
2132 isl_stream_push_token(s
, tok
);
2135 isl_token_free(tok
);
2136 tok
= isl_stream_next_token(s
);
2137 } else if (nparam
> 0)
2138 bmap
= isl_basic_map_add(bmap
, isl_dim_param
, nparam
);
2139 if (!tok
|| tok
->type
!= '{') {
2140 isl_stream_error(s
, tok
, "expecting '{'");
2142 isl_stream_push_token(s
, tok
);
2145 isl_token_free(tok
);
2147 tok
= isl_stream_next_token(s
);
2150 else if (tok
->type
== ISL_TOKEN_IDENT
&& !strcmp(tok
->u
.s
, "Sym")) {
2151 isl_token_free(tok
);
2152 if (isl_stream_eat(s
, '='))
2154 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2158 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2159 } else if (tok
->type
== '}') {
2160 obj
.type
= isl_obj_union_set
;
2161 obj
.v
= isl_union_set_empty(isl_basic_map_get_dim(bmap
));
2162 isl_token_free(tok
);
2165 isl_stream_push_token(s
, tok
);
2170 o
= obj_read_body(s
, isl_basic_map_copy(bmap
), v
);
2171 if (o
.type
== isl_obj_none
|| !o
.v
)
2176 obj
= obj_add(s
->ctx
, obj
, o
);
2177 if (obj
.type
== isl_obj_none
|| !obj
.v
)
2180 tok
= isl_stream_next_token(s
);
2181 if (!tok
|| tok
->type
!= ';')
2183 isl_token_free(tok
);
2184 if (isl_stream_next_token_is(s
, '}')) {
2185 tok
= isl_stream_next_token(s
);
2190 if (tok
&& tok
->type
== '}') {
2191 isl_token_free(tok
);
2193 isl_stream_error(s
, tok
, "unexpected isl_token");
2195 isl_token_free(tok
);
2200 isl_basic_map_free(bmap
);
2204 isl_basic_map_free(bmap
);
2205 obj
.type
->free(obj
.v
);
2212 struct isl_obj
isl_stream_read_obj(struct isl_stream
*s
)
2214 return obj_read(s
, -1);
2217 __isl_give isl_map
*isl_stream_read_map(struct isl_stream
*s
, int nparam
)
2221 obj
= obj_read(s
, nparam
);
2223 isl_assert(s
->ctx
, obj
.type
== isl_obj_map
||
2224 obj
.type
== isl_obj_set
, goto error
);
2228 obj
.type
->free(obj
.v
);
2232 __isl_give isl_set
*isl_stream_read_set(struct isl_stream
*s
, int nparam
)
2236 obj
= obj_read(s
, nparam
);
2238 isl_assert(s
->ctx
, obj
.type
== isl_obj_set
, goto error
);
2242 obj
.type
->free(obj
.v
);
2246 __isl_give isl_union_map
*isl_stream_read_union_map(struct isl_stream
*s
)
2250 obj
= obj_read(s
, -1);
2251 if (obj
.type
== isl_obj_map
) {
2252 obj
.type
= isl_obj_union_map
;
2253 obj
.v
= isl_union_map_from_map(obj
.v
);
2255 if (obj
.type
== isl_obj_set
) {
2256 obj
.type
= isl_obj_union_set
;
2257 obj
.v
= isl_union_set_from_set(obj
.v
);
2260 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_map
||
2261 obj
.type
== isl_obj_union_set
, goto error
);
2265 obj
.type
->free(obj
.v
);
2269 __isl_give isl_union_set
*isl_stream_read_union_set(struct isl_stream
*s
)
2273 obj
= obj_read(s
, -1);
2274 if (obj
.type
== isl_obj_set
) {
2275 obj
.type
= isl_obj_union_set
;
2276 obj
.v
= isl_union_set_from_set(obj
.v
);
2279 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_set
, goto error
);
2283 obj
.type
->free(obj
.v
);
2287 static struct isl_basic_map
*basic_map_read(struct isl_stream
*s
, int nparam
)
2290 struct isl_map
*map
;
2291 struct isl_basic_map
*bmap
;
2293 obj
= obj_read(s
, nparam
);
2298 isl_assert(map
->ctx
, map
->n
<= 1, goto error
);
2301 bmap
= isl_basic_map_empty_like_map(map
);
2303 bmap
= isl_basic_map_copy(map
->p
[0]);
2313 __isl_give isl_basic_map
*isl_basic_map_read_from_file(isl_ctx
*ctx
,
2314 FILE *input
, int nparam
)
2316 struct isl_basic_map
*bmap
;
2317 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2320 bmap
= basic_map_read(s
, nparam
);
2325 __isl_give isl_basic_set
*isl_basic_set_read_from_file(isl_ctx
*ctx
,
2326 FILE *input
, int nparam
)
2328 struct isl_basic_map
*bmap
;
2329 bmap
= isl_basic_map_read_from_file(ctx
, input
, nparam
);
2332 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2333 return (struct isl_basic_set
*)bmap
;
2335 isl_basic_map_free(bmap
);
2339 struct isl_basic_map
*isl_basic_map_read_from_str(struct isl_ctx
*ctx
,
2340 const char *str
, int nparam
)
2342 struct isl_basic_map
*bmap
;
2343 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2346 bmap
= basic_map_read(s
, nparam
);
2351 struct isl_basic_set
*isl_basic_set_read_from_str(struct isl_ctx
*ctx
,
2352 const char *str
, int nparam
)
2354 struct isl_basic_map
*bmap
;
2355 bmap
= isl_basic_map_read_from_str(ctx
, str
, nparam
);
2358 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2359 return (struct isl_basic_set
*)bmap
;
2361 isl_basic_map_free(bmap
);
2365 __isl_give isl_map
*isl_map_read_from_file(struct isl_ctx
*ctx
,
2366 FILE *input
, int nparam
)
2368 struct isl_map
*map
;
2369 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2372 map
= isl_stream_read_map(s
, nparam
);
2377 __isl_give isl_map
*isl_map_read_from_str(struct isl_ctx
*ctx
,
2378 const char *str
, int nparam
)
2380 struct isl_map
*map
;
2381 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2384 map
= isl_stream_read_map(s
, nparam
);
2389 __isl_give isl_set
*isl_set_read_from_file(struct isl_ctx
*ctx
,
2390 FILE *input
, int nparam
)
2392 struct isl_map
*map
;
2393 map
= isl_map_read_from_file(ctx
, input
, nparam
);
2396 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2397 return (struct isl_set
*)map
;
2403 struct isl_set
*isl_set_read_from_str(struct isl_ctx
*ctx
,
2404 const char *str
, int nparam
)
2406 struct isl_map
*map
;
2407 map
= isl_map_read_from_str(ctx
, str
, nparam
);
2410 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2411 return (struct isl_set
*)map
;
2417 __isl_give isl_union_map
*isl_union_map_read_from_file(isl_ctx
*ctx
,
2420 isl_union_map
*umap
;
2421 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2424 umap
= isl_stream_read_union_map(s
);
2429 __isl_give isl_union_map
*isl_union_map_read_from_str(struct isl_ctx
*ctx
,
2432 isl_union_map
*umap
;
2433 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2436 umap
= isl_stream_read_union_map(s
);
2441 __isl_give isl_union_set
*isl_union_set_read_from_file(isl_ctx
*ctx
,
2444 isl_union_set
*uset
;
2445 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2448 uset
= isl_stream_read_union_set(s
);
2453 __isl_give isl_union_set
*isl_union_set_read_from_str(struct isl_ctx
*ctx
,
2456 isl_union_set
*uset
;
2457 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2460 uset
= isl_stream_read_union_set(s
);
2465 static __isl_give isl_vec
*isl_vec_read_polylib(struct isl_stream
*s
)
2467 struct isl_vec
*vec
= NULL
;
2468 struct isl_token
*tok
;
2472 tok
= isl_stream_next_token(s
);
2473 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2474 isl_stream_error(s
, tok
, "expecting vector length");
2478 size
= isl_int_get_si(tok
->u
.v
);
2479 isl_token_free(tok
);
2481 vec
= isl_vec_alloc(s
->ctx
, size
);
2483 for (j
= 0; j
< size
; ++j
) {
2484 tok
= isl_stream_next_token(s
);
2485 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2486 isl_stream_error(s
, tok
, "expecting constant value");
2489 isl_int_set(vec
->el
[j
], tok
->u
.v
);
2490 isl_token_free(tok
);
2495 isl_token_free(tok
);
2500 static __isl_give isl_vec
*vec_read(struct isl_stream
*s
)
2502 return isl_vec_read_polylib(s
);
2505 __isl_give isl_vec
*isl_vec_read_from_file(isl_ctx
*ctx
, FILE *input
)
2508 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2516 __isl_give isl_pw_qpolynomial
*isl_stream_read_pw_qpolynomial(
2517 struct isl_stream
*s
)
2521 obj
= obj_read(s
, -1);
2523 isl_assert(s
->ctx
, obj
.type
== isl_obj_pw_qpolynomial
,
2528 obj
.type
->free(obj
.v
);
2532 __isl_give isl_pw_qpolynomial
*isl_pw_qpolynomial_read_from_str(isl_ctx
*ctx
,
2535 isl_pw_qpolynomial
*pwqp
;
2536 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2539 pwqp
= isl_stream_read_pw_qpolynomial(s
);
2544 __isl_give isl_pw_qpolynomial
*isl_pw_qpolynomial_read_from_file(isl_ctx
*ctx
,
2547 isl_pw_qpolynomial
*pwqp
;
2548 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2551 pwqp
= isl_stream_read_pw_qpolynomial(s
);