omega/parser.y

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