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