evalue_read.c

   1 #include <barvinok/util.h>
   2 #include "evalue_read.h"
   3
   4 #define ALLOC(type) (type*)malloc(sizeof(type))
   5 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
   6
   7 enum token_type { TOKEN_UNKNOWN = 256, TOKEN_VALUE, TOKEN_IDENT, TOKEN_GE,
   8                   TOKEN_NE, TOKEN_UNION, TOKEN_VARS };
   9
  10 struct token {
  11     enum token_type  type;
  12
  13     int line;
  14     int col;
  15
  16     union {
  17         Value   v;
  18         char    *s;
  19     } u;
  20 };
  21
  22 static struct token *token_new(int line, int col)
  23 {
  24     struct token *tok = ALLOC(struct token);
  25     tok->line = line;
  26     tok->col = col;
  27     return tok;
  28 }
  29
  30 void token_free(struct token *tok)
  31 {
  32     if (tok->type == TOKEN_VALUE)
  33         value_clear(tok->u.v);
  34     else if (tok->type == TOKEN_IDENT)
  35         free(tok->u.s);
  36     free(tok);
  37 }
  38
  39 struct stream {
  40     FILE            *file;
  41     const char      *str;
  42     int             line;
  43     int             col;
  44     int             eof;
  45
  46     char            *buffer;
  47     size_t          size;
  48     size_t          len;
  49     int             c;
  50
  51     struct token    *tokens[5];
  52     int             n_token;
  53 };
  54
  55 static struct stream* stream_new()
  56 {
  57     int i;
  58     struct stream *s = ALLOC(struct stream);
  59     s->size = 256;
  60     s->file = NULL;
  61     s->str = NULL;
  62     s->buffer = (char*)malloc(s->size);
  63     s->len = 0;
  64     s->line = 1;
  65     s->col = 0;
  66     s->eof = 0;
  67     s->c = -1;
  68     for (i = 0; i < 5; ++i)
  69         s->tokens[i] = NULL;
  70     s->n_token = 0;
  71     return s;
  72 }
  73
  74 static struct stream* stream_new_file(FILE *file)
  75 {
  76     struct stream *s = stream_new();
  77     s->file = file;
  78     return s;
  79 }
  80
  81 static struct stream* stream_new_str(const char *str)
  82 {
  83     struct stream *s = stream_new();
  84     s->str = str;
  85     return s;
  86 }
  87
  88 static int stream_getc(struct stream *s)
  89 {
  90     int c;
  91     if (s->eof)
  92         return -1;
  93     if (s->file)
  94         c = fgetc(s->file);
  95     else {
  96         c = *s->str++;
  97         if (c == '\0')
  98             c = -1;
  99     }
 100     if (c == -1)
 101         s->eof = 1;
 102     if (!s->eof) {
 103         if (s->c == '\n') {
 104             s->line++;
 105             s->col = 0;
 106         } else
 107             s->col++;
 108     }
 109     s->c = c;
 110     return c;
 111 }
 112
 113 static void stream_ungetc(struct stream *s, int c)
 114 {
 115     if (s->file)
 116         ungetc(c, s->file);
 117     else
 118         --s->str;
 119     s->c = -1;
 120 }
 121
 122 static void stream_push_char(struct stream *s, int c)
 123 {
 124     if (s->len >= s->size) {
 125         s->size = (3*s->size)/2;
 126         s->buffer = (char*)realloc(s->buffer, s->size);
 127     }
 128     s->buffer[s->len++] = c;
 129 }
 130
 131 static struct token *stream_push_token(struct stream *s, struct token *tok)
 132 {
 133     assert(s->n_token < 5);
 134     s->tokens[s->n_token++] = tok;
 135 }
 136
 137 static struct token *stream_next_token(struct stream *s)
 138 {
 139     int c;
 140     struct token *tok;
 141     int line, col;
 142
 143     if (s->n_token)
 144         return s->tokens[--s->n_token];
 145
 146     s->len = 0;
 147
 148     /* skip spaces */
 149     while ((c = stream_getc(s)) != -1 && isspace(c))
 150         /* nothing */
 151         ;
 152
 153     line = s->line;
 154     col = s->col;
 155
 156     if (c == -1)
 157         return NULL;
 158     if (c == '(' ||
 159         c == ')' ||
 160         c == '+' ||
 161         c == '/' ||
 162         c == '*' ||
 163         c == '^' ||
 164         c == '=' ||
 165         c == ',' ||
 166         c == '_' ||
 167         c == '[' ||
 168         c == ']' ||
 169         c == '{' ||
 170         c == '}') {
 171         tok = token_new(line, col);
 172         tok->type = (enum token_type)c;
 173         return tok;
 174     }
 175     if (c == '-' || isdigit(c)) {
 176         tok = token_new(line, col);
 177         tok->type = TOKEN_VALUE;
 178         value_init(tok->u.v);
 179         stream_push_char(s, c);
 180         while ((c = stream_getc(s)) != -1 && isdigit(c))
 181             stream_push_char(s, c);
 182         if (c != -1)
 183             stream_ungetc(s, c);
 184         if (s->len == 1 && s->buffer[0] == '-')
 185             value_set_si(tok->u.v, -1);
 186         else {
 187             stream_push_char(s, '\0');
 188             mpz_set_str(tok->u.v, s->buffer, 0);
 189         }
 190         return tok;
 191     }
 192     if (c == '#' || isalpha(c)) {
 193         tok = token_new(line, col);
 194         stream_push_char(s, c);
 195         while ((c = stream_getc(s)) != -1 && isalnum(c))
 196             stream_push_char(s, c);
 197         if (c != -1)
 198             stream_ungetc(s, c);
 199         stream_push_char(s, '\0');
 200         if (!strcmp(s->buffer, "#variables")) {
 201             tok->type = TOKEN_VARS;
 202         } else if (s->buffer[0] == '#') {
 203             tok->type = TOKEN_UNKNOWN;
 204         } else if (!strcmp(s->buffer, "UNION")) {
 205             tok->type = TOKEN_UNION;
 206         } else {
 207             tok->type = TOKEN_IDENT;
 208             tok->u.s = strdup(s->buffer);
 209         }
 210         return tok;
 211     }
 212     if (c == '>') {
 213         if ((c = stream_getc(s)) == '=') {
 214             tok = token_new(line, col);
 215             tok->type = TOKEN_GE;
 216             return tok;
 217         }
 218         if (c != -1)
 219             stream_ungetc(s, c);
 220     }
 221     if (c == '!') {
 222         if ((c = stream_getc(s)) == '=') {
 223             tok = token_new(line, col);
 224             tok->type = TOKEN_NE;
 225             return tok;
 226         }
 227         if (c != -1)
 228             stream_ungetc(s, c);
 229     }
 230
 231     tok = token_new(line, col);
 232     tok->type = TOKEN_UNKNOWN;
 233     return tok;
 234 }
 235
 236 void stream_error(struct stream *s, struct token *tok, char *msg)
 237 {
 238     int line = tok ? tok->line : s->line;
 239     int col = tok ? tok->col : s->col;
 240     fprintf(stderr, "syntax error (%d, %d): %s\n", line, col, msg);
 241     if (tok) {
 242         if (tok->type < 256)
 243             fprintf(stderr, "got '%c'\n", tok->type);
 244         else
 245             fprintf(stderr, "got token type %d\n", tok->type);
 246     }
 247 }
 248
 249 static void stream_free(struct stream *s)
 250 {
 251     free(s->buffer);
 252     if (s->n_token != 0) {
 253         struct token *tok = stream_next_token(s);
 254         stream_error(s, tok, "unexpected token");
 255     }
 256     free(s);
 257 }
 258
 259 struct parameter {
 260     char                *name;
 261     int                  pos;
 262     struct parameter    *next;
 263 };
 264
 265 struct parameter *parameter_new(const char *name, int pos, struct parameter *next)
 266 {
 267     struct parameter *p = ALLOC(struct parameter);
 268     p->name = strdup(name);
 269     p->pos = pos;
 270     p->next = next;
 271     return p;
 272 }
 273
 274 static int parameter_pos(struct parameter **p, const char *s, int len)
 275 {
 276     int pos = *p ? (*p)->pos+1 : 0;
 277     struct parameter *q;
 278
 279     if (len == -1)
 280         len = strlen(s);
 281     for (q = *p; q; q = q->next) {
 282         if (strncmp(q->name, s, len) == 0)
 283             break;
 284     }
 285     if (q)
 286         pos = q->pos;
 287     else
 288         *p = parameter_new(s, pos, *p);
 289     return pos;
 290 }
 291
 292 static int optional_power(struct stream *s)
 293 {
 294     int pow;
 295     struct token *tok;
 296     tok = stream_next_token(s);
 297     if (!tok)
 298         return 1;
 299     if (tok->type != '^') {
 300         stream_push_token(s, tok);
 301         return 1;
 302     }
 303     token_free(tok);
 304     tok = stream_next_token(s);
 305     if (!tok || tok->type != TOKEN_VALUE) {
 306         stream_error(s, tok, "expecting exponent");
 307         if (tok)
 308             stream_push_token(s, tok);
 309         return 1;
 310     }
 311     pow = VALUE_TO_INT(tok->u.v);
 312     token_free(tok);
 313     return pow;
 314 }
 315
 316 static evalue *evalue_read_factor(struct stream *s, struct parameter **p);
 317 static evalue *evalue_read_term(struct stream *s, struct parameter **p);
 318
 319 static evalue *create_fract_like(struct stream *s, evalue *arg, enode_type type,
 320                                  struct parameter **p)
 321 {
 322     evalue *e;
 323     int pow;
 324     pow = optional_power(s);
 325
 326     e = ALLOC(evalue);
 327     value_init(e->d);
 328     e->x.p = new_enode(type, pow+2, -1);
 329     value_clear(e->x.p->arr[0].d);
 330     e->x.p->arr[0] = *arg;
 331     free(arg);
 332     evalue_set_si(&e->x.p->arr[1+pow], 1, 1);
 333     while (--pow >= 0)
 334         evalue_set_si(&e->x.p->arr[1+pow], 0, 1);
 335
 336     return e;
 337 }
 338
 339 static evalue *create_relation(evalue *arg, int ne)
 340 {
 341     evalue *e;
 342
 343     e = ALLOC(evalue);
 344     value_init(e->d);
 345     e->x.p = new_enode(relation, 2+ne, 0);
 346     value_clear(e->x.p->arr[0].d);
 347     e->x.p->arr[0] = *arg;
 348     free(arg);
 349     if (ne)
 350         evalue_set_si(&e->x.p->arr[1], 0, 1);
 351     evalue_set_si(&e->x.p->arr[1+ne], 1, 1);
 352
 353     return e;
 354 }
 355
 356 static evalue *read_fract(struct stream *s, struct token *tok, struct parameter **p)
 357 {
 358     evalue *arg;
 359
 360     tok = stream_next_token(s);
 361     assert(tok);
 362     assert(tok->type == '{');
 363
 364     token_free(tok);
 365     arg = evalue_read_term(s, p);
 366     tok = stream_next_token(s);
 367     if (!tok || tok->type != '}') {
 368         stream_error(s, tok, "expecting \"}\"");
 369         if (tok)
 370             stream_push_token(s, tok);
 371     } else
 372         token_free(tok);
 373
 374     return create_fract_like(s, arg, fractional, p);
 375 }
 376
 377 static evalue *read_periodic(struct stream *s, struct parameter **p)
 378 {
 379     evalue **list;
 380     int len;
 381     int n;
 382     evalue *e = NULL;
 383
 384     struct token *tok;
 385     tok = stream_next_token(s);
 386     assert(tok && tok->type == '[');
 387     token_free(tok);
 388
 389     len = 100;
 390     list = (evalue **)malloc(len * sizeof(evalue *));
 391     n = 0;
 392
 393     for (;;) {
 394         evalue *e = evalue_read_term(s, p);
 395         if (!e) {
 396             stream_error(s, NULL, "missing argument or list element");
 397             goto out;
 398         }
 399         if (n >= len) {
 400             len = (3*len)/2;
 401             list = (evalue **)realloc(list, len * sizeof(evalue *));
 402         }
 403         list[n++] = e;
 404
 405         tok = stream_next_token(s);
 406         if (!tok) {
 407             stream_error(s, NULL, "unexpected EOF");
 408             goto out;
 409         }
 410         if (tok->type != ',')
 411             break;
 412         token_free(tok);
 413     }
 414
 415     if (n == 1 && (tok->type == '=' || tok->type == TOKEN_NE)) {
 416         int ne = tok->type == TOKEN_NE;
 417         token_free(tok);
 418         tok = stream_next_token(s);
 419         if (!tok || tok->type != TOKEN_VALUE) {
 420             stream_error(s, tok, "expecting \"0\"");
 421             if (tok)
 422                 stream_push_token(s, tok);
 423             goto out;
 424         }
 425         token_free(tok);
 426         tok = stream_next_token(s);
 427         if (!tok || tok->type != ']') {
 428             stream_error(s, tok, "expecting \"]\"");
 429             if (tok)
 430                 stream_push_token(s, tok);
 431             goto out;
 432         }
 433         token_free(tok);
 434         e = create_relation(list[0], ne);
 435         n = 0;
 436         goto out;
 437     }
 438
 439     if (tok->type != ']') {
 440         stream_error(s, tok, "expecting \"]\"");
 441         stream_push_token(s, tok);
 442         goto out;
 443     }
 444
 445     token_free(tok);
 446
 447     tok = stream_next_token(s);
 448     if (tok && tok->type == '_') {
 449         int pos;
 450         token_free(tok);
 451         tok = stream_next_token(s);
 452         if (!tok || tok->type != TOKEN_IDENT) {
 453             stream_error(s, tok, "expecting identifier");
 454             if (tok)
 455                 stream_push_token(s, tok);
 456             goto out;
 457         }
 458         e = ALLOC(evalue);
 459         value_init(e->d);
 460         pos = parameter_pos(p, tok->u.s, -1);
 461         token_free(tok);
 462         e->x.p = new_enode(periodic, n, pos+1);
 463         while (--n >= 0) {
 464             value_clear(e->x.p->arr[n].d);
 465             e->x.p->arr[n] = *list[n];
 466             free(list[n]);
 467         }
 468     } else if (n == 1) {
 469         if (tok)
 470             stream_push_token(s, tok);
 471         e = create_fract_like(s, list[0], flooring, p);
 472         n = 0;
 473     } else {
 474         stream_error(s, tok, "unexpected token");
 475         if (tok)
 476             stream_push_token(s, tok);
 477     }
 478
 479 out:
 480     while (--n >= 0)
 481         evalue_free(list[n]);
 482     free(list);
 483     return e;
 484 }
 485
 486 /* frees product on error */
 487 static evalue *read_factor_and_multiply(struct stream *s, struct parameter **p,
 488                                         evalue *product)
 489 {
 490     evalue *e2;
 491     e2 = evalue_read_factor(s, p);
 492     if (!e2) {
 493         stream_error(s, NULL, "unexpected EOF");
 494         evalue_free(product);
 495         return NULL;
 496     }
 497     emul(e2, product);
 498     evalue_free(e2);
 499     return product;
 500 }
 501
 502 static evalue *evalue_read_factor(struct stream *s, struct parameter **p)
 503 {
 504     struct token *tok;
 505     evalue *e = NULL;
 506
 507     tok = stream_next_token(s);
 508     if (!tok)
 509         return NULL;
 510
 511     if (tok->type == '(') {
 512         token_free(tok);
 513         e = evalue_read_term(s, p);
 514         tok = stream_next_token(s);
 515         if (!tok || tok->type != ')') {
 516             stream_error(s, tok, "expecting \")\"");
 517             if (tok)
 518                 stream_push_token(s, tok);
 519         } else
 520             token_free(tok);
 521     } else if (tok->type == TOKEN_VALUE) {
 522         e = ALLOC(evalue);
 523         value_init(e->d);
 524         value_set_si(e->d, 1);
 525         value_init(e->x.n);
 526         value_assign(e->x.n, tok->u.v);
 527         token_free(tok);
 528         tok = stream_next_token(s);
 529         if (tok && tok->type == '/') {
 530             token_free(tok);
 531             tok = stream_next_token(s);
 532             if (!tok || tok->type != TOKEN_VALUE) {
 533                 stream_error(s, tok, "expecting denominator");
 534                 if (tok)
 535                     stream_push_token(s, tok);
 536                 return NULL;
 537             }
 538             value_assign(e->d, tok->u.v);
 539             token_free(tok);
 540         } else if (tok && tok->type == TOKEN_IDENT) {
 541             stream_push_token(s, tok);
 542             e = read_factor_and_multiply(s, p, e);
 543         } else if (tok)
 544             stream_push_token(s, tok);
 545     } else if (tok->type == TOKEN_IDENT) {
 546         int pos = parameter_pos(p, tok->u.s, -1);
 547         int pow = optional_power(s);
 548         token_free(tok);
 549         e = ALLOC(evalue);
 550         value_init(e->d);
 551         e->x.p = new_enode(polynomial, pow+1, pos+1);
 552         evalue_set_si(&e->x.p->arr[pow], 1, 1);
 553         while (--pow >= 0)
 554             evalue_set_si(&e->x.p->arr[pow], 0, 1);
 555     } else if (tok->type == '[') {
 556         stream_push_token(s, tok);
 557         e = read_periodic(s, p);
 558     } else if (tok->type == '{') {
 559         stream_push_token(s, tok);
 560         e = read_fract(s, tok, p);
 561     }
 562
 563     tok = stream_next_token(s);
 564     if (tok && tok->type == '*') {
 565         token_free(tok);
 566         e = read_factor_and_multiply(s, p, e);
 567     } else if (tok)
 568         stream_push_token(s, tok);
 569
 570     return e;
 571 }
 572
 573 static evalue *evalue_read_term(struct stream *s, struct parameter **p)
 574 {
 575     struct token *tok;
 576     evalue *e = NULL;
 577
 578     e = evalue_read_factor(s, p);
 579     if (!e)
 580         return NULL;
 581
 582     tok = stream_next_token(s);
 583     if (!tok)
 584         return e;
 585
 586     if (tok->type == '+' || tok->type == TOKEN_VALUE) {
 587         evalue *e2;
 588         if (tok->type == '+')
 589             token_free(tok);
 590         else
 591             stream_push_token(s, tok);
 592         e2 = evalue_read_term(s, p);
 593         if (!e2) {
 594             stream_error(s, NULL, "unexpected EOF");
 595             return NULL;
 596         }
 597         eadd(e2, e);
 598         evalue_free(e2);
 599     } else
 600         stream_push_token(s, tok);
 601
 602     return e;
 603 }
 604
 605 struct constraint {
 606     int                  type;
 607     Vector              *v;
 608     struct constraint   *next;
 609     struct constraint   *union_next;
 610 };
 611
 612 static struct constraint *constraint_new()
 613 {
 614     struct constraint *c = ALLOC(struct constraint);
 615     c->type = -1;
 616     c->v = Vector_Alloc(16);
 617     c->next = NULL;
 618     c->union_next = NULL;
 619     return c;
 620 }
 621
 622 static void constraint_free(struct constraint *c)
 623 {
 624     while (c) {
 625         struct constraint *next = c->next ? c->next : c->union_next;
 626         Vector_Free(c->v);
 627         free(c);
 628         c = next;
 629     }
 630 }
 631
 632 static void constraint_extend(struct constraint *c, int pos)
 633 {
 634     Vector *v;
 635     if (pos < c->v->Size)
 636         return;
 637
 638     v = Vector_Alloc((3*c->v->Size)/2);
 639     Vector_Copy(c->v->p, v->p, c->v->Size);
 640     Vector_Free(c->v);
 641     c->v = v;
 642 }
 643
 644 static int evalue_read_constraint(struct stream *s, struct parameter **p,
 645                                   struct constraint **constraints,
 646                                   struct constraint *union_next)
 647 {
 648     struct token *tok;
 649     struct constraint *c = NULL;
 650
 651     while ((tok = stream_next_token(s))) {
 652         struct token *tok2;
 653         int pos;
 654         if (tok->type == '+')
 655             token_free(tok);
 656         else if (tok->type == TOKEN_IDENT) {
 657             if (!c)
 658                 c = constraint_new();
 659             pos = parameter_pos(p, tok->u.s, -1);
 660             constraint_extend(c, 1+pos);
 661             value_set_si(c->v->p[1+pos], 1);
 662             token_free(tok);
 663         } else if (tok->type == TOKEN_VALUE) {
 664             if (!c)
 665                 c = constraint_new();
 666             tok2 = stream_next_token(s);
 667             if (tok2 && tok2->type == TOKEN_IDENT) {
 668                 pos = parameter_pos(p, tok2->u.s, -1);
 669                 constraint_extend(c, 1+pos);
 670                 value_assign(c->v->p[1+pos], tok->u.v);
 671                 token_free(tok);
 672                 token_free(tok2);
 673             } else {
 674                 if (tok2)
 675                     stream_push_token(s, tok2);
 676                 value_assign(c->v->p[0], tok->u.v);
 677                 token_free(tok);
 678             }
 679         } else if (tok->type == TOKEN_GE || tok->type == '=') {
 680             int type = tok->type == TOKEN_GE;
 681             token_free(tok);
 682             tok = stream_next_token(s);
 683             if (!tok || tok->type != TOKEN_VALUE || value_notzero_p(tok->u.v)) {
 684                 stream_error(s, tok, "expecting \"0\"");
 685                 if (tok)
 686                     stream_push_token(s, tok);
 687                 *constraints = NULL;
 688             } else {
 689                 c->type = type;
 690                 c->next = *constraints;
 691                 c->union_next = union_next;
 692                 *constraints = c;
 693                 token_free(tok);
 694             }
 695             break;
 696         } else {
 697             if (!c)
 698                 stream_push_token(s, tok);
 699             else {
 700                 stream_error(s, tok, "unexpected token");
 701                 *constraints = NULL;
 702             }
 703             return 0;
 704         }
 705     }
 706     return tok != NULL;
 707 }
 708
 709 static struct constraint *evalue_read_domain(struct stream *s, struct parameter **p,
 710                                              unsigned MaxRays)
 711 {
 712     struct constraint *constraints = NULL;
 713     struct constraint *union_next = NULL;
 714     struct token *tok;
 715     int line;
 716
 717     tok = stream_next_token(s);
 718     if (!tok)
 719         return NULL;
 720     stream_push_token(s, tok);
 721
 722     line = tok->line;
 723     while (evalue_read_constraint(s, p, &constraints, union_next)) {
 724         tok = stream_next_token(s);
 725         if (tok) {
 726             if (tok->type == TOKEN_UNION) {
 727                 token_free(tok);
 728                 tok = stream_next_token(s);
 729                 if (!tok) {
 730                     stream_error(s, NULL, "unexpected EOF");
 731                     return constraints;
 732                 }
 733                 stream_push_token(s, tok);
 734                 union_next = constraints;
 735                 constraints = NULL;
 736             } else {
 737                 union_next = NULL;
 738                 stream_push_token(s, tok);
 739                 /* empty line separates domain from evalue */
 740                 if (tok->line > line+1)
 741                     break;
 742             }
 743             line = tok->line;
 744         }
 745     }
 746     return constraints;
 747 }
 748
 749 struct section {
 750     struct constraint   *constraints;
 751     evalue              *e;
 752     struct section      *next;
 753 };
 754
 755 static char **extract_parameters(struct parameter *p, unsigned *nparam)
 756 {
 757     int i;
 758     char **params;
 759
 760     *nparam = p ? p->pos+1 : 0;
 761     params = ALLOCN(char *, *nparam);
 762     for (i = 0; i < *nparam; ++i) {
 763         struct parameter *next = p->next;
 764         params[p->pos] = p->name;
 765         free(p);
 766         p = next;
 767     }
 768     return params;
 769 }
 770
 771 static Polyhedron *constraints2domain(struct constraint *constraints,
 772                                       unsigned nparam, unsigned MaxRays)
 773 {
 774     Polyhedron *D;
 775     Matrix *M;
 776     int n;
 777     struct constraint *c;
 778     struct constraint *union_next = NULL;
 779
 780     for (n = 0, c = constraints; c; ++n, c = c->next)
 781         ;
 782     M = Matrix_Alloc(n, 1+nparam+1);
 783     while (--n >= 0) {
 784         struct constraint *next = constraints->next;
 785         union_next = constraints->union_next;
 786         Vector_Copy(constraints->v->p+1, M->p[n]+1, nparam);
 787         if (constraints->type)
 788             value_set_si(M->p[n][0], 1);
 789         value_assign(M->p[n][1+nparam], constraints->v->p[0]);
 790         constraints->next = NULL;
 791         constraints->union_next = NULL;
 792         constraint_free(constraints);
 793         constraints = next;
 794     }
 795     D = Constraints2Polyhedron(M, MaxRays);
 796     Matrix_Free(M);
 797
 798     if (union_next)
 799         D = DomainConcat(D, constraints2domain(union_next, nparam, MaxRays));
 800     return D;
 801 }
 802
 803 static evalue *evalue_read_partition(struct stream *s, struct parameter *p,
 804                                      char ***ppp,
 805                                      unsigned *nparam, unsigned MaxRays)
 806 {
 807     struct section *part = NULL;
 808     struct constraint *constraints;
 809     evalue *e = NULL;
 810     int m = 0;
 811
 812     while ((constraints = evalue_read_domain(s, &p, MaxRays))) {
 813         struct section *sect;
 814         evalue *e = evalue_read_term(s, &p);
 815         if (!e) {
 816             stream_error(s, NULL, "missing evalue");
 817             break;
 818         }
 819         sect = ALLOC(struct section);
 820         sect->constraints = constraints;
 821         sect->e = e;
 822         sect->next = part;
 823         part = sect;
 824         ++m;
 825     }
 826
 827     if (part) {
 828         Polyhedron *D;
 829         int j;
 830
 831         *ppp = extract_parameters(p, nparam);
 832         e = ALLOC(evalue);
 833         value_init(e->d);
 834         e->x.p = new_enode(partition, 2*m, *nparam);
 835
 836         for (j = 0; j < m; ++j) {
 837             int n;
 838             struct section *next = part->next;
 839             constraints = part->constraints;
 840             D = constraints2domain(part->constraints, *nparam, MaxRays);
 841             EVALUE_SET_DOMAIN(e->x.p->arr[2*j], D);
 842             value_clear(e->x.p->arr[2*j+1].d);
 843             e->x.p->arr[2*j+1] = *part->e;
 844             free(part->e);
 845             free(part);
 846             part = next;
 847         }
 848     }
 849     return e;
 850 }
 851
 852 static evalue *evalue_read(struct stream *s, const char *var_list, char ***ppp,
 853                            unsigned *nvar, unsigned *nparam, unsigned MaxRays)
 854 {
 855     struct token *tok;
 856     evalue *e;
 857     struct parameter *p = NULL;
 858     char *next;
 859     int nv;
 860
 861     if (var_list) {
 862         while ((next = strchr(var_list, ','))) {
 863             if (next > var_list)
 864                 parameter_pos(&p, var_list, next-var_list);
 865             var_list = next+1;
 866         }
 867         if (strlen(var_list) > 0)
 868             parameter_pos(&p, var_list, -1);
 869         nv = p ? p->pos+1 : 0;
 870     } else
 871         nv = -1;
 872
 873     if (!(tok = stream_next_token(s)))
 874         return NULL;
 875
 876     if (tok->type == TOKEN_VARS) {
 877         token_free(tok);
 878         for (;;) {
 879             tok = stream_next_token(s);
 880             if (!tok || tok->type != TOKEN_IDENT) {
 881                 stream_error(s, tok, "expecting identifier");
 882                 break;
 883             }
 884             if (nv == -1)
 885                 parameter_pos(&p, tok->u.s, -1);
 886             token_free(tok);
 887             tok = stream_next_token(s);
 888             if (!tok || tok->type != ',')
 889                 break;
 890             token_free(tok);
 891         }
 892         if (!tok)
 893             return NULL;
 894         if (nv = -1)
 895             nv = p ? p->pos+1 : 0;
 896     }
 897
 898     if (tok->type == '(') {
 899         stream_push_token(s, tok);
 900         e = evalue_read_term(s, &p);
 901         *ppp = extract_parameters(p, nparam);
 902     } else if (tok->type == TOKEN_VALUE) {
 903         struct token *tok2 = stream_next_token(s);
 904         if (tok2)
 905             stream_push_token(s, tok2);
 906         stream_push_token(s, tok);
 907         if (tok2 && (tok2->type == TOKEN_IDENT || tok2->type == TOKEN_GE))
 908             e = evalue_read_partition(s, p, ppp, nparam, MaxRays);
 909         else {
 910             e = evalue_read_term(s, &p);
 911             *ppp = extract_parameters(p, nparam);
 912         }
 913     } else if (tok->type == TOKEN_IDENT) {
 914         stream_push_token(s, tok);
 915         e = evalue_read_partition(s, p, ppp, nparam, MaxRays);
 916     } else {
 917         stream_error(s, tok, "unexpected token");
 918         *nparam = nv == -1 ? 0 : nv;
 919         e = NULL;
 920     }
 921     if (nv == -1)
 922         *nvar = *nparam;
 923     else
 924         *nvar = nv;
 925     *nparam -= *nvar;
 926     return e;
 927 }
 928
 929 evalue *evalue_read_from_file(FILE *in, const char *var_list, char ***ppp,
 930                               unsigned *nvar, unsigned *nparam, unsigned MaxRays)
 931 {
 932     evalue *e;
 933     struct stream *s = stream_new_file(in);
 934     e = evalue_read(s, var_list, ppp, nvar, nparam, MaxRays);
 935     stream_free(s);
 936     return e;
 937 }
 938
 939 evalue *evalue_read_from_str(const char *str, const char *var_list, char ***ppp,
 940                              unsigned *nvar, unsigned *nparam, unsigned MaxRays)
 941 {
 942     evalue *e;
 943     struct stream *s = stream_new_str(str);
 944     e = evalue_read(s, var_list, ppp, nvar, nparam, MaxRays);
 945     stream_free(s);
 946     return e;
 947 }