isl_input_omega.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  *
   4  * Use of this software is governed by the GNU LGPLv2.1 license
   5  *
   6  * Written by Sven Verdoolaege, K.U.Leuven, Departement
   7  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
   8  */
   9
  10 #include <ctype.h>
  11 #include <string.h>
  12 #include <strings.h>
  13 #include <isl_seq.h>
  14 #include "isl_stream.h"
  15 #include "isl_map_private.h"
  16 #include "isl_input_omega.h"
  17
  18 struct variable {
  19         char                    *name;
  20         int                      pos;
  21         struct variable         *next;
  22 };
  23
  24 struct vars {
  25         struct isl_ctx  *ctx;
  26         int              n;
  27         struct variable *v;
  28 };
  29
  30 static struct vars *vars_new(struct isl_ctx *ctx)
  31 {
  32         struct vars *v;
  33         v = isl_alloc_type(ctx, struct vars);
  34         if (!v)
  35                 return NULL;
  36         v->ctx = ctx;
  37         v->n = 0;
  38         v->v = NULL;
  39         return v;
  40 }
  41
  42 static void variable_free(struct variable *var)
  43 {
  44         while (var) {
  45                 struct variable *next = var->next;
  46                 free(var->name);
  47                 free(var);
  48                 var = next;
  49         }
  50 }
  51
  52 static void vars_free(struct vars *v)
  53 {
  54         if (!v)
  55                 return;
  56         variable_free(v->v);
  57         free(v);
  58 }
  59
  60 static struct variable *variable_new(struct vars *v, const char *name, int len,
  61                                 int pos)
  62 {
  63         struct variable *var;
  64         var = isl_alloc_type(v->ctx, struct variable);
  65         if (!var)
  66                 goto error;
  67         var->name = strdup(name);
  68         var->name[len] = '\0';
  69         var->pos = pos;
  70         var->next = v->v;
  71         return var;
  72 error:
  73         variable_free(v->v);
  74         return NULL;
  75 }
  76
  77 static int vars_pos(struct vars *v, const char *s, int len)
  78 {
  79         int pos;
  80         struct variable *q;
  81
  82         if (len == -1)
  83                 len = strlen(s);
  84         for (q = v->v; q; q = q->next) {
  85                 if (strncmp(q->name, s, len) == 0 && q->name[len] == '\0')
  86                         break;
  87         }
  88         if (q)
  89                 pos = q->pos;
  90         else {
  91                 pos = v->n;
  92                 v->v = variable_new(v, s, len, v->n);
  93                 if (!v->v)
  94                         return -1;
  95                 v->n++;
  96         }
  97         return pos;
  98 }
  99
 100 static struct vars *read_var_list(struct isl_stream *s, struct vars *v)
 101 {
 102         struct isl_token *tok;
 103
 104         while ((tok = isl_stream_next_token(s)) != NULL) {
 105                 int p;
 106                 int n = v->n;
 107
 108                 if (tok->type != ISL_TOKEN_IDENT)
 109                         break;
 110
 111                 p = vars_pos(v, tok->u.s, -1);
 112                 if (p < 0)
 113                         goto error;
 114                 if (p < n) {
 115                         isl_stream_error(s, tok, "expecting unique identifier");
 116                         goto error;
 117                 }
 118                 isl_token_free(tok);
 119                 tok = isl_stream_next_token(s);
 120                 if (!tok || tok->type != ',')
 121                         break;
 122
 123                 isl_token_free(tok);
 124         }
 125         if (tok)
 126                 isl_stream_push_token(s, tok);
 127
 128         return v;
 129 error:
 130         isl_token_free(tok);
 131         vars_free(v);
 132         return NULL;
 133 }
 134
 135 static struct vars *read_tuple(struct isl_stream *s, struct vars *v)
 136 {
 137         struct isl_token *tok;
 138
 139         tok = isl_stream_next_token(s);
 140         if (!tok || tok->type != '[') {
 141                 isl_stream_error(s, tok, "expecting '['");
 142                 goto error;
 143         }
 144         isl_token_free(tok);
 145         v = read_var_list(s, v);
 146         tok = isl_stream_next_token(s);
 147         if (!tok || tok->type != ']') {
 148                 isl_stream_error(s, tok, "expecting ']'");
 149                 goto error;
 150         }
 151         isl_token_free(tok);
 152
 153         return v;
 154 error:
 155         if (tok)
 156                 isl_token_free(tok);
 157         vars_free(v);
 158         return NULL;
 159 }
 160
 161 static struct isl_basic_map *add_constraints(struct isl_stream *s,
 162         struct vars **v, struct isl_basic_map *bmap);
 163
 164 static struct isl_basic_map *add_exists(struct isl_stream *s,
 165         struct vars **v, struct isl_basic_map *bmap)
 166 {
 167         struct isl_token *tok;
 168         int n = (*v)->n;
 169         int extra;
 170         int seen_paren = 0;
 171         int i;
 172         unsigned total;
 173
 174         tok = isl_stream_next_token(s);
 175         if (!tok)
 176                 goto error;
 177         if (tok->type == '(') {
 178                 seen_paren = 1;
 179                 isl_token_free(tok);
 180         } else
 181                 isl_stream_push_token(s, tok);
 182         *v = read_var_list(s, *v);
 183         if (!*v)
 184                 goto error;
 185         extra = (*v)->n - n;
 186         bmap = isl_basic_map_cow(bmap);
 187         bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
 188                         extra, 0, 0);
 189         total = isl_basic_map_total_dim(bmap);
 190         for (i = 0; i < extra; ++i) {
 191                 int k;
 192                 if ((k = isl_basic_map_alloc_div(bmap)) < 0)
 193                         goto error;
 194                 isl_seq_clr(bmap->div[k], 1+1+total);
 195         }
 196         if (!bmap)
 197                 return NULL;
 198         if (isl_stream_eat(s, ':'))
 199                 goto error;
 200         bmap = add_constraints(s, v, bmap);
 201         if (seen_paren && isl_stream_eat(s, ')'))
 202                 goto error;
 203         return bmap;
 204 error:
 205         isl_basic_map_free(bmap);
 206         return NULL;
 207 }
 208
 209 static struct isl_basic_map *add_constraint(struct isl_stream *s,
 210         struct vars **v, struct isl_basic_map *bmap)
 211 {
 212         unsigned total = isl_basic_map_total_dim(bmap);
 213         int k;
 214         int sign = 1;
 215         int equality = 0;
 216         int op = 0;
 217         struct isl_token *tok = NULL;
 218
 219         tok = isl_stream_next_token(s);
 220         if (!tok)
 221                 goto error;
 222         if (tok->type == ISL_TOKEN_EXISTS) {
 223                 isl_token_free(tok);
 224                 return add_exists(s, v, bmap);
 225         }
 226         isl_stream_push_token(s, tok);
 227
 228         bmap = isl_basic_map_cow(bmap);
 229         bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
 230         k = isl_basic_map_alloc_inequality(bmap);
 231         if (k < 0)
 232                 goto error;
 233         isl_seq_clr(bmap->ineq[k], 1+total);
 234
 235         for (;;) {
 236                 tok = isl_stream_next_token(s);
 237                 if (!tok) {
 238                         isl_stream_error(s, NULL, "unexpected EOF");
 239                         goto error;
 240                 }
 241                 if (tok->type == ISL_TOKEN_IDENT) {
 242                         int n = (*v)->n;
 243                         int pos = vars_pos(*v, tok->u.s, -1);
 244                         if (pos < 0)
 245                                 goto error;
 246                         if (pos >= n) {
 247                                 isl_stream_error(s, tok, "unknown identifier");
 248                                 goto error;
 249                         }
 250                         if (sign > 0)
 251                                 isl_int_add_ui(bmap->ineq[k][1+pos],
 252                                                 bmap->ineq[k][1+pos], 1);
 253                         else
 254                                 isl_int_sub_ui(bmap->ineq[k][1+pos],
 255                                                 bmap->ineq[k][1+pos], 1);
 256                 } else if (tok->type == ISL_TOKEN_VALUE) {
 257                         struct isl_token *tok2;
 258                         int n = (*v)->n;
 259                         int pos = -1;
 260                         tok2 = isl_stream_next_token(s);
 261                         if (tok2 && tok2->type == ISL_TOKEN_IDENT) {
 262                                 pos = vars_pos(*v, tok2->u.s, -1);
 263                                 if (pos < 0)
 264                                         goto error;
 265                                 if (pos >= n) {
 266                                         isl_stream_error(s, tok2,
 267                                                 "unknown identifier");
 268                                         isl_token_free(tok2);
 269                                         goto error;
 270                                 }
 271                                 isl_token_free(tok2);
 272                         } else if (tok2)
 273                                 isl_stream_push_token(s, tok2);
 274                         if (sign < 0)
 275                                 isl_int_neg(tok->u.v, tok->u.v);
 276                         isl_int_add(bmap->ineq[k][1+pos],
 277                                         bmap->ineq[k][1+pos], tok->u.v);
 278                 } else if (tok->type == '+') {
 279                         /* nothing */
 280                 } else if (tok->type == ISL_TOKEN_LE) {
 281                         op = 1;
 282                         isl_seq_neg(bmap->ineq[k], bmap->ineq[k], 1+total);
 283                 } else if (tok->type == ISL_TOKEN_GE) {
 284                         op = 1;
 285                         sign = -1;
 286                 } else if (tok->type == '=') {
 287                         if (op) {
 288                                 isl_stream_error(s, tok, "too many operators");
 289                                 goto error;
 290                         }
 291                         op = 1;
 292                         equality = 1;
 293                         sign = -1;
 294                 } else {
 295                         isl_stream_push_token(s, tok);
 296                         break;
 297                 }
 298                 isl_token_free(tok);
 299         }
 300         tok = NULL;
 301         if (!op) {
 302                 isl_stream_error(s, tok, "missing operator");
 303                 goto error;
 304         }
 305         if (equality)
 306                 isl_basic_map_inequality_to_equality(bmap, k);
 307         return bmap;
 308 error:
 309         if (tok)
 310                 isl_token_free(tok);
 311         isl_basic_map_free(bmap);
 312         return NULL;
 313 }
 314
 315 static struct isl_basic_map *add_constraints(struct isl_stream *s,
 316         struct vars **v, struct isl_basic_map *bmap)
 317 {
 318         struct isl_token *tok;
 319
 320         for (;;) {
 321                 bmap = add_constraint(s, v, bmap);
 322                 if (!bmap)
 323                         return NULL;
 324                 tok = isl_stream_next_token(s);
 325                 if (!tok) {
 326                         isl_stream_error(s, NULL, "unexpected EOF");
 327                         goto error;
 328                 }
 329                 if (tok->type != ISL_TOKEN_AND)
 330                         break;
 331                 isl_token_free(tok);
 332         }
 333         isl_stream_push_token(s, tok);
 334
 335         return bmap;
 336 error:
 337         if (tok)
 338                 isl_token_free(tok);
 339         isl_basic_map_free(bmap);
 340         return NULL;
 341 }
 342
 343 static struct isl_basic_map *basic_map_read(struct isl_stream *s)
 344 {
 345         struct isl_basic_map *bmap = NULL;
 346         struct isl_token *tok;
 347         struct vars *v = NULL;
 348         int n1;
 349         int n2;
 350
 351         tok = isl_stream_next_token(s);
 352         if (!tok || tok->type != '{') {
 353                 isl_stream_error(s, tok, "expecting '{'");
 354                 if (tok)
 355                         isl_stream_push_token(s, tok);
 356                 goto error;
 357         }
 358         isl_token_free(tok);
 359         v = vars_new(s->ctx);
 360         v = read_tuple(s, v);
 361         if (!v)
 362                 return NULL;
 363         n1 = v->n;
 364         tok = isl_stream_next_token(s);
 365         if (tok && tok->type == ISL_TOKEN_TO) {
 366                 isl_token_free(tok);
 367                 v = read_tuple(s, v);
 368                 if (!v)
 369                         return NULL;
 370                 n2 = v->n - n1;
 371         } else {
 372                 if (tok)
 373                         isl_stream_push_token(s, tok);
 374                 n2 = n1;
 375                 n1 = 0;
 376         }
 377         bmap = isl_basic_map_alloc(s->ctx, 0, n1, n2, 0, 0,0);
 378         if (!bmap)
 379                 goto error;
 380         tok = isl_stream_next_token(s);
 381         if (tok && tok->type == ':') {
 382                 isl_token_free(tok);
 383                 bmap = add_constraints(s, &v, bmap);
 384                 tok = isl_stream_next_token(s);
 385         }
 386         if (tok && tok->type == '}') {
 387                 isl_token_free(tok);
 388         } else {
 389                 isl_stream_error(s, tok, "unexpected isl_token");
 390                 if (tok)
 391                         isl_token_free(tok);
 392                 goto error;
 393         }
 394         vars_free(v);
 395
 396         bmap = isl_basic_map_simplify(bmap);
 397         bmap = isl_basic_map_finalize(bmap);
 398         return bmap;
 399 error:
 400         isl_basic_map_free(bmap);
 401         if (v)
 402                 vars_free(v);
 403         return NULL;
 404 }
 405
 406 struct isl_basic_map *isl_basic_map_read_from_file_omega(
 407                 struct isl_ctx *ctx, FILE *input)
 408 {
 409         struct isl_basic_map *bmap;
 410         struct isl_stream *s = isl_stream_new_file(ctx, input);
 411         if (!s)
 412                 return NULL;
 413         bmap = basic_map_read(s);
 414         isl_stream_free(s);
 415         return bmap;
 416 }
 417
 418 struct isl_basic_set *isl_basic_set_read_from_file_omega(
 419                 struct isl_ctx *ctx, FILE *input)
 420 {
 421         struct isl_basic_map *bmap;
 422         bmap = isl_basic_map_read_from_file_omega(ctx, input);
 423         if (!bmap)
 424                 return NULL;
 425         isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
 426         return (struct isl_basic_set *)bmap;
 427 error:
 428         isl_basic_map_free(bmap);
 429         return NULL;
 430 }
 431
 432 struct isl_basic_map *isl_basic_map_read_from_str_omega(
 433                 struct isl_ctx *ctx, const char *str)
 434 {
 435         struct isl_basic_map *bmap;
 436         struct isl_stream *s = isl_stream_new_str(ctx, str);
 437         if (!s)
 438                 return NULL;
 439         bmap = basic_map_read(s);
 440         isl_stream_free(s);
 441         return bmap;
 442 }
 443
 444 struct isl_basic_set *isl_basic_set_read_from_str_omega(
 445                 struct isl_ctx *ctx, const char *str)
 446 {
 447         struct isl_basic_map *bmap;
 448         bmap = isl_basic_map_read_from_str_omega(ctx, str);
 449         if (!bmap)
 450                 return NULL;
 451         isl_assert(ctx, isl_basic_map_n_in(bmap) == 0, goto error);
 452         return (struct isl_basic_set *)bmap;
 453 error:
 454         isl_basic_map_free(bmap);
 455         return NULL;
 456 }