isl_input_omega.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 <string.h>
  15 #include <strings.h>
  16 #include <isl_seq.h>
  17 #include "isl_stream.h"
  18 #include "isl_map_private.h"
  19 #include "isl_input_omega.h"
  20
  21 struct variable {
  22         char                    *name;
  23         int                      pos;
  24         struct variable         *next;
  25 };
  26
  27 struct vars {
  28         struct isl_ctx  *ctx;
  29         int              n;
  30         struct variable *v;
  31 };
  32
  33 static struct vars *vars_new(struct isl_ctx *ctx)
  34 {
  35         struct vars *v;
  36         v = isl_alloc_type(ctx, struct vars);
  37         if (!v)
  38                 return NULL;
  39         v->ctx = ctx;
  40         v->n = 0;
  41         v->v = NULL;
  42         return v;
  43 }
  44
  45 static void variable_free(struct variable *var)
  46 {
  47         while (var) {
  48                 struct variable *next = var->next;
  49                 free(var->name);
  50                 free(var);
  51                 var = next;
  52         }
  53 }
  54
  55 static void vars_free(struct vars *v)
  56 {
  57         if (!v)
  58                 return;
  59         variable_free(v->v);
  60         free(v);
  61 }
  62
  63 static struct variable *variable_new(struct vars *v, const char *name, int len,
  64                                 int pos)
  65 {
  66         struct variable *var;
  67         var = isl_alloc_type(v->ctx, struct variable);
  68         if (!var)
  69                 goto error;
  70         var->name = strdup(name);
  71         var->name[len] = '\0';
  72         var->pos = pos;
  73         var->next = v->v;
  74         return var;
  75 error:
  76         variable_free(v->v);
  77         return NULL;
  78 }
  79
  80 static int vars_pos(struct vars *v, const char *s, int len)
  81 {
  82         int pos;
  83         struct variable *q;
  84
  85         if (len == -1)
  86                 len = strlen(s);
  87         for (q = v->v; q; q = q->next) {
  88                 if (strncmp(q->name, s, len) == 0 && q->name[len] == '\0')
  89                         break;
  90         }
  91         if (q)
  92                 pos = q->pos;
  93         else {
  94                 pos = v->n;
  95                 v->v = variable_new(v, s, len, v->n);
  96                 if (!v->v)
  97                         return -1;
  98                 v->n++;
  99         }
 100         return pos;
 101 }
 102
 103 static struct vars *read_var_list(struct isl_stream *s, struct vars *v)
 104 {
 105         struct isl_token *tok;
 106
 107         while ((tok = isl_stream_next_token(s)) != NULL) {
 108                 int p;
 109                 int n = v->n;
 110
 111                 if (tok->type != ISL_TOKEN_IDENT)
 112                         break;
 113
 114                 p = vars_pos(v, tok->u.s, -1);
 115                 if (p < 0)
 116                         goto error;
 117                 if (p < n) {
 118                         isl_stream_error(s, tok, "expecting unique identifier");
 119                         goto error;
 120                 }
 121                 isl_token_free(tok);
 122                 tok = isl_stream_next_token(s);
 123                 if (!tok || tok->type != ',')
 124                         break;
 125
 126                 isl_token_free(tok);
 127         }
 128         if (tok)
 129                 isl_stream_push_token(s, tok);
 130
 131         return v;
 132 error:
 133         isl_token_free(tok);
 134         vars_free(v);
 135         return NULL;
 136 }
 137
 138 static struct vars *read_tuple(struct isl_stream *s, struct vars *v)
 139 {
 140         struct isl_token *tok;
 141
 142         tok = isl_stream_next_token(s);
 143         if (!tok || tok->type != '[') {
 144                 isl_stream_error(s, tok, "expecting '['");
 145                 goto error;
 146         }
 147         isl_token_free(tok);
 148         v = read_var_list(s, v);
 149         tok = isl_stream_next_token(s);
 150         if (!tok || tok->type != ']') {
 151                 isl_stream_error(s, tok, "expecting ']'");
 152                 goto error;
 153         }
 154         isl_token_free(tok);
 155
 156         return v;
 157 error:
 158         if (tok)
 159                 isl_token_free(tok);
 160         vars_free(v);
 161         return NULL;
 162 }
 163
 164 static struct isl_basic_map *add_constraints(struct isl_stream *s,
 165         struct vars **v, struct isl_basic_map *bmap);
 166
 167 static struct isl_basic_map *add_exists(struct isl_stream *s,
 168         struct vars **v, struct isl_basic_map *bmap)
 169 {
 170         struct isl_token *tok;
 171         int n = (*v)->n;
 172         int extra;
 173         int seen_paren = 0;
 174         int i;
 175         unsigned total;
 176
 177         tok = isl_stream_next_token(s);
 178         if (!tok)
 179                 goto error;
 180         if (tok->type == '(') {
 181                 seen_paren = 1;
 182                 isl_token_free(tok);
 183         } else
 184                 isl_stream_push_token(s, tok);
 185         *v = read_var_list(s, *v);
 186         if (!*v)
 187                 goto error;
 188         extra = (*v)->n - n;
 189         bmap = isl_basic_map_cow(bmap);
 190         bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
 191                         extra, 0, 0);
 192         total = isl_basic_map_total_dim(bmap);
 193         for (i = 0; i < extra; ++i) {
 194                 int k;
 195                 if ((k = isl_basic_map_alloc_div(bmap)) < 0)
 196                         goto error;
 197                 isl_seq_clr(bmap->div[k], 1+1+total);
 198         }
 199         if (!bmap)
 200                 return NULL;
 201         if (isl_stream_eat(s, ':'))
 202                 goto error;
 203         bmap = add_constraints(s, v, bmap);
 204         if (seen_paren && isl_stream_eat(s, ')'))
 205                 goto error;
 206         return bmap;
 207 error:
 208         isl_basic_map_free(bmap);
 209         return NULL;
 210 }
 211
 212 static struct isl_basic_map *add_constraint(struct isl_stream *s,
 213         struct vars **v, struct isl_basic_map *bmap)
 214 {
 215         unsigned total = isl_basic_map_total_dim(bmap);
 216         int k;
 217         int sign = 1;
 218         int equality = 0;
 219         int op = 0;
 220         struct isl_token *tok = NULL;
 221
 222         tok = isl_stream_next_token(s);
 223         if (!tok)
 224                 goto error;
 225         if (tok->type == ISL_TOKEN_EXISTS) {
 226                 isl_token_free(tok);
 227                 return add_exists(s, v, bmap);
 228         }
 229         isl_stream_push_token(s, tok);
 230
 231         bmap = isl_basic_map_cow(bmap);
 232         bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
 233         k = isl_basic_map_alloc_inequality(bmap);
 234         if (k < 0)
 235                 goto error;
 236         isl_seq_clr(bmap->ineq[k], 1+total);
 237
 238         for (;;) {
 239                 tok = isl_stream_next_token(s);
 240                 if (!tok) {
 241                         isl_stream_error(s, NULL, "unexpected EOF");
 242                         goto error;
 243                 }
 244                 if (tok->type == ISL_TOKEN_IDENT) {
 245                         int n = (*v)->n;
 246                         int pos = vars_pos(*v, tok->u.s, -1);
 247                         if (pos < 0)
 248                                 goto error;
 249                         if (pos >= n) {
 250                                 isl_stream_error(s, tok, "unknown identifier");
 251                                 goto error;
 252                         }
 253                         if (sign > 0)
 254                                 isl_int_add_ui(bmap->ineq[k][1+pos],
 255                                                 bmap->ineq[k][1+pos], 1);
 256                         else
 257                                 isl_int_sub_ui(bmap->ineq[k][1+pos],
 258                                                 bmap->ineq[k][1+pos], 1);
 259                 } else if (tok->type == ISL_TOKEN_VALUE) {
 260                         struct isl_token *tok2;
 261                         int n = (*v)->n;
 262                         int pos = -1;
 263                         tok2 = isl_stream_next_token(s);
 264                         if (tok2 && tok2->type == ISL_TOKEN_IDENT) {
 265                                 pos = vars_pos(*v, tok2->u.s, -1);
 266                                 if (pos < 0)
 267                                         goto error;
 268                                 if (pos >= n) {
 269                                         isl_stream_error(s, tok2,
 270                                                 "unknown identifier");
 271                                         isl_token_free(tok2);
 272                                         goto error;
 273                                 }
 274                                 isl_token_free(tok2);
 275                         } else if (tok2)
 276                                 isl_stream_push_token(s, tok2);
 277                         if (sign < 0)
 278                                 isl_int_neg(tok->u.v, tok->u.v);
 279                         isl_int_add(bmap->ineq[k][1+pos],
 280                                         bmap->ineq[k][1+pos], tok->u.v);
 281                 } else if (tok->type == '+') {
 282                         /* nothing */
 283                 } else if (tok->type == ISL_TOKEN_LE) {
 284                         op = 1;
 285                         isl_seq_neg(bmap->ineq[k], bmap->ineq[k], 1+total);
 286                 } else if (tok->type == ISL_TOKEN_GE) {
 287                         op = 1;
 288                         sign = -1;
 289                 } else if (tok->type == '=') {
 290                         if (op) {
 291                                 isl_stream_error(s, tok, "too many operators");
 292                                 goto error;
 293                         }
 294                         op = 1;
 295                         equality = 1;
 296                         sign = -1;
 297                 } else {
 298                         isl_stream_push_token(s, tok);
 299                         break;
 300                 }
 301                 isl_token_free(tok);
 302         }
 303         tok = NULL;
 304         if (!op) {
 305                 isl_stream_error(s, tok, "missing operator");
 306                 goto error;
 307         }
 308         if (equality)
 309                 isl_basic_map_inequality_to_equality(bmap, k);
 310         return bmap;
 311 error:
 312         if (tok)
 313                 isl_token_free(tok);
 314         isl_basic_map_free(bmap);
 315         return NULL;
 316 }
 317
 318 static struct isl_basic_map *add_constraints(struct isl_stream *s,
 319         struct vars **v, struct isl_basic_map *bmap)
 320 {
 321         struct isl_token *tok;
 322
 323         for (;;) {
 324                 bmap = add_constraint(s, v, bmap);
 325                 if (!bmap)
 326                         return NULL;
 327                 tok = isl_stream_next_token(s);
 328                 if (!tok) {
 329                         isl_stream_error(s, NULL, "unexpected EOF");
 330                         goto error;
 331                 }
 332                 if (tok->type != ISL_TOKEN_AND)
 333                         break;
 334                 isl_token_free(tok);
 335         }
 336         isl_stream_push_token(s, tok);
 337
 338         return bmap;
 339 error:
 340         if (tok)
 341                 isl_token_free(tok);
 342         isl_basic_map_free(bmap);
 343         return NULL;
 344 }
 345
 346 static __isl_give isl_basic_map *basic_map_read_polylib_constraint(
 347         struct isl_stream *s, __isl_take isl_basic_map *bmap)
 348 {
 349         int j;
 350         struct isl_token *tok;
 351         int type;
 352         int k;
 353         isl_int *c;
 354         unsigned nparam;
 355         unsigned dim;
 356
 357         if (!bmap)
 358                 return NULL;
 359
 360         nparam = isl_basic_map_dim(bmap, isl_dim_param);
 361         dim = isl_basic_map_dim(bmap, isl_dim_out);
 362
 363         tok = isl_stream_next_token(s);
 364         if (!tok || tok->type != ISL_TOKEN_VALUE) {
 365                 isl_stream_error(s, tok, "expecting coefficient");
 366                 if (tok)
 367                         isl_stream_push_token(s, tok);
 368                 goto error;
 369         }
 370         if (!tok->on_new_line) {
 371                 isl_stream_error(s, tok, "coefficient should appear on new line");
 372                 isl_stream_push_token(s, tok);
 373                 goto error;
 374         }
 375
 376         type = isl_int_get_si(tok->u.v);
 377         isl_token_free(tok);
 378
 379         isl_assert(s->ctx, type == 0 || type == 1, goto error);
 380         if (type == 0) {
 381                 k = isl_basic_map_alloc_equality(bmap);
 382                 c = bmap->eq[k];
 383         } else {
 384                 k = isl_basic_map_alloc_inequality(bmap);
 385                 c = bmap->ineq[k];
 386         }
 387         if (k < 0)
 388                 goto error;
 389
 390         for (j = 0; j < dim; ++j) {
 391                 tok = isl_stream_next_token(s);
 392                 if (!tok || tok->type != ISL_TOKEN_VALUE) {
 393                         isl_stream_error(s, tok, "expecting coefficient");
 394                         if (tok)
 395                                 isl_stream_push_token(s, tok);
 396                         goto error;
 397                 }
 398                 isl_int_set(c[1 + nparam + j], tok->u.v);
 399                 isl_token_free(tok);
 400         }
 401         for (j = 0; j < nparam; ++j) {
 402                 tok = isl_stream_next_token(s);
 403                 if (!tok || tok->type != ISL_TOKEN_VALUE) {
 404                         isl_stream_error(s, tok, "expecting coefficient");
 405                         if (tok)
 406                                 isl_stream_push_token(s, tok);
 407                         goto error;
 408                 }
 409                 isl_int_set(c[1 + j], tok->u.v);
 410                 isl_token_free(tok);
 411         }
 412         tok = isl_stream_next_token(s);
 413         if (!tok || tok->type != ISL_TOKEN_VALUE) {
 414                 isl_stream_error(s, tok, "expecting coefficient");
 415                 if (tok)
 416                         isl_stream_push_token(s, tok);
 417                 goto error;
 418         }
 419         isl_int_set(c[0], tok->u.v);
 420         isl_token_free(tok);
 421
 422         return bmap;
 423 error:
 424         isl_basic_map_free(bmap);
 425         return NULL;
 426 }
 427
 428 static __isl_give isl_basic_map *basic_map_read_polylib(struct isl_stream *s,
 429         int nparam)
 430 {
 431         int i;
 432         struct isl_token *tok;
 433         struct isl_token *tok2;
 434         int n_row, n_col;
 435         int on_new_line;
 436         unsigned dim;
 437         struct isl_basic_map *bmap = NULL;
 438
 439         if (nparam < 0)
 440                 nparam = 0;
 441
 442         tok = isl_stream_next_token(s);
 443         if (!tok) {
 444                 isl_stream_error(s, NULL, "unexpected EOF");
 445                 return NULL;
 446         }
 447         tok2 = isl_stream_next_token(s);
 448         if (!tok2) {
 449                 isl_token_free(tok);
 450                 isl_stream_error(s, NULL, "unexpected EOF");
 451                 return NULL;
 452         }
 453         n_row = isl_int_get_si(tok->u.v);
 454         n_col = isl_int_get_si(tok2->u.v);
 455         on_new_line = tok2->on_new_line;
 456         isl_token_free(tok2);
 457         isl_token_free(tok);
 458         isl_assert(s->ctx, !on_new_line, return NULL);
 459         isl_assert(s->ctx, n_row >= 0, return NULL);
 460         isl_assert(s->ctx, n_col >= 2 + nparam, return NULL);
 461         dim = n_col - 2 - nparam;
 462         bmap = isl_basic_map_alloc(s->ctx, nparam, 0, dim, 0, n_row, n_row);
 463         if (!bmap)
 464                 return NULL;
 465
 466         for (i = 0; i < n_row; ++i)
 467                 bmap = basic_map_read_polylib_constraint(s, bmap);
 468
 469         bmap = isl_basic_map_simplify(bmap);
 470         bmap = isl_basic_map_finalize(bmap);
 471         return bmap;
 472 }
 473
 474 static struct isl_map *map_read_polylib(struct isl_stream *s, int nparam)
 475 {
 476         struct isl_token *tok;
 477         struct isl_token *tok2;
 478         int i, n;
 479         struct isl_map *map;
 480
 481         tok = isl_stream_next_token(s);
 482         if (!tok) {
 483                 isl_stream_error(s, NULL, "unexpected EOF");
 484                 return NULL;
 485         }
 486         tok2 = isl_stream_next_token(s);
 487         if (!tok2) {
 488                 isl_token_free(tok);
 489                 isl_stream_error(s, NULL, "unexpected EOF");
 490                 return NULL;
 491         }
 492         if (!tok2->on_new_line) {
 493                 isl_stream_push_token(s, tok2);
 494                 isl_stream_push_token(s, tok);
 495                 return isl_map_from_basic_map(basic_map_read_polylib(s, nparam));
 496         }
 497         isl_stream_push_token(s, tok2);
 498         n = isl_int_get_si(tok->u.v);
 499         isl_token_free(tok);
 500
 501         isl_assert(s->ctx, n >= 1, return NULL);
 502
 503         map = isl_map_from_basic_map(basic_map_read_polylib(s, nparam));
 504
 505         for (i = 1; i < n; ++i)
 506                 map = isl_map_union(map,
 507                         isl_map_from_basic_map(basic_map_read_polylib(s, nparam)));
 508
 509         return map;
 510 }
 511
 512 static struct isl_map *map_read(struct isl_stream *s, int nparam)
 513 {
 514         struct isl_basic_map *bmap = NULL;
 515         struct isl_token *tok;
 516         struct vars *v = NULL;
 517         int n1;
 518         int n2;
 519
 520         tok = isl_stream_next_token(s);
 521         if (!tok) {
 522                 isl_stream_error(s, NULL, "unexpected EOF");
 523                 goto error;
 524         }
 525         if (tok->type == ISL_TOKEN_VALUE) {
 526                 isl_stream_push_token(s, tok);
 527                 return map_read_polylib(s, nparam);
 528         }
 529         if (tok->type != '{') {
 530                 isl_stream_error(s, tok, "expecting '{'");
 531                 if (tok)
 532                         isl_stream_push_token(s, tok);
 533                 goto error;
 534         }
 535         isl_token_free(tok);
 536         v = vars_new(s->ctx);
 537         v = read_tuple(s, v);
 538         if (!v)
 539                 return NULL;
 540         n1 = v->n;
 541         tok = isl_stream_next_token(s);
 542         if (tok && tok->type == ISL_TOKEN_TO) {
 543                 isl_token_free(tok);
 544                 v = read_tuple(s, v);
 545                 if (!v)
 546                         return NULL;
 547                 n2 = v->n - n1;
 548         } else {
 549                 if (tok)
 550                         isl_stream_push_token(s, tok);
 551                 n2 = n1;
 552                 n1 = 0;
 553         }
 554         bmap = isl_basic_map_alloc(s->ctx, 0, n1, n2, 0, 0,0);
 555         if (!bmap)
 556                 goto error;
 557         tok = isl_stream_next_token(s);
 558         if (tok && tok->type == ':') {
 559                 isl_token_free(tok);
 560                 bmap = add_constraints(s, &v, bmap);
 561                 tok = isl_stream_next_token(s);
 562         }
 563         if (tok && tok->type == '}') {
 564                 isl_token_free(tok);
 565         } else {
 566                 isl_stream_error(s, tok, "unexpected isl_token");
 567                 if (tok)
 568                         isl_token_free(tok);
 569                 goto error;
 570         }
 571         vars_free(v);
 572
 573         bmap = isl_basic_map_simplify(bmap);
 574         bmap = isl_basic_map_finalize(bmap);
 575         return isl_map_from_basic_map(bmap);
 576 error:
 577         isl_basic_map_free(bmap);
 578         if (v)
 579                 vars_free(v);
 580         return NULL;
 581 }
 582
 583 static struct isl_basic_map *basic_map_read(struct isl_stream *s, int nparam)
 584 {
 585         struct isl_map *map;
 586         struct isl_basic_map *bmap;
 587
 588         map = map_read(s, nparam);
 589         if (!map)
 590                 return NULL;
 591
 592         isl_assert(map->ctx, map->n <= 1, goto error);
 593
 594         if (map->n == 0)
 595                 bmap = isl_basic_map_empty_like_map(map);
 596         else
 597                 bmap = isl_basic_map_copy(map->p[0]);
 598
 599         isl_map_free(map);
 600
 601         return bmap;
 602 error:
 603         isl_map_free(map);
 604         return NULL;
 605 }
 606
 607 struct isl_basic_map *isl_basic_map_read_from_file_omega(
 608                 struct isl_ctx *ctx, FILE *input)
 609 {
 610         struct isl_basic_map *bmap;
 611         struct isl_stream *s = isl_stream_new_file(ctx, input);
 612         if (!s)
 613                 return NULL;
 614         bmap = basic_map_read(s, 0);
 615         isl_stream_free(s);
 616         return bmap;
 617 }
 618
 619 struct isl_basic_set *isl_basic_set_read_from_file_omega(
 620                 struct isl_ctx *ctx, FILE *input)
 621 {
 622         struct isl_basic_map *bmap;
 623         bmap = isl_basic_map_read_from_file_omega(ctx, input);
 624         if (!bmap)
 625                 return NULL;
 626         isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
 627         return (struct isl_basic_set *)bmap;
 628 error:
 629         isl_basic_map_free(bmap);
 630         return NULL;
 631 }
 632
 633 struct isl_basic_map *isl_basic_map_read_from_str_omega(
 634                 struct isl_ctx *ctx, const char *str)
 635 {
 636         struct isl_basic_map *bmap;
 637         struct isl_stream *s = isl_stream_new_str(ctx, str);
 638         if (!s)
 639                 return NULL;
 640         bmap = basic_map_read(s, 0);
 641         isl_stream_free(s);
 642         return bmap;
 643 }
 644
 645 struct isl_basic_set *isl_basic_set_read_from_str_omega(
 646                 struct isl_ctx *ctx, const char *str)
 647 {
 648         struct isl_basic_map *bmap;
 649         bmap = isl_basic_map_read_from_str_omega(ctx, str);
 650         if (!bmap)
 651                 return NULL;
 652         isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
 653         return (struct isl_basic_set *)bmap;
 654 error:
 655         isl_basic_map_free(bmap);
 656         return NULL;
 657 }