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