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
)
1235 struct variable
*var
;
1238 var
= first_minmax(v
, n
);
1241 if (all_coefficients_of_sign(map
, var
->pos
, -var
->sign
))
1242 map
= bound_minmax(map
, var
);
1244 map
= set_minmax(map
, var
);
1251 static isl_map
*read_constraint(struct isl_stream
*s
,
1252 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1261 bmap
= isl_basic_set_unwrap(isl_basic_set_lift(isl_basic_map_wrap(bmap
)));
1262 total
= isl_basic_map_total_dim(bmap
);
1263 while (v
->n
< total
)
1264 if (vars_add_anon(v
) < 0)
1267 bmap
= add_constraint(s
, v
, bmap
);
1268 bmap
= isl_basic_map_simplify(bmap
);
1269 bmap
= isl_basic_map_finalize(bmap
);
1271 map
= isl_map_from_basic_map(bmap
);
1273 map
= add_minmax(map
, v
, n
);
1275 map
= isl_set_unwrap(isl_map_domain(map
));
1277 vars_drop(v
, v
->n
- n
);
1281 isl_basic_map_free(bmap
);
1285 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1286 struct vars
*v
, __isl_take isl_basic_map
*bmap
);
1288 static __isl_give isl_map
*read_exists(struct isl_stream
*s
,
1289 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1292 int seen_paren
= isl_stream_eat_if_available(s
, '(');
1293 isl_map
*map
= NULL
;
1295 bmap
= isl_basic_map_from_domain(isl_basic_map_wrap(bmap
));
1296 bmap
= read_defined_var_list(s
, v
, bmap
);
1298 if (isl_stream_eat(s
, ':'))
1301 map
= read_disjuncts(s
, v
, bmap
);
1302 map
= isl_set_unwrap(isl_map_domain(map
));
1305 vars_drop(v
, v
->n
- n
);
1306 if (seen_paren
&& isl_stream_eat(s
, ')'))
1311 isl_basic_map_free(bmap
);
1316 static __isl_give isl_map
*read_conjunct(struct isl_stream
*s
,
1317 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1321 if (isl_stream_eat_if_available(s
, '(')) {
1322 map
= read_disjuncts(s
, v
, bmap
);
1323 if (isl_stream_eat(s
, ')'))
1328 if (isl_stream_eat_if_available(s
, ISL_TOKEN_EXISTS
))
1329 return read_exists(s
, v
, bmap
);
1331 if (isl_stream_eat_if_available(s
, ISL_TOKEN_TRUE
))
1332 return isl_map_from_basic_map(bmap
);
1334 if (isl_stream_eat_if_available(s
, ISL_TOKEN_FALSE
)) {
1335 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1336 isl_basic_map_free(bmap
);
1337 return isl_map_empty(dim
);
1340 return read_constraint(s
, v
, bmap
);
1346 static __isl_give isl_map
*read_conjuncts(struct isl_stream
*s
,
1347 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1352 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1353 map
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1356 t
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1357 map
= isl_map_subtract(t
, map
);
1360 while (isl_stream_eat_if_available(s
, ISL_TOKEN_AND
)) {
1363 negate
= isl_stream_eat_if_available(s
, ISL_TOKEN_NOT
);
1364 map_i
= read_conjunct(s
, v
, isl_basic_map_copy(bmap
));
1366 map
= isl_map_subtract(map
, map_i
);
1368 map
= isl_map_intersect(map
, map_i
);
1371 isl_basic_map_free(bmap
);
1375 static struct isl_map
*read_disjuncts(struct isl_stream
*s
,
1376 struct vars
*v
, __isl_take isl_basic_map
*bmap
)
1378 struct isl_map
*map
;
1380 if (isl_stream_next_token_is(s
, '}')) {
1381 isl_dim
*dim
= isl_basic_map_get_dim(bmap
);
1382 isl_basic_map_free(bmap
);
1383 return isl_map_universe(dim
);
1386 map
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1387 while (isl_stream_eat_if_available(s
, ISL_TOKEN_OR
)) {
1390 map_i
= read_conjuncts(s
, v
, isl_basic_map_copy(bmap
));
1391 map
= isl_map_union(map
, map_i
);
1394 isl_basic_map_free(bmap
);
1398 static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map
*bmap
, int pos
)
1400 if (pos
< isl_basic_map_dim(bmap
, isl_dim_out
))
1401 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1402 isl_basic_map_dim(bmap
, isl_dim_in
) + pos
;
1403 pos
-= isl_basic_map_dim(bmap
, isl_dim_out
);
1405 if (pos
< isl_basic_map_dim(bmap
, isl_dim_in
))
1406 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) + pos
;
1407 pos
-= isl_basic_map_dim(bmap
, isl_dim_in
);
1409 if (pos
< isl_basic_map_dim(bmap
, isl_dim_div
))
1410 return 1 + isl_basic_map_dim(bmap
, isl_dim_param
) +
1411 isl_basic_map_dim(bmap
, isl_dim_in
) +
1412 isl_basic_map_dim(bmap
, isl_dim_out
) + pos
;
1413 pos
-= isl_basic_map_dim(bmap
, isl_dim_div
);
1415 if (pos
< isl_basic_map_dim(bmap
, isl_dim_param
))
1421 static __isl_give isl_basic_map
*basic_map_read_polylib_constraint(
1422 struct isl_stream
*s
, __isl_take isl_basic_map
*bmap
)
1425 struct isl_token
*tok
;
1435 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
1436 dim
= isl_basic_map_dim(bmap
, isl_dim_out
);
1438 tok
= isl_stream_next_token(s
);
1439 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1440 isl_stream_error(s
, tok
, "expecting coefficient");
1442 isl_stream_push_token(s
, tok
);
1445 if (!tok
->on_new_line
) {
1446 isl_stream_error(s
, tok
, "coefficient should appear on new line");
1447 isl_stream_push_token(s
, tok
);
1451 type
= isl_int_get_si(tok
->u
.v
);
1452 isl_token_free(tok
);
1454 isl_assert(s
->ctx
, type
== 0 || type
== 1, goto error
);
1456 k
= isl_basic_map_alloc_equality(bmap
);
1459 k
= isl_basic_map_alloc_inequality(bmap
);
1465 for (j
= 0; j
< 1 + isl_basic_map_total_dim(bmap
); ++j
) {
1467 tok
= isl_stream_next_token(s
);
1468 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1469 isl_stream_error(s
, tok
, "expecting coefficient");
1471 isl_stream_push_token(s
, tok
);
1474 if (tok
->on_new_line
) {
1475 isl_stream_error(s
, tok
,
1476 "coefficient should not appear on new line");
1477 isl_stream_push_token(s
, tok
);
1480 pos
= polylib_pos_to_isl_pos(bmap
, j
);
1481 isl_int_set(c
[pos
], tok
->u
.v
);
1482 isl_token_free(tok
);
1487 isl_basic_map_free(bmap
);
1491 static __isl_give isl_basic_map
*basic_map_read_polylib(struct isl_stream
*s
,
1495 struct isl_token
*tok
;
1496 struct isl_token
*tok2
;
1499 unsigned in
= 0, out
, local
= 0;
1500 struct isl_basic_map
*bmap
= NULL
;
1505 tok
= isl_stream_next_token(s
);
1507 isl_stream_error(s
, NULL
, "unexpected EOF");
1510 tok2
= isl_stream_next_token(s
);
1512 isl_token_free(tok
);
1513 isl_stream_error(s
, NULL
, "unexpected EOF");
1516 if (tok
->type
!= ISL_TOKEN_VALUE
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1517 isl_stream_push_token(s
, tok2
);
1518 isl_stream_push_token(s
, tok
);
1519 isl_stream_error(s
, NULL
,
1520 "expecting constraint matrix dimensions");
1523 n_row
= isl_int_get_si(tok
->u
.v
);
1524 n_col
= isl_int_get_si(tok2
->u
.v
);
1525 on_new_line
= tok2
->on_new_line
;
1526 isl_token_free(tok2
);
1527 isl_token_free(tok
);
1528 isl_assert(s
->ctx
, !on_new_line
, return NULL
);
1529 isl_assert(s
->ctx
, n_row
>= 0, return NULL
);
1530 isl_assert(s
->ctx
, n_col
>= 2 + nparam
, return NULL
);
1531 tok
= isl_stream_next_token_on_same_line(s
);
1533 if (tok
->type
!= ISL_TOKEN_VALUE
) {
1534 isl_stream_error(s
, tok
,
1535 "expecting number of output dimensions");
1536 isl_stream_push_token(s
, tok
);
1539 out
= isl_int_get_si(tok
->u
.v
);
1540 isl_token_free(tok
);
1542 tok
= isl_stream_next_token_on_same_line(s
);
1543 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1544 isl_stream_error(s
, tok
,
1545 "expecting number of input dimensions");
1547 isl_stream_push_token(s
, tok
);
1550 in
= isl_int_get_si(tok
->u
.v
);
1551 isl_token_free(tok
);
1553 tok
= isl_stream_next_token_on_same_line(s
);
1554 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1555 isl_stream_error(s
, tok
,
1556 "expecting number of existentials");
1558 isl_stream_push_token(s
, tok
);
1561 local
= isl_int_get_si(tok
->u
.v
);
1562 isl_token_free(tok
);
1564 tok
= isl_stream_next_token_on_same_line(s
);
1565 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1566 isl_stream_error(s
, tok
,
1567 "expecting number of parameters");
1569 isl_stream_push_token(s
, tok
);
1572 nparam
= isl_int_get_si(tok
->u
.v
);
1573 isl_token_free(tok
);
1574 if (n_col
!= 1 + out
+ in
+ local
+ nparam
+ 1) {
1575 isl_stream_error(s
, NULL
,
1576 "dimensions don't match");
1580 out
= n_col
- 2 - nparam
;
1581 bmap
= isl_basic_map_alloc(s
->ctx
, nparam
, in
, out
, local
, n_row
, n_row
);
1585 for (i
= 0; i
< local
; ++i
) {
1586 int k
= isl_basic_map_alloc_div(bmap
);
1589 isl_seq_clr(bmap
->div
[k
], 1 + 1 + nparam
+ in
+ out
+ local
);
1592 for (i
= 0; i
< n_row
; ++i
)
1593 bmap
= basic_map_read_polylib_constraint(s
, bmap
);
1595 tok
= isl_stream_next_token_on_same_line(s
);
1597 isl_stream_error(s
, tok
, "unexpected extra token on line");
1598 isl_stream_push_token(s
, tok
);
1602 bmap
= isl_basic_map_simplify(bmap
);
1603 bmap
= isl_basic_map_finalize(bmap
);
1606 isl_basic_map_free(bmap
);
1610 static struct isl_map
*map_read_polylib(struct isl_stream
*s
, int nparam
)
1612 struct isl_token
*tok
;
1613 struct isl_token
*tok2
;
1615 struct isl_map
*map
;
1617 tok
= isl_stream_next_token(s
);
1619 isl_stream_error(s
, NULL
, "unexpected EOF");
1622 tok2
= isl_stream_next_token_on_same_line(s
);
1623 if (tok2
&& tok2
->type
== ISL_TOKEN_VALUE
) {
1624 isl_stream_push_token(s
, tok2
);
1625 isl_stream_push_token(s
, tok
);
1626 return isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1629 isl_stream_error(s
, tok2
, "unexpected token");
1630 isl_stream_push_token(s
, tok2
);
1631 isl_stream_push_token(s
, tok
);
1634 n
= isl_int_get_si(tok
->u
.v
);
1635 isl_token_free(tok
);
1637 isl_assert(s
->ctx
, n
>= 1, return NULL
);
1639 map
= isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
));
1641 for (i
= 1; map
&& i
< n
; ++i
)
1642 map
= isl_map_union(map
,
1643 isl_map_from_basic_map(basic_map_read_polylib(s
, nparam
)));
1648 static int optional_power(struct isl_stream
*s
)
1651 struct isl_token
*tok
;
1653 tok
= isl_stream_next_token(s
);
1656 if (tok
->type
!= '^') {
1657 isl_stream_push_token(s
, tok
);
1660 isl_token_free(tok
);
1661 tok
= isl_stream_next_token(s
);
1662 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
1663 isl_stream_error(s
, tok
, "expecting exponent");
1665 isl_stream_push_token(s
, tok
);
1668 pow
= isl_int_get_si(tok
->u
.v
);
1669 isl_token_free(tok
);
1673 static __isl_give isl_div
*read_div(struct isl_stream
*s
,
1674 __isl_take isl_dim
*dim
, struct vars
*v
)
1677 isl_basic_map
*bmap
;
1680 bmap
= isl_basic_map_universe(dim
);
1682 if (vars_add_anon(v
) < 0)
1684 if (read_div_definition(s
, v
) < 0)
1686 bmap
= add_divs(bmap
, v
);
1687 bmap
= isl_basic_map_order_divs(bmap
);
1690 vars_drop(v
, v
->n
- n
);
1692 return isl_basic_map_div(bmap
, bmap
->n_div
- 1);
1694 isl_basic_map_free(bmap
);
1698 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1699 __isl_keep isl_basic_map
*bmap
, struct vars
*v
);
1701 static __isl_give isl_qpolynomial
*read_factor(struct isl_stream
*s
,
1702 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1704 struct isl_qpolynomial
*qp
;
1705 struct isl_token
*tok
;
1707 tok
= next_token(s
);
1709 isl_stream_error(s
, NULL
, "unexpected EOF");
1712 if (tok
->type
== '(') {
1715 isl_token_free(tok
);
1716 qp
= read_term(s
, bmap
, v
);
1719 if (isl_stream_eat(s
, ')'))
1721 pow
= optional_power(s
);
1722 qp
= isl_qpolynomial_pow(qp
, pow
);
1723 } else if (tok
->type
== ISL_TOKEN_VALUE
) {
1724 struct isl_token
*tok2
;
1725 tok2
= isl_stream_next_token(s
);
1726 if (tok2
&& tok2
->type
== '/') {
1727 isl_token_free(tok2
);
1728 tok2
= next_token(s
);
1729 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
) {
1730 isl_stream_error(s
, tok2
, "expected denominator");
1731 isl_token_free(tok
);
1732 isl_token_free(tok2
);
1735 qp
= isl_qpolynomial_rat_cst(isl_basic_map_get_dim(bmap
),
1736 tok
->u
.v
, tok2
->u
.v
);
1737 isl_token_free(tok2
);
1739 isl_stream_push_token(s
, tok2
);
1740 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1743 isl_token_free(tok
);
1744 } else if (tok
->type
== ISL_TOKEN_INFTY
) {
1745 isl_token_free(tok
);
1746 qp
= isl_qpolynomial_infty(isl_basic_map_get_dim(bmap
));
1747 } else if (tok
->type
== ISL_TOKEN_NAN
) {
1748 isl_token_free(tok
);
1749 qp
= isl_qpolynomial_nan(isl_basic_map_get_dim(bmap
));
1750 } else if (tok
->type
== ISL_TOKEN_IDENT
) {
1752 int pos
= vars_pos(v
, tok
->u
.s
, -1);
1755 isl_token_free(tok
);
1759 vars_drop(v
, v
->n
- n
);
1760 isl_stream_error(s
, tok
, "unknown identifier");
1761 isl_token_free(tok
);
1764 isl_token_free(tok
);
1765 pow
= optional_power(s
);
1766 qp
= isl_qpolynomial_var_pow(isl_basic_map_get_dim(bmap
), pos
, pow
);
1767 } else if (tok
->type
== '[') {
1771 isl_stream_push_token(s
, tok
);
1772 div
= read_div(s
, isl_basic_map_get_dim(bmap
), v
);
1773 pow
= optional_power(s
);
1774 qp
= isl_qpolynomial_div_pow(div
, pow
);
1775 } else if (tok
->type
== '-') {
1776 struct isl_qpolynomial
*qp2
;
1778 isl_token_free(tok
);
1779 qp
= isl_qpolynomial_cst(isl_basic_map_get_dim(bmap
),
1781 qp2
= read_factor(s
, bmap
, v
);
1782 qp
= isl_qpolynomial_mul(qp
, qp2
);
1784 isl_stream_error(s
, tok
, "unexpected isl_token");
1785 isl_stream_push_token(s
, tok
);
1789 if (isl_stream_eat_if_available(s
, '*') ||
1790 isl_stream_next_token_is(s
, ISL_TOKEN_IDENT
)) {
1791 struct isl_qpolynomial
*qp2
;
1793 qp2
= read_factor(s
, bmap
, v
);
1794 qp
= isl_qpolynomial_mul(qp
, qp2
);
1799 isl_qpolynomial_free(qp
);
1803 static __isl_give isl_qpolynomial
*read_term(struct isl_stream
*s
,
1804 __isl_keep isl_basic_map
*bmap
, struct vars
*v
)
1806 struct isl_token
*tok
;
1807 struct isl_qpolynomial
*qp
;
1809 qp
= read_factor(s
, bmap
, v
);
1812 tok
= next_token(s
);
1816 if (tok
->type
== '+') {
1817 struct isl_qpolynomial
*qp2
;
1819 isl_token_free(tok
);
1820 qp2
= read_factor(s
, bmap
, v
);
1821 qp
= isl_qpolynomial_add(qp
, qp2
);
1822 } else if (tok
->type
== '-') {
1823 struct isl_qpolynomial
*qp2
;
1825 isl_token_free(tok
);
1826 qp2
= read_factor(s
, bmap
, v
);
1827 qp
= isl_qpolynomial_sub(qp
, qp2
);
1828 } else if (tok
->type
== ISL_TOKEN_VALUE
&&
1829 isl_int_is_neg(tok
->u
.v
)) {
1830 struct isl_qpolynomial
*qp2
;
1832 isl_stream_push_token(s
, tok
);
1833 qp2
= read_factor(s
, bmap
, v
);
1834 qp
= isl_qpolynomial_add(qp
, qp2
);
1836 isl_stream_push_token(s
, tok
);
1844 static __isl_give isl_map
*read_optional_disjuncts(struct isl_stream
*s
,
1845 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1847 struct isl_token
*tok
;
1848 struct isl_map
*map
;
1850 tok
= isl_stream_next_token(s
);
1852 isl_stream_error(s
, NULL
, "unexpected EOF");
1855 map
= isl_map_from_basic_map(isl_basic_map_copy(bmap
));
1856 if (tok
->type
== ':' ||
1857 (tok
->type
== ISL_TOKEN_OR
&& !strcmp(tok
->u
.s
, "|"))) {
1858 isl_token_free(tok
);
1859 map
= isl_map_intersect(map
,
1860 read_disjuncts(s
, v
, isl_basic_map_copy(bmap
)));
1862 isl_stream_push_token(s
, tok
);
1864 isl_basic_map_free(bmap
);
1868 isl_basic_map_free(bmap
);
1872 static struct isl_obj
obj_read_poly(struct isl_stream
*s
,
1873 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1875 struct isl_obj obj
= { isl_obj_pw_qpolynomial
, NULL
};
1876 struct isl_pw_qpolynomial
*pwqp
;
1877 struct isl_qpolynomial
*qp
;
1878 struct isl_map
*map
;
1879 struct isl_set
*set
;
1881 qp
= read_term(s
, bmap
, v
);
1882 map
= read_optional_disjuncts(s
, bmap
, v
);
1883 set
= isl_map_range(map
);
1885 pwqp
= isl_pw_qpolynomial_alloc(set
, qp
);
1887 vars_drop(v
, v
->n
- n
);
1893 static struct isl_obj
obj_read_poly_or_fold(struct isl_stream
*s
,
1894 __isl_take isl_basic_map
*bmap
, struct vars
*v
, int n
)
1896 struct isl_obj obj
= { isl_obj_pw_qpolynomial_fold
, NULL
};
1897 isl_qpolynomial
*qp
;
1898 isl_qpolynomial_fold
*fold
= NULL
;
1899 isl_pw_qpolynomial_fold
*pwf
;
1903 if (!isl_stream_eat_if_available(s
, ISL_TOKEN_MAX
))
1904 return obj_read_poly(s
, bmap
, v
, n
);
1906 if (isl_stream_eat(s
, '('))
1909 qp
= read_term(s
, bmap
, v
);
1910 fold
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1912 while (isl_stream_eat_if_available(s
, ',')) {
1913 isl_qpolynomial_fold
*fold_i
;
1914 qp
= read_term(s
, bmap
, v
);
1915 fold_i
= isl_qpolynomial_fold_alloc(isl_fold_max
, qp
);
1916 fold
= isl_qpolynomial_fold_fold(fold
, fold_i
);
1919 if (isl_stream_eat(s
, ')'))
1922 map
= read_optional_disjuncts(s
, bmap
, v
);
1923 set
= isl_map_range(map
);
1924 pwf
= isl_pw_qpolynomial_fold_alloc(isl_fold_max
, set
, fold
);
1926 vars_drop(v
, v
->n
- n
);
1931 isl_basic_map_free(bmap
);
1932 isl_qpolynomial_fold_free(fold
);
1933 obj
.type
= isl_obj_none
;
1937 static int is_rational(struct isl_stream
*s
)
1939 struct isl_token
*tok
;
1941 tok
= isl_stream_next_token(s
);
1944 if (tok
->type
== ISL_TOKEN_RAT
&& isl_stream_next_token_is(s
, ':')) {
1945 isl_token_free(tok
);
1946 isl_stream_eat(s
, ':');
1950 isl_stream_push_token(s
, tok
);
1955 static struct isl_obj
obj_read_body(struct isl_stream
*s
,
1956 __isl_take isl_basic_map
*bmap
, struct vars
*v
)
1958 struct isl_map
*map
= NULL
;
1959 struct isl_token
*tok
;
1960 struct isl_obj obj
= { isl_obj_set
, NULL
};
1964 bmap
= isl_basic_map_set_rational(bmap
);
1966 if (!next_is_tuple(s
))
1967 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1969 bmap
= read_tuple(s
, bmap
, isl_dim_in
, v
);
1972 tok
= isl_stream_next_token(s
);
1973 if (tok
&& tok
->type
== ISL_TOKEN_TO
) {
1974 obj
.type
= isl_obj_map
;
1975 isl_token_free(tok
);
1976 if (!next_is_tuple(s
)) {
1977 bmap
= isl_basic_map_reverse(bmap
);
1978 return obj_read_poly_or_fold(s
, bmap
, v
, n
);
1980 bmap
= read_tuple(s
, bmap
, isl_dim_out
, v
);
1984 bmap
= isl_basic_map_reverse(bmap
);
1986 isl_stream_push_token(s
, tok
);
1989 map
= read_optional_disjuncts(s
, bmap
, v
);
1991 vars_drop(v
, v
->n
- n
);
1996 isl_basic_map_free(bmap
);
1997 obj
.type
= isl_obj_none
;
2001 static struct isl_obj
to_union(isl_ctx
*ctx
, struct isl_obj obj
)
2003 if (obj
.type
== isl_obj_map
) {
2004 obj
.v
= isl_union_map_from_map(obj
.v
);
2005 obj
.type
= isl_obj_union_map
;
2006 } else if (obj
.type
== isl_obj_set
) {
2007 obj
.v
= isl_union_set_from_set(obj
.v
);
2008 obj
.type
= isl_obj_union_set
;
2009 } else if (obj
.type
== isl_obj_pw_qpolynomial
) {
2010 obj
.v
= isl_union_pw_qpolynomial_from_pw_qpolynomial(obj
.v
);
2011 obj
.type
= isl_obj_union_pw_qpolynomial
;
2012 } else if (obj
.type
== isl_obj_pw_qpolynomial_fold
) {
2013 obj
.v
= isl_union_pw_qpolynomial_fold_from_pw_qpolynomial_fold(obj
.v
);
2014 obj
.type
= isl_obj_union_pw_qpolynomial_fold
;
2016 isl_assert(ctx
, 0, goto error
);
2019 obj
.type
->free(obj
.v
);
2020 obj
.type
= isl_obj_none
;
2024 static struct isl_obj
obj_add(struct isl_ctx
*ctx
,
2025 struct isl_obj obj1
, struct isl_obj obj2
)
2027 if (obj1
.type
== isl_obj_set
&& obj2
.type
== isl_obj_union_set
)
2028 obj1
= to_union(ctx
, obj1
);
2029 if (obj1
.type
== isl_obj_union_set
&& obj2
.type
== isl_obj_set
)
2030 obj2
= to_union(ctx
, obj2
);
2031 if (obj1
.type
== isl_obj_map
&& obj2
.type
== isl_obj_union_map
)
2032 obj1
= to_union(ctx
, obj1
);
2033 if (obj1
.type
== isl_obj_union_map
&& obj2
.type
== isl_obj_map
)
2034 obj2
= to_union(ctx
, obj2
);
2035 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2036 obj2
.type
== isl_obj_union_pw_qpolynomial
)
2037 obj1
= to_union(ctx
, obj1
);
2038 if (obj1
.type
== isl_obj_union_pw_qpolynomial
&&
2039 obj2
.type
== isl_obj_pw_qpolynomial
)
2040 obj2
= to_union(ctx
, obj2
);
2041 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2042 obj2
.type
== isl_obj_union_pw_qpolynomial_fold
)
2043 obj1
= to_union(ctx
, obj1
);
2044 if (obj1
.type
== isl_obj_union_pw_qpolynomial_fold
&&
2045 obj2
.type
== isl_obj_pw_qpolynomial_fold
)
2046 obj2
= to_union(ctx
, obj2
);
2047 isl_assert(ctx
, obj1
.type
== obj2
.type
, goto error
);
2048 if (obj1
.type
== isl_obj_map
&& !isl_map_has_equal_dim(obj1
.v
, obj2
.v
)) {
2049 obj1
= to_union(ctx
, obj1
);
2050 obj2
= to_union(ctx
, obj2
);
2052 if (obj1
.type
== isl_obj_set
&& !isl_set_has_equal_dim(obj1
.v
, obj2
.v
)) {
2053 obj1
= to_union(ctx
, obj1
);
2054 obj2
= to_union(ctx
, obj2
);
2056 if (obj1
.type
== isl_obj_pw_qpolynomial
&&
2057 !isl_pw_qpolynomial_has_equal_dim(obj1
.v
, obj2
.v
)) {
2058 obj1
= to_union(ctx
, obj1
);
2059 obj2
= to_union(ctx
, obj2
);
2061 if (obj1
.type
== isl_obj_pw_qpolynomial_fold
&&
2062 !isl_pw_qpolynomial_fold_has_equal_dim(obj1
.v
, obj2
.v
)) {
2063 obj1
= to_union(ctx
, obj1
);
2064 obj2
= to_union(ctx
, obj2
);
2066 obj1
.v
= obj1
.type
->add(obj1
.v
, obj2
.v
);
2069 obj1
.type
->free(obj1
.v
);
2070 obj2
.type
->free(obj2
.v
);
2071 obj1
.type
= isl_obj_none
;
2076 static struct isl_obj
obj_read(struct isl_stream
*s
, int nparam
)
2078 isl_basic_map
*bmap
= NULL
;
2079 struct isl_token
*tok
;
2080 struct vars
*v
= NULL
;
2081 struct isl_obj obj
= { isl_obj_set
, NULL
};
2083 tok
= next_token(s
);
2085 isl_stream_error(s
, NULL
, "unexpected EOF");
2088 if (tok
->type
== ISL_TOKEN_VALUE
) {
2089 struct isl_token
*tok2
;
2090 struct isl_map
*map
;
2092 tok2
= isl_stream_next_token(s
);
2093 if (!tok2
|| tok2
->type
!= ISL_TOKEN_VALUE
||
2094 isl_int_is_neg(tok2
->u
.v
)) {
2096 isl_stream_push_token(s
, tok2
);
2097 obj
.type
= isl_obj_int
;
2098 obj
.v
= isl_int_obj_alloc(s
->ctx
, tok
->u
.v
);
2099 isl_token_free(tok
);
2102 isl_stream_push_token(s
, tok2
);
2103 isl_stream_push_token(s
, tok
);
2104 map
= map_read_polylib(s
, nparam
);
2107 if (isl_map_dim(map
, isl_dim_in
) > 0)
2108 obj
.type
= isl_obj_map
;
2112 v
= vars_new(s
->ctx
);
2114 isl_stream_push_token(s
, tok
);
2117 bmap
= isl_basic_map_alloc(s
->ctx
, 0, 0, 0, 0, 0, 0);
2118 if (tok
->type
== '[') {
2119 isl_stream_push_token(s
, tok
);
2120 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2124 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2125 tok
= isl_stream_next_token(s
);
2126 if (!tok
|| tok
->type
!= ISL_TOKEN_TO
) {
2127 isl_stream_error(s
, tok
, "expecting '->'");
2129 isl_stream_push_token(s
, tok
);
2132 isl_token_free(tok
);
2133 tok
= isl_stream_next_token(s
);
2134 } else if (nparam
> 0)
2135 bmap
= isl_basic_map_add(bmap
, isl_dim_param
, nparam
);
2136 if (!tok
|| tok
->type
!= '{') {
2137 isl_stream_error(s
, tok
, "expecting '{'");
2139 isl_stream_push_token(s
, tok
);
2142 isl_token_free(tok
);
2144 tok
= isl_stream_next_token(s
);
2147 else if (tok
->type
== ISL_TOKEN_IDENT
&& !strcmp(tok
->u
.s
, "Sym")) {
2148 isl_token_free(tok
);
2149 if (isl_stream_eat(s
, '='))
2151 bmap
= read_tuple(s
, bmap
, isl_dim_param
, v
);
2155 isl_assert(s
->ctx
, nparam
== v
->n
, goto error
);
2156 } else if (tok
->type
== '}') {
2157 obj
.type
= isl_obj_union_set
;
2158 obj
.v
= isl_union_set_empty(isl_basic_map_get_dim(bmap
));
2159 isl_token_free(tok
);
2162 isl_stream_push_token(s
, tok
);
2167 o
= obj_read_body(s
, isl_basic_map_copy(bmap
), v
);
2168 if (o
.type
== isl_obj_none
|| !o
.v
)
2173 obj
= obj_add(s
->ctx
, obj
, o
);
2174 if (obj
.type
== isl_obj_none
|| !obj
.v
)
2177 tok
= isl_stream_next_token(s
);
2178 if (!tok
|| tok
->type
!= ';')
2180 isl_token_free(tok
);
2181 if (isl_stream_next_token_is(s
, '}')) {
2182 tok
= isl_stream_next_token(s
);
2187 if (tok
&& tok
->type
== '}') {
2188 isl_token_free(tok
);
2190 isl_stream_error(s
, tok
, "unexpected isl_token");
2192 isl_token_free(tok
);
2197 isl_basic_map_free(bmap
);
2201 isl_basic_map_free(bmap
);
2202 obj
.type
->free(obj
.v
);
2209 struct isl_obj
isl_stream_read_obj(struct isl_stream
*s
)
2211 return obj_read(s
, -1);
2214 __isl_give isl_map
*isl_stream_read_map(struct isl_stream
*s
, int nparam
)
2218 obj
= obj_read(s
, nparam
);
2220 isl_assert(s
->ctx
, obj
.type
== isl_obj_map
||
2221 obj
.type
== isl_obj_set
, goto error
);
2225 obj
.type
->free(obj
.v
);
2229 __isl_give isl_set
*isl_stream_read_set(struct isl_stream
*s
, int nparam
)
2233 obj
= obj_read(s
, nparam
);
2235 isl_assert(s
->ctx
, obj
.type
== isl_obj_set
, goto error
);
2239 obj
.type
->free(obj
.v
);
2243 __isl_give isl_union_map
*isl_stream_read_union_map(struct isl_stream
*s
)
2247 obj
= obj_read(s
, -1);
2248 if (obj
.type
== isl_obj_map
) {
2249 obj
.type
= isl_obj_union_map
;
2250 obj
.v
= isl_union_map_from_map(obj
.v
);
2252 if (obj
.type
== isl_obj_set
) {
2253 obj
.type
= isl_obj_union_set
;
2254 obj
.v
= isl_union_set_from_set(obj
.v
);
2257 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_map
||
2258 obj
.type
== isl_obj_union_set
, goto error
);
2262 obj
.type
->free(obj
.v
);
2266 __isl_give isl_union_set
*isl_stream_read_union_set(struct isl_stream
*s
)
2270 obj
= obj_read(s
, -1);
2271 if (obj
.type
== isl_obj_set
) {
2272 obj
.type
= isl_obj_union_set
;
2273 obj
.v
= isl_union_set_from_set(obj
.v
);
2276 isl_assert(s
->ctx
, obj
.type
== isl_obj_union_set
, goto error
);
2280 obj
.type
->free(obj
.v
);
2284 static struct isl_basic_map
*basic_map_read(struct isl_stream
*s
, int nparam
)
2287 struct isl_map
*map
;
2288 struct isl_basic_map
*bmap
;
2290 obj
= obj_read(s
, nparam
);
2295 isl_assert(map
->ctx
, map
->n
<= 1, goto error
);
2298 bmap
= isl_basic_map_empty_like_map(map
);
2300 bmap
= isl_basic_map_copy(map
->p
[0]);
2310 __isl_give isl_basic_map
*isl_basic_map_read_from_file(isl_ctx
*ctx
,
2311 FILE *input
, int nparam
)
2313 struct isl_basic_map
*bmap
;
2314 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2317 bmap
= basic_map_read(s
, nparam
);
2322 __isl_give isl_basic_set
*isl_basic_set_read_from_file(isl_ctx
*ctx
,
2323 FILE *input
, int nparam
)
2325 struct isl_basic_map
*bmap
;
2326 bmap
= isl_basic_map_read_from_file(ctx
, input
, nparam
);
2329 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2330 return (struct isl_basic_set
*)bmap
;
2332 isl_basic_map_free(bmap
);
2336 struct isl_basic_map
*isl_basic_map_read_from_str(struct isl_ctx
*ctx
,
2337 const char *str
, int nparam
)
2339 struct isl_basic_map
*bmap
;
2340 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2343 bmap
= basic_map_read(s
, nparam
);
2348 struct isl_basic_set
*isl_basic_set_read_from_str(struct isl_ctx
*ctx
,
2349 const char *str
, int nparam
)
2351 struct isl_basic_map
*bmap
;
2352 bmap
= isl_basic_map_read_from_str(ctx
, str
, nparam
);
2355 isl_assert(ctx
, isl_basic_map_n_in(bmap
) == 0, goto error
);
2356 return (struct isl_basic_set
*)bmap
;
2358 isl_basic_map_free(bmap
);
2362 __isl_give isl_map
*isl_map_read_from_file(struct isl_ctx
*ctx
,
2363 FILE *input
, int nparam
)
2365 struct isl_map
*map
;
2366 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2369 map
= isl_stream_read_map(s
, nparam
);
2374 __isl_give isl_map
*isl_map_read_from_str(struct isl_ctx
*ctx
,
2375 const char *str
, int nparam
)
2377 struct isl_map
*map
;
2378 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2381 map
= isl_stream_read_map(s
, nparam
);
2386 __isl_give isl_set
*isl_set_read_from_file(struct isl_ctx
*ctx
,
2387 FILE *input
, int nparam
)
2389 struct isl_map
*map
;
2390 map
= isl_map_read_from_file(ctx
, input
, nparam
);
2393 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2394 return (struct isl_set
*)map
;
2400 struct isl_set
*isl_set_read_from_str(struct isl_ctx
*ctx
,
2401 const char *str
, int nparam
)
2403 struct isl_map
*map
;
2404 map
= isl_map_read_from_str(ctx
, str
, nparam
);
2407 isl_assert(ctx
, isl_map_n_in(map
) == 0, goto error
);
2408 return (struct isl_set
*)map
;
2414 __isl_give isl_union_map
*isl_union_map_read_from_file(isl_ctx
*ctx
,
2417 isl_union_map
*umap
;
2418 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2421 umap
= isl_stream_read_union_map(s
);
2426 __isl_give isl_union_map
*isl_union_map_read_from_str(struct isl_ctx
*ctx
,
2429 isl_union_map
*umap
;
2430 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2433 umap
= isl_stream_read_union_map(s
);
2438 __isl_give isl_union_set
*isl_union_set_read_from_file(isl_ctx
*ctx
,
2441 isl_union_set
*uset
;
2442 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2445 uset
= isl_stream_read_union_set(s
);
2450 __isl_give isl_union_set
*isl_union_set_read_from_str(struct isl_ctx
*ctx
,
2453 isl_union_set
*uset
;
2454 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2457 uset
= isl_stream_read_union_set(s
);
2462 static __isl_give isl_vec
*isl_vec_read_polylib(struct isl_stream
*s
)
2464 struct isl_vec
*vec
= NULL
;
2465 struct isl_token
*tok
;
2469 tok
= isl_stream_next_token(s
);
2470 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2471 isl_stream_error(s
, tok
, "expecting vector length");
2475 size
= isl_int_get_si(tok
->u
.v
);
2476 isl_token_free(tok
);
2478 vec
= isl_vec_alloc(s
->ctx
, size
);
2480 for (j
= 0; j
< size
; ++j
) {
2481 tok
= isl_stream_next_token(s
);
2482 if (!tok
|| tok
->type
!= ISL_TOKEN_VALUE
) {
2483 isl_stream_error(s
, tok
, "expecting constant value");
2486 isl_int_set(vec
->el
[j
], tok
->u
.v
);
2487 isl_token_free(tok
);
2492 isl_token_free(tok
);
2497 static __isl_give isl_vec
*vec_read(struct isl_stream
*s
)
2499 return isl_vec_read_polylib(s
);
2502 __isl_give isl_vec
*isl_vec_read_from_file(isl_ctx
*ctx
, FILE *input
)
2505 struct isl_stream
*s
= isl_stream_new_file(ctx
, input
);
2513 __isl_give isl_pw_qpolynomial
*isl_stream_read_pw_qpolynomial(
2514 struct isl_stream
*s
)
2518 obj
= obj_read(s
, -1);
2520 isl_assert(s
->ctx
, obj
.type
== isl_obj_pw_qpolynomial
,
2525 obj
.type
->free(obj
.v
);
2529 __isl_give isl_pw_qpolynomial
*isl_pw_qpolynomial_read_from_str(isl_ctx
*ctx
,
2532 isl_pw_qpolynomial
*pwqp
;
2533 struct isl_stream
*s
= isl_stream_new_str(ctx
, str
);
2536 pwqp
= isl_stream_read_pw_qpolynomial(s
);