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
17 #include <isl_ctx_private.h>
18 #include <isl_map_private.h>
22 #include <isl/stream.h>
24 #include "isl_polynomial_private.h"
25 #include <isl/union_map.h>
26 #include <isl_mat_private.h>
32 /* non-zero if variable represents a min (-1) or a max (1) */
35 struct variable
*next
;
44 static struct vars
*vars_new(struct isl_ctx
*ctx
)
47 v
= isl_alloc_type(ctx
, struct vars
);
56 static void variable_free(struct variable
*var
)
59 struct variable
*next
= var
->next
;
60 isl_mat_free(var
->list
);
61 isl_vec_free(var
->def
);
68 static void vars_free(struct vars
*v
)
76 static void vars_drop(struct vars
*v
, int n
)
87 struct variable
*next
= var
->next
;
88 isl_mat_free(var
->list
);
89 isl_vec_free(var
->def
);
97 static struct variable
*variable_new(struct vars
*v
, const char *name
, int len
,
100 struct variable
*var
;
101 var
= isl_calloc_type(v
->ctx
, struct variable
);
104 var
->name
= strdup(name
);
105 var
->name
[len
] = '\0';
115 static int vars_pos(struct vars
*v
, const char *s
, int len
)
122 for (q
= v
->v
; q
; q
= q
->next
) {
123 if (strncmp(q
->name
, s
, len
) == 0 && q
->name
[len
] == '\0')
130 v
->v
= variable_new(v
, s
, len
, v
->n
);
138 static int vars_add_anon(struct vars
*v
)
140 v
->v
= variable_new(v
, "", 0, v
->n
);
149 static __isl_give isl_basic_map
*set_name(__isl_take isl_basic_map
*bmap
,
150 enum isl_dim_type type
, unsigned pos
, char *name
)
159 prime
= strchr(name
, '\'');
162 bmap
= isl_basic_map_set_dim_name(bmap
, type
, pos
, name
);
169 /* Obtain next token, with some preprocessing.
170 * In particular, evaluate expressions of the form x^y,
171 * with x and y values.
173 static struct isl_token
*next_token(struct isl_stream
*s
)
175 struct isl_token
*tok
, *tok2
;
177 tok
= isl_stream_next_token(s
);
178 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
)
180 if (!isl_stream_eat_if_available(s
, '^'))
182 tok2
= isl_stream_next_token(s
);
183 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
184 isl_stream_error(s
, tok2
, "expecting constant value");
188 isl_int_pow_ui(tok
->u
.v
, tok
->u
.v
, isl_int_get_ui(tok2
->u
.v
));
190 isl_token_free(tok2
);
194 isl_token_free(tok2
);
198 static int accept_cst_factor(struct isl_stream
*s
, isl_int
*f
)
200 struct isl_token
*tok
;
203 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
204 isl_stream_error(s
, tok
, "expecting constant value");
208 isl_int_mul(*f
, *f
, tok
->u
.v
);
212 if (isl_stream_eat_if_available(s
, '*'))
213 return accept_cst_factor(s
, f
);
221 /* Given an affine expression aff, return an affine expression
222 * for aff % d, with d the next token on the stream, which is
223 * assumed to be a constant.
225 * We introduce an integer division q = [aff/d] and the result
226 * is set to aff - d q.
228 static __isl_give isl_vec
*affine_mod(struct isl_stream
*s
,
229 struct vars
*v
, __isl_take isl_vec
*aff
)
231 struct isl_token
*tok
;
232 struct variable
*var
;
236 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
237 isl_stream_error(s
, tok
, "expecting constant value");
241 if (vars_add_anon(v
) < 0)
246 var
->def
= isl_vec_alloc(s
->ctx
, 2 + v
->n
);
249 isl_seq_cpy(var
->def
->el
+ 1, aff
->el
, aff
->size
);
250 isl_int_set_si(var
->def
->el
[1 + aff
->size
], 0);
251 isl_int_set(var
->def
->el
[0], tok
->u
.v
);
253 mod
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
257 isl_seq_cpy(mod
->el
, aff
->el
, aff
->size
);
258 isl_int_neg(mod
->el
[aff
->size
], tok
->u
.v
);
269 static struct isl_vec
*accept_affine(struct isl_stream
*s
, struct vars
*v
);
270 static int read_div_definition(struct isl_stream
*s
, struct vars
*v
);
271 static int read_minmax_definition(struct isl_stream
*s
, struct vars
*v
);
273 static __isl_give isl_vec
*accept_affine_factor(struct isl_stream
*s
,
276 struct isl_token
*tok
= NULL
;
281 isl_stream_error(s
, NULL
, "unexpected EOF");
284 if (tok
->type
== ISL_TOKEN_IDENT
) {
286 int pos
= vars_pos(v
, tok
->u
.s
, -1);
290 isl_stream_error(s
, tok
, "unknown identifier");
294 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
297 isl_seq_clr(aff
->el
, aff
->size
);
298 isl_int_set_si(aff
->el
[1 + pos
], 1);
300 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
301 if (isl_stream_eat_if_available(s
, '*')) {
302 aff
= accept_affine_factor(s
, v
);
303 aff
= isl_vec_scale(aff
, tok
->u
.v
);
305 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
308 isl_seq_clr(aff
->el
, aff
->size
);
309 isl_int_set(aff
->el
[0], tok
->u
.v
);
312 } else if (tok
->type
== '(') {
315 aff
= accept_affine(s
, v
);
318 if (isl_stream_eat(s
, ')'))
320 } else if (tok
->type
== '[' ||
321 tok
->type
== ISL_TOKEN_FLOORD
||
322 tok
->type
== ISL_TOKEN_CEILD
) {
323 int ceil
= tok
->type
== ISL_TOKEN_CEILD
;
324 struct variable
*var
;
325 if (vars_add_anon(v
) < 0)
328 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
331 isl_seq_clr(aff
->el
, aff
->size
);
332 isl_int_set_si(aff
->el
[1 + v
->n
- 1], ceil
? -1 : 1);
333 isl_stream_push_token(s
, tok
);
335 if (read_div_definition(s
, v
) < 0)
338 isl_seq_neg(var
->def
->el
+ 1, var
->def
->el
+ 1,
340 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
341 } else if (tok
->type
== ISL_TOKEN_MIN
|| tok
->type
== ISL_TOKEN_MAX
) {
342 if (vars_add_anon(v
) < 0)
344 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
347 isl_seq_clr(aff
->el
, aff
->size
);
348 isl_int_set_si(aff
->el
[1 + v
->n
- 1], 1);
349 isl_stream_push_token(s
, tok
);
351 if (read_minmax_definition(s
, v
) < 0)
353 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
355 isl_stream_error(s
, tok
, "expecting factor");
358 if (isl_stream_eat_if_available(s
, '%'))
359 return affine_mod(s
, v
, aff
);
360 if (isl_stream_eat_if_available(s
, '*')) {
363 isl_int_set_si(f
, 1);
364 if (accept_cst_factor(s
, &f
) < 0) {
368 aff
= isl_vec_scale(aff
, f
);
380 static struct isl_vec
*accept_affine(struct isl_stream
*s
, struct vars
*v
)
382 struct isl_token
*tok
= NULL
;
386 aff
= isl_vec_alloc(v
->ctx
, 1 + v
->n
);
389 isl_seq_clr(aff
->el
, aff
->size
);
394 isl_stream_error(s
, NULL
, "unexpected EOF");
397 if (tok
->type
== '-') {
402 if (tok
->type
== '(' || tok
->type
== '[' ||
403 tok
->type
== ISL_TOKEN_MIN
|| tok
->type
== ISL_TOKEN_MAX
||
404 tok
->type
== ISL_TOKEN_FLOORD
||
405 tok
->type
== ISL_TOKEN_CEILD
||
406 tok
->type
== ISL_TOKEN_IDENT
) {
408 isl_stream_push_token(s
, tok
);
410 aff2
= accept_affine_factor(s
, v
);
412 aff2
= isl_vec_scale(aff2
, s
->ctx
->negone
);
413 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
414 aff
= isl_vec_add(aff
, aff2
);
418 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
420 isl_int_neg(tok
->u
.v
, tok
->u
.v
);
421 if (isl_stream_eat_if_available(s
, '*') ||
422 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
424 aff2
= accept_affine_factor(s
, v
);
425 aff2
= isl_vec_scale(aff2
, tok
->u
.v
);
426 aff
= isl_vec_zero_extend(aff
, 1 + v
->n
);
427 aff
= isl_vec_add(aff
, aff2
);
431 isl_int_add(aff
->el
[0], aff
->el
[0], tok
->u
.v
);
435 isl_stream_error(s
, tok
, "unexpected isl_token");
436 isl_stream_push_token(s
, tok
);
443 if (tok
&& tok
->type
== '-') {
446 } else if (tok
&& tok
->type
== '+') {
449 } else if (tok
&& tok
->type
== ISL_TOKEN_VALUE
&&
450 isl_int_is_neg(tok
->u
.v
)) {
451 isl_stream_push_token(s
, tok
);
454 isl_stream_push_token(s
, tok
);
466 /* Add any variables in the variable list "v" that are not already in "bmap"
467 * as existentially quantified variables in "bmap".
469 static __isl_give isl_basic_map
*add_divs(__isl_take isl_basic_map
*bmap
,
474 struct variable
*var
;
476 extra
= v
->n
- isl_basic_map_total_dim(bmap
);
481 bmap
= isl_basic_map_extend_dim(bmap
, isl_basic_map_get_dim(bmap
),
482 extra
, 0, 2 * extra
);
484 for (i
= 0; i
< extra
; ++i
)
485 if (isl_basic_map_alloc_div(bmap
) < 0)
488 for (i
= 0, var
= v
->v
; i
< extra
; ++i
, var
= var
->next
) {
489 int k
= bmap
->n_div
- 1 - i
;
491 isl_seq_cpy(bmap
->div
[k
], var
->def
->el
, var
->def
->size
);
492 isl_seq_clr(bmap
->div
[k
] + var
->def
->size
,
493 2 + v
->n
- var
->def
->size
);
495 if (isl_basic_map_add_div_constraints(bmap
, k
) < 0)
501 isl_basic_map_free(bmap
);
505 static __isl_give isl_basic_map
*read_var_def(struct isl_stream
*s
,
506 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
509 isl_basic_map
*def
= NULL
;
514 if (vars_add_anon(v
) < 0)
518 vec
= accept_affine(s
, v
);
522 dim
= isl_basic_map_get_dim(bmap
);
523 def
= isl_basic_map_universe(dim
);
524 def
= add_divs(def
, v
);
525 def
= isl_basic_map_extend_constraints(def
, 1, 0);
526 k
= isl_basic_map_alloc_equality(def
);
528 isl_seq_cpy(def
->eq
[k
], vec
->el
, vec
->size
);
529 isl_int_set_si(def
->eq
[k
][1 + n
- 1], -1);
535 vars_drop(v
, v
->n
- n
);
537 def
= isl_basic_map_simplify(def
);
538 def
= isl_basic_map_finalize(def
);
539 bmap
= isl_basic_map_intersect(bmap
, def
);
542 isl_basic_map_free(bmap
);
543 isl_basic_map_free(def
);
547 static __isl_give isl_basic_map
*read_var_list(struct isl_stream
*s
,
548 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
551 struct isl_token
*tok
;
553 while ((tok
= next_token(s
)) != NULL
) {
556 if (tok
->type
== ISL_TOKEN_IDENT
) {
558 int p
= vars_pos(v
, tok
->u
.s
, -1);
565 bmap
= isl_basic_map_add(bmap
, type
, 1);
566 bmap
= set_name(bmap
, type
, i
, v
->v
->name
);
568 } else if (tok
->type
== ISL_TOKEN_IDENT
||
569 tok
->type
== ISL_TOKEN_VALUE
||
572 if (type
== isl_dim_param
) {
573 isl_stream_error(s
, tok
,
574 "expecting unique identifier");
577 isl_stream_push_token(s
, tok
);
579 bmap
= isl_basic_map_add(bmap
, type
, 1);
580 bmap
= read_var_def(s
, bmap
, type
, v
);
584 tok
= isl_stream_next_token(s
);
585 if (!tok
|| tok
->type
!= ',')
592 isl_stream_push_token(s
, tok
);
597 isl_basic_map_free(bmap
);
601 static __isl_give isl_mat
*accept_affine_list(struct isl_stream
*s
,
606 struct isl_token
*tok
= NULL
;
608 vec
= accept_affine(s
, v
);
609 mat
= isl_mat_from_row_vec(vec
);
614 tok
= isl_stream_next_token(s
);
616 isl_stream_error(s
, NULL
, "unexpected EOF");
619 if (tok
->type
!= ',') {
620 isl_stream_push_token(s
, tok
);
625 vec
= accept_affine(s
, v
);
626 mat
= isl_mat_add_zero_cols(mat
, 1 + v
->n
- isl_mat_cols(mat
));
627 mat
= isl_mat_vec_concat(mat
, vec
);
638 static int read_minmax_definition(struct isl_stream
*s
, struct vars
*v
)
640 struct isl_token
*tok
;
641 struct variable
*var
;
645 tok
= isl_stream_next_token(s
);
648 var
->sign
= tok
->type
== ISL_TOKEN_MIN
? -1 : 1;
651 if (isl_stream_eat(s
, '('))
654 var
->list
= accept_affine_list(s
, v
);
658 if (isl_stream_eat(s
, ')'))
664 static int read_div_definition(struct isl_stream
*s
, struct vars
*v
)
666 struct isl_token
*tok
;
669 struct variable
*var
;
672 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FLOORD
) ||
673 isl_stream_eat_if_available(s
, ISL_TOKEN_CEILD
)) {
675 if (isl_stream_eat(s
, '('))
678 if (isl_stream_eat(s
, '['))
680 if (isl_stream_eat_if_available(s
, '('))
686 aff
= accept_affine(s
, v
);
690 var
->def
= isl_vec_alloc(s
->ctx
, 2 + v
->n
);
696 isl_seq_cpy(var
->def
->el
+ 1, aff
->el
, aff
->size
);
701 if (isl_stream_eat(s
, ','))
704 if (seen_paren
&& isl_stream_eat(s
, ')'))
706 if (isl_stream_eat(s
, '/'))
713 if (tok
->type
!= ISL_TOKEN_VALUE
) {
714 isl_stream_error(s
, tok
, "expected denominator");
715 isl_stream_push_token(s
, tok
);
718 isl_int_set(var
->def
->el
[0], tok
->u
.v
);
722 if (isl_stream_eat(s
, ')'))
725 if (isl_stream_eat(s
, ']'))
732 static struct isl_basic_map
*add_div_definition(struct isl_stream
*s
,
733 struct vars
*v
, struct isl_basic_map
*bmap
, int pos
)
735 struct variable
*var
= v
->v
;
736 unsigned o_out
= isl_basic_map_offset(bmap
, isl_dim_out
) - 1;
738 if (read_div_definition(s
, v
) < 0)
741 if (isl_basic_map_add_div_constraints_var(bmap
, o_out
+ pos
,
747 isl_basic_map_free(bmap
);
751 static struct isl_basic_map
*read_defined_var_list(struct isl_stream
*s
,
752 struct vars
*v
, struct isl_basic_map
*bmap
)
754 struct isl_token
*tok
;
756 while ((tok
= isl_stream_next_token(s
)) != NULL
) {
759 unsigned n_out
= isl_basic_map_dim(bmap
, isl_dim_out
);
761 if (tok
->type
!= ISL_TOKEN_IDENT
)
764 p
= vars_pos(v
, tok
->u
.s
, -1);
768 isl_stream_error(s
, tok
, "expecting unique identifier");
772 bmap
= isl_basic_map_cow(bmap
);
773 bmap
= isl_basic_map_add(bmap
, isl_dim_out
, 1);
774 bmap
= isl_basic_map_extend_dim(bmap
, isl_dim_copy(bmap
->dim
),
778 tok
= isl_stream_next_token(s
);
779 if (tok
&& tok
->type
== '=') {
781 bmap
= add_div_definition(s
, v
, bmap
, n_out
);
782 tok
= isl_stream_next_token(s
);
785 if (!tok
|| tok
->type
!= ',')
791 isl_stream_push_token(s
, tok
);
796 isl_basic_map_free(bmap
);
800 static int next_is_tuple(struct isl_stream
*s
)
802 struct isl_token
*tok
;
805 tok
= isl_stream_next_token(s
);
808 if (tok
->type
== '[') {
809 isl_stream_push_token(s
, tok
);
812 if (tok
->type
!= ISL_TOKEN_IDENT
&& !tok
->is_keyword
) {
813 isl_stream_push_token(s
, tok
);
817 is_tuple
= isl_stream_next_token_is(s
, '[');
819 isl_stream_push_token(s
, tok
);
824 static __isl_give isl_basic_map
*read_tuple(struct isl_stream
*s
,
825 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
);
827 static __isl_give isl_basic_map
*read_nested_tuple(struct isl_stream
*s
,
828 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
830 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
831 if (isl_stream_eat(s
, ISL_TOKEN_TO
))
833 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
834 bmap
= isl_basic_map_from_range(isl_basic_map_wrap(bmap
));
837 isl_basic_map_free(bmap
);
841 static __isl_give isl_basic_map
*read_tuple(struct isl_stream
*s
,
842 __isl_take isl_basic_map
*bmap
, enum isl_dim_type type
, struct vars
*v
)
844 struct isl_token
*tok
;
847 tok
= isl_stream_next_token(s
);
848 if (tok
&& (tok
->type
== ISL_TOKEN_IDENT
|| tok
->is_keyword
)) {
849 name
= strdup(tok
->u
.s
);
853 tok
= isl_stream_next_token(s
);
855 if (!tok
|| tok
->type
!= '[') {
856 isl_stream_error(s
, tok
, "expecting '['");
860 if (type
!= isl_dim_param
&& next_is_tuple(s
)) {
861 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
862 int nparam
= isl_dim_size(dim
, isl_dim_param
);
863 int n_in
= isl_dim_size(dim
, isl_dim_in
);
864 isl_basic_map
*nested
;
865 if (type
== isl_dim_out
)
866 dim
= isl_dim_move(dim
, isl_dim_param
, nparam
,
867 isl_dim_in
, 0, n_in
);
868 nested
= isl_basic_map_alloc_dim(dim
, 0, 0, 0);
869 nested
= read_nested_tuple(s
, nested
, v
);
870 if (type
== isl_dim_in
) {
871 nested
= isl_basic_map_reverse(nested
);
872 bmap
= isl_basic_map_intersect(nested
, bmap
);
875 dim
= isl_dim_range(isl_basic_map_get_dim(nested
));
876 dim
= isl_dim_drop(dim
, isl_dim_param
, nparam
, n_in
);
877 dim
= isl_dim_join(isl_basic_map_get_dim(bmap
), dim
);
878 bset
= isl_basic_map_domain(bmap
);
879 nested
= isl_basic_map_reset_dim(nested
, dim
);
880 bmap
= isl_basic_map_intersect_domain(nested
, bset
);
883 bmap
= read_var_list(s
, bmap
, type
, v
);
884 tok
= isl_stream_next_token(s
);
885 if (!tok
|| tok
->type
!= ']') {
886 isl_stream_error(s
, tok
, "expecting ']'");
892 bmap
= isl_basic_map_set_tuple_name(bmap
, type
, name
);
900 isl_basic_map_free(bmap
);
904 static __isl_give isl_basic_map
*construct_constraint(
905 __isl_take isl_basic_map
*bmap
, enum isl_token_type type
,
906 isl_int
*left
, isl_int
*right
)
914 len
= 1 + isl_basic_map_total_dim(bmap
);
917 k
= isl_basic_map_alloc_inequality(bmap
);
920 if (type
== ISL_TOKEN_LE
)
921 isl_seq_combine(bmap
->ineq
[k
], ctx
->negone
, left
,
924 else if (type
== ISL_TOKEN_GE
)
925 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
928 else if (type
== ISL_TOKEN_LT
) {
929 isl_seq_combine(bmap
->ineq
[k
], ctx
->negone
, left
,
932 isl_int_sub_ui(bmap
->ineq
[k
][0], bmap
->ineq
[k
][0], 1);
933 } else if (type
== ISL_TOKEN_GT
) {
934 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
937 isl_int_sub_ui(bmap
->ineq
[k
][0], bmap
->ineq
[k
][0], 1);
939 isl_seq_combine(bmap
->ineq
[k
], ctx
->one
, left
,
942 isl_basic_map_inequality_to_equality(bmap
, k
);
947 isl_basic_map_free(bmap
);
951 static int is_comparator(struct isl_token
*tok
)
968 /* Add any variables in the variable list "v" that are not already in "bmap"
969 * as output variables in "bmap".
971 static __isl_give isl_basic_map
*add_lifted_divs(__isl_take isl_basic_map
*bmap
,
976 struct variable
*var
;
978 extra
= v
->n
- isl_basic_map_total_dim(bmap
);
983 bmap
= isl_basic_map_add(bmap
, isl_dim_out
, extra
);
984 bmap
= isl_basic_map_extend_dim(bmap
, isl_basic_map_get_dim(bmap
),
987 for (i
= 0, var
= v
->v
; i
< extra
; ++i
, var
= var
->next
) {
990 var
->def
= isl_vec_zero_extend(var
->def
, 2 + v
->n
);
993 if (isl_basic_map_add_div_constraints_var(bmap
, var
->pos
,
1000 isl_basic_map_free(bmap
);
1004 static struct isl_basic_map
*add_constraint(struct isl_stream
*s
,
1005 struct vars
*v
, struct isl_basic_map
*bmap
)
1008 struct isl_token
*tok
= NULL
;
1009 struct isl_mat
*aff1
= NULL
, *aff2
= NULL
;
1011 bmap
= isl_basic_map_cow(bmap
);
1013 aff1
= accept_affine_list(s
, v
);
1016 tok
= isl_stream_next_token(s
);
1017 if (!is_comparator(tok
)) {
1018 isl_stream_error(s
, tok
, "missing operator");
1020 isl_stream_push_token(s
, tok
);
1025 aff2
= accept_affine_list(s
, v
);
1029 aff1
= isl_mat_add_zero_cols(aff1
, aff2
->n_col
- aff1
->n_col
);
1032 bmap
= add_lifted_divs(bmap
, v
);
1033 bmap
= isl_basic_map_extend_constraints(bmap
, 0,
1034 aff1
->n_row
* aff2
->n_row
);
1035 for (i
= 0; i
< aff1
->n_row
; ++i
)
1036 for (j
= 0; j
< aff2
->n_row
; ++j
)
1037 bmap
= construct_constraint(bmap
, tok
->type
,
1038 aff1
->row
[i
], aff2
->row
[j
]);
1039 isl_token_free(tok
);
1043 tok
= isl_stream_next_token(s
);
1044 if (!is_comparator(tok
)) {
1046 isl_stream_push_token(s
, tok
);
1055 isl_token_free(tok
);
1058 isl_basic_map_free(bmap
);
1062 /* Return first variable, starting at n, representing a min or max,
1063 * or NULL if there is no such variable.
1065 static struct variable
*first_minmax(struct vars
*v
, int n
)
1067 struct variable
*first
= NULL
;
1068 struct variable
*var
;
1070 for (var
= v
->v
; var
&& var
->pos
>= n
; var
= var
->next
)
1077 /* Check whether the variable at the given position only occurs in
1078 * inequalities and only with the given sign.
1080 static int all_coefficients_of_sign(__isl_keep isl_map
*map
, int pos
, int sign
)
1087 for (i
= 0; i
< map
->n
; ++i
) {
1088 isl_basic_map
*bmap
= map
->p
[i
];
1090 for (j
= 0; j
< bmap
->n_eq
; ++j
)
1091 if (!isl_int_is_zero(bmap
->eq
[j
][1 + pos
]))
1093 for (j
= 0; j
< bmap
->n_ineq
; ++j
) {
1094 int s
= isl_int_sgn(bmap
->ineq
[j
][1 + pos
]);
1105 /* Given a variable m which represents a min or a max of n expressions
1106 * b_i, add the constraints
1110 * in case of a min (var->sign < 0) and m >= b_i in case of a max.
1112 static __isl_give isl_map
*bound_minmax(__isl_take isl_map
*map
,
1113 struct variable
*var
)
1116 isl_basic_map
*bound
;
1119 total
= isl_map_dim(map
, isl_dim_all
);
1120 bound
= isl_basic_map_alloc_dim(isl_map_get_dim(map
),
1121 0, 0, var
->list
->n_row
);
1123 for (i
= 0; i
< var
->list
->n_row
; ++i
) {
1124 k
= isl_basic_map_alloc_inequality(bound
);
1128 isl_seq_cpy(bound
->ineq
[k
], var
->list
->row
[i
],
1131 isl_seq_neg(bound
->ineq
[k
], var
->list
->row
[i
],
1133 isl_int_set_si(bound
->ineq
[k
][1 + var
->pos
], var
->sign
);
1134 isl_seq_clr(bound
->ineq
[k
] + var
->list
->n_col
,
1135 1 + total
- var
->list
->n_col
);
1138 map
= isl_map_intersect(map
, isl_map_from_basic_map(bound
));
1142 isl_basic_map_free(bound
);
1147 /* Given a variable m which represents a min (or max) of n expressions
1148 * b_i, add constraints that assigns the minimal upper bound to m, i.e.,
1149 * divide the space into cells where one
1150 * of the upper bounds is smaller than all the others and assign
1151 * this upper bound to m.
1153 * In particular, if there are n bounds b_i, then the input map
1154 * is split into n pieces, each with the extra constraints
1157 * b_i <= b_j for j > i
1158 * b_i < b_j for j < i
1160 * in case of a min (var->sign < 0) and similarly in case of a max.
1162 * Note: this function is very similar to set_minimum in isl_tab_pip.c
1163 * Perhaps we should try to merge the two.
1165 static __isl_give isl_map
*set_minmax(__isl_take isl_map
*map
,
1166 struct variable
*var
)
1169 isl_basic_map
*bmap
= NULL
;
1171 isl_map
*split
= NULL
;
1174 ctx
= isl_map_get_ctx(map
);
1175 total
= isl_map_dim(map
, isl_dim_all
);
1176 split
= isl_map_alloc_dim(isl_map_get_dim(map
),
1177 var
->list
->n_row
, ISL_SET_DISJOINT
);
1179 for (i
= 0; i
< var
->list
->n_row
; ++i
) {
1180 bmap
= isl_basic_map_alloc_dim(isl_map_get_dim(map
), 0,
1181 1, var
->list
->n_row
- 1);
1182 k
= isl_basic_map_alloc_equality(bmap
);
1185 isl_seq_cpy(bmap
->eq
[k
], var
->list
->row
[i
], var
->list
->n_col
);
1186 isl_int_set_si(bmap
->eq
[k
][1 + var
->pos
], -1);
1187 for (j
= 0; j
< var
->list
->n_row
; ++j
) {
1190 k
= isl_basic_map_alloc_inequality(bmap
);
1194 isl_seq_combine(bmap
->ineq
[k
],
1195 ctx
->one
, var
->list
->row
[j
],
1196 ctx
->negone
, var
->list
->row
[i
],
1199 isl_seq_combine(bmap
->ineq
[k
],
1200 ctx
->negone
, var
->list
->row
[j
],
1201 ctx
->one
, var
->list
->row
[i
],
1203 isl_seq_clr(bmap
->ineq
[k
] + var
->list
->n_col
,
1204 1 + total
- var
->list
->n_col
);
1206 isl_int_sub_ui(bmap
->ineq
[k
][0],
1207 bmap
->ineq
[k
][0], 1);
1209 bmap
= isl_basic_map_finalize(bmap
);
1210 split
= isl_map_add_basic_map(split
, bmap
);
1213 map
= isl_map_intersect(map
, split
);
1217 isl_basic_map_free(bmap
);
1218 isl_map_free(split
);
1223 /* Plug in the definitions of all min and max expressions.
1224 * If a min expression only appears in inequalities and only
1225 * with a positive coefficient, then we can simply bound
1226 * the variable representing the min by its defining terms
1227 * and similarly for a max expression.
1228 * Otherwise, we have to assign the different terms to the
1229 * variable under the condition that the assigned term is smaller
1230 * than the other terms.
1232 static __isl_give isl_map
*add_minmax(__isl_take isl_map
*map
,
1233 struct vars
*v
, int n
)
1236 struct variable
*var
;
1239 var
= first_minmax(v
, n
);
1242 if (all_coefficients_of_sign(map
, var
->pos
, -var
->sign
))
1243 map
= bound_minmax(map
, var
);
1245 map
= set_minmax(map
, var
);
1252 static isl_map
*read_constraint(struct isl_stream
*s
,
1253 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1261 bmap
= isl_basic_set_unwrap(isl_basic_set_lift(isl_basic_map_wrap(bmap
)));
1263 bmap
= add_constraint(s
, v
, bmap
);
1264 bmap
= isl_basic_map_simplify(bmap
);
1265 bmap
= isl_basic_map_finalize(bmap
);
1267 map
= isl_map_from_basic_map(bmap
);
1269 map
= add_minmax(map
, v
, n
);
1271 map
= isl_set_unwrap(isl_map_domain(map
));
1273 vars_drop(v
, v
->n
- n
);
1278 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1279 struct vars
*v
, __isl_take isl_basic_map
*bmap
);
1281 static __isl_give isl_map
*read_exists(struct isl_stream
*s
,
1282 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1285 int seen_paren
= isl_stream_eat_if_available(s
, '(');
1286 isl_map
*map
= NULL
;
1288 bmap
= isl_basic_map_from_domain(isl_basic_map_wrap(bmap
));
1289 bmap
= read_defined_var_list(s
, v
, bmap
);
1291 if (isl_stream_eat(s
, ':'))
1294 map
= read_disjuncts(s
, v
, bmap
);
1295 map
= isl_set_unwrap(isl_map_domain(map
));
1298 vars_drop(v
, v
->n
- n
);
1299 if (seen_paren
&& isl_stream_eat(s
, ')'))
1304 isl_basic_map_free(bmap
);
1309 static __isl_give isl_map
*read_conjunct(struct isl_stream
*s
,
1310 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1314 if (isl_stream_eat_if_available(s
, '(')) {
1315 map
= read_disjuncts(s
, v
, bmap
);
1316 if (isl_stream_eat(s
, ')'))
1321 if (isl_stream_eat_if_available(s
, ISL_TOKEN_EXISTS
))
1322 return read_exists(s
, v
, bmap
);
1324 if (isl_stream_eat_if_available(s
, ISL_TOKEN_TRUE
))
1325 return isl_map_from_basic_map(bmap
);
1327 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FALSE
)) {
1328 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1329 isl_basic_map_free(bmap
);
1330 return isl_map_empty(dim
);
1333 return read_constraint(s
, v
, bmap
);
1339 static __isl_give isl_map
*read_conjuncts(struct isl_stream
*s
,
1340 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1345 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1346 map
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1349 t
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1350 map
= isl_map_subtract(t
, map
);
1353 while (isl_stream_eat_if_available(s
, ISL_TOKEN_AND
)) {
1356 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1357 map_i
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1359 map
= isl_map_subtract(map
, map_i
);
1361 map
= isl_map_intersect(map
, map_i
);
1364 isl_basic_map_free(bmap
);
1368 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1369 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1371 struct isl_map
*map
;
1373 if (isl_stream_next_token_is(s
, '}')) {
1374 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1375 isl_basic_map_free(bmap
);
1376 return isl_map_universe(dim
);
1379 map
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1380 while (isl_stream_eat_if_available(s
, ISL_TOKEN_OR
)) {
1383 map_i
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1384 map
= isl_map_union(map
, map_i
);
1387 isl_basic_map_free(bmap
);
1391 static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map
*bmap
, int pos
)
1393 if (pos
< isl_basic_map_dim(bmap
, isl_dim_out
))
1394 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1395 isl_basic_map_dim(bmap
, isl_dim_in
) + pos
;
1396 pos
-= isl_basic_map_dim(bmap
, isl_dim_out
);
1398 if (pos
< isl_basic_map_dim(bmap
, isl_dim_in
))
1399 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) + pos
;
1400 pos
-= isl_basic_map_dim(bmap
, isl_dim_in
);
1402 if (pos
< isl_basic_map_dim(bmap
, isl_dim_div
))
1403 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1404 isl_basic_map_dim(bmap
, isl_dim_in
) +
1405 isl_basic_map_dim(bmap
, isl_dim_out
) + pos
;
1406 pos
-= isl_basic_map_dim(bmap
, isl_dim_div
);
1408 if (pos
< isl_basic_map_dim(bmap
, isl_dim_param
))
1414 static __isl_give isl_basic_map
*basic_map_read_polylib_constraint(
1415 struct isl_stream
*s
, __isl_take isl_basic_map
*bmap
)
1418 struct isl_token
*tok
;
1428 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
1429 dim
= isl_basic_map_dim(bmap
, isl_dim_out
);
1431 tok
= isl_stream_next_token(s
);
1432 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1433 isl_stream_error(s
, tok
, "expecting coefficient");
1435 isl_stream_push_token(s
, tok
);
1438 if (!tok
->on_new_line
) {
1439 isl_stream_error(s
, tok
, "coefficient should appear on new line");
1440 isl_stream_push_token(s
, tok
);
1444 type
= isl_int_get_si(tok
->u
.v
);
1445 isl_token_free(tok
);
1447 isl_assert(s
->ctx
, type
== 0 || type
== 1, goto error
);
1449 k
= isl_basic_map_alloc_equality(bmap
);
1452 k
= isl_basic_map_alloc_inequality(bmap
);
1458 for (j
= 0; j
< 1 + isl_basic_map_total_dim(bmap
); ++j
) {
1460 tok
= isl_stream_next_token(s
);
1461 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1462 isl_stream_error(s
, tok
, "expecting coefficient");
1464 isl_stream_push_token(s
, tok
);
1467 if (tok
->on_new_line
) {
1468 isl_stream_error(s
, tok
,
1469 "coefficient should not appear on new line");
1470 isl_stream_push_token(s
, tok
);
1473 pos
= polylib_pos_to_isl_pos(bmap
, j
);
1474 isl_int_set(c
[pos
], tok
->u
.v
);
1475 isl_token_free(tok
);
1480 isl_basic_map_free(bmap
);
1484 static __isl_give isl_basic_map
*basic_map_read_polylib(struct isl_stream
*s
,
1488 struct isl_token
*tok
;
1489 struct isl_token
*tok2
;
1492 unsigned in
= 0, out
, local
= 0;
1493 struct isl_basic_map
*bmap
= NULL
;
1498 tok
= isl_stream_next_token(s
);
1500 isl_stream_error(s
, NULL
, "unexpected EOF");
1503 tok2
= isl_stream_next_token(s
);
1505 isl_token_free(tok
);
1506 isl_stream_error(s
, NULL
, "unexpected EOF");
1509 if (tok
->type
!= ISL_TOKEN_VALUE
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1510 isl_stream_push_token(s
, tok2
);
1511 isl_stream_push_token(s
, tok
);
1512 isl_stream_error(s
, NULL
,
1513 "expecting constraint matrix dimensions");
1516 n_row
= isl_int_get_si(tok
->u
.v
);
1517 n_col
= isl_int_get_si(tok2
->u
.v
);
1518 on_new_line
= tok2
->on_new_line
;
1519 isl_token_free(tok2
);
1520 isl_token_free(tok
);
1521 isl_assert(s
->ctx
, !on_new_line
, return NULL
);
1522 isl_assert(s
->ctx
, n_row
>= 0, return NULL
);
1523 isl_assert(s
->ctx
, n_col
>= 2 + nparam
, return NULL
);
1524 tok
= isl_stream_next_token_on_same_line(s
);
1526 if (tok
->type
!= ISL_TOKEN_VALUE
) {
1527 isl_stream_error(s
, tok
,
1528 "expecting number of output dimensions");
1529 isl_stream_push_token(s
, tok
);
1532 out
= isl_int_get_si(tok
->u
.v
);
1533 isl_token_free(tok
);
1535 tok
= isl_stream_next_token_on_same_line(s
);
1536 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1537 isl_stream_error(s
, tok
,
1538 "expecting number of input dimensions");
1540 isl_stream_push_token(s
, tok
);
1543 in
= isl_int_get_si(tok
->u
.v
);
1544 isl_token_free(tok
);
1546 tok
= isl_stream_next_token_on_same_line(s
);
1547 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1548 isl_stream_error(s
, tok
,
1549 "expecting number of existentials");
1551 isl_stream_push_token(s
, tok
);
1554 local
= isl_int_get_si(tok
->u
.v
);
1555 isl_token_free(tok
);
1557 tok
= isl_stream_next_token_on_same_line(s
);
1558 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1559 isl_stream_error(s
, tok
,
1560 "expecting number of parameters");
1562 isl_stream_push_token(s
, tok
);
1565 nparam
= isl_int_get_si(tok
->u
.v
);
1566 isl_token_free(tok
);
1567 if (n_col
!= 1 + out
+ in
+ local
+ nparam
+ 1) {
1568 isl_stream_error(s
, NULL
,
1569 "dimensions don't match");
1573 out
= n_col
- 2 - nparam
;
1574 bmap
= isl_basic_map_alloc(s
->ctx
, nparam
, in
, out
, local
, n_row
, n_row
);
1578 for (i
= 0; i
< local
; ++i
) {
1579 int k
= isl_basic_map_alloc_div(bmap
);
1582 isl_seq_clr(bmap
->div
[k
], 1 + 1 + nparam
+ in
+ out
+ local
);
1585 for (i
= 0; i
< n_row
; ++i
)
1586 bmap
= basic_map_read_polylib_constraint(s
, bmap
);
1588 tok
= isl_stream_next_token_on_same_line(s
);
1590 isl_stream_error(s
, tok
, "unexpected extra token on line");
1591 isl_stream_push_token(s
, tok
);
1595 bmap
= isl_basic_map_simplify(bmap
);
1596 bmap
= isl_basic_map_finalize(bmap
);
1599 isl_basic_map_free(bmap
);
1603 static struct isl_map
*map_read_polylib(struct isl_stream
*s
, int nparam
)
1605 struct isl_token
*tok
;
1606 struct isl_token
*tok2
;
1608 struct isl_map
*map
;
1610 tok
= isl_stream_next_token(s
);
1612 isl_stream_error(s
, NULL
, "unexpected EOF");
1615 tok2
= isl_stream_next_token_on_same_line(s
);
1616 if (tok2
&& tok2
->type
== ISL_TOKEN_VALUE
) {
1617 isl_stream_push_token(s
, tok2
);
1618 isl_stream_push_token(s
, tok
);
1619 return isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1622 isl_stream_error(s
, tok2
, "unexpected token");
1623 isl_stream_push_token(s
, tok2
);
1624 isl_stream_push_token(s
, tok
);
1627 n
= isl_int_get_si(tok
->u
.v
);
1628 isl_token_free(tok
);
1630 isl_assert(s
->ctx
, n
>= 1, return NULL
);
1632 map
= isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1634 for (i
= 1; map
&& i
< n
; ++i
)
1635 map
= isl_map_union(map
,
1636 isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
)));
1641 static int optional_power(struct isl_stream
*s
)
1644 struct isl_token
*tok
;
1646 tok
= isl_stream_next_token(s
);
1649 if (tok
->type
!= '^') {
1650 isl_stream_push_token(s
, tok
);
1653 isl_token_free(tok
);
1654 tok
= isl_stream_next_token(s
);
1655 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1656 isl_stream_error(s
, tok
, "expecting exponent");
1658 isl_stream_push_token(s
, tok
);
1661 pow
= isl_int_get_si(tok
->u
.v
);
1662 isl_token_free(tok
);
1666 static __isl_give isl_div
*read_div(struct isl_stream
*s
,
1667 __isl_take isl_dim
*dim
, struct vars
*v
)
1670 isl_basic_map
*bmap
;
1673 bmap
= isl_basic_map_universe(dim
);
1675 if (vars_add_anon(v
) < 0)
1677 if (read_div_definition(s
, v
) < 0)
1679 bmap
= add_divs(bmap
, v
);
1680 bmap
= isl_basic_map_order_divs(bmap
);
1683 vars_drop(v
, v
->n
- n
);
1685 return isl_basic_map_div(bmap
, bmap
->n_div
- 1);
1687 isl_basic_map_free(bmap
);
1691 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1692 __isl_keep isl_basic_map
*bmap
, struct vars
*v
);
1694 static __isl_give isl_qpolynomial
*read_factor(struct isl_stream
*s
,
1695 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1697 struct isl_qpolynomial
*qp
;
1698 struct isl_token
*tok
;
1700 tok
= next_token(s
);
1702 isl_stream_error(s
, NULL
, "unexpected EOF");
1705 if (tok
->type
== '(') {
1708 isl_token_free(tok
);
1709 qp
= read_term(s
, bmap
, v
);
1712 if (isl_stream_eat(s
, ')'))
1714 pow
= optional_power(s
);
1715 qp
= isl_qpolynomial_pow(qp
, pow
);
1716 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
1717 struct isl_token
*tok2
;
1718 tok2
= isl_stream_next_token(s
);
1719 if (tok2
&& tok2
->type
== '/') {
1720 isl_token_free(tok2
);
1721 tok2
= next_token(s
);
1722 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1723 isl_stream_error(s
, tok2
, "expected denominator");
1724 isl_token_free(tok
);
1725 isl_token_free(tok2
);
1728 qp
= isl_qpolynomial_rat_cst(isl_basic_map_get_dim(bmap
),
1729 tok
->u
.v
, tok2
->u
.v
);
1730 isl_token_free(tok2
);
1732 isl_stream_push_token(s
, tok2
);
1733 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1736 isl_token_free(tok
);
1737 } else if (tok
->type
== ISL_TOKEN_INFTY
) {
1738 isl_token_free(tok
);
1739 qp
= isl_qpolynomial_infty(isl_basic_map_get_dim(bmap
));
1740 } else if (tok
->type
== ISL_TOKEN_NAN
) {
1741 isl_token_free(tok
);
1742 qp
= isl_qpolynomial_nan(isl_basic_map_get_dim(bmap
));
1743 } else if (tok
->type
== ISL_TOKEN_IDENT
) {
1745 int pos
= vars_pos(v
, tok
->u
.s
, -1);
1748 isl_token_free(tok
);
1752 vars_drop(v
, v
->n
- n
);
1753 isl_stream_error(s
, tok
, "unknown identifier");
1754 isl_token_free(tok
);
1757 isl_token_free(tok
);
1758 pow
= optional_power(s
);
1759 qp
= isl_qpolynomial_var_pow(isl_basic_map_get_dim(bmap
), pos
, pow
);
1760 } else if (tok
->type
== '[') {
1764 isl_stream_push_token(s
, tok
);
1765 div
= read_div(s
, isl_basic_map_get_dim(bmap
), v
);
1766 pow
= optional_power(s
);
1767 qp
= isl_qpolynomial_div_pow(div
, pow
);
1768 } else if (tok
->type
== '-') {
1769 struct isl_qpolynomial
*qp2
;
1771 isl_token_free(tok
);
1772 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1774 qp2
= read_factor(s
, bmap
, v
);
1775 qp
= isl_qpolynomial_mul(qp
, qp2
);
1777 isl_stream_error(s
, tok
, "unexpected isl_token");
1778 isl_stream_push_token(s
, tok
);
1782 if (isl_stream_eat_if_available(s
, '*') ||
1783 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
1784 struct isl_qpolynomial
*qp2
;
1786 qp2
= read_factor(s
, bmap
, v
);
1787 qp
= isl_qpolynomial_mul(qp
, qp2
);
1792 isl_qpolynomial_free(qp
);
1796 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1797 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1799 struct isl_token
*tok
;
1800 struct isl_qpolynomial
*qp
;
1802 qp
= read_factor(s
, bmap
, v
);
1805 tok
= next_token(s
);
1809 if (tok
->type
== '+') {
1810 struct isl_qpolynomial
*qp2
;
1812 isl_token_free(tok
);
1813 qp2
= read_factor(s
, bmap
, v
);
1814 qp
= isl_qpolynomial_add(qp
, qp2
);
1815 } else if (tok
->type
== '-') {
1816 struct isl_qpolynomial
*qp2
;
1818 isl_token_free(tok
);
1819 qp2
= read_factor(s
, bmap
, v
);
1820 qp
= isl_qpolynomial_sub(qp
, qp2
);
1821 } else if (tok
->type
== ISL_TOKEN_VALUE
&&
1822 isl_int_is_neg(tok
->u
.v
)) {
1823 struct isl_qpolynomial
*qp2
;
1825 isl_stream_push_token(s
, tok
);
1826 qp2
= read_factor(s
, bmap
, v
);
1827 qp
= isl_qpolynomial_add(qp
, qp2
);
1829 isl_stream_push_token(s
, tok
);
1837 static __isl_give isl_map
*read_optional_disjuncts(struct isl_stream
*s
,
1838 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1840 struct isl_token
*tok
;
1841 struct isl_map
*map
;
1843 tok
= isl_stream_next_token(s
);
1845 isl_stream_error(s
, NULL
, "unexpected EOF");
1848 map
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1849 if (tok
->type
== ':' ||
1850 (tok
->type
== ISL_TOKEN_OR
&& !strcmp(tok
->u
.s
, "|"))) {
1851 isl_token_free(tok
);
1852 map
= isl_map_intersect(map
,
1853 read_disjuncts(s
, v
, isl_basic_map_copy(bmap
)));
1855 isl_stream_push_token(s
, tok
);
1857 isl_basic_map_free(bmap
);
1861 isl_basic_map_free(bmap
);
1865 static struct isl_obj
obj_read_poly(struct isl_stream
*s
,
1866 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1868 struct isl_obj obj
= { isl_obj_pw_qpolynomial
, NULL
};
1869 struct isl_pw_qpolynomial
*pwqp
;
1870 struct isl_qpolynomial
*qp
;
1871 struct isl_map
*map
;
1872 struct isl_set
*set
;
1874 qp
= read_term(s
, bmap
, v
);
1875 map
= read_optional_disjuncts(s
, bmap
, v
);
1876 set
= isl_map_range(map
);
1878 pwqp
= isl_pw_qpolynomial_alloc(set
, qp
);
1880 vars_drop(v
, v
->n
- n
);
1886 static struct isl_obj
obj_read_poly_or_fold(struct isl_stream
*s
,
1887 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1889 struct isl_obj obj
= { isl_obj_pw_qpolynomial_fold
, NULL
};
1890 struct isl_obj obj_p
;
1891 isl_qpolynomial
*qp
;
1892 isl_qpolynomial_fold
*fold
= NULL
;
1893 isl_pw_qpolynomial_fold
*pwf
;
1897 if (!isl_stream_eat_if_available(s
, ISL_TOKEN_MAX
))
1898 return obj_read_poly(s
, bmap
, v
, n
);
1900 if (isl_stream_eat(s
, '('))
1903 qp
= read_term(s
, bmap
, v
);
1904 fold
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1906 while (isl_stream_eat_if_available(s
, ',')) {
1907 isl_qpolynomial_fold
*fold_i
;
1908 qp
= read_term(s
, bmap
, v
);
1909 fold_i
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1910 fold
= isl_qpolynomial_fold_fold(fold
, fold_i
);
1913 if (isl_stream_eat(s
, ')'))
1916 map
= read_optional_disjuncts(s
, bmap
, v
);
1917 set
= isl_map_range(map
);
1918 pwf
= isl_pw_qpolynomial_fold_alloc(isl_fold_max
, set
, fold
);
1920 vars_drop(v
, v
->n
- n
);
1925 isl_basic_map_free(bmap
);
1926 isl_qpolynomial_fold_free(fold
);
1927 obj
.type
= isl_obj_none
;
1931 static int is_rational(struct isl_stream
*s
)
1933 struct isl_token
*tok
;
1935 tok
= isl_stream_next_token(s
);
1938 if (tok
->type
== ISL_TOKEN_RAT
&& isl_stream_next_token_is(s
, ':')) {
1939 isl_token_free(tok
);
1940 isl_stream_eat(s
, ':');
1944 isl_stream_push_token(s
, tok
);
1949 static struct isl_obj
obj_read_body(struct isl_stream
*s
,
1950 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1952 struct isl_map
*map
= NULL
;
1953 struct isl_token
*tok
;
1954 struct isl_obj obj
= { isl_obj_set
, NULL
};
1958 bmap
= isl_basic_map_set_rational(bmap
);
1960 if (!next_is_tuple(s
))
1961 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1963 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
1966 tok
= isl_stream_next_token(s
);
1967 if (tok
&& tok
->type
== ISL_TOKEN_TO
) {
1968 obj
.type
= isl_obj_map
;
1969 isl_token_free(tok
);
1970 if (!next_is_tuple(s
)) {
1971 bmap
= isl_basic_map_reverse(bmap
);
1972 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1974 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
1978 bmap
= isl_basic_map_reverse(bmap
);
1980 isl_stream_push_token(s
, tok
);
1983 map
= read_optional_disjuncts(s
, bmap
, v
);
1985 vars_drop(v
, v
->n
- n
);
1990 isl_basic_map_free(bmap
);
1991 obj
.type
= isl_obj_none
;
1995 static struct isl_obj
to_union(isl_ctx
*ctx
, struct isl_obj obj
)
1997 if (obj
.type
== isl_obj_map
) {
1998 obj
.v
= isl_union_map_from_map(obj
.v
);
1999 obj
.type
= isl_obj_union_map
;
2000 } else if (obj
.type
== isl_obj_set
) {
2001 obj
.v
= isl_union_set_from_set(obj
.v
);
2002 obj
.type
= isl_obj_union_set
;
2003 } else if (obj
.type
== isl_obj_pw_qpolynomial
) {
2004 obj
.v
= isl_union_pw_qpolynomial_from_pw_qpolynomial(obj
.v
);
2005 obj
.type
= isl_obj_union_pw_qpolynomial
;
2006 } else if (obj
.type
== isl_obj_pw_qpolynomial_fold
) {
2007 obj
.v
= isl_union_pw_qpolynomial_fold_from_pw_qpolynomial_fold(obj
.v
);
2008 obj
.type
= isl_obj_union_pw_qpolynomial_fold
;
2010 isl_assert(ctx
, 0, goto error
);
2013 obj
.type
->free(obj
.v
);
2014 obj
.type
= isl_obj_none
;
2018 static struct isl_obj
obj_add(struct isl_ctx
*ctx
,
2019 struct isl_obj obj1
, struct isl_obj obj2
)
2021 if (obj1
.type
== isl_obj_set
&& obj2
.type
== isl_obj_union_set
)
2022 obj1
= to_union(ctx
, obj1
);
2023 if (obj1
.type
== isl_obj_union_set
&& obj2
.type
== isl_obj_set
)
2024 obj2
= to_union(ctx
, obj2
);
2025 if (obj1
.type
== isl_obj_map
&& obj2
.type
== isl_obj_union_map
)
2026 obj1
= to_union(ctx
, obj1
);
2027 if (obj1
.type
== isl_obj_union_map
&& obj2
.type
== isl_obj_map
)
2028 obj2
= to_union(ctx
, obj2
);
2029 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2030 obj2
.type
== isl_obj_union_pw_qpolynomial
)
2031 obj1
= to_union(ctx
, obj1
);
2032 if (obj1
.type
== isl_obj_union_pw_qpolynomial
&&
2033 obj2
.type
== isl_obj_pw_qpolynomial
)
2034 obj2
= to_union(ctx
, obj2
);
2035 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2036 obj2
.type
== isl_obj_union_pw_qpolynomial_fold
)
2037 obj1
= to_union(ctx
, obj1
);
2038 if (obj1
.type
== isl_obj_union_pw_qpolynomial_fold
&&
2039 obj2
.type
== isl_obj_pw_qpolynomial_fold
)
2040 obj2
= to_union(ctx
, obj2
);
2041 isl_assert(ctx
, obj1
.type
== obj2
.type
, goto error
);
2042 if (obj1
.type
== isl_obj_map
&& !isl_map_has_equal_dim(obj1
.v
, obj2
.v
)) {
2043 obj1
= to_union(ctx
, obj1
);
2044 obj2
= to_union(ctx
, obj2
);
2046 if (obj1
.type
== isl_obj_set
&& !isl_set_has_equal_dim(obj1
.v
, obj2
.v
)) {
2047 obj1
= to_union(ctx
, obj1
);
2048 obj2
= to_union(ctx
, obj2
);
2050 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2051 !isl_pw_qpolynomial_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_fold
&&
2056 !isl_pw_qpolynomial_fold_has_equal_dim(obj1
.v
, obj2
.v
)) {
2057 obj1
= to_union(ctx
, obj1
);
2058 obj2
= to_union(ctx
, obj2
);
2060 obj1
.v
= obj1
.type
->add(obj1
.v
, obj2
.v
);
2063 obj1
.type
->free(obj1
.v
);
2064 obj2
.type
->free(obj2
.v
);
2065 obj1
.type
= isl_obj_none
;
2070 static struct isl_obj
obj_read(struct isl_stream
*s
, int nparam
)
2072 isl_basic_map
*bmap
= NULL
;
2073 struct isl_token
*tok
;
2074 struct vars
*v
= NULL
;
2075 struct isl_obj obj
= { isl_obj_set
, NULL
};
2077 tok
= next_token(s
);
2079 isl_stream_error(s
, NULL
, "unexpected EOF");
2082 if (tok
->type
== ISL_TOKEN_VALUE
) {
2083 struct isl_token
*tok2
;
2084 struct isl_map
*map
;
2086 tok2
= isl_stream_next_token(s
);
2087 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
||
2088 isl_int_is_neg(tok2
->u
.v
)) {
2090 isl_stream_push_token(s
, tok2
);
2091 obj
.type
= isl_obj_int
;
2092 obj
.v
= isl_int_obj_alloc(s
->ctx
, tok
->u
.v
);
2093 isl_token_free(tok
);
2096 isl_stream_push_token(s
, tok2
);
2097 isl_stream_push_token(s
, tok
);
2098 map
= map_read_polylib(s
, nparam
);
2101 if (isl_map_dim(map
, isl_dim_in
) > 0)
2102 obj
.type
= isl_obj_map
;
2106 v
= vars_new(s
->ctx
);
2108 isl_stream_push_token(s
, tok
);
2111 bmap
= isl_basic_map_alloc(s
->ctx
, 0, 0, 0, 0, 0, 0);
2112 if (tok
->type
== '[') {
2113 isl_stream_push_token(s
, tok
);
2114 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2118 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2119 tok
= isl_stream_next_token(s
);
2120 if (!tok
|| tok
->type
!= ISL_TOKEN_TO
) {
2121 isl_stream_error(s
, tok
, "expecting '->'");
2123 isl_stream_push_token(s
, tok
);
2126 isl_token_free(tok
);
2127 tok
= isl_stream_next_token(s
);
2128 } else if (nparam
> 0)
2129 bmap
= isl_basic_map_add(bmap
, isl_dim_param
, nparam
);
2130 if (!tok
|| tok
->type
!= '{') {
2131 isl_stream_error(s
, tok
, "expecting '{'");
2133 isl_stream_push_token(s
, tok
);
2136 isl_token_free(tok
);
2138 tok
= isl_stream_next_token(s
);
2141 else if (tok
->type
== ISL_TOKEN_IDENT
&& !strcmp(tok
->u
.s
, "Sym")) {
2142 isl_token_free(tok
);
2143 if (isl_stream_eat(s
, '='))
2145 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2149 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2150 } else if (tok
->type
== '}') {
2151 obj
.type
= isl_obj_union_set
;
2152 obj
.v
= isl_union_set_empty(isl_basic_map_get_dim(bmap
));
2153 isl_token_free(tok
);
2156 isl_stream_push_token(s
, tok
);
2161 o
= obj_read_body(s
, isl_basic_map_copy(bmap
), v
);
2162 if (o
.type
== isl_obj_none
|| !o
.v
)
2167 obj
= obj_add(s
->ctx
, obj
, o
);
2168 if (obj
.type
== isl_obj_none
|| !obj
.v
)
2171 tok
= isl_stream_next_token(s
);
2172 if (!tok
|| tok
->type
!= ';')
2174 isl_token_free(tok
);
2175 if (isl_stream_next_token_is(s
, '}')) {
2176 tok
= isl_stream_next_token(s
);
2181 if (tok
&& tok
->type
== '}') {
2182 isl_token_free(tok
);
2184 isl_stream_error(s
, tok
, "unexpected isl_token");
2186 isl_token_free(tok
);
2191 isl_basic_map_free(bmap
);
2195 isl_basic_map_free(bmap
);
2196 obj
.type
->free(obj
.v
);
2203 struct isl_obj
isl_stream_read_obj(struct isl_stream
*s
)
2205 return obj_read(s
, -1);
2208 __isl_give isl_map
*isl_stream_read_map(struct isl_stream
*s
, int nparam
)
2211 struct isl_map
*map
;
2213 obj
= obj_read(s
, nparam
);
2215 isl_assert(s
->ctx
, obj
.type
== isl_obj_map
||
2216 obj
.type
== isl_obj_set
, goto error
);
2220 obj
.type
->free(obj
.v
);
2224 __isl_give isl_set
*isl_stream_read_set(struct isl_stream
*s
, int nparam
)
2227 struct isl_set
*set
;
2229 obj
= obj_read(s
, nparam
);
2231 isl_assert(s
->ctx
, obj
.type
== isl_obj_set
, goto error
);
2235 obj
.type
->free(obj
.v
);
2239 __isl_give isl_union_map
*isl_stream_read_union_map(struct isl_stream
*s
)
2242 isl_union_map
*umap
;
2244 obj
= obj_read(s
, -1);
2245 if (obj
.type
== isl_obj_map
) {
2246 obj
.type
= isl_obj_union_map
;
2247 obj
.v
= isl_union_map_from_map(obj
.v
);
2249 if (obj
.type
== isl_obj_set
) {
2250 obj
.type
= isl_obj_union_set
;
2251 obj
.v
= isl_union_set_from_set(obj
.v
);
2254 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_map
||
2255 obj
.type
== isl_obj_union_set
, goto error
);
2259 obj
.type
->free(obj
.v
);
2263 __isl_give isl_union_set
*isl_stream_read_union_set(struct isl_stream
*s
)
2266 isl_union_set
*uset
;
2268 obj
= obj_read(s
, -1);
2269 if (obj
.type
== isl_obj_set
) {
2270 obj
.type
= isl_obj_union_set
;
2271 obj
.v
= isl_union_set_from_set(obj
.v
);
2274 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_set
, goto error
);
2278 obj
.type
->free(obj
.v
);
2282 static struct isl_basic_map
*basic_map_read(struct isl_stream
*s
, int nparam
)
2285 struct isl_map
*map
;
2286 struct isl_basic_map
*bmap
;
2288 obj
= obj_read(s
, nparam
);
2293 isl_assert(map
->ctx
, map
->n
<= 1, goto error
);
2296 bmap
= isl_basic_map_empty_like_map(map
);
2298 bmap
= isl_basic_map_copy(map
->p
[0]);
2308 __isl_give isl_basic_map
*isl_basic_map_read_from_file(isl_ctx
*ctx
,
2309 FILE *input
, int nparam
)
2311 struct isl_basic_map
*bmap
;
2312 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2315 bmap
= basic_map_read(s
, nparam
);
2320 __isl_give isl_basic_set
*isl_basic_set_read_from_file(isl_ctx
*ctx
,
2321 FILE *input
, int nparam
)
2323 struct isl_basic_map
*bmap
;
2324 bmap
= isl_basic_map_read_from_file(ctx
, input
, nparam
);
2327 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2328 return (struct isl_basic_set
*)bmap
;
2330 isl_basic_map_free(bmap
);
2334 struct isl_basic_map
*isl_basic_map_read_from_str(struct isl_ctx
*ctx
,
2335 const char *str
, int nparam
)
2337 struct isl_basic_map
*bmap
;
2338 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2341 bmap
= basic_map_read(s
, nparam
);
2346 struct isl_basic_set
*isl_basic_set_read_from_str(struct isl_ctx
*ctx
,
2347 const char *str
, int nparam
)
2349 struct isl_basic_map
*bmap
;
2350 bmap
= isl_basic_map_read_from_str(ctx
, str
, nparam
);
2353 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2354 return (struct isl_basic_set
*)bmap
;
2356 isl_basic_map_free(bmap
);
2360 __isl_give isl_map
*isl_map_read_from_file(struct isl_ctx
*ctx
,
2361 FILE *input
, int nparam
)
2363 struct isl_map
*map
;
2364 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2367 map
= isl_stream_read_map(s
, nparam
);
2372 __isl_give isl_map
*isl_map_read_from_str(struct isl_ctx
*ctx
,
2373 const char *str
, int nparam
)
2375 struct isl_map
*map
;
2376 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2379 map
= isl_stream_read_map(s
, nparam
);
2384 __isl_give isl_set
*isl_set_read_from_file(struct isl_ctx
*ctx
,
2385 FILE *input
, int nparam
)
2387 struct isl_map
*map
;
2388 map
= isl_map_read_from_file(ctx
, input
, nparam
);
2391 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2392 return (struct isl_set
*)map
;
2398 struct isl_set
*isl_set_read_from_str(struct isl_ctx
*ctx
,
2399 const char *str
, int nparam
)
2401 struct isl_map
*map
;
2402 map
= isl_map_read_from_str(ctx
, str
, nparam
);
2405 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2406 return (struct isl_set
*)map
;
2412 __isl_give isl_union_map
*isl_union_map_read_from_file(isl_ctx
*ctx
,
2415 isl_union_map
*umap
;
2416 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2419 umap
= isl_stream_read_union_map(s
);
2424 __isl_give isl_union_map
*isl_union_map_read_from_str(struct isl_ctx
*ctx
,
2427 isl_union_map
*umap
;
2428 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2431 umap
= isl_stream_read_union_map(s
);
2436 __isl_give isl_union_set
*isl_union_set_read_from_file(isl_ctx
*ctx
,
2439 isl_union_set
*uset
;
2440 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2443 uset
= isl_stream_read_union_set(s
);
2448 __isl_give isl_union_set
*isl_union_set_read_from_str(struct isl_ctx
*ctx
,
2451 isl_union_set
*uset
;
2452 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2455 uset
= isl_stream_read_union_set(s
);
2460 static __isl_give isl_vec
*isl_vec_read_polylib(struct isl_stream
*s
)
2462 struct isl_vec
*vec
= NULL
;
2463 struct isl_token
*tok
;
2467 tok
= isl_stream_next_token(s
);
2468 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2469 isl_stream_error(s
, tok
, "expecting vector length");
2473 size
= isl_int_get_si(tok
->u
.v
);
2474 isl_token_free(tok
);
2476 vec
= isl_vec_alloc(s
->ctx
, size
);
2478 for (j
= 0; j
< size
; ++j
) {
2479 tok
= isl_stream_next_token(s
);
2480 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2481 isl_stream_error(s
, tok
, "expecting constant value");
2484 isl_int_set(vec
->el
[j
], tok
->u
.v
);
2485 isl_token_free(tok
);
2490 isl_token_free(tok
);
2495 static __isl_give isl_vec
*vec_read(struct isl_stream
*s
)
2497 return isl_vec_read_polylib(s
);
2500 __isl_give isl_vec
*isl_vec_read_from_file(isl_ctx
*ctx
, FILE *input
)
2503 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2511 __isl_give isl_pw_qpolynomial
*isl_stream_read_pw_qpolynomial(
2512 struct isl_stream
*s
)
2515 struct isl_pw_qpolynomial
*pwqp
;
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
);