?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
isl_map_read: forget existentially quantified variables after each disjunct
[isl.git] / isl_input.c
blob1f48d0196eaaecc06d2393bb26333421da4e702f
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 }
Integer set library