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