omega/parser.y

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