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