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