From 147eb3bdde75eacf7a049fa7cbffbd612411c334 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Thu, 3 Apr 2008 16:19:13 +0200 Subject: [PATCH] omega/occ: optionally use parker for computing cardinality of a set Also remove the occ in parker, which would only provide this functionality. --- Makefile.am | 2 +- barvinok_enumerate_e.cc | 40 +- doc/barvinok.bib | 13 + doc/omega.tex | 5 + omega/Makefile.am | 6 +- omega/convert.cc | 41 +- omega/convert.h | 2 + omega/count.cc | 80 ++- omega/count.h | 9 +- omega/parser.l | 3 + omega/parser.y | 46 +- parker/Exit.cc | 11 - parker/Makefile.am | 17 - parker/count_solutions.cc | 13 + parker/count_solutions.h | 23 +- parker/omega_calc/yylex.h | 4 - parker/parser.l | 331 ---------- parker/parser.y | 1495 --------------------------------------------- 18 files changed, 195 insertions(+), 1946 deletions(-) delete mode 100644 parker/Exit.cc rewrite parker/count_solutions.h (90%) delete mode 100644 parker/omega_calc/yylex.h delete mode 100644 parker/parser.l delete mode 100644 parker/parser.y diff --git a/Makefile.am b/Makefile.am index fe3939e..a994710 100644 --- a/Makefile.am +++ b/Makefile.am @@ -201,7 +201,7 @@ barvinok_count_SOURCES = barvinok_count.c barvinok_ehrhart_SOURCES = barvinok_ehrhart.cc barvinok_union_SOURCES = barvinok_union.cc if HAVE_OMEGA -BEEO_SOURCES = omega/Exit.cc omega/convert.cc +BEEO_SOURCES = omega/Exit.cc omega/convert.cc omega/count.cc else BEEO_SOURCES = endif diff --git a/barvinok_enumerate_e.cc b/barvinok_enumerate_e.cc index ea9ef6c..312762a 100644 --- a/barvinok_enumerate_e.cc +++ b/barvinok_enumerate_e.cc @@ -9,16 +9,13 @@ #include "config.h" #ifdef HAVE_OMEGA #include "omega/convert.h" -#endif -#ifdef USE_PARKER -#include "parker/count_solutions.h" +#include "omega/count.h" #endif #include "skewed_genfun.h" #include "verify.h" #include "verif_ehrhart.h" #include "verify_series.h" #include "evalue_convert.h" -#include "normalization.h" /* The input of this example program is a polytope in combined * data and parameter space followed by two lines indicating @@ -29,8 +26,6 @@ * The polytope is in PolyLib notation. */ -#define ALLOC(t,p) p = (t*)malloc(sizeof(*p)) - struct argp_option argp_options[] = { { "omega", 'o', 0, 0 }, { "parker", 'P', 0, 0 }, @@ -114,37 +109,7 @@ Polyhedron *Omega_simplify(Polyhedron *P, { return P; } -#endif -#ifdef USE_PARKER -/* - * Use parker's method to compute the number of integer points in P. - * Since this method assumes all variables are non-negative, - * we have to transform the input polytope first. - */ -evalue *barvinok_enumerate_parker(Polyhedron *P, - unsigned exist, unsigned nparam, - unsigned MaxRays) -{ - Polyhedron *R; - evalue *res; - - assert(nparam == 0); - R = skew_to_positive_orthant(P, P->Dimension-exist, MaxRays); - Relation r = Polyhedron2relation(R, exist, 0, NULL); - Polyhedron_Free(R); - double d = count_solutions(r); - ALLOC(evalue, res); - value_init(res->d); - value_set_si(res->d, 0); - res->x.p = new_enode(partition, 2, 0); - EVALUE_SET_DOMAIN(res->x.p->arr[0], Universe_Polyhedron(0)); - value_set_si(res->x.p->arr[1].d, 1); - value_init(res->x.p->arr[1].x.n); - value_set_double(res->x.p->arr[1].x.n, d); - return res; -} -#else evalue *barvinok_enumerate_parker(Polyhedron *P, unsigned exist, unsigned nparam, unsigned MaxRays) @@ -235,7 +200,8 @@ int main(int argc, char **argv) } } else { if (arguments.parker) - EP = barvinok_enumerate_parker(A, exist, nparam, options->MaxRays); + EP = barvinok_enumerate_parker(A, A->Dimension-nparam-exist, + nparam, options->MaxRays); else if (arguments.scarf) EP = barvinok_enumerate_scarf(A, exist, nparam, options); else if (arguments.pip && exist > 0) diff --git a/doc/barvinok.bib b/doc/barvinok.bib index 9fabbaa..0c07406 100644 --- a/doc/barvinok.bib +++ b/doc/barvinok.bib @@ -992,3 +992,16 @@ MRREVIEWER = {P. McMullen}, pages = "121--134", year = "1994", } + +@inproceedings{Parker2004, + title = "An automata-theoretic algorithm for counting solutions to {Presburger} formulas", + author = "Erin Parker and Siddhartha Chatterjee", + year = 2004, + booktitle = "Compiler Construction 2004", + series = {Lecture Notes in Computer Science}, + volume = 2985, + pages = {104--119}, + month = apr, + publisher = "Springer-Verlag", + address = "Berlin", +} diff --git a/doc/omega.tex b/doc/omega.tex index e88c9c3..10e3cc6 100644 --- a/doc/omega.tex +++ b/doc/omega.tex @@ -33,6 +33,11 @@ Name & Syntax & Explanation Card & \ai[\tt]{card} $r$ & Computes the number of integer points in $r$ and prints the result to standard output \\ +Card & \ai[\tt]{card} $r$ {\tt using} \ai[\tt]{parker} & +Computes the number of integer points in $r$ and +prints the result to standard output +using the method of \shortciteN{Parker2004} +\\ Ranking & \ai[\tt]{ranking} $r$ & Computes the rank function of $r$ and prints the result to standard output \shortcite{Loechner2002,Turjan2002} diff --git a/omega/Makefile.am b/omega/Makefile.am index f0b9776..748e0c7 100644 --- a/omega/Makefile.am +++ b/omega/Makefile.am @@ -14,7 +14,11 @@ occ_SOURCES = \ vertices.h \ y.tab.cc \ omega_calc/yylex.h -LDADD = -lcode_gen -lomega ../libbarvinok.la ../bernstein/libbernstein.la \ +if USE_PARKER + PARKER_LA = ../parker/libparker.la +endif +LDADD = $(PARKER_LA) \ + -lcode_gen -lomega ../libbarvinok.la ../bernstein/libbernstein.la \ @POLYLIB_LIBS@ @PIPLIB_LIBS@ AM_LDFLAGS = @OMEGA_LDFLAGS@ @POLYLIB_LDFLAGS@ @PIPLIB_LDFLAGS@ AM_CPPFLAGS = -I$(top_srcdir) -I$(top_srcdir)/bernstein/include \ diff --git a/omega/convert.cc b/omega/convert.cc index 48e1c7d..2c9aed1 100644 --- a/omega/convert.cc +++ b/omega/convert.cc @@ -81,10 +81,19 @@ Polyhedron *relation2Domain(Relation& r, varvector& vv, varvector& params, return D; } +typedef std::vector globalvector; + +static void create_globals(globalvector& globals, unsigned nparam, + char **params) +{ + for (int i = 0; i < nparam; ++i) + globals.push_back(new Global_Var_Decl(params[i])); +} + Relation Polyhedron2relation(Polyhedron *P, - unsigned exist, unsigned nparam, char **params) + unsigned exist, globalvector& globals) { - int nvar = P->Dimension - exist - nparam; + int nvar = P->Dimension - exist - globals.size(); Relation r(nvar); varvector vars; @@ -95,8 +104,8 @@ Relation Polyhedron2relation(Polyhedron *P, vars.push_back(r.set_var(j)); for (int i = 0; i < exist; ++i) vars.push_back(e->declare()); - for (int i = 0; i < nparam; ++i) - vars.push_back(r.get_local(new Global_Var_Decl(params[i]))); + for (int i = 0; i < globals.size(); ++i) + vars.push_back(r.get_local(globals[i])); for (int i = 0; i < P->NbConstraints; ++i) { Constraint_Handle h; @@ -112,6 +121,30 @@ Relation Polyhedron2relation(Polyhedron *P, return r; } +Relation Polyhedron2relation(Polyhedron *P, + unsigned exist, unsigned nparam, char **params) +{ + globalvector globals; + create_globals(globals, nparam, params); + return Polyhedron2relation(P, exist, globals); +} + +Relation Domain2relation(Polyhedron *D, unsigned nvar, unsigned nparam, + char **params) +{ + globalvector globals; + create_globals(globals, nparam, params); + + Relation r = Polyhedron2relation(D, D->Dimension - nvar - nparam, + globals); + for (Polyhedron *P = D->next; P; P = P->next) { + Relation s = Polyhedron2relation(P, P->Dimension - nvar - nparam, + globals); + r = Union(r, s); + } + return r; +} + void dump(Relation& r) { varvector vv; diff --git a/omega/convert.h b/omega/convert.h index e048f5d..12a7a81 100644 --- a/omega/convert.h +++ b/omega/convert.h @@ -8,4 +8,6 @@ Polyhedron *relation2Domain(Relation& r, varvector& vv, varvector& params, unsigned MaxRays); Relation Polyhedron2relation(Polyhedron *P, unsigned exist, unsigned nparam, char **params); +Relation Domain2relation(Polyhedron *D, unsigned nvar, unsigned nparam, + char **params); void dump(Relation& r); diff --git a/omega/count.cc b/omega/count.cc index 7b1880c..e011481 100644 --- a/omega/count.cc +++ b/omega/count.cc @@ -1,30 +1,94 @@ +#include #include #include #include #include #include "omega/convert.h" +#include "normalization.h" #include "count.h" +#include "config.h" #include using namespace std; -evalue *count_relation(Relation& r) +#define ALLOC(t,p) p = (t*)malloc(sizeof(*p)) + +#ifdef USE_PARKER + +#include "parker/count_solutions.h" + +/* + * Use parker's method to compute the number of integer points in D. + * Since this method assumes all variables are non-negative, + * we have to transform the input polytope first. + */ +evalue *barvinok_enumerate_parker(Polyhedron *D, + unsigned nvar, unsigned nparam, + unsigned MaxRays) { - varvector vv; - varvector params; - struct barvinok_options *options = barvinok_options_new_with_defaults(); - Polyhedron *D = relation2Domain(r, vv, params, options->MaxRays); - int dim = r.is_set() ? r.n_set() : r.n_inp() + r.n_out(); + Polyhedron *R; + evalue *res; + + if (nparam != 0) { + fprintf(stderr, "parker method doesn't support parameters\n"); + return NULL; + } + R = skew_to_positive_orthant(D, nvar, MaxRays); + Relation r = Domain2relation(R, nvar, 0, NULL); + Polyhedron_Free(R); + double d = count_solutions(r); + ALLOC(evalue, res); + value_init(res->d); + value_set_si(res->d, 0); + res->x.p = new_enode(::partition, 2, 0); + EVALUE_SET_DOMAIN(res->x.p->arr[0], Universe_Polyhedron(0)); + value_set_si(res->x.p->arr[1].d, 1); + value_init(res->x.p->arr[1].x.n); + value_set_double(res->x.p->arr[1].x.n, d); + return res; +} +#else + +evalue *barvinok_enumerate_parker(Polyhedron *D, + unsigned nvar, unsigned nparam, + unsigned MaxRays) +{ + fprintf(stderr, "support for parker method not compiled in\n"); + return NULL; +} + +#endif + +static evalue *count_relation_barvinok(Polyhedron *D, unsigned nvar, + unsigned nparam, unsigned MaxRays) +{ int d = 0; evalue *EP = NULL; for (Polyhedron *P = D; P; P = P->next, ++d) { assert(d == 0); - int exist = P->Dimension - params.size() - dim; - EP = barvinok_enumerate_e(P, exist, params.size(), options->MaxRays); + int exist = P->Dimension - nparam - nvar; + EP = barvinok_enumerate_e(P, exist, nparam, MaxRays); } reduce_evalue(EP); Domain_Free(D); + return EP; +} + +evalue *count_relation(Relation& r, int counting_method) +{ + varvector vv; + varvector params; + struct barvinok_options *options = barvinok_options_new_with_defaults(); + Polyhedron *D = relation2Domain(r, vv, params, options->MaxRays); + + evalue *EP = NULL; + if (counting_method == COUNT_RELATION_BARVINOK) + EP = count_relation_barvinok(D, vv.size(), params.size(), + options->MaxRays); + else if (counting_method == COUNT_RELATION_PARKER) + EP = barvinok_enumerate_parker(D, vv.size(), params.size(), + options->MaxRays); barvinok_options_free(options); return EP; } diff --git a/omega/count.h b/omega/count.h index 6c1f5d2..578bb8c 100644 --- a/omega/count.h +++ b/omega/count.h @@ -1,6 +1,13 @@ #include #include -evalue *count_relation(Relation& r); +#define COUNT_RELATION_BARVINOK 0 +#define COUNT_RELATION_PARKER 1 + +evalue *count_relation(Relation& r, int method); evalue *rank_relation(Relation& r); evalue *count_lexsmaller(Relation& r, Relation& domain); + +evalue *barvinok_enumerate_parker(Polyhedron *D, + unsigned nvar, unsigned nparam, + unsigned MaxRays); diff --git a/omega/parser.l b/omega/parser.l index b825d4a..13a480c 100644 --- a/omega/parser.l +++ b/omega/parser.l @@ -200,6 +200,9 @@ void includeFile(char *s) { "assertUnsatisfiable" { BUFFER; return ASSERT_UNSAT; } "assert_unsatisfiable" { BUFFER; return ASSERT_UNSAT; } "card" { BUFFER; return CARD; } +"using" { BUFFER; return USING; } +"barvinok" { BUFFER; return BARVINOK; } +"parker" { BUFFER; return PARKER; } "ranking" { BUFFER; return RANKING; } "count_lexsmaller" { BUFFER; return COUNT_LEXSMALLER; } "vertices" { BUFFER; return VERTICES; } diff --git a/omega/parser.y b/omega/parser.y index e85a5c9..a1a1e10 100644 --- a/omega/parser.y +++ b/omega/parser.y @@ -77,6 +77,23 @@ Relation *build_relation(tupleDescriptor *tuple, AST* ast) Map *variableMap; +static void evalue_print_and_free(Relation *r, evalue *EP) +{ + if (!EP) + return; + + const Variable_ID_Tuple * globals = r->global_decls(); + const char **param_names = new const char *[globals->size()]; + r->setup_names(); + for (int i = 0; i < globals->size(); ++i) + param_names[i] = (*globals)[i+1]->char_name(); + print_evalue(stdout, EP, param_names); + puts(""); + delete [] param_names; + evalue_free(EP); +} + + %} %token VAR @@ -107,7 +124,7 @@ Map *variableMap; %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF %token ASSERT_UNSAT -%token CARD RANKING COUNT_LEXSMALLER +%token CARD USING BARVINOK PARKER RANKING COUNT_LEXSMALLER %token VERTICES %token BMAX %token DUMP @@ -129,7 +146,7 @@ Map *variableMap; %nonassoc GIVEN %left OMEGA_P9 %left '(' OMEGA_P10 -%right CARD RANKING COUNT_LEXSMALLER +%right CARD USING RANKING COUNT_LEXSMALLER %right VERTICES %right DUMP @@ -158,6 +175,7 @@ Map *variableMap; %type partialwrite %type polyfunc %type polynomial +%type counting_method %union { int INT_VALUE; @@ -486,18 +504,13 @@ printf("was substantially faster on the limited domain it handled.\n"); delete reachable_info; } | CARD relation ';' { - evalue *EP = count_relation(*$2); - if (EP) { - const Variable_ID_Tuple * globals = $2->global_decls(); - const char **param_names = new const char *[globals->size()]; - $2->setup_names(); - for (int i = 0; i < globals->size(); ++i) - param_names[i] = (*globals)[i+1]->char_name(); - print_evalue(stdout, EP, param_names); - puts(""); - delete [] param_names; - evalue_free(EP); - } + evalue *EP = count_relation(*$2, COUNT_RELATION_BARVINOK); + evalue_print_and_free($2, EP); + delete $2; + } + | CARD relation USING counting_method ';' { + evalue *EP = count_relation(*$2, $4); + evalue_print_and_free($2, EP); delete $2; } | RANKING relation ';' { @@ -589,6 +602,11 @@ blockAndProcsAndEffort : { Block_Size = 0; Num_Procs = 0; overheadEffort=0; } | INT INT INT { Block_Size = $1; Num_Procs = $2; overheadEffort=$3;} ; +counting_method: + BARVINOK { $$ = COUNT_RELATION_BARVINOK; } + | PARKER { $$ = COUNT_RELATION_PARKER; } + ; + effort : { $$ = 0; } | INT { $$ = $1; } | '-' INT { $$ = -$2; } diff --git a/parker/Exit.cc b/parker/Exit.cc deleted file mode 100644 index 5df5fc3..0000000 --- a/parker/Exit.cc +++ /dev/null @@ -1,11 +0,0 @@ -#include -#include - -List Exit_hooks; - -void Exit(int e) - { - foreach(func, exit_func, Exit_hooks, (*func)(e)); - - exit(e); - } diff --git a/parker/Makefile.am b/parker/Makefile.am index acf8c08..4fbc230 100644 --- a/parker/Makefile.am +++ b/parker/Makefile.am @@ -11,20 +11,3 @@ libparker_la_LIBADD = -ldfa -lbdd -lmem libparker_la_LDFLAGS = -L$(MONAPATH)/DFA -L$(MONAPATH)/BDD -L$(MONAPATH)/Mem INCLUDES = -I$(MONAPATH)/Mem -I$(MONAPATH)/DFA -I$(MONAPATH)/BDD libparker_la_CPPFLAGS = $(INCLUDES) @OMEGA_CPPFLAGS@ -DNDEBUG - -noinst_PROGRAMS = occ -occ_SOURCES = \ - Exit.cc \ - lex.yy.cc \ - y.tab.cc -occ_CPPFLAGS = @OMEGA_CPPFLAGS@ -occ_LDFLAGS = @OMEGA_LDFLAGS@ -occ_LDADD = -lcode_gen -lomega libparker.la - -YACC_FLAGS = -d - -y.tab.hh y.tab.cc: parser.y - $(YACC) -o y.tab.cc -v -d $< - -lex.yy.cc: parser.l y.tab.hh - $(LEX) -olex.yy.cc -i $< diff --git a/parker/count_solutions.cc b/parker/count_solutions.cc index 0b6153c..2dc5b7e 100644 --- a/parker/count_solutions.cc +++ b/parker/count_solutions.cc @@ -1,6 +1,19 @@ #include #include +extern "C" { +/* Erin Parker (parker@cs.unc.edu), March 2004 */ + +#include "dfa.h" + +/* Functions defined in construction.c */ +DFA* build_DFA_eq(int, int*, int, int*); +DFA* build_DFA_ineq(int, int*, int, int*); + +/* Function defined in count.c */ +double count_accepting_paths(DFA*, int, int); +} + #include "count_solutions.h" typedef std::vector varvector; diff --git a/parker/count_solutions.h b/parker/count_solutions.h dissimilarity index 90% index e4b0254..811b589 100644 --- a/parker/count_solutions.h +++ b/parker/count_solutions.h @@ -1,22 +1 @@ -/* Erin Parker (parker@cs.unc.edu), March 2004 */ - -#include - -#ifdef __cplusplus -extern "C" { -#endif - -#include "dfa.h" - -/* Functions defined in construction.c */ -DFA* build_DFA_eq(int, int*, int, int*); -DFA* build_DFA_ineq(int, int*, int, int*); - -/* Function defined in count.c */ -double count_accepting_paths(DFA*, int, int); - -#ifdef __cplusplus -} -#endif - -double count_solutions(Relation& r); +double count_solutions(Relation& r); diff --git a/parker/omega_calc/yylex.h b/parker/omega_calc/yylex.h deleted file mode 100644 index dda3ea9..0000000 --- a/parker/omega_calc/yylex.h +++ /dev/null @@ -1,4 +0,0 @@ -extern int yylex(void); -extern void yyerror(char * ); -extern void initializeScanBuffer(); -extern void flushScanBuffer(); diff --git a/parker/parser.l b/parker/parser.l deleted file mode 100644 index 59f0cee..0000000 --- a/parker/parser.l +++ /dev/null @@ -1,331 +0,0 @@ -%{ -#include -#include -#include -#include -#include -#include "y.tab.hh" -#include -#ifdef WIN32 -#include -#define isatty _isatty -#include -#define alloca _alloca -#endif - -extern "C" int yywrap() {return 1;}; - - -#if defined BRAIN_DAMAGED_FREE -void free(void *p); -void *realloc(void *p, size_t s); -#else -#define free(x) free((char *)(x)) -#endif - -char scanBuf[1024]; -void initializeScanBuffer() { - scanBuf[0] = '\0'; - }; -void flushScanBuffer() { - fprintf(yyout,"# %s\n",scanBuf); - if (omega_calc_debug) fprintf(DebugFile,"# %s\n",scanBuf); - initializeScanBuffer(); - } -#define BUFFER strcat(scanBuf,yytext) -void yyerror(char *s) { - fprintf(stderr,"%s\n",s); - fprintf(stderr,"line %d, at end of \"%s\"\n",yylineno,scanBuf); - } - -#define MAX_INCLUDE_DEPTH 10 -YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH]; -int include_stack_ptr = 0; - -void includeFile(char *s) { - if ( include_stack_ptr >= MAX_INCLUDE_DEPTH ) - { - fprintf( stderr, "Includes nested too deeply" ); - exit( 1 ); - } - - include_stack[include_stack_ptr++] = - YY_CURRENT_BUFFER; - - FILE *f = fopen( yytext, "r" ); - - if ( ! f ) { - include_stack_ptr--; - fprintf( stderr, "Can't open %s\n",s); - } - else { - yyin = f; - yy_switch_to_buffer( - yy_create_buffer( yyin, YY_BUF_SIZE ) ); - } - - } - -%} - -%s LATEX INCLUDE - -%% - - -"<<" {BUFFER; BEGIN(INCLUDE); } -[^>\n ]+">>" { BUFFER; - char *s = yytext; - while (*s != '>') s++; - *s = '\0'; - includeFile(s); - BEGIN(INITIAL); - - } -[ \n] { fprintf(stderr,"Error in include syntax\n"); - fprintf(stderr,"Use <> to include the file named fname\n"); - Exit(1); - - } - - -"\\ " { BUFFER; } -[ \t]+ { BUFFER; } -(#[^\n]*\n) {strncat(scanBuf,yytext,yyleng-1);yylineno++;flushScanBuffer();} - -"\$\$" { BUFFER; BEGIN 0; } -"\$\$" { BUFFER; BEGIN LATEX; } -"\\t" { BUFFER; } -"\\!" { BUFFER; } -"\\\\" { BUFFER; } - -"\n" { yylineno++; flushScanBuffer(); } -"{" { BUFFER; return OPEN_BRACE; } -"\\{" { BUFFER; return OPEN_BRACE; } -"}" { BUFFER; return CLOSE_BRACE; } -"\\}" { BUFFER; return CLOSE_BRACE; } -"approximate" { BUFFER; return APPROX; } -"union" { BUFFER; return UNION; } -"\\cup" { BUFFER; return UNION; } -"intersection" { BUFFER; return INTERSECTION; } -"\\cap" { BUFFER; return INTERSECTION; } -"symbolic" { BUFFER; return SYMBOLIC; } -"sym" { BUFFER; return SYMBOLIC; } -"\\mid" { BUFFER; return VERTICAL_BAR; } -"|" { BUFFER; return VERTICAL_BAR; } -"\\st" { BUFFER; return SUCH_THAT; } -"s.t." { BUFFER; return SUCH_THAT; } -"inverse" { BUFFER; return INVERSE; } -"complement" { BUFFER; return COMPLEMENT; } -"\\circ" { BUFFER; return COMPOSE; } -"compose" { BUFFER; return COMPOSE; } -"difference" { BUFFER; return DIFFERENCE; } -"diffToRel" { BUFFER; return DIFFERENCE_TO_RELATION; } -"project away symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; } -"project_away_symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; } -"projectAwaySymbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; } -"project on symbols" { BUFFER; return PROJECT_ON_SYMBOLS; } -"project_on_symbols" { BUFFER; return PROJECT_ON_SYMBOLS; } -"projectOnSymbols" { BUFFER; return PROJECT_ON_SYMBOLS; } -"\\join" { BUFFER; return JOIN; } -"\." { BUFFER; return JOIN; } -"join" { BUFFER; return JOIN; } -"domain" { BUFFER; return DOMAIN; } -"time" { BUFFER; return TIME; } -"timeclosure" { BUFFER; return TIMECLOSURE; } -"range" { BUFFER; return RANGE; } -"\\forall" { BUFFER; return FORALL; } -"forall" { BUFFER; return FORALL; } -"\\exists" { BUFFER; return EXISTS; } -"exists" { BUFFER; return EXISTS; } -"PairwiseCheck" { BUFFER; return PAIRWISE_CHECK; } -"Venn" { BUFFER; return VENN; } -"ConvexCheck" { BUFFER; return CONVEX_CHECK; } -"ConvexCombination" { BUFFER; return CONVEX_COMBINATION; } -"PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; } -"ConvexHull" { BUFFER; return CONVEX_HULL; } -"AffineHull" { BUFFER; return AFFINE_HULL; } -"ConicHull" { BUFFER; return CONIC_HULL; } -"LinearHull" { BUFFER; return LINEAR_HULL; } -"hull" { BUFFER; return HULL; } -"minimize" { BUFFER; return MINIMIZE; } -"maximize" { BUFFER; return MAXIMIZE; } -"minimize-range" { BUFFER; return MINIMIZE_RANGE; } -"maximize-range" { BUFFER; return MAXIMIZE_RANGE; } -"minimizerange" { BUFFER; return MINIMIZE_RANGE; } -"maximizerange" { BUFFER; return MAXIMIZE_RANGE; } -"minimize-domain" { BUFFER; return MINIMIZE_DOMAIN; } -"maximize-domain" { BUFFER; return MAXIMIZE_DOMAIN; } -"minimizedomain" { BUFFER; return MINIMIZE_DOMAIN; } -"maximizedomain" { BUFFER; return MAXIMIZE_DOMAIN; } -"gist" { BUFFER; return GIST; } -"given" { BUFFER; return GIVEN; } -"within" { BUFFER; return WITHIN; } -"subset" { BUFFER; return SUBSET; } -"codegen" { BUFFER; return CODEGEN; } -"tcodegen" { BUFFER; return TCODEGEN; } -"trans_is" { BUFFER; return TRANS_IS; } -"trans-is" { BUFFER; return TRANS_IS; } -"set_mmap" { BUFFER; return SET_MMAP; } -"set-mmap" { BUFFER; return SET_MMAP; } -"unroll_is" { BUFFER; return UNROLL_IS; } -"unroll-is" { BUFFER; return UNROLL_IS; } -"peel_is" { BUFFER; return PEEL_IS; } -"peel-is" { BUFFER; return PEEL_IS; } -"spmd" { BUFFER; return SPMD; } -"farkas" { BUFFER; return FARKAS; } -"decoupledfarkas" { BUFFER; return DECOUPLED_FARKAS; } -"decoupled-farkas" { BUFFER; return DECOUPLED_FARKAS; } -"decoupled_farkas" { BUFFER; return DECOUPLED_FARKAS; } -"upper_bound" { BUFFER; return MAKE_UPPER_BOUND; } -"lower_bound" { BUFFER; return MAKE_LOWER_BOUND; } -"supersetof" { BUFFER; return SUPERSETOF;} -"subsetof" { BUFFER; return SUBSETOF;} -"sym_example" { BUFFER; return SYM_SAMPLE;} -"example" { BUFFER; return SAMPLE;} -"carried_by" { BUFFER; return CARRIED_BY;} -"iterations" { BUFFER; return ITERATIONS; } -"reachable" { BUFFER; return REACHABLE_FROM; } -"reachable of" { BUFFER; return REACHABLE_OF; } -"restrict_domain" { BUFFER; return RESTRICT_DOMAIN; } -"restrictDomain" { BUFFER; return RESTRICT_DOMAIN; } -"\\" { yyerror("Can't use \\ for restrict_domain in Tex mode"); } -"\\" { BUFFER; return RESTRICT_DOMAIN; } -"restrict_range" { BUFFER; return RESTRICT_RANGE; } -"restrictRange" { BUFFER; return RESTRICT_RANGE; } -"assertUnsatisfiable" { BUFFER; return ASSERT_UNSAT; } -"assert_unsatisfiable" { BUFFER; return ASSERT_UNSAT; } -"count" { BUFFER; return COUNT; } -"yaml" { BUFFER; return YAML; } -"/" { BUFFER; return RESTRICT_RANGE; } -"&" { BUFFER; return AND; } -"|" { BUFFER; return OR; } -"&&" { BUFFER; return AND; } -"||" { BUFFER; return OR; } -"and" { BUFFER; return AND; } -"or" { BUFFER; return OR; } -"\\land" { BUFFER; return AND; } -"\\lor" { BUFFER; return OR; } -"!" { BUFFER; return NOT; } -"not" { BUFFER; return NOT; } -"\\neg" { BUFFER; return NOT; } -":=" { BUFFER; return IS_ASSIGNED; } -"->" { BUFFER; return GOES_TO; } -"in" { BUFFER; return IN; } -"\\rightarrow" { BUFFER; return GOES_TO; } -"<=" { BUFFER; yylval.REL_OPERATOR = leq; - return REL_OP; - } -"\\leq" { BUFFER; yylval.REL_OPERATOR = leq; - return REL_OP; - } -"\\le" { BUFFER; yylval.REL_OPERATOR = leq; - return REL_OP; - } -">=" { BUFFER; yylval.REL_OPERATOR = geq; - return REL_OP; - } -"\\geq" { BUFFER; yylval.REL_OPERATOR = geq; - return REL_OP; - } -"\\ge" { BUFFER; yylval.REL_OPERATOR = geq; - return REL_OP; - } -"!=" { BUFFER; yylval.REL_OPERATOR = neq; - return REL_OP; - } -"\\neq" { BUFFER; yylval.REL_OPERATOR = neq; - return REL_OP; - } -"<" { BUFFER; yylval.REL_OPERATOR = lt; - return REL_OP; - } -">" { BUFFER; yylval.REL_OPERATOR = gt; - return REL_OP; - } -"=" { BUFFER; yylval.REL_OPERATOR = eq; - return REL_OP; - } -[A-Za-z][A-Za-z0-9_']* { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - return VAR; - } -[A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase - yylval.VAR_NAME[yyleng-2] = 'n'; - return VAR; - } -[A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in" - yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid - yylval.VAR_NAME[yyleng-2] = ')'; - yylval.VAR_NAME[yyleng-1] = '\0'; - return VAR; - } -[A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase - yylval.VAR_NAME[yyleng-3] = 'u'; - yylval.VAR_NAME[yyleng-2] = 't'; - return VAR; - } - -"\\"[A-Za-z][A-Za-z0-9_]* { BUFFER; - if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - return VAR; - } -"\\"[A-Za-z][A-Za-z0-9_]*"(in)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase - yylval.VAR_NAME[yyleng-2] = 'n'; - return VAR; - } -"\\"[A-Za-z][A-Za-z0-9_]*"(set)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in" - yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid - yylval.VAR_NAME[yyleng-2] = ')'; - yylval.VAR_NAME[yyleng-1] = '\0'; - return VAR; - } -"\\"[A-Za-z][A-Za-z0-9_]*"(out)" { BUFFER; if (yyleng > 19) yyerror("Identifier too long"); - yylval.VAR_NAME = (char *) malloc(1+yyleng); - strcpy(yylval.VAR_NAME,yytext); - yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase - yylval.VAR_NAME[yyleng-3] = 'u'; - yylval.VAR_NAME[yyleng-2] = 't'; - return VAR; - } -[0-9]+ { BUFFER; yylval.INT_VALUE = atoi(yytext); - return INT; - } -\"[^"]*\" { BUFFER; - yytext[strlen(yytext)-1]='\0'; - yylval.STRING_VALUE = new String(yytext+1); - return STRING; - } -<> { - if ( --include_stack_ptr < 0 ) - { - yyterminate(); - } - else - { - yy_delete_buffer( YY_CURRENT_BUFFER ); - yy_switch_to_buffer( - include_stack[include_stack_ptr] ); - } - } - -. { BUFFER; return yytext[0]; } - diff --git a/parker/parser.y b/parker/parser.y deleted file mode 100644 index 7f13180..0000000 --- a/parker/parser.y +++ /dev/null @@ -1,1495 +0,0 @@ -%{ - -#define compilingParser -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#ifndef WIN32 -#include -#include -#endif -#include "count_solutions.h" - -#define CALC_VERSION_STRING "Omega Calculator v1.2" - -#define DEBUG_FILE_NAME "./oc.out" - - -Map relationMap ((Relation *)0); -static int redundant_conj_level; - -#if defined BRAIN_DAMAGED_FREE -void free(void *p); -void *realloc(void *p, size_t s); -#endif - -#if !defined(OMIT_GETRUSAGE) -void start_clock( void ); -int clock_diff( void ); -bool anyTimingDone = false; -#endif - -int argCount = 0; -int tuplePos = 0; -Argument_Tuple currentTuple = Input_Tuple; - -Relation LexForward(int n); - - -reachable_information *reachable_info; - - -%} - -%token VAR -%token INT -%token STRING -%token OPEN_BRACE CLOSE_BRACE -%token SYMBOLIC -%token OR AND NOT -%token ST APPROX -%token IS_ASSIGNED -%token FORALL EXISTS -%token DOMAIN RANGE -%token DIFFERENCE DIFFERENCE_TO_RELATION -%token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE -%token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK -%token MAXIMIZE_RANGE MINIMIZE_RANGE -%token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN -%token LEQ GEQ NEQ -%token GOES_TO -%token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE -%token UNION INTERSECTION -%token VERTICAL_BAR SUCH_THAT -%token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS -%token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS -%token MAKE_UPPER_BOUND MAKE_LOWER_BOUND -%token REL_OP -%token RESTRICT_DOMAIN RESTRICT_RANGE -%token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE -%token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF -%token ASSERT_UNSAT -%token COUNT -%token YAML - -%token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION - -%nonassoc ASSERT_UNSAT -%left UNION OMEGA_P1 '+' '-' -%nonassoc SUPERSETOF SUBSETOF -%left OMEGA_P2 RESTRICT_DOMAIN RESTRICT_RANGE -%left INTERSECTION OMEGA_P3 '*' '@' -%left OMEGA_P4 -%left OR OMEGA_P5 -%left AND OMEGA_P6 -%left COMPOSE JOIN CARRIED_BY -%right NOT APPROX 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 -%left OMEGA_P8 -%nonassoc GIVEN -%left OMEGA_P9 -%left '(' OMEGA_P10 -%right COUNT -%right YAML - - -%type effort -%type exp simpleExp -%type expList -%type varList -%type argumentList -%type formula optionalFormula -%type constraintChain -%type tupleDeclaration -%type varDecl varDeclOptBrackets -%type relation builtRelation context -%type reachable_of -%type relPairList -%type relTripList -%type reachable -%type statementInfoList statementInfoResult -%type statementInfo -%type reads -%type oneread -%type partials -%type partial -%type partialwrites -%type partialwrite - -%union { - int INT_VALUE; - Rel_Op REL_OPERATOR; - char *VAR_NAME; - VarList *VAR_LIST; - Exp *EXP; - ExpList *EXP_LIST; - AST *ASTP; - Argument_Tuple ARGUMENT_TUPLE; - AST_constraints *ASTCP; - Declaration_Site * DECLARATION_SITE; - Relation * RELATION; - tupleDescriptor * TUPLE_DESCRIPTOR; - RelTuplePair * REL_TUPLE_PAIR; - RelTupleTriple * REL_TUPLE_TRIPLE; - Dynamic_Array2 * RELATION_ARRAY_2D; - Dynamic_Array1 * RELATION_ARRAY_1D; - Tuple *STRING_TUPLE; - String *STRING_VALUE; - Tuple *STM_INFO_TUPLE; - stm_info *STM_INFO; - Read *READ; - PartialRead *PREAD; - MMap *MMAP; - PartialMMap *PMMAP; - }; - - -%% - - -start : { - } - inputSequence ; - -inputSequence : inputItem - | inputSequence { assert( current_Declaration_Site == globalDecls);} - inputItem - ; - -inputItem : - error ';' { - flushScanBuffer(); - /* Kill all the local declarations -- ejr */ - Declaration_Site *ds1, *ds2; - for(ds1 = current_Declaration_Site; ds1 != globalDecls;) { - ds2 = ds1; - ds1=ds1->previous; - delete ds2; - } - current_Declaration_Site = globalDecls; - yyerror("skipping to statement end"); - } - | SYMBOLIC globVarList ';' - { flushScanBuffer(); - } - | VAR IS_ASSIGNED relation ';' - { - flushScanBuffer(); - $3->simplify(min(2,redundant_conj_level),4); - Relation *r = relationMap((Const_String)$1); - if (r) delete r; - relationMap[(Const_String)$1] = $3; - delete $1; - } - | relation ';' { - flushScanBuffer(); - printf("\n"); - $1->simplify(redundant_conj_level,4); - $1->print_with_subs(stdout); - printf("\n"); - delete $1; - } - | TIME relation ';' { - -#if defined(OMIT_GETRUSAGE) - printf("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n"); - -#else - - flushScanBuffer(); - printf("\n"); - int t; - Relation R; - bool SKIP_FULL_CHECK = getenv("OC_TIMING_SKIP_FULL_CHECK"); - ($2)->and_with_GEQ(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - } - int copyTime = clock_diff(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - R.simplify(); - } - int simplifyTime = clock_diff() -copyTime; - Relation R2; - if (!SKIP_FULL_CHECK) - { - start_clock(); - for (t=1;t<=100;t++) { - R2 = *$2; - R2.finalize(); - R2.simplify(2,4); - } - } - int excessiveTime = clock_diff() - copyTime; - printf("Times (in microseconds): \n"); - printf("%5d us to copy original set of constraints\n",copyTime/100); - printf("%5d us to do the default amount of simplification, obtaining: \n\t", - simplifyTime/100); - R.print_with_subs(stdout); - printf("\n"); - if (!SKIP_FULL_CHECK) - { - printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", - excessiveTime/100); - R2.print_with_subs(stdout); - printf("\n"); - } - if (!anyTimingDone) { - bool warn = false; -#ifndef SPEED - warn =true; -#endif -#ifndef NDEBUG - warn = true; -#endif - if (warn) { - printf("WARNING: The Omega calculator was compiled with options that force\n"); - printf("it to perform additional consistency and error checks\n"); - printf("that may slow it down substantially\n"); - printf("\n"); - } - printf("NOTE: These times relect the time of the current _implementation_\n"); - printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n"); - printf("report on the performance on the Omega test, we respectfully but strongly \n"); - printf("request that send your test cases to us to allow us to determine if the \n"); - printf("times are appropriate, and if the way you are using the Omega library to \n"); - printf("solve your problem is the most effective way.\n"); - printf("\n"); - -printf("Also, please be aware that over the past two years, we have focused our \n"); -printf("efforts on the expressive power of the Omega library, sometimes at the\n"); -printf("expensive of raw speed. Our original implementation of the Omega test\n"); -printf("was substantially faster on the limited domain it handled.\n"); - printf("\n"); - printf(" Thanks, \n"); - printf(" the Omega Team \n"); - } - anyTimingDone = true; - delete $2; -#endif - } - | TIMECLOSURE relation ';' { - -#if defined(OMIT_GETRUSAGE) - printf("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n"); -#else - flushScanBuffer(); - printf("\n"); - int t; - Relation R; - ($2)->and_with_GEQ(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - } - int copyTime = clock_diff(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - R.simplify(); - }; - int simplifyTime = clock_diff() -copyTime; - Relation Rclosed; - start_clock(); - for (t=1;t<=100;t++) { - Rclosed = *$2; - Rclosed.finalize(); - Rclosed = TransitiveClosure(Rclosed, 1,Relation::Null()); - }; - int closureTime = clock_diff() - copyTime; - Relation R2; - start_clock(); - for (t=1;t<=100;t++) { - R2 = *$2; - R2.finalize(); - R2.simplify(2,4); - }; - int excessiveTime = clock_diff() - copyTime; - printf("Times (in microseconds): \n"); - printf("%5d us to copy original set of constraints\n",copyTime/100); - printf("%5d us to do the default amount of simplification, obtaining: \n\t", - simplifyTime/100); - R.print_with_subs(stdout); - printf("\n"); - printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", - excessiveTime/100); - R2.print_with_subs(stdout); - printf("%5d us to do the transitive closure, obtaining: \n\t", - closureTime/100); - Rclosed.print_with_subs(stdout); - printf("\n"); - if (!anyTimingDone) { - bool warn = false; -#ifndef SPEED - warn =true; -#endif -#ifndef NDEBUG - warn = true; -#endif - if (warn) { - printf("WARNING: The Omega calculator was compiled with options that force\n"); - printf("it to perform additional consistency and error checks\n"); - printf("that may slow it down substantially\n"); - printf("\n"); - } - printf("NOTE: These times relect the time of the current _implementation_\n"); - printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n"); - printf("report on the performance on the Omega test, we respectfully but strongly \n"); - printf("request that send your test cases to us to allow us to determine if the \n"); - printf("times are appropriate, and if the way you are using the Omega library to \n"); - printf("solve your problem is the most effective way.\n"); - printf("\n"); - -printf("Also, please be aware that over the past two years, we have focused our \n"); -printf("efforts on the expressive power of the Omega library, sometimes at the\n"); -printf("expensive of raw speed. Our original implementation of the Omega test\n"); -printf("was substantially faster on the limited domain it handled.\n"); - printf("\n"); - printf(" Thanks, \n"); - printf(" the Omega Team \n"); - } - anyTimingDone = true; - delete $2; -#endif - } - - - | relation SUBSET relation ';' { - flushScanBuffer(); - int c = Must_Be_Subset(*$1, *$3); - printf("\n%s\n", c ? "True" : "False"); - delete $1; - delete $3; - } - | CODEGEN effort relPairList context';' - { - flushScanBuffer(); - String s = MMGenerateCode($3->mappings, $3->ispaces,*$4,$2); - delete $4; - delete $3; - printf("%s\n", (const char *) s); - } - | TCODEGEN effort statementInfoResult context';' - { - flushScanBuffer(); - String s = tcodegen($2, *($3), *($4)); - delete $4; - delete $3; - printf("%s\n", (const char *) s); - } -/* | TCODEGEN NOT effort statementInfoResult context';' - * { - * flushScanBuffer(); - * String s = tcodegen($3, *($4), *($5), false); - * delete $5; - * delete $4; - * printf("%s\n", (const char *) s); - * } - */ - | SPMD blockAndProcsAndEffort relTripList';' - { - Tuple lowerBounds(0), upperBounds(0), my_procs(0); - Tuple names(0); - - flushScanBuffer(); - int nr_statements = $3->space.size(); - - for (int i = 1; i<= $3->space[1].n_out(); i++) - { - lowerBounds.append(new Free_Var_Decl("lb" + itoS(i))); - upperBounds.append(new Free_Var_Decl("ub" + itoS(i))); - my_procs.append(new Free_Var_Decl("my_proc" + itoS(i))); - } - - for (int p = 1; p <= nr_statements; p++) - names.append(new numbered_stmt_info(p-1, Identity($3->time[p].n_out()), - $3->space[p], - (char *)(const char *)("s"+itoS(p-1)))); - - String s = SPMD_GenerateCode("", $3->space, $3->time, $3->ispaces, - names, - lowerBounds, upperBounds, my_procs, - nr_statements); - - delete $3; - printf("%s\n", (const char *) s); - } - | reachable ';' - { flushScanBuffer(); - Dynamic_Array1 &final = *$1; - bool any_sat=false; - int i,n_nodes = reachable_info->node_names.size(); - for(i = 1; i <= n_nodes; i++) if(final[i].is_upper_bound_satisfiable()) { - any_sat = true; - fprintf(stdout,"Node %s: ", - (const char *) (reachable_info->node_names[i])); - final[i].print_with_subs(stdout); - } - if(!any_sat) - fprintf(stdout,"No nodes reachable.\n"); - delete $1; - delete reachable_info; - } - | COUNT relation ';' { - double c = count_solutions(*$2); - fprintf(stdout, "%.0f\n", c); - } - ; - -relTripList: relTripList ',' relation ':' relation ':' relation - { - $1->space.append(*$3); - $1->time.append(*$5); - $1->ispaces.append(*$7); - delete $3; - delete $5; - delete $7; - $$ = $1; - } - | relation ':' relation ':' relation - { - RelTupleTriple *rtt = new RelTupleTriple; - rtt->space.append(*$1); - rtt->time.append(*$3); - rtt->ispaces.append(*$5); - delete $1; - delete $3; - delete $5; - $$ = rtt; - } - ; - -blockAndProcsAndEffort : { Block_Size = 0; Num_Procs = 0; overheadEffort=0; } - | INT { Block_Size = $1; Num_Procs = 0; overheadEffort=0;} - | INT INT { Block_Size = $1; Num_Procs = $2; overheadEffort=0;} - | INT INT INT { Block_Size = $1; Num_Procs = $2; overheadEffort=$3;} - ; - -effort : { $$ = 0; } - | INT { $$ = $1; } - | '-' INT { $$ = -$2; } - ; - -context : { $$ = new Relation(); - *$$ = Relation::Null(); } - | GIVEN relation {$$ = $2; } - ; - -relPairList: relPairList ',' relation ':' relation - { - $1->mappings.append(*$3); - $1->mappings[$1->mappings.size()].compress(); - $1->ispaces.append(*$5); - $1->ispaces[$1->ispaces.size()].compress(); - delete $3; - delete $5; - $$ = $1; - } - | relPairList ',' relation - { - $1->mappings.append(Identity($3->n_set())); - $1->mappings[$1->mappings.size()].compress(); - $1->ispaces.append(*$3); - $1->ispaces[$1->ispaces.size()].compress(); - delete $3; - $$ = $1; - } - | relation ':' relation - { - RelTuplePair *rtp = new RelTuplePair; - rtp->mappings.append(*$1); - rtp->mappings[rtp->mappings.size()].compress(); - rtp->ispaces.append(*$3); - rtp->ispaces[rtp->ispaces.size()].compress(); - delete $1; - delete $3; - $$ = rtp; - } - | relation - { - RelTuplePair *rtp = new RelTuplePair; - rtp->mappings.append(Identity($1->n_set())); - rtp->mappings[rtp->mappings.size()].compress(); - rtp->ispaces.append(*$1); - rtp->ispaces[rtp->ispaces.size()].compress(); - delete $1; - $$ = rtp; - } - ; - -statementInfoResult : statementInfoList - { $$ = $1; } -/* | ASSERT_UNSAT statementInfoResult - * { $$ = ($2); - * DoDebug2("Debug info requested in input", *($2)); - * } - */ - | TRANS_IS relation statementInfoResult - { $$ = &Trans_IS(*($3), *($2)); - delete $2; - } - | SET_MMAP INT partialwrites statementInfoResult - { $$ = &Set_MMap(*($4), $2, *($3)); - delete $3; - } - | UNROLL_IS INT INT INT statementInfoResult - { $$ = &Unroll_One_IS(*($5), $2, $3, $4);} - | PEEL_IS INT INT relation statementInfoResult - { $$ = &Peel_One_IS(*($5), $2, $3, *($4)); - delete $4; - } - | PEEL_IS INT INT relation ',' relation statementInfoResult - { $$ = &Peel_One_IS(*($7), $2, $3, *($4), *($6)); - delete $4; - delete $6; - } - ; - -statementInfoList : statementInfo { $$ = new Tuple; - $$->append(*($1)); - delete $1; } - | statementInfoList ',' statementInfo { $$ = $1; - $$->append(*($3)); - delete $3; } - ; - -statementInfo : '[' STRING ',' relation ',' partialwrites ',' reads ']' - { $$ = $8; - $$->stm = *($2); delete $2; - $$->IS = *($4); delete $4; - $$->map = *($6); delete $6; - } - | '[' STRING ',' relation ',' partialwrites ']' - { $$ = new stm_info; - $$->stm = *($2); delete $2; - $$->IS = *($4); delete $4; - $$->map = *($6); delete $6; - } - ; - -partialwrites : partialwrites ',' partialwrite - { $$ = $1; - $$->partials.append(*($3)); delete $3; - } - | partialwrite { $$ = new MMap; - $$->partials.append(*($1)); delete $1; - } - ; - -partialwrite : STRING '[' relation ']' ',' relation - { $$ = new PartialMMap; - $$->mapping = *($6); delete $6; - $$->bounds = *($3); delete $3; - $$->var = *($1); delete $1; - } - | STRING ',' relation { $$ = new PartialMMap; - $$->mapping = *($3); delete $3; - $$->bounds = Relation::True(0); - $$->var = *($1); delete $1; - } - ; - -reads : reads ',' oneread { $$ = $1; - $$->read.append(*($3)); delete $3; - } - | oneread { $$ = new stm_info; - $$->read.append(*($1)); delete $1; - } - ; - -oneread : '[' partials ']' { $$ = $2; } - ; - -partials : partials ',' partial { $$ = $1; - $$->partials.append(*($3)); delete $3; - } - | partial { $$ = new Read; - $$->partials.append(*($1)); delete $1; - } - ; - -partial : INT ',' relation { $$ = new PartialRead; - $$->from = $1; - $$->dataFlow = *($3); delete $3; - } - ; - -globVarList: globVarList ',' globVar - | globVar - ; - -globVar: VAR '(' INT ')' - { globalDecls->extend_both_tuples($1, $3); free($1); } - | VAR - { globalDecls->extend($1); free($1); } - ; - -relation : OPEN_BRACE - { relationDecl = new Declaration_Site(); } - builtRelation - CLOSE_BRACE - { $$ = $3; - if (omega_calc_debug) { - fprintf(DebugFile,"Built relation:\n"); - $$->prefix_print(DebugFile); - }; - current_Declaration_Site = globalDecls; - delete relationDecl; - } - | VAR { - Const_String s = $1; - free($1); - if (relationMap(s) == 0) { - fprintf(stderr,"Variable %s not declared\n",$1); - YYERROR; - assert(0); - }; - $$ = new Relation(*relationMap(s)); - } - | '(' relation ')' {$$ = $2;} - | relation '+' %prec OMEGA_P9 - { $$ = new Relation(); - *$$ = TransitiveClosure(*$1, 1,Relation::Null()); - delete $1; - } - | relation '*' %prec OMEGA_P9 - { $$ = new Relation(); - int vars = $1->n_inp(); - *$$ = Union(Identity(vars), - TransitiveClosure(*$1, 1,Relation::Null())); - delete $1; - } - | relation '+' WITHIN relation %prec OMEGA_P9 - {$$ = new Relation(); - *$$= TransitiveClosure(*$1, 1,*$4); - delete $1; - delete $4; - } - | MINIMIZE_RANGE relation %prec OMEGA_P8 - { - Relation o(*$2); - Relation r(*$2); - r = Join(r,LexForward($2->n_out())); - $$ = new Relation(); - *$$ = Difference(o,r); - delete $2; - } - | MAXIMIZE_RANGE relation %prec OMEGA_P8 - { - Relation o(*$2); - Relation r(*$2); - r = Join(r,Inverse(LexForward($2->n_out()))); - $$ = new Relation(); - *$$ = Difference(o,r); - delete $2; - } - | MINIMIZE_DOMAIN relation %prec OMEGA_P8 - { - Relation o(*$2); - Relation r(*$2); - r = Join(LexForward($2->n_inp()),r); - $$ = new Relation(); - *$$ = Difference(o,r); - delete $2; - } - | MAXIMIZE_DOMAIN relation %prec OMEGA_P8 - { - Relation o(*$2); - Relation r(*$2); - r = Join(Inverse(LexForward($2->n_inp())),r); - $$ = new Relation(); - *$$ = Difference(o,r); - delete $2; - } - | MAXIMIZE relation %prec OMEGA_P8 - { - Relation c(*$2); - Relation r(*$2); - $$ = new Relation(); - *$$ = Cross_Product(Relation(*$2),c); - delete $2; - assert($$->n_inp() ==$$->n_out()); - *$$ = Difference(r,Domain(Intersection(*$$,LexForward($$->n_inp())))); - } - | MINIMIZE relation %prec OMEGA_P8 - { - Relation c(*$2); - Relation r(*$2); - $$ = new Relation(); - *$$ = Cross_Product(Relation(*$2),c); - delete $2; - assert($$->n_inp() ==$$->n_out()); - *$$ = Difference(r,Range(Intersection(*$$,LexForward($$->n_inp())))); - } - | FARKAS relation %prec OMEGA_P8 - { - $$ = new Relation(); - *$$ = Farkas(*$2, Basic_Farkas); - delete $2; - } - | DECOUPLED_FARKAS relation %prec OMEGA_P8 - { - $$ = new Relation(); - *$$ = Farkas(*$2, Decoupled_Farkas); - delete $2; - } - | relation '@' %prec OMEGA_P9 - { $$ = new Relation(); - *$$ = ConicClosure(*$1); - delete $1; - } - | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Project_Sym(*$2); - delete $2; - } - | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Project_On_Sym(*$2); - delete $2; - } - | DIFFERENCE relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Deltas(*$2); - delete $2; - } - | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = DeltasToRelation(*$2,$2->n_set(),$2->n_set()); - delete $2; - } - | DOMAIN relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Domain(*$2); - delete $2; - } - | VENN relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = VennDiagramForm(*$2,Relation::True(*$2)); - delete $2; - } - | VENN relation GIVEN relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = VennDiagramForm(*$2,*$4); - delete $2; - delete $4; - } - | CONVEX_HULL relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = ConvexHull(*$2); - delete $2; - } - | POSITIVE_COMBINATION relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Farkas(*$2,Positive_Combination_Farkas); - delete $2; - } - | CONVEX_COMBINATION relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Farkas(*$2,Convex_Combination_Farkas); - delete $2; - } - | PAIRWISE_CHECK relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = CheckForConvexRepresentation(CheckForConvexPairs(*$2)); - delete $2; - } - | CONVEX_CHECK relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = CheckForConvexRepresentation(*$2); - delete $2; - } - | AFFINE_HULL relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = AffineHull(*$2); - delete $2; - } - | CONIC_HULL relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = ConicHull(*$2); - delete $2; - } - | LINEAR_HULL relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = LinearHull(*$2); - delete $2; - } - | HULL relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Hull(*$2,false,1,Null_Relation()); - delete $2; - } - | HULL relation GIVEN relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Hull(*$2,false,1,*$4); - delete $2; - delete $4; - } - | APPROX relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Approximate(*$2); - delete $2; - } - | RANGE relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Range(*$2); - delete $2; - } - | INVERSE relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Inverse(*$2); - delete $2; - } - | COMPLEMENT relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Complement(*$2); - delete $2; - } - | GIST relation GIVEN relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Gist(*$2,*$4,1); - delete $2; - delete $4; - } - | relation '(' relation ')' - { $$ = new Relation(); - *$$ = Composition(*$1,*$3); - delete $1; - delete $3; - } - | relation COMPOSE relation - { $$ = new Relation(); - *$$ = Composition(*$1,*$3); - delete $1; - delete $3; - } - | relation CARRIED_BY INT - { $$ = new Relation(); - *$$ = After(*$1,$3,$3); - delete $1; - (*$$).prefix_print(stdout); - } - | relation JOIN relation - { $$ = new Relation(); - *$$ = Composition(*$3,*$1); - delete $1; - delete $3; - } - | relation RESTRICT_RANGE relation - { $$ = new Relation(); - *$$ = Restrict_Range(*$1,*$3); - delete $1; - delete $3; - } - | relation RESTRICT_DOMAIN relation - { $$ = new Relation(); - *$$ = Restrict_Domain(*$1,*$3); - delete $1; - delete $3; - } - | relation INTERSECTION relation - { $$ = new Relation(); - *$$ = Intersection(*$1,*$3); - delete $1; - delete $3; - } - | relation '-' relation %prec INTERSECTION - { $$ = new Relation(); - *$$ = Difference(*$1,*$3); - delete $1; - delete $3; - } - | relation UNION relation - { $$ = new Relation(); - *$$ = Union(*$1,*$3); - delete $1; - delete $3; - } - | relation '*' relation - { $$ = new Relation(); - *$$ = Cross_Product(*$1,*$3); - delete $1; - delete $3; - } - | SUPERSETOF relation - { $$ = new Relation(); - *$$ = Union(*$2, Relation::Unknown(*$2)); - delete $2; - } - | SUBSETOF relation - { $$ = new Relation(); - *$$ = Intersection(*$2, Relation::Unknown(*$2)); - delete $2; - } - | MAKE_UPPER_BOUND relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Upper_Bound(*$2); - delete $2; - } - | MAKE_LOWER_BOUND relation %prec OMEGA_P8 - { $$ = new Relation(); - *$$ = Lower_Bound(*$2); - delete $2; - } - | SAMPLE relation - { $$ = new Relation(); - *$$ = Sample_Solution(*$2); - delete $2; - } - | SYM_SAMPLE relation - { $$ = new Relation(); - *$$ = Symbolic_Solution(*$2); - delete $2; - } - | reachable_of { $$ = $1; } - | ASSERT_UNSAT relation - { - if (($2)->is_satisfiable()) - { - fprintf(stderr,"assert_unsatisfiable failed on "); - ($2)->print_with_subs(stderr); - Exit(1); - } - $$=$2; - } - - ; - -builtRelation : - tupleDeclaration GOES_TO {currentTuple = Output_Tuple;} - tupleDeclaration {currentTuple = Input_Tuple;} optionalFormula { - Relation * r = new Relation($1->size,$4->size); - resetGlobals(); - F_And *f = r->add_and(); - int i; - for(i=1;i<=$1->size;i++) { - $1->vars[i]->vid = r->input_var(i); - if (!$1->vars[i]->anonymous) - r->name_input_var(i,$1->vars[i]->stripped_name); - }; - for(i=1;i<=$4->size;i++) { - $4->vars[i]->vid = r->output_var(i); - if (!$4->vars[i]->anonymous) - r->name_output_var(i,$4->vars[i]->stripped_name); - }; - foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0)); - foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0)); - foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c)); - foreach(e,Exp*,$4->eq_constraints, install_eq(f,e,0)); - foreach(e,Exp*,$4->geq_constraints, install_geq(f,e,0)); - foreach(c,strideConstraint*,$4->stride_constraints, install_stride(f,c)); - if ($6) $6->install(f); - delete $1; - delete $4; - delete $6; - $$ = r; } - | tupleDeclaration optionalFormula { - Relation * r = new Relation($1->size); - resetGlobals(); - F_And *f = r->add_and(); - int i; - for(i=1;i<=$1->size;i++) { - $1->vars[i]->vid = r->set_var(i); - if (!$1->vars[i]->anonymous) - r->name_set_var(i,$1->vars[i]->stripped_name); - }; - foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0)); - foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0)); - foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c)); - if ($2) $2->install(f); - delete $1; - delete $2; - $$ = r; } - | formula { - Relation * r = new Relation(0,0); - F_And *f = r->add_and(); - $1->install(f); - delete $1; - $$ = r; - } - ; - -optionalFormula : formula_sep formula { $$ = $2; } - | {$$ = 0;} - ; - -formula_sep : ':' - | VERTICAL_BAR - | SUCH_THAT - ; - -tupleDeclaration : - { currentTupleDescriptor = new tupleDescriptor; tuplePos = 1; } - '[' optionalTupleVarList ']' - {$$ = currentTupleDescriptor; } - ; - -optionalTupleVarList : - tupleVar - | optionalTupleVarList ',' tupleVar - | - ; - -tupleVar : VAR %prec OMEGA_P10 - { Declaration_Site *ds = defined($1); - if (!ds) currentTupleDescriptor->extend($1,currentTuple,tuplePos); - else { - Variable_Ref * v = lookupScalar($1); - assert(v); - if (ds != globalDecls) - currentTupleDescriptor->extend($1, new Exp(v)); - else - currentTupleDescriptor->extend(new Exp(v)); - } - free($1); - tuplePos++; - } - | '*' - {currentTupleDescriptor->extend(); tuplePos++; } - | exp %prec OMEGA_P1 - {currentTupleDescriptor->extend($1); tuplePos++; } - | exp ':' exp %prec OMEGA_P1 - {currentTupleDescriptor->extend($1,$3); tuplePos++; } - | exp ':' exp ':' INT %prec OMEGA_P1 - {currentTupleDescriptor->extend($1,$3,$5); tuplePos++; } - ; - - -varList: varList ',' VAR {$$ = $1; $$->insert($3); } - | VAR { $$ = new VarList; - $$->insert($1); } - ; - -varDecl : varList - { - $$ = current_Declaration_Site = new Declaration_Site($1); - foreach(s,char *, *$1, delete s); - delete $1; - } - ; - -/* variable declaration with optional brackets */ - -varDeclOptBrackets : varDecl { $$ = $1; } - | '[' varDecl ']' { $$ = $2; } - ; - -formula : formula AND formula { $$ = new AST_And($1,$3); } - | formula OR formula { $$ = new AST_Or($1,$3); } - | constraintChain { $$ = $1; } - | '(' formula ')' { $$ = $2; } - | NOT formula { $$ = new AST_Not($2); } - | start_exists varDeclOptBrackets exists_sep formula end_quant - { $$ = new AST_exists($2,$4); } - | start_forall varDeclOptBrackets forall_sep formula end_quant - { $$ = new AST_forall($2,$4); } - ; - -start_exists : '(' EXISTS - | EXISTS '(' - ; - -exists_sep : ':' - | VERTICAL_BAR - | SUCH_THAT - ; - -start_forall : '(' FORALL - | FORALL '(' - ; - -forall_sep : ':' - ; - -end_quant : ')' - { popScope(); } - ; - -expList : exp ',' expList - { - $$ = $3; - $$->insert($1); - } - | exp { - $$ = new ExpList; - $$->insert($1); - } - ; - -constraintChain : expList REL_OP expList - { $$ = new AST_constraints($1,$2,$3); } - | expList REL_OP constraintChain - { $$ = new AST_constraints($1,$2,$3); } - ; - -simpleExp : - VAR %prec OMEGA_P9 - { Variable_Ref * v = lookupScalar($1); - if (!v) YYERROR; - $$ = new Exp(v); - free($1); - } - | VAR '(' {argCount = 1;} argumentList ')' %prec OMEGA_P9 - {Variable_Ref *v; - if ($4 == Input_Tuple) v = functionOfInput[$1]; - else v = functionOfOutput[$1]; - free($1); - if (v == 0) { - fprintf(stderr,"Function %s(...) not declared\n",$1); - YYERROR; - } - $$ = new Exp(v); - } - | '(' exp ')' { $$ = $2;} - ; - - - -argumentList : - argumentList ',' VAR { - Variable_Ref * v = lookupScalar($3); - if (!v) YYERROR; - free($3); - if (v->pos != argCount || v->of != $1 || v->of != Input_Tuple && v->of != Output_Tuple) { - fprintf(stderr,"arguments to function must be prefix of input or output tuple\n"); - YYERROR; - } - $$ = v->of; - argCount++; - } - | VAR { Variable_Ref * v = lookupScalar($1); - if (!v) YYERROR; - free($1); - if (v->pos != argCount || v->of != Input_Tuple && v->of != Output_Tuple) { - fprintf(stderr,"arguments to function must be prefix of input or output tuple\n"); - YYERROR; - } - $$ = v->of; - argCount++; - } - ; - -exp : INT {$$ = new Exp($1);} - | INT simpleExp %prec '*' {$$ = multiply($1,$2);} - | simpleExp { $$ = $1; } - | '-' exp %prec '*' { $$ = negate($2);} - | exp '+' exp { $$ = add($1,$3);} - | exp '-' exp { $$ = subtract($1,$3);} - | exp '*' exp { $$ = multiply($1,$3);} - ; - - -reachable : - REACHABLE_FROM nodeNameList nodeSpecificationList - { - Dynamic_Array1 *final = - Reachable_Nodes(reachable_info); - $$ = final; - } - ; - -reachable_of : - REACHABLE_OF VAR IN nodeNameList nodeSpecificationList - { - Dynamic_Array1 *final = - Reachable_Nodes(reachable_info); - int index = reachable_info->node_names.index(String($2)); - assert(index != 0 && "No such node"); - $$ = new Relation; - *$$ = (*final)[index]; - delete final; - delete reachable_info; - delete $2; - } - ; - - -nodeNameList: '(' realNodeNameList ')' - { int sz = reachable_info->node_names.size(); - reachable_info->node_arity.reallocate(sz); - reachable_info->transitions.resize(sz+1,sz+1); - reachable_info->start_nodes.resize(sz+1); - } - ; - -realNodeNameList: realNodeNameList ',' VAR - { reachable_info->node_names.append(String($3)); - delete $3; } - | VAR { reachable_info = new reachable_information; - reachable_info->node_names.append(String($1)); - delete $1; } - ; - - -nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE - { - int i,j; - int n_nodes = reachable_info->node_names.size(); - Tuple &arity = reachable_info->node_arity; - Dynamic_Array2 &transitions = reachable_info->transitions; - - /* fixup unspecified transitions to be false */ - /* find arity */ - for(i = 1; i <= n_nodes; i++) arity[i] = -1; - for(i = 1; i <= n_nodes; i++) - for(j = 1; j <= n_nodes; j++) - if(! transitions[i][j].is_null()) { - int in_arity = transitions[i][j].n_inp(); - int out_arity = transitions[i][j].n_out(); - if(arity[i] < 0) arity[i] = in_arity; - if(arity[j] < 0) arity[j] = out_arity; - if(in_arity != arity[i] || out_arity != arity[j]) { - fprintf(stderr, - "Arity mismatch in node transition: %s -> %s", - (const char *) reachable_info->node_names[i], - (const char *) reachable_info->node_names[j]); - assert(0); - YYERROR; - } - } - for(i = 1; i <= n_nodes; i++) - if(arity[i] < 0) arity[i] = 0; - /* Fill in false relations */ - for(i = 1; i <= n_nodes; i++) - for(j = 1; j <= n_nodes; j++) - if(transitions[i][j].is_null()) - transitions[i][j] = Relation::False(arity[i],arity[j]); - - - /* fixup unused start node positions */ - Dynamic_Array1 &nodes = reachable_info->start_nodes; - for(i = 1; i <= n_nodes; i++) - if(nodes[i].is_null()) - nodes[i] = Relation::False(arity[i]); - else - if(nodes[i].n_set() != arity[i]){ - fprintf(stderr,"Arity mismatch in start node %s", - (const char *) reachable_info->node_names[i]); - assert(0); - YYERROR; - } - } - ; - -realNodeSpecificationList: - realNodeSpecificationList ',' VAR ':' relation - { int n_nodes = reachable_info->node_names.size(); - int index = reachable_info->node_names.index($3); - assert(index != 0 && index <= n_nodes); - reachable_info->start_nodes[index] = *$5; - delete $3; - delete $5; - } - | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation - { int n_nodes = reachable_info->node_names.size(); - int from_index = reachable_info->node_names.index($3); - int to_index = reachable_info->node_names.index($5); - assert(from_index != 0 && to_index != 0); - assert(from_index <= n_nodes && to_index <= n_nodes); - reachable_info->transitions[from_index][to_index] = *$7; - delete $3; - delete $5; - delete $7; - } - | VAR GOES_TO VAR ':' relation - { int n_nodes = reachable_info->node_names.size(); - int from_index = reachable_info->node_names.index($1); - int to_index = reachable_info->node_names.index($3); - assert(from_index != 0 && to_index != 0); - assert(from_index <= n_nodes && to_index <= n_nodes); - reachable_info->transitions[from_index][to_index] = *$5; - delete $1; - delete $3; - delete $5; - } - | VAR ':' relation - { int n_nodes = reachable_info->node_names.size(); - int index = reachable_info->node_names.index($1); - assert(index != 0 && index <= n_nodes); - reachable_info->start_nodes[index] = *$3; - delete $1; - delete $3; - } - ; - -%% - -#if !defined(OMIT_GETRUSAGE) -#include -#include -#include - -struct rusage start_time; -#endif - -#if defined BRAIN_DAMAGED_FREE -void free(void *p) - { - free((char *)p); - } - -void *realloc(void *p, size_t s) - { - return realloc((malloc_t) p, s); - } -#endif - -#if ! defined(OMIT_GETRUSAGE) -#ifdef __sparc__ -extern "C" int getrusage (int, struct rusage*); -#endif - -void start_clock( void ) - { - getrusage(RUSAGE_SELF, &start_time); - } - -int clock_diff( void ) - { - struct rusage current_time; - getrusage(RUSAGE_SELF, ¤t_time); - return (current_time.ru_utime.tv_sec -start_time.ru_utime.tv_sec)*1000000 + - (current_time.ru_utime.tv_usec-start_time.ru_utime.tv_usec); - } -#endif - -void printUsage(FILE *outf, char **argv) { - 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); -} - -int omega_calc_debug; -extern FILE *yyin; - -int main(int argc, char **argv){ - redundant_conj_level = 2; - current_Declaration_Site = globalDecls = new Global_Declaration_Site(); -#if YYDEBUG != 0 - yydebug = 1; -#endif - int i; - char * fileName = 0; - - printf("# %s (based on %s, %s):\n",CALC_VERSION_STRING, Omega_Library_Version, Omega_Library_Date); - - calc_all_debugging_off(); - -#ifdef SPEED - DebugFile = fopen("/dev/null","w"); - assert(DebugFile); -#else - DebugFile = fopen(DEBUG_FILE_NAME, "w"); - if (!DebugFile) { - fprintf(stderr, "Can't open debug file %s\n", DEBUG_FILE_NAME); - DebugFile = stderr; - } - setbuf(DebugFile,0); -#endif - - closure_presburger_debug = 0; - - setOutputFile(DebugFile); - - // Process flags - for(i=1; iadd_and(); - for(int j=1;jadd_EQ(); - e.update_coef(r.input_var(j),-1); - e.update_coef(r.output_var(j),1); - e.finalize(); - } - GEQ_Handle e = g->add_GEQ(); - e.update_coef(r.input_var(i),-1); - e.update_coef(r.output_var(i),1); - e.update_const(-1); - e.finalize(); - } - r.finalize(); - return r; - } - - -- 2.11.4.GIT