add isl_set_complement
[platform/upstream/isl.git] / isl_input.c
index 50a1f7c..12838bf 100644 (file)
@@ -61,6 +61,25 @@ static void vars_free(struct vars *v)
        free(v);
 }
 
+static void vars_drop(struct vars *v, int n)
+{
+       struct variable *var;
+
+       if (!v)
+               return;
+
+       v->n -= n;
+
+       var = v->v;
+       while (--n >= 0) {
+               struct variable *next = var->next;
+               free(var->name);
+               free(var);
+               var = next;
+       }
+       v->v = var;
+}
+
 static struct variable *variable_new(struct vars *v, const char *name, int len,
                                int pos)
 {
@@ -101,13 +120,277 @@ static int vars_pos(struct vars *v, const char *s, int len)
        return pos;
 }
 
-static struct vars *read_var_list(struct isl_stream *s, struct vars *v)
+static __isl_give isl_basic_map *set_name(__isl_take isl_basic_map *bmap,
+       enum isl_dim_type type, unsigned pos, char *name)
+{
+       char *prime;
+
+       if (!bmap)
+               return NULL;
+       if (!name)
+               return bmap;
+
+       prime = strchr(name, '\'');
+       if (prime)
+               *prime = '\0';
+       bmap->dim = isl_dim_set_name(bmap->dim, type, pos, name);
+       if (prime)
+               *prime = '\'';
+
+       if (!bmap->dim)
+               goto error;
+
+       return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
+static struct isl_vec *accept_affine(struct isl_stream *s, struct vars *v)
+{
+       struct isl_token *tok = NULL;
+       struct isl_vec *aff;
+       int sign = 1;
+
+       aff = isl_vec_alloc(v->ctx, 1 + v->n);
+       isl_seq_clr(aff->el, aff->size);
+       if (!aff)
+               return NULL;
+
+       for (;;) {
+               tok = isl_stream_next_token(s);
+               if (!tok) {
+                       isl_stream_error(s, NULL, "unexpected EOF");
+                       goto error;
+               }
+               if (tok->type == ISL_TOKEN_IDENT) {
+                       int n = v->n;
+                       int pos = vars_pos(v, tok->u.s, -1);
+                       if (pos < 0)
+                               goto error;
+                       if (pos >= n) {
+                               isl_stream_error(s, tok, "unknown identifier");
+                               isl_token_free(tok);
+                               goto error;
+                       }
+                       if (sign > 0)
+                               isl_int_add_ui(aff->el[1 + pos],
+                                              aff->el[1 + pos], 1);
+                       else
+                               isl_int_sub_ui(aff->el[1 + pos],
+                                              aff->el[1 + pos], 1);
+                       sign = 1;
+               } else if (tok->type == ISL_TOKEN_VALUE) {
+                       struct isl_token *tok2;
+                       int n = v->n;
+                       int pos = -1;
+                       tok2 = isl_stream_next_token(s);
+                       if (tok2 && tok2->type == ISL_TOKEN_IDENT) {
+                               pos = vars_pos(v, tok2->u.s, -1);
+                               if (pos < 0)
+                                       goto error;
+                               if (pos >= n) {
+                                       isl_stream_error(s, tok2,
+                                               "unknown identifier");
+                                       isl_token_free(tok);
+                                       isl_token_free(tok2);
+                                       goto error;
+                               }
+                               isl_token_free(tok2);
+                       } else if (tok2)
+                               isl_stream_push_token(s, tok2);
+                       if (sign < 0)
+                               isl_int_neg(tok->u.v, tok->u.v);
+                       isl_int_add(aff->el[1 + pos],
+                                       aff->el[1 + pos], tok->u.v);
+                       sign = 1;
+               } else if (tok->type == '-') {
+                       sign = -sign;
+               } else if (tok->type == '+') {
+                       /* nothing */
+               } else {
+                       isl_stream_push_token(s, tok);
+                       break;
+               }
+               isl_token_free(tok);
+       }
+
+       return aff;
+error:
+       isl_vec_free(aff);
+       return NULL;
+}
+
+static __isl_give isl_basic_map *read_var_list(struct isl_stream *s,
+       __isl_take isl_basic_map *bmap, enum isl_dim_type type, struct vars *v)
 {
+       int i = 0;
        struct isl_token *tok;
 
        while ((tok = isl_stream_next_token(s)) != NULL) {
+               int new_name = 0;
+
+               if (tok->type == ISL_TOKEN_IDENT) {
+                       int n = v->n;
+                       int p = vars_pos(v, tok->u.s, -1);
+                       if (p < 0)
+                               goto error;
+                       new_name = p >= n;
+               }
+
+               if (new_name) {
+                       bmap = isl_basic_map_add(bmap, type, 1);
+                       bmap = set_name(bmap, type, i, v->v->name);
+                       isl_token_free(tok);
+               } else if (tok->type == ISL_TOKEN_IDENT ||
+                          tok->type == ISL_TOKEN_VALUE) {
+                       struct isl_vec *vec;
+                       int k;
+                       if (type == isl_dim_param) {
+                               isl_stream_error(s, tok,
+                                               "expecting unique identifier");
+                               goto error;
+                       }
+                       isl_stream_push_token(s, tok);
+                       tok = NULL;
+                       vec = accept_affine(s, v);
+                       if (!vec)
+                               goto error;
+                       v->v = variable_new(v, "", 0, v->n);
+                       if (!v->v)
+                               goto error;
+                       v->n++;
+                       bmap = isl_basic_map_add(bmap, type, 1);
+                       bmap = isl_basic_map_extend_constraints(bmap, 1, 0);
+                       k = isl_basic_map_alloc_equality(bmap);
+                       if (k >= 0) {
+                               isl_seq_cpy(bmap->eq[k], vec->el, vec->size);
+                               isl_int_set_si(bmap->eq[k][vec->size], -1);
+                       }
+                       isl_vec_free(vec);
+                       if (k < 0)
+                               goto error;
+               } else
+                       break;
+
+               tok = isl_stream_next_token(s);
+               if (!tok || tok->type != ',')
+                       break;
+
+               isl_token_free(tok);
+               i++;
+       }
+       if (tok)
+               isl_stream_push_token(s, tok);
+
+       return bmap;
+error:
+       isl_token_free(tok);
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
+static __isl_give isl_mat *accept_affine_list(struct isl_stream *s,
+       struct vars *v)
+{
+       struct isl_vec *vec;
+       struct isl_mat *mat;
+       struct isl_token *tok = NULL;
+
+       vec = accept_affine(s, v);
+       mat = isl_mat_from_row_vec(vec);
+       if (!mat)
+               return NULL;
+
+       for (;;) {
+               tok = isl_stream_next_token(s);
+               if (!tok) {
+                       isl_stream_error(s, NULL, "unexpected EOF");
+                       goto error;
+               }
+               if (tok->type != ',') {
+                       isl_stream_push_token(s, tok);
+                       break;
+               }
+               isl_token_free(tok);
+
+               vec = accept_affine(s, v);
+               mat = isl_mat_vec_concat(mat, vec);
+               if (!mat)
+                       return NULL;
+       }
+
+       return mat;
+error:
+       isl_mat_free(mat);
+       return NULL;
+}
+
+static struct isl_basic_map *add_div_definition(struct isl_stream *s,
+       struct vars *v, struct isl_basic_map *bmap, int k)
+{
+       struct isl_token *tok;
+       int seen_paren = 0;
+       struct isl_vec *aff;
+
+       if (isl_stream_eat(s, '['))
+               goto error;
+
+       tok = isl_stream_next_token(s);
+       if (!tok)
+               goto error;
+       if (tok->type == '(') {
+               seen_paren = 1;
+               isl_token_free(tok);
+       } else
+               isl_stream_push_token(s, tok);
+
+       aff = accept_affine(s, v);
+       if (!aff)
+               goto error;
+
+       isl_seq_cpy(bmap->div[k] + 1, aff->el, aff->size);
+
+       isl_vec_free(aff);
+
+       if (seen_paren && isl_stream_eat(s, ')'))
+               goto error;
+       if (isl_stream_eat(s, '/'))
+               goto error;
+
+       tok = isl_stream_next_token(s);
+       if (!tok)
+               goto error;
+       if (tok->type != ISL_TOKEN_VALUE) {
+               isl_stream_error(s, tok, "expected denominator");
+               isl_stream_push_token(s, tok);
+               goto error;
+       }
+       isl_int_set(bmap->div[k][0], tok->u.v);
+       isl_token_free(tok);
+
+       if (isl_stream_eat(s, ']'))
+               goto error;
+
+       if (isl_basic_map_add_div_constraints(bmap, k) < 0)
+               goto error;
+
+       return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
+static struct isl_basic_map *read_defined_var_list(struct isl_stream *s,
+       struct vars *v, struct isl_basic_map *bmap)
+{
+       struct isl_token *tok;
+
+       while ((tok = isl_stream_next_token(s)) != NULL) {
+               int k;
                int p;
                int n = v->n;
+               unsigned total = isl_basic_map_total_dim(bmap);
 
                if (tok->type != ISL_TOKEN_IDENT)
                        break;
@@ -120,7 +403,22 @@ static struct vars *read_var_list(struct isl_stream *s, struct vars *v)
                        goto error;
                }
                isl_token_free(tok);
+
+               bmap = isl_basic_map_cow(bmap);
+               bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
+                                               1, 0, 2);
+
+               if ((k = isl_basic_map_alloc_div(bmap)) < 0)
+                       goto error;
+               isl_seq_clr(bmap->div[k], 1 + 1 + total);
+
                tok = isl_stream_next_token(s);
+               if (tok && tok->type == '=') {
+                       isl_token_free(tok);
+                       bmap = add_div_definition(s, v, bmap, k);
+                       tok = isl_stream_next_token(s);
+               }
+
                if (!tok || tok->type != ',')
                        break;
 
@@ -129,14 +427,15 @@ static struct vars *read_var_list(struct isl_stream *s, struct vars *v)
        if (tok)
                isl_stream_push_token(s, tok);
 
-       return v;
+       return bmap;
 error:
        isl_token_free(tok);
-       vars_free(v);
+       isl_basic_map_free(bmap);
        return NULL;
 }
 
-static struct vars *read_tuple(struct isl_stream *s, struct vars *v)
+static __isl_give isl_basic_map *read_tuple(struct isl_stream *s,
+       __isl_take isl_basic_map *bmap, enum isl_dim_type type, struct vars *v)
 {
        struct isl_token *tok;
 
@@ -146,7 +445,7 @@ static struct vars *read_tuple(struct isl_stream *s, struct vars *v)
                goto error;
        }
        isl_token_free(tok);
-       v = read_var_list(s, v);
+       bmap = read_var_list(s, bmap, type, v);
        tok = isl_stream_next_token(s);
        if (!tok || tok->type != ']') {
                isl_stream_error(s, tok, "expecting ']'");
@@ -154,22 +453,22 @@ static struct vars *read_tuple(struct isl_stream *s, struct vars *v)
        }
        isl_token_free(tok);
 
-       return v;
+       return bmap;
 error:
        if (tok)
                isl_token_free(tok);
-       vars_free(v);
+       isl_basic_map_free(bmap);
        return NULL;
 }
 
 static struct isl_basic_map *add_constraints(struct isl_stream *s,
-       struct vars **v, struct isl_basic_map *bmap);
+       struct vars *v, struct isl_basic_map *bmap);
 
 static struct isl_basic_map *add_exists(struct isl_stream *s,
-       struct vars **v, struct isl_basic_map *bmap)
+       struct vars *v, struct isl_basic_map *bmap)
 {
        struct isl_token *tok;
-       int n = (*v)->n;
+       int n = v->n;
        int extra;
        int seen_paren = 0;
        int i;
@@ -183,22 +482,11 @@ static struct isl_basic_map *add_exists(struct isl_stream *s,
                isl_token_free(tok);
        } else
                isl_stream_push_token(s, tok);
-       *v = read_var_list(s, *v);
-       if (!*v)
-               goto error;
-       extra = (*v)->n - n;
-       bmap = isl_basic_map_cow(bmap);
-       bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
-                       extra, 0, 0);
-       total = isl_basic_map_total_dim(bmap);
-       for (i = 0; i < extra; ++i) {
-               int k;
-               if ((k = isl_basic_map_alloc_div(bmap)) < 0)
-                       goto error;
-               isl_seq_clr(bmap->div[k], 1+1+total);
-       }
+
+       bmap = read_defined_var_list(s, v, bmap);
        if (!bmap)
