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