omega/parser.y

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