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