omega/parser.y

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