diff options
author | Tuowen Zhao <ztuowen@gmail.com> | 2016-09-19 11:52:51 -0600 |
---|---|---|
committer | Tuowen Zhao <ztuowen@gmail.com> | 2016-09-19 11:52:51 -0600 |
commit | 372c92e7c1901dd7bdd1d2fd48bff205c31dca2d (patch) | |
tree | 439073a6481f50b26e2e881999cc568619628987 /omegalib/omegacalc/src | |
parent | 62f7acd88465f4f20b9b25c3f7edd4e3b7ce453b (diff) | |
download | chill-372c92e7c1901dd7bdd1d2fd48bff205c31dca2d.tar.gz chill-372c92e7c1901dd7bdd1d2fd48bff205c31dca2d.tar.bz2 chill-372c92e7c1901dd7bdd1d2fd48bff205c31dca2d.zip |
remove omegacalc as subproject
Diffstat (limited to 'omegalib/omegacalc/src')
-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 |
6 files changed, 0 insertions, 5441 deletions
diff --git a/omegalib/omegacalc/src/AST.cc b/omegalib/omegacalc/src/AST.cc deleted file mode 100644 index 1f885a6..0000000 --- a/omegalib/omegacalc/src/AST.cc +++ /dev/null @@ -1,467 +0,0 @@ -/***************************************************************************** - 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 deleted file mode 100755 index 89a2544..0000000 --- a/omegalib/omegacalc/src/myflex.cc +++ /dev/null @@ -1,421 +0,0 @@ -/***************************************************************************** - 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 deleted file mode 100644 index 04933f4..0000000 --- a/omegalib/omegacalc/src/parser.l +++ /dev/null @@ -1,350 +0,0 @@ -%{ -#include <stdio.h> -#include <string> -#include <sstream> -#include <iostream> -#include <omega_calc/AST.h> -#include <basic/DynamicArray.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 deleted file mode 100755 index e095f24..0000000 --- a/omegalib/omegacalc/src/parser.ll +++ /dev/null @@ -1,350 +0,0 @@ -/***************************************************************************** - 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/DynamicArray.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 deleted file mode 100644 index d365797..0000000 --- a/omegalib/omegacalc/src/parser.y +++ /dev/null @@ -1,1925 +0,0 @@ -/***************************************************************************** - Copyright (C) 1994-2000 University of Maryland. - Copyright (C) 2008 University of Southern California. - Copyright (C) 2009-2010 University of Utah. - All Rights Reserved. - - Purpose: - omega calculator yacc parser. - - Notes: - - History: -*****************************************************************************/ - -%{ - -#include <basic/DynamicArray.h> -#include <basic/Iterator.h> -#include <code_gen/code_gen.h> -#include <omega_calc/AST.h> -#include <omega/hull.h> -#include <omega/closure.h> -#include <omega/reach.h> -#include <string> -#include <iostream> - -#ifdef WIN32 -#include <io.h> -#define isatty _isatty -#define alloca _alloca -#endif -#ifndef WIN32 -#include <sys/time.h> -#include <sys/resource.h> -#endif -#if !defined(OMIT_GETRUSAGE) -#include <sys/types.h> -#include <sys/time.h> -#include <sys/resource.h> -#endif - -#if !defined(OMIT_GETRUSAGE) -#ifdef __sparc__ -extern "C" int getrusage (int, struct rusage*); -#endif - -using namespace omega; - -struct rusage start_time; -bool anyTimingDone = false; - -void start_clock( void ) { - getrusage(RUSAGE_SELF, &start_time); -} - -int clock_diff( void ) { - struct rusage current_time; - getrusage(RUSAGE_SELF, ¤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; - DynamicArray2<Relation> * RELATION_ARRAY_2D; - DynamicArray1<Relation> * RELATION_ARRAY_1D; - Tuple<std::string> *STRING_TUPLE; - std::string *STRING_VALUE; -} - -%token <VAR_NAME> VAR -%token <INT_VALUE> INT -%token <COEF_VALUE> COEF -%token <STRING_VALUE> STRING -%token OPEN_BRACE CLOSE_BRACE -%token SYMBOLIC -%token OR AND NOT -%token ST APPROX -%token IS_ASSIGNED -%token FORALL EXISTS -%token DOMAIN RANGE -%token DIFFERENCE DIFFERENCE_TO_RELATION -%token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE -%token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION LINEAR_COMBINATION AFFINE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL QUICK_HULL PAIRWISE_CHECK CONVEX_CHECK CONVEX_REPRESENTATION RECT_HULL DECOUPLED_CONVEX_HULL -%token MAXIMIZE_RANGE MINIMIZE_RANGE -%token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN -%token LEQ GEQ NEQ -%token GOES_TO -%token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE -%token UNION INTERSECTION -%token VERTICAL_BAR SUCH_THAT -%token SUBSET CODEGEN DECOUPLED_FARKAS FARKAS -%token MAKE_UPPER_BOUND MAKE_LOWER_BOUND -%token <REL_OPERATOR> REL_OP -%token RESTRICT_DOMAIN RESTRICT_RANGE -%token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE -%token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF -%token ASSERT_UNSAT -%token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION - -%type <INT_VALUE> effort -%type <EXP> exp simpleExp -%type <EXP_LIST> expList -%type <VAR_LIST> varList -%type <ARGUMENT_TUPLE> argumentList -%type <ASTP> formula optionalFormula -%type <ASTCP> constraintChain -%type <TUPLE_DESCRIPTOR> tupleDeclaration -%type <DECLARATION_SITE> varDecl varDeclOptBrackets -%type <RELATION> relation builtRelation context -%type <RELATION> reachable_of -%type <REL_TUPLE_PAIR> relPairList -%type <RELATION_ARRAY_1D> reachable - -%destructor {delete []$$;} VAR -%destructor {delete $$;} STRING -%destructor {delete $$;} relation builtRelation tupleDeclaration formula optionalFormula context reachable_of constraintChain varDecl varDeclOptBrackets relPairList reachable -%destructor {delete $$;} varList exp simpleExp -%destructor { - foreach(e, Exp *, *$$, delete e); - delete $$; - } expList; - -%nonassoc ASSERT_UNSAT -%left UNION p1 '+' '-' -%nonassoc SUPERSETOF SUBSETOF -%left p2 RESTRICT_DOMAIN RESTRICT_RANGE -%left INTERSECTION p3 '*' '@' -%left p4 -%left OR p5 -%left AND p6 -%left COMPOSE JOIN CARRIED_BY -%right NOT APPROX DOMAIN RANGE HULL PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS DIFFERENCE DIFFERENCE_TO_RELATION INVERSE COMPLEMENT FARKAS SAMPLE SYM_SAMPLE MAKE_UPPER_BOUND MAKE_LOWER_BOUND p7 -%left p8 -%nonassoc GIVEN -%left p9 -%left '(' p10 - -%% - -inputSequence : /*empty*/ - | inputSequence { assert( current_Declaration_Site == globalDecls);} - inputItem -; - -inputItem : ';' /*empty*/ - | error ';' { - flushScanBuffer(); - std::cout << err_msg; - err_msg.clear(); - current_Declaration_Site = globalDecls; - need_coef = false; - std::cout << "...skipping to statement end..." << std::endl; - delete relationDecl; - relationDecl = NULL; - } - | SYMBOLIC globVarList ';' {flushScanBuffer();} - | VAR IS_ASSIGNED relation ';' { - flushScanBuffer(); - try { - $3->simplify(redundant_conj_level, redundant_constr_level); - Relation *r = relationMap((Const_String)$1); - if (r) delete r; - relationMap[(Const_String)$1] = $3; - } - catch (const std::exception &e) { - std::cout << e.what() << std::endl; - } - delete []$1; - } - | relation ';' { - flushScanBuffer(); - $1->simplify(redundant_conj_level, redundant_constr_level); - $1->print_with_subs(stdout); - delete $1; - } - | TIME relation ';' { -#if defined(OMIT_GETRUSAGE) - printf("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n"); -#else - flushScanBuffer(); - printf("\n"); - int t; - Relation R; - bool SKIP_FULL_CHECK = getenv("OC_TIMING_SKIP_FULL_CHECK"); - ($2)->and_with_GEQ(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - } - int copyTime = clock_diff(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - R.simplify(); /* default simplification effort */ - } - int simplifyTime = clock_diff() -copyTime; - Relation R2; - if (!SKIP_FULL_CHECK) { - start_clock(); - for (t=1;t<=100;t++) { - R2 = *$2; - R2.finalize(); - R2.simplify(2,4); /* maximal simplification effort */ - } - } - int excessiveTime = clock_diff() - copyTime; - printf("Times (in microseconds): \n"); - printf("%5d us to copy original set of constraints\n",copyTime/100); - printf("%5d us to do the default amount of simplification, obtaining: \n\t", simplifyTime/100); - R.print_with_subs(stdout); - printf("\n"); - if (!SKIP_FULL_CHECK) { - printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", excessiveTime/100); - R2.print_with_subs(stdout); - printf("\n"); - } - if (!anyTimingDone) { - bool warn = false; -#ifndef SPEED - warn =true; -#endif -#ifndef NDEBUG - warn = true; -#endif - if (warn) { - printf("WARNING: The Omega calculator was compiled with options that force\n"); - printf("it to perform additional consistency and error checks\n"); - printf("that may slow it down substantially\n"); - printf("\n"); - } - printf("NOTE: These times relect the time of the current _implementation_\n"); - printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n"); - printf("report on the performance on the Omega test, we respectfully but strongly \n"); - printf("request that send your test cases to us to allow us to determine if the \n"); - printf("times are appropriate, and if the way you are using the Omega library to \n"); - printf("solve your problem is the most effective way.\n"); - printf("\n"); - - printf("Also, please be aware that over the past two years, we have focused our \n"); - printf("efforts on the expressive power of the Omega library, sometimes at the\n"); - printf("expensive of raw speed. Our original implementation of the Omega test\n"); - printf("was substantially faster on the limited domain it handled.\n"); - printf("\n"); - printf(" Thanks, \n"); - printf(" the Omega Team \n"); - } - anyTimingDone = true; - delete $2; -#endif - } - | TIMECLOSURE relation ';' { -#if defined(OMIT_GETRUSAGE) - printf("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n"); -#else - flushScanBuffer(); - try { - int t; - Relation R; - ($2)->and_with_GEQ(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - } - int copyTime = clock_diff(); - start_clock(); - for (t=1;t<=100;t++) { - R = *$2; - R.finalize(); - R.simplify(); - } - int simplifyTime = clock_diff() -copyTime; - Relation Rclosed; - start_clock(); - for (t=1;t<=100;t++) { - Rclosed = *$2; - Rclosed.finalize(); - Rclosed = TransitiveClosure(Rclosed, 1,Relation::Null()); - } - int closureTime = clock_diff() - copyTime; - Relation R2; - start_clock(); - for (t=1;t<=100;t++) { - R2 = *$2; - R2.finalize(); - R2.simplify(2,4); - } - int excessiveTime = clock_diff() - copyTime; - printf("Times (in microseconds): \n"); - printf("%5d us to copy original set of constraints\n",copyTime/100); - printf("%5d us to do the default amount of simplification, obtaining: \n\t", simplifyTime/100); - R.print_with_subs(stdout); - printf("\n"); - printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", excessiveTime/100); - R2.print_with_subs(stdout); - printf("%5d us to do the transitive closure, obtaining: \n\t", closureTime/100); - Rclosed.print_with_subs(stdout); - printf("\n"); - if (!anyTimingDone) { - bool warn = false; -#ifndef SPEED - warn =true; -#endif -#ifndef NDEBUG - warn = true; -#endif - if (warn) { - printf("WARNING: The Omega calculator was compiled with options that force\n"); - printf("it to perform additional consistency and error checks\n"); - printf("that may slow it down substantially\n"); - printf("\n"); - } - printf("NOTE: These times relect the time of the current _implementation_\n"); - printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n"); - printf("report on the performance on the Omega test, we respectfully but strongly \n"); - printf("request that send your test cases to us to allow us to determine if the \n"); - printf("times are appropriate, and if the way you are using the Omega library to \n"); - printf("solve your problem is the most effective way.\n"); - printf("\n"); - - printf("Also, please be aware that over the past two years, we have focused our \n"); - printf("efforts on the expressive power of the Omega library, sometimes at the\n"); - printf("expensive of raw speed. Our original implementation of the Omega test\n"); - printf("was substantially faster on the limited domain it handled.\n"); - printf("\n"); - printf(" Thanks, \n"); - printf(" the Omega Team \n"); - } - anyTimingDone = true; - } - catch (const std::exception &e) { - std::cout << e.what() << std::endl; - } - delete $2; -#endif - } - | relation SUBSET relation ';' { - flushScanBuffer(); - try { - if (Must_Be_Subset(copy(*$1), copy(*$3))) - std::cout << "True" << std::endl; - else if (Might_Be_Subset(copy(*$1), copy(*$3))) - std::cout << "Possible" << std::endl; - else - std::cout << "False" << std::endl; - } - catch (const std::exception &e) { - std::cout << e.what() << std::endl; - } - delete $1; - delete $3; - } - | CODEGEN effort relPairList context';' { - flushScanBuffer(); - try { - std::string s = MMGenerateCode($3->mappings, $3->ispaces,*$4,$2); - std::cout << s << std::endl; - } - catch (const std::exception &e) { - std::cout << e.what() << std::endl; - } - delete $4; - delete $3; - } - | reachable ';' { - flushScanBuffer(); - DynamicArray1<Relation> &final = *$1; - bool any_sat = false; - int i,n_nodes = reachable_info->node_names.size(); - for(i = 1; i <= n_nodes; i++) - if(final[i].is_upper_bound_satisfiable()) { - any_sat = true; - std::cout << "Node %s: " << reachable_info->node_names[i]; - final[i].print_with_subs(stdout); - } - if(!any_sat) - std::cout << "No nodes reachable.\n"; - delete $1; - delete reachable_info; - } -; - - -effort : {$$ = 1;} - | INT {$$ = $1;} - | '-' INT {$$ = -$2;} -; - -context : {$$ = new Relation(); *$$ = Relation::Null();} - | GIVEN relation {$$ = $2; } -; - -relPairList : relPairList ',' relation ':' relation { - try { - $1->mappings.append(*$3); - $1->mappings[$1->mappings.size()].compress(); - $1->ispaces.append(*$5); - $1->ispaces[$1->ispaces.size()].compress(); - } - catch (const std::exception &e) { - delete $1; - delete $3; - delete $5; - yyerror(e.what()); - YYERROR; - } - delete $3; - delete $5; - $$ = $1; - } - | relPairList ',' relation { - try { - $1->mappings.append(Identity($3->n_set())); - $1->mappings[$1->mappings.size()].compress(); - $1->ispaces.append(*$3); - $1->ispaces[$1->ispaces.size()].compress(); - } - catch (const std::exception &e) { - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $3; - $$ = $1; - } - | relation ':' relation { - RelTuplePair *rtp = new RelTuplePair; - try { - rtp->mappings.append(*$1); - rtp->mappings[rtp->mappings.size()].compress(); - rtp->ispaces.append(*$3); - rtp->ispaces[rtp->ispaces.size()].compress(); - } - catch (const std::exception &e) { - delete rtp; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - $$ = rtp; - } - | relation { - RelTuplePair *rtp = new RelTuplePair; - try { - rtp->mappings.append(Identity($1->n_set())); - rtp->mappings[rtp->mappings.size()].compress(); - rtp->ispaces.append(*$1); - rtp->ispaces[rtp->ispaces.size()].compress(); - } - catch (const std::exception &e) { - delete rtp; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - $$ = rtp; - } -; - -relation : OPEN_BRACE {need_coef = true; relationDecl = new Declaration_Site();} - builtRelation CLOSE_BRACE { - need_coef = false; - $$ = $3; - if (omega_calc_debug) { - fprintf(DebugFile,"Built relation:\n"); - $$->prefix_print(DebugFile); - } - current_Declaration_Site = globalDecls; - delete relationDecl; - relationDecl = NULL; - } - | VAR { - Const_String s = $1; - Relation *r = relationMap(s); - if (r == NULL) { - yyerror(std::string("relation ") + to_string($1) + std::string(" not declared")); - delete []$1; - YYERROR; - } - $$ = new Relation(*r); - delete []$1; - } - | '(' relation ')' {$$ = $2;} - | relation '+' %prec p9 { - $$ = new Relation(); - try { - *$$ = TransitiveClosure(*$1, 1, Relation::Null()); - } - catch (const std::exception &e) { - delete $$; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - } - | relation '*' %prec p9 { - $$ = new Relation(); - try { - int vars = $1->n_inp(); - *$$ = Union(Identity(vars), TransitiveClosure(*$1, 1, Relation::Null())); - } - catch (const std::exception &e) { - delete $$; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - } - | relation '+' WITHIN relation %prec p9 { - $$ = new Relation(); - try { - *$$= TransitiveClosure(*$1, 1, *$4); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $4; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $4; - } - | relation '^' '@' %prec p8 { - $$ = new Relation(); - try { - *$$ = ApproxClosure(*$1); - } - catch (const std::exception &e) { - delete $$; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - } - | relation '^' '+' %prec p8 { - $$ = new Relation(); - try { - *$$ = calculateTransitiveClosure(*$1); - } - catch (const std::exception &e) { - delete $$; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - } - | MINIMIZE_RANGE relation %prec p8 { - $$ = new Relation(); - try { - Relation o(*$2); - Relation r(*$2); - r = Join(r,LexForward($2->n_out())); - *$$ = Difference(o,r); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MAXIMIZE_RANGE relation %prec p8 { - $$ = new Relation(); - try { - Relation o(*$2); - Relation r(*$2); - r = Join(r,Inverse(LexForward($2->n_out()))); - *$$ = Difference(o,r); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MINIMIZE_DOMAIN relation %prec p8 { - $$ = new Relation(); - try { - Relation o(*$2); - Relation r(*$2); - r = Join(LexForward($2->n_inp()),r); - *$$ = Difference(o,r); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MAXIMIZE_DOMAIN relation %prec p8 { - $$ = new Relation(); - try { - Relation o(*$2); - Relation r(*$2); - r = Join(Inverse(LexForward($2->n_inp())),r); - *$$ = Difference(o,r); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MAXIMIZE relation %prec p8 { - $$ = new Relation(); - try { - Relation c(*$2); - Relation r(*$2); - *$$ = Cross_Product(Relation(*$2),c); - *$$ = Difference(r,Domain(Intersection(*$$,LexForward($$->n_inp())))); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MINIMIZE relation %prec p8 { - $$ = new Relation(); - try { - Relation c(*$2); - Relation r(*$2); - *$$ = Cross_Product(Relation(*$2),c); - *$$ = Difference(r,Range(Intersection(*$$,LexForward($$->n_inp())))); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | FARKAS relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Farkas(*$2, Basic_Farkas); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | DECOUPLED_FARKAS relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Farkas(*$2, Decoupled_Farkas); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | relation '@' %prec p9 { - $$ = new Relation(); - try { - *$$ = ConicClosure(*$1); - } - catch (const std::exception &e) { - delete $$; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - } - | PROJECT_AWAY_SYMBOLS relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Project_Sym(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | PROJECT_ON_SYMBOLS relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Project_On_Sym(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | DIFFERENCE relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Deltas(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | DIFFERENCE_TO_RELATION relation %prec p8 { - $$ = new Relation(); - try { - *$$ = DeltasToRelation(*$2,$2->n_set(),$2->n_set()); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | DOMAIN relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Domain(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | VENN relation %prec p8 { - $$ = new Relation(); - try { - *$$ = VennDiagramForm(*$2,Relation::True(*$2)); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | VENN relation GIVEN relation %prec p8 { - $$ = new Relation(); - try { - *$$ = VennDiagramForm(*$2,*$4); - } - catch (const std::exception &e) { - delete $$; - delete $2; - delete $4; - yyerror(e.what()); - YYERROR; - } - delete $2; - delete $4; - } - | CONVEX_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = ConvexHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | DECOUPLED_CONVEX_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = DecoupledConvexHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | POSITIVE_COMBINATION relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Farkas(*$2,Positive_Combination_Farkas); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | LINEAR_COMBINATION relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Farkas(*$2,Linear_Combination_Farkas); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | AFFINE_COMBINATION relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Farkas(*$2,Affine_Combination_Farkas); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | CONVEX_COMBINATION relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Farkas(*$2,Convex_Combination_Farkas); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | PAIRWISE_CHECK relation %prec p8 { - $$ = new Relation(); - try { - *$$ = CheckForConvexRepresentation(CheckForConvexPairs(*$2)); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | CONVEX_CHECK relation %prec p8 { - $$ = new Relation(); - try { - *$$ = CheckForConvexRepresentation(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | CONVEX_REPRESENTATION relation %prec p8 { - $$ = new Relation(); - try { - *$$ = ConvexRepresentation(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | AFFINE_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = AffineHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | CONIC_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = ConicHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | LINEAR_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = LinearHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | QUICK_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = QuickHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | RECT_HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = RectHull(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | HULL relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Hull(*$2,false,1,Relation::Null()); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | HULL relation GIVEN relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Hull(*$2,false,1,*$4); - } - catch (const std::exception &e) { - delete $$; - delete $2; - delete $4; - yyerror(e.what()); - YYERROR; - } - delete $2; - delete $4; - } - | APPROX relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Approximate(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | RANGE relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Range(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | INVERSE relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Inverse(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | COMPLEMENT relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Complement(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | GIST relation GIVEN relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Gist(*$2,*$4,1); - } - catch (const std::exception &e) { - delete $$; - delete $2; - delete $4; - yyerror(e.what()); - YYERROR; - } - delete $2; - delete $4; - } - | relation '(' relation ')' { - $$ = new Relation(); - try { - *$$ = Composition(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation COMPOSE relation { - $$ = new Relation(); - try { - *$$ = Composition(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation CARRIED_BY INT { - $$ = new Relation(); - try { - *$$ = After(*$1,$3,$3); - (*$$).prefix_print(stdout); - } - catch (const std::exception &e) { - delete $$; - delete $1; - yyerror(e.what()); - YYERROR; - } - delete $1; - } - | relation JOIN relation { - $$ = new Relation(); - try { - *$$ = Composition(*$3,*$1); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation RESTRICT_RANGE relation { - $$ = new Relation(); - try { - *$$ = Restrict_Range(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation RESTRICT_DOMAIN relation { - $$ = new Relation(); - try { - *$$ = Restrict_Domain(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation INTERSECTION relation { - $$ = new Relation(); - try { - *$$ = Intersection(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation '-' relation %prec INTERSECTION { - $$ = new Relation(); - try { - *$$ = Difference(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation UNION relation { - $$ = new Relation(); - try { - *$$ = Union(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | relation '*' relation { - $$ = new Relation(); - try { - *$$ = Cross_Product(*$1,*$3); - } - catch (const std::exception &e) { - delete $$; - delete $1; - delete $3; - yyerror(e.what()); - YYERROR; - } - delete $1; - delete $3; - } - | SUPERSETOF relation { - $$ = new Relation(); - try { - *$$ = Union(*$2, Relation::Unknown(*$2)); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | SUBSETOF relation { - $$ = new Relation(); - try { - *$$ = Intersection(*$2, Relation::Unknown(*$2)); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MAKE_UPPER_BOUND relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Upper_Bound(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | MAKE_LOWER_BOUND relation %prec p8 { - $$ = new Relation(); - try { - *$$ = Lower_Bound(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | SAMPLE relation { - $$ = new Relation(); - try { - *$$ = Sample_Solution(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | SYM_SAMPLE relation { - $$ = new Relation(); - try { - *$$ = Symbolic_Solution(*$2); - } - catch (const std::exception &e) { - delete $$; - delete $2; - yyerror(e.what()); - YYERROR; - } - delete $2; - } - | reachable_of { $$ = $1; } - | ASSERT_UNSAT relation { - if (($2)->is_satisfiable()) { - fprintf(stderr,"assert_unsatisfiable failed on "); - ($2)->print_with_subs(stderr); - exit(1); - } - $$=$2; - } -; - -builtRelation : tupleDeclaration GOES_TO {currentTuple = Output_Tuple;} - tupleDeclaration {currentTuple = Input_Tuple;} optionalFormula { - Relation * r = new Relation($1->size,$4->size); - resetGlobals(); - F_And *f = r->add_and(); - for(int i=1;i<=$1->size;i++) { - $1->vars[i]->vid = r->input_var(i); - if (!$1->vars[i]->anonymous) - r->name_input_var(i,$1->vars[i]->stripped_name); - } - for(int i=1;i<=$4->size;i++) { - $4->vars[i]->vid = r->output_var(i); - if (!$4->vars[i]->anonymous) - r->name_output_var(i,$4->vars[i]->stripped_name); - } - r->setup_names(); - foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0)); - foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0)); - foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c)); - foreach(e,Exp*,$4->eq_constraints, install_eq(f,e,0)); - foreach(e,Exp*,$4->geq_constraints, install_geq(f,e,0)); - foreach(c,strideConstraint*,$4->stride_constraints, install_stride(f,c)); - if ($6) $6->install(f); - delete $1; - delete $4; - delete $6; - $$ = r; - } - | tupleDeclaration optionalFormula { - Relation * r = new Relation($1->size); - resetGlobals(); - F_And *f = r->add_and(); - for(int i=1;i<=$1->size;i++) { - $1->vars[i]->vid = r->set_var(i); - if (!$1->vars[i]->anonymous) - r->name_set_var(i,$1->vars[i]->stripped_name); - } - r->setup_names(); - foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0)); - foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0)); - foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c)); - if ($2) $2->install(f); - delete $1; - delete $2; - $$ = r; - } - | formula { - Relation * r = new Relation(0,0); - F_And *f = r->add_and(); - $1->install(f); - delete $1; - $$ = r; - } -; - -optionalFormula : formula_sep formula {$$ = $2;} - | {$$ = 0;} -; - -formula_sep : ':' - | VERTICAL_BAR - | SUCH_THAT -; - -tupleDeclaration : {currentTupleDescriptor = new tupleDescriptor; tuplePos = 1;} - '[' optionalTupleVarList ']' - {$$ = currentTupleDescriptor; tuplePos = 0;} -; - -optionalTupleVarList : /* empty */ - | tupleVar - | optionalTupleVarList ',' tupleVar -; - -tupleVar : VAR %prec p10 { - Declaration_Site *ds = defined($1); - if (!ds) - currentTupleDescriptor->extend($1,currentTuple,tuplePos); - else { - Variable_Ref *v = lookupScalar($1); - if (v == NULL) { - yyerror(std::string("cannot find declaration for variable ") + to_string($1)); - delete []$1; - YYERROR; - } - if (ds != globalDecls) - currentTupleDescriptor->extend($1, new Exp(v)); - else - currentTupleDescriptor->extend(new Exp(v)); - } - tuplePos++; - delete []$1; - } - | '*' {currentTupleDescriptor->extend(); tuplePos++;} - | exp %prec p1 { - currentTupleDescriptor->extend($1); - tuplePos++; - } - | exp ':' exp %prec p1 { - currentTupleDescriptor->extend($1,$3); - tuplePos++; - } - | exp ':' exp ':' COEF %prec p1 { - currentTupleDescriptor->extend($1,$3,$5); - tuplePos++; - } -; - -varList : varList ',' VAR {$$ = $1; $$->insert($3); $3 = NULL;} - | VAR {$$ = new VarList; $$->insert($1); $1 = NULL;} -; - -varDecl : varList { - $$ = current_Declaration_Site = new Declaration_Site($1); - foreach(s,char *, *$1, delete []s); - delete $1; - } -; - -varDeclOptBrackets : varDecl {$$ = $1;} - |'[' varDecl ']' {$$ = $2;} -; - -globVarList : globVarList ',' globVar - | globVar -; - -globVar : VAR '(' INT ')' {globalDecls->extend_both_tuples($1, $3); delete []$1;} - | VAR { - globalDecls->extend($1); - delete []$1; - } -; - -formula : formula AND formula {$$ = new AST_And($1,$3);} - | formula OR formula {$$ = new AST_Or($1,$3);} - | constraintChain {$$ = $1;} - | '(' formula ')' {$$ = $2;} - | NOT formula {$$ = new AST_Not($2);} - | start_exists varDeclOptBrackets exists_sep formula end_quant {$$ = new AST_exists($2,$4);} - | start_forall varDeclOptBrackets forall_sep formula end_quant {$$ = new AST_forall($2,$4);} -; - -start_exists : '(' EXISTS - | EXISTS '(' -; - -exists_sep : ':' - | VERTICAL_BAR - | SUCH_THAT -; - -start_forall : '(' FORALL - | FORALL '(' -; - -forall_sep : ':' -; - -end_quant : ')' {popScope();} -; - -expList : exp ',' expList {$$ = $3; $$->insert($1);} - | exp {$$ = new ExpList; $$->insert($1);} -; - -constraintChain : expList REL_OP expList {$$ = new AST_constraints($1,$2,$3);} - | expList REL_OP constraintChain {$$ = new AST_constraints($1,$2,$3);} -; - -simpleExp : VAR %prec p9 { - Variable_Ref *v = lookupScalar($1); - if (v == NULL) { - yyerror(std::string("cannot find declaration for variable ") + to_string($1)); - delete []$1; - YYERROR; - } - $$ = new Exp(v); - delete []$1; - } - | VAR '(' {argCount = 1;} argumentList ')' %prec p9 { - Variable_Ref *v; - if ($4 == Input_Tuple) - v = functionOfInput[$1]; - else - v = functionOfOutput[$1]; - if (v == NULL) { - yyerror(std::string("Function ") + to_string($1) + std::string(" not declared")); - delete []$1; - YYERROR; - } - $$ = new Exp(v); - delete []$1; - } - | '(' exp ')' { $$ = $2; } -; - -argumentList : argumentList ',' VAR { - Variable_Ref *v = lookupScalar($3); - if (v == NULL) { - yyerror(std::string("cannot find declaration for variable ") + to_string($1)); - delete []$3; - YYERROR; - } - if (v->pos != argCount || v->of != $1 || (v->of != Input_Tuple && v->of != Output_Tuple)) { - yyerror("arguments to function must be prefix of input or output tuple"); - delete []$3; - YYERROR; - } - $$ = v->of; - argCount++; - delete []$3; - } - | VAR { - Variable_Ref *v = lookupScalar($1); - if (v == NULL) { - yyerror(std::string("cannot find declaration for variable ") + to_string($1)); - delete []$1; - YYERROR; - } - if (v->pos != argCount || (v->of != Input_Tuple && v->of != Output_Tuple)) { - yyerror("arguments to function must be prefix of input or output tuple"); - delete []$1; - YYERROR; - } - $$ = v->of; - argCount++; - delete []$1; - } -; - -exp : COEF {$$ = new Exp($1);} - | COEF simpleExp %prec '*' {$$ = multiply($1,$2);} - | simpleExp {$$ = $1; } - | '-' exp %prec '*' {$$ = negate($2);} - | exp '+' exp {$$ = add($1,$3);} - | exp '-' exp {$$ = subtract($1,$3);} - | exp '*' exp {$$ = multiply($1,$3);} -; - - -reachable : REACHABLE_FROM nodeNameList nodeSpecificationList { - DynamicArray1<Relation> *final = Reachable_Nodes(reachable_info); - $$ = final; - } -; - -reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList { - DynamicArray1<Relation> *final = Reachable_Nodes(reachable_info); - int index = reachable_info->node_names.index(std::string($2)); - if (index == 0) { - yyerror(std::string("no such node ") + to_string($2)); - delete []$2; - delete final; - delete reachable_info; - YYERROR; - } - $$ = new Relation; - *$$ = (*final)[index]; - delete final; - delete reachable_info; - delete []$2; - } -; - -nodeNameList : '(' realNodeNameList ')' { - int sz = reachable_info->node_names.size(); - reachable_info->node_arity.reallocate(sz); - reachable_info->transitions.resize(sz+1,sz+1); - reachable_info->start_nodes.resize(sz+1); - } -; - -realNodeNameList : realNodeNameList ',' VAR { - reachable_info->node_names.append(std::string($3)); - delete []$3; - } - | VAR { - reachable_info = new reachable_information; - reachable_info->node_names.append(std::string($1)); - delete []$1; - } -; - - -nodeSpecificationList : OPEN_BRACE realNodeSpecificationList CLOSE_BRACE { - int i,j; - int n_nodes = reachable_info->node_names.size(); - Tuple<int> &arity = reachable_info->node_arity; - DynamicArray2<Relation> &transitions = reachable_info->transitions; - - /* fixup unspecified transitions to be false */ - /* find arity */ - for(i = 1; i <= n_nodes; i++) arity[i] = -1; - for(i = 1; i <= n_nodes; i++) - for(j = 1; j <= n_nodes; j++) - if(! transitions[i][j].is_null()) { - int in_arity = transitions[i][j].n_inp(); - int out_arity = transitions[i][j].n_out(); - if(arity[i] < 0) arity[i] = in_arity; - if(arity[j] < 0) arity[j] = out_arity; - if(in_arity != arity[i] || out_arity != arity[j]) { - yyerror(std::string("arity mismatch in node transition: ") + to_string(reachable_info->node_names[i]) + std::string(" -> ") + to_string(reachable_info->node_names[j])); - delete reachable_info; - YYERROR; - } - } - for(i = 1; i <= n_nodes; i++) - if(arity[i] < 0) arity[i] = 0; - /* Fill in false relations */ - for(i = 1; i <= n_nodes; i++) - for(j = 1; j <= n_nodes; j++) - if(transitions[i][j].is_null()) - transitions[i][j] = Relation::False(arity[i],arity[j]); - - /* fixup unused start node positions */ - DynamicArray1<Relation> &nodes = reachable_info->start_nodes; - for(i = 1; i <= n_nodes; i++) - if(nodes[i].is_null()) - nodes[i] = Relation::False(arity[i]); - else - if(nodes[i].n_set() != arity[i]){ - yyerror(std::string("arity mismatch in start node ") + to_string(reachable_info->node_names[i])); - delete reachable_info; - YYERROR; - } - } -; - -realNodeSpecificationList : realNodeSpecificationList ',' VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int index = reachable_info->node_names.index($3); - if (!(index > 0 && index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($3)); - delete $5; - delete []$3; - delete reachable_info; - YYERROR; - } - reachable_info->start_nodes[index] = *$5; - delete $5; - delete []$3; - } - | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int from_index = reachable_info->node_names.index($3); - if (!(from_index > 0 && from_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($3)); - delete $7; - delete []$3; - delete []$5; - delete reachable_info; - YYERROR; - } - int to_index = reachable_info->node_names.index($5); - if (!(to_index > 0 && to_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($5)); - delete $7; - delete []$3; - delete []$5; - delete reachable_info; - YYERROR; - } - reachable_info->transitions[from_index][to_index] = *$7; - delete $7; - delete []$3; - delete []$5; - } - | VAR GOES_TO VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int from_index = reachable_info->node_names.index($1); - if (!(from_index > 0 && from_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($1)); - delete $5; - delete []$1; - delete []$3; - delete reachable_info; - YYERROR; - } - int to_index = reachable_info->node_names.index($3); - if (!(to_index > 0 && to_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($3)); - delete $5; - delete []$1; - delete []$3; - delete reachable_info; - YYERROR; - } - reachable_info->transitions[from_index][to_index] = *$5; - delete $5; - delete []$1; - delete []$3; - } - | VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int index = reachable_info->node_names.index($1); - if (!(index > 0 && index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($1)); - delete $3; - delete []$1; - delete reachable_info; - YYERROR; - } - reachable_info->start_nodes[index] = *$3; - delete $3; - delete []$1; - } -; - -%% - - -void printUsage(FILE *outf, char **argv) { - fprintf(outf, "usage: %s {-R} {-D[facility][level]...} infile\n -R means skip redundant conjunct elimination\n -D sets debugging level as follows:\n a = all debugging flags\n g = code generation\n l = calculator\n c = omega core\n p = presburger functions\n r = relational operators\n t = transitive closure\n", argv[0]); -} - - -bool process_calc_debugging_flags(char *arg,int &j) { - char debug_type; - while((debug_type=arg[j]) != 0) { - j++; - int level; - if(isdigit(arg[j])) - level = (arg[j++]) - '0'; - else - if(arg[j] == 0 || isalpha(arg[j])) - level = 1; - else - return false; - if (level < 0 || level > 4) { - fprintf(stderr,"Debug level %c out of range: %d\n", debug_type, level); - return false; - } - switch(debug_type) { - case 'a': - omega_core_debug = relation_debug = hull_debug = - closure_presburger_debug = - farkas_debug = - pres_debug = omega_calc_debug = code_gen_debug = level; - break; - case 'g': - code_gen_debug = level; break; - case 'f': - farkas_debug = level; break; - case 'h': - hull_debug = level; break; - case 'c': - omega_core_debug = level; break; - case 'r': - relation_debug = level; break; - case 'p': - pres_debug = level; break; - case 't': - closure_presburger_debug = level; break; - case 'l': - omega_calc_debug = level; break; -#if defined STUDY_EVACUATIONS - case 'e': - evac_debug = level; break; -#endif - default: - fprintf(stderr, "Unknown debug type %c\n", debug_type); - return false; - } - } - return true; -} - - -int main(int argc, char **argv) { -#if YYDEBUG != 0 - yydebug = 1; -#endif - - /* process flags */ - char *fileName = 0; - for(int i=1; i<argc; i++) { - if(argv[i][0] == '-') { - int j = 1, c; - while((c=argv[i][j++]) != 0) { - switch(c) { - case 'D': - if (!process_calc_debugging_flags(argv[i],j)) { - printUsage(stderr, argv); - exit(1); - } - break; - case 'G': - fprintf(stderr,"Note: specifying number of GEQ's is no longer useful.\n"); - while(argv[i][j] != 0) j++; - break; - case 'E': - fprintf(stderr,"Note: specifying number of EQ's is no longer useful.\n"); - while(argv[i][j] != 0) j++; - break; - case 'R': - redundant_conj_level = 1; - break; - /* Other future options go here */ - case 'h': - printUsage(stderr, argv); - exit(1); - break; - default: - fprintf(stderr, "\nUnknown flag -%c\n", c); - printUsage(stderr, argv); - exit(1); - } - } - } - else { - /* Make sure this is a file name */ - if (fileName) { - fprintf(stderr,"\nCan only handle a single input file\n"); - printUsage(stderr,argv); - exit(1); - } - fileName = argv[i]; - yyin = fopen(fileName, "r"); - if (!yyin) { - fprintf(stderr, "\nCan't open input file %s\n",fileName); - printUsage(stderr,argv); - exit(1); - } - } - } - - if (fileName || !isatty((int)fileno(stdin))) { - is_interactive = false; - } - else { - is_interactive = true; - setbuf(DebugFile, NULL); - printf("Calculator for Omega+ v20110204snapshot (built on %s)\n", OMEGA_BUILD_DATE); - printf("Copyright (C) 1994-2000 University of Maryland the Omega Project Team\n"); - printf("Copyright (C) 2008 University of Southern California\n"); - printf("Copyright (C) 2009-2011 University of Utah\n"); - printf("%s ", PROMPT_STRING); - } - need_coef = false; - current_Declaration_Site = globalDecls = new Global_Declaration_Site(); - - if (yyparse() != 0) { - if (!is_interactive) - std::cout << "syntax error at the end of the file, missing ';'" << std::endl; - else - std::cout << std::endl; - delete relationDecl; - relationDecl = NULL; - } - else { - if (is_interactive) - std::cout << std::endl; - } - - foreach_map(cs,Const_String,r,Relation *,relationMap, - {delete r; relationMap[cs]=0;}); - delete globalDecls; - fclose(yyin); - - return 0; -} - -Relation LexForward(int n) { - Relation r(n,n); - F_Or *f = r.add_or(); - for (int i=1; i <= n; i++) { - F_And *g = f->add_and(); - for(int j=1;j<i;j++) { - EQ_Handle e = g->add_EQ(); - e.update_coef(r.input_var(j),-1); - e.update_coef(r.output_var(j),1); - e.finalize(); - } - GEQ_Handle e = g->add_GEQ(); - e.update_coef(r.input_var(i),-1); - e.update_coef(r.output_var(i),1); - e.update_const(-1); - e.finalize(); - } - r.finalize(); - return r; -} diff --git a/omegalib/omegacalc/src/parser.yy b/omegalib/omegacalc/src/parser.yy deleted file mode 100755 index c2821cc..0000000 --- a/omegalib/omegacalc/src/parser.yy +++ /dev/null @@ -1,1928 +0,0 @@ -/***************************************************************************** - 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/DynamicArray.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::DynamicArray1<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(); - DynamicArray1<Relation> &final = *$1; - bool any_sat = false; - int i,n_nodes = reachable_info->node_names.size(); - for(i = 1; i <= n_nodes; i++) - if(final[i].is_upper_bound_satisfiable()) { - any_sat = true; - std::cout << "Node " << 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 { - DynamicArray1<Relation> *final = Reachable_Nodes(reachable_info); - $$ = final; - } -; - -reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList { - DynamicArray1<Relation> *final = Reachable_Nodes(reachable_info); - int index = reachable_info->node_names.index(std::string($2)); - if (index == 0) { - yyerror(std::string("no such node ") + to_string($2)); - delete []$2; - delete final; - delete reachable_info; - YYERROR; - } - $$ = new Relation; - *$$ = (*final)[index]; - delete final; - delete reachable_info; - delete []$2; - } -; - -nodeNameList : '(' realNodeNameList ')' { - int sz = reachable_info->node_names.size(); - reachable_info->node_arity.reallocate(sz); - reachable_info->transitions.resize(sz+1,sz+1); - reachable_info->start_nodes.resize(sz+1); - } -; - -realNodeNameList : realNodeNameList ',' VAR { - reachable_info->node_names.append(std::string($3)); - delete []$3; - } - | VAR { - reachable_info = new reachable_information; - reachable_info->node_names.append(std::string($1)); - delete []$1; - } -; - - -nodeSpecificationList : OPEN_BRACE realNodeSpecificationList CLOSE_BRACE { - int i,j; - int n_nodes = reachable_info->node_names.size(); - Tuple<int> &arity = reachable_info->node_arity; - DynamicArray2<Relation> &transitions = reachable_info->transitions; - - /* fixup unspecified transitions to be false */ - /* find arity */ - for(i = 1; i <= n_nodes; i++) arity[i] = -1; - for(i = 1; i <= n_nodes; i++) - for(j = 1; j <= n_nodes; j++) - if(! transitions[i][j].is_null()) { - int in_arity = transitions[i][j].n_inp(); - int out_arity = transitions[i][j].n_out(); - if(arity[i] < 0) arity[i] = in_arity; - if(arity[j] < 0) arity[j] = out_arity; - if(in_arity != arity[i] || out_arity != arity[j]) { - yyerror(std::string("arity mismatch in node transition: ") + to_string(reachable_info->node_names[i]) + std::string(" -> ") + to_string(reachable_info->node_names[j])); - delete reachable_info; - YYERROR; - } - } - for(i = 1; i <= n_nodes; i++) - if(arity[i] < 0) arity[i] = 0; - /* Fill in false relations */ - for(i = 1; i <= n_nodes; i++) - for(j = 1; j <= n_nodes; j++) - if(transitions[i][j].is_null()) - transitions[i][j] = Relation::False(arity[i],arity[j]); - - /* fixup unused start node positions */ - DynamicArray1<Relation> &nodes = reachable_info->start_nodes; - for(i = 1; i <= n_nodes; i++) - if(nodes[i].is_null()) - nodes[i] = Relation::False(arity[i]); - else - if(nodes[i].n_set() != arity[i]){ - yyerror(std::string("arity mismatch in start node ") + to_string(reachable_info->node_names[i])); - delete reachable_info; - YYERROR; - } - } -; - -realNodeSpecificationList : realNodeSpecificationList ',' VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int index = reachable_info->node_names.index($3); - if (!(index > 0 && index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($3)); - delete $5; - delete []$3; - delete reachable_info; - YYERROR; - } - reachable_info->start_nodes[index] = *$5; - delete $5; - delete []$3; - } - | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int from_index = reachable_info->node_names.index($3); - if (!(from_index > 0 && from_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($3)); - delete $7; - delete []$3; - delete []$5; - delete reachable_info; - YYERROR; - } - int to_index = reachable_info->node_names.index($5); - if (!(to_index > 0 && to_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($5)); - delete $7; - delete []$3; - delete []$5; - delete reachable_info; - YYERROR; - } - reachable_info->transitions[from_index][to_index] = *$7; - delete $7; - delete []$3; - delete []$5; - } - | VAR GOES_TO VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int from_index = reachable_info->node_names.index($1); - if (!(from_index > 0 && from_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($1)); - delete $5; - delete []$1; - delete []$3; - delete reachable_info; - YYERROR; - } - int to_index = reachable_info->node_names.index($3); - if (!(to_index > 0 && to_index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($3)); - delete $5; - delete []$1; - delete []$3; - delete reachable_info; - YYERROR; - } - reachable_info->transitions[from_index][to_index] = *$5; - delete $5; - delete []$1; - delete []$3; - } - | VAR ':' relation { - int n_nodes = reachable_info->node_names.size(); - int index = reachable_info->node_names.index($1); - if (!(index > 0 && index <= n_nodes)) { - yyerror(std::string("no such node ")+to_string($1)); - delete $3; - delete []$1; - delete reachable_info; - YYERROR; - } - reachable_info->start_nodes[index] = *$3; - delete $3; - delete []$1; - } -; - -%% - -void 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; -} |