-               return NULL;
+               goto error;
+
        if (isl_stream_eat(s, ':'))
                goto error;
        bmap = add_constraints(s, v, bmap);
@@ -210,15 +498,77 @@ error:
        return NULL;
 }
 
+static __isl_give isl_basic_map *construct_constraint(
+       __isl_take isl_basic_map *bmap, enum isl_token_type type,
+       isl_int *left, isl_int *right)
+{
+       int k;
+       unsigned len;
+       struct isl_ctx *ctx;
+
+       if (!bmap)
+               return NULL;
+       len = 1 + isl_basic_map_total_dim(bmap);
+       ctx = bmap->ctx;
+
+       k = isl_basic_map_alloc_inequality(bmap);
+       if (k < 0)
+               goto error;
+       if (type == ISL_TOKEN_LE)
+               isl_seq_combine(bmap->ineq[k], ctx->negone, left,
+                                              ctx->one, right,
+                                              len);
+       else if (type == ISL_TOKEN_GE)
+               isl_seq_combine(bmap->ineq[k], ctx->one, left,
+                                              ctx->negone, right,
+                                              len);
+       else if (type == ISL_TOKEN_LT) {
+               isl_seq_combine(bmap->ineq[k], ctx->negone, left,
+                                              ctx->one, right,
+                                              len);
+               isl_int_sub_ui(bmap->ineq[k][0], bmap->ineq[k][0], 1);
+       } else if (type == ISL_TOKEN_GT) {
+               isl_seq_combine(bmap->ineq[k], ctx->one, left,
+                                              ctx->negone, right,
+                                              len);
+               isl_int_sub_ui(bmap->ineq[k][0], bmap->ineq[k][0], 1);
+       } else {
+               isl_seq_combine(bmap->ineq[k], ctx->one, left,
+                                              ctx->negone, right,
+                                              len);
+               isl_basic_map_inequality_to_equality(bmap, k);
+       }
+
+       return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
+static int is_comparator(struct isl_token *tok)
+{
+       if (!tok)
+               return 0;
+
+       switch (tok->type) {
+       case ISL_TOKEN_LT:
+       case ISL_TOKEN_GT:
+       case ISL_TOKEN_LE:
+       case ISL_TOKEN_GE:
+       case '=':
+               return 1;
+       default:
+               return 0;
+       }
+}
+
 static struct isl_basic_map *add_constraint(struct isl_stream *s,
-       struct vars **v, struct isl_basic_map *bmap)
+       struct vars *v, struct isl_basic_map *bmap)
 {
+       int i, j;
        unsigned total = isl_basic_map_total_dim(bmap);
-       int k;
-       int sign = 1;
-       int equality = 0;
-       int op = 0;
        struct isl_token *tok = NULL;
+       struct isl_mat *aff1 = NULL, *aff2 = NULL;
 
        tok = isl_stream_next_token(s);
        if (!tok)
@@ -228,96 +578,59 @@ static struct isl_basic_map *add_constraint(struct isl_stream *s,
                return add_exists(s, v, bmap);
        }
        isl_stream_push_token(s, tok);
+       tok = NULL;
 
        bmap = isl_basic_map_cow(bmap);
-       bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
-       k = isl_basic_map_alloc_inequality(bmap);
-       if (k < 0)
-               goto error;
-       isl_seq_clr(bmap->ineq[k], 1+total);
 
+       aff1 = accept_affine_list(s, v);
+       if (!aff1)
+               goto error;
+       tok = isl_stream_next_token(s);
+       if (!is_comparator(tok)) {
+               isl_stream_error(s, tok, "missing operator");
+               if (tok)
+                       isl_stream_push_token(s, tok);
+               tok = NULL;
+               goto error;
+       }
+       isl_assert(aff1->ctx, aff1->n_col == 1 + total, goto error);
        for (;;) {
-               tok = isl_stream_next_token(s);
-               if (!tok) {
-                       isl_stream_error(s, NULL, "unexpected EOF");
+               aff2 = accept_affine_list(s, v);
+               if (!aff2)
                        goto error;
-               }
-               if (tok->type == ISL_TOKEN_IDENT) {
-                       int n = (*v)->n;
-                       int pos = vars_pos(*v, tok->u.s, -1);
-                       if (pos < 0)
-                               goto error;
-                       if (pos >= n) {
-                               isl_stream_error(s, tok, "unknown identifier");
-                               goto error;
-                       }
-                       if (sign > 0)
-                               isl_int_add_ui(bmap->ineq[k][1+pos],
-                                               bmap->ineq[k][1+pos], 1);
-                       else
-                               isl_int_sub_ui(bmap->ineq[k][1+pos],
-                                               bmap->ineq[k][1+pos], 1);
-               } else if (tok->type == ISL_TOKEN_VALUE) {
-                       struct isl_token *tok2;
-                       int n = (*v)->n;
-                       int pos = -1;
-                       tok2 = isl_stream_next_token(s);
-                       if (tok2 && tok2->type == ISL_TOKEN_IDENT) {
-                               pos = vars_pos(*v, tok2->u.s, -1);
-                               if (pos < 0)
-                                       goto error;
-                               if (pos >= n) {
-                                       isl_stream_error(s, tok2,
-                                               "unknown identifier");
-                                       isl_token_free(tok2);
-                                       goto error;
-                               }
-                               isl_token_free(tok2);
-                       } else if (tok2)
-                               isl_stream_push_token(s, tok2);
-                       if (sign < 0)
-                               isl_int_neg(tok->u.v, tok->u.v);
-                       isl_int_add(bmap->ineq[k][1+pos],
-                                       bmap->ineq[k][1+pos], tok->u.v);
-               } else if (tok->type == '+') {
-                       /* nothing */
-               } else if (tok->type == ISL_TOKEN_LE) {
-                       op = 1;
-                       isl_seq_neg(bmap->ineq[k], bmap->ineq[k], 1+total);
-               } else if (tok->type == ISL_TOKEN_GE) {
-                       op = 1;
-                       sign = -1;
-               } else if (tok->type == '=') {
-                       if (op) {
-                               isl_stream_error(s, tok, "too many operators");
-                               goto error;
-                       }
-                       op = 1;
-                       equality = 1;
-                       sign = -1;
-               } else {
-                       isl_stream_push_token(s, tok);
+               isl_assert(aff2->ctx, aff2->n_col == 1 + total, goto error);
+
+               bmap = isl_basic_map_extend_constraints(bmap, 0,
+                                               aff1->n_row * aff2->n_row);
+               for (i = 0; i < aff1->n_row; ++i)
+                       for (j = 0; j < aff2->n_row; ++j)
+                               bmap = construct_constraint(bmap, tok->type,
+                                                   aff1->row[i], aff2->row[j]);
+               isl_token_free(tok);
+               isl_mat_free(aff1);
+               aff1 = aff2;
+
+               tok = isl_stream_next_token(s);
+               if (!is_comparator(tok)) {
+                       if (tok)
+                               isl_stream_push_token(s, tok);
                        break;
                }
-               isl_token_free(tok);
-       }
-       tok = NULL;
-       if (!op) {
-               isl_stream_error(s, tok, "missing operator");
-               goto error;
        }
-       if (equality)
-               isl_basic_map_inequality_to_equality(bmap, k);
+       isl_mat_free(aff1);
+
        return bmap;
 error:
        if (tok)
                isl_token_free(tok);
+       isl_mat_free(aff1);
+       isl_mat_free(aff2);
        isl_basic_map_free(bmap);
        return NULL;
 }
 
 static struct isl_basic_map *add_constraints(struct isl_stream *s,
-       struct vars **v, struct isl_basic_map *bmap)
+       struct vars *v, struct isl_basic_map *bmap)
 {
        struct isl_token *tok;
 
@@ -344,6 +657,104 @@ error:
        return NULL;
 }
 
