omega/parser.y

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