isl_input.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  * Copyright 2010      INRIA Saclay
   4  *
   5  * Use of this software is governed by the GNU LGPLv2.1 license
   6  *
   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
  11  */
  12
  13 #include <ctype.h>
  14 #include <stdio.h>
  15 #include <string.h>
  16 #include <strings.h>
  17 #include <isl_set.h>
  18 #include <isl_seq.h>
  19 #include "isl_stream.h"
  20 #include "isl_map_private.h"
  21
  22 struct variable {
  23         char                    *name;
  24         int                      pos;
  25         struct variable         *next;
  26 };
  27
  28 struct vars {
  29         struct isl_ctx  *ctx;
  30         int              n;
  31         struct variable *v;
  32 };
  33
  34 static struct vars *vars_new(struct isl_ctx *ctx)
  35 {
  36         struct vars *v;
  37         v = isl_alloc_type(ctx, struct vars);
  38         if (!v)
  39                 return NULL;
  40         v->ctx = ctx;
  41         v->n = 0;
  42         v->v = NULL;
  43         return v;
  44 }
  45
  46 static void variable_free(struct variable *var)
  47 {
  48         while (var) {
  49                 struct variable *next = var->next;
  50                 free(var->name);
  51                 free(var);
  52                 var = next;
  53         }
  54 }
  55
  56 static void vars_free(struct vars *v)
  57 {
  58         if (!v)
  59                 return;
  60         variable_free(v->v);
  61         free(v);
  62 }
  63
  64 static void vars_drop(struct vars *v, int n)
  65 {
  66         struct variable *var;
  67
  68         if (!v)
  69                 return;
  70
  71         v->n -= n;
  72
  73         var = v->v;
  74         while (--n >= 0) {
  75                 struct variable *next = var->next;
  76                 free(var->name);
  77                 free(var);
  78                 var = next;
  79         }
  80         v->v = var;
  81 }
  82
  83 static struct variable *variable_new(struct vars *v, const char *name, int len,
  84                                 int pos)
  85 {
  86         struct variable *var;
  87         var = isl_alloc_type(v->ctx, struct variable);
  88         if (!var)
  89                 goto error;
  90         var->name = strdup(name);
  91         var->name[len] = '\0';
  92         var->pos = pos;
  93         var->next = v->v;
  94         return var;
  95 error:
  96         variable_free(v->v);
  97         return NULL;
  98 }
  99
 100 static int vars_pos(struct vars *v, const char *s, int len)
 101 {
 102         int pos;
 103         struct variable *q;
 104
 105         if (len == -1)
 106                 len = strlen(s);
 107         for (q = v->v; q; q = q->next) {
 108                 if (strncmp(q->name, s, len) == 0 && q->name[len] == '\0')
 109                         break;
 110         }
 111         if (q)
 112                 pos = q->pos;
 113         else {
 114                 pos = v->n;
 115                 v->v = variable_new(v, s, len, v->n);
 116                 if (!v->v)
 117                         return -1;
 118                 v->n++;
 119         }
 120         return pos;
 121 }
 122
 123 static struct vars *read_var_list(struct isl_stream *s, struct vars *v)
 124 {
 125         struct isl_token *tok;
 126
 127         while ((tok = isl_stream_next_token(s)) != NULL) {
 128                 int p;
 129                 int n = v->n;
 130
 131                 if (tok->type != ISL_TOKEN_IDENT)
 132                         break;
 133
 134                 p = vars_pos(v, tok->u.s, -1);
 135                 if (p < 0)
 136                         goto error;
 137                 if (p < n) {
 138                         isl_stream_error(s, tok, "expecting unique identifier");
 139                         goto error;
 140                 }
 141                 isl_token_free(tok);
 142                 tok = isl_stream_next_token(s);
 143                 if (!tok || tok->type != ',')
 144                         break;
 145
 146                 isl_token_free(tok);
 147         }
 148         if (tok)
 149                 isl_stream_push_token(s, tok);
 150
 151         return v;
 152 error:
 153         isl_token_free(tok);
 154         vars_free(v);
 155         return NULL;
 156 }
 157
 158 static struct isl_vec *accept_affine(struct isl_stream *s, struct vars *v)
 159 {
 160         struct isl_token *tok = NULL;
 161         struct isl_vec *aff;
 162         int sign = 1;
 163
 164         aff = isl_vec_alloc(v->ctx, 1 + v->n);
 165         isl_seq_clr(aff->el, aff->size);
 166         if (!aff)
 167                 return NULL;
 168
 169         for (;;) {
 170                 tok = isl_stream_next_token(s);
 171                 if (!tok) {
 172                         isl_stream_error(s, NULL, "unexpected EOF");
 173                         goto error;
 174                 }
 175                 if (tok->type == ISL_TOKEN_IDENT) {
 176                         int n = v->n;
 177                         int pos = vars_pos(v, tok->u.s, -1);
 178                         if (pos < 0)
 179                                 goto error;
 180                         if (pos >= n) {
 181                                 isl_stream_error(s, tok, "unknown identifier");
 182                                 goto error;
 183                         }
 184                         if (sign > 0)
 185                                 isl_int_add_ui(aff->el[1 + pos],
 186                                                aff->el[1 + pos], 1);
 187                         else
 188                                 isl_int_sub_ui(aff->el[1 + pos],
 189                                                aff->el[1 + pos], 1);
 190                         sign = 1;
 191                 } else if (tok->type == ISL_TOKEN_VALUE) {
 192                         struct isl_token *tok2;
 193                         int n = v->n;
 194                         int pos = -1;
 195                         tok2 = isl_stream_next_token(s);
 196                         if (tok2 && tok2->type == ISL_TOKEN_IDENT) {
 197                                 pos = vars_pos(v, tok2->u.s, -1);
 198                                 if (pos < 0)
 199                                         goto error;
 200                                 if (pos >= n) {
 201                                         isl_stream_error(s, tok2,
 202                                                 "unknown identifier");
 203                                         isl_token_free(tok2);
 204                                         goto error;
 205                                 }
 206                                 isl_token_free(tok2);
 207                         } else if (tok2)
 208                                 isl_stream_push_token(s, tok2);
 209                         if (sign < 0)
 210                                 isl_int_neg(tok->u.v, tok->u.v);
 211                         isl_int_add(aff->el[1 + pos],
 212                                         aff->el[1 + pos], tok->u.v);
 213                         sign = 1;
 214                 } else if (tok->type == '-') {
 215                         sign = -sign;
 216                 } else if (tok->type == '+') {
 217                         /* nothing */
 218                 } else {
 219                         isl_stream_push_token(s, tok);
 220                         break;
 221                 }
 222                 isl_token_free(tok);
 223         }
 224
 225         return aff;
 226 error:
 227         isl_vec_free(aff);
 228         return NULL;
 229 }
 230
 231 static __isl_give isl_mat *accept_affine_list(struct isl_stream *s,
 232         struct vars *v)
 233 {
 234         struct isl_vec *vec;
 235         struct isl_mat *mat;
 236         struct isl_token *tok = NULL;
 237
 238         vec = accept_affine(s, v);
 239         mat = isl_mat_from_row_vec(vec);
 240         if (!mat)
 241                 return NULL;
 242
 243         for (;;) {
 244                 tok = isl_stream_next_token(s);
 245                 if (!tok) {
 246                         isl_stream_error(s, NULL, "unexpected EOF");
 247                         goto error;
 248                 }
 249                 if (tok->type != ',') {
 250                         isl_stream_push_token(s, tok);
 251                         break;
 252                 }
 253                 isl_token_free(tok);
 254
 255                 vec = accept_affine(s, v);
 256                 mat = isl_mat_vec_concat(mat, vec);
 257                 if (!mat)
 258                         return NULL;
 259         }
 260
 261         return mat;
 262 error:
 263         isl_mat_free(mat);
 264         return NULL;
 265 }
 266
 267 static struct isl_basic_map *add_div_definition(struct isl_stream *s,
 268         struct vars *v, struct isl_basic_map *bmap, int k)
 269 {
 270         struct isl_token *tok;
 271         int seen_paren = 0;
 272         struct isl_vec *aff;
 273
 274         if (isl_stream_eat(s, '['))
 275                 goto error;
 276
 277         tok = isl_stream_next_token(s);
 278         if (!tok)
 279                 goto error;
 280         if (tok->type == '(') {
 281                 seen_paren = 1;
 282                 isl_token_free(tok);
 283         } else
 284                 isl_stream_push_token(s, tok);
 285
 286         aff = accept_affine(s, v);
 287         if (!aff)
 288                 goto error;
 289
 290         isl_seq_cpy(bmap->div[k] + 1, aff->el, aff->size);
 291
 292         isl_vec_free(aff);
 293
 294         if (seen_paren && isl_stream_eat(s, ')'))
 295                 goto error;
 296         if (isl_stream_eat(s, '/'))
 297                 goto error;
 298
 299         tok = isl_stream_next_token(s);
 300         if (!tok)
 301                 goto error;
 302         if (tok->type != ISL_TOKEN_VALUE) {
 303                 isl_stream_error(s, tok, "expected denominator");
 304                 isl_stream_push_token(s, tok);
 305                 goto error;
 306         }
 307         isl_int_set(bmap->div[k][0], tok->u.v);
 308         isl_token_free(tok);
 309
 310         if (isl_stream_eat(s, ']'))
 311                 goto error;
 312
 313         if (isl_basic_map_add_div_constraints(bmap, k) < 0)
 314                 goto error;
 315
 316         return bmap;
 317 error:
 318         isl_basic_map_free(bmap);
 319         return NULL;
 320 }
 321
 322 static struct isl_basic_map *read_defined_var_list(struct isl_stream *s,
 323         struct vars *v, struct isl_basic_map *bmap)
 324 {
 325         struct isl_token *tok;
 326
 327         while ((tok = isl_stream_next_token(s)) != NULL) {
 328                 int k;
 329                 int p;
 330                 int n = v->n;
 331                 unsigned total = isl_basic_map_total_dim(bmap);
 332
 333                 if (tok->type != ISL_TOKEN_IDENT)
 334                         break;
 335
 336                 p = vars_pos(v, tok->u.s, -1);
 337                 if (p < 0)
 338                         goto error;
 339                 if (p < n) {
 340                         isl_stream_error(s, tok, "expecting unique identifier");
 341                         goto error;
 342                 }
 343                 isl_token_free(tok);
 344
 345                 bmap = isl_basic_map_cow(bmap);
 346                 bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
 347                                                 1, 0, 2);
 348
 349                 if ((k = isl_basic_map_alloc_div(bmap)) < 0)
 350                         goto error;
 351                 isl_seq_clr(bmap->div[k], 1 + 1 + total);
 352
 353                 tok = isl_stream_next_token(s);
 354                 if (tok && tok->type == '=') {
 355                         isl_token_free(tok);
 356                         bmap = add_div_definition(s, v, bmap, k);
 357                         tok = isl_stream_next_token(s);
 358                 }
 359
 360                 if (!tok || tok->type != ',')
 361                         break;
 362
 363                 isl_token_free(tok);
 364         }
 365         if (tok)
 366                 isl_stream_push_token(s, tok);
 367
 368         return bmap;
 369 error:
 370         isl_token_free(tok);
 371         isl_basic_map_free(bmap);
 372         return NULL;
 373 }
 374
 375 static struct vars *read_tuple(struct isl_stream *s, struct vars *v)
 376 {
 377         struct isl_token *tok;
 378
 379         tok = isl_stream_next_token(s);
 380         if (!tok || tok->type != '[') {
 381                 isl_stream_error(s, tok, "expecting '['");
 382                 goto error;
 383         }
 384         isl_token_free(tok);
 385         v = read_var_list(s, v);
 386         tok = isl_stream_next_token(s);
 387         if (!tok || tok->type != ']') {
 388                 isl_stream_error(s, tok, "expecting ']'");
 389                 goto error;
 390         }
 391         isl_token_free(tok);
 392
 393         return v;
 394 error:
 395         if (tok)
 396                 isl_token_free(tok);
 397         vars_free(v);
 398         return NULL;
 399 }
 400
 401 static struct isl_basic_map *add_constraints(struct isl_stream *s,
 402         struct vars *v, struct isl_basic_map *bmap);
 403
 404 static struct isl_basic_map *add_exists(struct isl_stream *s,
 405         struct vars *v, struct isl_basic_map *bmap)
 406 {
 407         struct isl_token *tok;
 408         int n = v->n;
 409         int extra;
 410         int seen_paren = 0;
 411         int i;
 412         unsigned total;
 413
 414         tok = isl_stream_next_token(s);
 415         if (!tok)
 416                 goto error;
 417         if (tok->type == '(') {
 418                 seen_paren = 1;
 419                 isl_token_free(tok);
 420         } else
 421                 isl_stream_push_token(s, tok);
 422
 423         bmap = read_defined_var_list(s, v, bmap);
 424         if (!bmap)
 425                 goto error;
 426
 427         if (isl_stream_eat(s, ':'))
 428                 goto error;
 429         bmap = add_constraints(s, v, bmap);
 430         if (seen_paren && isl_stream_eat(s, ')'))
 431                 goto error;
 432         return bmap;
 433 error:
 434         isl_basic_map_free(bmap);
 435         return NULL;
 436 }
 437
 438 static __isl_give isl_basic_map *construct_constraint(
 439         __isl_take isl_basic_map *bmap, enum isl_token_type type,
 440         isl_int *left, isl_int *right)
 441 {
 442         int k;
 443         unsigned len;
 444         struct isl_ctx *ctx;
 445
 446         if (!bmap)
 447                 return NULL;
 448         len = 1 + isl_basic_map_total_dim(bmap);
 449         ctx = bmap->ctx;
 450
 451         k = isl_basic_map_alloc_inequality(bmap);
 452         if (k < 0)
 453                 goto error;
 454         if (type == ISL_TOKEN_LE)
 455                 isl_seq_combine(bmap->ineq[k], ctx->negone, left,
 456                                                ctx->one, right,
 457                                                len);
 458         else if (type == ISL_TOKEN_GE)
 459                 isl_seq_combine(bmap->ineq[k], ctx->one, left,
 460                                                ctx->negone, right,
 461                                                len);
 462         else if (type == ISL_TOKEN_LT) {
 463                 isl_seq_combine(bmap->ineq[k], ctx->negone, left,
 464                                                ctx->one, right,
 465                                                len);
 466                 isl_int_sub_ui(bmap->ineq[k][0], bmap->ineq[k][0], 1);
 467         } else if (type == ISL_TOKEN_GT) {
 468                 isl_seq_combine(bmap->ineq[k], ctx->one, left,
 469                                                ctx->negone, right,
 470                                                len);
 471                 isl_int_sub_ui(bmap->ineq[k][0], bmap->ineq[k][0], 1);
 472         } else {
 473                 isl_seq_combine(bmap->ineq[k], ctx->one, left,
 474                                                ctx->negone, right,
 475                                                len);
 476                 isl_basic_map_inequality_to_equality(bmap, k);
 477         }
 478
 479         return bmap;
 480 error:
 481         isl_basic_map_free(bmap);
 482         return NULL;
 483 }
 484
 485 static int is_comparator(struct isl_token *tok)
 486 {
 487         if (!tok)
 488                 return 0;
 489
 490         switch (tok->type) {
 491         case ISL_TOKEN_LT:
 492         case ISL_TOKEN_GT:
 493         case ISL_TOKEN_LE:
 494         case ISL_TOKEN_GE:
 495         case '=':
 496                 return 1;
 497         default:
 498                 return 0;
 499         }
 500 }
 501
 502 static struct isl_basic_map *add_constraint(struct isl_stream *s,
 503         struct vars *v, struct isl_basic_map *bmap)
 504 {
 505         int i, j;
 506         unsigned total = isl_basic_map_total_dim(bmap);
 507         struct isl_token *tok = NULL;
 508         struct isl_mat *aff1 = NULL, *aff2 = NULL;
 509
 510         tok = isl_stream_next_token(s);
 511         if (!tok)
 512                 goto error;
 513         if (tok->type == ISL_TOKEN_EXISTS) {
 514                 isl_token_free(tok);
 515                 return add_exists(s, v, bmap);
 516         }
 517         isl_stream_push_token(s, tok);
 518         tok = NULL;
 519
 520         bmap = isl_basic_map_cow(bmap);
 521
 522         aff1 = accept_affine_list(s, v);
 523         if (!aff1)
 524                 goto error;
 525         tok = isl_stream_next_token(s);
 526         if (!is_comparator(tok)) {
 527                 isl_stream_error(s, tok, "missing operator");
 528                 if (tok)
 529                         isl_stream_push_token(s, tok);
 530                 tok = NULL;
 531                 goto error;
 532         }
 533         isl_assert(aff1->ctx, aff1->n_col == 1 + total, goto error);
 534         for (;;) {
 535                 aff2 = accept_affine_list(s, v);
 536                 if (!aff2)
 537                         goto error;
 538                 isl_assert(aff2->ctx, aff2->n_col == 1 + total, goto error);
 539
 540                 bmap = isl_basic_map_extend_constraints(bmap, 0,
 541                                                 aff1->n_row * aff2->n_row);
 542                 for (i = 0; i < aff1->n_row; ++i)
 543                         for (j = 0; j < aff2->n_row; ++j)
 544                                 bmap = construct_constraint(bmap, tok->type,
 545                                                     aff1->row[i], aff2->row[j]);
 546                 isl_token_free(tok);
 547                 isl_mat_free(aff1);
 548                 aff1 = aff2;
 549
 550                 tok = isl_stream_next_token(s);
 551                 if (!is_comparator(tok)) {
 552                         if (tok)
 553                                 isl_stream_push_token(s, tok);
 554                         break;
 555                 }
 556         }
 557         isl_mat_free(aff1);
 558
 559         return bmap;
 560 error:
 561         if (tok)
 562                 isl_token_free(tok);
 563         isl_mat_free(aff1);
 564         isl_mat_free(aff2);
 565         isl_basic_map_free(bmap);
 566         return NULL;
 567 }
 568
 569 static struct isl_basic_map *add_constraints(struct isl_stream *s,
 570         struct vars *v, struct isl_basic_map *bmap)
 571 {
 572         struct isl_token *tok;
 573
 574         for (;;) {
 575                 bmap = add_constraint(s, v, bmap);
 576                 if (!bmap)
 577                         return NULL;
 578                 tok = isl_stream_next_token(s);
 579                 if (!tok) {
 580                         isl_stream_error(s, NULL, "unexpected EOF");
 581                         goto error;
 582                 }
 583                 if (tok->type != ISL_TOKEN_AND)
 584                         break;
 585                 isl_token_free(tok);
 586         }
 587         isl_stream_push_token(s, tok);
 588
 589         return bmap;
 590 error:
 591         if (tok)
 592                 isl_token_free(tok);
 593         isl_basic_map_free(bmap);
 594         return NULL;
 595 }
 596
 597 static struct isl_basic_map *read_disjunct(struct isl_stream *s,
 598         struct vars *v, __isl_take isl_dim *dim)
 599 {
 600         int seen_paren = 0;
 601         struct isl_token *tok;
 602         struct isl_basic_map *bmap;
 603
 604         bmap = isl_basic_map_alloc_dim(dim, 0, 0, 0);
 605         if (!bmap)
 606                 return NULL;
 607
 608         tok = isl_stream_next_token(s);
 609         if (!tok)
 610                 goto error;
 611         if (tok->type == '(') {
 612                 seen_paren = 1;
 613                 isl_token_free(tok);
 614         } else
 615                 isl_stream_push_token(s, tok);
 616
 617         bmap = add_constraints(s, v, bmap);
 618         bmap = isl_basic_map_simplify(bmap);
 619         bmap = isl_basic_map_finalize(bmap);
 620
 621         if (seen_paren && isl_stream_eat(s, ')'))
 622                 goto error;
 623
 624         return bmap;
 625 error:
 626         isl_basic_map_free(bmap);
 627         return NULL;
 628 }
 629
 630 static struct isl_map *read_disjuncts(struct isl_stream *s,
 631         struct vars *v, __isl_take isl_dim *dim)
 632 {
 633         struct isl_token *tok;
 634         struct isl_map *map;
 635
 636         tok = isl_stream_next_token(s);
 637         if (!tok) {
 638                 isl_stream_error(s, NULL, "unexpected EOF");
 639                 goto error;
 640         }
 641         if (tok->type == '}') {
 642                 isl_stream_push_token(s, tok);
 643                 return isl_map_universe(dim);
 644         }
 645         isl_stream_push_token(s, tok);
 646
 647         map = isl_map_empty(isl_dim_copy(dim));
 648         for (;;) {
 649                 struct isl_basic_map *bmap;
 650                 int n = v->n;
 651
 652                 bmap = read_disjunct(s, v, isl_dim_copy(dim));
 653                 map = isl_map_union(map, isl_map_from_basic_map(bmap));
 654
 655                 vars_drop(v, v->n - n);
 656
 657                 tok = isl_stream_next_token(s);
 658                 if (!tok || tok->type != ISL_TOKEN_OR)
 659                         break;
 660                 isl_token_free(tok);
 661         }
 662         if (tok)
 663                 isl_stream_push_token(s, tok);
 664
 665         isl_dim_free(dim);
 666         return map;
 667 error:
 668         isl_dim_free(dim);
 669         return NULL;
 670 }
 671
 672 static int polylib_pos_to_isl_pos(__isl_keep isl_basic_map *bmap, int pos)
 673 {
 674         if (pos < isl_basic_map_dim(bmap, isl_dim_out))
 675                 return 1 + isl_basic_map_dim(bmap, isl_dim_param) +
 676                            isl_basic_map_dim(bmap, isl_dim_in) + pos;
 677         pos -= isl_basic_map_dim(bmap, isl_dim_out);
 678
 679         if (pos < isl_basic_map_dim(bmap, isl_dim_in))
 680                 return 1 + isl_basic_map_dim(bmap, isl_dim_param) + pos;
 681         pos -= isl_basic_map_dim(bmap, isl_dim_in);
 682
 683         if (pos < isl_basic_map_dim(bmap, isl_dim_div))
 684                 return 1 + isl_basic_map_dim(bmap, isl_dim_param) +
 685                            isl_basic_map_dim(bmap, isl_dim_in) +
 686                            isl_basic_map_dim(bmap, isl_dim_out) + pos;
 687         pos -= isl_basic_map_dim(bmap, isl_dim_div);
 688
 689         if (pos < isl_basic_map_dim(bmap, isl_dim_param))
 690                 return 1 + pos;
 691
 692         return 0;
 693 }
 694
 695 static __isl_give isl_basic_map *basic_map_read_polylib_constraint(
 696         struct isl_stream *s, __isl_take isl_basic_map *bmap)
 697 {
 698         int j;
 699         struct isl_token *tok;
 700         int type;
 701         int k;
 702         isl_int *c;
 703         unsigned nparam;
 704         unsigned dim;
 705
 706         if (!bmap)
 707                 return NULL;
 708
 709         nparam = isl_basic_map_dim(bmap, isl_dim_param);
 710         dim = isl_basic_map_dim(bmap, isl_dim_out);
 711
 712         tok = isl_stream_next_token(s);
 713         if (!tok || tok->type != ISL_TOKEN_VALUE) {
 714                 isl_stream_error(s, tok, "expecting coefficient");
 715                 if (tok)
 716                         isl_stream_push_token(s, tok);
 717                 goto error;
 718         }
 719         if (!tok->on_new_line) {
 720                 isl_stream_error(s, tok, "coefficient should appear on new line");
 721                 isl_stream_push_token(s, tok);
 722                 goto error;
 723         }
 724
 725         type = isl_int_get_si(tok->u.v);
 726         isl_token_free(tok);
 727
 728         isl_assert(s->ctx, type == 0 || type == 1, goto error);
 729         if (type == 0) {
 730                 k = isl_basic_map_alloc_equality(bmap);
 731                 c = bmap->eq[k];
 732         } else {
 733                 k = isl_basic_map_alloc_inequality(bmap);
 734                 c = bmap->ineq[k];
 735         }
 736         if (k < 0)
 737                 goto error;
 738
 739         for (j = 0; j < 1 + isl_basic_map_total_dim(bmap); ++j) {
 740                 int pos;
 741                 tok = isl_stream_next_token(s);
 742                 if (!tok || tok->type != ISL_TOKEN_VALUE) {
 743                         isl_stream_error(s, tok, "expecting coefficient");
 744                         if (tok)
 745                                 isl_stream_push_token(s, tok);
 746                         goto error;
 747                 }
 748                 if (tok->on_new_line) {
 749                         isl_stream_error(s, tok,
 750                                 "coefficient should not appear on new line");
 751                         isl_stream_push_token(s, tok);
 752                         goto error;
 753                 }
 754                 pos = polylib_pos_to_isl_pos(bmap, j);
 755                 isl_int_set(c[pos], tok->u.v);
 756                 isl_token_free(tok);
 757         }
 758
 759         return bmap;
 760 error:
 761         isl_basic_map_free(bmap);
 762         return NULL;
 763 }
 764
 765 static __isl_give isl_basic_map *basic_map_read_polylib(struct isl_stream *s,
 766         int nparam)
 767 {
 768         int i;
 769         struct isl_token *tok;
 770         struct isl_token *tok2;
 771         int n_row, n_col;
 772         int on_new_line;
 773         unsigned in = 0, out, local = 0;
 774         struct isl_basic_map *bmap = NULL;
 775
 776         if (nparam < 0)
 777                 nparam = 0;
 778
 779         tok = isl_stream_next_token(s);
 780         if (!tok) {
 781                 isl_stream_error(s, NULL, "unexpected EOF");
 782                 return NULL;
 783         }
 784         tok2 = isl_stream_next_token(s);
 785         if (!tok2) {
 786                 isl_token_free(tok);
 787                 isl_stream_error(s, NULL, "unexpected EOF");
 788                 return NULL;
 789         }
 790         n_row = isl_int_get_si(tok->u.v);
 791         n_col = isl_int_get_si(tok2->u.v);
 792         on_new_line = tok2->on_new_line;
 793         isl_token_free(tok2);
 794         isl_token_free(tok);
 795         isl_assert(s->ctx, !on_new_line, return NULL);
 796         isl_assert(s->ctx, n_row >= 0, return NULL);
 797         isl_assert(s->ctx, n_col >= 2 + nparam, return NULL);
 798         tok = isl_stream_next_token_on_same_line(s);
 799         if (tok) {
 800                 if (tok->type != ISL_TOKEN_VALUE) {
 801                         isl_stream_error(s, tok,
 802                                     "expecting number of output dimensions");
 803                         isl_stream_push_token(s, tok);
 804                         goto error;
 805                 }
 806                 out = isl_int_get_si(tok->u.v);
 807                 isl_token_free(tok);
 808
 809                 tok = isl_stream_next_token_on_same_line(s);
 810                 if (!tok || tok->type != ISL_TOKEN_VALUE) {
 811                         isl_stream_error(s, tok,
 812                                     "expecting number of input dimensions");
 813                         if (tok)
 814                                 isl_stream_push_token(s, tok);
 815                         goto error;
 816                 }
 817                 in = isl_int_get_si(tok->u.v);
 818                 isl_token_free(tok);
 819
 820                 tok = isl_stream_next_token_on_same_line(s);
 821                 if (!tok || tok->type != ISL_TOKEN_VALUE) {
 822                         isl_stream_error(s, tok,
 823                                     "expecting number of existentials");
 824                         if (tok)
 825                                 isl_stream_push_token(s, tok);
 826                         goto error;
 827                 }
 828                 local = isl_int_get_si(tok->u.v);
 829                 isl_token_free(tok);
 830
 831                 tok = isl_stream_next_token_on_same_line(s);
 832                 if (!tok || tok->type != ISL_TOKEN_VALUE) {
 833                         isl_stream_error(s, tok,
 834                                     "expecting number of parameters");
 835                         if (tok)
 836                                 isl_stream_push_token(s, tok);
 837                         goto error;
 838                 }
 839                 nparam = isl_int_get_si(tok->u.v);
 840                 isl_token_free(tok);
 841                 if (n_col != 1 + out + in + local + nparam + 1) {
 842                         isl_stream_error(s, NULL,
 843                                     "dimensions don't match");
 844                         goto error;
 845                 }
 846         } else
 847                 out = n_col - 2 - nparam;
 848         bmap = isl_basic_map_alloc(s->ctx, nparam, in, out, local, n_row, n_row);
 849         if (!bmap)
 850                 return NULL;
 851
 852         for (i = 0; i < local; ++i) {
 853                 int k = isl_basic_map_alloc_div(bmap);
 854                 if (k < 0)
 855                         goto error;
 856         }
 857
 858         for (i = 0; i < n_row; ++i)
 859                 bmap = basic_map_read_polylib_constraint(s, bmap);
 860
 861         bmap = isl_basic_map_simplify(bmap);
 862         bmap = isl_basic_map_finalize(bmap);
 863         return bmap;
 864 error:
 865         isl_basic_map_free(bmap);
 866         return NULL;
 867 }
 868
 869 static struct isl_map *map_read_polylib(struct isl_stream *s, int nparam)
 870 {
 871         struct isl_token *tok;
 872         struct isl_token *tok2;
 873         int i, n;
 874         struct isl_map *map;
 875
 876         tok = isl_stream_next_token(s);
 877         if (!tok) {
 878                 isl_stream_error(s, NULL, "unexpected EOF");
 879                 return NULL;
 880         }
 881         tok2 = isl_stream_next_token(s);
 882         if (!tok2) {
 883                 isl_token_free(tok);
 884                 isl_stream_error(s, NULL, "unexpected EOF");
 885                 return NULL;
 886         }
 887         if (!tok2->on_new_line) {
 888                 isl_stream_push_token(s, tok2);
 889                 isl_stream_push_token(s, tok);
 890                 return isl_map_from_basic_map(basic_map_read_polylib(s, nparam));
 891         }
 892         isl_stream_push_token(s, tok2);
 893         n = isl_int_get_si(tok->u.v);
 894         isl_token_free(tok);
 895
 896         isl_assert(s->ctx, n >= 1, return NULL);
 897
 898         map = isl_map_from_basic_map(basic_map_read_polylib(s, nparam));
 899
 900         for (i = 1; i < n; ++i)
 901                 map = isl_map_union(map,
 902                         isl_map_from_basic_map(basic_map_read_polylib(s, nparam)));
 903
 904         return map;
 905 }
 906
 907 static struct isl_dim *set_names(struct isl_dim *dim, struct vars *vars,
 908         enum isl_dim_type type, int offset, int n)
 909 {
 910         int i;
 911         struct variable *v;
 912
 913         for (i = 0, v = vars->v; i < offset; ++i, v = v->next)
 914                 ;
 915         for (i = n - 1; i >= 0; --i, v = v->next) {
 916                 char *prime = strchr(v->name, '\'');
 917                 if (prime)
 918                         *prime = '\0';
 919                 dim = isl_dim_set_name(dim, type, i, v->name);
 920                 if (prime)
 921                         *prime = '\'';
 922         }
 923
 924         return dim;
 925 }
 926
 927 static struct isl_dim *dim_from_vars(struct vars *vars,
 928         int nparam, int n_in, int n_out)
 929 {
 930         struct isl_dim *dim;
 931
 932         dim = isl_dim_alloc(vars->ctx, nparam, n_in, n_out);
 933         dim = set_names(dim, vars, isl_dim_param, n_out + n_in, nparam);
 934         dim = set_names(dim, vars, isl_dim_in, n_out, n_in);
 935         dim = set_names(dim, vars, isl_dim_out, 0, n_out);
 936
 937         return dim;
 938 }
 939
 940 static struct isl_map *map_read(struct isl_stream *s, int nparam)
 941 {
 942         struct isl_dim *dim = NULL;
 943         struct isl_map *map = NULL;
 944         struct isl_token *tok;
 945         struct vars *v = NULL;
 946         int n1;
 947         int n2;
 948
 949         tok = isl_stream_next_token(s);
 950         if (!tok) {
 951                 isl_stream_error(s, NULL, "unexpected EOF");
 952                 goto error;
 953         }
 954         if (tok->type == ISL_TOKEN_VALUE) {
 955                 isl_stream_push_token(s, tok);
 956                 return map_read_polylib(s, nparam);
 957         }
 958         v = vars_new(s->ctx);
 959         if (tok->type == '[') {
 960                 isl_stream_push_token(s, tok);
 961                 v = read_tuple(s, v);
 962                 if (!v)
 963                         return NULL;
 964                 if (nparam >= 0)
 965                         isl_assert(s->ctx, nparam == v->n, goto error);
 966                 nparam = v->n;
 967                 tok = isl_stream_next_token(s);
 968                 if (!tok || tok->type != ISL_TOKEN_TO) {
 969                         isl_stream_error(s, tok, "expecting '->'");
 970                         if (tok)
 971                                 isl_stream_push_token(s, tok);
 972                         goto error;
 973                 }
 974                 isl_token_free(tok);
 975                 tok = isl_stream_next_token(s);
 976         }
 977         if (nparam < 0)
 978                 nparam = 0;
 979         if (!tok || tok->type != '{') {
 980                 isl_stream_error(s, tok, "expecting '{'");
 981                 if (tok)
 982                         isl_stream_push_token(s, tok);
 983                 goto error;
 984         }
 985         isl_token_free(tok);
 986         v = read_tuple(s, v);
 987         if (!v)
 988                 return NULL;
 989         n1 = v->n - nparam;
 990         tok = isl_stream_next_token(s);
 991         if (tok && tok->type == ISL_TOKEN_TO) {
 992                 isl_token_free(tok);
 993                 v = read_tuple(s, v);
 994                 if (!v)
 995                         return NULL;
 996                 n2 = v->n - n1 - nparam;
 997         } else {
 998                 if (tok)
 999                         isl_stream_push_token(s, tok);
1000                 n2 = n1;
1001                 n1 = 0;
1002         }
1003         dim = dim_from_vars(v, nparam, n1, n2);
1004         tok = isl_stream_next_token(s);
1005         if (!tok) {
1006                 isl_stream_error(s, NULL, "unexpected EOF");
1007                 goto error;
1008         }
1009         if (tok->type == ':') {
1010                 isl_token_free(tok);
1011                 map = read_disjuncts(s, v, isl_dim_copy(dim));
1012                 tok = isl_stream_next_token(s);
1013         } else
1014                 map = isl_map_universe(isl_dim_copy(dim));
1015         if (tok && tok->type == '}') {
1016                 isl_token_free(tok);
1017         } else {
1018                 isl_stream_error(s, tok, "unexpected isl_token");
1019                 if (tok)
1020                         isl_token_free(tok);
1021                 goto error;
1022         }
1023         vars_free(v);
1024         isl_dim_free(dim);
1025
1026         return map;
1027 error:
1028         isl_dim_free(dim);
1029         isl_map_free(map);
1030         if (v)
1031                 vars_free(v);
1032         return NULL;
1033 }
1034
1035 static struct isl_basic_map *basic_map_read(struct isl_stream *s, int nparam)
1036 {
1037         struct isl_map *map;
1038         struct isl_basic_map *bmap;
1039
1040         map = map_read(s, nparam);
1041         if (!map)
1042                 return NULL;
1043
1044         isl_assert(map->ctx, map->n <= 1, goto error);
1045
1046         if (map->n == 0)
1047                 bmap = isl_basic_map_empty_like_map(map);
1048         else
1049                 bmap = isl_basic_map_copy(map->p[0]);
1050
1051         isl_map_free(map);
1052
1053         return bmap;
1054 error:
1055         isl_map_free(map);
1056         return NULL;
1057 }
1058
1059 __isl_give isl_basic_map *isl_basic_map_read_from_file(isl_ctx *ctx,
1060                 FILE *input, int nparam)
1061 {
1062         struct isl_basic_map *bmap;
1063         struct isl_stream *s = isl_stream_new_file(ctx, input);
1064         if (!s)
1065                 return NULL;
1066         bmap = basic_map_read(s, nparam);
1067         isl_stream_free(s);
1068         return bmap;
1069 }
1070
1071 __isl_give isl_basic_set *isl_basic_set_read_from_file(isl_ctx *ctx,
1072                 FILE *input, int nparam)
1073 {
1074         struct isl_basic_map *bmap;
1075         bmap = isl_basic_map_read_from_file(ctx, input, nparam);
1076         if (!bmap)
1077                 return NULL;
1078         isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
1079         return (struct isl_basic_set *)bmap;
1080 error:
1081         isl_basic_map_free(bmap);
1082         return NULL;
1083 }
1084
1085 struct isl_basic_map *isl_basic_map_read_from_str(struct isl_ctx *ctx,
1086                 const char *str, int nparam)
1087 {
1088         struct isl_basic_map *bmap;
1089         struct isl_stream *s = isl_stream_new_str(ctx, str);
1090         if (!s)
1091                 return NULL;
1092         bmap = basic_map_read(s, nparam);
1093         isl_stream_free(s);
1094         return bmap;
1095 }
1096
1097 struct isl_basic_set *isl_basic_set_read_from_str(struct isl_ctx *ctx,
1098                 const char *str, int nparam)
1099 {
1100         struct isl_basic_map *bmap;
1101         bmap = isl_basic_map_read_from_str(ctx, str, nparam);
1102         if (!bmap)
1103                 return NULL;
1104         isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
1105         return (struct isl_basic_set *)bmap;
1106 error:
1107         isl_basic_map_free(bmap);
1108         return NULL;
1109 }
1110
1111 __isl_give isl_map *isl_map_read_from_file(struct isl_ctx *ctx,
1112                 FILE *input, int nparam)
1113 {
1114         struct isl_map *map;
1115         struct isl_stream *s = isl_stream_new_file(ctx, input);
1116         if (!s)
1117                 return NULL;
1118         map = map_read(s, nparam);
1119         isl_stream_free(s);
1120         return map;
1121 }
1122
1123 __isl_give isl_map *isl_map_read_from_str(struct isl_ctx *ctx,
1124                 const char *str, int nparam)
1125 {
1126         struct isl_map *map;
1127         struct isl_stream *s = isl_stream_new_str(ctx, str);
1128         if (!s)
1129                 return NULL;
1130         map = map_read(s, nparam);
1131         isl_stream_free(s);
1132         return map;
1133 }
1134
1135 __isl_give isl_set *isl_set_read_from_file(struct isl_ctx *ctx,
1136                 FILE *input, int nparam)
1137 {
1138         struct isl_map *map;
1139         map = isl_map_read_from_file(ctx, input, nparam);
1140         if (!map)
1141                 return NULL;
1142         isl_assert(ctx, isl_map_n_in(map) == 0, goto error);
1143         return (struct isl_set *)map;
1144 error:
1145         isl_map_free(map);
1146         return NULL;
1147 }
1148
1149 struct isl_set *isl_set_read_from_str(struct isl_ctx *ctx,
1150                 const char *str, int nparam)
1151 {
1152         struct isl_map *map;
1153         map = isl_map_read_from_str(ctx, str, nparam);
1154         if (!map)
1155                 return NULL;
1156         isl_assert(ctx, isl_map_n_in(map) == 0, goto error);
1157         return (struct isl_set *)map;
1158 error:
1159         isl_map_free(map);
1160         return NULL;
1161 }
1162
1163 static char *next_line(FILE *input, char *line, unsigned len)
1164 {
1165         char *p;
1166
1167         do {
1168                 if (!(p = fgets(line, len, input)))
1169                         return NULL;
1170                 while (isspace(*p) && *p != '\n')
1171                         ++p;
1172         } while (*p == '#' || *p == '\n');
1173
1174         return p;
1175 }
1176
1177 static struct isl_vec *isl_vec_read_from_file_polylib(struct isl_ctx *ctx,
1178                 FILE *input)
1179 {
1180         struct isl_vec *vec = NULL;
1181         char line[1024];
1182         char val[1024];
1183         char *p;
1184         unsigned size;
1185         int j;
1186         int n;
1187         int offset;
1188
1189         isl_assert(ctx, next_line(input, line, sizeof(line)), return NULL);
1190         isl_assert(ctx, sscanf(line, "%u", &size) == 1, return NULL);
1191
1192         vec = isl_vec_alloc(ctx, size);
1193
1194         p = next_line(input, line, sizeof(line));
1195         isl_assert(ctx, p, goto error);
1196
1197         for (j = 0; j < size; ++j) {
1198                 n = sscanf(p, "%s%n", val, &offset);
1199                 isl_assert(ctx, n != 0, goto error);
1200                 isl_int_read(vec->el[j], val);
1201                 p += offset;
1202         }
1203
1204         return vec;
1205 error:
1206         isl_vec_free(vec);
1207         return NULL;
1208 }
1209
1210 struct isl_vec *isl_vec_read_from_file(struct isl_ctx *ctx,
1211                 FILE *input, unsigned input_format)
1212 {
1213         if (input_format == ISL_FORMAT_POLYLIB)
1214                 return isl_vec_read_from_file_polylib(ctx, input);
1215         else
1216                 isl_assert(ctx, 0, return NULL);
1217 }