omega/parser.y

   1 %{
   2
   3 #define compilingParser
   4 #include <basic/Dynamic_Array.h>
   5 #include <code_gen/code_gen.h>
   6 #include <code_gen/spmd.h>
   7 #include <omega/library_version.h>
   8 #include <omega/AST.h>
   9 #include <omega_calc/yylex.h>
  10 #include <omega/hull.h>
  11 #include <omega/calc_debug.h>
  12 #include <basic/Exit.h>
  13 #include <omega/closure.h>
  14 #include <omega/reach.h>
  15 #include <code_gen/mmap-codegen.h>
  16 #include <code_gen/mmap-util.h>
  17 #ifndef WIN32
  18 #include <sys/time.h>
  19 #include <sys/resource.h>
  20 #endif
  21 #include "count.h"
  22 #include "vertices.h"
  23
  24 #define CALC_VERSION_STRING "Omega Calculator v1.2"
  25
  26 #define DEBUG_FILE_NAME "./oc.out"
  27
  28
  29 Map<Const_String,Relation*> relationMap ((Relation *)0);
  30 static int redundant_conj_level;
  31
  32 #if defined BRAIN_DAMAGED_FREE
  33 void free(void *p);
  34 void *realloc(void *p, size_t s);
  35 #endif
  36
  37 #if !defined(OMIT_GETRUSAGE)
  38 void start_clock( void );
  39 int clock_diff( void );
  40 bool anyTimingDone = false;
  41 #endif
  42
  43 int argCount = 0;
  44 int tuplePos = 0;
  45 Argument_Tuple currentTuple = Input_Tuple;
  46 char *currentVar = NULL;
  47
  48 Relation LexForward(int n);
  49
  50
  51 reachable_information *reachable_info;
  52
  53
  54 %}
  55
  56 %token <VAR_NAME> VAR
  57 %token <INT_VALUE> INT
  58 %token <STRING_VALUE> STRING
  59 %token OPEN_BRACE CLOSE_BRACE
  60 %token SYMBOLIC
  61 %token OR AND NOT
  62 %token ST APPROX
  63 %token IS_ASSIGNED
  64 %token FORALL EXISTS
  65 %token OMEGA_DOMAIN RANGE
  66 %token DIFFERENCE DIFFERENCE_TO_RELATION
  67 %token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
  68 %token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK
  69 %token MAXIMIZE_RANGE MINIMIZE_RANGE
  70 %token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
  71 %token LEQ GEQ NEQ
  72 %token GOES_TO
  73 %token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
  74 %token UNION INTERSECTION
  75 %token VERTICAL_BAR SUCH_THAT
  76 %token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS
  77 %token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS
  78 %token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
  79 %token <REL_OPERATOR> REL_OP
  80 %token RESTRICT_DOMAIN RESTRICT_RANGE
  81 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
  82 %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
  83 %token ASSERT_UNSAT
  84 %token CARD RANKING COUNT_LEXSMALLER
  85 %token VERTICES
  86
  87 %token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
  88
  89 %nonassoc ASSERT_UNSAT
  90 %left UNION OMEGA_P1 '+' '-'
  91 %nonassoc  SUPERSETOF SUBSETOF
  92 %left           OMEGA_P2 RESTRICT_DOMAIN RESTRICT_RANGE
  93 %left INTERSECTION OMEGA_P3 '*' '@'
  94 %left           OMEGA_P4
  95 %left OR        OMEGA_P5
  96 %left AND       OMEGA_P6
  97 %left COMPOSE JOIN CARRIED_BY
  98 %right NOT APPROX OMEGA_DOMAIN RANGE HULL PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS DIFFERENCE DIFFERENCE_TO_RELATION INVERSE COMPLEMENT FARKAS SAMPLE SYM_SAMPLE MAKE_UPPER_BOUND MAKE_LOWER_BOUND OMEGA_P7
  99 %left OMEGA_P8
 100 %nonassoc GIVEN
 101 %left OMEGA_P9
 102 %left '('       OMEGA_P10
 103 %right CARD RANKING COUNT_LEXSMALLER
 104 %right VERTICES
 105
 106
 107 %type <INT_VALUE> effort
 108 %type <EXP> exp simpleExp
 109 %type <EXP_LIST> expList
 110 %type <VAR_LIST> varList
 111 %type <ARGUMENT_TUPLE> argumentList
 112 %type <ASTP> formula optionalFormula
 113 %type <ASTCP> constraintChain
 114 %type <TUPLE_DESCRIPTOR> tupleDeclaration
 115 %type <DECLARATION_SITE> varDecl varDeclOptBrackets
 116 %type <RELATION> relation builtRelation context
 117 %type <RELATION> reachable_of
 118 %type <REL_TUPLE_PAIR> relPairList
 119 %type <REL_TUPLE_TRIPLE> relTripList
 120 %type <RELATION_ARRAY_1D> reachable
 121 %type <STM_INFO_TUPLE> statementInfoList statementInfoResult
 122 %type <STM_INFO> statementInfo
 123 %type <STM_INFO> reads
 124 %type <READ>  oneread
 125 %type <READ>  partials
 126 %type <PREAD> partial
 127 %type <MMAP>  partialwrites
 128 %type <PMMAP> partialwrite
 129
 130 %union {
 131         int INT_VALUE;
 132         Rel_Op REL_OPERATOR;
 133         char *VAR_NAME;
 134         VarList *VAR_LIST;
 135         Exp *EXP;
 136         ExpList *EXP_LIST;
 137         AST *ASTP;
 138         Argument_Tuple ARGUMENT_TUPLE;
 139         AST_constraints *ASTCP;
 140         Declaration_Site * DECLARATION_SITE;
 141         Relation * RELATION;
 142         tupleDescriptor * TUPLE_DESCRIPTOR;
 143         RelTuplePair * REL_TUPLE_PAIR;
 144         RelTupleTriple * REL_TUPLE_TRIPLE;
 145         Dynamic_Array2<Relation> * RELATION_ARRAY_2D;
 146         Dynamic_Array1<Relation> * RELATION_ARRAY_1D;
 147         Tuple<String> *STRING_TUPLE;
 148         String *STRING_VALUE;
 149         Tuple<stm_info> *STM_INFO_TUPLE;
 150         stm_info *STM_INFO;
 151         Read *READ;
 152         PartialRead *PREAD;
 153         MMap *MMAP;
 154         PartialMMap *PMMAP;
 155         };
 156
 157
 158 %%
 159
 160
 161 start : {
 162         }
 163         inputSequence ;
 164
 165 inputSequence : inputItem
 166         | inputSequence { assert( current_Declaration_Site == globalDecls);}
 167                 inputItem
 168         ;
 169
 170 inputItem :
 171         error ';' {
 172                 flushScanBuffer();
 173                 /* Kill all the local declarations -- ejr */
 174                 if (currentVar)
 175                     free(currentVar);
 176                 Declaration_Site *ds1, *ds2;
 177                 for(ds1 = current_Declaration_Site; ds1 != globalDecls;) {
 178                     ds2 = ds1;
 179                     ds1=ds1->previous;
 180                     delete ds2;
 181                 }
 182                 current_Declaration_Site = globalDecls;
 183                 yyerror("skipping to statement end");
 184                 }
 185         | SYMBOLIC globVarList ';'
 186                 { flushScanBuffer();
 187                 }
 188         | VAR { currentVar = $1; } IS_ASSIGNED relation ';'
 189                         {
 190                           flushScanBuffer();
 191                           $4->simplify(min(2,redundant_conj_level),4);
 192                           Relation *r = relationMap((Const_String)$1);
 193                           if (r) delete r;
 194                           relationMap[(Const_String)$1] = $4;
 195                           currentVar = NULL;
 196                           free($1);
 197                         }
 198         | relation ';' {
 199                           flushScanBuffer();
 200                         printf("\n");
 201                         $1->simplify(redundant_conj_level,4);
 202                         $1->print_with_subs(stdout);
 203                         printf("\n");
 204                         delete $1;
 205                         }
 206         | TIME relation ';' {
 207
 208 #if defined(OMIT_GETRUSAGE)
 209             printf("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
 210
 211 #else
 212
 213                         flushScanBuffer();
 214                         printf("\n");
 215                         int t;
 216                         Relation R;
 217                         bool SKIP_FULL_CHECK = getenv("OC_TIMING_SKIP_FULL_CHECK");
 218                         ($2)->and_with_GEQ();
 219                         start_clock();
 220                         for (t=1;t<=100;t++) {
 221                                 R = *$2;
 222                                 R.finalize();
 223                                 }
 224                         int copyTime = clock_diff();
 225                         start_clock();
 226                         for (t=1;t<=100;t++) {
 227                                 R = *$2;
 228                                 R.finalize();
 229                                 R.simplify();
 230                                 }
 231                         int simplifyTime = clock_diff() -copyTime;
 232                         Relation R2;
 233                         if (!SKIP_FULL_CHECK)
 234                           {
 235                             start_clock();
 236                             for (t=1;t<=100;t++) {
 237                               R2 = *$2;
 238                               R2.finalize();
 239                               R2.simplify(2,4);
 240                             }
 241                           }
 242                         int excessiveTime = clock_diff() - copyTime;
 243                         printf("Times (in microseconds): \n");
 244                         printf("%5d us to copy original set of constraints\n",copyTime/100);
 245                         printf("%5d us to do the default amount of simplification, obtaining: \n\t",
 246                                         simplifyTime/100);
 247                         R.print_with_subs(stdout);
 248                     printf("\n");
 249                         if (!SKIP_FULL_CHECK)
 250                           {
 251                             printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
 252                                    excessiveTime/100);
 253                             R2.print_with_subs(stdout);
 254                             printf("\n");
 255                           }
 256                         if (!anyTimingDone) {
 257                                 bool warn = false;
 258 #ifndef SPEED
 259                                 warn =true;
 260 #endif
 261 #ifndef NDEBUG
 262                                 warn = true;
 263 #endif
 264                                 if (warn) {
 265                                    printf("WARNING: The Omega calculator was compiled with options that force\n");
 266                                    printf("it to perform additional consistency and error checks\n");
 267                                    printf("that may slow it down substantially\n");
 268                                   printf("\n");
 269                                    }
 270                                 printf("NOTE: These times relect the time of the current _implementation_\n");
 271                                 printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
 272                                 printf("report on the performance on the Omega test, we respectfully but strongly \n");
 273                                 printf("request that send your test cases to us to allow us to determine if the \n");
 274                                 printf("times are appropriate, and if the way you are using the Omega library to \n");
 275                                 printf("solve your problem is the most effective way.\n");
 276                                 printf("\n");
 277
 278 printf("Also, please be aware that over the past two years, we have focused our \n");
 279 printf("efforts on the expressive power of the Omega library, sometimes at the\n");
 280 printf("expensive of raw speed. Our original implementation of the Omega test\n");
 281 printf("was substantially faster on the limited domain it handled.\n");
 282                                 printf("\n");
 283                                 printf("        Thanks, \n");
 284                                 printf("           the Omega Team \n");
 285                                 }
 286                         anyTimingDone = true;
 287                         delete $2;
 288 #endif
 289                         }
 290         | TIMECLOSURE relation ';' {
 291
 292 #if defined(OMIT_GETRUSAGE)
 293             printf("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
 294 #else
 295                         flushScanBuffer();
 296                         printf("\n");
 297                         int t;
 298                         Relation R;
 299                         ($2)->and_with_GEQ();
 300                         start_clock();
 301                         for (t=1;t<=100;t++) {
 302                                 R = *$2;
 303                                 R.finalize();
 304                                 }
 305                         int copyTime = clock_diff();
 306                         start_clock();
 307                         for (t=1;t<=100;t++) {
 308                                 R = *$2;
 309                                 R.finalize();
 310                                 R.simplify();
 311                                 };
 312                         int simplifyTime = clock_diff() -copyTime;
 313                         Relation Rclosed;
 314                         start_clock();
 315                         for (t=1;t<=100;t++) {
 316                                 Rclosed = *$2;
 317                                 Rclosed.finalize();
 318                                 Rclosed = TransitiveClosure(Rclosed, 1,Relation::Null());
 319                                 };
 320                         int closureTime = clock_diff() - copyTime;
 321                         Relation R2;
 322                         start_clock();
 323                         for (t=1;t<=100;t++) {
 324                                 R2 = *$2;
 325                                 R2.finalize();
 326                                 R2.simplify(2,4);
 327                                 };
 328                         int excessiveTime = clock_diff() - copyTime;
 329                         printf("Times (in microseconds): \n");
 330                         printf("%5d us to copy original set of constraints\n",copyTime/100);
 331                         printf("%5d us to do the default amount of simplification, obtaining: \n\t",
 332                                         simplifyTime/100);
 333                         R.print_with_subs(stdout);
 334                     printf("\n");
 335                         printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
 336                                         excessiveTime/100);
 337                         R2.print_with_subs(stdout);
 338                         printf("%5d us to do the transitive closure, obtaining: \n\t",
 339                                         closureTime/100);
 340                         Rclosed.print_with_subs(stdout);
 341                         printf("\n");
 342                         if (!anyTimingDone) {
 343                                 bool warn = false;
 344 #ifndef SPEED
 345                                 warn =true;
 346 #endif
 347 #ifndef NDEBUG
 348                                 warn = true;
 349 #endif
 350                                 if (warn) {
 351                                    printf("WARNING: The Omega calculator was compiled with options that force\n");
 352                                    printf("it to perform additional consistency and error checks\n");
 353                                    printf("that may slow it down substantially\n");
 354                                   printf("\n");
 355                                    }
 356                                 printf("NOTE: These times relect the time of the current _implementation_\n");
 357                                 printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
 358                                 printf("report on the performance on the Omega test, we respectfully but strongly \n");
 359                                 printf("request that send your test cases to us to allow us to determine if the \n");
 360                                 printf("times are appropriate, and if the way you are using the Omega library to \n");
 361                                 printf("solve your problem is the most effective way.\n");
 362                                 printf("\n");
 363
 364 printf("Also, please be aware that over the past two years, we have focused our \n");
 365 printf("efforts on the expressive power of the Omega library, sometimes at the\n");
 366 printf("expensive of raw speed. Our original implementation of the Omega test\n");
 367 printf("was substantially faster on the limited domain it handled.\n");
 368                                 printf("\n");
 369                                 printf("        Thanks, \n");
 370                                 printf("           the Omega Team \n");
 371                                 }
 372                         anyTimingDone = true;
 373                         delete $2;
 374 #endif
 375                         }
 376
 377
 378         | relation SUBSET relation ';' {
 379                           flushScanBuffer();
 380                         int c = Must_Be_Subset(*$1, *$3);
 381                         printf("\n%s\n", c ? "True" : "False");
 382                         delete $1;
 383                         delete $3;
 384                         }
 385         | CODEGEN effort relPairList context';'
 386                        {
 387                           flushScanBuffer();
 388                           String s = MMGenerateCode($3->mappings, $3->ispaces,*$4,$2);
 389                           delete $4;
 390                           delete $3;
 391                           printf("%s\n", (const char *) s);
 392                        }
 393         | TCODEGEN effort statementInfoResult context';'
 394                         {
 395                           flushScanBuffer();
 396                           String s = tcodegen($2, *($3), *($4));
 397                           delete $4;
 398                           delete $3;
 399                           printf("%s\n", (const char *) s);
 400                         }
 401 /*        | TCODEGEN NOT effort statementInfoResult context';'
 402  *                      {
 403  *                        flushScanBuffer();
 404  *                        String s = tcodegen($3, *($4), *($5), false);
 405  *                        delete $5;
 406  *                        delete $4;
 407  *                        printf("%s\n", (const char *) s);
 408  *                      }
 409  */
 410         | SPMD blockAndProcsAndEffort relTripList';'
 411             {
 412             Tuple<Free_Var_Decl*> lowerBounds(0), upperBounds(0), my_procs(0);
 413             Tuple<spmd_stmt_info *> names(0);
 414
 415             flushScanBuffer();
 416             int nr_statements = $3->space.size();
 417
 418             for (int i = 1; i<= $3->space[1].n_out(); i++)
 419                 {
 420                 lowerBounds.append(new Free_Var_Decl("lb" + itoS(i)));
 421                 upperBounds.append(new Free_Var_Decl("ub" + itoS(i)));
 422                 my_procs.append(new Free_Var_Decl("my_proc" + itoS(i)));
 423                 }
 424
 425             for (int p = 1; p <= nr_statements; p++)
 426                 names.append(new numbered_stmt_info(p-1, Identity($3->time[p].n_out()),
 427                                                     $3->space[p],
 428                                         (char *)(const char *)("s"+itoS(p-1))));
 429
 430             String s = SPMD_GenerateCode("", $3->space, $3->time, $3->ispaces,
 431                                          names,
 432                                          lowerBounds, upperBounds, my_procs,
 433                                          nr_statements);
 434
 435             delete $3;
 436             printf("%s\n", (const char *) s);
 437             }
 438         | reachable ';'
 439         {       flushScanBuffer();
 440                 Dynamic_Array1<Relation> &final = *$1;
 441                 bool any_sat=false;
 442                 int i,n_nodes = reachable_info->node_names.size();
 443                 for(i = 1; i <= n_nodes; i++) if(final[i].is_upper_bound_satisfiable()) {
 444                   any_sat = true;
 445                   fprintf(stdout,"Node %s: ",
 446                           (const char *) (reachable_info->node_names[i]));
 447                   final[i].print_with_subs(stdout);
 448                 }
 449                 if(!any_sat)
 450                   fprintf(stdout,"No nodes reachable.\n");
 451                 delete $1;
 452                 delete reachable_info;
 453         }
 454         | CARD relation ';' {
 455             evalue *EP = count_relation(*$2);
 456             if (EP) {
 457                 const Variable_ID_Tuple * globals = $2->global_decls();
 458                 const char **param_names = new (const char *)[globals->size()];
 459                 for (int i = 0; i < globals->size(); ++i)
 460                     param_names[i] = (*globals)[i+1]->char_name();
 461                 print_evalue(stdout, EP, (char**)param_names);
 462                 puts("");
 463                 delete [] param_names;
 464                 free_evalue_refs(EP);
 465                 free(EP);
 466             }
 467             delete $2;
 468         }
 469         | RANKING relation ';' {
 470             evalue *EP = rank_relation(*$2);
 471             if (EP) {
 472                 const Variable_ID_Tuple * globals = $2->global_decls();
 473                 int nvar = $2->n_set();
 474                 int n = nvar + globals->size();
 475                 const char **names = new (const char *)[n];
 476                 $2->setup_names();
 477                 for (int i = 0; i < nvar; ++i)
 478                     names[i] = $2->set_var(i+1)->char_name();
 479                 for (int i = 0; i < globals->size(); ++i)
 480                     names[nvar+i] = (*globals)[i+1]->char_name();
 481                 print_evalue(stdout, EP, (char**)names);
 482                 puts("");
 483                 delete [] names;
 484                 free_evalue_refs(EP);
 485                 free(EP);
 486             }
 487             delete $2;
 488         }
 489         | COUNT_LEXSMALLER relation WITHIN relation ';' {
 490             evalue *EP = count_lexsmaller(*$2, *$4);
 491             if (EP) {
 492                 const Variable_ID_Tuple * globals = $4->global_decls();
 493                 int nvar = $4->n_set();
 494                 int n = nvar + globals->size();
 495                 const char **names = new (const char *)[n];
 496                 $4->setup_names();
 497                 for (int i = 0; i < nvar; ++i)
 498                     names[i] = $4->set_var(i+1)->char_name();
 499                 for (int i = 0; i < globals->size(); ++i)
 500                     names[nvar+i] = (*globals)[i+1]->char_name();
 501                 print_evalue(stdout, EP, (char**)names);
 502                 puts("");
 503                 delete [] names;
 504                 free_evalue_refs(EP);
 505                 free(EP);
 506             }
 507             delete $2;
 508             delete $4;
 509         }
 510         | VERTICES relation ';' {
 511             vertices(*$2);
 512             delete $2;
 513         }
 514         ;
 515
 516 relTripList: relTripList ',' relation ':' relation ':' relation
 517                 {
 518                 $1->space.append(*$3);
 519                 $1->time.append(*$5);
 520                 $1->ispaces.append(*$7);
 521                 delete $3;
 522                 delete $5;
 523                 delete $7;
 524                 $$ = $1;
 525                 }
 526         | relation ':' relation ':' relation
 527                 {
 528                 RelTupleTriple *rtt = new RelTupleTriple;
 529                 rtt->space.append(*$1);
 530                 rtt->time.append(*$3);
 531                 rtt->ispaces.append(*$5);
 532                 delete $1;
 533                 delete $3;
 534                 delete $5;
 535                 $$ = rtt;
 536                 }
 537                 ;
 538
 539 blockAndProcsAndEffort  : { Block_Size = 0; Num_Procs = 0; overheadEffort=0; }
 540                | INT { Block_Size = $1; Num_Procs = 0; overheadEffort=0;}
 541                | INT INT { Block_Size = $1; Num_Procs = $2; overheadEffort=0;}
 542                | INT INT INT { Block_Size = $1; Num_Procs = $2; overheadEffort=$3;}
 543                ;
 544
 545 effort : { $$ = 0; }
 546         | INT { $$ = $1; }
 547         | '-' INT { $$ = -$2; }
 548         ;
 549
 550 context : { $$ = new Relation();
 551                 *$$ = Relation::Null(); }
 552         | GIVEN relation {$$ = $2; }
 553         ;
 554
 555 relPairList: relPairList ',' relation ':' relation
 556                 {
 557                 $1->mappings.append(*$3);
 558                 $1->mappings[$1->mappings.size()].compress();
 559                 $1->ispaces.append(*$5);
 560                 $1->ispaces[$1->ispaces.size()].compress();
 561                 delete $3;
 562                 delete $5;
 563                 $$ = $1;
 564                 }
 565         | relPairList ',' relation
 566                 {
 567                 $1->mappings.append(Identity($3->n_set()));
 568                 $1->mappings[$1->mappings.size()].compress();
 569                 $1->ispaces.append(*$3);
 570                 $1->ispaces[$1->ispaces.size()].compress();
 571                 delete $3;
 572                 $$ = $1;
 573                 }
 574         | relation ':' relation
 575                 {
 576                 RelTuplePair *rtp = new RelTuplePair;
 577                 rtp->mappings.append(*$1);
 578                 rtp->mappings[rtp->mappings.size()].compress();
 579                 rtp->ispaces.append(*$3);
 580                 rtp->ispaces[rtp->ispaces.size()].compress();
 581                 delete $1;
 582                 delete $3;
 583                 $$ = rtp;
 584                 }
 585         | relation
 586                 {
 587                 RelTuplePair *rtp = new RelTuplePair;
 588                 rtp->mappings.append(Identity($1->n_set()));
 589                 rtp->mappings[rtp->mappings.size()].compress();
 590                 rtp->ispaces.append(*$1);
 591                 rtp->ispaces[rtp->ispaces.size()].compress();
 592                 delete $1;
 593                 $$ = rtp;
 594                 }
 595         ;
 596
 597 statementInfoResult : statementInfoList
 598                 { $$ = $1; }
 599 /*      | ASSERT_UNSAT statementInfoResult
 600  *              { $$ = ($2);
 601  *                DoDebug2("Debug info requested in input", *($2));
 602  *              }
 603  */
 604         | TRANS_IS relation statementInfoResult
 605                 { $$ = &Trans_IS(*($3), *($2));
 606                   delete $2;
 607                 }
 608         | SET_MMAP INT partialwrites statementInfoResult
 609                 { $$ = &Set_MMap(*($4), $2, *($3));
 610                   delete $3;
 611                 }
 612         | UNROLL_IS INT INT INT statementInfoResult
 613                 { $$ = &Unroll_One_IS(*($5), $2, $3, $4);}
 614         | PEEL_IS INT INT relation statementInfoResult
 615                 { $$ = &Peel_One_IS(*($5), $2, $3, *($4));
 616                   delete $4;
 617                 }
 618         | PEEL_IS INT INT relation ',' relation statementInfoResult
 619                 { $$ = &Peel_One_IS(*($7), $2, $3, *($4), *($6));
 620                   delete $4;
 621                   delete $6;
 622                 }
 623         ;
 624
 625 statementInfoList : statementInfo               { $$ = new Tuple<stm_info>;
 626                                                   $$->append(*($1));
 627                                                   delete $1; }
 628         | statementInfoList ',' statementInfo   { $$ = $1;
 629                                                   $$->append(*($3));
 630                                                   delete $3; }
 631         ;
 632
 633 statementInfo : '[' STRING ',' relation ',' partialwrites ',' reads ']'
 634                 { $$ = $8;
 635                   $$->stm = *($2); delete $2;
 636                   $$->IS  = *($4); delete $4;
 637                   $$->map = *($6); delete $6;
 638                   }
 639              |  '[' STRING ',' relation ',' partialwrites ']'
 640                 { $$ = new stm_info;
 641                   $$->stm = *($2); delete $2;
 642                   $$->IS  = *($4); delete $4;
 643                   $$->map = *($6); delete $6;
 644                 }
 645         ;
 646
 647 partialwrites   : partialwrites ',' partialwrite
 648                                 { $$ = $1;
 649                                   $$->partials.append(*($3)); delete $3;
 650                                 }
 651                 | partialwrite  { $$ = new MMap;
 652                                   $$->partials.append(*($1)); delete $1;
 653                                 }
 654         ;
 655
 656 partialwrite : STRING '[' relation ']' ',' relation
 657                                         { $$ = new PartialMMap;
 658                                           $$->mapping = *($6); delete $6;
 659                                           $$->bounds  = *($3); delete $3;
 660                                           $$->var     = *($1); delete $1;
 661                                         }
 662               | STRING ',' relation     { $$ = new PartialMMap;
 663                                           $$->mapping = *($3); delete $3;
 664                                           $$->bounds  = Relation::True(0);
 665                                           $$->var     = *($1); delete $1;
 666                                         }
 667         ;
 668
 669 reads : reads ',' oneread       { $$ = $1;
 670                                   $$->read.append(*($3)); delete $3;
 671                                 }
 672         | oneread               { $$ = new stm_info;
 673                                   $$->read.append(*($1)); delete $1;
 674                                 }
 675         ;
 676
 677 oneread :  '[' partials ']' { $$ = $2; }
 678         ;
 679
 680 partials : partials ',' partial { $$ = $1;
 681                                   $$->partials.append(*($3)); delete $3;
 682                                 }
 683         | partial               { $$ = new Read;
 684                                   $$->partials.append(*($1)); delete $1;
 685                                 }
 686         ;
 687
 688 partial : INT ',' relation      { $$ = new PartialRead;
 689                                   $$->from = $1;
 690                                   $$->dataFlow = *($3); delete $3;
 691                                 }
 692         ;
 693
 694 globVarList: globVarList ',' globVar
 695         | globVar
 696         ;
 697
 698 globVar:  VAR '(' INT ')'
 699                 { globalDecls->extend_both_tuples($1, $3); free($1); }
 700         | VAR
 701                 { globalDecls->extend($1); free($1); }
 702         ;
 703
 704 relation : OPEN_BRACE
 705                 { relationDecl = new Declaration_Site(); }
 706                   builtRelation
 707                 CLOSE_BRACE
 708                 { $$ = $3;
 709                   if (omega_calc_debug) {
 710                         fprintf(DebugFile,"Built relation:\n");
 711                         $$->prefix_print(DebugFile);
 712                         };
 713                   current_Declaration_Site = globalDecls;
 714                   delete relationDecl;
 715                 }
 716          | VAR {
 717                 Const_String s = $1;
 718                 if (relationMap(s) == 0) {
 719                         fprintf(stderr,"Variable %s not declared\n",$1);
 720                         free($1);
 721                         YYERROR;
 722                         assert(0);
 723                         };
 724                 free($1);
 725                 $$ = new Relation(*relationMap(s));
 726                 }
 727          | '(' relation ')'     {$$ = $2;}
 728          | relation '+'         %prec OMEGA_P9
 729                 { $$ = new Relation();
 730                   *$$ = TransitiveClosure(*$1, 1,Relation::Null());
 731                   delete $1;
 732                 }
 733          | relation '*'         %prec OMEGA_P9
 734                 { $$ = new Relation();
 735                   int vars = $1->n_inp();
 736                   *$$ = Union(Identity(vars),
 737                               TransitiveClosure(*$1, 1,Relation::Null()));
 738                   delete $1;
 739                 }
 740          | relation '+' WITHIN relation %prec OMEGA_P9
 741                 {$$ = new Relation();
 742                  *$$= TransitiveClosure(*$1, 1,*$4);
 743                  delete $1;
 744                  delete $4;
 745                }
 746          | MINIMIZE_RANGE relation %prec OMEGA_P8
 747                 {
 748                 Relation o(*$2);
 749                 Relation r(*$2);
 750                 r = Join(r,LexForward($2->n_out()));
 751                 $$ = new Relation();
 752                 *$$ = Difference(o,r);
 753                 delete $2;
 754                 }
 755          | MAXIMIZE_RANGE relation %prec OMEGA_P8
 756                 {
 757                 Relation o(*$2);
 758                 Relation r(*$2);
 759                 r = Join(r,Inverse(LexForward($2->n_out())));
 760                 $$ = new Relation();
 761                 *$$ = Difference(o,r);
 762                 delete $2;
 763                 }
 764          | MINIMIZE_DOMAIN relation %prec OMEGA_P8
 765                 {
 766                 Relation o(*$2);
 767                 Relation r(*$2);
 768                 r = Join(LexForward($2->n_inp()),r);
 769                 $$ = new Relation();
 770                 *$$ = Difference(o,r);
 771                 delete $2;
 772                 }
 773          | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
 774                 {
 775                 Relation o(*$2);
 776                 Relation r(*$2);
 777                 r = Join(Inverse(LexForward($2->n_inp())),r);
 778                 $$ = new Relation();
 779                 *$$ = Difference(o,r);
 780                 delete $2;
 781                 }
 782          | MAXIMIZE relation %prec OMEGA_P8
 783                 {
 784                 Relation c(*$2);
 785                 Relation r(*$2);
 786                 $$ = new Relation();
 787                 *$$ = Cross_Product(Relation(*$2),c);
 788                 delete $2;
 789                 assert($$->n_inp() ==$$->n_out());
 790                 *$$ = Difference(r,Domain(Intersection(*$$,LexForward($$->n_inp()))));
 791                 }
 792          | MINIMIZE relation %prec OMEGA_P8
 793                 {
 794                 Relation c(*$2);
 795                 Relation r(*$2);
 796                 $$ = new Relation();
 797                 *$$ = Cross_Product(Relation(*$2),c);
 798                 delete $2;
 799                 assert($$->n_inp() ==$$->n_out());
 800                 *$$ = Difference(r,Range(Intersection(*$$,LexForward($$->n_inp()))));
 801                 }
 802          | FARKAS relation   %prec OMEGA_P8
 803                 {
 804                 $$ = new Relation();
 805                 *$$ = Farkas(*$2, Basic_Farkas);
 806                 delete $2;
 807                 }
 808          | DECOUPLED_FARKAS relation   %prec OMEGA_P8
 809                 {
 810                 $$ = new Relation();
 811                 *$$ = Farkas(*$2, Decoupled_Farkas);
 812                 delete $2;
 813                 }
 814          | relation '@'         %prec OMEGA_P9
 815                 { $$ = new Relation();
 816                   *$$ = ConicClosure(*$1);
 817                   delete $1;
 818                 }
 819          | PROJECT_AWAY_SYMBOLS relation   %prec OMEGA_P8
 820                 { $$ = new Relation();
 821                   *$$ = Project_Sym(*$2);
 822                   delete $2;
 823                 }
 824          | PROJECT_ON_SYMBOLS relation   %prec OMEGA_P8
 825                 { $$ = new Relation();
 826                   *$$ = Project_On_Sym(*$2);
 827                   delete $2;
 828                 }
 829          | DIFFERENCE relation   %prec OMEGA_P8
 830                 { $$ = new Relation();
 831                   *$$ = Deltas(*$2);
 832                   delete $2;
 833                 }
 834          | DIFFERENCE_TO_RELATION relation   %prec OMEGA_P8
 835                 { $$ = new Relation();
 836                   *$$ = DeltasToRelation(*$2,$2->n_set(),$2->n_set());
 837                   delete $2;
 838                 }
 839          | OMEGA_DOMAIN relation   %prec OMEGA_P8
 840                 { $$ = new Relation();
 841                   *$$ = Domain(*$2);
 842                   delete $2;
 843                 }
 844          | VENN relation   %prec OMEGA_P8
 845                 { $$ = new Relation();
 846                   *$$ = VennDiagramForm(*$2,Relation::True(*$2));
 847                   delete $2;
 848                 }
 849          | VENN relation GIVEN  relation  %prec OMEGA_P8
 850                 { $$ = new Relation();
 851                   *$$ = VennDiagramForm(*$2,*$4);
 852                   delete $2;
 853                   delete $4;
 854                 }
 855          | CONVEX_HULL relation   %prec OMEGA_P8
 856                 { $$ = new Relation();
 857                   *$$ = ConvexHull(*$2);
 858                   delete $2;
 859                 }
 860          | POSITIVE_COMBINATION relation   %prec OMEGA_P8
 861                 { $$ = new Relation();
 862                   *$$ = Farkas(*$2,Positive_Combination_Farkas);
 863                   delete $2;
 864                 }
 865          | CONVEX_COMBINATION relation   %prec OMEGA_P8
 866                 { $$ = new Relation();
 867                   *$$ = Farkas(*$2,Convex_Combination_Farkas);
 868                   delete $2;
 869                 }
 870          | PAIRWISE_CHECK relation   %prec OMEGA_P8
 871                 { $$ = new Relation();
 872                   *$$ = CheckForConvexRepresentation(CheckForConvexPairs(*$2));
 873                   delete $2;
 874                 }
 875          | CONVEX_CHECK relation   %prec OMEGA_P8
 876                 { $$ = new Relation();
 877                   *$$ = CheckForConvexRepresentation(*$2);
 878                   delete $2;
 879                 }
 880          | AFFINE_HULL relation   %prec OMEGA_P8
 881                 { $$ = new Relation();
 882                   *$$ = AffineHull(*$2);
 883                   delete $2;
 884                 }
 885          | CONIC_HULL relation   %prec OMEGA_P8
 886                 { $$ = new Relation();
 887                   *$$ = ConicHull(*$2);
 888                   delete $2;
 889                 }
 890          | LINEAR_HULL relation   %prec OMEGA_P8
 891                 { $$ = new Relation();
 892                   *$$ = LinearHull(*$2);
 893                   delete $2;
 894                 }
 895          | HULL relation   %prec OMEGA_P8
 896                 { $$ = new Relation();
 897                   *$$ = Hull(*$2,false,1,Null_Relation());
 898                   delete $2;
 899                 }
 900          | HULL relation GIVEN relation  %prec OMEGA_P8
 901                 { $$ = new Relation();
 902                   *$$ = Hull(*$2,false,1,*$4);
 903                   delete $2;
 904                   delete $4;
 905                 }
 906          | APPROX relation   %prec OMEGA_P8
 907                 { $$ = new Relation();
 908                   *$$ = Approximate(*$2);
 909                   delete $2;
 910                 }
 911          | RANGE relation   %prec OMEGA_P8
 912                 { $$ = new Relation();
 913                   *$$ = Range(*$2);
 914                   delete $2;
 915                 }
 916          | INVERSE relation   %prec OMEGA_P8
 917                 { $$ = new Relation();
 918                   *$$ = Inverse(*$2);
 919                   delete $2;
 920                 }
 921          | COMPLEMENT relation   %prec OMEGA_P8
 922                 { $$ = new Relation();
 923                   *$$ = Complement(*$2);
 924                   delete $2;
 925                 }
 926          | GIST relation GIVEN relation %prec OMEGA_P8
 927                 { $$ = new Relation();
 928                   *$$ = Gist(*$2,*$4,1);
 929                   delete $2;
 930                   delete $4;
 931                 }
 932          | relation '(' relation ')'
 933                 { $$ = new Relation();
 934                   *$$ = Composition(*$1,*$3);
 935                   delete $1;
 936                   delete $3;
 937                 }
 938          | relation COMPOSE relation
 939                 { $$ = new Relation();
 940                   *$$ = Composition(*$1,*$3);
 941                   delete $1;
 942                   delete $3;
 943                 }
 944          | relation CARRIED_BY INT
 945                 { $$ = new Relation();
 946                   *$$ = After(*$1,$3,$3);
 947                   delete $1;
 948                   (*$$).prefix_print(stdout);
 949                 }
 950          | relation JOIN relation
 951                 { $$ = new Relation();
 952                   *$$ = Composition(*$3,*$1);
 953                   delete $1;
 954                   delete $3;
 955                 }
 956          | relation RESTRICT_RANGE relation
 957                 { $$ = new Relation();
 958                   *$$ = Restrict_Range(*$1,*$3);
 959                   delete $1;
 960                   delete $3;
 961                 }
 962          | relation RESTRICT_DOMAIN relation
 963                 { $$ = new Relation();
 964                   *$$ = Restrict_Domain(*$1,*$3);
 965                   delete $1;
 966                   delete $3;
 967                 }
 968          | relation INTERSECTION relation
 969                 { $$ = new Relation();
 970                   *$$ = Intersection(*$1,*$3);
 971                   delete $1;
 972                   delete $3;
 973                 }
 974          | relation '-' relation %prec INTERSECTION
 975                 { $$ = new Relation();
 976                   *$$ = Difference(*$1,*$3);
 977                   delete $1;
 978                   delete $3;
 979                 }
 980          | relation UNION relation
 981                 { $$ = new Relation();
 982                   *$$ = Union(*$1,*$3);
 983                   delete $1;
 984                   delete $3;
 985                 }
 986          | relation '*' relation
 987                 { $$ = new Relation();
 988                   *$$ = Cross_Product(*$1,*$3);
 989                   delete $1;
 990                   delete $3;
 991                 }
 992          | SUPERSETOF relation
 993                 { $$ = new Relation();
 994                   *$$ = Union(*$2, Relation::Unknown(*$2));
 995                   delete $2;
 996                 }
 997          | SUBSETOF relation
 998                 { $$ = new Relation();
 999                   *$$ = Intersection(*$2, Relation::Unknown(*$2));
1000                   delete $2;
1001                 }
1002          | MAKE_UPPER_BOUND relation %prec OMEGA_P8
1003                 { $$ = new Relation();
1004                   *$$ = Upper_Bound(*$2);
1005                   delete $2;
1006                 }
1007          | MAKE_LOWER_BOUND relation %prec OMEGA_P8
1008                 { $$ = new Relation();
1009                   *$$ = Lower_Bound(*$2);
1010                   delete $2;
1011                 }
1012          | SAMPLE relation
1013                 { $$ = new Relation();
1014                   *$$ = Sample_Solution(*$2);
1015                   delete $2;
1016                 }
1017          | SYM_SAMPLE relation
1018                 { $$ = new Relation();
1019                   *$$ = Symbolic_Solution(*$2);
1020                   delete $2;
1021                 }
1022          | reachable_of { $$ = $1; }
1023          | ASSERT_UNSAT relation
1024                 {
1025                   if (($2)->is_satisfiable())
1026                           {
1027                             fprintf(stderr,"assert_unsatisfiable failed on ");
1028                             ($2)->print_with_subs(stderr);
1029                             Exit(1);
1030                           }
1031                   $$=$2;
1032                 }
1033
1034         ;
1035
1036 builtRelation :
1037         tupleDeclaration GOES_TO {currentTuple = Output_Tuple;}
1038                         tupleDeclaration {currentTuple = Input_Tuple;} optionalFormula {
1039                 Relation * r = new Relation($1->size,$4->size);
1040                 resetGlobals();
1041                 F_And *f = r->add_and();
1042                 int i;
1043                 for(i=1;i<=$1->size;i++) {
1044                         $1->vars[i]->vid = r->input_var(i);
1045                         if (!$1->vars[i]->anonymous)
1046                                 r->name_input_var(i,$1->vars[i]->stripped_name);
1047                         };
1048                 for(i=1;i<=$4->size;i++) {
1049                         $4->vars[i]->vid = r->output_var(i);
1050                         if (!$4->vars[i]->anonymous)
1051                                 r->name_output_var(i,$4->vars[i]->stripped_name);
1052                         };
1053                 foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0));
1054                 foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0));
1055                 foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c));
1056                 foreach(e,Exp*,$4->eq_constraints, install_eq(f,e,0));
1057                 foreach(e,Exp*,$4->geq_constraints, install_geq(f,e,0));
1058                 foreach(c,strideConstraint*,$4->stride_constraints, install_stride(f,c));
1059                 if ($6) $6->install(f);
1060                 delete $1;
1061                 delete $4;
1062                 delete $6;
1063                 $$ = r; }
1064         | tupleDeclaration optionalFormula {
1065                 Relation * r = new Relation($1->size);
1066                 resetGlobals();
1067                 F_And *f = r->add_and();
1068                 int i;
1069                 for(i=1;i<=$1->size;i++) {
1070                         $1->vars[i]->vid = r->set_var(i);
1071                         if (!$1->vars[i]->anonymous)
1072                                 r->name_set_var(i,$1->vars[i]->stripped_name);
1073                         };
1074                 foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0));
1075                 foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0));
1076                 foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c));
1077                 if ($2) $2->install(f);
1078                 delete $1;
1079                 delete $2;
1080                 $$ = r; }
1081         | formula {
1082                 Relation * r = new Relation(0,0);
1083                 F_And *f = r->add_and();
1084                 $1->install(f);
1085                 delete $1;
1086                 $$ = r;
1087                 }
1088         ;
1089
1090 optionalFormula : formula_sep formula { $$ = $2; }
1091         | {$$ = 0;}
1092         ;
1093
1094 formula_sep : ':'
1095         | VERTICAL_BAR
1096         | SUCH_THAT
1097         ;
1098
1099 tupleDeclaration :
1100         {
1101             if (currentTupleDescriptor)
1102                 delete currentTupleDescriptor;
1103             currentTupleDescriptor = new tupleDescriptor;
1104             tuplePos = 1;
1105         }
1106         '[' optionalTupleVarList ']'
1107         {$$ = currentTupleDescriptor; currentTupleDescriptor = NULL; }
1108         ;
1109
1110 optionalTupleVarList :
1111           tupleVar
1112         | optionalTupleVarList ',' tupleVar
1113         |
1114         ;
1115
1116 tupleVar : VAR %prec OMEGA_P10
1117         { Declaration_Site *ds = defined($1);
1118           if (!ds) currentTupleDescriptor->extend($1,currentTuple,tuplePos);
1119           else {
1120               Variable_Ref * v = lookupScalar($1);
1121               assert(v);
1122               if (ds != globalDecls)
1123                 currentTupleDescriptor->extend($1, new Exp(v));
1124               else
1125                 currentTupleDescriptor->extend(new Exp(v));
1126               }
1127           free($1);
1128           tuplePos++;
1129         }
1130         | '*'
1131         {currentTupleDescriptor->extend(); tuplePos++; }
1132         | exp %prec OMEGA_P1
1133         {currentTupleDescriptor->extend($1); tuplePos++; }
1134         | exp ':' exp %prec OMEGA_P1
1135         {currentTupleDescriptor->extend($1,$3); tuplePos++; }
1136         | exp ':' exp ':' INT %prec OMEGA_P1
1137         {currentTupleDescriptor->extend($1,$3,$5); tuplePos++; }
1138         ;
1139
1140
1141 varList: varList ',' VAR {$$ = $1; $$->insert($3); }
1142         | VAR { $$ = new VarList;
1143                 $$->insert($1); }
1144         ;
1145
1146 varDecl : varList
1147                 {
1148                 $$ = current_Declaration_Site = new Declaration_Site($1);
1149                 foreach(s,char *, *$1, delete s);
1150                 delete $1;
1151                 }
1152         ;
1153
1154 /* variable declaration with optional brackets */
1155
1156 varDeclOptBrackets : varDecl    { $$ = $1; }
1157         | '[' varDecl ']'       { $$ = $2; }
1158         ;
1159
1160 formula : formula AND formula   { $$ = new AST_And($1,$3); }
1161         | formula OR formula    { $$ = new AST_Or($1,$3); }
1162         | constraintChain       { $$ = $1; }
1163         | '(' formula ')'       { $$ = $2; }
1164         | NOT formula           { $$ = new AST_Not($2); }
1165         | start_exists varDeclOptBrackets exists_sep formula end_quant
1166                                 { $$ = new AST_exists($2,$4); }
1167         | start_forall varDeclOptBrackets forall_sep formula end_quant
1168                                 { $$ = new AST_forall($2,$4); }
1169         ;
1170
1171 start_exists : '(' EXISTS
1172         | EXISTS '('
1173         ;
1174
1175 exists_sep : ':'
1176         | VERTICAL_BAR
1177         | SUCH_THAT
1178         ;
1179
1180 start_forall : '(' FORALL
1181         | FORALL '('
1182         ;
1183
1184 forall_sep : ':'
1185         ;
1186
1187 end_quant : ')'
1188         { popScope(); }
1189         ;
1190
1191 expList : exp ',' expList
1192                 {
1193                 $$ = $3;
1194                 $$->insert($1);
1195                 }
1196         | exp {
1197                 $$ = new ExpList;
1198                 $$->insert($1);
1199                 }
1200         ;
1201
1202 constraintChain : expList REL_OP expList
1203                         { $$ = new AST_constraints($1,$2,$3); }
1204                 | expList REL_OP constraintChain
1205                         { $$ = new AST_constraints($1,$2,$3); }
1206                 ;
1207
1208 simpleExp :
1209         VAR     %prec OMEGA_P9
1210                 { Variable_Ref * v = lookupScalar($1);
1211                   free($1);
1212                   if (!v) YYERROR;
1213                   $$ = new Exp(v);
1214                   }
1215         | VAR '(' {argCount = 1;}  argumentList ')' %prec OMEGA_P9
1216                 {Variable_Ref *v;
1217                  if ($4 == Input_Tuple) v = functionOfInput[$1];
1218                  else v = functionOfOutput[$1];
1219                  if (v == 0) {
1220                         fprintf(stderr,"Function %s(...) not declared\n",$1);
1221                         free($1);
1222                         YYERROR;
1223                         }
1224                  free($1);
1225                  $$ = new Exp(v);
1226                 }
1227         | '(' exp ')'  { $$ = $2;}
1228         ;
1229
1230
1231
1232 argumentList :
1233         argumentList ',' VAR {
1234                 Variable_Ref * v = lookupScalar($3);
1235                 free($3);
1236                 if (!v) YYERROR;
1237                  if (v->pos != argCount || v->of != $1 || v->of != Input_Tuple && v->of != Output_Tuple) {
1238                         fprintf(stderr,"arguments to function must be prefix of input or output tuple\n");
1239                         YYERROR;
1240                         }
1241                  $$ = v->of;
1242                  argCount++;
1243                 }
1244         | VAR { Variable_Ref * v = lookupScalar($1);
1245                 free($1);
1246                 if (!v) YYERROR;
1247                  if (v->pos != argCount || v->of != Input_Tuple && v->of != Output_Tuple) {
1248                         fprintf(stderr,"arguments to function must be prefix of input or output tuple\n");
1249                         YYERROR;
1250                         }
1251                  $$ = v->of;
1252                  argCount++;
1253                 }
1254         ;
1255
1256 exp : INT               {$$ = new Exp($1);}
1257         | INT simpleExp  %prec '*' {$$ = multiply($1,$2);}
1258         | simpleExp     { $$ = $1; }
1259         | '-' exp %prec '*'   { $$ = negate($2);}
1260         | exp '+' exp  { $$ = add($1,$3);}
1261         | exp '-' exp  { $$ = subtract($1,$3);}
1262         | exp '*' exp  { $$ = multiply($1,$3);}
1263         ;
1264
1265
1266 reachable :
1267         REACHABLE_FROM nodeNameList nodeSpecificationList
1268                 {
1269                   Dynamic_Array1<Relation> *final =
1270                     Reachable_Nodes(reachable_info);
1271                   $$ = final;
1272                 }
1273         ;
1274
1275 reachable_of :
1276         REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1277                 {
1278                   Dynamic_Array1<Relation> *final =
1279                     Reachable_Nodes(reachable_info);
1280                   int index = reachable_info->node_names.index(String($2));
1281                   assert(index != 0 && "No such node");
1282                   $$ = new Relation;
1283                   *$$ = (*final)[index];
1284                   delete final;
1285                   delete reachable_info;
1286                   delete $2;
1287                 }
1288         ;
1289
1290
1291 nodeNameList: '(' realNodeNameList ')'
1292               { int sz = reachable_info->node_names.size();
1293                 reachable_info->node_arity.reallocate(sz);
1294                 reachable_info->transitions.resize(sz+1,sz+1);
1295                 reachable_info->start_nodes.resize(sz+1);
1296               }
1297         ;
1298
1299 realNodeNameList: realNodeNameList ',' VAR
1300               { reachable_info->node_names.append(String($3));
1301                 delete $3; }
1302         | VAR { reachable_info = new reachable_information;
1303                 reachable_info->node_names.append(String($1));
1304                 delete $1; }
1305         ;
1306
1307
1308 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1309         {
1310            int i,j;
1311            int n_nodes = reachable_info->node_names.size();
1312            Tuple<int> &arity = reachable_info->node_arity;
1313            Dynamic_Array2<Relation> &transitions = reachable_info->transitions;
1314
1315            /* fixup unspecified transitions to be false */
1316            /* find arity */
1317            for(i = 1; i <= n_nodes; i++) arity[i] = -1;
1318            for(i = 1; i <= n_nodes; i++)
1319              for(j = 1; j <= n_nodes; j++)
1320                 if(! transitions[i][j].is_null()) {
1321                   int in_arity = transitions[i][j].n_inp();
1322                   int out_arity = transitions[i][j].n_out();
1323                   if(arity[i] < 0) arity[i] = in_arity;
1324                   if(arity[j] < 0) arity[j] = out_arity;
1325                   if(in_arity != arity[i] || out_arity != arity[j]) {
1326                     fprintf(stderr,
1327                             "Arity mismatch in node transition: %s -> %s",
1328                             (const char *) reachable_info->node_names[i],
1329                             (const char *) reachable_info->node_names[j]);
1330                         assert(0);
1331                     YYERROR;
1332                   }
1333                 }
1334            for(i = 1; i <= n_nodes; i++)
1335              if(arity[i] < 0) arity[i] = 0;
1336            /* Fill in false relations */
1337            for(i = 1; i <= n_nodes; i++)
1338              for(j = 1; j <= n_nodes; j++)
1339                 if(transitions[i][j].is_null())
1340                   transitions[i][j] = Relation::False(arity[i],arity[j]);
1341
1342
1343           /* fixup unused start node positions */
1344            Dynamic_Array1<Relation> &nodes = reachable_info->start_nodes;
1345            for(i = 1; i <= n_nodes; i++)
1346              if(nodes[i].is_null())
1347                 nodes[i] = Relation::False(arity[i]);
1348              else
1349                 if(nodes[i].n_set() != arity[i]){
1350                     fprintf(stderr,"Arity mismatch in start node %s",
1351                             (const char *) reachable_info->node_names[i]);
1352                 assert(0);
1353                     YYERROR;
1354                 }
1355         }
1356         ;
1357
1358 realNodeSpecificationList:
1359         realNodeSpecificationList ',' VAR ':' relation
1360           {  int n_nodes = reachable_info->node_names.size();
1361              int index = reachable_info->node_names.index($3);
1362              assert(index != 0 && index <= n_nodes);
1363              reachable_info->start_nodes[index] = *$5;
1364              delete $3;
1365              delete $5;
1366           }
1367         | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation
1368           {  int n_nodes = reachable_info->node_names.size();
1369              int from_index = reachable_info->node_names.index($3);
1370              int   to_index = reachable_info->node_names.index($5);
1371              assert(from_index != 0 && to_index != 0);
1372              assert(from_index <= n_nodes && to_index <= n_nodes);
1373              reachable_info->transitions[from_index][to_index] = *$7;
1374              delete $3;
1375              delete $5;
1376              delete $7;
1377           }
1378         | VAR GOES_TO VAR ':' relation
1379           {  int n_nodes = reachable_info->node_names.size();
1380              int from_index = reachable_info->node_names.index($1);
1381              int   to_index = reachable_info->node_names.index($3);
1382              assert(from_index != 0 && to_index != 0);
1383              assert(from_index <= n_nodes && to_index <= n_nodes);
1384              reachable_info->transitions[from_index][to_index] = *$5;
1385              delete $1;
1386              delete $3;
1387              delete $5;
1388           }
1389         | VAR ':' relation
1390           {  int n_nodes = reachable_info->node_names.size();
1391              int index = reachable_info->node_names.index($1);
1392              assert(index != 0 && index <= n_nodes);
1393              reachable_info->start_nodes[index] = *$3;
1394              delete $1;
1395              delete $3;
1396           }
1397         ;
1398
1399 %%
1400
1401 #if !defined(OMIT_GETRUSAGE)
1402 #include <sys/types.h>
1403 #include <sys/time.h>
1404 #include <sys/resource.h>
1405
1406 struct rusage start_time;
1407 #endif
1408
1409 #if defined BRAIN_DAMAGED_FREE
1410 void free(void *p)
1411     {
1412     free((char *)p);
1413     }
1414
1415 void *realloc(void *p, size_t s)
1416     {
1417     return realloc((malloc_t) p, s);
1418     }
1419 #endif
1420
1421 #if ! defined(OMIT_GETRUSAGE)
1422 #ifdef __sparc__
1423 extern "C" int getrusage (int, struct rusage*);
1424 #endif
1425
1426 void start_clock( void )
1427     {
1428     getrusage(RUSAGE_SELF, &start_time);
1429     }
1430
1431 int clock_diff( void )
1432     {
1433     struct rusage current_time;
1434     getrusage(RUSAGE_SELF, &current_time);
1435     return (current_time.ru_utime.tv_sec -start_time.ru_utime.tv_sec)*1000000 +
1436            (current_time.ru_utime.tv_usec-start_time.ru_utime.tv_usec);
1437     }
1438 #endif
1439
1440 void printUsage(FILE *outf, char **argv) {
1441     fprintf(outf, "usage: %s {-R} {-D[facility][level]...} infile\n  -R means skip redundant conjunct elimination\n  -D sets debugging level as follows:\n    a = all debugging flags\n    g = code generation\n    l = calculator\n    c = omega core\n    p = presburger functions\n    r = relational operators\n    t = transitive closure\nAll debugging output goes to %s\n",argv[0],DEBUG_FILE_NAME);
1442 }
1443
1444 int omega_calc_debug;
1445 extern FILE *yyin;
1446
1447 int main(int argc, char **argv){
1448   redundant_conj_level = 2;
1449   current_Declaration_Site = globalDecls = new Global_Declaration_Site();
1450 #if YYDEBUG != 0
1451   yydebug  = 1;
1452 #endif
1453   int i;
1454   char * fileName = 0;
1455
1456   printf("# %s (based on %s, %s):\n",CALC_VERSION_STRING, Omega_Library_Version, Omega_Library_Date);
1457
1458   calc_all_debugging_off();
1459
1460 #ifdef SPEED
1461   DebugFile = fopen("/dev/null","w");
1462   assert(DebugFile);
1463 #else
1464   DebugFile = fopen(DEBUG_FILE_NAME, "w");
1465   if (!DebugFile) {
1466     fprintf(stderr, "Can't open debug file %s\n", DEBUG_FILE_NAME);
1467     DebugFile = stderr;
1468   }
1469   setbuf(DebugFile,0);
1470 #endif
1471
1472   closure_presburger_debug = 0;
1473
1474   setOutputFile(DebugFile);
1475
1476   // Process flags
1477   for(i=1; i<argc; i++) {
1478     if(argv[i][0] == '-') {
1479       int j = 1, c;
1480       while((c=argv[i][j++]) != 0) {
1481         switch(c) {
1482         case 'D':
1483             if (! process_calc_debugging_flags(argv[i],j)) {
1484                 printUsage(stderr,argv);
1485                 Exit(1);
1486             }
1487             break;
1488         case 'G':
1489             {
1490               fprintf(stderr,"Note: specifying number of GEQ's is no longer useful.\n");
1491               while(argv[i][j] != 0) j++;
1492             }
1493             break;
1494         case 'E':
1495             {
1496               fprintf(stderr,"Note: specifying number of EQ's is no longer useful.\n");
1497               while(argv[i][j] != 0) j++;
1498             }
1499             break;
1500         case 'R':
1501             redundant_conj_level = 1;
1502             break;
1503         // Other future options go here
1504         default:
1505           fprintf(stderr, "\nUnknown flag -%c\n", c);
1506           printUsage(stderr,argv);
1507           Exit(1);
1508         }
1509       }
1510     }
1511    else {
1512      // Make sure this is a file name
1513      if (fileName) {
1514         fprintf(stderr,"\nCan only handle a single input file\n");
1515         printUsage(stderr,argv);
1516         Exit(1);
1517         };
1518      fileName = argv[i];
1519      yyin = fopen(fileName, "r");
1520      if (!yyin) {
1521             fprintf(stderr, "\nCan't open input file %s\n",fileName);
1522             printUsage(stderr,argv);
1523             Exit(1);
1524             };
1525      }
1526    }
1527
1528
1529   initializeOmega();
1530   initializeScanBuffer();
1531   currentTupleDescriptor = NULL;
1532
1533   yyparse();
1534
1535   delete globalDecls;
1536   foreach_map(cs,Const_String,r,Relation *,relationMap,
1537               {delete r; relationMap[cs]=0;});
1538
1539   return(0);
1540 } /* end main */
1541
1542
1543 Relation LexForward(int n) {
1544   Relation r(n,n);
1545   F_Or *f = r.add_or();
1546   for (int i=1; i <= n; i++) {
1547         F_And *g = f->add_and();
1548         for(int j=1;j<i;j++) {
1549            EQ_Handle e = g->add_EQ();
1550            e.update_coef(r.input_var(j),-1);
1551            e.update_coef(r.output_var(j),1);
1552            e.finalize();
1553            }
1554         GEQ_Handle e = g->add_GEQ();
1555         e.update_coef(r.input_var(i),-1);
1556         e.update_coef(r.output_var(i),1);
1557         e.update_const(-1);
1558         e.finalize();
1559         }
1560   r.finalize();
1561   return r;
1562   }
1563
1564