diff options
Diffstat (limited to 'omegalib/omegacalc')
| -rw-r--r-- | omegalib/omegacalc/CMakeLists.txt | 34 | ||||
| -rw-r--r-- | omegalib/omegacalc/doc/calculator.pdf | bin | 0 -> 108062 bytes | |||
| -rw-r--r-- | omegalib/omegacalc/include/omega_calc/AST.h | 310 | ||||
| -rw-r--r-- | omegalib/omegacalc/include/omega_calc/PT-omega.c | 81 | ||||
| -rwxr-xr-x | omegalib/omegacalc/include/omega_calc/myflex.h | 27 | ||||
| -rw-r--r-- | omegalib/omegacalc/src/AST.cc | 467 | ||||
| -rwxr-xr-x | omegalib/omegacalc/src/myflex.cc | 421 | ||||
| -rw-r--r-- | omegalib/omegacalc/src/parser.l | 350 | ||||
| -rwxr-xr-x | omegalib/omegacalc/src/parser.ll | 350 | ||||
| -rw-r--r-- | omegalib/omegacalc/src/parser.y | 1925 | ||||
| -rwxr-xr-x | omegalib/omegacalc/src/parser.yy | 1928 |
11 files changed, 5893 insertions, 0 deletions
diff --git a/omegalib/omegacalc/CMakeLists.txt b/omegalib/omegacalc/CMakeLists.txt new file mode 100644 index 0000000..05e2988 --- /dev/null +++ b/omegalib/omegacalc/CMakeLists.txt @@ -0,0 +1,34 @@ +set(OC_VERSION 2.2.3) + +find_package(BISON) +find_package(FLEX) + +FLEX_TARGET(OCScanner src/parser.ll ${CMAKE_CURRENT_BINARY_DIR}/lex.yy.cc COMPILE_FLAGS "-+") +BISON_TARGET(OCParser src/parser.yy ${CMAKE_CURRENT_BINARY_DIR}/parser.tab.cc COMPILE_FLAGS "-t -d") +ADD_FLEX_BISON_DEPENDENCY(OCScanner OCParser) + +include_directories( + ${CMAKE_CURRENT_BINARY_DIR} + include + ${OMEGAROOT}/omega/include + ${OMEGAROOT}/codegen/include + ) + +string(TIMESTAMP build_date "\\\"%m/%d/%Y\\\"") + +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DBUILD_CODEGEN -DOC_VERSION=\"\\\"OC_VERSION\\\"\" -DOC_BUILD_DATE=\"${build_date}\"") + +add_executable(omegacalc + EXCLUDE_FROM_ALL + src/AST.cc + src/myflex.cc + ${FLEX_OCScanner_OUTPUTS} + ${BISON_OCParser_OUTPUTS} + ) + +add_dependencies(omegacalc omega codegen) +target_link_libraries(omegacalc omega codegen) + +install(TARGETS omegacalc + DESTINATION bin + COMPONENT omegacalc OPTIONAL) diff --git a/omegalib/omegacalc/doc/calculator.pdf b/omegalib/omegacalc/doc/calculator.pdf Binary files differnew file mode 100644 index 0000000..5c307ab --- /dev/null +++ b/omegalib/omegacalc/doc/calculator.pdf diff --git a/omegalib/omegacalc/include/omega_calc/AST.h b/omegalib/omegacalc/include/omega_calc/AST.h new file mode 100644 index 0000000..58d74fb --- /dev/null +++ b/omegalib/omegacalc/include/omega_calc/AST.h @@ -0,0 +1,310 @@ +#ifndef _AST_H +#define _AST_H + +#include <assert.h> +#include <omega.h> +#include <map> +#include <set> + +typedef enum {eq, lt, gt, geq, leq, neq} Rel_Op; + +class tupleDescriptor; + +class Variable_Ref { +public: + int anonymous; + omega::Const_String name; + omega::Const_String stripped_name; + omega::Variable_ID vid; + omega::Variable_ID id(omega::Rel_Body *R) { + if (vid) return vid; + if (arity == 0) + vid = R->get_local(g); + else + vid = R->get_local(g,of); + return vid; + } + omega::Variable_ID id(omega::Relation &R) { + if (vid) return vid; + if (arity == 0) + vid = R.get_local(g); + else + vid = R.get_local(g,of); + return vid; + } + omega::Free_Var_Decl *g; + int arity; + int pos; + omega::Argument_Tuple of; + Variable_Ref(char *s, int _arity, omega::Argument_Tuple _of); + Variable_Ref(char *s); + Variable_Ref(); + ~Variable_Ref(); +}; + +extern std::map<omega::Const_String, Variable_Ref *> functionOfInput; +extern std::map<omega::Const_String, Variable_Ref *> functionOfOutput; + +class Declaration_Site { +public: + Declaration_Site(); + Declaration_Site(std::set<char *> *v); + virtual Variable_Ref *extend(char *s); + virtual Variable_Ref *extend(char *s, omega::Argument_Tuple, int); + virtual ~Declaration_Site(); + + Variable_Ref *extend(); + void print() { + for (std::set<Variable_Ref *>::iterator i = declarations.begin(); ;) { + printf("%s", static_cast<const char *>((*i)->name)); + i++; + if (i != declarations.end()) + printf(","); + else + break; + } + } + + Declaration_Site *previous; + std::set<Variable_Ref *> declarations; +}; + +class Global_Declaration_Site: public Declaration_Site { +public: + virtual Variable_Ref *extend(char *s); + virtual Variable_Ref *extend() { + return Declaration_Site::extend(); + } + virtual Variable_Ref *extend(char *s, omega::Argument_Tuple in_of, int in_arity) { + return Declaration_Site::extend(s,in_of,in_arity); + } + void extend_both_tuples(char *s, int arity); + virtual ~Global_Declaration_Site(); +}; + +extern Declaration_Site *current_Declaration_Site; + +inline void popScope() { + assert(current_Declaration_Site); + current_Declaration_Site = current_Declaration_Site->previous; +} + +Variable_Ref *lookupScalar(char *s); +Declaration_Site * defined (char *); + +class Exp { +public: + Exp(omega::coef_t c); + Exp(Variable_Ref *v); + friend Exp *multiply (omega::coef_t c, Exp *x); + friend Exp *multiply (Exp *x, Exp *y); + friend Exp *negate (Exp *x); + friend Exp *add (Exp *x, Exp *y); + friend Exp *subtract (Exp *x, Exp *y); + std::map<Variable_Ref *, omega::coef_t> coefs; + omega::coef_t constantTerm; +protected: + void addTerm(omega::coef_t coef, omega::Variable_ID v); +}; + + +typedef struct { + Exp *e; + int step; +} strideConstraint; + + +class AST; +class AST_constraints; + + +class Tuple_Part { +public: + Variable_Ref *from,*to; + Tuple_Part(Variable_Ref *f, Variable_Ref *t) + { from = f; to = t; } + Tuple_Part(Variable_Ref *f) + { from = f; to = 0; } + Tuple_Part() + { from = 0; to = 0; } +}; + + +class AST { +public: + virtual void install(omega::Formula *F) = 0; + virtual void print() = 0; + virtual ~AST() {} +}; + + +class AST_And: public AST { +public: + AST_And(AST *l, AST *r) { left = l; right = r; } + ~AST_And() { delete left; delete right; } + + virtual void install(omega::Formula *F); + + virtual void print() { + printf("("); + left->print(); + printf(" && "); + right->print(); + printf(")"); + } + + AST *left,*right; +}; + + +class AST_Or: public AST { +public: + AST_Or(AST *l, AST *r) { left = l; right = r; } + ~AST_Or() { delete left; delete right; } + + virtual void install(omega::Formula *F); + + virtual void print() { + printf("("); + left->print(); + printf(" || "); + right->print(); + printf(")"); + } + + + AST *left, *right; +}; + + +class AST_Not: public AST { +public: + AST_Not(AST *c) { child = c; } + ~AST_Not() { delete child; } + + virtual void install(omega::Formula *F); + + virtual void print() { + printf("(!"); + child->print(); + printf(")"); + } + + AST *child; +}; + + +class AST_declare: public AST { +public: + virtual void install(omega::Formula *F) = 0; + + virtual void print() { + printf("("); + declaredVariables->print(); + printf(" : "); + child->print(); + printf(")"); + } + + Declaration_Site *declaredVariables; + AST *child; +}; + + +class AST_exists: public AST_declare { +public: + AST_exists(Declaration_Site *dV, AST *c) {declaredVariables = dV, child = c;} + ~AST_exists() { delete child; delete declaredVariables; } + + virtual void install(omega::Formula *F); + + virtual void print() { + printf("exists "); + AST_declare::print(); + } +}; + + +class AST_forall: public AST_declare { +public: + AST_forall(Declaration_Site *dV, AST *c) {declaredVariables = dV, child = c; } + ~AST_forall() { delete child; delete declaredVariables; } + + virtual void install(omega::Formula *F); + + virtual void print() { + printf("forall "); + AST_declare::print(); + } +}; + + + +class AST_constraints: public AST { +public: + AST_constraints(std::set<Exp *> *f, Rel_Op r, AST_constraints *o); + AST_constraints(std::set<Exp *> *f, Rel_Op r, std::set<Exp *> *s); + AST_constraints(std::set<Exp *> *f); + ~AST_constraints(); + + virtual void install(omega::Formula *F); + + virtual void print(); + + AST_constraints *others; + std::set<Exp *> *first; + Rel_Op rel_op; +}; + +void install_stride(omega::F_And *F, strideConstraint *c); +void install_eq(omega::F_And *F, Exp *e1, Exp *e2); +void install_geq(omega::F_And *F, Exp *e1, Exp *e2); +void install_gt(omega::F_And *F, Exp *e1, Exp *e2); +void install_neq(omega::F_And *F, Exp *e1, Exp *e2); + + + +class tupleDescriptor { +public: + tupleDescriptor() { size = 0; } + void extend(); + void extend(Exp * e); + void extend(Exp * lb, Exp *ub); + void extend(Exp * lb, Exp *ub, omega::coef_t stride); + void extend(char * s, Exp *e); + void extend(char * s); + void extend(char * s, omega::Argument_Tuple, int); + + int size; + std::vector<Variable_Ref *> vars; + std::set<Exp *> eq_constraints; + std::set<Exp *> geq_constraints; + std::set<strideConstraint *> stride_constraints; + ~tupleDescriptor() { + for (std::set<Exp *>::iterator i = eq_constraints.begin(); i != eq_constraints.end(); i++) + delete *i; + for (std::set<Exp *>::iterator i = geq_constraints.begin(); i != geq_constraints.end(); i++) + delete *i; + for (std::set<strideConstraint *>::iterator i = stride_constraints.begin(); i != stride_constraints.end(); i++) { + delete (*i)->e; + delete *i; + } + } +}; + +extern Global_Declaration_Site *globalDecls; +extern Declaration_Site *relationDecl; +extern tupleDescriptor *currentTupleDescriptor; + +void resetGlobals(); + + +// Used to parse a list of paired relations for code generation commands +// class RelTuplePair { +// public: +// RelTuplePair() : ispaces(0), mappings(0) {} +// omega::Tuple<omega::Relation> ispaces; +// omega::Tuple<omega::Relation> mappings; +// }; + +#endif diff --git a/omegalib/omegacalc/include/omega_calc/PT-omega.c b/omegalib/omegacalc/include/omega_calc/PT-omega.c new file mode 100644 index 0000000..ad6b979 --- /dev/null +++ b/omegalib/omegacalc/include/omega_calc/PT-omega.c @@ -0,0 +1,81 @@ +#undef DONT_INCLUDE_TEMPLATE_CODE + +#include <basic/bool.h> +#include <basic/util.h> +#include <basic/List.h> +#include <basic/SimpleList.h> +#include <basic/Bag.h> +#include <basic/Map.h> +#include <basic/Tuple.h> +#include <basic/Section.h> +#include <basic/Exit.h> +#include <basic/Dynamic_Array.h> +#include <omega.h> +#include <omega/AST.h> + +template int max(int, int); +template int min(int, int); +template unsigned int min(unsigned int, unsigned int); +template void set_max(int&,int); +template void set_min(int&,int); +template void swap(int&,int&); +template void swap(short&,short&); +template void swap(signed char&,signed char&); +template Relation copy(const Relation &); + +instantiate_Set(int); +instantiate_Set(Global_Var_ID); +instantiate_Set(Variable_ID); + +instantiate_List(int); +instantiate_List(exit_func); +instantiate_List(Formula *); +instantiate_List(Conjunct *); +instantiate_List(DNF *); +instantiate_List(Relation *); +instantiate_Simple_List(Relation); + +typedef Tuple<Relation> RelationTuple; +instantiate_Tuple(bool); +instantiate_Tuple(int); +instantiate_Tuple(coef_t); +instantiate_Tuple(char *); +instantiate_Tuple(Const_String); +instantiate_Tuple(Conjunct *); +instantiate_Tuple(Relation); +instantiate_Tuple(RelationTuple); +instantiate_Tuple(Variable_ID); +instantiate_Tuple(Free_Var_Decl *); +instantiate_Tuple(std::string); +instantiate_Tuple(GEQ_Handle); + +instantiate_Section(Variable_ID); + +instantiate_Generator(Variable_Info); +instantiate_Generator(GEQ_Handle); +instantiate_Generator(EQ_Handle); +instantiate_Generator(Constraint_Handle); +instantiate_Generator(Sub_Handle); + +instantiate_Map(Variable_ID,int); +instantiate_Map(Global_Var_ID, Variable_ID); +instantiate_Map(GEQ_Handle,Variable_ID); +instantiate_Map(EQ_Handle,Variable_ID); +instantiate_Map(Variable_ID,Set<Variable_ID>); +instantiate_Map(Const_String, Relation *); + +instantiate_Dynamic_Array1(Coef_Var_Decl *); +instantiate_Dynamic_Array1(Relation); +instantiate_Dynamic_Array2(Relation); + + +/* Stuff required by calculator: */ +instantiate_Bag(Exp *); +instantiate_Bag(strideConstraint *); +instantiate_Bag(Variable_Ref *); +instantiate_Bag(char *); +instantiate_Map(Variable_Ref *, int); +instantiate_Map(Variable_Ref *, Variable_Ref *); +instantiate_Map(Const_String, Variable_Ref *); +instantiate_Set(Free_Var_Decl *); +instantiate_Tuple(Variable_Ref *); diff --git a/omegalib/omegacalc/include/omega_calc/myflex.h b/omegalib/omegacalc/include/omega_calc/myflex.h new file mode 100755 index 0000000..d472e51 --- /dev/null +++ b/omegalib/omegacalc/include/omega_calc/myflex.h @@ -0,0 +1,27 @@ +#ifndef _MYFLEX_H +#define _MYFLEX_H + +#ifndef yyFlexLexerOnce +#include <FlexLexer.h> +#endif +#include <iostream> +#include <string> +#include <vector> + +class myFlexLexer: public yyFlexLexer { +protected: + std::string cur_line; + int cur_pos; + std::vector<std::string> history; + int first_history_pos; + int last_history_pos; + std::vector<std::string> key_seqs; + +public: + myFlexLexer(std::istream *arg_yyin = NULL, std::ostream *arg_yyout = NULL); + ~myFlexLexer() {} +protected: + int LexerInput(char *buf, int max_size); +}; + +#endif diff --git a/omegalib/omegacalc/src/AST.cc b/omegalib/omegacalc/src/AST.cc new file mode 100644 index 0000000..1f885a6 --- /dev/null +++ b/omegalib/omegacalc/src/AST.cc @@ -0,0 +1,467 @@ +/***************************************************************************** + Copyright (C) 1994-2000 the Omega Project Team + Copyright (C) 2009-2011 Chun Chen + All Rights Reserved. + + Purpose: + build relation from parsed input. + + Notes: + + History: +*****************************************************************************/ + +#include <omega_calc/AST.h> +#include <string.h> + +using namespace omega; + +Global_Declaration_Site *globalDecls; +Declaration_Site *relationDecl = NULL; +tupleDescriptor *currentTupleDescriptor; +std::map<omega::Const_String, Variable_Ref *> functionOfInput; +std::map<omega::Const_String, Variable_Ref *> functionOfOutput; + +AST_constraints::AST_constraints(std::set<Exp *> *f, Rel_Op r, AST_constraints *o) { + others = o; + rel_op = r; + first = f; +} + +AST_constraints::AST_constraints(std::set<Exp *> *f, Rel_Op r, std::set<Exp *> *s) { + others = new AST_constraints(s); + rel_op = r; + first = f; +} + +AST_constraints::AST_constraints(std::set<Exp *> *f){ + others = 0; + first = f; +} + +AST_constraints::~AST_constraints() { + for (std::set<Exp *>::iterator i = first->begin(); i != first->end(); i++) + delete *i; + delete first; + delete others; +} + +void AST_constraints::print() { + for (std::set<Exp *>::iterator i = first->begin(); ;) { + printf(coef_fmt, (*i)->constantTerm); + for (std::map<Variable_Ref *, omega::coef_t>::iterator j = (*i)->coefs.begin(); j != (*i)->coefs.end(); j++) + printf("+"coef_fmt"%s", (*j).second, static_cast<const char *>((*j).first->name)); + i++; + if (i != first->end()) + printf(", "); + else + break; + } +} + + +Exp::Exp(coef_t c) : coefs() { + constantTerm = c; +} + +Exp::Exp(Variable_Ref *v) : coefs() { + assert(v != 0); + constantTerm = 0; + coefs[v] = 1; +} + +Exp *negate (Exp *x) { + x->constantTerm = -x->constantTerm; + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = x->coefs.begin(); i != x->coefs.end(); i++) + (*i).second = -(*i).second; + return x; +} + +Exp *add (Exp *x, Exp *y) { + x->constantTerm += y->constantTerm; + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = y->coefs.begin(); i != y->coefs.end(); i++) + x->coefs[(*i).first] += (*i).second; + delete y; + return x; +} + +Exp *subtract (Exp *x, Exp *y) { + x->constantTerm -= y->constantTerm; + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = y->coefs.begin(); i != y->coefs.end(); i++) + x->coefs[(*i).first] -= (*i).second; + delete y; + return x; +} + +Exp *multiply (coef_t c, Exp *x) { + x->constantTerm *= c; + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = x->coefs.begin(); i != x->coefs.end(); i++) + (*i).second *= c; + return x; +} + +Exp *multiply (Exp *x, Exp *y) { + bool found_nonzero = false; + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = x->coefs.begin(); i != x->coefs.end(); i++) + if ((*i).second != 0) + found_nonzero = true; + if (!found_nonzero) { + coef_t c = x->constantTerm; + delete x; + return multiply(c,y); + } + + found_nonzero = false; + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = y->coefs.begin(); i != y->coefs.end(); i++) + if ((*i).second != 0) + found_nonzero = true; + if (!found_nonzero) { + coef_t c = y->constantTerm; + delete y; + return multiply(c,x); + } + + delete x; + delete y; + throw std::runtime_error("invalid exp multiply"); +} + + + +Declaration_Site *current_Declaration_Site = 0; + +Declaration_Site::Declaration_Site() { + previous = current_Declaration_Site; + current_Declaration_Site = this; +} + +Declaration_Site::Declaration_Site(std::set<char *> *v) { + previous = current_Declaration_Site; + current_Declaration_Site = this; + for (std::set<char *>::iterator i = v->begin(); i != v->end(); i++) + declarations.insert(new Variable_Ref(*i)); +} + +Declaration_Site::~Declaration_Site() { + for (std::set<Variable_Ref *>::iterator i = declarations.begin(); i != declarations.end(); i++) + delete *i; +} + +Variable_Ref::Variable_Ref(char *s, int _arity, Argument_Tuple _of) { + name = s; + arity = _arity; + of = _of; + anonymous = !strncmp("In_",s,3) || !strncmp("Out_",s,4); + char *t = s; + while (*t != '\0') t++; + t--; + while (*t == '\'') t--; + t++; + *t = '\0'; + stripped_name = s; + g = 0; +} + +Variable_Ref::Variable_Ref(char *s) { + name = s; + arity = 0; + anonymous = !strncmp("In_",s,3) || !strncmp("Out_",s,4); + char *t = s; + while (*t != '\0') t++; + t--; + while (*t == '\'') t--; + t++; + *t = '\0'; + stripped_name = s; + g = 0; +} + +Variable_Ref::Variable_Ref() { + name = "#anonymous"; + arity = 0; + anonymous = 1; + stripped_name = name; + g = 0; +} + +Variable_Ref::~Variable_Ref() { + assert(g == 0); +} + +Variable_Ref *lookupScalar(char *s) { + Declaration_Site *ds; + for(ds = current_Declaration_Site; ds; ds = ds->previous) + for (std::set<Variable_Ref *>::iterator i = ds->declarations.begin(); i != ds->declarations.end(); i++) + if ((*i)->name == static_cast<Const_String>(s)) + return (*i); + return NULL; +} + +Declaration_Site *defined(char *s) { + Declaration_Site *ds; + for(ds = current_Declaration_Site; ds; ds = ds->previous) + for (std::set<Variable_Ref *>::iterator i = ds->declarations.begin(); i != ds->declarations.end(); i++) + if ((*i)->name == static_cast<Const_String>(s)) + return ds; + return NULL; +} + + +void AST_Or::install(Formula *F) { + if (F->node_type() != Op_Or) + F = F->add_or(); + left->install(F); + right->install(F); +} + +void AST_And::install(Formula *F) { + if (F->node_type() != Op_And) F = F->add_and(); + left->install(F); + right->install(F); +} + +void AST_Not::install(Formula *F) { + child->install(F->add_not()); +} + +void AST_exists::install(Formula *F) { + F_Exists *G = F->add_exists(); + for (std::set<Variable_Ref *>::iterator i = declaredVariables->declarations.begin(); i != declaredVariables->declarations.end(); i++) + (*i)->vid = G->declare((*i)->stripped_name); + child->install(G); +} + +void AST_forall::install(Formula *F) { + F_Forall *G = F->add_forall(); + for (std::set<Variable_Ref *>::iterator i = declaredVariables->declarations.begin(); i != declaredVariables->declarations.end(); i++) + (*i)->vid = G->declare((*i)->stripped_name); + child->install(G); +} + +void AST_constraints::install(Formula *F) { + if (!others) return; + F_And *f = F->and_with(); + + for (std::set<Exp *>::iterator i = first->begin(); i != first->end(); i++) + for (std::set<Exp *>::iterator j = others->first->begin(); j != others->first->end(); j++) + switch (rel_op) { + case(lt) : install_gt(f, *j, *i); break; + case(gt) : install_gt(f, *i, *j); break; + case(leq) : install_geq(f, *j, *i); break; + case(geq) : install_geq(f, *i, *j); break; + case(eq) : install_eq(f, *i, *j); break; + case(neq) : install_neq(f, *i, *j); break; + default : assert(0); + } + others->install(f); +} + + +void install_neq(F_And *F, Exp *e1, Exp *e2) { + F_Or *or_ = F->add_or(); + F_And *and1 = or_->add_and(); + F_And *and2 = or_->add_and(); + install_gt(and1,e1,e2); + install_gt(and2,e2,e1); +}; + +void install_stride(F_And *F, strideConstraint *s) { + Stride_Handle c = F->add_stride(s->step); + c.update_const(s->e->constantTerm); + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = s->e->coefs.begin(); i != s->e->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), (*i).second); + c.finalize(); +} + +void install_eq(F_And *F, Exp *e1, Exp *e2) { + EQ_Handle c = F->add_EQ(); + c.update_const(e1->constantTerm); + if (e2) c.update_const(-e2->constantTerm); + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e1->coefs.begin(); i != e1->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), (*i).second); + if (e2) + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e2->coefs.begin(); i != e2->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), -(*i).second); + c.finalize(); +} + +void install_geq(F_And *F, Exp *e1, Exp *e2) { + GEQ_Handle c = F->add_GEQ(); + c.update_const(e1->constantTerm); + if (e2) c.update_const(-e2->constantTerm); + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e1->coefs.begin(); i != e1->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), (*i).second); + if (e2) + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e2->coefs.begin(); i != e2->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), -(*i).second); + c.finalize(); +} + +void install_gt(F_And *F, Exp *e1, Exp *e2) { + GEQ_Handle c = F->add_GEQ(); + c.update_const(-1); + c.update_const(e1->constantTerm); + if (e2) c.update_const(-e2->constantTerm); + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e1->coefs.begin(); i != e1->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), (*i).second); + if (e2) + for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e2->coefs.begin(); i != e2->coefs.end(); i++) + c.update_coef((*i).first->id(F->relation()), -(*i).second); + c.finalize(); +} + + +Global_Declaration_Site::~Global_Declaration_Site() { +/* // Take care of global variables - since we do that kludge */ +/* // of declaring globals twice if arity > 0, we must take care */ +/* // not to just delete each global once per declaration. */ + +/* // Actually, we can't free these, since Relations containing references to */ +/* // this may get freed later */ +/* foreach(v,Variable_Ref*,this->declarations,v->g=0); */ +/* //Set<Free_Var_Decl *> globals; */ +/* //foreach(v,Variable_Ref*,this->declarations,(globals.insert(v->g),v->g=0)); */ +/* //foreach(g,Free_Var_Decl*,globals,delete g); */ + + // Only delete global variables here. --chun 5/28/2008 + for (std::set<Variable_Ref *>::iterator i= declarations.begin(); i != declarations.end(); i++) { + if ((*i)->g != 0) { + if ((*i)->arity != 0) { // functional symbols + // only delete once from a pair of "(in)" and "(out)" variables + const char *name = static_cast<const char *>((*i)->name); + const char *s = "(in)"; + bool match = true; + for (size_t p = strlen(name)-4, q = 0; p < strlen(name); p++, q++) + if (s[q] != name[p]) { + match = false; + break; + } + if (match) + delete (*i)->g; + } + else // not functions + delete (*i)->g; + + (*i)->g = 0; + } + } +} + +Variable_Ref * Global_Declaration_Site::extend(char *s) { + Variable_Ref *r = new Variable_Ref(s); + r->g = new Free_Var_Decl(r->stripped_name); + declarations.insert(r); + return r; +} + +void Global_Declaration_Site::extend_both_tuples(char *s, int arity) { + if (arity == 0) + extend(s); + else { + assert(arity > 0); + + char s1[strlen(s)+5], s2[strlen(s)+6]; + strcpy(s1,s); strcat(s1,"(in)"); + strcpy(s2,s); strcat(s2,"(out)"); + Const_String name = s; + + Variable_Ref *r1 = new Variable_Ref(s1, arity, Input_Tuple); + Variable_Ref *r2 = new Variable_Ref(s2, arity, Output_Tuple); + r1->g = r2->g = new Free_Var_Decl(s,arity); + + functionOfInput[name] = r1; + functionOfOutput[name] = r2; + + declarations.insert(r1); + declarations.insert(r2); + } +} + + +void resetGlobals() { + for (std::set<Variable_Ref *>::iterator i = globalDecls->declarations.begin(); i != globalDecls->declarations.end(); i++) + (*i)->vid = 0; +} + + +Variable_Ref *Declaration_Site::extend(char *s) { + Variable_Ref *r = new Variable_Ref(s); + declarations.insert(r); + return r; +} + +Variable_Ref *Declaration_Site::extend(char *s, Argument_Tuple of, int pos) { + Variable_Ref *r = new Variable_Ref(s); + declarations.insert(r); + r->of = of; + r->pos = pos; + return r; +} + +Variable_Ref * Declaration_Site::extend() { + Variable_Ref *r = new Variable_Ref(); + declarations.insert(r); + return r; +} + +void tupleDescriptor::extend(char *s) { + Variable_Ref *r = relationDecl->extend(s); + size++; + vars.push_back(r); + assert(size == vars.size()); +} + +void tupleDescriptor::extend(char *s, Argument_Tuple of, int pos) { + Variable_Ref *r = relationDecl->extend(s, of, pos); + size++; + vars.push_back(r); + assert(size == vars.size()); +} + +void tupleDescriptor::extend(Exp *e) { + Variable_Ref *r = relationDecl->extend(); + size++; + vars.push_back(r); + assert(size == vars.size()); + Exp *eq = subtract(e, new Exp(r)); + eq_constraints.insert(eq); +} + +void tupleDescriptor::extend(char *s, Exp *e) { + Variable_Ref *r = relationDecl->extend(s); + size++; + vars.push_back(r); + assert(size == vars.size()); + Exp *eq = subtract(e, new Exp(r)); + eq_constraints.insert(eq); +} + +void tupleDescriptor::extend() { + Variable_Ref *r = relationDecl->extend(); + size++; + vars.push_back(r); + assert(size == vars.size()); +} +void tupleDescriptor::extend(Exp *lb,Exp *ub) { + Variable_Ref *r = relationDecl->extend(); + size++; + vars.push_back(r); + assert(size == vars.size()); + Exp *lb_exp = subtract(new Exp(r), lb); + geq_constraints.insert(lb_exp); + Exp *ub_exp = subtract(ub, new Exp(r)); + geq_constraints.insert(ub_exp); +} +void tupleDescriptor::extend(Exp *lb,Exp *ub, coef_t stride) { + Variable_Ref *r = relationDecl->extend(); + size++; + vars.push_back(r); + Exp *lb_exp = subtract(new Exp(r), new Exp(*lb)); + geq_constraints.insert(lb_exp); + Exp *ub_exp = subtract(ub, new Exp(r)); + geq_constraints.insert(ub_exp); + strideConstraint *s = new strideConstraint; + s->e = subtract(lb, new Exp(r)); + s->step = stride; + stride_constraints.insert(s); +} diff --git a/omegalib/omegacalc/src/myflex.cc b/omegalib/omegacalc/src/myflex.cc new file mode 100755 index 0000000..89a2544 --- /dev/null +++ b/omegalib/omegacalc/src/myflex.cc @@ -0,0 +1,421 @@ +/***************************************************************************** + Copyright (C) 2011 Chun Chen + All Rights Reserved. + + Purpose: + support command line editing for calculator. + + Notes: + Since terminfo database is not queried for those nagging escape sequences, + current supported terminials are limited to xterm, linux, cygwin. + + History: + 02/06/11 created by Chun Chen +*****************************************************************************/ + +#include <omega_calc/myflex.h> +#include <basic/util.h> +#include <string.h> +#include <stdlib.h> + +#if defined __USE_POSIX +#include <unistd.h> +#include <termios.h> +#include <sys/ioctl.h> +#elif defined __WIN32 +#else +#endif + +#define HISTORY_SIZE 100 + +namespace { +enum {MY_KEY_EOF=0, MY_KEY_LEFT, MY_KEY_RIGHT, MY_KEY_UP, MY_KEY_DOWN, + MY_KEY_DEL, MY_KEY_HOME, MY_KEY_END, MY_KEY_PGUP, MY_KEY_PGDOWN, + MY_KEY_NUMPAD_HOME, MY_KEY_NUMPAD_END}; +} + +extern bool is_interactive; +extern const char * PROMPT_STRING; + +void move_cursor(int col, int n, int num_cols, const std::vector<std::string> &key_seqs) { + if (n == 0) + return; + + int new_col = omega::int_mod(col + n, num_cols); + if (new_col == 0) + new_col = num_cols; + + for (int i = 0; i < new_col-col; i++) + std::cout.write(key_seqs[MY_KEY_RIGHT].c_str(), key_seqs[MY_KEY_RIGHT].length()); + for (int i = 0; i < col-new_col; i++) + std::cout.write(key_seqs[MY_KEY_LEFT].c_str(), key_seqs[MY_KEY_LEFT].length()); + + if (n < 0) + for (int i = 0; i < omega::abs(n) / num_cols + (new_col>col)?1:0; i++) + std::cout.write(key_seqs[MY_KEY_UP].c_str(), key_seqs[MY_KEY_UP].length()); + else + for (int i = 0; i < omega::abs(n) / num_cols + (new_col<col)?1:0; i++) + std::cout.write(key_seqs[MY_KEY_DOWN].c_str(), key_seqs[MY_KEY_DOWN].length()); +} + + + +myFlexLexer::myFlexLexer(std::istream *arg_yyin, std::ostream *arg_yyout): + yyFlexLexer(arg_yyin, arg_yyout), history(HISTORY_SIZE), key_seqs(12) { + cur_pos = 0; + first_history_pos = 0; + last_history_pos = -1; + + if (strcmp(getenv("TERM"), "xterm") == 0 || + strcmp(getenv("TERM"), "xterm-color") == 0) { + key_seqs[MY_KEY_EOF] = "\x04"; + key_seqs[MY_KEY_LEFT] = "\x1B\x5B\x44"; + key_seqs[MY_KEY_RIGHT] = "\x1B\x5B\x43"; + key_seqs[MY_KEY_UP] = "\x1B\x5B\x41"; + key_seqs[MY_KEY_DOWN] = "\x1B\x5B\x42"; + key_seqs[MY_KEY_DEL] = "\x1B\x5B\x33\x7E"; + key_seqs[MY_KEY_HOME] = "\x1B\x4F\x48"; + key_seqs[MY_KEY_END] = "\x1B\x4F\x46"; + key_seqs[MY_KEY_PGUP] = "\x1B\x5B\x35\x7E"; + key_seqs[MY_KEY_PGDOWN] = "\x1B\x5B\x36\x7E"; + key_seqs[MY_KEY_NUMPAD_HOME] = "\x1B\x5B\x31\x7E"; + key_seqs[MY_KEY_NUMPAD_END] = "\x1B\x5B\x34\x7E"; + } + else if (strcmp(getenv("TERM"), "linux") == 0 || + strcmp(getenv("TERM"), "cygwin") == 0) { + key_seqs[MY_KEY_EOF] = "\x04"; + key_seqs[MY_KEY_LEFT] = "\x1B\x5B\x44"; + key_seqs[MY_KEY_RIGHT] = "\x1B\x5B\x43"; + key_seqs[MY_KEY_UP] = "\x1B\x5B\x41"; + key_seqs[MY_KEY_DOWN] = "\x1B\x5B\x42"; + key_seqs[MY_KEY_DEL] = "\x1B\x5B\x33\x7E"; + key_seqs[MY_KEY_HOME] = "\x1B\x5B\x31\x7E"; + key_seqs[MY_KEY_END] = "\x1B\x5B\x34\x7E"; + key_seqs[MY_KEY_PGUP] = "\x1B\x5B\x35\x7E"; + key_seqs[MY_KEY_PGDOWN] = "\x1B\x5B\x36\x7E"; + key_seqs[MY_KEY_NUMPAD_HOME] = "\x1B\x5B\x31\x7E"; + key_seqs[MY_KEY_NUMPAD_END] = "\x1B\x5B\x34\x7E"; + } + else { + key_seqs[MY_KEY_EOF] = "\x04"; + } +} + +int myFlexLexer::LexerInput(char *buf, int max_size) { + if (!is_interactive) + return yyFlexLexer::LexerInput(buf, max_size); + +#if defined __USE_POSIX + winsize wsz; + ioctl(0, TIOCGWINSZ, &wsz); + int num_cols = wsz.ws_col; + + // unknown screen size, bail out + if (num_cols == 0) + return yyFlexLexer::LexerInput(buf, max_size); + + termios old_settings; + termios new_settings; + char keycodes[255]; + + // set console to no echo, raw input mode + tcgetattr(STDIN_FILENO, &old_settings); + new_settings = old_settings; + new_settings.c_cc[VTIME] = 1; + new_settings.c_cc[VMIN] = 1; + new_settings.c_iflag &= ~(IXOFF); + new_settings.c_lflag &= ~(ECHO|ICANON); + tcsetattr(STDIN_FILENO, TCSANOW, &new_settings); + + int cur_history_pos = (last_history_pos+1)%HISTORY_SIZE; + while (true) { + // feed current line to lex + int len = cur_line.length(); + if (len > 0 && cur_line[len-1] == '\n') { + int n = omega::min(len-cur_pos, max_size); + for (int i = 0; i < n; i++) + buf[i] = cur_line[cur_pos+i]; + cur_pos = cur_pos + n; + if (cur_pos == len) { + // save history + if (len > 1) { + if (last_history_pos == -1) + last_history_pos = 0; + else { + last_history_pos = (last_history_pos+1)%HISTORY_SIZE; + if ((last_history_pos + 1)%HISTORY_SIZE == first_history_pos) + first_history_pos = (first_history_pos+1)%HISTORY_SIZE; + } + history[last_history_pos] = cur_line.substr(0, len-1); + cur_history_pos = (last_history_pos+1)%HISTORY_SIZE; + } + + // clear the working line + cur_pos = 0; + cur_line.clear(); + } + tcsetattr(STDIN_FILENO, TCSANOW, &old_settings); + return n; + } + + int count = read(STDIN_FILENO, keycodes, 255); + + // handle special key my way + int eaten = 0; + while (eaten < count) { + if (key_seqs[MY_KEY_EOF].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_EOF].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_EOF].c_str(), key_seqs[MY_KEY_EOF].length()) == 0) { + if (cur_line.length() == 0) { + tcsetattr(STDIN_FILENO, TCSANOW, &old_settings); + return 0; + } + + eaten += key_seqs[MY_KEY_EOF].length(); + } + else if (key_seqs[MY_KEY_LEFT].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_LEFT].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_LEFT].c_str(), key_seqs[MY_KEY_LEFT].length()) == 0) { + if (cur_pos > 0) { + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + cur_pos--; + + move_cursor(cur_col, -1, num_cols, key_seqs); + } + eaten += key_seqs[MY_KEY_LEFT].length(); + } + else if (key_seqs[MY_KEY_RIGHT].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_RIGHT].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_RIGHT].c_str(), key_seqs[MY_KEY_RIGHT].length()) == 0) { + if (static_cast<size_t>(cur_pos) < cur_line.length()) { + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + cur_pos++; + + move_cursor(cur_col, 1, num_cols, key_seqs); + } + eaten += key_seqs[MY_KEY_RIGHT].length(); + } + else if (key_seqs[MY_KEY_UP].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_UP].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_UP].c_str(), key_seqs[MY_KEY_UP].length()) == 0) { + if (cur_history_pos >= 0 && cur_history_pos != first_history_pos) { + history[cur_history_pos] = cur_line; + cur_history_pos = omega::int_mod(cur_history_pos-1, HISTORY_SIZE); + + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + move_cursor(cur_col, -cur_pos, num_cols, key_seqs); + + std::cout.write(history[cur_history_pos].c_str(), history[cur_history_pos].length()); + + cur_col = (history[cur_history_pos].length() + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) { + std::cout.put(' '); + std::cout.put('\b'); + } + + if (cur_line.length() > history[cur_history_pos].length()) { + for (size_t i = 0; i < cur_line.length() - history[cur_history_pos].length(); i++) + std::cout.put(' '); + + cur_col = (cur_line.length() + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols + 1; + else + cur_col++; + + move_cursor(cur_col, -(cur_line.length() - history[cur_history_pos].length()), num_cols, key_seqs); + } + cur_line = history[cur_history_pos]; + cur_pos = cur_line.length(); + } + + eaten += key_seqs[MY_KEY_UP].length(); + } + else if (key_seqs[MY_KEY_DOWN].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_DOWN].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_DOWN].c_str(), key_seqs[MY_KEY_DOWN].length()) == 0) { + if (cur_history_pos >= 0 && cur_history_pos != (last_history_pos+1)%HISTORY_SIZE) { + history[cur_history_pos] = cur_line; + cur_history_pos = (cur_history_pos+1)%HISTORY_SIZE; + + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + move_cursor(cur_col, -cur_pos, num_cols, key_seqs); + + std::cout.write(history[cur_history_pos].c_str(), history[cur_history_pos].length()); + + cur_col = (history[cur_history_pos].length() + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) { + std::cout.put(' '); + std::cout.put('\b'); + } + + if (cur_line.length() > history[cur_history_pos].length()) { + for (size_t i = 0; i < cur_line.length() - history[cur_history_pos].length(); i++) + std::cout.put(' '); + + cur_col = (cur_line.length() + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols + 1; + else + cur_col++; + + move_cursor(cur_col, -(cur_line.length() - history[cur_history_pos].length()), num_cols, key_seqs); + } + cur_line = history[cur_history_pos]; + cur_pos = cur_line.length(); + } + + eaten += key_seqs[MY_KEY_DOWN].length(); + } + else if (key_seqs[MY_KEY_DEL].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_DEL].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_DEL].c_str(), key_seqs[MY_KEY_DEL].length()) == 0) { + if (static_cast<size_t>(cur_pos) < cur_line.length()) { + cur_line.erase(cur_pos, 1); + std::cout.write(&(cur_line.c_str()[cur_pos]), cur_line.length()-cur_pos); + std::cout.put(' '); + + int cur_col = (cur_line.length() + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols + 1; + else + cur_col++; + + move_cursor(cur_col, -(cur_line.length()-cur_pos+1), num_cols, key_seqs); + } + + eaten += key_seqs[MY_KEY_DEL].length(); + } + else if (key_seqs[MY_KEY_HOME].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_HOME].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_HOME].c_str(), key_seqs[MY_KEY_HOME].length()) == 0) { + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + move_cursor(cur_col, -cur_pos, num_cols, key_seqs); + + cur_pos = 0; + eaten += key_seqs[MY_KEY_HOME].length(); + } + else if (key_seqs[MY_KEY_END].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_END].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_END].c_str(), key_seqs[MY_KEY_END].length()) == 0) { + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + move_cursor(cur_col, cur_line.length()-cur_pos, num_cols, key_seqs); + + cur_pos = cur_line.length(); + eaten += key_seqs[MY_KEY_END].length(); + } + else if (key_seqs[MY_KEY_PGUP].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_PGUP].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_PGUP].c_str(), key_seqs[MY_KEY_PGUP].length()) == 0) { + eaten += key_seqs[MY_KEY_PGUP].length(); + } + else if (key_seqs[MY_KEY_PGDOWN].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_PGDOWN].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_PGDOWN].c_str(), key_seqs[MY_KEY_PGDOWN].length()) == 0) { + eaten += key_seqs[MY_KEY_PGDOWN].length(); + } + else if (key_seqs[MY_KEY_NUMPAD_HOME].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_NUMPAD_HOME].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_NUMPAD_HOME].c_str(), key_seqs[MY_KEY_NUMPAD_HOME].length()) == 0) { + eaten += key_seqs[MY_KEY_NUMPAD_HOME].length(); + } + else if (key_seqs[MY_KEY_NUMPAD_END].length() > 0 && + static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_NUMPAD_END].length() && + strncmp(&keycodes[eaten], key_seqs[MY_KEY_NUMPAD_END].c_str(), key_seqs[MY_KEY_NUMPAD_END].length()) == 0) { + eaten += key_seqs[MY_KEY_NUMPAD_END].length(); + } + else if (keycodes[eaten] == '\x1B' && (count - eaten == 1 || keycodes[eaten+1] == '\x1B')) { // single ESC key + eaten++; + } + else if (keycodes[eaten] == '\x1B') { // unknown escape sequences + while (eaten+1 < count && keycodes[eaten+1] != '\x1B') + eaten++; + + keycodes[eaten] = '~'; + } + else if (keycodes[eaten] == '\x7F') { // backspace key + if (cur_pos > 0) { + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + cur_pos--; + cur_line.erase(cur_pos, 1); + + move_cursor(cur_col, -1, num_cols, key_seqs); + + std::cout.write(&(cur_line.c_str()[cur_pos]), cur_line.length()-cur_pos); + std::cout.put(' '); + + cur_col = (cur_line.length() + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols + 1; + else + cur_col++; + + move_cursor(cur_col, -(cur_line.length()-cur_pos+1), num_cols, key_seqs); + } + + eaten++; + } + else if (keycodes[eaten] == '\n'){ // return key + int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) + cur_col = num_cols; + + move_cursor(cur_col, cur_line.length()-cur_pos, num_cols, key_seqs); + + std::cout.put(keycodes[eaten]); + cur_line.append(1, '\n'); + cur_pos = 0; + break; + } + else { // all other key + std::cout.put(keycodes[eaten]); + std::cout.write(&(cur_line.c_str()[cur_pos]), cur_line.length()-cur_pos); + + cur_line.insert(cur_pos, &keycodes[eaten], 1); + cur_pos++; + + int cur_col = (cur_line.length() + strlen(PROMPT_STRING) + 1) % num_cols; + if (cur_col == 0) { + // force cursor to move to the next line when the last printed char is at + // the right boundary of the terminal + std::cout.put(' '); + std::cout.put('\b'); + + cur_col = 1; + } + else + cur_col++; + + move_cursor(cur_col, -(cur_line.length()-cur_pos), num_cols, key_seqs); + + eaten++; + } + + std::cout.flush(); + } + } +#else + return yyFlexLexer::LexerInput(buf, max_size); +#endif +} diff --git a/omegalib/omegacalc/src/parser.l b/omegalib/omegacalc/src/parser.l new file mode 100644 index 0000000..ac2b448 --- /dev/null +++ b/omegalib/omegacalc/src/parser.l @@ -0,0 +1,350 @@ +%{ +#include <stdio.h> +#include <string> +#include <sstream> +#include <iostream> +#include <omega_calc/AST.h> +#include <basic/Dynamic_Array.h> + +using namespace omega; +#include "y.tab.h" + +#define BUFFER scanBuf += yytext +std::string scanBuf; +std::string err_msg; + +extern "C" int yywrap() {return 1;}; + + +#define MAX_INCLUDE_DEPTH 10 +YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH]; +int include_stack_ptr = 0; +int comment_caller; + +extern bool is_interactive; +extern const char *PROMPT_STRING; +extern bool need_coef; + +// void yyerror(const char *s); +void yyerror(const std::string &s); +void flushScanBuffer(); + +%} + +%s LATEX INCLUDE COMMENT +%option yylineno + +%% + +"<<" { BUFFER; BEGIN(INCLUDE); } +<INCLUDE>[^>\n ]+">>" { + BUFFER; + scanBuf += "\n"; + flushScanBuffer(); + + if (include_stack_ptr >= MAX_INCLUDE_DEPTH) { + fprintf(stderr, "File including nested too deeply, abort"); + exit(1); + } + + char *s = yytext; + while (*s != '>') s++; + *s = '\0'; + FILE *f = fopen(yytext, "r"); + if (!f) { + fprintf(stderr, "Can't open file %s\n", yytext); + } + else { + include_stack[include_stack_ptr++] = YY_CURRENT_BUFFER; + yyin = f; + yy_switch_to_buffer(yy_create_buffer(yyin, YY_BUF_SIZE)); + } + BEGIN(INITIAL); +} +<INCLUDE>[ \n] { + fprintf(stderr,"Error in include syntax\n"); + fprintf(stderr,"Use <<fname>> to include the file named fname\n"); + BEGIN(INITIAL); + if(is_interactive && include_stack_ptr == 0) + printf("%s ", PROMPT_STRING); +} + +<COMMENT>\n { + BUFFER; + BEGIN(comment_caller); + if(is_interactive && include_stack_ptr == 0) + printf("%s ", PROMPT_STRING); +} + +\n { + BUFFER; + if(is_interactive && include_stack_ptr == 0) + printf("%s ", PROMPT_STRING); +} + +<LATEX>"\\ " { BUFFER; } +[ \t]+ { BUFFER; } +# { BUFFER; comment_caller = YY_START; BEGIN(COMMENT); } +<COMMENT>.* { BUFFER; flushScanBuffer(); } +<LATEX>"\$\$" { BUFFER; BEGIN(INITIAL); } +"\$\$" { BUFFER; BEGIN(LATEX); } +<LATEX>"\\t" { BUFFER; } +<LATEX>"\\!" { BUFFER; } +<LATEX>"\\\\" { BUFFER; } + +"{" { BUFFER; return OPEN_BRACE; } +<LATEX>"\\{" { BUFFER; return OPEN_BRACE; } +"}" { BUFFER; return CLOSE_BRACE; } +<LATEX>"\\}" { BUFFER; return CLOSE_BRACE; } +"approximate" { BUFFER; return APPROX; } +"union" { BUFFER; return UNION; } +<LATEX>"\\cup" { BUFFER; return UNION; } +"intersection" { BUFFER; return INTERSECTION; } +<LATEX>"\\cap" { BUFFER; return INTERSECTION; } +"symbolic" { BUFFER; return SYMBOLIC; } +"sym" { BUFFER; return SYMBOLIC; } +<LATEX>"\\mid" { BUFFER; return VERTICAL_BAR; } +<LATEX>"|" { BUFFER; return VERTICAL_BAR; } +<LATEX>"\\st" { BUFFER; return SUCH_THAT; } +"s.t." { BUFFER; return SUCH_THAT; } +"inverse" { BUFFER; return INVERSE; } +"complement" { BUFFER; return COMPLEMENT; } +<LATEX>"\\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; } +<LATEX>"\\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; } +<LATEX>"\\forall" { BUFFER; return FORALL; } +"forall" { BUFFER; return FORALL; } +<LATEX>"\\exists" { BUFFER; return EXISTS; } +"exists" { BUFFER; return EXISTS; } + +"Venn" { BUFFER; return VENN; } +"ConvexRepresentation" { BUFFER; return CONVEX_REPRESENTATION; } +"ConvexCombination" { BUFFER; return CONVEX_COMBINATION; } +"PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; } +"LinearCombination" { BUFFER; return LINEAR_COMBINATION; } +"AffineCombination" { BUFFER; return AFFINE_COMBINATION; } +"RectHull" { BUFFER; return RECT_HULL; } +"ConvexHull" { BUFFER; return CONVEX_HULL; } +"DecoupledConvexHull" { BUFFER; return DECOUPLED_CONVEX_HULL; } +"AffineHull" { BUFFER; return AFFINE_HULL; } +"ConicHull" { BUFFER; return CONIC_HULL; } +"LinearHull" { BUFFER; return LINEAR_HULL; } +"PairwiseCheck" { /*deprecated*/ BUFFER; return PAIRWISE_CHECK; } +"ConvexCheck" { /*deprecated*/ BUFFER; return CONVEX_CHECK; } +"QuickHull" { /*deprecated*/ BUFFER; return QUICK_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; } +"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;} +"reachable" { BUFFER; return REACHABLE_FROM; } +"reachable of" { BUFFER; return REACHABLE_OF; } +"restrict_domain" { BUFFER; return RESTRICT_DOMAIN; } +"restrictDomain" { BUFFER; return RESTRICT_DOMAIN; } +<LATEX>"\\" { 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; } + +"/" { BUFFER; return RESTRICT_RANGE; } +"&" { BUFFER; return AND; } +"|" { BUFFER; return OR; } +"&&" { BUFFER; return AND; } +"||" { BUFFER; return OR; } +"and" { BUFFER; return AND; } +"or" { BUFFER; return OR; } +<LATEX>"\\land" { BUFFER; return AND; } +<LATEX>"\\lor" { BUFFER; return OR; } +"!" { BUFFER; return NOT; } +"not" { BUFFER; return NOT; } +<LATEX>"\\neg" { BUFFER; return NOT; } +":=" { BUFFER; return IS_ASSIGNED; } +"->" { BUFFER; return GOES_TO; } +"in" { BUFFER; return IN; } +<LATEX>"\\rightarrow" { BUFFER; return GOES_TO; } +"<=" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; } +<LATEX>"\\leq" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; } +<LATEX>"\\le" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; } +">=" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; } +<LATEX>"\\geq" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; } +<LATEX>"\\ge" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; } +"!=" { BUFFER; yylval.REL_OPERATOR = neq; return REL_OP; } +<LATEX>"\\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; } +"==" { 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 = new char[yyleng+1]; + 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 = new char[yyleng+1]; + 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 = new char[yyleng+1]; + 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 = new char[yyleng+1]; + 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; +} +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]* { + BUFFER; + if (yyleng > 19) yyerror("Identifier too long"); + yylval.VAR_NAME = new char[yyleng+1]; + strcpy(yylval.VAR_NAME,yytext); + return VAR; + } +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(in)" { + BUFFER; + if (yyleng > 19) yyerror("Identifier too long"); + yylval.VAR_NAME = new char[yyleng+1]; + strcpy(yylval.VAR_NAME,yytext); + yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase + yylval.VAR_NAME[yyleng-2] = 'n'; + return VAR; + } +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(set)" { + BUFFER; + if (yyleng > 19) yyerror("Identifier too long"); + yylval.VAR_NAME = new char[yyleng+1]; + 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; + } +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(out)" { + BUFFER; + if (yyleng > 19) yyerror("Identifier too long"); + yylval.VAR_NAME = new char[yyleng+1]; + 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; + if (need_coef) { + sscanf(yytext, coef_fmt, &yylval.COEF_VALUE); + return COEF; + } + else { + yylval.INT_VALUE = atoi(yytext); + return INT; + } +} + +\"[^\"]*\" { BUFFER; + yytext[strlen(yytext)-1]='\0'; + yylval.STRING_VALUE = new std::string(yytext+1); + return STRING; +} + + +<<EOF>> { + if (--include_stack_ptr < 0) { + flushScanBuffer(); + return yytext[0]; + } + yy_delete_buffer(YY_CURRENT_BUFFER); + yy_switch_to_buffer(include_stack[include_stack_ptr]); +} + +. { BUFFER; return yytext[0]; } + + +%% + +void yyerror(const std::string &s) { + std::stringstream ss; + if (is_interactive && include_stack_ptr == 0) + ss << s << "\n"; + else + ss << s << " at line " << yylineno << "\n"; + err_msg = ss.str(); +} + + +void flushScanBuffer() { + if (scanBuf.size() == 0) + return; + if (!is_interactive || include_stack_ptr > 0) { + size_t prev_pos = 0; + if (scanBuf[0] == '\n') + prev_pos = 1; + for (size_t pos = prev_pos; pos <= scanBuf.size(); pos++) { + if (pos == scanBuf.size() || scanBuf[pos] == '\n') { + std::cout << PROMPT_STRING << " " << scanBuf.substr(prev_pos, pos-prev_pos) << std::endl; + prev_pos = pos+1; + } + } + } + + scanBuf.clear(); +} diff --git a/omegalib/omegacalc/src/parser.ll b/omegalib/omegacalc/src/parser.ll new file mode 100755 index 0000000..86de3a4 --- /dev/null +++ b/omegalib/omegacalc/src/parser.ll @@ -0,0 +1,350 @@ +/***************************************************************************** + Copyright (C) 1994-2000 the Omega Project Team + Copyright (C) 2005-2011 Chun Chen + All Rights Reserved. + + Purpose: + lex parser for calculator. + + Notes: + + History: + 02/04/11 migrate to flex c++ mode, Chun Chen +*****************************************************************************/ + +%{ +#include <stdio.h> +#include <string.h> +#include <string> +#include <sstream> +#include <iostream> +#include <fstream> +#include <omega_calc/AST.h> +#include <basic/Dynamic_Array.h> +#include "parser.tab.hh" +#include <omega_calc/myflex.h> + +myFlexLexer mylexer; +bool is_interactive; +const char *PROMPT_STRING = ">>>"; + +#define BUFFER scanBuf += yytext +std::string scanBuf; +std::string err_msg; + +extern bool need_coef; + +void yyerror(const std::string &s); +void flushScanBuffer(); + +%} + +%s LATEX INCLUDE COMMENT +%option yylineno +%option noyywrap + +%% + +"<<" { BUFFER; BEGIN(INCLUDE); } +<INCLUDE>[^>\n ]+">>" { + BUFFER; + scanBuf += "\n"; + flushScanBuffer(); + + if (is_interactive) { + std::cout << "file include disabled in interactive mode\n"; + } + else { + char *s = yytext; + while (*s != '>') s++; + *s = '\0'; + std::ifstream *ifs = new std::ifstream(yytext, std::ifstream::in); + if (!ifs->is_open()) { + fprintf(stderr, "Can't open file %s\n", yytext); + } + else { + yy_buffer_state *bs = mylexer.yy_create_buffer(ifs, 8092); + mylexer.yypush_buffer_state(bs); + } + } + BEGIN(INITIAL); +} +<INCLUDE>[ \n] { + std::cout << "Error in include syntax\n"; + std::cout << "Use <<fname>> to include the file named fname\n"; + BEGIN(INITIAL); + if(is_interactive) { + std::cout << PROMPT_STRING << ' '; + std::cout.flush(); + } +} + + + + + +<LATEX>"\\ " { BUFFER; } +[ \t]+ { BUFFER; } +# { BUFFER; BEGIN(COMMENT); } +<COMMENT>.* { BUFFER; } +<LATEX>"\$\$\n" { BUFFER; BEGIN(INITIAL); } +<LATEX>"\$\$" { BUFFER; BEGIN(INITIAL); } +"\$\$" { BUFFER; BEGIN(LATEX); } +<LATEX>"\\n" { BUFFER; } +<LATEX>"\\t" { BUFFER; } +<LATEX>"\\!" { BUFFER; } +<LATEX>"\\\\" { BUFFER; } +<LATEX>"\n" { BUFFER; } + + +\n { + BUFFER; + BEGIN(INITIAL); + if(is_interactive) { + std::cout << PROMPT_STRING << ' '; + std::cout.flush(); + } +} + + + + + +"{" { BUFFER; return OPEN_BRACE; } +<LATEX>"\\{" { BUFFER; return OPEN_BRACE; } +"}" { BUFFER; return CLOSE_BRACE; } +<LATEX>"\\}" { BUFFER; return CLOSE_BRACE; } +"approximate" { BUFFER; return APPROX; } +"union" { BUFFER; return UNION; } +<LATEX>"\\cup" { BUFFER; return UNION; } +"intersection" { BUFFER; return INTERSECTION; } +<LATEX>"\\cap" { BUFFER; return INTERSECTION; } +"without_simplify" { BUFFER; return NO_SIMPLIFY; } +"symbolic" { BUFFER; return SYMBOLIC; } +"sym" { BUFFER; return SYMBOLIC; } +<LATEX>"\\mid" { BUFFER; return VERTICAL_BAR; } +<LATEX>"|" { BUFFER; return VERTICAL_BAR; } +<LATEX>"\\st" { BUFFER; return SUCH_THAT; } +"s.t." { BUFFER; return SUCH_THAT; } +"inverse" { BUFFER; return INVERSE; } +"complement" { BUFFER; return COMPLEMENT; } +<LATEX>"\\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; } +<LATEX>"\\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; } +<LATEX>"\\forall" { BUFFER; return FORALL; } +"forall" { BUFFER; return FORALL; } +<LATEX>"\\exists" { BUFFER; return EXISTS; } +"exists" { BUFFER; return EXISTS; } + +"Venn" { BUFFER; return VENN; } +"ConvexRepresentation" { BUFFER; return CONVEX_REPRESENTATION; } +"ConvexCombination" { BUFFER; return CONVEX_COMBINATION; } +"PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; } +"LinearCombination" { BUFFER; return LINEAR_COMBINATION; } +"AffineCombination" { BUFFER; return AFFINE_COMBINATION; } +"RectHull" { /*deprecated*/ BUFFER; return RECT_HULL; } +"SimpleHull" { BUFFER; return SIMPLE_HULL; } +"ConvexHull" { BUFFER; return CONVEX_HULL; } +"DecoupledConvexHull" { BUFFER; return DECOUPLED_CONVEX_HULL; } +"AffineHull" { BUFFER; return AFFINE_HULL; } +"ConicHull" { BUFFER; return CONIC_HULL; } +"LinearHull" { BUFFER; return LINEAR_HULL; } +"PairwiseCheck" { /*deprecated*/ BUFFER; return PAIRWISE_CHECK; } +"ConvexCheck" { /*deprecated*/ BUFFER; return CONVEX_CHECK; } +"QuickHull" { /*deprecated*/ BUFFER; return QUICK_HULL; } +"Hull" { BUFFER; return HULL; } +"farkas" { BUFFER; return FARKAS; } +"decoupledfarkas" { BUFFER; return DECOUPLED_FARKAS; } +"decoupled-farkas" { BUFFER; return DECOUPLED_FARKAS; } +"decoupled_farkas" { BUFFER; return DECOUPLED_FARKAS; } + +"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; } +"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;} +"reachable" { BUFFER; return REACHABLE_FROM; } +"reachable of" { BUFFER; return REACHABLE_OF; } +"restrict_domain" { BUFFER; return RESTRICT_DOMAIN; } +"restrictDomain" { BUFFER; return RESTRICT_DOMAIN; } +"\\" { 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; } + +"/" { BUFFER; return RESTRICT_RANGE; } +"&" { BUFFER; return AND; } +"|" { BUFFER; return OR; } +"&&" { BUFFER; return AND; } +"||" { BUFFER; return OR; } +"and" { BUFFER; return AND; } +"or" { BUFFER; return OR; } +<LATEX>"\\land" { BUFFER; return AND; } +<LATEX>"\\lor" { BUFFER; return OR; } +"!" { BUFFER; return NOT; } +"not" { BUFFER; return NOT; } +<LATEX>"\\neg" { BUFFER; return NOT; } +":=" { BUFFER; return IS_ASSIGNED; } +"->" { BUFFER; return GOES_TO; } +"in" { BUFFER; return IN; } +<LATEX>"\\rightarrow" { BUFFER; return GOES_TO; } +"<=" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; } +<LATEX>"\\leq" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; } +<LATEX>"\\le" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; } +">=" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; } +<LATEX>"\\geq" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; } +<LATEX>"\\ge" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; } +"!=" { BUFFER; yylval.REL_OPERATOR = neq; return REL_OP; } +<LATEX>"\\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; } +"==" { BUFFER; yylval.REL_OPERATOR = eq; return REL_OP; } + +[A-Za-z_][A-Za-z0-9_]*[\']* { + BUFFER; + yylval.VAR_NAME = new char[yyleng+1]; + strcpy(yylval.VAR_NAME,yytext); + return VAR; +} +[A-Za-z][A-Za-z0-9_]*"(In)" { + BUFFER; + yylval.VAR_NAME = new char[yyleng+1]; + 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; + yylval.VAR_NAME = new char[yyleng+1]; + 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; + yylval.VAR_NAME = new char[yyleng+1]; + 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; +} +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]* { + BUFFER; + yylval.VAR_NAME = new char[yyleng+1]; + strcpy(yylval.VAR_NAME,yytext); + return VAR; + } +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(In)" { + BUFFER; + yylval.VAR_NAME = new char[yyleng+1]; + strcpy(yylval.VAR_NAME,yytext); + yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase + yylval.VAR_NAME[yyleng-2] = 'n'; + return VAR; + } +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(Set)" { + BUFFER; + yylval.VAR_NAME = new char[yyleng+1]; + 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; + } +<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(Out)" { + BUFFER; + yylval.VAR_NAME = new char[yyleng+1]; + 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; + if (need_coef) { + sscanf(yytext, coef_fmt, &yylval.COEF_VALUE); + return COEF; + } + else { + yylval.INT_VALUE = atoi(yytext); + return INT; + } +} + +\"[^\"]*\" { BUFFER; + yytext[yyleng-1]='\0'; + yylval.STRING_VALUE = new std::string(yytext+1); + return STRING; +} + + +<<EOF>> { + mylexer.yypop_buffer_state(); + if (!YY_CURRENT_BUFFER) { + flushScanBuffer(); + return YY_NULL; + } +} + +. { BUFFER; return yytext[0]; } + + +%% + +void flushScanBuffer() { + if (scanBuf.size() == 0) + return; + if (!is_interactive) { + size_t prev_pos = 0; + if (scanBuf[0] == '\n') + prev_pos = 1; + for (size_t pos = prev_pos; pos <= scanBuf.size(); pos++) { + if (pos == scanBuf.size() || scanBuf[pos] == '\n') { + std::cout << PROMPT_STRING << " " << scanBuf.substr(prev_pos, pos-prev_pos) << std::endl; + prev_pos = pos+1; + } + } + } + + scanBuf.clear(); +} diff --git a/omegalib/omegacalc/src/parser.y b/omegalib/omegacalc/src/parser.y new file mode 100644 index 0000000..7369b94 --- /dev/null +++ b/omegalib/omegacalc/src/parser.y @@ -0,0 +1,1925 @@ +/***************************************************************************** + 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/Dynamic_Array.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, ¤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 + +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; + Dynamic_Array2<Relation> * RELATION_ARRAY_2D; + Dynamic_Array1<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(); + Dynamic_Array1<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 { + Dynamic_Array1<Relation> *final = Reachable_Nodes(reachable_info); + $$ = final; + } +; + +reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList { + Dynamic_Array1<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; + Dynamic_Array2<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 */ + Dynamic_Array1<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; +} diff --git a/omegalib/omegacalc/src/parser.yy b/omegalib/omegacalc/src/parser.yy new file mode 100755 index 0000000..896f926 --- /dev/null +++ b/omegalib/omegacalc/src/parser.yy @@ -0,0 +1,1928 @@ +/***************************************************************************** + Copyright (C) 1994-2000 the Omega Project Team + Copyright (C) 2005-2011 Chun Chen + All Rights Reserved. + + Purpose: + yacc parser for calculator. + + Notes: + + History: + 02/04/11 work with flex c++ mode, Chun Chen +*****************************************************************************/ + +%{ +//#define YYDEBUG 1 +#include <basic/Dynamic_Array.h> +#include <basic/Iterator.h> +#include <omega_calc/AST.h> +#include <omega/hull.h> +#include <omega/closure.h> +#include <omega/reach.h> +#include <string> +#include <iostream> +#include <fstream> +#include "parser.tab.hh" +#include <omega_calc/myflex.h> +//#include <stdio.h> + +#if defined __USE_POSIX +#include <unistd.h> +#elif defined __WIN32 +#include <io.h> +#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 + + + + +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, ¤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 + + +#ifdef BUILD_CODEGEN +#include <code_gen/codegen.h> +#endif + +extern myFlexLexer mylexer; +#define yylex mylexer.yylex + + + + +int omega_calc_debug = 0; + +extern bool is_interactive; +extern const char *PROMPT_STRING; +bool simplify = true; +using namespace omega; + +extern std::string err_msg; + +bool need_coef; + +namespace { + int redundant_conj_level = 2; // default maximum 2 + int redundant_constr_level = 4; // default maximum 4 +} + +std::map<std::string, Relation *> relationMap; +int argCount = 0; +int tuplePos = 0; +Argument_Tuple currentTuple = Input_Tuple; + +Relation LexForward(int n); +reachable_information *reachable_info; + +void yyerror(const std::string &s); +void flushScanBuffer(); + +%} + +%union { + int INT_VALUE; + omega::coef_t COEF_VALUE; + Rel_Op REL_OPERATOR; + char *VAR_NAME; + std::set<char *> *VAR_LIST; + Exp *EXP; + std::set<Exp *> *EXP_LIST; + AST *ASTP; + omega::Argument_Tuple ARGUMENT_TUPLE; + AST_constraints *ASTCP; + Declaration_Site *DECLARATION_SITE; + omega::Relation *RELATION; + tupleDescriptor *TUPLE_DESCRIPTOR; + std::pair<std::vector<omega::Relation>, std::vector<omega::Relation> > *REL_TUPLE_PAIR; + omega::Dynamic_Array1<omega::Relation> * RELATION_ARRAY_1D; + 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 NO_SIMPLIFY +%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 SIMPLE_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 <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 $$;} exp simpleExp +%destructor { + for (std::set<Exp *>::iterator i = $$->begin(); i != $$->end(); i++) + delete *i; + delete $$; + } expList; +%destructor { + for (std::set<char *>::iterator i = $$->begin(); i != $$->end(); i++) + delete []*i; + delete $$; + } varList; + +%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*/ + | NO_SIMPLIFY ';'{ + simplify = false; + } + | 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 { + if(simplify) + $3->simplify(redundant_conj_level, redundant_constr_level); + else + $3->simplify(); + Relation *r = relationMap[std::string($1)]; + if (r != NULL) delete r; + relationMap[std::string($1)] = $3; + } + catch(const std::exception &e){ + std::cout << e.what() << std::endl; + } + + delete []$1; + } + | relation ';' { + flushScanBuffer(); + if(simplify) + $1->simplify(redundant_conj_level, redundant_constr_level); + else + $1->simplify(); + $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 relPairList context';' { + flushScanBuffer(); +#ifdef BUILD_CODEGEN + try { + CodeGen cg($2->first, $2->second, *$3); + CG_result *cgr = cg.buildAST(); + if (cgr != NULL) { + std::string s = cgr->printString(); + std::cout << s << std::endl; + delete cgr; + } + else + std::cout << "/* empty */" << std::endl; + } + catch (const std::exception &e) { + std::cout << e.what() << std::endl; + } +#else + std::cout << "CodeGen package not built" << std::endl; +#endif + delete $3; + delete $2; + } + | CODEGEN INT relPairList context';' { + flushScanBuffer(); +#ifdef BUILD_CODEGEN + try { + CodeGen cg($3->first, $3->second, *$4); + CG_result *cgr = cg.buildAST($2); + if (cgr != NULL) { + std::string s = cgr->printString(); + std::cout << s << std::endl; + delete cgr; + } + else + std::cout << "/* empty */" << std::endl; + } + catch (const std::exception &e) { + std::cout << e.what() << std::endl; + } +#else + std::cout << "CodeGen package not built" << std::endl; +#endif + delete $4; + delete $3; + } + | reachable ';' { + flushScanBuffer(); + Dynamic_Array1<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 " << 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; + } +; + + +context : {$$ = new Relation(); *$$ = Relation::Null();} + | GIVEN relation {$$ = $2; } +; + +relPairList : relPairList ',' relation ':' relation { + try { + $1->first.push_back(*$3); + $1->second.push_back(*$5); + } + catch (const std::exception &e) { + delete $1; + delete $3; + delete $5; + yyerror(e.what()); + YYERROR; + } + delete $3; + delete $5; + $$ = $1; + } + | relPairList ',' relation { + try { + $1->first.push_back(Identity($3->n_set())); + $1->second.push_back(*$3); + } + catch (const std::exception &e) { + delete $1; + delete $3; + yyerror(e.what()); + YYERROR; + } + delete $3; + $$ = $1; + } + | relation ':' relation { + std::pair<std::vector<Relation>, std::vector<Relation> > *rtp = new std::pair<std::vector<Relation>, std::vector<Relation> >(); + try { + rtp->first.push_back(*$1); + rtp->second.push_back(*$3); + } + catch (const std::exception &e) { + delete rtp; + delete $1; + delete $3; + yyerror(e.what()); + YYERROR; + } + delete $1; + delete $3; + $$ = rtp; + } + | relation { + std::pair<std::vector<Relation>, std::vector<Relation> > *rtp = new std::pair<std::vector<Relation>, std::vector<Relation> >(); + try { + rtp->first.push_back(Identity($1->n_set())); + rtp->second.push_back(*$1); + } + 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; + current_Declaration_Site = globalDecls; + delete relationDecl; + relationDecl = NULL; + } + | VAR { + Relation *r = relationMap[std::string($1)]; + 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; + } + | SIMPLE_HULL relation %prec p8 { + $$ = new Relation(); + try { + *$$ = SimpleHull(*$2, true, true); + } + catch (const std::exception &e) { + delete $$; + delete $2; + yyerror(e.what()); + YYERROR; + } + delete $2; + } + | HULL relation %prec p8 { + $$ = new Relation(); + try { + *$$ = Hull(*$2,true,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,true,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-1]->vid = r->input_var(i); + if (!$1->vars[i-1]->anonymous) + r->name_input_var(i, $1->vars[i-1]->stripped_name); + } + for(int i = 1; i <= $4->size; i++) { + $4->vars[i-1]->vid = r->output_var(i); + if (!$4->vars[i-1]->anonymous) + r->name_output_var(i, $4->vars[i-1]->stripped_name); + } + r->setup_names(); + for (std::set<Exp *>::iterator i = $1->eq_constraints.begin(); i != $1->eq_constraints.end(); i++) + install_eq(f, *i, 0); + for (std::set<Exp *>::iterator i = $1->geq_constraints.begin(); i != $1->geq_constraints.end(); i++) + install_geq(f, *i, 0); + for (std::set<strideConstraint *>::iterator i = $1->stride_constraints.begin(); i != $1->stride_constraints.end(); i++) + install_stride(f, *i); + for (std::set<Exp *>::iterator i = $4->eq_constraints.begin(); i != $4->eq_constraints.end(); i++) + install_eq(f, *i, 0); + for (std::set<Exp *>::iterator i = $4->geq_constraints.begin(); i != $4->geq_constraints.end(); i++) + install_geq(f, *i, 0); + for (std::set<strideConstraint *>::iterator i = $4->stride_constraints.begin(); i != $4->stride_constraints.end(); i++) + install_stride(f, *i); + 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-1]->vid = r->set_var(i); + if (!$1->vars[i-1]->anonymous) + r->name_set_var(i, $1->vars[i-1]->stripped_name); + } + r->setup_names(); + for (std::set<Exp *>::iterator i = $1->eq_constraints.begin(); i != $1->eq_constraints.end(); i++) + install_eq(f, *i, 0); + for (std::set<Exp *>::iterator i = $1->geq_constraints.begin(); i != $1->geq_constraints.end(); i++) + install_geq(f, *i, 0); + for (std::set<strideConstraint *>::iterator i = $1->stride_constraints.begin(); i != $1->stride_constraints.end(); i++) + install_stride(f, *i); + 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 std::set<char *>(); $$->insert($1); $1 = NULL;} +; + +varDecl : varList { + $$ = current_Declaration_Site = new Declaration_Site($1); + for (std::set<char *>::iterator i = $1->begin(); i != $1->end(); i++) + delete [](*i); + 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 std::set<Exp *>(); $$->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 { + try { + $$ = multiply($1,$3); + } + catch (const std::exception &e) { + yyerror(e.what()); + YYERROR; + } + } +; + + +reachable : REACHABLE_FROM nodeNameList nodeSpecificationList { + Dynamic_Array1<Relation> *final = Reachable_Nodes(reachable_info); + $$ = final; + } +; + +reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList { + Dynamic_Array1<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; + Dynamic_Array2<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 */ + Dynamic_Array1<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 yyerror(const std::string &s) { + std::stringstream ss; + if (is_interactive) + ss << s << "\n"; + else + ss << s << " at line " << mylexer.lineno() << "\n"; + err_msg = ss.str(); +} + + +int main(int argc, char **argv) { + if (argc > 2){ + fprintf(stderr, "Usage: %s [script_file]\n", argv[0]); + exit(1); + } + + if (argc == 2) { + std::ifstream *ifs = new std::ifstream; + ifs->open(argv[1], std::ifstream::in); + if (!ifs->is_open()) { + fprintf(stderr, "can't open input file %s\n", argv[1]); + exit(1); + } + yy_buffer_state *bs = mylexer.yy_create_buffer(ifs, 8092); + mylexer.yypush_buffer_state(bs); + } + + //yydebug = 1; + is_interactive = false; + if (argc == 1) { +#if defined __USE_POSIX + if (isatty((int)fileno(stdin))) + is_interactive = true; +#elif defined __WIN32 + if (_isatty(_fileno(stdin))) + is_interactive = true; +#endif + } + + if (is_interactive) { +#ifdef BUILD_CODEGEN + std::cout << "Omega+ and CodeGen+ "; +#else + std::cout << "Omega+ "; +#endif + std::cout << "v" OC_VERSION " (built on " OC_BUILD_DATE ")" << std::endl; + std::cout << "Copyright (C) 1994-2000 the Omega Project Team" << std::endl; + std::cout << "Copyright (C) 2005-2011 Chun Chen" << std::endl; + std::cout << "Copyright (C) 2011-2012 University of Utah" << std::endl; + std::cout << PROMPT_STRING << ' '; + std::cout.flush(); + } + + 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; + } + + for (std::map<std::string, Relation *>::iterator i = relationMap.begin(); i != relationMap.end(); i++) + delete (*i).second; + delete globalDecls; + + 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; +} |