+static struct isl_basic_map *read_disjunct(struct isl_stream *s,
+       struct vars *v, __isl_take isl_dim *dim)
+{
+       int seen_paren = 0;
+       struct isl_token *tok;
+       struct isl_basic_map *bmap;
+
+       bmap = isl_basic_map_alloc_dim(dim, 0, 0, 0);
+       if (!bmap)
+               return NULL;
+
+       tok = isl_stream_next_token(s);
+       if (!tok)
+               goto error;
+       if (tok->type == '(') {
+               seen_paren = 1;
+               isl_token_free(tok);
+       } else
+               isl_stream_push_token(s, tok);
+
+       bmap = add_constraints(s, v, bmap);
+       bmap = isl_basic_map_simplify(bmap);
+       bmap = isl_basic_map_finalize(bmap);
+
+       if (seen_paren && isl_stream_eat(s, ')'))
+               goto error;
+
+       return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
+static struct isl_map *read_disjuncts(struct isl_stream *s,
+       struct vars *v, __isl_take isl_dim *dim)
+{
+       struct isl_token *tok;
+       struct isl_map *map;
+
+       tok = isl_stream_next_token(s);
+       if (!tok) {
+               isl_stream_error(s, NULL, "unexpected EOF");
+               goto error;
+       }
+       if (tok->type == '}') {
+               isl_stream_push_token(s, tok);
+               return isl_map_universe(dim);
+       }
+       isl_stream_push_token(s, tok);
+
+       map = isl_map_empty(isl_dim_copy(dim));
+       for (;;) {
+               struct isl_basic_map *bmap;
+               int n = v->n;
+
+               bmap = read_disjunct(s, v, isl_dim_copy(dim));
+               map = isl_map_union(map, isl_map_from_basic_map(bmap));
+
+               vars_drop(v, v->n - n);
+
+               tok = isl_stream_next_token(s);
+               if (!tok || tok->type != ISL_TOKEN_OR)
+                       break;
+               isl_token_free(tok);
+       }
+       if (tok)
+               isl_stream_push_token(s, tok);
+
+       isl_dim_free(dim);
+       return map;
+error:
+       isl_dim_free(dim);
+       return NULL;
+}
+
+static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map *bmap, int pos)
+{
+       if (pos < isl_basic_map_dim(bmap, isl_dim_out))
+               return 1 + isl_basic_map_dim(bmap, isl_dim_param) +
+                          isl_basic_map_dim(bmap, isl_dim_in) + pos;
+       pos -= isl_basic_map_dim(bmap, isl_dim_out);
+
+       if (pos < isl_basic_map_dim(bmap, isl_dim_in))
+               return 1 + isl_basic_map_dim(bmap, isl_dim_param) + pos;
+       pos -= isl_basic_map_dim(bmap, isl_dim_in);
+
+       if (pos < isl_basic_map_dim(bmap, isl_dim_div))
+               return 1 + isl_basic_map_dim(bmap, isl_dim_param) +
+                          isl_basic_map_dim(bmap, isl_dim_in) +
+                          isl_basic_map_dim(bmap, isl_dim_out) + pos;
+       pos -= isl_basic_map_dim(bmap, isl_dim_div);
+
+       if (pos < isl_basic_map_dim(bmap, isl_dim_param))
+               return 1 + pos;
+
+       return 0;
+}
+
 static __isl_give isl_basic_map *basic_map_read_polylib_constraint(
        struct isl_stream *s, __isl_take isl_basic_map *bmap)
 {
@@ -388,7 +799,8 @@ static __isl_give isl_basic_map *basic_map_read_polylib_constraint(
        if (k < 0)
                goto error;
 
-       for (j = 0; j < dim; ++j) {
+       for (j = 0; j < 1 + isl_basic_map_total_dim(bmap); ++j) {
+               int pos;
                tok = isl_stream_next_token(s);
                if (!tok || tok->type != ISL_TOKEN_VALUE) {
                        isl_stream_error(s, tok, "expecting coefficient");
@@ -396,29 +808,16 @@ static __isl_give isl_basic_map *basic_map_read_polylib_constraint(
                                isl_stream_push_token(s, tok);
                        goto error;
                }
-               isl_int_set(c[1 + nparam + j], tok->u.v);
-               isl_token_free(tok);
-       }
-       for (j = 0; j < nparam; ++j) {
-               tok = isl_stream_next_token(s);
-               if (!tok || tok->type != ISL_TOKEN_VALUE) {
-                       isl_stream_error(s, tok, "expecting coefficient");
-                       if (tok)
-                               isl_stream_push_token(s, tok);
+               if (tok->on_new_line) {
+                       isl_stream_error(s, tok,
+                               "coefficient should not appear on new line");
+                       isl_stream_push_token(s, tok);
                        goto error;
                }
-               isl_int_set(c[1 + j], tok->u.v);
+               pos = polylib_pos_to_isl_pos(bmap, j);
+               isl_int_set(c[pos], tok->u.v);
                isl_token_free(tok);
        }
-       tok = isl_stream_next_token(s);
-       if (!tok || tok->type != ISL_TOKEN_VALUE) {
-               isl_stream_error(s, tok, "expecting coefficient");
-               if (tok)
-                       isl_stream_push_token(s, tok);
-               goto error;
-       }
-       isl_int_set(c[0], tok->u.v);
-       isl_token_free(tok);
 
        return bmap;
 error:
@@ -434,7 +833,7 @@ static __isl_give isl_basic_map *basic_map_read_polylib(struct isl_stream *s,
        struct isl_token *tok2;
        int n_row, n_col;
        int on_new_line;
-       unsigned dim;
+       unsigned in = 0, out, local = 0;
        struct isl_basic_map *bmap = NULL;
 
        if (nparam < 0)
@@ -459,17 +858,82 @@ static __isl_give isl_basic_map *basic_map_read_polylib(struct isl_stream *s,
        isl_assert(s->ctx, !on_new_line, return NULL);
        isl_assert(s->ctx, n_row >= 0, return NULL);
        isl_assert(s->ctx, n_col >= 2 + nparam, return NULL);
-       dim = n_col - 2 - nparam;
-       bmap = isl_basic_map_alloc(s->ctx, nparam, 0, dim, 0, n_row, n_row);
+       tok = isl_stream_next_token_on_same_line(s);
+       if (tok) {
+               if (tok->type != ISL_TOKEN_VALUE) {
+                       isl_stream_error(s, tok,
+                                   "expecting number of output dimensions");
+                       isl_stream_push_token(s, tok);
+                       goto error;
+               }
+               out = isl_int_get_si(tok->u.v);
+               isl_token_free(tok);
+
+               tok = isl_stream_next_token_on_same_line(s);
+               if (!tok || tok->type != ISL_TOKEN_VALUE) {
+                       isl_stream_error(s, tok,
+                                   "expecting number of input dimensions");
+                       if (tok)
+                               isl_stream_push_token(s, tok);
+                       goto error;
+               }
+               in = isl_int_get_si(tok->u.v);
+               isl_token_free(tok);
+
+               tok = isl_stream_next_token_on_same_line(s);
+               if (!tok || tok->type != ISL_TOKEN_VALUE) {
+                       isl_stream_error(s, tok,
+                                   "expecting number of existentials");
+                       if (tok)
+                               isl_stream_push_token(s, tok);
+                       goto error;
+               }
+               local = isl_int_get_si(tok->u.v);
+               isl_token_free(tok);
+
+               tok = isl_stream_next_token_on_same_line(s);
+               if (!tok || tok->type != ISL_TOKEN_VALUE) {
+                       isl_stream_error(s, tok,
+                                   "expecting number of parameters");
+                       if (tok)
+                               isl_stream_push_token(s, tok);
+                       goto error;
+               }
+               nparam = isl_int_get_si(tok->u.v);
+               isl_token_free(tok);
+               if (n_col != 1 + out + in + local + nparam + 1) {
+                       isl_stream_error(s, NULL,
+                                   "dimensions don't match");
+                       goto error;
+               }
+       } else
+               out = n_col - 2 - nparam;
+       bmap = isl_basic_map_alloc(s->ctx, nparam, in, out, local, n_row, n_row);
        if (!bmap)
                return NULL;
 
+       for (i = 0; i < local; ++i) {
+               int k = isl_basic_map_alloc_div(bmap);
+               if (k < 0)
+                       goto error;
+       }
+
        for (i = 0; i < n_row; ++i)
                bmap = basic_map_read_polylib_constraint(s, bmap);
 
+       tok = isl_stream_next_token_on_same_line(s);
+       if (tok) {
+               isl_stream_error(s, tok, "unexpected extra token on line");
+               isl_stream_push_token(s, tok);
+               goto error;
+       }
+
        bmap = isl_basic_map_simplify(bmap);
        bmap = isl_basic_map_finalize(bmap);
        return bmap;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
 }
 
 static struct isl_map *map_read_polylib(struct isl_stream *s, int nparam)
@@ -484,18 +948,12 @@ static struct isl_map *map_read_polylib(struct isl_stream *s, int nparam)
                isl_stream_error(s, NULL, "unexpected EOF");
                return NULL;
        }
-       tok2 = isl_stream_next_token(s);
-       if (!tok2) {
-               isl_token_free(tok);
-               isl_stream_error(s, NULL, "unexpected EOF");
-               return NULL;
-       }
-       if (!tok2->on_new_line) {
+       tok2 = isl_stream_next_token_on_same_line(s);
+       if (tok2) {
                isl_stream_push_token(s, tok2);
                isl_stream_push_token(s, tok);
                return isl_map_from_basic_map(basic_map_read_polylib(s, nparam));
        }
-       isl_stream_push_token(s, tok2);
        n = isl_int_get_si(tok->u.v);
        isl_token_free(tok);
 
@@ -510,13 +968,55 @@ static struct isl_map *map_read_polylib(struct isl_stream *s, int nparam)
        return map;
 }
 
+static struct isl_map *map_read_body(struct isl_stream *s,
+       __isl_take isl_basic_map *bmap, struct vars *v)
+{
+       struct isl_map *map = NULL;
+       struct isl_token *tok;
+       int n = v->n;
+
+       bmap = read_tuple(s, bmap, isl_dim_in, v);
+       if (!bmap)
+               goto error;
+       tok = isl_stream_next_token(s);
+       if (tok && tok->type == ISL_TOKEN_TO) {
+               isl_token_free(tok);
+               bmap = read_tuple(s, bmap, isl_dim_out, v);
+               if (!bmap)
+                       goto error;
+       } else {
+               bmap = isl_basic_map_reverse(bmap);
+               if (tok)
+                       isl_stream_push_token(s, tok);
+       }
+       tok = isl_stream_next_token(s);
+       if (!tok) {
+               isl_stream_error(s, NULL, "unexpected EOF");
+               goto error;
+       }
+       map = isl_map_from_basic_map(isl_basic_map_copy(bmap));
+       if (tok->type == ':') {
+               isl_token_free(tok);
+               map = isl_map_intersect(map,
+                           read_disjuncts(s, v, isl_basic_map_get_dim(bmap)));
+       } else
+               isl_stream_push_token(s, tok);
+
+       vars_drop(v, v->n - n);
+
+       isl_basic_map_free(bmap);
+       return map;
+error:
+       isl_basic_map_free(bmap);
+       return NULL;
+}
+
 static struct isl_map *map_read(struct isl_stream *s, int nparam)
 {
        struct isl_basic_map *bmap = NULL;
+       struct isl_map *map = NULL;
        struct isl_token *tok;
        struct vars *v = NULL;
-       int n1;
-       int n2;
 
        tok = isl_stream_next_token(s);
        if (!tok) {
@@ -527,41 +1027,48 @@ static struct isl_map *map_read(struct isl_stream *s, int nparam)
                isl_stream_push_token(s, tok);
                return map_read_polylib(s, nparam);
        }
-       if (tok->type != '{') {
+       v = vars_new(s->ctx);
+       bmap = isl_basic_map_alloc(s->ctx, 0, 0, 0, 0, 0, 0);
+       if (tok->type == '[') {
+               isl_stream_push_token(s, tok);
+               bmap = read_tuple(s, bmap, isl_dim_param, v);
+               if (!bmap)
+                       goto error;
+               if (nparam >= 0)
+                       isl_assert(s->ctx, nparam == v->n, goto error);
+               tok = isl_stream_next_token(s);
+               if (!tok || tok->type != ISL_TOKEN_TO) {
+                       isl_stream_error(s, tok, "expecting '->'");
+                       if (tok)
+                               isl_stream_push_token(s, tok);
+                       goto error;
+               }
+               isl_token_free(tok);
+               tok = isl_stream_next_token(s);
+       } if (nparam > 0)
+               bmap = isl_basic_map_add(bmap, isl_dim_param, nparam);
+       if (!tok || tok->type != '{') {
                isl_stream_error(s, tok, "expecting '{'");
                if (tok)
                        isl_stream_push_token(s, tok);
                goto error;
        }
        isl_token_free(tok);
-       isl_assert(s->ctx, nparam == 0, goto error);
-       v = vars_new(s->ctx);
-       v = read_tuple(s, v);
-       if (!v)
-               return NULL;
-       n1 = v->n;
-       tok = isl_stream_next_token(s);
-       if (tok && tok->type == ISL_TOKEN_TO) {
-               isl_token_free(tok);
-               v = read_tuple(s, v);
-               if (!v)
-                       return NULL;
-               n2 = v->n - n1;
-       } else {
-               if (tok)
-                       isl_stream_push_token(s, tok);
-               n2 = n1;
-               n1 = 0;
-       }
-       bmap = isl_basic_map_alloc(s->ctx, 0, n1, n2, 0, 0,0);
-       if (!bmap)
-               goto error;
-       tok = isl_stream_next_token(s);
-       if (tok && tok->type == ':') {
-               isl_token_free(tok);
-               bmap = add_constraints(s, &v, bmap);
+
+       for (;;) {
+               isl_map *m = map_read_body(s, isl_basic_map_copy(bmap), v);
+               if (!m)
+                       break;
+               if (map)
+                       map = isl_map_union(map, m);
+               else
+                       map = m;
                tok = isl_stream_next_token(s);
+               if (!tok || tok->type != ';')
+                       break;
+               isl_token_free(tok);
        }
+
        if (tok && tok->type == '}') {
                isl_token_free(tok);
        } else {
@@ -571,12 +1078,12 @@ static struct isl_map *map_read(struct isl_stream *s, int nparam)
                goto error;
        }
        vars_free(v);
+       isl_basic_map_free(bmap);
 
-       bmap = isl_basic_map_simplify(bmap);
-       bmap = isl_basic_map_finalize(bmap);
-       return isl_map_from_basic_map(bmap);
+       return map;
 error:
        isl_basic_map_free(bmap);
+       isl_map_free(map);
        if (v)
                vars_free(v);
        return NULL;
@@ -607,7 +1114,7 @@ error:
 }
 
 __isl_give isl_basic_map *isl_basic_map_read_from_file(isl_ctx *ctx,
-               FILE *input, unsigned nparam, unsigned input_format)
+               FILE *input, int nparam)
 {
        struct isl_basic_map *bmap;
        struct isl_stream *s = isl_stream_new_file(ctx, input);
@@ -619,10 +1126,10 @@ __isl_give isl_basic_map *isl_basic_map_read_from_file(isl_ctx *ctx,
 }
 
 __isl_give isl_basic_set *isl_basic_set_read_from_file(isl_ctx *ctx,
-               FILE *input, unsigned nparam, unsigned input_format)
+               FILE *input, int nparam)
 {
        struct isl_basic_map *bmap;
-       bmap = isl_basic_map_read_from_file(ctx, input, nparam, input_format);
+       bmap = isl_basic_map_read_from_file(ctx, input, nparam);
        if (!bmap)
                return NULL;
        isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
@@ -633,7 +1140,7 @@ error:
 }
 
 struct isl_basic_map *isl_basic_map_read_from_str(struct isl_ctx *ctx,
-               const char *str, unsigned nparam, unsigned input_format)
+               const char *str, int nparam)
 {
        struct isl_basic_map *bmap;
        struct isl_stream *s = isl_stream_new_str(ctx, str);
@@ -645,10 +1152,10 @@ struct isl_basic_map *isl_basic_map_read_from_str(struct isl_ctx *ctx,
 }
 
 struct isl_basic_set *isl_basic_set_read_from_str(struct isl_ctx *ctx,
-               const char *str, unsigned nparam, unsigned input_format)
+               const char *str, int nparam)
 {
        struct isl_basic_map *bmap;
-       bmap = isl_basic_map_read_from_str(ctx, str, nparam, input_format);
+       bmap = isl_basic_map_read_from_str(ctx, str, nparam);
        if (!bmap)
                return NULL;
        isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
@@ -659,7 +1166,7 @@ error:
 }
 
 __isl_give isl_map *isl_map_read_from_file(struct isl_ctx *ctx,
-               FILE *input, unsigned nparam, unsigned input_format)
+               FILE *input, int nparam)
 {
        struct isl_map *map;
        struct isl_stream *s = isl_stream_new_file(ctx, input);
@@ -670,11 +1177,37 @@ __isl_give isl_map *isl_map_read_from_file(struct isl_ctx *ctx,
        return map;
 }
 
+__isl_give isl_map *isl_map_read_from_str(struct isl_ctx *ctx,
+               const char *str, int nparam)
+{
+       struct isl_map *map;
+       struct isl_stream *s = isl_stream_new_str(ctx, str);
+       if (!s)
+               return NULL;
+       map = map_read(s, nparam);
+       isl_stream_free(s);
+       return map;
+}
+
 __isl_give isl_set *isl_set_read_from_file(struct isl_ctx *ctx,
-               FILE *input, unsigned nparam, unsigned input_format)
+               FILE *input, int nparam)
+{
+       struct isl_map *map;
+       map = isl_map_read_from_file(ctx, input, nparam);
+       if (!map)
+               return NULL;
+       isl_assert(ctx, isl_map_n_in(map) == 0, goto error);
+       return (struct isl_set *)map;
+error:
+       isl_map_free(map);
+       return NULL;
+}
+
+struct isl_set *isl_set_read_from_str(struct isl_ctx *ctx,
+               const char *str, int nparam)
 {
        struct isl_map *map;
-       map = isl_map_read_from_file(ctx, input, nparam, input_format);
+       map = isl_map_read_from_str(ctx, str, nparam);
        if (!map)
                return NULL;
        isl_assert(ctx, isl_map_n_in(map) == 0, goto error);