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
)
1262 bmap
= isl_basic_set_unwrap(isl_basic_set_lift(isl_basic_map_wrap(bmap
)));
1263 total
= isl_basic_map_total_dim(bmap
);
1264 while (v
->n
< total
)
1265 if (vars_add_anon(v
) < 0)
1268 bmap
= add_constraint(s
, v
, bmap
);
1269 bmap
= isl_basic_map_simplify(bmap
);
1270 bmap
= isl_basic_map_finalize(bmap
);
1272 map
= isl_map_from_basic_map(bmap
);
1274 map
= add_minmax(map
, v
, n
);
1276 map
= isl_set_unwrap(isl_map_domain(map
));
1278 vars_drop(v
, v
->n
- n
);
1282 isl_basic_map_free(bmap
);
1286 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1287 struct vars
*v
, __isl_take isl_basic_map
*bmap
);
1289 static __isl_give isl_map
*read_exists(struct isl_stream
*s
,
1290 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1293 int seen_paren
= isl_stream_eat_if_available(s
, '(');
1294 isl_map
*map
= NULL
;
1296 bmap
= isl_basic_map_from_domain(isl_basic_map_wrap(bmap
));
1297 bmap
= read_defined_var_list(s
, v
, bmap
);
1299 if (isl_stream_eat(s
, ':'))
1302 map
= read_disjuncts(s
, v
, bmap
);
1303 map
= isl_set_unwrap(isl_map_domain(map
));
1306 vars_drop(v
, v
->n
- n
);
1307 if (seen_paren
&& isl_stream_eat(s
, ')'))
1312 isl_basic_map_free(bmap
);
1317 static __isl_give isl_map
*read_conjunct(struct isl_stream
*s
,
1318 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1322 if (isl_stream_eat_if_available(s
, '(')) {
1323 map
= read_disjuncts(s
, v
, bmap
);
1324 if (isl_stream_eat(s
, ')'))
1329 if (isl_stream_eat_if_available(s
, ISL_TOKEN_EXISTS
))
1330 return read_exists(s
, v
, bmap
);
1332 if (isl_stream_eat_if_available(s
, ISL_TOKEN_TRUE
))
1333 return isl_map_from_basic_map(bmap
);
1335 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FALSE
)) {
1336 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1337 isl_basic_map_free(bmap
);
1338 return isl_map_empty(dim
);
1341 return read_constraint(s
, v
, bmap
);
1347 static __isl_give isl_map
*read_conjuncts(struct isl_stream
*s
,
1348 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1353 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1354 map
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1357 t
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1358 map
= isl_map_subtract(t
, map
);
1361 while (isl_stream_eat_if_available(s
, ISL_TOKEN_AND
)) {
1364 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1365 map_i
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1367 map
= isl_map_subtract(map
, map_i
);
1369 map
= isl_map_intersect(map
, map_i
);
1372 isl_basic_map_free(bmap
);
1376 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1377 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1379 struct isl_map
*map
;
1381 if (isl_stream_next_token_is(s
, '}')) {
1382 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1383 isl_basic_map_free(bmap
);
1384 return isl_map_universe(dim
);
1387 map
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1388 while (isl_stream_eat_if_available(s
, ISL_TOKEN_OR
)) {
1391 map_i
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1392 map
= isl_map_union(map
, map_i
);
1395 isl_basic_map_free(bmap
);
1399 static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map
*bmap
, int pos
)
1401 if (pos
< isl_basic_map_dim(bmap
, isl_dim_out
))
1402 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1403 isl_basic_map_dim(bmap
, isl_dim_in
) + pos
;
1404 pos
-= isl_basic_map_dim(bmap
, isl_dim_out
);
1406 if (pos
< isl_basic_map_dim(bmap
, isl_dim_in
))
1407 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) + pos
;
1408 pos
-= isl_basic_map_dim(bmap
, isl_dim_in
);
1410 if (pos
< isl_basic_map_dim(bmap
, isl_dim_div
))
1411 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1412 isl_basic_map_dim(bmap
, isl_dim_in
) +
1413 isl_basic_map_dim(bmap
, isl_dim_out
) + pos
;
1414 pos
-= isl_basic_map_dim(bmap
, isl_dim_div
);
1416 if (pos
< isl_basic_map_dim(bmap
, isl_dim_param
))
1422 static __isl_give isl_basic_map
*basic_map_read_polylib_constraint(
1423 struct isl_stream
*s
, __isl_take isl_basic_map
*bmap
)
1426 struct isl_token
*tok
;
1436 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
1437 dim
= isl_basic_map_dim(bmap
, isl_dim_out
);
1439 tok
= isl_stream_next_token(s
);
1440 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1441 isl_stream_error(s
, tok
, "expecting coefficient");
1443 isl_stream_push_token(s
, tok
);
1446 if (!tok
->on_new_line
) {
1447 isl_stream_error(s
, tok
, "coefficient should appear on new line");
1448 isl_stream_push_token(s
, tok
);
1452 type
= isl_int_get_si(tok
->u
.v
);
1453 isl_token_free(tok
);
1455 isl_assert(s
->ctx
, type
== 0 || type
== 1, goto error
);
1457 k
= isl_basic_map_alloc_equality(bmap
);
1460 k
= isl_basic_map_alloc_inequality(bmap
);
1466 for (j
= 0; j
< 1 + isl_basic_map_total_dim(bmap
); ++j
) {
1468 tok
= isl_stream_next_token(s
);
1469 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1470 isl_stream_error(s
, tok
, "expecting coefficient");
1472 isl_stream_push_token(s
, tok
);
1475 if (tok
->on_new_line
) {
1476 isl_stream_error(s
, tok
,
1477 "coefficient should not appear on new line");
1478 isl_stream_push_token(s
, tok
);
1481 pos
= polylib_pos_to_isl_pos(bmap
, j
);
1482 isl_int_set(c
[pos
], tok
->u
.v
);
1483 isl_token_free(tok
);
1488 isl_basic_map_free(bmap
);
1492 static __isl_give isl_basic_map
*basic_map_read_polylib(struct isl_stream
*s
,
1496 struct isl_token
*tok
;
1497 struct isl_token
*tok2
;
1500 unsigned in
= 0, out
, local
= 0;
1501 struct isl_basic_map
*bmap
= NULL
;
1506 tok
= isl_stream_next_token(s
);
1508 isl_stream_error(s
, NULL
, "unexpected EOF");
1511 tok2
= isl_stream_next_token(s
);
1513 isl_token_free(tok
);
1514 isl_stream_error(s
, NULL
, "unexpected EOF");
1517 if (tok
->type
!= ISL_TOKEN_VALUE
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1518 isl_stream_push_token(s
, tok2
);
1519 isl_stream_push_token(s
, tok
);
1520 isl_stream_error(s
, NULL
,
1521 "expecting constraint matrix dimensions");
1524 n_row
= isl_int_get_si(tok
->u
.v
);
1525 n_col
= isl_int_get_si(tok2
->u
.v
);
1526 on_new_line
= tok2
->on_new_line
;
1527 isl_token_free(tok2
);
1528 isl_token_free(tok
);
1529 isl_assert(s
->ctx
, !on_new_line
, return NULL
);
1530 isl_assert(s
->ctx
, n_row
>= 0, return NULL
);
1531 isl_assert(s
->ctx
, n_col
>= 2 + nparam
, return NULL
);
1532 tok
= isl_stream_next_token_on_same_line(s
);
1534 if (tok
->type
!= ISL_TOKEN_VALUE
) {
1535 isl_stream_error(s
, tok
,
1536 "expecting number of output dimensions");
1537 isl_stream_push_token(s
, tok
);
1540 out
= isl_int_get_si(tok
->u
.v
);
1541 isl_token_free(tok
);
1543 tok
= isl_stream_next_token_on_same_line(s
);
1544 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1545 isl_stream_error(s
, tok
,
1546 "expecting number of input dimensions");
1548 isl_stream_push_token(s
, tok
);
1551 in
= isl_int_get_si(tok
->u
.v
);
1552 isl_token_free(tok
);
1554 tok
= isl_stream_next_token_on_same_line(s
);
1555 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1556 isl_stream_error(s
, tok
,
1557 "expecting number of existentials");
1559 isl_stream_push_token(s
, tok
);
1562 local
= isl_int_get_si(tok
->u
.v
);
1563 isl_token_free(tok
);
1565 tok
= isl_stream_next_token_on_same_line(s
);
1566 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1567 isl_stream_error(s
, tok
,
1568 "expecting number of parameters");
1570 isl_stream_push_token(s
, tok
);
1573 nparam
= isl_int_get_si(tok
->u
.v
);
1574 isl_token_free(tok
);
1575 if (n_col
!= 1 + out
+ in
+ local
+ nparam
+ 1) {
1576 isl_stream_error(s
, NULL
,
1577 "dimensions don't match");
1581 out
= n_col
- 2 - nparam
;
1582 bmap
= isl_basic_map_alloc(s
->ctx
, nparam
, in
, out
, local
, n_row
, n_row
);
1586 for (i
= 0; i
< local
; ++i
) {
1587 int k
= isl_basic_map_alloc_div(bmap
);
1590 isl_seq_clr(bmap
->div
[k
], 1 + 1 + nparam
+ in
+ out
+ local
);
1593 for (i
= 0; i
< n_row
; ++i
)
1594 bmap
= basic_map_read_polylib_constraint(s
, bmap
);
1596 tok
= isl_stream_next_token_on_same_line(s
);
1598 isl_stream_error(s
, tok
, "unexpected extra token on line");
1599 isl_stream_push_token(s
, tok
);
1603 bmap
= isl_basic_map_simplify(bmap
);
1604 bmap
= isl_basic_map_finalize(bmap
);
1607 isl_basic_map_free(bmap
);
1611 static struct isl_map
*map_read_polylib(struct isl_stream
*s
, int nparam
)
1613 struct isl_token
*tok
;
1614 struct isl_token
*tok2
;
1616 struct isl_map
*map
;
1618 tok
= isl_stream_next_token(s
);
1620 isl_stream_error(s
, NULL
, "unexpected EOF");
1623 tok2
= isl_stream_next_token_on_same_line(s
);
1624 if (tok2
&& tok2
->type
== ISL_TOKEN_VALUE
) {
1625 isl_stream_push_token(s
, tok2
);
1626 isl_stream_push_token(s
, tok
);
1627 return isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1630 isl_stream_error(s
, tok2
, "unexpected token");
1631 isl_stream_push_token(s
, tok2
);
1632 isl_stream_push_token(s
, tok
);
1635 n
= isl_int_get_si(tok
->u
.v
);
1636 isl_token_free(tok
);
1638 isl_assert(s
->ctx
, n
>= 1, return NULL
);
1640 map
= isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1642 for (i
= 1; map
&& i
< n
; ++i
)
1643 map
= isl_map_union(map
,
1644 isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
)));
1649 static int optional_power(struct isl_stream
*s
)
1652 struct isl_token
*tok
;
1654 tok
= isl_stream_next_token(s
);
1657 if (tok
->type
!= '^') {
1658 isl_stream_push_token(s
, tok
);
1661 isl_token_free(tok
);
1662 tok
= isl_stream_next_token(s
);
1663 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1664 isl_stream_error(s
, tok
, "expecting exponent");
1666 isl_stream_push_token(s
, tok
);
1669 pow
= isl_int_get_si(tok
->u
.v
);
1670 isl_token_free(tok
);
1674 static __isl_give isl_div
*read_div(struct isl_stream
*s
,
1675 __isl_take isl_dim
*dim
, struct vars
*v
)
1678 isl_basic_map
*bmap
;
1681 bmap
= isl_basic_map_universe(dim
);
1683 if (vars_add_anon(v
) < 0)
1685 if (read_div_definition(s
, v
) < 0)
1687 bmap
= add_divs(bmap
, v
);
1688 bmap
= isl_basic_map_order_divs(bmap
);
1691 vars_drop(v
, v
->n
- n
);
1693 return isl_basic_map_div(bmap
, bmap
->n_div
- 1);
1695 isl_basic_map_free(bmap
);
1699 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1700 __isl_keep isl_basic_map
*bmap
, struct vars
*v
);
1702 static __isl_give isl_qpolynomial
*read_factor(struct isl_stream
*s
,
1703 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1705 struct isl_qpolynomial
*qp
;
1706 struct isl_token
*tok
;
1708 tok
= next_token(s
);
1710 isl_stream_error(s
, NULL
, "unexpected EOF");
1713 if (tok
->type
== '(') {
1716 isl_token_free(tok
);
1717 qp
= read_term(s
, bmap
, v
);
1720 if (isl_stream_eat(s
, ')'))
1722 pow
= optional_power(s
);
1723 qp
= isl_qpolynomial_pow(qp
, pow
);
1724 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
1725 struct isl_token
*tok2
;
1726 tok2
= isl_stream_next_token(s
);
1727 if (tok2
&& tok2
->type
== '/') {
1728 isl_token_free(tok2
);
1729 tok2
= next_token(s
);
1730 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1731 isl_stream_error(s
, tok2
, "expected denominator");
1732 isl_token_free(tok
);
1733 isl_token_free(tok2
);
1736 qp
= isl_qpolynomial_rat_cst(isl_basic_map_get_dim(bmap
),
1737 tok
->u
.v
, tok2
->u
.v
);
1738 isl_token_free(tok2
);
1740 isl_stream_push_token(s
, tok2
);
1741 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1744 isl_token_free(tok
);
1745 } else if (tok
->type
== ISL_TOKEN_INFTY
) {
1746 isl_token_free(tok
);
1747 qp
= isl_qpolynomial_infty(isl_basic_map_get_dim(bmap
));
1748 } else if (tok
->type
== ISL_TOKEN_NAN
) {
1749 isl_token_free(tok
);
1750 qp
= isl_qpolynomial_nan(isl_basic_map_get_dim(bmap
));
1751 } else if (tok
->type
== ISL_TOKEN_IDENT
) {
1753 int pos
= vars_pos(v
, tok
->u
.s
, -1);
1756 isl_token_free(tok
);
1760 vars_drop(v
, v
->n
- n
);
1761 isl_stream_error(s
, tok
, "unknown identifier");
1762 isl_token_free(tok
);
1765 isl_token_free(tok
);
1766 pow
= optional_power(s
);
1767 qp
= isl_qpolynomial_var_pow(isl_basic_map_get_dim(bmap
), pos
, pow
);
1768 } else if (tok
->type
== '[') {
1772 isl_stream_push_token(s
, tok
);
1773 div
= read_div(s
, isl_basic_map_get_dim(bmap
), v
);
1774 pow
= optional_power(s
);
1775 qp
= isl_qpolynomial_div_pow(div
, pow
);
1776 } else if (tok
->type
== '-') {
1777 struct isl_qpolynomial
*qp2
;
1779 isl_token_free(tok
);
1780 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1782 qp2
= read_factor(s
, bmap
, v
);
1783 qp
= isl_qpolynomial_mul(qp
, qp2
);
1785 isl_stream_error(s
, tok
, "unexpected isl_token");
1786 isl_stream_push_token(s
, tok
);
1790 if (isl_stream_eat_if_available(s
, '*') ||
1791 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
1792 struct isl_qpolynomial
*qp2
;
1794 qp2
= read_factor(s
, bmap
, v
);
1795 qp
= isl_qpolynomial_mul(qp
, qp2
);
1800 isl_qpolynomial_free(qp
);
1804 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1805 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1807 struct isl_token
*tok
;
1808 struct isl_qpolynomial
*qp
;
1810 qp
= read_factor(s
, bmap
, v
);
1813 tok
= next_token(s
);
1817 if (tok
->type
== '+') {
1818 struct isl_qpolynomial
*qp2
;
1820 isl_token_free(tok
);
1821 qp2
= read_factor(s
, bmap
, v
);
1822 qp
= isl_qpolynomial_add(qp
, qp2
);
1823 } else if (tok
->type
== '-') {
1824 struct isl_qpolynomial
*qp2
;
1826 isl_token_free(tok
);
1827 qp2
= read_factor(s
, bmap
, v
);
1828 qp
= isl_qpolynomial_sub(qp
, qp2
);
1829 } else if (tok
->type
== ISL_TOKEN_VALUE
&&
1830 isl_int_is_neg(tok
->u
.v
)) {
1831 struct isl_qpolynomial
*qp2
;
1833 isl_stream_push_token(s
, tok
);
1834 qp2
= read_factor(s
, bmap
, v
);
1835 qp
= isl_qpolynomial_add(qp
, qp2
);
1837 isl_stream_push_token(s
, tok
);
1845 static __isl_give isl_map
*read_optional_disjuncts(struct isl_stream
*s
,
1846 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1848 struct isl_token
*tok
;
1849 struct isl_map
*map
;
1851 tok
= isl_stream_next_token(s
);
1853 isl_stream_error(s
, NULL
, "unexpected EOF");
1856 map
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1857 if (tok
->type
== ':' ||
1858 (tok
->type
== ISL_TOKEN_OR
&& !strcmp(tok
->u
.s
, "|"))) {
1859 isl_token_free(tok
);
1860 map
= isl_map_intersect(map
,
1861 read_disjuncts(s
, v
, isl_basic_map_copy(bmap
)));
1863 isl_stream_push_token(s
, tok
);
1865 isl_basic_map_free(bmap
);
1869 isl_basic_map_free(bmap
);
1873 static struct isl_obj
obj_read_poly(struct isl_stream
*s
,
1874 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1876 struct isl_obj obj
= { isl_obj_pw_qpolynomial
, NULL
};
1877 struct isl_pw_qpolynomial
*pwqp
;
1878 struct isl_qpolynomial
*qp
;
1879 struct isl_map
*map
;
1880 struct isl_set
*set
;
1882 qp
= read_term(s
, bmap
, v
);
1883 map
= read_optional_disjuncts(s
, bmap
, v
);
1884 set
= isl_map_range(map
);
1886 pwqp
= isl_pw_qpolynomial_alloc(set
, qp
);
1888 vars_drop(v
, v
->n
- n
);
1894 static struct isl_obj
obj_read_poly_or_fold(struct isl_stream
*s
,
1895 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1897 struct isl_obj obj
= { isl_obj_pw_qpolynomial_fold
, NULL
};
1898 struct isl_obj obj_p
;
1899 isl_qpolynomial
*qp
;
1900 isl_qpolynomial_fold
*fold
= NULL
;
1901 isl_pw_qpolynomial_fold
*pwf
;
1905 if (!isl_stream_eat_if_available(s
, ISL_TOKEN_MAX
))
1906 return obj_read_poly(s
, bmap
, v
, n
);
1908 if (isl_stream_eat(s
, '('))
1911 qp
= read_term(s
, bmap
, v
);
1912 fold
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1914 while (isl_stream_eat_if_available(s
, ',')) {
1915 isl_qpolynomial_fold
*fold_i
;
1916 qp
= read_term(s
, bmap
, v
);
1917 fold_i
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1918 fold
= isl_qpolynomial_fold_fold(fold
, fold_i
);
1921 if (isl_stream_eat(s
, ')'))
1924 map
= read_optional_disjuncts(s
, bmap
, v
);
1925 set
= isl_map_range(map
);
1926 pwf
= isl_pw_qpolynomial_fold_alloc(isl_fold_max
, set
, fold
);
1928 vars_drop(v
, v
->n
- n
);
1933 isl_basic_map_free(bmap
);
1934 isl_qpolynomial_fold_free(fold
);
1935 obj
.type
= isl_obj_none
;
1939 static int is_rational(struct isl_stream
*s
)
1941 struct isl_token
*tok
;
1943 tok
= isl_stream_next_token(s
);
1946 if (tok
->type
== ISL_TOKEN_RAT
&& isl_stream_next_token_is(s
, ':')) {
1947 isl_token_free(tok
);
1948 isl_stream_eat(s
, ':');
1952 isl_stream_push_token(s
, tok
);
1957 static struct isl_obj
obj_read_body(struct isl_stream
*s
,
1958 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1960 struct isl_map
*map
= NULL
;
1961 struct isl_token
*tok
;
1962 struct isl_obj obj
= { isl_obj_set
, NULL
};
1966 bmap
= isl_basic_map_set_rational(bmap
);
1968 if (!next_is_tuple(s
))
1969 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1971 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
1974 tok
= isl_stream_next_token(s
);
1975 if (tok
&& tok
->type
== ISL_TOKEN_TO
) {
1976 obj
.type
= isl_obj_map
;
1977 isl_token_free(tok
);
1978 if (!next_is_tuple(s
)) {
1979 bmap
= isl_basic_map_reverse(bmap
);
1980 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1982 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
1986 bmap
= isl_basic_map_reverse(bmap
);
1988 isl_stream_push_token(s
, tok
);
1991 map
= read_optional_disjuncts(s
, bmap
, v
);
1993 vars_drop(v
, v
->n
- n
);
1998 isl_basic_map_free(bmap
);
1999 obj
.type
= isl_obj_none
;
2003 static struct isl_obj
to_union(isl_ctx
*ctx
, struct isl_obj obj
)
2005 if (obj
.type
== isl_obj_map
) {
2006 obj
.v
= isl_union_map_from_map(obj
.v
);
2007 obj
.type
= isl_obj_union_map
;
2008 } else if (obj
.type
== isl_obj_set
) {
2009 obj
.v
= isl_union_set_from_set(obj
.v
);
2010 obj
.type
= isl_obj_union_set
;
2011 } else if (obj
.type
== isl_obj_pw_qpolynomial
) {
2012 obj
.v
= isl_union_pw_qpolynomial_from_pw_qpolynomial(obj
.v
);
2013 obj
.type
= isl_obj_union_pw_qpolynomial
;
2014 } else if (obj
.type
== isl_obj_pw_qpolynomial_fold
) {
2015 obj
.v
= isl_union_pw_qpolynomial_fold_from_pw_qpolynomial_fold(obj
.v
);
2016 obj
.type
= isl_obj_union_pw_qpolynomial_fold
;
2018 isl_assert(ctx
, 0, goto error
);
2021 obj
.type
->free(obj
.v
);
2022 obj
.type
= isl_obj_none
;
2026 static struct isl_obj
obj_add(struct isl_ctx
*ctx
,
2027 struct isl_obj obj1
, struct isl_obj obj2
)
2029 if (obj1
.type
== isl_obj_set
&& obj2
.type
== isl_obj_union_set
)
2030 obj1
= to_union(ctx
, obj1
);
2031 if (obj1
.type
== isl_obj_union_set
&& obj2
.type
== isl_obj_set
)
2032 obj2
= to_union(ctx
, obj2
);
2033 if (obj1
.type
== isl_obj_map
&& obj2
.type
== isl_obj_union_map
)
2034 obj1
= to_union(ctx
, obj1
);
2035 if (obj1
.type
== isl_obj_union_map
&& obj2
.type
== isl_obj_map
)
2036 obj2
= to_union(ctx
, obj2
);
2037 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2038 obj2
.type
== isl_obj_union_pw_qpolynomial
)
2039 obj1
= to_union(ctx
, obj1
);
2040 if (obj1
.type
== isl_obj_union_pw_qpolynomial
&&
2041 obj2
.type
== isl_obj_pw_qpolynomial
)
2042 obj2
= to_union(ctx
, obj2
);
2043 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2044 obj2
.type
== isl_obj_union_pw_qpolynomial_fold
)
2045 obj1
= to_union(ctx
, obj1
);
2046 if (obj1
.type
== isl_obj_union_pw_qpolynomial_fold
&&
2047 obj2
.type
== isl_obj_pw_qpolynomial_fold
)
2048 obj2
= to_union(ctx
, obj2
);
2049 isl_assert(ctx
, obj1
.type
== obj2
.type
, goto error
);
2050 if (obj1
.type
== isl_obj_map
&& !isl_map_has_equal_dim(obj1
.v
, obj2
.v
)) {
2051 obj1
= to_union(ctx
, obj1
);
2052 obj2
= to_union(ctx
, obj2
);
2054 if (obj1
.type
== isl_obj_set
&& !isl_set_has_equal_dim(obj1
.v
, obj2
.v
)) {
2055 obj1
= to_union(ctx
, obj1
);
2056 obj2
= to_union(ctx
, obj2
);
2058 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2059 !isl_pw_qpolynomial_has_equal_dim(obj1
.v
, obj2
.v
)) {
2060 obj1
= to_union(ctx
, obj1
);
2061 obj2
= to_union(ctx
, obj2
);
2063 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2064 !isl_pw_qpolynomial_fold_has_equal_dim(obj1
.v
, obj2
.v
)) {
2065 obj1
= to_union(ctx
, obj1
);
2066 obj2
= to_union(ctx
, obj2
);
2068 obj1
.v
= obj1
.type
->add(obj1
.v
, obj2
.v
);
2071 obj1
.type
->free(obj1
.v
);
2072 obj2
.type
->free(obj2
.v
);
2073 obj1
.type
= isl_obj_none
;
2078 static struct isl_obj
obj_read(struct isl_stream
*s
, int nparam
)
2080 isl_basic_map
*bmap
= NULL
;
2081 struct isl_token
*tok
;
2082 struct vars
*v
= NULL
;
2083 struct isl_obj obj
= { isl_obj_set
, NULL
};
2085 tok
= next_token(s
);
2087 isl_stream_error(s
, NULL
, "unexpected EOF");
2090 if (tok
->type
== ISL_TOKEN_VALUE
) {
2091 struct isl_token
*tok2
;
2092 struct isl_map
*map
;
2094 tok2
= isl_stream_next_token(s
);
2095 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
||
2096 isl_int_is_neg(tok2
->u
.v
)) {
2098 isl_stream_push_token(s
, tok2
);
2099 obj
.type
= isl_obj_int
;
2100 obj
.v
= isl_int_obj_alloc(s
->ctx
, tok
->u
.v
);
2101 isl_token_free(tok
);
2104 isl_stream_push_token(s
, tok2
);
2105 isl_stream_push_token(s
, tok
);
2106 map
= map_read_polylib(s
, nparam
);
2109 if (isl_map_dim(map
, isl_dim_in
) > 0)
2110 obj
.type
= isl_obj_map
;
2114 v
= vars_new(s
->ctx
);
2116 isl_stream_push_token(s
, tok
);
2119 bmap
= isl_basic_map_alloc(s
->ctx
, 0, 0, 0, 0, 0, 0);
2120 if (tok
->type
== '[') {
2121 isl_stream_push_token(s
, tok
);
2122 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2126 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2127 tok
= isl_stream_next_token(s
);
2128 if (!tok
|| tok
->type
!= ISL_TOKEN_TO
) {
2129 isl_stream_error(s
, tok
, "expecting '->'");
2131 isl_stream_push_token(s
, tok
);
2134 isl_token_free(tok
);
2135 tok
= isl_stream_next_token(s
);
2136 } else if (nparam
> 0)
2137 bmap
= isl_basic_map_add(bmap
, isl_dim_param
, nparam
);
2138 if (!tok
|| tok
->type
!= '{') {
2139 isl_stream_error(s
, tok
, "expecting '{'");
2141 isl_stream_push_token(s
, tok
);
2144 isl_token_free(tok
);
2146 tok
= isl_stream_next_token(s
);
2149 else if (tok
->type
== ISL_TOKEN_IDENT
&& !strcmp(tok
->u
.s
, "Sym")) {
2150 isl_token_free(tok
);
2151 if (isl_stream_eat(s
, '='))
2153 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2157 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2158 } else if (tok
->type
== '}') {
2159 obj
.type
= isl_obj_union_set
;
2160 obj
.v
= isl_union_set_empty(isl_basic_map_get_dim(bmap
));
2161 isl_token_free(tok
);
2164 isl_stream_push_token(s
, tok
);
2169 o
= obj_read_body(s
, isl_basic_map_copy(bmap
), v
);
2170 if (o
.type
== isl_obj_none
|| !o
.v
)
2175 obj
= obj_add(s
->ctx
, obj
, o
);
2176 if (obj
.type
== isl_obj_none
|| !obj
.v
)
2179 tok
= isl_stream_next_token(s
);
2180 if (!tok
|| tok
->type
!= ';')
2182 isl_token_free(tok
);
2183 if (isl_stream_next_token_is(s
, '}')) {
2184 tok
= isl_stream_next_token(s
);
2189 if (tok
&& tok
->type
== '}') {
2190 isl_token_free(tok
);
2192 isl_stream_error(s
, tok
, "unexpected isl_token");
2194 isl_token_free(tok
);
2199 isl_basic_map_free(bmap
);
2203 isl_basic_map_free(bmap
);
2204 obj
.type
->free(obj
.v
);
2211 struct isl_obj
isl_stream_read_obj(struct isl_stream
*s
)
2213 return obj_read(s
, -1);
2216 __isl_give isl_map
*isl_stream_read_map(struct isl_stream
*s
, int nparam
)
2219 struct isl_map
*map
;
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
)
2235 struct isl_set
*set
;
2237 obj
= obj_read(s
, nparam
);
2239 isl_assert(s
->ctx
, obj
.type
== isl_obj_set
, goto error
);
2243 obj
.type
->free(obj
.v
);
2247 __isl_give isl_union_map
*isl_stream_read_union_map(struct isl_stream
*s
)
2250 isl_union_map
*umap
;
2252 obj
= obj_read(s
, -1);
2253 if (obj
.type
== isl_obj_map
) {
2254 obj
.type
= isl_obj_union_map
;
2255 obj
.v
= isl_union_map_from_map(obj
.v
);
2257 if (obj
.type
== isl_obj_set
) {
2258 obj
.type
= isl_obj_union_set
;
2259 obj
.v
= isl_union_set_from_set(obj
.v
);
2262 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_map
||
2263 obj
.type
== isl_obj_union_set
, goto error
);
2267 obj
.type
->free(obj
.v
);
2271 __isl_give isl_union_set
*isl_stream_read_union_set(struct isl_stream
*s
)
2274 isl_union_set
*uset
;
2276 obj
= obj_read(s
, -1);
2277 if (obj
.type
== isl_obj_set
) {
2278 obj
.type
= isl_obj_union_set
;
2279 obj
.v
= isl_union_set_from_set(obj
.v
);
2282 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_set
, goto error
);
2286 obj
.type
->free(obj
.v
);
2290 static struct isl_basic_map
*basic_map_read(struct isl_stream
*s
, int nparam
)
2293 struct isl_map
*map
;
2294 struct isl_basic_map
*bmap
;
2296 obj
= obj_read(s
, nparam
);
2301 isl_assert(map
->ctx
, map
->n
<= 1, goto error
);
2304 bmap
= isl_basic_map_empty_like_map(map
);
2306 bmap
= isl_basic_map_copy(map
->p
[0]);
2316 __isl_give isl_basic_map
*isl_basic_map_read_from_file(isl_ctx
*ctx
,
2317 FILE *input
, int nparam
)
2319 struct isl_basic_map
*bmap
;
2320 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2323 bmap
= basic_map_read(s
, nparam
);
2328 __isl_give isl_basic_set
*isl_basic_set_read_from_file(isl_ctx
*ctx
,
2329 FILE *input
, int nparam
)
2331 struct isl_basic_map
*bmap
;
2332 bmap
= isl_basic_map_read_from_file(ctx
, input
, nparam
);
2335 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2336 return (struct isl_basic_set
*)bmap
;
2338 isl_basic_map_free(bmap
);
2342 struct isl_basic_map
*isl_basic_map_read_from_str(struct isl_ctx
*ctx
,
2343 const char *str
, int nparam
)
2345 struct isl_basic_map
*bmap
;
2346 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2349 bmap
= basic_map_read(s
, nparam
);
2354 struct isl_basic_set
*isl_basic_set_read_from_str(struct isl_ctx
*ctx
,
2355 const char *str
, int nparam
)
2357 struct isl_basic_map
*bmap
;
2358 bmap
= isl_basic_map_read_from_str(ctx
, str
, nparam
);
2361 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2362 return (struct isl_basic_set
*)bmap
;
2364 isl_basic_map_free(bmap
);
2368 __isl_give isl_map
*isl_map_read_from_file(struct isl_ctx
*ctx
,
2369 FILE *input
, int nparam
)
2371 struct isl_map
*map
;
2372 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2375 map
= isl_stream_read_map(s
, nparam
);
2380 __isl_give isl_map
*isl_map_read_from_str(struct isl_ctx
*ctx
,
2381 const char *str
, int nparam
)
2383 struct isl_map
*map
;
2384 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2387 map
= isl_stream_read_map(s
, nparam
);
2392 __isl_give isl_set
*isl_set_read_from_file(struct isl_ctx
*ctx
,
2393 FILE *input
, int nparam
)
2395 struct isl_map
*map
;
2396 map
= isl_map_read_from_file(ctx
, input
, nparam
);
2399 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2400 return (struct isl_set
*)map
;
2406 struct isl_set
*isl_set_read_from_str(struct isl_ctx
*ctx
,
2407 const char *str
, int nparam
)
2409 struct isl_map
*map
;
2410 map
= isl_map_read_from_str(ctx
, str
, nparam
);
2413 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2414 return (struct isl_set
*)map
;
2420 __isl_give isl_union_map
*isl_union_map_read_from_file(isl_ctx
*ctx
,
2423 isl_union_map
*umap
;
2424 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2427 umap
= isl_stream_read_union_map(s
);
2432 __isl_give isl_union_map
*isl_union_map_read_from_str(struct isl_ctx
*ctx
,
2435 isl_union_map
*umap
;
2436 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2439 umap
= isl_stream_read_union_map(s
);
2444 __isl_give isl_union_set
*isl_union_set_read_from_file(isl_ctx
*ctx
,
2447 isl_union_set
*uset
;
2448 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2451 uset
= isl_stream_read_union_set(s
);
2456 __isl_give isl_union_set
*isl_union_set_read_from_str(struct isl_ctx
*ctx
,
2459 isl_union_set
*uset
;
2460 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2463 uset
= isl_stream_read_union_set(s
);
2468 static __isl_give isl_vec
*isl_vec_read_polylib(struct isl_stream
*s
)
2470 struct isl_vec
*vec
= NULL
;
2471 struct isl_token
*tok
;
2475 tok
= isl_stream_next_token(s
);
2476 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2477 isl_stream_error(s
, tok
, "expecting vector length");
2481 size
= isl_int_get_si(tok
->u
.v
);
2482 isl_token_free(tok
);
2484 vec
= isl_vec_alloc(s
->ctx
, size
);
2486 for (j
= 0; j
< size
; ++j
) {
2487 tok
= isl_stream_next_token(s
);
2488 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2489 isl_stream_error(s
, tok
, "expecting constant value");
2492 isl_int_set(vec
->el
[j
], tok
->u
.v
);
2493 isl_token_free(tok
);
2498 isl_token_free(tok
);
2503 static __isl_give isl_vec
*vec_read(struct isl_stream
*s
)
2505 return isl_vec_read_polylib(s
);
2508 __isl_give isl_vec
*isl_vec_read_from_file(isl_ctx
*ctx
, FILE *input
)
2511 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2519 __isl_give isl_pw_qpolynomial
*isl_stream_read_pw_qpolynomial(
2520 struct isl_stream
*s
)
2523 struct isl_pw_qpolynomial
*pwqp
;
2525 obj
= obj_read(s
, -1);
2527 isl_assert(s
->ctx
, obj
.type
== isl_obj_pw_qpolynomial
,
2532 obj
.type
->free(obj
.v
);
2536 __isl_give isl_pw_qpolynomial
*isl_pw_qpolynomial_read_from_str(isl_ctx
*ctx
,
2539 isl_pw_qpolynomial
*pwqp
;
2540 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2543 pwqp
= isl_stream_read_pw_qpolynomial(s
);