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