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