summaryrefslogtreecommitdiff
path: root/omegalib/omegacalc/src/parser.y
diff options
context:
space:
mode:
Diffstat (limited to 'omegalib/omegacalc/src/parser.y')
-rw-r--r--omegalib/omegacalc/src/parser.y1925
1 files changed, 0 insertions, 1925 deletions
diff --git a/omegalib/omegacalc/src/parser.y b/omegalib/omegacalc/src/parser.y
deleted file mode 100644
index d365797..0000000
--- a/omegalib/omegacalc/src/parser.y
+++ /dev/null
@@ -1,1925 +0,0 @@
-/*****************************************************************************
- Copyright (C) 1994-2000 University of Maryland.
- Copyright (C) 2008 University of Southern California.
- Copyright (C) 2009-2010 University of Utah.
- All Rights Reserved.
-
- Purpose:
- omega calculator yacc parser.
-
- Notes:
-
- History:
-*****************************************************************************/
-
-%{
-
-#include <basic/DynamicArray.h>
-#include <basic/Iterator.h>
-#include <code_gen/code_gen.h>
-#include <omega_calc/AST.h>
-#include <omega/hull.h>
-#include <omega/closure.h>
-#include <omega/reach.h>
-#include <string>
-#include <iostream>
-
-#ifdef WIN32
-#include <io.h>
-#define isatty _isatty
-#define alloca _alloca
-#endif
-#ifndef WIN32
-#include <sys/time.h>
-#include <sys/resource.h>
-#endif
-#if !defined(OMIT_GETRUSAGE)
-#include <sys/types.h>
-#include <sys/time.h>
-#include <sys/resource.h>
-#endif
-
-#if !defined(OMIT_GETRUSAGE)
-#ifdef __sparc__
-extern "C" int getrusage (int, struct rusage*);
-#endif
-
-using namespace omega;
-
-struct rusage start_time;
-bool anyTimingDone = false;
-
-void start_clock( void ) {
- getrusage(RUSAGE_SELF, &start_time);
-}
-
-int clock_diff( void ) {
- struct rusage current_time;
- getrusage(RUSAGE_SELF, &current_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
-
-int omega_calc_debug = 0;
-
-bool is_interactive;
-const char *PROMPT_STRING = ">>>";
-extern std::string err_msg;
-extern FILE *yyin;
-bool need_coef;
-
-Map<Const_String,Relation*> relationMap ((Relation *)0);
-namespace {
- int redundant_conj_level = 2; // default maximum 2
- int redundant_constr_level = 4; // default maximum 4
-}
-
-int argCount = 0;
-int tuplePos = 0;
-Argument_Tuple currentTuple = Input_Tuple;
-
-Relation LexForward(int n);
-reachable_information *reachable_info;
-
-int yylex();
-void yyerror(const std::string &s);
-void flushScanBuffer();
-
-%}
-
-%union {
- int INT_VALUE;
- coef_t COEF_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;
- DynamicArray2<Relation> * RELATION_ARRAY_2D;
- DynamicArray1<Relation> * RELATION_ARRAY_1D;
- Tuple<std::string> *STRING_TUPLE;
- std::string *STRING_VALUE;
-}
-
-%token <VAR_NAME> VAR
-%token <INT_VALUE> INT
-%token <COEF_VALUE> COEF
-%token <STRING_VALUE> 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 LINEAR_COMBINATION AFFINE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL QUICK_HULL PAIRWISE_CHECK CONVEX_CHECK CONVEX_REPRESENTATION RECT_HULL DECOUPLED_CONVEX_HULL
-%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 CODEGEN DECOUPLED_FARKAS FARKAS
-%token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
-%token <REL_OPERATOR> 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 PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
-
-%type <INT_VALUE> effort
-%type <EXP> exp simpleExp
-%type <EXP_LIST> expList
-%type <VAR_LIST> varList
-%type <ARGUMENT_TUPLE> argumentList
-%type <ASTP> formula optionalFormula
-%type <ASTCP> constraintChain
-%type <TUPLE_DESCRIPTOR> tupleDeclaration
-%type <DECLARATION_SITE> varDecl varDeclOptBrackets
-%type <RELATION> relation builtRelation context
-%type <RELATION> reachable_of
-%type <REL_TUPLE_PAIR> relPairList
-%type <RELATION_ARRAY_1D> reachable
-
-%destructor {delete []$$;} VAR
-%destructor {delete $$;} STRING
-%destructor {delete $$;} relation builtRelation tupleDeclaration formula optionalFormula context reachable_of constraintChain varDecl varDeclOptBrackets relPairList reachable
-%destructor {delete $$;} varList exp simpleExp
-%destructor {
- foreach(e, Exp *, *$$, delete e);
- delete $$;
- } expList;
-
-%nonassoc ASSERT_UNSAT
-%left UNION p1 '+' '-'
-%nonassoc SUPERSETOF SUBSETOF
-%left p2 RESTRICT_DOMAIN RESTRICT_RANGE
-%left INTERSECTION p3 '*' '@'
-%left p4
-%left OR p5
-%left AND 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 p7
-%left p8
-%nonassoc GIVEN
-%left p9
-%left '(' p10
-
-%%
-
-inputSequence : /*empty*/
- | inputSequence { assert( current_Declaration_Site == globalDecls);}
- inputItem
-;
-
-inputItem : ';' /*empty*/
- | error ';' {
- flushScanBuffer();
- std::cout << err_msg;
- err_msg.clear();
- current_Declaration_Site = globalDecls;
- need_coef = false;
- std::cout << "...skipping to statement end..." << std::endl;
- delete relationDecl;
- relationDecl = NULL;
- }
- | SYMBOLIC globVarList ';' {flushScanBuffer();}
- | VAR IS_ASSIGNED relation ';' {
- flushScanBuffer();
- try {
- $3->simplify(redundant_conj_level, redundant_constr_level);
- Relation *r = relationMap((Const_String)$1);
- if (r) delete r;
- relationMap[(Const_String)$1] = $3;
- }
- catch (const std::exception &e) {
- std::cout << e.what() << std::endl;
- }
- delete []$1;
- }
- | relation ';' {
- flushScanBuffer();
- $1->simplify(redundant_conj_level, redundant_constr_level);
- $1->print_with_subs(stdout);
- 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(); /* default simplification effort */
- }
- 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); /* maximal simplification effort */
- }
- }
- 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();
- try {
- 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;
- }
- catch (const std::exception &e) {
- std::cout << e.what() << std::endl;
- }
- delete $2;
-#endif
- }
- | relation SUBSET relation ';' {
- flushScanBuffer();
- try {
- if (Must_Be_Subset(copy(*$1), copy(*$3)))
- std::cout << "True" << std::endl;
- else if (Might_Be_Subset(copy(*$1), copy(*$3)))
- std::cout << "Possible" << std::endl;
- else
- std::cout << "False" << std::endl;
- }
- catch (const std::exception &e) {
- std::cout << e.what() << std::endl;
- }
- delete $1;
- delete $3;
- }
- | CODEGEN effort relPairList context';' {
- flushScanBuffer();
- try {
- std::string s = MMGenerateCode($3->mappings, $3->ispaces,*$4,$2);
- std::cout << s << std::endl;
- }
- catch (const std::exception &e) {
- std::cout << e.what() << std::endl;
- }
- delete $4;
- delete $3;
- }
- | reachable ';' {
- flushScanBuffer();
- DynamicArray1<Relation> &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;
- std::cout << "Node %s: " << reachable_info->node_names[i];
- final[i].print_with_subs(stdout);
- }
- if(!any_sat)
- std::cout << "No nodes reachable.\n";
- delete $1;
- delete reachable_info;
- }
-;
-
-
-effort : {$$ = 1;}
- | INT {$$ = $1;}
- | '-' INT {$$ = -$2;}
-;
-
-context : {$$ = new Relation(); *$$ = Relation::Null();}
- | GIVEN relation {$$ = $2; }
-;
-
-relPairList : relPairList ',' relation ':' relation {
- try {
- $1->mappings.append(*$3);
- $1->mappings[$1->mappings.size()].compress();
- $1->ispaces.append(*$5);
- $1->ispaces[$1->ispaces.size()].compress();
- }
- catch (const std::exception &e) {
- delete $1;
- delete $3;
- delete $5;
- yyerror(e.what());
- YYERROR;
- }
- delete $3;
- delete $5;
- $$ = $1;
- }
- | relPairList ',' relation {
- try {
- $1->mappings.append(Identity($3->n_set()));
- $1->mappings[$1->mappings.size()].compress();
- $1->ispaces.append(*$3);
- $1->ispaces[$1->ispaces.size()].compress();
- }
- catch (const std::exception &e) {
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $3;
- $$ = $1;
- }
- | relation ':' relation {
- RelTuplePair *rtp = new RelTuplePair;
- try {
- rtp->mappings.append(*$1);
- rtp->mappings[rtp->mappings.size()].compress();
- rtp->ispaces.append(*$3);
- rtp->ispaces[rtp->ispaces.size()].compress();
- }
- catch (const std::exception &e) {
- delete rtp;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- $$ = rtp;
- }
- | relation {
- RelTuplePair *rtp = new RelTuplePair;
- try {
- rtp->mappings.append(Identity($1->n_set()));
- rtp->mappings[rtp->mappings.size()].compress();
- rtp->ispaces.append(*$1);
- rtp->ispaces[rtp->ispaces.size()].compress();
- }
- catch (const std::exception &e) {
- delete rtp;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- $$ = rtp;
- }
-;
-
-relation : OPEN_BRACE {need_coef = true; relationDecl = new Declaration_Site();}
- builtRelation CLOSE_BRACE {
- need_coef = false;
- $$ = $3;
- if (omega_calc_debug) {
- fprintf(DebugFile,"Built relation:\n");
- $$->prefix_print(DebugFile);
- }
- current_Declaration_Site = globalDecls;
- delete relationDecl;
- relationDecl = NULL;
- }
- | VAR {
- Const_String s = $1;
- Relation *r = relationMap(s);
- if (r == NULL) {
- yyerror(std::string("relation ") + to_string($1) + std::string(" not declared"));
- delete []$1;
- YYERROR;
- }
- $$ = new Relation(*r);
- delete []$1;
- }
- | '(' relation ')' {$$ = $2;}
- | relation '+' %prec p9 {
- $$ = new Relation();
- try {
- *$$ = TransitiveClosure(*$1, 1, Relation::Null());
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- }
- | relation '*' %prec p9 {
- $$ = new Relation();
- try {
- int vars = $1->n_inp();
- *$$ = Union(Identity(vars), TransitiveClosure(*$1, 1, Relation::Null()));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- }
- | relation '+' WITHIN relation %prec p9 {
- $$ = new Relation();
- try {
- *$$= TransitiveClosure(*$1, 1, *$4);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $4;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $4;
- }
- | relation '^' '@' %prec p8 {
- $$ = new Relation();
- try {
- *$$ = ApproxClosure(*$1);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- }
- | relation '^' '+' %prec p8 {
- $$ = new Relation();
- try {
- *$$ = calculateTransitiveClosure(*$1);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- }
- | MINIMIZE_RANGE relation %prec p8 {
- $$ = new Relation();
- try {
- Relation o(*$2);
- Relation r(*$2);
- r = Join(r,LexForward($2->n_out()));
- *$$ = Difference(o,r);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MAXIMIZE_RANGE relation %prec p8 {
- $$ = new Relation();
- try {
- Relation o(*$2);
- Relation r(*$2);
- r = Join(r,Inverse(LexForward($2->n_out())));
- *$$ = Difference(o,r);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MINIMIZE_DOMAIN relation %prec p8 {
- $$ = new Relation();
- try {
- Relation o(*$2);
- Relation r(*$2);
- r = Join(LexForward($2->n_inp()),r);
- *$$ = Difference(o,r);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MAXIMIZE_DOMAIN relation %prec p8 {
- $$ = new Relation();
- try {
- Relation o(*$2);
- Relation r(*$2);
- r = Join(Inverse(LexForward($2->n_inp())),r);
- *$$ = Difference(o,r);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MAXIMIZE relation %prec p8 {
- $$ = new Relation();
- try {
- Relation c(*$2);
- Relation r(*$2);
- *$$ = Cross_Product(Relation(*$2),c);
- *$$ = Difference(r,Domain(Intersection(*$$,LexForward($$->n_inp()))));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MINIMIZE relation %prec p8 {
- $$ = new Relation();
- try {
- Relation c(*$2);
- Relation r(*$2);
- *$$ = Cross_Product(Relation(*$2),c);
- *$$ = Difference(r,Range(Intersection(*$$,LexForward($$->n_inp()))));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | FARKAS relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Farkas(*$2, Basic_Farkas);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | DECOUPLED_FARKAS relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Farkas(*$2, Decoupled_Farkas);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | relation '@' %prec p9 {
- $$ = new Relation();
- try {
- *$$ = ConicClosure(*$1);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- }
- | PROJECT_AWAY_SYMBOLS relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Project_Sym(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | PROJECT_ON_SYMBOLS relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Project_On_Sym(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | DIFFERENCE relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Deltas(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | DIFFERENCE_TO_RELATION relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = DeltasToRelation(*$2,$2->n_set(),$2->n_set());
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | DOMAIN relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Domain(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | VENN relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = VennDiagramForm(*$2,Relation::True(*$2));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | VENN relation GIVEN relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = VennDiagramForm(*$2,*$4);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- delete $4;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- delete $4;
- }
- | CONVEX_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = ConvexHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | DECOUPLED_CONVEX_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = DecoupledConvexHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | POSITIVE_COMBINATION relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Farkas(*$2,Positive_Combination_Farkas);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | LINEAR_COMBINATION relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Farkas(*$2,Linear_Combination_Farkas);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | AFFINE_COMBINATION relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Farkas(*$2,Affine_Combination_Farkas);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | CONVEX_COMBINATION relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Farkas(*$2,Convex_Combination_Farkas);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | PAIRWISE_CHECK relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = CheckForConvexRepresentation(CheckForConvexPairs(*$2));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | CONVEX_CHECK relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = CheckForConvexRepresentation(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | CONVEX_REPRESENTATION relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = ConvexRepresentation(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | AFFINE_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = AffineHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | CONIC_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = ConicHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | LINEAR_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = LinearHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | QUICK_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = QuickHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | RECT_HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = RectHull(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | HULL relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Hull(*$2,false,1,Relation::Null());
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | HULL relation GIVEN relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Hull(*$2,false,1,*$4);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- delete $4;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- delete $4;
- }
- | APPROX relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Approximate(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | RANGE relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Range(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | INVERSE relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Inverse(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | COMPLEMENT relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Complement(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | GIST relation GIVEN relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Gist(*$2,*$4,1);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- delete $4;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- delete $4;
- }
- | relation '(' relation ')' {
- $$ = new Relation();
- try {
- *$$ = Composition(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation COMPOSE relation {
- $$ = new Relation();
- try {
- *$$ = Composition(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation CARRIED_BY INT {
- $$ = new Relation();
- try {
- *$$ = After(*$1,$3,$3);
- (*$$).prefix_print(stdout);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- }
- | relation JOIN relation {
- $$ = new Relation();
- try {
- *$$ = Composition(*$3,*$1);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation RESTRICT_RANGE relation {
- $$ = new Relation();
- try {
- *$$ = Restrict_Range(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation RESTRICT_DOMAIN relation {
- $$ = new Relation();
- try {
- *$$ = Restrict_Domain(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation INTERSECTION relation {
- $$ = new Relation();
- try {
- *$$ = Intersection(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation '-' relation %prec INTERSECTION {
- $$ = new Relation();
- try {
- *$$ = Difference(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation UNION relation {
- $$ = new Relation();
- try {
- *$$ = Union(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | relation '*' relation {
- $$ = new Relation();
- try {
- *$$ = Cross_Product(*$1,*$3);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $1;
- delete $3;
- yyerror(e.what());
- YYERROR;
- }
- delete $1;
- delete $3;
- }
- | SUPERSETOF relation {
- $$ = new Relation();
- try {
- *$$ = Union(*$2, Relation::Unknown(*$2));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | SUBSETOF relation {
- $$ = new Relation();
- try {
- *$$ = Intersection(*$2, Relation::Unknown(*$2));
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MAKE_UPPER_BOUND relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Upper_Bound(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | MAKE_LOWER_BOUND relation %prec p8 {
- $$ = new Relation();
- try {
- *$$ = Lower_Bound(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | SAMPLE relation {
- $$ = new Relation();
- try {
- *$$ = Sample_Solution(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- delete $2;
- }
- | SYM_SAMPLE relation {
- $$ = new Relation();
- try {
- *$$ = Symbolic_Solution(*$2);
- }
- catch (const std::exception &e) {
- delete $$;
- delete $2;
- yyerror(e.what());
- YYERROR;
- }
- 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();
- for(int 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(int 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);
- }
- r->setup_names();
- 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();
- for(int 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);
- }
- r->setup_names();
- 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; tuplePos = 0;}
-;
-
-optionalTupleVarList : /* empty */
- | tupleVar
- | optionalTupleVarList ',' tupleVar
-;
-
-tupleVar : VAR %prec p10 {
- Declaration_Site *ds = defined($1);
- if (!ds)
- currentTupleDescriptor->extend($1,currentTuple,tuplePos);
- else {
- Variable_Ref *v = lookupScalar($1);
- if (v == NULL) {
- yyerror(std::string("cannot find declaration for variable ") + to_string($1));
- delete []$1;
- YYERROR;
- }
- if (ds != globalDecls)
- currentTupleDescriptor->extend($1, new Exp(v));
- else
- currentTupleDescriptor->extend(new Exp(v));
- }
- tuplePos++;
- delete []$1;
- }
- | '*' {currentTupleDescriptor->extend(); tuplePos++;}
- | exp %prec p1 {
- currentTupleDescriptor->extend($1);
- tuplePos++;
- }
- | exp ':' exp %prec p1 {
- currentTupleDescriptor->extend($1,$3);
- tuplePos++;
- }
- | exp ':' exp ':' COEF %prec p1 {
- currentTupleDescriptor->extend($1,$3,$5);
- tuplePos++;
- }
-;
-
-varList : varList ',' VAR {$$ = $1; $$->insert($3); $3 = NULL;}
- | VAR {$$ = new VarList; $$->insert($1); $1 = NULL;}
-;
-
-varDecl : varList {
- $$ = current_Declaration_Site = new Declaration_Site($1);
- foreach(s,char *, *$1, delete []s);
- delete $1;
- }
-;
-
-varDeclOptBrackets : varDecl {$$ = $1;}
- |'[' varDecl ']' {$$ = $2;}
-;
-
-globVarList : globVarList ',' globVar
- | globVar
-;
-
-globVar : VAR '(' INT ')' {globalDecls->extend_both_tuples($1, $3); delete []$1;}
- | VAR {
- globalDecls->extend($1);
- delete []$1;
- }
-;
-
-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 p9 {
- Variable_Ref *v = lookupScalar($1);
- if (v == NULL) {
- yyerror(std::string("cannot find declaration for variable ") + to_string($1));
- delete []$1;
- YYERROR;
- }
- $$ = new Exp(v);
- delete []$1;
- }
- | VAR '(' {argCount = 1;} argumentList ')' %prec p9 {
- Variable_Ref *v;
- if ($4 == Input_Tuple)
- v = functionOfInput[$1];
- else
- v = functionOfOutput[$1];
- if (v == NULL) {
- yyerror(std::string("Function ") + to_string($1) + std::string(" not declared"));
- delete []$1;
- YYERROR;
- }
- $$ = new Exp(v);
- delete []$1;
- }
- | '(' exp ')' { $$ = $2; }
-;
-
-argumentList : argumentList ',' VAR {
- Variable_Ref *v = lookupScalar($3);
- if (v == NULL) {
- yyerror(std::string("cannot find declaration for variable ") + to_string($1));
- delete []$3;
- YYERROR;
- }
- if (v->pos != argCount || v->of != $1 || (v->of != Input_Tuple && v->of != Output_Tuple)) {
- yyerror("arguments to function must be prefix of input or output tuple");
- delete []$3;
- YYERROR;
- }
- $$ = v->of;
- argCount++;
- delete []$3;
- }
- | VAR {
- Variable_Ref *v = lookupScalar($1);
- if (v == NULL) {
- yyerror(std::string("cannot find declaration for variable ") + to_string($1));
- delete []$1;
- YYERROR;
- }
- if (v->pos != argCount || (v->of != Input_Tuple && v->of != Output_Tuple)) {
- yyerror("arguments to function must be prefix of input or output tuple");
- delete []$1;
- YYERROR;
- }
- $$ = v->of;
- argCount++;
- delete []$1;
- }
-;
-
-exp : COEF {$$ = new Exp($1);}
- | COEF 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 {
- DynamicArray1<Relation> *final = Reachable_Nodes(reachable_info);
- $$ = final;
- }
-;
-
-reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList {
- DynamicArray1<Relation> *final = Reachable_Nodes(reachable_info);
- int index = reachable_info->node_names.index(std::string($2));
- if (index == 0) {
- yyerror(std::string("no such node ") + to_string($2));
- delete []$2;
- delete final;
- delete reachable_info;
- YYERROR;
- }
- $$ = 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(std::string($3));
- delete []$3;
- }
- | VAR {
- reachable_info = new reachable_information;
- reachable_info->node_names.append(std::string($1));
- delete []$1;
- }
-;
-
-
-nodeSpecificationList : OPEN_BRACE realNodeSpecificationList CLOSE_BRACE {
- int i,j;
- int n_nodes = reachable_info->node_names.size();
- Tuple<int> &arity = reachable_info->node_arity;
- DynamicArray2<Relation> &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]) {
- yyerror(std::string("arity mismatch in node transition: ") + to_string(reachable_info->node_names[i]) + std::string(" -> ") + to_string(reachable_info->node_names[j]));
- delete reachable_info;
- 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 */
- DynamicArray1<Relation> &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]){
- yyerror(std::string("arity mismatch in start node ") + to_string(reachable_info->node_names[i]));
- delete reachable_info;
- YYERROR;
- }
- }
-;
-
-realNodeSpecificationList : realNodeSpecificationList ',' VAR ':' relation {
- int n_nodes = reachable_info->node_names.size();
- int index = reachable_info->node_names.index($3);
- if (!(index > 0 && index <= n_nodes)) {
- yyerror(std::string("no such node ")+to_string($3));
- delete $5;
- delete []$3;
- delete reachable_info;
- YYERROR;
- }
- reachable_info->start_nodes[index] = *$5;
- delete $5;
- delete []$3;
- }
- | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation {
- int n_nodes = reachable_info->node_names.size();
- int from_index = reachable_info->node_names.index($3);
- if (!(from_index > 0 && from_index <= n_nodes)) {
- yyerror(std::string("no such node ")+to_string($3));
- delete $7;
- delete []$3;
- delete []$5;
- delete reachable_info;
- YYERROR;
- }
- int to_index = reachable_info->node_names.index($5);
- if (!(to_index > 0 && to_index <= n_nodes)) {
- yyerror(std::string("no such node ")+to_string($5));
- delete $7;
- delete []$3;
- delete []$5;
- delete reachable_info;
- YYERROR;
- }
- reachable_info->transitions[from_index][to_index] = *$7;
- delete $7;
- delete []$3;
- delete []$5;
- }
- | VAR GOES_TO VAR ':' relation {
- int n_nodes = reachable_info->node_names.size();
- int from_index = reachable_info->node_names.index($1);
- if (!(from_index > 0 && from_index <= n_nodes)) {
- yyerror(std::string("no such node ")+to_string($1));
- delete $5;
- delete []$1;
- delete []$3;
- delete reachable_info;
- YYERROR;
- }
- int to_index = reachable_info->node_names.index($3);
- if (!(to_index > 0 && to_index <= n_nodes)) {
- yyerror(std::string("no such node ")+to_string($3));
- delete $5;
- delete []$1;
- delete []$3;
- delete reachable_info;
- YYERROR;
- }
- reachable_info->transitions[from_index][to_index] = *$5;
- delete $5;
- delete []$1;
- delete []$3;
- }
- | VAR ':' relation {
- int n_nodes = reachable_info->node_names.size();
- int index = reachable_info->node_names.index($1);
- if (!(index > 0 && index <= n_nodes)) {
- yyerror(std::string("no such node ")+to_string($1));
- delete $3;
- delete []$1;
- delete reachable_info;
- YYERROR;
- }
- reachable_info->start_nodes[index] = *$3;
- delete $3;
- delete []$1;
- }
-;
-
-%%
-
-
-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\n", argv[0]);
-}
-
-
-bool process_calc_debugging_flags(char *arg,int &j) {
- char debug_type;
- while((debug_type=arg[j]) != 0) {
- j++;
- int level;
- if(isdigit(arg[j]))
- level = (arg[j++]) - '0';
- else
- if(arg[j] == 0 || isalpha(arg[j]))
- level = 1;
- else
- return false;
- if (level < 0 || level > 4) {
- fprintf(stderr,"Debug level %c out of range: %d\n", debug_type, level);
- return false;
- }
- switch(debug_type) {
- case 'a':
- omega_core_debug = relation_debug = hull_debug =
- closure_presburger_debug =
- farkas_debug =
- pres_debug = omega_calc_debug = code_gen_debug = level;
- break;
- case 'g':
- code_gen_debug = level; break;
- case 'f':
- farkas_debug = level; break;
- case 'h':
- hull_debug = level; break;
- case 'c':
- omega_core_debug = level; break;
- case 'r':
- relation_debug = level; break;
- case 'p':
- pres_debug = level; break;
- case 't':
- closure_presburger_debug = level; break;
- case 'l':
- omega_calc_debug = level; break;
-#if defined STUDY_EVACUATIONS
- case 'e':
- evac_debug = level; break;
-#endif
- default:
- fprintf(stderr, "Unknown debug type %c\n", debug_type);
- return false;
- }
- }
- return true;
-}
-
-
-int main(int argc, char **argv) {
-#if YYDEBUG != 0
- yydebug = 1;
-#endif
-
- /* process flags */
- char *fileName = 0;
- for(int i=1; i<argc; i++) {
- if(argv[i][0] == '-') {
- int j = 1, c;
- while((c=argv[i][j++]) != 0) {
- switch(c) {
- case 'D':
- if (!process_calc_debugging_flags(argv[i],j)) {
- printUsage(stderr, argv);
- exit(1);
- }
- break;
- case 'G':
- fprintf(stderr,"Note: specifying number of GEQ's is no longer useful.\n");
- while(argv[i][j] != 0) j++;
- break;
- case 'E':
- fprintf(stderr,"Note: specifying number of EQ's is no longer useful.\n");
- while(argv[i][j] != 0) j++;
- break;
- case 'R':
- redundant_conj_level = 1;
- break;
- /* Other future options go here */
- case 'h':
- printUsage(stderr, argv);
- exit(1);
- break;
- default:
- fprintf(stderr, "\nUnknown flag -%c\n", c);
- printUsage(stderr, argv);
- exit(1);
- }
- }
- }
- else {
- /* Make sure this is a file name */
- if (fileName) {
- fprintf(stderr,"\nCan only handle a single input file\n");
- printUsage(stderr,argv);
- exit(1);
- }
- fileName = argv[i];
- yyin = fopen(fileName, "r");
- if (!yyin) {
- fprintf(stderr, "\nCan't open input file %s\n",fileName);
- printUsage(stderr,argv);
- exit(1);
- }
- }
- }
-
- if (fileName || !isatty((int)fileno(stdin))) {
- is_interactive = false;
- }
- else {
- is_interactive = true;
- setbuf(DebugFile, NULL);
- printf("Calculator for Omega+ v20110204snapshot (built on %s)\n", OMEGA_BUILD_DATE);
- printf("Copyright (C) 1994-2000 University of Maryland the Omega Project Team\n");
- printf("Copyright (C) 2008 University of Southern California\n");
- printf("Copyright (C) 2009-2011 University of Utah\n");
- printf("%s ", PROMPT_STRING);
- }
- need_coef = false;
- current_Declaration_Site = globalDecls = new Global_Declaration_Site();
-
- if (yyparse() != 0) {
- if (!is_interactive)
- std::cout << "syntax error at the end of the file, missing ';'" << std::endl;
- else
- std::cout << std::endl;
- delete relationDecl;
- relationDecl = NULL;
- }
- else {
- if (is_interactive)
- std::cout << std::endl;
- }
-
- foreach_map(cs,Const_String,r,Relation *,relationMap,
- {delete r; relationMap[cs]=0;});
- delete globalDecls;
- fclose(yyin);
-
- return 0;
-}
-
-Relation LexForward(int n) {
- Relation r(n,n);
- F_Or *f = r.add_or();
- for (int i=1; i <= n; i++) {
- F_And *g = f->add_and();
- for(int j=1;j<i;j++) {
- EQ_Handle e = g->add_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;
-}
generated by cgit v1.2.3-70-g09d2 (git 2.47.1) at 2025-02-02 00:43:47 +0000