From e4b20015a4ee35f1279af4caa983478fa2ff0d4a Mon Sep 17 00:00:00 2001
From: dhuth <derickhuth@gmail.com>
Date: Mon, 6 Oct 2014 11:56:47 -0600
Subject: Added omega to source
---
omega/omega_calc/src/AST.cc | 467 ++++++++++
omega/omega_calc/src/myflex.cc | 421 +++++++++
omega/omega_calc/src/parser.l | 350 ++++++++
omega/omega_calc/src/parser.ll | 350 ++++++++
omega/omega_calc/src/parser.y | 1925 +++++++++++++++++++++++++++++++++++++++
omega/omega_calc/src/parser.yy | 1928 ++++++++++++++++++++++++++++++++++++++++
6 files changed, 5441 insertions(+)
create mode 100644 omega/omega_calc/src/AST.cc
create mode 100755 omega/omega_calc/src/myflex.cc
create mode 100644 omega/omega_calc/src/parser.l
create mode 100755 omega/omega_calc/src/parser.ll
create mode 100644 omega/omega_calc/src/parser.y
create mode 100755 omega/omega_calc/src/parser.yy
(limited to 'omega/omega_calc/src')
diff --git a/omega/omega_calc/src/AST.cc b/omega/omega_calc/src/AST.cc
new file mode 100644
index 0000000..1f885a6
--- /dev/null
+++ b/omega/omega_calc/src/AST.cc
@@ -0,0 +1,467 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2009-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+ build relation from parsed input.
+
+ Notes:
+
+ History:
+*****************************************************************************/
+
+#include <omega_calc/AST.h>
+#include <string.h>
+
+using namespace omega;
+
+Global_Declaration_Site *globalDecls;
+Declaration_Site *relationDecl = NULL;
+tupleDescriptor *currentTupleDescriptor;
+std::map<omega::Const_String, Variable_Ref *> functionOfInput;
+std::map<omega::Const_String, Variable_Ref *> functionOfOutput;
+
+AST_constraints::AST_constraints(std::set<Exp *> *f, Rel_Op r, AST_constraints *o) {
+ others = o;
+ rel_op = r;
+ first = f;
+}
+
+AST_constraints::AST_constraints(std::set<Exp *> *f, Rel_Op r, std::set<Exp *> *s) {
+ others = new AST_constraints(s);
+ rel_op = r;
+ first = f;
+}
+
+AST_constraints::AST_constraints(std::set<Exp *> *f){
+ others = 0;
+ first = f;
+}
+
+AST_constraints::~AST_constraints() {
+ for (std::set<Exp *>::iterator i = first->begin(); i != first->end(); i++)
+ delete *i;
+ delete first;
+ delete others;
+}
+
+void AST_constraints::print() {
+ for (std::set<Exp *>::iterator i = first->begin(); ;) {
+ printf(coef_fmt, (*i)->constantTerm);
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator j = (*i)->coefs.begin(); j != (*i)->coefs.end(); j++)
+ printf("+"coef_fmt"%s", (*j).second, static_cast<const char *>((*j).first->name));
+ i++;
+ if (i != first->end())
+ printf(", ");
+ else
+ break;
+ }
+}
+
+
+Exp::Exp(coef_t c) : coefs() {
+ constantTerm = c;
+}
+
+Exp::Exp(Variable_Ref *v) : coefs() {
+ assert(v != 0);
+ constantTerm = 0;
+ coefs[v] = 1;
+}
+
+Exp *negate (Exp *x) {
+ x->constantTerm = -x->constantTerm;
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = x->coefs.begin(); i != x->coefs.end(); i++)
+ (*i).second = -(*i).second;
+ return x;
+}
+
+Exp *add (Exp *x, Exp *y) {
+ x->constantTerm += y->constantTerm;
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = y->coefs.begin(); i != y->coefs.end(); i++)
+ x->coefs[(*i).first] += (*i).second;
+ delete y;
+ return x;
+}
+
+Exp *subtract (Exp *x, Exp *y) {
+ x->constantTerm -= y->constantTerm;
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = y->coefs.begin(); i != y->coefs.end(); i++)
+ x->coefs[(*i).first] -= (*i).second;
+ delete y;
+ return x;
+}
+
+Exp *multiply (coef_t c, Exp *x) {
+ x->constantTerm *= c;
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = x->coefs.begin(); i != x->coefs.end(); i++)
+ (*i).second *= c;
+ return x;
+}
+
+Exp *multiply (Exp *x, Exp *y) {
+ bool found_nonzero = false;
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = x->coefs.begin(); i != x->coefs.end(); i++)
+ if ((*i).second != 0)
+ found_nonzero = true;
+ if (!found_nonzero) {
+ coef_t c = x->constantTerm;
+ delete x;
+ return multiply(c,y);
+ }
+
+ found_nonzero = false;
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = y->coefs.begin(); i != y->coefs.end(); i++)
+ if ((*i).second != 0)
+ found_nonzero = true;
+ if (!found_nonzero) {
+ coef_t c = y->constantTerm;
+ delete y;
+ return multiply(c,x);
+ }
+
+ delete x;
+ delete y;
+ throw std::runtime_error("invalid exp multiply");
+}
+
+
+
+Declaration_Site *current_Declaration_Site = 0;
+
+Declaration_Site::Declaration_Site() {
+ previous = current_Declaration_Site;
+ current_Declaration_Site = this;
+}
+
+Declaration_Site::Declaration_Site(std::set<char *> *v) {
+ previous = current_Declaration_Site;
+ current_Declaration_Site = this;
+ for (std::set<char *>::iterator i = v->begin(); i != v->end(); i++)
+ declarations.insert(new Variable_Ref(*i));
+}
+
+Declaration_Site::~Declaration_Site() {
+ for (std::set<Variable_Ref *>::iterator i = declarations.begin(); i != declarations.end(); i++)
+ delete *i;
+}
+
+Variable_Ref::Variable_Ref(char *s, int _arity, Argument_Tuple _of) {
+ name = s;
+ arity = _arity;
+ of = _of;
+ anonymous = !strncmp("In_",s,3) || !strncmp("Out_",s,4);
+ char *t = s;
+ while (*t != '\0') t++;
+ t--;
+ while (*t == '\'') t--;
+ t++;
+ *t = '\0';
+ stripped_name = s;
+ g = 0;
+}
+
+Variable_Ref::Variable_Ref(char *s) {
+ name = s;
+ arity = 0;
+ anonymous = !strncmp("In_",s,3) || !strncmp("Out_",s,4);
+ char *t = s;
+ while (*t != '\0') t++;
+ t--;
+ while (*t == '\'') t--;
+ t++;
+ *t = '\0';
+ stripped_name = s;
+ g = 0;
+}
+
+Variable_Ref::Variable_Ref() {
+ name = "#anonymous";
+ arity = 0;
+ anonymous = 1;
+ stripped_name = name;
+ g = 0;
+}
+
+Variable_Ref::~Variable_Ref() {
+ assert(g == 0);
+}
+
+Variable_Ref *lookupScalar(char *s) {
+ Declaration_Site *ds;
+ for(ds = current_Declaration_Site; ds; ds = ds->previous)
+ for (std::set<Variable_Ref *>::iterator i = ds->declarations.begin(); i != ds->declarations.end(); i++)
+ if ((*i)->name == static_cast<Const_String>(s))
+ return (*i);
+ return NULL;
+}
+
+Declaration_Site *defined(char *s) {
+ Declaration_Site *ds;
+ for(ds = current_Declaration_Site; ds; ds = ds->previous)
+ for (std::set<Variable_Ref *>::iterator i = ds->declarations.begin(); i != ds->declarations.end(); i++)
+ if ((*i)->name == static_cast<Const_String>(s))
+ return ds;
+ return NULL;
+}
+
+
+void AST_Or::install(Formula *F) {
+ if (F->node_type() != Op_Or)
+ F = F->add_or();
+ left->install(F);
+ right->install(F);
+}
+
+void AST_And::install(Formula *F) {
+ if (F->node_type() != Op_And) F = F->add_and();
+ left->install(F);
+ right->install(F);
+}
+
+void AST_Not::install(Formula *F) {
+ child->install(F->add_not());
+}
+
+void AST_exists::install(Formula *F) {
+ F_Exists *G = F->add_exists();
+ for (std::set<Variable_Ref *>::iterator i = declaredVariables->declarations.begin(); i != declaredVariables->declarations.end(); i++)
+ (*i)->vid = G->declare((*i)->stripped_name);
+ child->install(G);
+}
+
+void AST_forall::install(Formula *F) {
+ F_Forall *G = F->add_forall();
+ for (std::set<Variable_Ref *>::iterator i = declaredVariables->declarations.begin(); i != declaredVariables->declarations.end(); i++)
+ (*i)->vid = G->declare((*i)->stripped_name);
+ child->install(G);
+}
+
+void AST_constraints::install(Formula *F) {
+ if (!others) return;
+ F_And *f = F->and_with();
+
+ for (std::set<Exp *>::iterator i = first->begin(); i != first->end(); i++)
+ for (std::set<Exp *>::iterator j = others->first->begin(); j != others->first->end(); j++)
+ switch (rel_op) {
+ case(lt) : install_gt(f, *j, *i); break;
+ case(gt) : install_gt(f, *i, *j); break;
+ case(leq) : install_geq(f, *j, *i); break;
+ case(geq) : install_geq(f, *i, *j); break;
+ case(eq) : install_eq(f, *i, *j); break;
+ case(neq) : install_neq(f, *i, *j); break;
+ default : assert(0);
+ }
+ others->install(f);
+}
+
+
+void install_neq(F_And *F, Exp *e1, Exp *e2) {
+ F_Or *or_ = F->add_or();
+ F_And *and1 = or_->add_and();
+ F_And *and2 = or_->add_and();
+ install_gt(and1,e1,e2);
+ install_gt(and2,e2,e1);
+};
+
+void install_stride(F_And *F, strideConstraint *s) {
+ Stride_Handle c = F->add_stride(s->step);
+ c.update_const(s->e->constantTerm);
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = s->e->coefs.begin(); i != s->e->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), (*i).second);
+ c.finalize();
+}
+
+void install_eq(F_And *F, Exp *e1, Exp *e2) {
+ EQ_Handle c = F->add_EQ();
+ c.update_const(e1->constantTerm);
+ if (e2) c.update_const(-e2->constantTerm);
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e1->coefs.begin(); i != e1->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), (*i).second);
+ if (e2)
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e2->coefs.begin(); i != e2->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), -(*i).second);
+ c.finalize();
+}
+
+void install_geq(F_And *F, Exp *e1, Exp *e2) {
+ GEQ_Handle c = F->add_GEQ();
+ c.update_const(e1->constantTerm);
+ if (e2) c.update_const(-e2->constantTerm);
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e1->coefs.begin(); i != e1->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), (*i).second);
+ if (e2)
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e2->coefs.begin(); i != e2->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), -(*i).second);
+ c.finalize();
+}
+
+void install_gt(F_And *F, Exp *e1, Exp *e2) {
+ GEQ_Handle c = F->add_GEQ();
+ c.update_const(-1);
+ c.update_const(e1->constantTerm);
+ if (e2) c.update_const(-e2->constantTerm);
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e1->coefs.begin(); i != e1->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), (*i).second);
+ if (e2)
+ for (std::map<Variable_Ref *, omega::coef_t>::iterator i = e2->coefs.begin(); i != e2->coefs.end(); i++)
+ c.update_coef((*i).first->id(F->relation()), -(*i).second);
+ c.finalize();
+}
+
+
+Global_Declaration_Site::~Global_Declaration_Site() {
+/* // Take care of global variables - since we do that kludge */
+/* // of declaring globals twice if arity > 0, we must take care */
+/* // not to just delete each global once per declaration. */
+
+/* // Actually, we can't free these, since Relations containing references to */
+/* // this may get freed later */
+/* foreach(v,Variable_Ref*,this->declarations,v->g=0); */
+/* //Set<Free_Var_Decl *> globals; */
+/* //foreach(v,Variable_Ref*,this->declarations,(globals.insert(v->g),v->g=0)); */
+/* //foreach(g,Free_Var_Decl*,globals,delete g); */
+
+ // Only delete global variables here. --chun 5/28/2008
+ for (std::set<Variable_Ref *>::iterator i= declarations.begin(); i != declarations.end(); i++) {
+ if ((*i)->g != 0) {
+ if ((*i)->arity != 0) { // functional symbols
+ // only delete once from a pair of "(in)" and "(out)" variables
+ const char *name = static_cast<const char *>((*i)->name);
+ const char *s = "(in)";
+ bool match = true;
+ for (size_t p = strlen(name)-4, q = 0; p < strlen(name); p++, q++)
+ if (s[q] != name[p]) {
+ match = false;
+ break;
+ }
+ if (match)
+ delete (*i)->g;
+ }
+ else // not functions
+ delete (*i)->g;
+
+ (*i)->g = 0;
+ }
+ }
+}
+
+Variable_Ref * Global_Declaration_Site::extend(char *s) {
+ Variable_Ref *r = new Variable_Ref(s);
+ r->g = new Free_Var_Decl(r->stripped_name);
+ declarations.insert(r);
+ return r;
+}
+
+void Global_Declaration_Site::extend_both_tuples(char *s, int arity) {
+ if (arity == 0)
+ extend(s);
+ else {
+ assert(arity > 0);
+
+ char s1[strlen(s)+5], s2[strlen(s)+6];
+ strcpy(s1,s); strcat(s1,"(in)");
+ strcpy(s2,s); strcat(s2,"(out)");
+ Const_String name = s;
+
+ Variable_Ref *r1 = new Variable_Ref(s1, arity, Input_Tuple);
+ Variable_Ref *r2 = new Variable_Ref(s2, arity, Output_Tuple);
+ r1->g = r2->g = new Free_Var_Decl(s,arity);
+
+ functionOfInput[name] = r1;
+ functionOfOutput[name] = r2;
+
+ declarations.insert(r1);
+ declarations.insert(r2);
+ }
+}
+
+
+void resetGlobals() {
+ for (std::set<Variable_Ref *>::iterator i = globalDecls->declarations.begin(); i != globalDecls->declarations.end(); i++)
+ (*i)->vid = 0;
+}
+
+
+Variable_Ref *Declaration_Site::extend(char *s) {
+ Variable_Ref *r = new Variable_Ref(s);
+ declarations.insert(r);
+ return r;
+}
+
+Variable_Ref *Declaration_Site::extend(char *s, Argument_Tuple of, int pos) {
+ Variable_Ref *r = new Variable_Ref(s);
+ declarations.insert(r);
+ r->of = of;
+ r->pos = pos;
+ return r;
+}
+
+Variable_Ref * Declaration_Site::extend() {
+ Variable_Ref *r = new Variable_Ref();
+ declarations.insert(r);
+ return r;
+}
+
+void tupleDescriptor::extend(char *s) {
+ Variable_Ref *r = relationDecl->extend(s);
+ size++;
+ vars.push_back(r);
+ assert(size == vars.size());
+}
+
+void tupleDescriptor::extend(char *s, Argument_Tuple of, int pos) {
+ Variable_Ref *r = relationDecl->extend(s, of, pos);
+ size++;
+ vars.push_back(r);
+ assert(size == vars.size());
+}
+
+void tupleDescriptor::extend(Exp *e) {
+ Variable_Ref *r = relationDecl->extend();
+ size++;
+ vars.push_back(r);
+ assert(size == vars.size());
+ Exp *eq = subtract(e, new Exp(r));
+ eq_constraints.insert(eq);
+}
+
+void tupleDescriptor::extend(char *s, Exp *e) {
+ Variable_Ref *r = relationDecl->extend(s);
+ size++;
+ vars.push_back(r);
+ assert(size == vars.size());
+ Exp *eq = subtract(e, new Exp(r));
+ eq_constraints.insert(eq);
+}
+
+void tupleDescriptor::extend() {
+ Variable_Ref *r = relationDecl->extend();
+ size++;
+ vars.push_back(r);
+ assert(size == vars.size());
+}
+void tupleDescriptor::extend(Exp *lb,Exp *ub) {
+ Variable_Ref *r = relationDecl->extend();
+ size++;
+ vars.push_back(r);
+ assert(size == vars.size());
+ Exp *lb_exp = subtract(new Exp(r), lb);
+ geq_constraints.insert(lb_exp);
+ Exp *ub_exp = subtract(ub, new Exp(r));
+ geq_constraints.insert(ub_exp);
+}
+void tupleDescriptor::extend(Exp *lb,Exp *ub, coef_t stride) {
+ Variable_Ref *r = relationDecl->extend();
+ size++;
+ vars.push_back(r);
+ Exp *lb_exp = subtract(new Exp(r), new Exp(*lb));
+ geq_constraints.insert(lb_exp);
+ Exp *ub_exp = subtract(ub, new Exp(r));
+ geq_constraints.insert(ub_exp);
+ strideConstraint *s = new strideConstraint;
+ s->e = subtract(lb, new Exp(r));
+ s->step = stride;
+ stride_constraints.insert(s);
+}
diff --git a/omega/omega_calc/src/myflex.cc b/omega/omega_calc/src/myflex.cc
new file mode 100755
index 0000000..89a2544
--- /dev/null
+++ b/omega/omega_calc/src/myflex.cc
@@ -0,0 +1,421 @@
+/*****************************************************************************
+ Copyright (C) 2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+ support command line editing for calculator.
+
+ Notes:
+ Since terminfo database is not queried for those nagging escape sequences,
+ current supported terminials are limited to xterm, linux, cygwin.
+
+ History:
+ 02/06/11 created by Chun Chen
+*****************************************************************************/
+
+#include <omega_calc/myflex.h>
+#include <basic/util.h>
+#include <string.h>
+#include <stdlib.h>
+
+#if defined __USE_POSIX
+#include <unistd.h>
+#include <termios.h>
+#include <sys/ioctl.h>
+#elif defined __WIN32
+#else
+#endif
+
+#define HISTORY_SIZE 100
+
+namespace {
+enum {MY_KEY_EOF=0, MY_KEY_LEFT, MY_KEY_RIGHT, MY_KEY_UP, MY_KEY_DOWN,
+ MY_KEY_DEL, MY_KEY_HOME, MY_KEY_END, MY_KEY_PGUP, MY_KEY_PGDOWN,
+ MY_KEY_NUMPAD_HOME, MY_KEY_NUMPAD_END};
+}
+
+extern bool is_interactive;
+extern const char * PROMPT_STRING;
+
+void move_cursor(int col, int n, int num_cols, const std::vector<std::string> &key_seqs) {
+ if (n == 0)
+ return;
+
+ int new_col = omega::int_mod(col + n, num_cols);
+ if (new_col == 0)
+ new_col = num_cols;
+
+ for (int i = 0; i < new_col-col; i++)
+ std::cout.write(key_seqs[MY_KEY_RIGHT].c_str(), key_seqs[MY_KEY_RIGHT].length());
+ for (int i = 0; i < col-new_col; i++)
+ std::cout.write(key_seqs[MY_KEY_LEFT].c_str(), key_seqs[MY_KEY_LEFT].length());
+
+ if (n < 0)
+ for (int i = 0; i < omega::abs(n) / num_cols + (new_col>col)?1:0; i++)
+ std::cout.write(key_seqs[MY_KEY_UP].c_str(), key_seqs[MY_KEY_UP].length());
+ else
+ for (int i = 0; i < omega::abs(n) / num_cols + (new_col<col)?1:0; i++)
+ std::cout.write(key_seqs[MY_KEY_DOWN].c_str(), key_seqs[MY_KEY_DOWN].length());
+}
+
+
+
+myFlexLexer::myFlexLexer(std::istream *arg_yyin, std::ostream *arg_yyout):
+ yyFlexLexer(arg_yyin, arg_yyout), history(HISTORY_SIZE), key_seqs(12) {
+ cur_pos = 0;
+ first_history_pos = 0;
+ last_history_pos = -1;
+
+ if (strcmp(getenv("TERM"), "xterm") == 0 ||
+ strcmp(getenv("TERM"), "xterm-color") == 0) {
+ key_seqs[MY_KEY_EOF] = "\x04";
+ key_seqs[MY_KEY_LEFT] = "\x1B\x5B\x44";
+ key_seqs[MY_KEY_RIGHT] = "\x1B\x5B\x43";
+ key_seqs[MY_KEY_UP] = "\x1B\x5B\x41";
+ key_seqs[MY_KEY_DOWN] = "\x1B\x5B\x42";
+ key_seqs[MY_KEY_DEL] = "\x1B\x5B\x33\x7E";
+ key_seqs[MY_KEY_HOME] = "\x1B\x4F\x48";
+ key_seqs[MY_KEY_END] = "\x1B\x4F\x46";
+ key_seqs[MY_KEY_PGUP] = "\x1B\x5B\x35\x7E";
+ key_seqs[MY_KEY_PGDOWN] = "\x1B\x5B\x36\x7E";
+ key_seqs[MY_KEY_NUMPAD_HOME] = "\x1B\x5B\x31\x7E";
+ key_seqs[MY_KEY_NUMPAD_END] = "\x1B\x5B\x34\x7E";
+ }
+ else if (strcmp(getenv("TERM"), "linux") == 0 ||
+ strcmp(getenv("TERM"), "cygwin") == 0) {
+ key_seqs[MY_KEY_EOF] = "\x04";
+ key_seqs[MY_KEY_LEFT] = "\x1B\x5B\x44";
+ key_seqs[MY_KEY_RIGHT] = "\x1B\x5B\x43";
+ key_seqs[MY_KEY_UP] = "\x1B\x5B\x41";
+ key_seqs[MY_KEY_DOWN] = "\x1B\x5B\x42";
+ key_seqs[MY_KEY_DEL] = "\x1B\x5B\x33\x7E";
+ key_seqs[MY_KEY_HOME] = "\x1B\x5B\x31\x7E";
+ key_seqs[MY_KEY_END] = "\x1B\x5B\x34\x7E";
+ key_seqs[MY_KEY_PGUP] = "\x1B\x5B\x35\x7E";
+ key_seqs[MY_KEY_PGDOWN] = "\x1B\x5B\x36\x7E";
+ key_seqs[MY_KEY_NUMPAD_HOME] = "\x1B\x5B\x31\x7E";
+ key_seqs[MY_KEY_NUMPAD_END] = "\x1B\x5B\x34\x7E";
+ }
+ else {
+ key_seqs[MY_KEY_EOF] = "\x04";
+ }
+}
+
+int myFlexLexer::LexerInput(char *buf, int max_size) {
+ if (!is_interactive)
+ return yyFlexLexer::LexerInput(buf, max_size);
+
+#if defined __USE_POSIX
+ winsize wsz;
+ ioctl(0, TIOCGWINSZ, &wsz);
+ int num_cols = wsz.ws_col;
+
+ // unknown screen size, bail out
+ if (num_cols == 0)
+ return yyFlexLexer::LexerInput(buf, max_size);
+
+ termios old_settings;
+ termios new_settings;
+ char keycodes[255];
+
+ // set console to no echo, raw input mode
+ tcgetattr(STDIN_FILENO, &old_settings);
+ new_settings = old_settings;
+ new_settings.c_cc[VTIME] = 1;
+ new_settings.c_cc[VMIN] = 1;
+ new_settings.c_iflag &= ~(IXOFF);
+ new_settings.c_lflag &= ~(ECHO|ICANON);
+ tcsetattr(STDIN_FILENO, TCSANOW, &new_settings);
+
+ int cur_history_pos = (last_history_pos+1)%HISTORY_SIZE;
+ while (true) {
+ // feed current line to lex
+ int len = cur_line.length();
+ if (len > 0 && cur_line[len-1] == '\n') {
+ int n = omega::min(len-cur_pos, max_size);
+ for (int i = 0; i < n; i++)
+ buf[i] = cur_line[cur_pos+i];
+ cur_pos = cur_pos + n;
+ if (cur_pos == len) {
+ // save history
+ if (len > 1) {
+ if (last_history_pos == -1)
+ last_history_pos = 0;
+ else {
+ last_history_pos = (last_history_pos+1)%HISTORY_SIZE;
+ if ((last_history_pos + 1)%HISTORY_SIZE == first_history_pos)
+ first_history_pos = (first_history_pos+1)%HISTORY_SIZE;
+ }
+ history[last_history_pos] = cur_line.substr(0, len-1);
+ cur_history_pos = (last_history_pos+1)%HISTORY_SIZE;
+ }
+
+ // clear the working line
+ cur_pos = 0;
+ cur_line.clear();
+ }
+ tcsetattr(STDIN_FILENO, TCSANOW, &old_settings);
+ return n;
+ }
+
+ int count = read(STDIN_FILENO, keycodes, 255);
+
+ // handle special key my way
+ int eaten = 0;
+ while (eaten < count) {
+ if (key_seqs[MY_KEY_EOF].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_EOF].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_EOF].c_str(), key_seqs[MY_KEY_EOF].length()) == 0) {
+ if (cur_line.length() == 0) {
+ tcsetattr(STDIN_FILENO, TCSANOW, &old_settings);
+ return 0;
+ }
+
+ eaten += key_seqs[MY_KEY_EOF].length();
+ }
+ else if (key_seqs[MY_KEY_LEFT].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_LEFT].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_LEFT].c_str(), key_seqs[MY_KEY_LEFT].length()) == 0) {
+ if (cur_pos > 0) {
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ cur_pos--;
+
+ move_cursor(cur_col, -1, num_cols, key_seqs);
+ }
+ eaten += key_seqs[MY_KEY_LEFT].length();
+ }
+ else if (key_seqs[MY_KEY_RIGHT].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_RIGHT].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_RIGHT].c_str(), key_seqs[MY_KEY_RIGHT].length()) == 0) {
+ if (static_cast<size_t>(cur_pos) < cur_line.length()) {
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ cur_pos++;
+
+ move_cursor(cur_col, 1, num_cols, key_seqs);
+ }
+ eaten += key_seqs[MY_KEY_RIGHT].length();
+ }
+ else if (key_seqs[MY_KEY_UP].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_UP].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_UP].c_str(), key_seqs[MY_KEY_UP].length()) == 0) {
+ if (cur_history_pos >= 0 && cur_history_pos != first_history_pos) {
+ history[cur_history_pos] = cur_line;
+ cur_history_pos = omega::int_mod(cur_history_pos-1, HISTORY_SIZE);
+
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ move_cursor(cur_col, -cur_pos, num_cols, key_seqs);
+
+ std::cout.write(history[cur_history_pos].c_str(), history[cur_history_pos].length());
+
+ cur_col = (history[cur_history_pos].length() + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0) {
+ std::cout.put(' ');
+ std::cout.put('\b');
+ }
+
+ if (cur_line.length() > history[cur_history_pos].length()) {
+ for (size_t i = 0; i < cur_line.length() - history[cur_history_pos].length(); i++)
+ std::cout.put(' ');
+
+ cur_col = (cur_line.length() + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols + 1;
+ else
+ cur_col++;
+
+ move_cursor(cur_col, -(cur_line.length() - history[cur_history_pos].length()), num_cols, key_seqs);
+ }
+ cur_line = history[cur_history_pos];
+ cur_pos = cur_line.length();
+ }
+
+ eaten += key_seqs[MY_KEY_UP].length();
+ }
+ else if (key_seqs[MY_KEY_DOWN].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_DOWN].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_DOWN].c_str(), key_seqs[MY_KEY_DOWN].length()) == 0) {
+ if (cur_history_pos >= 0 && cur_history_pos != (last_history_pos+1)%HISTORY_SIZE) {
+ history[cur_history_pos] = cur_line;
+ cur_history_pos = (cur_history_pos+1)%HISTORY_SIZE;
+
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ move_cursor(cur_col, -cur_pos, num_cols, key_seqs);
+
+ std::cout.write(history[cur_history_pos].c_str(), history[cur_history_pos].length());
+
+ cur_col = (history[cur_history_pos].length() + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0) {
+ std::cout.put(' ');
+ std::cout.put('\b');
+ }
+
+ if (cur_line.length() > history[cur_history_pos].length()) {
+ for (size_t i = 0; i < cur_line.length() - history[cur_history_pos].length(); i++)
+ std::cout.put(' ');
+
+ cur_col = (cur_line.length() + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols + 1;
+ else
+ cur_col++;
+
+ move_cursor(cur_col, -(cur_line.length() - history[cur_history_pos].length()), num_cols, key_seqs);
+ }
+ cur_line = history[cur_history_pos];
+ cur_pos = cur_line.length();
+ }
+
+ eaten += key_seqs[MY_KEY_DOWN].length();
+ }
+ else if (key_seqs[MY_KEY_DEL].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_DEL].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_DEL].c_str(), key_seqs[MY_KEY_DEL].length()) == 0) {
+ if (static_cast<size_t>(cur_pos) < cur_line.length()) {
+ cur_line.erase(cur_pos, 1);
+ std::cout.write(&(cur_line.c_str()[cur_pos]), cur_line.length()-cur_pos);
+ std::cout.put(' ');
+
+ int cur_col = (cur_line.length() + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols + 1;
+ else
+ cur_col++;
+
+ move_cursor(cur_col, -(cur_line.length()-cur_pos+1), num_cols, key_seqs);
+ }
+
+ eaten += key_seqs[MY_KEY_DEL].length();
+ }
+ else if (key_seqs[MY_KEY_HOME].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_HOME].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_HOME].c_str(), key_seqs[MY_KEY_HOME].length()) == 0) {
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ move_cursor(cur_col, -cur_pos, num_cols, key_seqs);
+
+ cur_pos = 0;
+ eaten += key_seqs[MY_KEY_HOME].length();
+ }
+ else if (key_seqs[MY_KEY_END].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_END].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_END].c_str(), key_seqs[MY_KEY_END].length()) == 0) {
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ move_cursor(cur_col, cur_line.length()-cur_pos, num_cols, key_seqs);
+
+ cur_pos = cur_line.length();
+ eaten += key_seqs[MY_KEY_END].length();
+ }
+ else if (key_seqs[MY_KEY_PGUP].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_PGUP].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_PGUP].c_str(), key_seqs[MY_KEY_PGUP].length()) == 0) {
+ eaten += key_seqs[MY_KEY_PGUP].length();
+ }
+ else if (key_seqs[MY_KEY_PGDOWN].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_PGDOWN].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_PGDOWN].c_str(), key_seqs[MY_KEY_PGDOWN].length()) == 0) {
+ eaten += key_seqs[MY_KEY_PGDOWN].length();
+ }
+ else if (key_seqs[MY_KEY_NUMPAD_HOME].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_NUMPAD_HOME].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_NUMPAD_HOME].c_str(), key_seqs[MY_KEY_NUMPAD_HOME].length()) == 0) {
+ eaten += key_seqs[MY_KEY_NUMPAD_HOME].length();
+ }
+ else if (key_seqs[MY_KEY_NUMPAD_END].length() > 0 &&
+ static_cast<size_t>(count - eaten) >= key_seqs[MY_KEY_NUMPAD_END].length() &&
+ strncmp(&keycodes[eaten], key_seqs[MY_KEY_NUMPAD_END].c_str(), key_seqs[MY_KEY_NUMPAD_END].length()) == 0) {
+ eaten += key_seqs[MY_KEY_NUMPAD_END].length();
+ }
+ else if (keycodes[eaten] == '\x1B' && (count - eaten == 1 || keycodes[eaten+1] == '\x1B')) { // single ESC key
+ eaten++;
+ }
+ else if (keycodes[eaten] == '\x1B') { // unknown escape sequences
+ while (eaten+1 < count && keycodes[eaten+1] != '\x1B')
+ eaten++;
+
+ keycodes[eaten] = '~';
+ }
+ else if (keycodes[eaten] == '\x7F') { // backspace key
+ if (cur_pos > 0) {
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ cur_pos--;
+ cur_line.erase(cur_pos, 1);
+
+ move_cursor(cur_col, -1, num_cols, key_seqs);
+
+ std::cout.write(&(cur_line.c_str()[cur_pos]), cur_line.length()-cur_pos);
+ std::cout.put(' ');
+
+ cur_col = (cur_line.length() + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols + 1;
+ else
+ cur_col++;
+
+ move_cursor(cur_col, -(cur_line.length()-cur_pos+1), num_cols, key_seqs);
+ }
+
+ eaten++;
+ }
+ else if (keycodes[eaten] == '\n'){ // return key
+ int cur_col = (cur_pos + 1 + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0)
+ cur_col = num_cols;
+
+ move_cursor(cur_col, cur_line.length()-cur_pos, num_cols, key_seqs);
+
+ std::cout.put(keycodes[eaten]);
+ cur_line.append(1, '\n');
+ cur_pos = 0;
+ break;
+ }
+ else { // all other key
+ std::cout.put(keycodes[eaten]);
+ std::cout.write(&(cur_line.c_str()[cur_pos]), cur_line.length()-cur_pos);
+
+ cur_line.insert(cur_pos, &keycodes[eaten], 1);
+ cur_pos++;
+
+ int cur_col = (cur_line.length() + strlen(PROMPT_STRING) + 1) % num_cols;
+ if (cur_col == 0) {
+ // force cursor to move to the next line when the last printed char is at
+ // the right boundary of the terminal
+ std::cout.put(' ');
+ std::cout.put('\b');
+
+ cur_col = 1;
+ }
+ else
+ cur_col++;
+
+ move_cursor(cur_col, -(cur_line.length()-cur_pos), num_cols, key_seqs);
+
+ eaten++;
+ }
+
+ std::cout.flush();
+ }
+ }
+#else
+ return yyFlexLexer::LexerInput(buf, max_size);
+#endif
+}
diff --git a/omega/omega_calc/src/parser.l b/omega/omega_calc/src/parser.l
new file mode 100644
index 0000000..ac2b448
--- /dev/null
+++ b/omega/omega_calc/src/parser.l
@@ -0,0 +1,350 @@
+%{
+#include <stdio.h>
+#include <string>
+#include <sstream>
+#include <iostream>
+#include <omega_calc/AST.h>
+#include <basic/Dynamic_Array.h>
+
+using namespace omega;
+#include "y.tab.h"
+
+#define BUFFER scanBuf += yytext
+std::string scanBuf;
+std::string err_msg;
+
+extern "C" int yywrap() {return 1;};
+
+
+#define MAX_INCLUDE_DEPTH 10
+YY_BUFFER_STATE include_stack[MAX_INCLUDE_DEPTH];
+int include_stack_ptr = 0;
+int comment_caller;
+
+extern bool is_interactive;
+extern const char *PROMPT_STRING;
+extern bool need_coef;
+
+// void yyerror(const char *s);
+void yyerror(const std::string &s);
+void flushScanBuffer();
+
+%}
+
+%s LATEX INCLUDE COMMENT
+%option yylineno
+
+%%
+
+"<<" { BUFFER; BEGIN(INCLUDE); }
+<INCLUDE>[^>\n ]+">>" {
+ BUFFER;
+ scanBuf += "\n";
+ flushScanBuffer();
+
+ if (include_stack_ptr >= MAX_INCLUDE_DEPTH) {
+ fprintf(stderr, "File including nested too deeply, abort");
+ exit(1);
+ }
+
+ char *s = yytext;
+ while (*s != '>') s++;
+ *s = '\0';
+ FILE *f = fopen(yytext, "r");
+ if (!f) {
+ fprintf(stderr, "Can't open file %s\n", yytext);
+ }
+ else {
+ include_stack[include_stack_ptr++] = YY_CURRENT_BUFFER;
+ yyin = f;
+ yy_switch_to_buffer(yy_create_buffer(yyin, YY_BUF_SIZE));
+ }
+ BEGIN(INITIAL);
+}
+<INCLUDE>[ \n] {
+ fprintf(stderr,"Error in include syntax\n");
+ fprintf(stderr,"Use <<fname>> to include the file named fname\n");
+ BEGIN(INITIAL);
+ if(is_interactive && include_stack_ptr == 0)
+ printf("%s ", PROMPT_STRING);
+}
+
+<COMMENT>\n {
+ BUFFER;
+ BEGIN(comment_caller);
+ if(is_interactive && include_stack_ptr == 0)
+ printf("%s ", PROMPT_STRING);
+}
+
+\n {
+ BUFFER;
+ if(is_interactive && include_stack_ptr == 0)
+ printf("%s ", PROMPT_STRING);
+}
+
+<LATEX>"\\ " { BUFFER; }
+[ \t]+ { BUFFER; }
+# { BUFFER; comment_caller = YY_START; BEGIN(COMMENT); }
+<COMMENT>.* { BUFFER; flushScanBuffer(); }
+<LATEX>"\$\$" { BUFFER; BEGIN(INITIAL); }
+"\$\$" { BUFFER; BEGIN(LATEX); }
+<LATEX>"\\t" { BUFFER; }
+<LATEX>"\\!" { BUFFER; }
+<LATEX>"\\\\" { BUFFER; }
+
+"{" { BUFFER; return OPEN_BRACE; }
+<LATEX>"\\{" { BUFFER; return OPEN_BRACE; }
+"}" { BUFFER; return CLOSE_BRACE; }
+<LATEX>"\\}" { BUFFER; return CLOSE_BRACE; }
+"approximate" { BUFFER; return APPROX; }
+"union" { BUFFER; return UNION; }
+<LATEX>"\\cup" { BUFFER; return UNION; }
+"intersection" { BUFFER; return INTERSECTION; }
+<LATEX>"\\cap" { BUFFER; return INTERSECTION; }
+"symbolic" { BUFFER; return SYMBOLIC; }
+"sym" { BUFFER; return SYMBOLIC; }
+<LATEX>"\\mid" { BUFFER; return VERTICAL_BAR; }
+<LATEX>"|" { BUFFER; return VERTICAL_BAR; }
+<LATEX>"\\st" { BUFFER; return SUCH_THAT; }
+"s.t." { BUFFER; return SUCH_THAT; }
+"inverse" { BUFFER; return INVERSE; }
+"complement" { BUFFER; return COMPLEMENT; }
+<LATEX>"\\circ" { BUFFER; return COMPOSE; }
+"compose" { BUFFER; return COMPOSE; }
+"difference" { BUFFER; return DIFFERENCE; }
+"diffToRel" { BUFFER; return DIFFERENCE_TO_RELATION; }
+"project away symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
+"project_away_symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
+"projectAwaySymbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
+"project on symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
+"project_on_symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
+"projectOnSymbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
+<LATEX>"\\join" { BUFFER; return JOIN; }
+"\." { BUFFER; return JOIN; }
+"join" { BUFFER; return JOIN; }
+"domain" { BUFFER; return DOMAIN; }
+"time" { BUFFER; return TIME; }
+"timeclosure" { BUFFER; return TIMECLOSURE; }
+"range" { BUFFER; return RANGE; }
+<LATEX>"\\forall" { BUFFER; return FORALL; }
+"forall" { BUFFER; return FORALL; }
+<LATEX>"\\exists" { BUFFER; return EXISTS; }
+"exists" { BUFFER; return EXISTS; }
+
+"Venn" { BUFFER; return VENN; }
+"ConvexRepresentation" { BUFFER; return CONVEX_REPRESENTATION; }
+"ConvexCombination" { BUFFER; return CONVEX_COMBINATION; }
+"PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; }
+"LinearCombination" { BUFFER; return LINEAR_COMBINATION; }
+"AffineCombination" { BUFFER; return AFFINE_COMBINATION; }
+"RectHull" { BUFFER; return RECT_HULL; }
+"ConvexHull" { BUFFER; return CONVEX_HULL; }
+"DecoupledConvexHull" { BUFFER; return DECOUPLED_CONVEX_HULL; }
+"AffineHull" { BUFFER; return AFFINE_HULL; }
+"ConicHull" { BUFFER; return CONIC_HULL; }
+"LinearHull" { BUFFER; return LINEAR_HULL; }
+"PairwiseCheck" { /*deprecated*/ BUFFER; return PAIRWISE_CHECK; }
+"ConvexCheck" { /*deprecated*/ BUFFER; return CONVEX_CHECK; }
+"QuickHull" { /*deprecated*/ BUFFER; return QUICK_HULL; }
+"hull" { BUFFER; return HULL; }
+
+"minimize" { BUFFER; return MINIMIZE; }
+"maximize" { BUFFER; return MAXIMIZE; }
+"minimize-range" { BUFFER; return MINIMIZE_RANGE; }
+"maximize-range" { BUFFER; return MAXIMIZE_RANGE; }
+"minimizerange" { BUFFER; return MINIMIZE_RANGE; }
+"maximizerange" { BUFFER; return MAXIMIZE_RANGE; }
+"minimize-domain" { BUFFER; return MINIMIZE_DOMAIN; }
+"maximize-domain" { BUFFER; return MAXIMIZE_DOMAIN; }
+"minimizedomain" { BUFFER; return MINIMIZE_DOMAIN; }
+"maximizedomain" { BUFFER; return MAXIMIZE_DOMAIN; }
+"gist" { BUFFER; return GIST; }
+"given" { BUFFER; return GIVEN; }
+"within" { BUFFER; return WITHIN; }
+"subset" { BUFFER; return SUBSET; }
+"codegen" { BUFFER; return CODEGEN; }
+"farkas" { BUFFER; return FARKAS; }
+"decoupledfarkas" { BUFFER; return DECOUPLED_FARKAS; }
+"decoupled-farkas" { BUFFER; return DECOUPLED_FARKAS; }
+"decoupled_farkas" { BUFFER; return DECOUPLED_FARKAS; }
+"upper_bound" { BUFFER; return MAKE_UPPER_BOUND; }
+"lower_bound" { BUFFER; return MAKE_LOWER_BOUND; }
+"supersetof" { BUFFER; return SUPERSETOF;}
+"subsetof" { BUFFER; return SUBSETOF;}
+"sym_example" { BUFFER; return SYM_SAMPLE;}
+"example" { BUFFER; return SAMPLE;}
+"carried_by" { BUFFER; return CARRIED_BY;}
+"reachable" { BUFFER; return REACHABLE_FROM; }
+"reachable of" { BUFFER; return REACHABLE_OF; }
+"restrict_domain" { BUFFER; return RESTRICT_DOMAIN; }
+"restrictDomain" { BUFFER; return RESTRICT_DOMAIN; }
+<LATEX>"\\" { yyerror("Can't use \\ for restrict_domain in Tex mode"); }
+"\\" { BUFFER; return RESTRICT_DOMAIN; }
+"restrict_range" { BUFFER; return RESTRICT_RANGE; }
+"restrictRange" { BUFFER; return RESTRICT_RANGE; }
+"assertUnsatisfiable" { BUFFER; return ASSERT_UNSAT; }
+"assert_unsatisfiable" { BUFFER; return ASSERT_UNSAT; }
+
+"/" { BUFFER; return RESTRICT_RANGE; }
+"&" { BUFFER; return AND; }
+"|" { BUFFER; return OR; }
+"&&" { BUFFER; return AND; }
+"||" { BUFFER; return OR; }
+"and" { BUFFER; return AND; }
+"or" { BUFFER; return OR; }
+<LATEX>"\\land" { BUFFER; return AND; }
+<LATEX>"\\lor" { BUFFER; return OR; }
+"!" { BUFFER; return NOT; }
+"not" { BUFFER; return NOT; }
+<LATEX>"\\neg" { BUFFER; return NOT; }
+":=" { BUFFER; return IS_ASSIGNED; }
+"->" { BUFFER; return GOES_TO; }
+"in" { BUFFER; return IN; }
+<LATEX>"\\rightarrow" { BUFFER; return GOES_TO; }
+"<=" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; }
+<LATEX>"\\leq" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; }
+<LATEX>"\\le" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; }
+">=" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; }
+<LATEX>"\\geq" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; }
+<LATEX>"\\ge" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; }
+"!=" { BUFFER; yylval.REL_OPERATOR = neq; return REL_OP; }
+<LATEX>"\\neq" { BUFFER; yylval.REL_OPERATOR = neq; return REL_OP; }
+"<" { BUFFER; yylval.REL_OPERATOR = lt; return REL_OP; }
+">" { BUFFER; yylval.REL_OPERATOR = gt; return REL_OP; }
+"=" { BUFFER; yylval.REL_OPERATOR = eq; return REL_OP; }
+"==" { BUFFER; yylval.REL_OPERATOR = eq; return REL_OP; }
+
+[A-Za-z][A-Za-z0-9_]*[\']* {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ return VAR;
+}
+[A-Za-z][A-Za-z0-9_]*"(in)" {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
+ yylval.VAR_NAME[yyleng-2] = 'n';
+ return VAR;
+}
+[A-Za-z][A-Za-z0-9_]*"(set)" {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
+ yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
+ yylval.VAR_NAME[yyleng-2] = ')';
+ yylval.VAR_NAME[yyleng-1] = '\0';
+ return VAR;
+}
+[A-Za-z][A-Za-z0-9_]*"(out)" {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
+ yylval.VAR_NAME[yyleng-3] = 'u';
+ yylval.VAR_NAME[yyleng-2] = 't';
+ return VAR;
+}
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]* {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ return VAR;
+ }
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(in)" {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
+ yylval.VAR_NAME[yyleng-2] = 'n';
+ return VAR;
+ }
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(set)" {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
+ yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
+ yylval.VAR_NAME[yyleng-2] = ')';
+ yylval.VAR_NAME[yyleng-1] = '\0';
+ return VAR;
+ }
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(out)" {
+ BUFFER;
+ if (yyleng > 19) yyerror("Identifier too long");
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
+ yylval.VAR_NAME[yyleng-3] = 'u';
+ yylval.VAR_NAME[yyleng-2] = 't';
+ return VAR;
+ }
+
+[0-9]+ { BUFFER;
+ if (need_coef) {
+ sscanf(yytext, coef_fmt, &yylval.COEF_VALUE);
+ return COEF;
+ }
+ else {
+ yylval.INT_VALUE = atoi(yytext);
+ return INT;
+ }
+}
+
+\"[^\"]*\" { BUFFER;
+ yytext[strlen(yytext)-1]='\0';
+ yylval.STRING_VALUE = new std::string(yytext+1);
+ return STRING;
+}
+
+
+<<EOF>> {
+ if (--include_stack_ptr < 0) {
+ flushScanBuffer();
+ return yytext[0];
+ }
+ yy_delete_buffer(YY_CURRENT_BUFFER);
+ yy_switch_to_buffer(include_stack[include_stack_ptr]);
+}
+
+. { BUFFER; return yytext[0]; }
+
+
+%%
+
+void yyerror(const std::string &s) {
+ std::stringstream ss;
+ if (is_interactive && include_stack_ptr == 0)
+ ss << s << "\n";
+ else
+ ss << s << " at line " << yylineno << "\n";
+ err_msg = ss.str();
+}
+
+
+void flushScanBuffer() {
+ if (scanBuf.size() == 0)
+ return;
+ if (!is_interactive || include_stack_ptr > 0) {
+ size_t prev_pos = 0;
+ if (scanBuf[0] == '\n')
+ prev_pos = 1;
+ for (size_t pos = prev_pos; pos <= scanBuf.size(); pos++) {
+ if (pos == scanBuf.size() || scanBuf[pos] == '\n') {
+ std::cout << PROMPT_STRING << " " << scanBuf.substr(prev_pos, pos-prev_pos) << std::endl;
+ prev_pos = pos+1;
+ }
+ }
+ }
+
+ scanBuf.clear();
+}
diff --git a/omega/omega_calc/src/parser.ll b/omega/omega_calc/src/parser.ll
new file mode 100755
index 0000000..86de3a4
--- /dev/null
+++ b/omega/omega_calc/src/parser.ll
@@ -0,0 +1,350 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2005-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+ lex parser for calculator.
+
+ Notes:
+
+ History:
+ 02/04/11 migrate to flex c++ mode, Chun Chen
+*****************************************************************************/
+
+%{
+#include <stdio.h>
+#include <string.h>
+#include <string>
+#include <sstream>
+#include <iostream>
+#include <fstream>
+#include <omega_calc/AST.h>
+#include <basic/Dynamic_Array.h>
+#include "parser.tab.hh"
+#include <omega_calc/myflex.h>
+
+myFlexLexer mylexer;
+bool is_interactive;
+const char *PROMPT_STRING = ">>>";
+
+#define BUFFER scanBuf += yytext
+std::string scanBuf;
+std::string err_msg;
+
+extern bool need_coef;
+
+void yyerror(const std::string &s);
+void flushScanBuffer();
+
+%}
+
+%s LATEX INCLUDE COMMENT
+%option yylineno
+%option noyywrap
+
+%%
+
+"<<" { BUFFER; BEGIN(INCLUDE); }
+<INCLUDE>[^>\n ]+">>" {
+ BUFFER;
+ scanBuf += "\n";
+ flushScanBuffer();
+
+ if (is_interactive) {
+ std::cout << "file include disabled in interactive mode\n";
+ }
+ else {
+ char *s = yytext;
+ while (*s != '>') s++;
+ *s = '\0';
+ std::ifstream *ifs = new std::ifstream(yytext, std::ifstream::in);
+ if (!ifs->is_open()) {
+ fprintf(stderr, "Can't open file %s\n", yytext);
+ }
+ else {
+ yy_buffer_state *bs = mylexer.yy_create_buffer(ifs, 8092);
+ mylexer.yypush_buffer_state(bs);
+ }
+ }
+ BEGIN(INITIAL);
+}
+<INCLUDE>[ \n] {
+ std::cout << "Error in include syntax\n";
+ std::cout << "Use <<fname>> to include the file named fname\n";
+ BEGIN(INITIAL);
+ if(is_interactive) {
+ std::cout << PROMPT_STRING << ' ';
+ std::cout.flush();
+ }
+}
+
+
+
+
+
+<LATEX>"\\ " { BUFFER; }
+[ \t]+ { BUFFER; }
+# { BUFFER; BEGIN(COMMENT); }
+<COMMENT>.* { BUFFER; }
+<LATEX>"\$\$\n" { BUFFER; BEGIN(INITIAL); }
+<LATEX>"\$\$" { BUFFER; BEGIN(INITIAL); }
+"\$\$" { BUFFER; BEGIN(LATEX); }
+<LATEX>"\\n" { BUFFER; }
+<LATEX>"\\t" { BUFFER; }
+<LATEX>"\\!" { BUFFER; }
+<LATEX>"\\\\" { BUFFER; }
+<LATEX>"\n" { BUFFER; }
+
+
+\n {
+ BUFFER;
+ BEGIN(INITIAL);
+ if(is_interactive) {
+ std::cout << PROMPT_STRING << ' ';
+ std::cout.flush();
+ }
+}
+
+
+
+
+
+"{" { BUFFER; return OPEN_BRACE; }
+<LATEX>"\\{" { BUFFER; return OPEN_BRACE; }
+"}" { BUFFER; return CLOSE_BRACE; }
+<LATEX>"\\}" { BUFFER; return CLOSE_BRACE; }
+"approximate" { BUFFER; return APPROX; }
+"union" { BUFFER; return UNION; }
+<LATEX>"\\cup" { BUFFER; return UNION; }
+"intersection" { BUFFER; return INTERSECTION; }
+<LATEX>"\\cap" { BUFFER; return INTERSECTION; }
+"without_simplify" { BUFFER; return NO_SIMPLIFY; }
+"symbolic" { BUFFER; return SYMBOLIC; }
+"sym" { BUFFER; return SYMBOLIC; }
+<LATEX>"\\mid" { BUFFER; return VERTICAL_BAR; }
+<LATEX>"|" { BUFFER; return VERTICAL_BAR; }
+<LATEX>"\\st" { BUFFER; return SUCH_THAT; }
+"s.t." { BUFFER; return SUCH_THAT; }
+"inverse" { BUFFER; return INVERSE; }
+"complement" { BUFFER; return COMPLEMENT; }
+<LATEX>"\\circ" { BUFFER; return COMPOSE; }
+"compose" { BUFFER; return COMPOSE; }
+"difference" { BUFFER; return DIFFERENCE; }
+"diffToRel" { BUFFER; return DIFFERENCE_TO_RELATION; }
+"project away symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
+"project_away_symbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
+"projectAwaySymbols" { BUFFER; return PROJECT_AWAY_SYMBOLS; }
+"project on symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
+"project_on_symbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
+"projectOnSymbols" { BUFFER; return PROJECT_ON_SYMBOLS; }
+<LATEX>"\\join" { BUFFER; return JOIN; }
+"\." { BUFFER; return JOIN; }
+"join" { BUFFER; return JOIN; }
+"domain" { BUFFER; return DOMAIN; }
+"time" { BUFFER; return TIME; }
+"timeclosure" { BUFFER; return TIMECLOSURE; }
+"range" { BUFFER; return RANGE; }
+<LATEX>"\\forall" { BUFFER; return FORALL; }
+"forall" { BUFFER; return FORALL; }
+<LATEX>"\\exists" { BUFFER; return EXISTS; }
+"exists" { BUFFER; return EXISTS; }
+
+"Venn" { BUFFER; return VENN; }
+"ConvexRepresentation" { BUFFER; return CONVEX_REPRESENTATION; }
+"ConvexCombination" { BUFFER; return CONVEX_COMBINATION; }
+"PositiveCombination" { BUFFER; return POSITIVE_COMBINATION; }
+"LinearCombination" { BUFFER; return LINEAR_COMBINATION; }
+"AffineCombination" { BUFFER; return AFFINE_COMBINATION; }
+"RectHull" { /*deprecated*/ BUFFER; return RECT_HULL; }
+"SimpleHull" { BUFFER; return SIMPLE_HULL; }
+"ConvexHull" { BUFFER; return CONVEX_HULL; }
+"DecoupledConvexHull" { BUFFER; return DECOUPLED_CONVEX_HULL; }
+"AffineHull" { BUFFER; return AFFINE_HULL; }
+"ConicHull" { BUFFER; return CONIC_HULL; }
+"LinearHull" { BUFFER; return LINEAR_HULL; }
+"PairwiseCheck" { /*deprecated*/ BUFFER; return PAIRWISE_CHECK; }
+"ConvexCheck" { /*deprecated*/ BUFFER; return CONVEX_CHECK; }
+"QuickHull" { /*deprecated*/ BUFFER; return QUICK_HULL; }
+"Hull" { BUFFER; return HULL; }
+"farkas" { BUFFER; return FARKAS; }
+"decoupledfarkas" { BUFFER; return DECOUPLED_FARKAS; }
+"decoupled-farkas" { BUFFER; return DECOUPLED_FARKAS; }
+"decoupled_farkas" { BUFFER; return DECOUPLED_FARKAS; }
+
+"minimize" { BUFFER; return MINIMIZE; }
+"maximize" { BUFFER; return MAXIMIZE; }
+"minimize-range" { BUFFER; return MINIMIZE_RANGE; }
+"maximize-range" { BUFFER; return MAXIMIZE_RANGE; }
+"minimizerange" { BUFFER; return MINIMIZE_RANGE; }
+"maximizerange" { BUFFER; return MAXIMIZE_RANGE; }
+"minimize-domain" { BUFFER; return MINIMIZE_DOMAIN; }
+"maximize-domain" { BUFFER; return MAXIMIZE_DOMAIN; }
+"minimizedomain" { BUFFER; return MINIMIZE_DOMAIN; }
+"maximizedomain" { BUFFER; return MAXIMIZE_DOMAIN; }
+"gist" { BUFFER; return GIST; }
+"given" { BUFFER; return GIVEN; }
+"within" { BUFFER; return WITHIN; }
+"subset" { BUFFER; return SUBSET; }
+"codegen" { BUFFER; return CODEGEN; }
+"upper_bound" { BUFFER; return MAKE_UPPER_BOUND; }
+"lower_bound" { BUFFER; return MAKE_LOWER_BOUND; }
+"supersetof" { BUFFER; return SUPERSETOF;}
+"subsetof" { BUFFER; return SUBSETOF;}
+"sym_example" { BUFFER; return SYM_SAMPLE;}
+"example" { BUFFER; return SAMPLE;}
+"carried_by" { BUFFER; return CARRIED_BY;}
+"reachable" { BUFFER; return REACHABLE_FROM; }
+"reachable of" { BUFFER; return REACHABLE_OF; }
+"restrict_domain" { BUFFER; return RESTRICT_DOMAIN; }
+"restrictDomain" { BUFFER; return RESTRICT_DOMAIN; }
+"\\" { BUFFER; return RESTRICT_DOMAIN; }
+"restrict_range" { BUFFER; return RESTRICT_RANGE; }
+"restrictRange" { BUFFER; return RESTRICT_RANGE; }
+"assertUnsatisfiable" { BUFFER; return ASSERT_UNSAT; }
+"assert_unsatisfiable" { BUFFER; return ASSERT_UNSAT; }
+
+"/" { BUFFER; return RESTRICT_RANGE; }
+"&" { BUFFER; return AND; }
+"|" { BUFFER; return OR; }
+"&&" { BUFFER; return AND; }
+"||" { BUFFER; return OR; }
+"and" { BUFFER; return AND; }
+"or" { BUFFER; return OR; }
+<LATEX>"\\land" { BUFFER; return AND; }
+<LATEX>"\\lor" { BUFFER; return OR; }
+"!" { BUFFER; return NOT; }
+"not" { BUFFER; return NOT; }
+<LATEX>"\\neg" { BUFFER; return NOT; }
+":=" { BUFFER; return IS_ASSIGNED; }
+"->" { BUFFER; return GOES_TO; }
+"in" { BUFFER; return IN; }
+<LATEX>"\\rightarrow" { BUFFER; return GOES_TO; }
+"<=" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; }
+<LATEX>"\\leq" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; }
+<LATEX>"\\le" { BUFFER; yylval.REL_OPERATOR = leq; return REL_OP; }
+">=" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; }
+<LATEX>"\\geq" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; }
+<LATEX>"\\ge" { BUFFER; yylval.REL_OPERATOR = geq; return REL_OP; }
+"!=" { BUFFER; yylval.REL_OPERATOR = neq; return REL_OP; }
+<LATEX>"\\neq" { BUFFER; yylval.REL_OPERATOR = neq; return REL_OP; }
+"<" { BUFFER; yylval.REL_OPERATOR = lt; return REL_OP; }
+">" { BUFFER; yylval.REL_OPERATOR = gt; return REL_OP; }
+"=" { BUFFER; yylval.REL_OPERATOR = eq; return REL_OP; }
+"==" { BUFFER; yylval.REL_OPERATOR = eq; return REL_OP; }
+
+[A-Za-z_][A-Za-z0-9_]*[\']* {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ return VAR;
+}
+[A-Za-z][A-Za-z0-9_]*"(In)" {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
+ yylval.VAR_NAME[yyleng-2] = 'n';
+ return VAR;
+}
+[A-Za-z][A-Za-z0-9_]*"(Set)" {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
+ yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
+ yylval.VAR_NAME[yyleng-2] = ')';
+ yylval.VAR_NAME[yyleng-1] = '\0';
+ return VAR;
+}
+[A-Za-z][A-Za-z0-9_]*"(Out)" {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
+ yylval.VAR_NAME[yyleng-3] = 'u';
+ yylval.VAR_NAME[yyleng-2] = 't';
+ return VAR;
+}
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]* {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ return VAR;
+ }
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(In)" {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-3] = 'i'; // lowercase
+ yylval.VAR_NAME[yyleng-2] = 'n';
+ return VAR;
+ }
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(Set)" {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'i'; // Change to "in"
+ yylval.VAR_NAME[yyleng-3] = 'n'; // Be afraid
+ yylval.VAR_NAME[yyleng-2] = ')';
+ yylval.VAR_NAME[yyleng-1] = '\0';
+ return VAR;
+ }
+<LATEX>"\\"[A-Za-z][A-Za-z0-9_]*"(Out)" {
+ BUFFER;
+ yylval.VAR_NAME = new char[yyleng+1];
+ strcpy(yylval.VAR_NAME,yytext);
+ yylval.VAR_NAME[yyleng-4] = 'o'; // lowercase
+ yylval.VAR_NAME[yyleng-3] = 'u';
+ yylval.VAR_NAME[yyleng-2] = 't';
+ return VAR;
+ }
+
+[0-9]+ { BUFFER;
+ if (need_coef) {
+ sscanf(yytext, coef_fmt, &yylval.COEF_VALUE);
+ return COEF;
+ }
+ else {
+ yylval.INT_VALUE = atoi(yytext);
+ return INT;
+ }
+}
+
+\"[^\"]*\" { BUFFER;
+ yytext[yyleng-1]='\0';
+ yylval.STRING_VALUE = new std::string(yytext+1);
+ return STRING;
+}
+
+
+<<EOF>> {
+ mylexer.yypop_buffer_state();
+ if (!YY_CURRENT_BUFFER) {
+ flushScanBuffer();
+ return YY_NULL;
+ }
+}
+
+. { BUFFER; return yytext[0]; }
+
+
+%%
+
+void flushScanBuffer() {
+ if (scanBuf.size() == 0)
+ return;
+ if (!is_interactive) {
+ size_t prev_pos = 0;
+ if (scanBuf[0] == '\n')
+ prev_pos = 1;
+ for (size_t pos = prev_pos; pos <= scanBuf.size(); pos++) {
+ if (pos == scanBuf.size() || scanBuf[pos] == '\n') {
+ std::cout << PROMPT_STRING << " " << scanBuf.substr(prev_pos, pos-prev_pos) << std::endl;
+ prev_pos = pos+1;
+ }
+ }
+ }
+
+ scanBuf.clear();
+}
diff --git a/omega/omega_calc/src/parser.y b/omega/omega_calc/src/parser.y
new file mode 100644
index 0000000..7369b94
--- /dev/null
+++ b/omega/omega_calc/src/parser.y
@@ -0,0 +1,1925 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 University of Maryland.
+ Copyright (C) 2008 University of Southern California.
+ Copyright (C) 2009-2010 University of Utah.
+ All Rights Reserved.
+
+ Purpose:
+ omega calculator yacc parser.
+
+ Notes:
+
+ History:
+*****************************************************************************/
+
+%{
+
+#include <basic/Dynamic_Array.h>
+#include <basic/Iterator.h>
+#include <code_gen/code_gen.h>
+#include <omega_calc/AST.h>
+#include <omega/hull.h>
+#include <omega/closure.h>
+#include <omega/reach.h>
+#include <string>
+#include <iostream>
+
+#ifdef WIN32
+#include <io.h>
+#define isatty _isatty
+#define alloca _alloca
+#endif
+#ifndef WIN32
+#include <sys/time.h>
+#include <sys/resource.h>
+#endif
+#if !defined(OMIT_GETRUSAGE)
+#include <sys/types.h>
+#include <sys/time.h>
+#include <sys/resource.h>
+#endif
+
+#if !defined(OMIT_GETRUSAGE)
+#ifdef __sparc__
+extern "C" int getrusage (int, struct rusage*);
+#endif
+
+using namespace omega;
+
+struct rusage start_time;
+bool anyTimingDone = false;
+
+void start_clock( void ) {
+ getrusage(RUSAGE_SELF, &start_time);
+}
+
+int clock_diff( void ) {
+ struct rusage current_time;
+ getrusage(RUSAGE_SELF, ¤t_time);
+ return (current_time.ru_utime.tv_sec -start_time.ru_utime.tv_sec)*1000000 + (current_time.ru_utime.tv_usec-start_time.ru_utime.tv_usec);
+}
+#endif
+
+int omega_calc_debug = 0;
+
+bool is_interactive;
+const char *PROMPT_STRING = ">>>";
+extern std::string err_msg;
+extern FILE *yyin;
+bool need_coef;
+
+Map<Const_String,Relation*> relationMap ((Relation *)0);
+namespace {
+ int redundant_conj_level = 2; // default maximum 2
+ int redundant_constr_level = 4; // default maximum 4
+}
+
+int argCount = 0;
+int tuplePos = 0;
+Argument_Tuple currentTuple = Input_Tuple;
+
+Relation LexForward(int n);
+reachable_information *reachable_info;
+
+int yylex();
+void yyerror(const std::string &s);
+void flushScanBuffer();
+
+%}
+
+%union {
+ int INT_VALUE;
+ coef_t COEF_VALUE;
+ Rel_Op REL_OPERATOR;
+ char *VAR_NAME;
+ VarList *VAR_LIST;
+ Exp *EXP;
+ ExpList *EXP_LIST;
+ AST *ASTP;
+ Argument_Tuple ARGUMENT_TUPLE;
+ AST_constraints *ASTCP;
+ Declaration_Site * DECLARATION_SITE;
+ Relation * RELATION;
+ tupleDescriptor * TUPLE_DESCRIPTOR;
+ RelTuplePair * REL_TUPLE_PAIR;
+ Dynamic_Array2<Relation> * RELATION_ARRAY_2D;
+ Dynamic_Array1<Relation> * RELATION_ARRAY_1D;
+ Tuple<std::string> *STRING_TUPLE;
+ std::string *STRING_VALUE;
+}
+
+%token <VAR_NAME> VAR
+%token <INT_VALUE> INT
+%token <COEF_VALUE> COEF
+%token <STRING_VALUE> STRING
+%token OPEN_BRACE CLOSE_BRACE
+%token SYMBOLIC
+%token OR AND NOT
+%token ST APPROX
+%token IS_ASSIGNED
+%token FORALL EXISTS
+%token DOMAIN RANGE
+%token DIFFERENCE DIFFERENCE_TO_RELATION
+%token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
+%token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION LINEAR_COMBINATION AFFINE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL QUICK_HULL PAIRWISE_CHECK CONVEX_CHECK CONVEX_REPRESENTATION RECT_HULL DECOUPLED_CONVEX_HULL
+%token MAXIMIZE_RANGE MINIMIZE_RANGE
+%token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
+%token LEQ GEQ NEQ
+%token GOES_TO
+%token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
+%token UNION INTERSECTION
+%token VERTICAL_BAR SUCH_THAT
+%token SUBSET CODEGEN DECOUPLED_FARKAS FARKAS
+%token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
+%token <REL_OPERATOR> REL_OP
+%token RESTRICT_DOMAIN RESTRICT_RANGE
+%token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
+%token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
+%token ASSERT_UNSAT
+%token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
+
+%type <INT_VALUE> effort
+%type <EXP> exp simpleExp
+%type <EXP_LIST> expList
+%type <VAR_LIST> varList
+%type <ARGUMENT_TUPLE> argumentList
+%type <ASTP> formula optionalFormula
+%type <ASTCP> constraintChain
+%type <TUPLE_DESCRIPTOR> tupleDeclaration
+%type <DECLARATION_SITE> varDecl varDeclOptBrackets
+%type <RELATION> relation builtRelation context
+%type <RELATION> reachable_of
+%type <REL_TUPLE_PAIR> relPairList
+%type <RELATION_ARRAY_1D> reachable
+
+%destructor {delete []$$;} VAR
+%destructor {delete $$;} STRING
+%destructor {delete $$;} relation builtRelation tupleDeclaration formula optionalFormula context reachable_of constraintChain varDecl varDeclOptBrackets relPairList reachable
+%destructor {delete $$;} varList exp simpleExp
+%destructor {
+ foreach(e, Exp *, *$$, delete e);
+ delete $$;
+ } expList;
+
+%nonassoc ASSERT_UNSAT
+%left UNION p1 '+' '-'
+%nonassoc SUPERSETOF SUBSETOF
+%left p2 RESTRICT_DOMAIN RESTRICT_RANGE
+%left INTERSECTION p3 '*' '@'
+%left p4
+%left OR p5
+%left AND p6
+%left COMPOSE JOIN CARRIED_BY
+%right NOT APPROX DOMAIN RANGE HULL PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS DIFFERENCE DIFFERENCE_TO_RELATION INVERSE COMPLEMENT FARKAS SAMPLE SYM_SAMPLE MAKE_UPPER_BOUND MAKE_LOWER_BOUND p7
+%left p8
+%nonassoc GIVEN
+%left p9
+%left '(' p10
+
+%%
+
+inputSequence : /*empty*/
+ | inputSequence { assert( current_Declaration_Site == globalDecls);}
+ inputItem
+;
+
+inputItem : ';' /*empty*/
+ | error ';' {
+ flushScanBuffer();
+ std::cout << err_msg;
+ err_msg.clear();
+ current_Declaration_Site = globalDecls;
+ need_coef = false;
+ std::cout << "...skipping to statement end..." << std::endl;
+ delete relationDecl;
+ relationDecl = NULL;
+ }
+ | SYMBOLIC globVarList ';' {flushScanBuffer();}
+ | VAR IS_ASSIGNED relation ';' {
+ flushScanBuffer();
+ try {
+ $3->simplify(redundant_conj_level, redundant_constr_level);
+ Relation *r = relationMap((Const_String)$1);
+ if (r) delete r;
+ relationMap[(Const_String)$1] = $3;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+ delete []$1;
+ }
+ | relation ';' {
+ flushScanBuffer();
+ $1->simplify(redundant_conj_level, redundant_constr_level);
+ $1->print_with_subs(stdout);
+ delete $1;
+ }
+ | TIME relation ';' {
+#if defined(OMIT_GETRUSAGE)
+ printf("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
+#else
+ flushScanBuffer();
+ printf("\n");
+ int t;
+ Relation R;
+ bool SKIP_FULL_CHECK = getenv("OC_TIMING_SKIP_FULL_CHECK");
+ ($2)->and_with_GEQ();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ }
+ int copyTime = clock_diff();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ R.simplify(); /* default simplification effort */
+ }
+ int simplifyTime = clock_diff() -copyTime;
+ Relation R2;
+ if (!SKIP_FULL_CHECK) {
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R2 = *$2;
+ R2.finalize();
+ R2.simplify(2,4); /* maximal simplification effort */
+ }
+ }
+ int excessiveTime = clock_diff() - copyTime;
+ printf("Times (in microseconds): \n");
+ printf("%5d us to copy original set of constraints\n",copyTime/100);
+ printf("%5d us to do the default amount of simplification, obtaining: \n\t", simplifyTime/100);
+ R.print_with_subs(stdout);
+ printf("\n");
+ if (!SKIP_FULL_CHECK) {
+ printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", excessiveTime/100);
+ R2.print_with_subs(stdout);
+ printf("\n");
+ }
+ if (!anyTimingDone) {
+ bool warn = false;
+#ifndef SPEED
+ warn =true;
+#endif
+#ifndef NDEBUG
+ warn = true;
+#endif
+ if (warn) {
+ printf("WARNING: The Omega calculator was compiled with options that force\n");
+ printf("it to perform additional consistency and error checks\n");
+ printf("that may slow it down substantially\n");
+ printf("\n");
+ }
+ printf("NOTE: These times relect the time of the current _implementation_\n");
+ printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
+ printf("report on the performance on the Omega test, we respectfully but strongly \n");
+ printf("request that send your test cases to us to allow us to determine if the \n");
+ printf("times are appropriate, and if the way you are using the Omega library to \n");
+ printf("solve your problem is the most effective way.\n");
+ printf("\n");
+
+ printf("Also, please be aware that over the past two years, we have focused our \n");
+ printf("efforts on the expressive power of the Omega library, sometimes at the\n");
+ printf("expensive of raw speed. Our original implementation of the Omega test\n");
+ printf("was substantially faster on the limited domain it handled.\n");
+ printf("\n");
+ printf(" Thanks, \n");
+ printf(" the Omega Team \n");
+ }
+ anyTimingDone = true;
+ delete $2;
+#endif
+ }
+ | TIMECLOSURE relation ';' {
+#if defined(OMIT_GETRUSAGE)
+ printf("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
+#else
+ flushScanBuffer();
+ try {
+ int t;
+ Relation R;
+ ($2)->and_with_GEQ();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ }
+ int copyTime = clock_diff();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ R.simplify();
+ }
+ int simplifyTime = clock_diff() -copyTime;
+ Relation Rclosed;
+ start_clock();
+ for (t=1;t<=100;t++) {
+ Rclosed = *$2;
+ Rclosed.finalize();
+ Rclosed = TransitiveClosure(Rclosed, 1,Relation::Null());
+ }
+ int closureTime = clock_diff() - copyTime;
+ Relation R2;
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R2 = *$2;
+ R2.finalize();
+ R2.simplify(2,4);
+ }
+ int excessiveTime = clock_diff() - copyTime;
+ printf("Times (in microseconds): \n");
+ printf("%5d us to copy original set of constraints\n",copyTime/100);
+ printf("%5d us to do the default amount of simplification, obtaining: \n\t", simplifyTime/100);
+ R.print_with_subs(stdout);
+ printf("\n");
+ printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", excessiveTime/100);
+ R2.print_with_subs(stdout);
+ printf("%5d us to do the transitive closure, obtaining: \n\t", closureTime/100);
+ Rclosed.print_with_subs(stdout);
+ printf("\n");
+ if (!anyTimingDone) {
+ bool warn = false;
+#ifndef SPEED
+ warn =true;
+#endif
+#ifndef NDEBUG
+ warn = true;
+#endif
+ if (warn) {
+ printf("WARNING: The Omega calculator was compiled with options that force\n");
+ printf("it to perform additional consistency and error checks\n");
+ printf("that may slow it down substantially\n");
+ printf("\n");
+ }
+ printf("NOTE: These times relect the time of the current _implementation_\n");
+ printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
+ printf("report on the performance on the Omega test, we respectfully but strongly \n");
+ printf("request that send your test cases to us to allow us to determine if the \n");
+ printf("times are appropriate, and if the way you are using the Omega library to \n");
+ printf("solve your problem is the most effective way.\n");
+ printf("\n");
+
+ printf("Also, please be aware that over the past two years, we have focused our \n");
+ printf("efforts on the expressive power of the Omega library, sometimes at the\n");
+ printf("expensive of raw speed. Our original implementation of the Omega test\n");
+ printf("was substantially faster on the limited domain it handled.\n");
+ printf("\n");
+ printf(" Thanks, \n");
+ printf(" the Omega Team \n");
+ }
+ anyTimingDone = true;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+ delete $2;
+#endif
+ }
+ | relation SUBSET relation ';' {
+ flushScanBuffer();
+ try {
+ if (Must_Be_Subset(copy(*$1), copy(*$3)))
+ std::cout << "True" << std::endl;
+ else if (Might_Be_Subset(copy(*$1), copy(*$3)))
+ std::cout << "Possible" << std::endl;
+ else
+ std::cout << "False" << std::endl;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+ delete $1;
+ delete $3;
+ }
+ | CODEGEN effort relPairList context';' {
+ flushScanBuffer();
+ try {
+ std::string s = MMGenerateCode($3->mappings, $3->ispaces,*$4,$2);
+ std::cout << s << std::endl;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+ delete $4;
+ delete $3;
+ }
+ | reachable ';' {
+ flushScanBuffer();
+ Dynamic_Array1<Relation> &final = *$1;
+ bool any_sat = false;
+ int i,n_nodes = reachable_info->node_names.size();
+ for(i = 1; i <= n_nodes; i++)
+ if(final[i].is_upper_bound_satisfiable()) {
+ any_sat = true;
+ std::cout << "Node %s: " << reachable_info->node_names[i];
+ final[i].print_with_subs(stdout);
+ }
+ if(!any_sat)
+ std::cout << "No nodes reachable.\n";
+ delete $1;
+ delete reachable_info;
+ }
+;
+
+
+effort : {$$ = 1;}
+ | INT {$$ = $1;}
+ | '-' INT {$$ = -$2;}
+;
+
+context : {$$ = new Relation(); *$$ = Relation::Null();}
+ | GIVEN relation {$$ = $2; }
+;
+
+relPairList : relPairList ',' relation ':' relation {
+ try {
+ $1->mappings.append(*$3);
+ $1->mappings[$1->mappings.size()].compress();
+ $1->ispaces.append(*$5);
+ $1->ispaces[$1->ispaces.size()].compress();
+ }
+ catch (const std::exception &e) {
+ delete $1;
+ delete $3;
+ delete $5;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $3;
+ delete $5;
+ $$ = $1;
+ }
+ | relPairList ',' relation {
+ try {
+ $1->mappings.append(Identity($3->n_set()));
+ $1->mappings[$1->mappings.size()].compress();
+ $1->ispaces.append(*$3);
+ $1->ispaces[$1->ispaces.size()].compress();
+ }
+ catch (const std::exception &e) {
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $3;
+ $$ = $1;
+ }
+ | relation ':' relation {
+ RelTuplePair *rtp = new RelTuplePair;
+ try {
+ rtp->mappings.append(*$1);
+ rtp->mappings[rtp->mappings.size()].compress();
+ rtp->ispaces.append(*$3);
+ rtp->ispaces[rtp->ispaces.size()].compress();
+ }
+ catch (const std::exception &e) {
+ delete rtp;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ $$ = rtp;
+ }
+ | relation {
+ RelTuplePair *rtp = new RelTuplePair;
+ try {
+ rtp->mappings.append(Identity($1->n_set()));
+ rtp->mappings[rtp->mappings.size()].compress();
+ rtp->ispaces.append(*$1);
+ rtp->ispaces[rtp->ispaces.size()].compress();
+ }
+ catch (const std::exception &e) {
+ delete rtp;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ $$ = rtp;
+ }
+;
+
+relation : OPEN_BRACE {need_coef = true; relationDecl = new Declaration_Site();}
+ builtRelation CLOSE_BRACE {
+ need_coef = false;
+ $$ = $3;
+ if (omega_calc_debug) {
+ fprintf(DebugFile,"Built relation:\n");
+ $$->prefix_print(DebugFile);
+ }
+ current_Declaration_Site = globalDecls;
+ delete relationDecl;
+ relationDecl = NULL;
+ }
+ | VAR {
+ Const_String s = $1;
+ Relation *r = relationMap(s);
+ if (r == NULL) {
+ yyerror(std::string("relation ") + to_string($1) + std::string(" not declared"));
+ delete []$1;
+ YYERROR;
+ }
+ $$ = new Relation(*r);
+ delete []$1;
+ }
+ | '(' relation ')' {$$ = $2;}
+ | relation '+' %prec p9 {
+ $$ = new Relation();
+ try {
+ *$$ = TransitiveClosure(*$1, 1, Relation::Null());
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation '*' %prec p9 {
+ $$ = new Relation();
+ try {
+ int vars = $1->n_inp();
+ *$$ = Union(Identity(vars), TransitiveClosure(*$1, 1, Relation::Null()));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation '+' WITHIN relation %prec p9 {
+ $$ = new Relation();
+ try {
+ *$$= TransitiveClosure(*$1, 1, *$4);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $4;
+ }
+ | relation '^' '@' %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ApproxClosure(*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation '^' '+' %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = calculateTransitiveClosure(*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | MINIMIZE_RANGE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(r,LexForward($2->n_out()));
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAXIMIZE_RANGE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(r,Inverse(LexForward($2->n_out())));
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MINIMIZE_DOMAIN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(LexForward($2->n_inp()),r);
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAXIMIZE_DOMAIN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(Inverse(LexForward($2->n_inp())),r);
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAXIMIZE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation c(*$2);
+ Relation r(*$2);
+ *$$ = Cross_Product(Relation(*$2),c);
+ *$$ = Difference(r,Domain(Intersection(*$$,LexForward($$->n_inp()))));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MINIMIZE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation c(*$2);
+ Relation r(*$2);
+ *$$ = Cross_Product(Relation(*$2),c);
+ *$$ = Difference(r,Range(Intersection(*$$,LexForward($$->n_inp()))));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | FARKAS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2, Basic_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DECOUPLED_FARKAS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2, Decoupled_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | relation '@' %prec p9 {
+ $$ = new Relation();
+ try {
+ *$$ = ConicClosure(*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | PROJECT_AWAY_SYMBOLS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Project_Sym(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | PROJECT_ON_SYMBOLS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Project_On_Sym(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DIFFERENCE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Deltas(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DIFFERENCE_TO_RELATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = DeltasToRelation(*$2,$2->n_set(),$2->n_set());
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DOMAIN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Domain(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | VENN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = VennDiagramForm(*$2,Relation::True(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | VENN relation GIVEN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = VennDiagramForm(*$2,*$4);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ delete $4;
+ }
+ | CONVEX_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ConvexHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DECOUPLED_CONVEX_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = DecoupledConvexHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | POSITIVE_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Positive_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | LINEAR_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Linear_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | AFFINE_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Affine_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONVEX_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Convex_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | PAIRWISE_CHECK relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = CheckForConvexRepresentation(CheckForConvexPairs(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONVEX_CHECK relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = CheckForConvexRepresentation(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONVEX_REPRESENTATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ConvexRepresentation(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | AFFINE_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = AffineHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONIC_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ConicHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | LINEAR_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = LinearHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | QUICK_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = QuickHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | RECT_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = RectHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Hull(*$2,false,1,Relation::Null());
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | HULL relation GIVEN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Hull(*$2,false,1,*$4);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ delete $4;
+ }
+ | APPROX relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Approximate(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | RANGE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Range(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | INVERSE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Inverse(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | COMPLEMENT relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Complement(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | GIST relation GIVEN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Gist(*$2,*$4,1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ delete $4;
+ }
+ | relation '(' relation ')' {
+ $$ = new Relation();
+ try {
+ *$$ = Composition(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation COMPOSE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Composition(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation CARRIED_BY INT {
+ $$ = new Relation();
+ try {
+ *$$ = After(*$1,$3,$3);
+ (*$$).prefix_print(stdout);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation JOIN relation {
+ $$ = new Relation();
+ try {
+ *$$ = Composition(*$3,*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation RESTRICT_RANGE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Restrict_Range(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation RESTRICT_DOMAIN relation {
+ $$ = new Relation();
+ try {
+ *$$ = Restrict_Domain(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation INTERSECTION relation {
+ $$ = new Relation();
+ try {
+ *$$ = Intersection(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation '-' relation %prec INTERSECTION {
+ $$ = new Relation();
+ try {
+ *$$ = Difference(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation UNION relation {
+ $$ = new Relation();
+ try {
+ *$$ = Union(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation '*' relation {
+ $$ = new Relation();
+ try {
+ *$$ = Cross_Product(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | SUPERSETOF relation {
+ $$ = new Relation();
+ try {
+ *$$ = Union(*$2, Relation::Unknown(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SUBSETOF relation {
+ $$ = new Relation();
+ try {
+ *$$ = Intersection(*$2, Relation::Unknown(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAKE_UPPER_BOUND relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Upper_Bound(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAKE_LOWER_BOUND relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Lower_Bound(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SAMPLE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Sample_Solution(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SYM_SAMPLE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Symbolic_Solution(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | reachable_of { $$ = $1; }
+ | ASSERT_UNSAT relation {
+ if (($2)->is_satisfiable()) {
+ fprintf(stderr,"assert_unsatisfiable failed on ");
+ ($2)->print_with_subs(stderr);
+ exit(1);
+ }
+ $$=$2;
+ }
+;
+
+builtRelation : tupleDeclaration GOES_TO {currentTuple = Output_Tuple;}
+ tupleDeclaration {currentTuple = Input_Tuple;} optionalFormula {
+ Relation * r = new Relation($1->size,$4->size);
+ resetGlobals();
+ F_And *f = r->add_and();
+ for(int i=1;i<=$1->size;i++) {
+ $1->vars[i]->vid = r->input_var(i);
+ if (!$1->vars[i]->anonymous)
+ r->name_input_var(i,$1->vars[i]->stripped_name);
+ }
+ for(int i=1;i<=$4->size;i++) {
+ $4->vars[i]->vid = r->output_var(i);
+ if (!$4->vars[i]->anonymous)
+ r->name_output_var(i,$4->vars[i]->stripped_name);
+ }
+ r->setup_names();
+ foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0));
+ foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0));
+ foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c));
+ foreach(e,Exp*,$4->eq_constraints, install_eq(f,e,0));
+ foreach(e,Exp*,$4->geq_constraints, install_geq(f,e,0));
+ foreach(c,strideConstraint*,$4->stride_constraints, install_stride(f,c));
+ if ($6) $6->install(f);
+ delete $1;
+ delete $4;
+ delete $6;
+ $$ = r;
+ }
+ | tupleDeclaration optionalFormula {
+ Relation * r = new Relation($1->size);
+ resetGlobals();
+ F_And *f = r->add_and();
+ for(int i=1;i<=$1->size;i++) {
+ $1->vars[i]->vid = r->set_var(i);
+ if (!$1->vars[i]->anonymous)
+ r->name_set_var(i,$1->vars[i]->stripped_name);
+ }
+ r->setup_names();
+ foreach(e,Exp*,$1->eq_constraints, install_eq(f,e,0));
+ foreach(e,Exp*,$1->geq_constraints, install_geq(f,e,0));
+ foreach(c,strideConstraint*,$1->stride_constraints, install_stride(f,c));
+ if ($2) $2->install(f);
+ delete $1;
+ delete $2;
+ $$ = r;
+ }
+ | formula {
+ Relation * r = new Relation(0,0);
+ F_And *f = r->add_and();
+ $1->install(f);
+ delete $1;
+ $$ = r;
+ }
+;
+
+optionalFormula : formula_sep formula {$$ = $2;}
+ | {$$ = 0;}
+;
+
+formula_sep : ':'
+ | VERTICAL_BAR
+ | SUCH_THAT
+;
+
+tupleDeclaration : {currentTupleDescriptor = new tupleDescriptor; tuplePos = 1;}
+ '[' optionalTupleVarList ']'
+ {$$ = currentTupleDescriptor; tuplePos = 0;}
+;
+
+optionalTupleVarList : /* empty */
+ | tupleVar
+ | optionalTupleVarList ',' tupleVar
+;
+
+tupleVar : VAR %prec p10 {
+ Declaration_Site *ds = defined($1);
+ if (!ds)
+ currentTupleDescriptor->extend($1,currentTuple,tuplePos);
+ else {
+ Variable_Ref *v = lookupScalar($1);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$1;
+ YYERROR;
+ }
+ if (ds != globalDecls)
+ currentTupleDescriptor->extend($1, new Exp(v));
+ else
+ currentTupleDescriptor->extend(new Exp(v));
+ }
+ tuplePos++;
+ delete []$1;
+ }
+ | '*' {currentTupleDescriptor->extend(); tuplePos++;}
+ | exp %prec p1 {
+ currentTupleDescriptor->extend($1);
+ tuplePos++;
+ }
+ | exp ':' exp %prec p1 {
+ currentTupleDescriptor->extend($1,$3);
+ tuplePos++;
+ }
+ | exp ':' exp ':' COEF %prec p1 {
+ currentTupleDescriptor->extend($1,$3,$5);
+ tuplePos++;
+ }
+;
+
+varList : varList ',' VAR {$$ = $1; $$->insert($3); $3 = NULL;}
+ | VAR {$$ = new VarList; $$->insert($1); $1 = NULL;}
+;
+
+varDecl : varList {
+ $$ = current_Declaration_Site = new Declaration_Site($1);
+ foreach(s,char *, *$1, delete []s);
+ delete $1;
+ }
+;
+
+varDeclOptBrackets : varDecl {$$ = $1;}
+ |'[' varDecl ']' {$$ = $2;}
+;
+
+globVarList : globVarList ',' globVar
+ | globVar
+;
+
+globVar : VAR '(' INT ')' {globalDecls->extend_both_tuples($1, $3); delete []$1;}
+ | VAR {
+ globalDecls->extend($1);
+ delete []$1;
+ }
+;
+
+formula : formula AND formula {$$ = new AST_And($1,$3);}
+ | formula OR formula {$$ = new AST_Or($1,$3);}
+ | constraintChain {$$ = $1;}
+ | '(' formula ')' {$$ = $2;}
+ | NOT formula {$$ = new AST_Not($2);}
+ | start_exists varDeclOptBrackets exists_sep formula end_quant {$$ = new AST_exists($2,$4);}
+ | start_forall varDeclOptBrackets forall_sep formula end_quant {$$ = new AST_forall($2,$4);}
+;
+
+start_exists : '(' EXISTS
+ | EXISTS '('
+;
+
+exists_sep : ':'
+ | VERTICAL_BAR
+ | SUCH_THAT
+;
+
+start_forall : '(' FORALL
+ | FORALL '('
+;
+
+forall_sep : ':'
+;
+
+end_quant : ')' {popScope();}
+;
+
+expList : exp ',' expList {$$ = $3; $$->insert($1);}
+ | exp {$$ = new ExpList; $$->insert($1);}
+;
+
+constraintChain : expList REL_OP expList {$$ = new AST_constraints($1,$2,$3);}
+ | expList REL_OP constraintChain {$$ = new AST_constraints($1,$2,$3);}
+;
+
+simpleExp : VAR %prec p9 {
+ Variable_Ref *v = lookupScalar($1);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$1;
+ YYERROR;
+ }
+ $$ = new Exp(v);
+ delete []$1;
+ }
+ | VAR '(' {argCount = 1;} argumentList ')' %prec p9 {
+ Variable_Ref *v;
+ if ($4 == Input_Tuple)
+ v = functionOfInput[$1];
+ else
+ v = functionOfOutput[$1];
+ if (v == NULL) {
+ yyerror(std::string("Function ") + to_string($1) + std::string(" not declared"));
+ delete []$1;
+ YYERROR;
+ }
+ $$ = new Exp(v);
+ delete []$1;
+ }
+ | '(' exp ')' { $$ = $2; }
+;
+
+argumentList : argumentList ',' VAR {
+ Variable_Ref *v = lookupScalar($3);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$3;
+ YYERROR;
+ }
+ if (v->pos != argCount || v->of != $1 || (v->of != Input_Tuple && v->of != Output_Tuple)) {
+ yyerror("arguments to function must be prefix of input or output tuple");
+ delete []$3;
+ YYERROR;
+ }
+ $$ = v->of;
+ argCount++;
+ delete []$3;
+ }
+ | VAR {
+ Variable_Ref *v = lookupScalar($1);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$1;
+ YYERROR;
+ }
+ if (v->pos != argCount || (v->of != Input_Tuple && v->of != Output_Tuple)) {
+ yyerror("arguments to function must be prefix of input or output tuple");
+ delete []$1;
+ YYERROR;
+ }
+ $$ = v->of;
+ argCount++;
+ delete []$1;
+ }
+;
+
+exp : COEF {$$ = new Exp($1);}
+ | COEF simpleExp %prec '*' {$$ = multiply($1,$2);}
+ | simpleExp {$$ = $1; }
+ | '-' exp %prec '*' {$$ = negate($2);}
+ | exp '+' exp {$$ = add($1,$3);}
+ | exp '-' exp {$$ = subtract($1,$3);}
+ | exp '*' exp {$$ = multiply($1,$3);}
+;
+
+
+reachable : REACHABLE_FROM nodeNameList nodeSpecificationList {
+ Dynamic_Array1<Relation> *final = Reachable_Nodes(reachable_info);
+ $$ = final;
+ }
+;
+
+reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList {
+ Dynamic_Array1<Relation> *final = Reachable_Nodes(reachable_info);
+ int index = reachable_info->node_names.index(std::string($2));
+ if (index == 0) {
+ yyerror(std::string("no such node ") + to_string($2));
+ delete []$2;
+ delete final;
+ delete reachable_info;
+ YYERROR;
+ }
+ $$ = new Relation;
+ *$$ = (*final)[index];
+ delete final;
+ delete reachable_info;
+ delete []$2;
+ }
+;
+
+nodeNameList : '(' realNodeNameList ')' {
+ int sz = reachable_info->node_names.size();
+ reachable_info->node_arity.reallocate(sz);
+ reachable_info->transitions.resize(sz+1,sz+1);
+ reachable_info->start_nodes.resize(sz+1);
+ }
+;
+
+realNodeNameList : realNodeNameList ',' VAR {
+ reachable_info->node_names.append(std::string($3));
+ delete []$3;
+ }
+ | VAR {
+ reachable_info = new reachable_information;
+ reachable_info->node_names.append(std::string($1));
+ delete []$1;
+ }
+;
+
+
+nodeSpecificationList : OPEN_BRACE realNodeSpecificationList CLOSE_BRACE {
+ int i,j;
+ int n_nodes = reachable_info->node_names.size();
+ Tuple<int> &arity = reachable_info->node_arity;
+ Dynamic_Array2<Relation> &transitions = reachable_info->transitions;
+
+ /* fixup unspecified transitions to be false */
+ /* find arity */
+ for(i = 1; i <= n_nodes; i++) arity[i] = -1;
+ for(i = 1; i <= n_nodes; i++)
+ for(j = 1; j <= n_nodes; j++)
+ if(! transitions[i][j].is_null()) {
+ int in_arity = transitions[i][j].n_inp();
+ int out_arity = transitions[i][j].n_out();
+ if(arity[i] < 0) arity[i] = in_arity;
+ if(arity[j] < 0) arity[j] = out_arity;
+ if(in_arity != arity[i] || out_arity != arity[j]) {
+ yyerror(std::string("arity mismatch in node transition: ") + to_string(reachable_info->node_names[i]) + std::string(" -> ") + to_string(reachable_info->node_names[j]));
+ delete reachable_info;
+ YYERROR;
+ }
+ }
+ for(i = 1; i <= n_nodes; i++)
+ if(arity[i] < 0) arity[i] = 0;
+ /* Fill in false relations */
+ for(i = 1; i <= n_nodes; i++)
+ for(j = 1; j <= n_nodes; j++)
+ if(transitions[i][j].is_null())
+ transitions[i][j] = Relation::False(arity[i],arity[j]);
+
+ /* fixup unused start node positions */
+ Dynamic_Array1<Relation> &nodes = reachable_info->start_nodes;
+ for(i = 1; i <= n_nodes; i++)
+ if(nodes[i].is_null())
+ nodes[i] = Relation::False(arity[i]);
+ else
+ if(nodes[i].n_set() != arity[i]){
+ yyerror(std::string("arity mismatch in start node ") + to_string(reachable_info->node_names[i]));
+ delete reachable_info;
+ YYERROR;
+ }
+ }
+;
+
+realNodeSpecificationList : realNodeSpecificationList ',' VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int index = reachable_info->node_names.index($3);
+ if (!(index > 0 && index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($3));
+ delete $5;
+ delete []$3;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->start_nodes[index] = *$5;
+ delete $5;
+ delete []$3;
+ }
+ | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int from_index = reachable_info->node_names.index($3);
+ if (!(from_index > 0 && from_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($3));
+ delete $7;
+ delete []$3;
+ delete []$5;
+ delete reachable_info;
+ YYERROR;
+ }
+ int to_index = reachable_info->node_names.index($5);
+ if (!(to_index > 0 && to_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($5));
+ delete $7;
+ delete []$3;
+ delete []$5;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->transitions[from_index][to_index] = *$7;
+ delete $7;
+ delete []$3;
+ delete []$5;
+ }
+ | VAR GOES_TO VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int from_index = reachable_info->node_names.index($1);
+ if (!(from_index > 0 && from_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($1));
+ delete $5;
+ delete []$1;
+ delete []$3;
+ delete reachable_info;
+ YYERROR;
+ }
+ int to_index = reachable_info->node_names.index($3);
+ if (!(to_index > 0 && to_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($3));
+ delete $5;
+ delete []$1;
+ delete []$3;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->transitions[from_index][to_index] = *$5;
+ delete $5;
+ delete []$1;
+ delete []$3;
+ }
+ | VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int index = reachable_info->node_names.index($1);
+ if (!(index > 0 && index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($1));
+ delete $3;
+ delete []$1;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->start_nodes[index] = *$3;
+ delete $3;
+ delete []$1;
+ }
+;
+
+%%
+
+
+void printUsage(FILE *outf, char **argv) {
+ fprintf(outf, "usage: %s {-R} {-D[facility][level]...} infile\n -R means skip redundant conjunct elimination\n -D sets debugging level as follows:\n a = all debugging flags\n g = code generation\n l = calculator\n c = omega core\n p = presburger functions\n r = relational operators\n t = transitive closure\n", argv[0]);
+}
+
+
+bool process_calc_debugging_flags(char *arg,int &j) {
+ char debug_type;
+ while((debug_type=arg[j]) != 0) {
+ j++;
+ int level;
+ if(isdigit(arg[j]))
+ level = (arg[j++]) - '0';
+ else
+ if(arg[j] == 0 || isalpha(arg[j]))
+ level = 1;
+ else
+ return false;
+ if (level < 0 || level > 4) {
+ fprintf(stderr,"Debug level %c out of range: %d\n", debug_type, level);
+ return false;
+ }
+ switch(debug_type) {
+ case 'a':
+ omega_core_debug = relation_debug = hull_debug =
+ closure_presburger_debug =
+ farkas_debug =
+ pres_debug = omega_calc_debug = code_gen_debug = level;
+ break;
+ case 'g':
+ code_gen_debug = level; break;
+ case 'f':
+ farkas_debug = level; break;
+ case 'h':
+ hull_debug = level; break;
+ case 'c':
+ omega_core_debug = level; break;
+ case 'r':
+ relation_debug = level; break;
+ case 'p':
+ pres_debug = level; break;
+ case 't':
+ closure_presburger_debug = level; break;
+ case 'l':
+ omega_calc_debug = level; break;
+#if defined STUDY_EVACUATIONS
+ case 'e':
+ evac_debug = level; break;
+#endif
+ default:
+ fprintf(stderr, "Unknown debug type %c\n", debug_type);
+ return false;
+ }
+ }
+ return true;
+}
+
+
+int main(int argc, char **argv) {
+#if YYDEBUG != 0
+ yydebug = 1;
+#endif
+
+ /* process flags */
+ char *fileName = 0;
+ for(int i=1; i<argc; i++) {
+ if(argv[i][0] == '-') {
+ int j = 1, c;
+ while((c=argv[i][j++]) != 0) {
+ switch(c) {
+ case 'D':
+ if (!process_calc_debugging_flags(argv[i],j)) {
+ printUsage(stderr, argv);
+ exit(1);
+ }
+ break;
+ case 'G':
+ fprintf(stderr,"Note: specifying number of GEQ's is no longer useful.\n");
+ while(argv[i][j] != 0) j++;
+ break;
+ case 'E':
+ fprintf(stderr,"Note: specifying number of EQ's is no longer useful.\n");
+ while(argv[i][j] != 0) j++;
+ break;
+ case 'R':
+ redundant_conj_level = 1;
+ break;
+ /* Other future options go here */
+ case 'h':
+ printUsage(stderr, argv);
+ exit(1);
+ break;
+ default:
+ fprintf(stderr, "\nUnknown flag -%c\n", c);
+ printUsage(stderr, argv);
+ exit(1);
+ }
+ }
+ }
+ else {
+ /* Make sure this is a file name */
+ if (fileName) {
+ fprintf(stderr,"\nCan only handle a single input file\n");
+ printUsage(stderr,argv);
+ exit(1);
+ }
+ fileName = argv[i];
+ yyin = fopen(fileName, "r");
+ if (!yyin) {
+ fprintf(stderr, "\nCan't open input file %s\n",fileName);
+ printUsage(stderr,argv);
+ exit(1);
+ }
+ }
+ }
+
+ if (fileName || !isatty((int)fileno(stdin))) {
+ is_interactive = false;
+ }
+ else {
+ is_interactive = true;
+ setbuf(DebugFile, NULL);
+ printf("Calculator for Omega+ v20110204snapshot (built on %s)\n", OMEGA_BUILD_DATE);
+ printf("Copyright (C) 1994-2000 University of Maryland the Omega Project Team\n");
+ printf("Copyright (C) 2008 University of Southern California\n");
+ printf("Copyright (C) 2009-2011 University of Utah\n");
+ printf("%s ", PROMPT_STRING);
+ }
+ need_coef = false;
+ current_Declaration_Site = globalDecls = new Global_Declaration_Site();
+
+ if (yyparse() != 0) {
+ if (!is_interactive)
+ std::cout << "syntax error at the end of the file, missing ';'" << std::endl;
+ else
+ std::cout << std::endl;
+ delete relationDecl;
+ relationDecl = NULL;
+ }
+ else {
+ if (is_interactive)
+ std::cout << std::endl;
+ }
+
+ foreach_map(cs,Const_String,r,Relation *,relationMap,
+ {delete r; relationMap[cs]=0;});
+ delete globalDecls;
+ fclose(yyin);
+
+ return 0;
+}
+
+Relation LexForward(int n) {
+ Relation r(n,n);
+ F_Or *f = r.add_or();
+ for (int i=1; i <= n; i++) {
+ F_And *g = f->add_and();
+ for(int j=1;j<i;j++) {
+ EQ_Handle e = g->add_EQ();
+ e.update_coef(r.input_var(j),-1);
+ e.update_coef(r.output_var(j),1);
+ e.finalize();
+ }
+ GEQ_Handle e = g->add_GEQ();
+ e.update_coef(r.input_var(i),-1);
+ e.update_coef(r.output_var(i),1);
+ e.update_const(-1);
+ e.finalize();
+ }
+ r.finalize();
+ return r;
+}
diff --git a/omega/omega_calc/src/parser.yy b/omega/omega_calc/src/parser.yy
new file mode 100755
index 0000000..cad6e8e
--- /dev/null
+++ b/omega/omega_calc/src/parser.yy
@@ -0,0 +1,1928 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2005-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+ yacc parser for calculator.
+
+ Notes:
+
+ History:
+ 02/04/11 work with flex c++ mode, Chun Chen
+*****************************************************************************/
+
+%{
+//#define YYDEBUG 1
+#include <basic/Dynamic_Array.h>
+#include <basic/Iterator.h>
+#include <omega_calc/AST.h>
+#include <omega/hull.h>
+#include <omega/closure.h>
+#include <omega/reach.h>
+#include <string>
+#include <iostream>
+#include <fstream>
+#include "parser.tab.hh"
+#include <omega_calc/myflex.h>
+//#include <stdio.h>
+
+#if defined __USE_POSIX
+#include <unistd.h>
+#elif defined __WIN32
+#include <io.h>
+#endif
+
+
+#ifndef WIN32
+#include <sys/time.h>
+#include <sys/resource.h>
+#endif
+#if !defined(OMIT_GETRUSAGE)
+#include <sys/types.h>
+#include <sys/time.h>
+#include <sys/resource.h>
+#endif
+
+#if !defined(OMIT_GETRUSAGE)
+#ifdef __sparc__
+extern "C" int getrusage (int, struct rusage*);
+#endif
+
+
+
+
+struct rusage start_time;
+bool anyTimingDone = false;
+
+void start_clock( void ) {
+ getrusage(RUSAGE_SELF, &start_time);
+}
+
+int clock_diff( void ) {
+ struct rusage current_time;
+ getrusage(RUSAGE_SELF, ¤t_time);
+ return (current_time.ru_utime.tv_sec -start_time.ru_utime.tv_sec)*1000000 + (current_time.ru_utime.tv_usec-start_time.ru_utime.tv_usec);
+}
+#endif
+
+
+#ifdef BUILD_CODEGEN
+#include <code_gen/codegen.h>
+#endif
+
+extern myFlexLexer mylexer;
+#define yylex mylexer.yylex
+
+
+
+
+int omega_calc_debug = 0;
+
+extern bool is_interactive;
+extern const char *PROMPT_STRING;
+bool simplify = true;
+using namespace omega;
+
+extern std::string err_msg;
+
+bool need_coef;
+
+namespace {
+ int redundant_conj_level = 2; // default maximum 2
+ int redundant_constr_level = 4; // default maximum 4
+}
+
+std::map<std::string, Relation *> relationMap;
+int argCount = 0;
+int tuplePos = 0;
+Argument_Tuple currentTuple = Input_Tuple;
+
+Relation LexForward(int n);
+reachable_information *reachable_info;
+
+void yyerror(const std::string &s);
+void flushScanBuffer();
+
+%}
+
+%union {
+ int INT_VALUE;
+ omega::coef_t COEF_VALUE;
+ Rel_Op REL_OPERATOR;
+ char *VAR_NAME;
+ std::set<char *> *VAR_LIST;
+ Exp *EXP;
+ std::set<Exp *> *EXP_LIST;
+ AST *ASTP;
+ omega::Argument_Tuple ARGUMENT_TUPLE;
+ AST_constraints *ASTCP;
+ Declaration_Site *DECLARATION_SITE;
+ omega::Relation *RELATION;
+ tupleDescriptor *TUPLE_DESCRIPTOR;
+ std::pair<std::vector<omega::Relation>, std::vector<omega::Relation> > *REL_TUPLE_PAIR;
+ omega::Dynamic_Array1<omega::Relation> * RELATION_ARRAY_1D;
+ std::string *STRING_VALUE;
+}
+
+%token <VAR_NAME> VAR
+%token <INT_VALUE> INT
+%token <COEF_VALUE> COEF
+%token <STRING_VALUE> STRING
+%token OPEN_BRACE CLOSE_BRACE
+%token SYMBOLIC NO_SIMPLIFY
+%token OR AND NOT
+%token ST APPROX
+%token IS_ASSIGNED
+%token FORALL EXISTS
+%token DOMAIN RANGE
+%token DIFFERENCE DIFFERENCE_TO_RELATION
+%token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
+%token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION LINEAR_COMBINATION AFFINE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL QUICK_HULL PAIRWISE_CHECK CONVEX_CHECK CONVEX_REPRESENTATION RECT_HULL SIMPLE_HULL DECOUPLED_CONVEX_HULL
+%token MAXIMIZE_RANGE MINIMIZE_RANGE
+%token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
+%token LEQ GEQ NEQ
+%token GOES_TO
+%token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
+%token UNION INTERSECTION
+%token VERTICAL_BAR SUCH_THAT
+%token SUBSET CODEGEN DECOUPLED_FARKAS FARKAS
+%token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
+%token <REL_OPERATOR> REL_OP
+%token RESTRICT_DOMAIN RESTRICT_RANGE
+%token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
+%token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
+%token ASSERT_UNSAT
+%token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
+
+%type <EXP> exp simpleExp
+%type <EXP_LIST> expList
+%type <VAR_LIST> varList
+%type <ARGUMENT_TUPLE> argumentList
+%type <ASTP> formula optionalFormula
+%type <ASTCP> constraintChain
+%type <TUPLE_DESCRIPTOR> tupleDeclaration
+%type <DECLARATION_SITE> varDecl varDeclOptBrackets
+%type <RELATION> relation builtRelation context
+%type <RELATION> reachable_of
+%type <REL_TUPLE_PAIR> relPairList
+%type <RELATION_ARRAY_1D> reachable
+
+%destructor {delete []$$;} VAR
+%destructor {delete $$;} STRING
+%destructor {delete $$;} relation builtRelation tupleDeclaration formula optionalFormula context reachable_of constraintChain varDecl varDeclOptBrackets relPairList reachable
+%destructor {delete $$;} exp simpleExp
+%destructor {
+ for (std::set<Exp *>::iterator i = $$->begin(); i != $$->end(); i++)
+ delete *i;
+ delete $$;
+ } expList;
+%destructor {
+ for (std::set<char *>::iterator i = $$->begin(); i != $$->end(); i++)
+ delete []*i;
+ delete $$;
+ } varList;
+
+%nonassoc ASSERT_UNSAT
+%left UNION p1 '+' '-'
+%nonassoc SUPERSETOF SUBSETOF
+%left p2 RESTRICT_DOMAIN RESTRICT_RANGE
+%left INTERSECTION p3 '*' '@'
+%left p4
+%left OR p5
+%left AND p6
+%left COMPOSE JOIN CARRIED_BY
+%right NOT APPROX DOMAIN RANGE HULL PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS DIFFERENCE DIFFERENCE_TO_RELATION INVERSE COMPLEMENT FARKAS SAMPLE SYM_SAMPLE MAKE_UPPER_BOUND MAKE_LOWER_BOUND p7
+%left p8
+%nonassoc GIVEN
+%left p9
+%left '(' p10
+
+%%
+
+inputSequence : /*empty*/
+ | inputSequence { assert( current_Declaration_Site == globalDecls);}
+ inputItem;
+;
+
+inputItem : ';' /*empty*/
+ | NO_SIMPLIFY ';'{
+ simplify = false;
+ }
+ | error ';' {
+ flushScanBuffer();
+ std::cout << err_msg;
+ err_msg.clear();
+ current_Declaration_Site = globalDecls;
+ need_coef = false;
+ std::cout << "...skipping to statement end..." << std::endl;
+ delete relationDecl;
+ relationDecl = NULL;
+ }
+ | SYMBOLIC globVarList ';' {flushScanBuffer();}
+ | VAR IS_ASSIGNED relation ';' {
+ flushScanBuffer();
+ try {
+ if(simplify)
+ $3->simplify(redundant_conj_level, redundant_constr_level);
+ else
+ $3->simplify();
+ Relation *r = relationMap[std::string($1)];
+ if (r != NULL) delete r;
+ relationMap[std::string($1)] = $3;
+ }
+ catch(const std::exception &e){
+ std::cout << e.what() << std::endl;
+ }
+
+ delete []$1;
+ }
+ | relation ';' {
+ flushScanBuffer();
+ if(simplify)
+ $1->simplify(redundant_conj_level, redundant_constr_level);
+ else
+ $1->simplify();
+ $1->print_with_subs(stdout);
+ delete $1;
+ }
+ | TIME relation ';' {
+#if defined(OMIT_GETRUSAGE)
+ printf("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
+#else
+ flushScanBuffer();
+ printf("\n");
+ int t;
+ Relation R;
+ bool SKIP_FULL_CHECK = getenv("OC_TIMING_SKIP_FULL_CHECK");
+ ($2)->and_with_GEQ();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ }
+ int copyTime = clock_diff();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ R.simplify(); /* default simplification effort */
+ }
+ int simplifyTime = clock_diff() -copyTime;
+ Relation R2;
+ if (!SKIP_FULL_CHECK) {
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R2 = *$2;
+ R2.finalize();
+ R2.simplify(2,4); /* maximal simplification effort */
+ }
+ }
+ int excessiveTime = clock_diff() - copyTime;
+ printf("Times (in microseconds): \n");
+ printf("%5d us to copy original set of constraints\n",copyTime/100);
+ printf("%5d us to do the default amount of simplification, obtaining: \n\t", simplifyTime/100);
+ R.print_with_subs(stdout);
+ printf("\n");
+ if (!SKIP_FULL_CHECK) {
+ printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", excessiveTime/100);
+ R2.print_with_subs(stdout);
+ printf("\n");
+ }
+ if (!anyTimingDone) {
+ bool warn = false;
+#ifndef SPEED
+ warn =true;
+#endif
+#ifndef NDEBUG
+ warn = true;
+#endif
+ if (warn) {
+ printf("WARNING: The Omega calculator was compiled with options that force\n");
+ printf("it to perform additional consistency and error checks\n");
+ printf("that may slow it down substantially\n");
+ printf("\n");
+ }
+ printf("NOTE: These times relect the time of the current _implementation_\n");
+ printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
+ printf("report on the performance on the Omega test, we respectfully but strongly \n");
+ printf("request that send your test cases to us to allow us to determine if the \n");
+ printf("times are appropriate, and if the way you are using the Omega library to \n");
+ printf("solve your problem is the most effective way.\n");
+ printf("\n");
+
+ printf("Also, please be aware that over the past two years, we have focused our \n");
+ printf("efforts on the expressive power of the Omega library, sometimes at the\n");
+ printf("expensive of raw speed. Our original implementation of the Omega test\n");
+ printf("was substantially faster on the limited domain it handled.\n");
+ printf("\n");
+ printf(" Thanks, \n");
+ printf(" the Omega Team \n");
+ }
+ anyTimingDone = true;
+ delete $2;
+#endif
+ }
+ | TIMECLOSURE relation ';' {
+#if defined(OMIT_GETRUSAGE)
+ printf("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
+#else
+ flushScanBuffer();
+ try {
+ int t;
+ Relation R;
+ ($2)->and_with_GEQ();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ }
+ int copyTime = clock_diff();
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R = *$2;
+ R.finalize();
+ R.simplify();
+ }
+ int simplifyTime = clock_diff() -copyTime;
+ Relation Rclosed;
+ start_clock();
+ for (t=1;t<=100;t++) {
+ Rclosed = *$2;
+ Rclosed.finalize();
+ Rclosed = TransitiveClosure(Rclosed, 1,Relation::Null());
+ }
+ int closureTime = clock_diff() - copyTime;
+ Relation R2;
+ start_clock();
+ for (t=1;t<=100;t++) {
+ R2 = *$2;
+ R2.finalize();
+ R2.simplify(2,4);
+ }
+ int excessiveTime = clock_diff() - copyTime;
+ printf("Times (in microseconds): \n");
+ printf("%5d us to copy original set of constraints\n",copyTime/100);
+ printf("%5d us to do the default amount of simplification, obtaining: \n\t", simplifyTime/100);
+ R.print_with_subs(stdout);
+ printf("\n");
+ printf("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t", excessiveTime/100);
+ R2.print_with_subs(stdout);
+ printf("%5d us to do the transitive closure, obtaining: \n\t", closureTime/100);
+ Rclosed.print_with_subs(stdout);
+ printf("\n");
+ if (!anyTimingDone) {
+ bool warn = false;
+#ifndef SPEED
+ warn =true;
+#endif
+#ifndef NDEBUG
+ warn = true;
+#endif
+ if (warn) {
+ printf("WARNING: The Omega calculator was compiled with options that force\n");
+ printf("it to perform additional consistency and error checks\n");
+ printf("that may slow it down substantially\n");
+ printf("\n");
+ }
+ printf("NOTE: These times relect the time of the current _implementation_\n");
+ printf("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
+ printf("report on the performance on the Omega test, we respectfully but strongly \n");
+ printf("request that send your test cases to us to allow us to determine if the \n");
+ printf("times are appropriate, and if the way you are using the Omega library to \n");
+ printf("solve your problem is the most effective way.\n");
+ printf("\n");
+
+ printf("Also, please be aware that over the past two years, we have focused our \n");
+ printf("efforts on the expressive power of the Omega library, sometimes at the\n");
+ printf("expensive of raw speed. Our original implementation of the Omega test\n");
+ printf("was substantially faster on the limited domain it handled.\n");
+ printf("\n");
+ printf(" Thanks, \n");
+ printf(" the Omega Team \n");
+ }
+ anyTimingDone = true;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+ delete $2;
+#endif
+ }
+ | relation SUBSET relation ';' {
+ flushScanBuffer();
+ try {
+ if (Must_Be_Subset(copy(*$1), copy(*$3)))
+ std::cout << "True" << std::endl;
+ else if (Might_Be_Subset(copy(*$1), copy(*$3)))
+ std::cout << "Possible" << std::endl;
+ else
+ std::cout << "False" << std::endl;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+ delete $1;
+ delete $3;
+ }
+ | CODEGEN relPairList context';' {
+ flushScanBuffer();
+#ifdef BUILD_CODEGEN
+ try {
+ CodeGen cg($2->first, $2->second, *$3);
+ CG_result *cgr = cg.buildAST();
+ if (cgr != NULL) {
+ std::string s = cgr->printString();
+ std::cout << s << std::endl;
+ delete cgr;
+ }
+ else
+ std::cout << "/* empty */" << std::endl;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+#else
+ std::cout << "CodeGen package not built" << std::endl;
+#endif
+ delete $3;
+ delete $2;
+ }
+ | CODEGEN INT relPairList context';' {
+ flushScanBuffer();
+#ifdef BUILD_CODEGEN
+ try {
+ CodeGen cg($3->first, $3->second, *$4);
+ CG_result *cgr = cg.buildAST($2);
+ if (cgr != NULL) {
+ std::string s = cgr->printString();
+ std::cout << s << std::endl;
+ delete cgr;
+ }
+ else
+ std::cout << "/* empty */" << std::endl;
+ }
+ catch (const std::exception &e) {
+ std::cout << e.what() << std::endl;
+ }
+#else
+ std::cout << "CodeGen package not built" << std::endl;
+#endif
+ delete $4;
+ delete $3;
+ }
+ | reachable ';' {
+ flushScanBuffer();
+ Dynamic_Array1<Relation> &final = *$1;
+ bool any_sat = false;
+ int i,n_nodes = reachable_info->node_names.size();
+ for(i = 1; i <= n_nodes; i++)
+ if(final[i].is_upper_bound_satisfiable()) {
+ any_sat = true;
+ std::cout << "Node " << reachable_info->node_names[i] << ": ";
+ final[i].print_with_subs(stdout);
+ }
+ if(!any_sat)
+ std::cout << "No nodes reachable.\n";
+ delete $1;
+ delete reachable_info;
+ }
+;
+
+
+context : {$$ = new Relation(); *$$ = Relation::Null();}
+ | GIVEN relation {$$ = $2; }
+;
+
+relPairList : relPairList ',' relation ':' relation {
+ try {
+ $1->first.push_back(*$3);
+ $1->second.push_back(*$5);
+ }
+ catch (const std::exception &e) {
+ delete $1;
+ delete $3;
+ delete $5;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $3;
+ delete $5;
+ $$ = $1;
+ }
+ | relPairList ',' relation {
+ try {
+ $1->first.push_back(Identity($3->n_set()));
+ $1->second.push_back(*$3);
+ }
+ catch (const std::exception &e) {
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $3;
+ $$ = $1;
+ }
+ | relation ':' relation {
+ std::pair<std::vector<Relation>, std::vector<Relation> > *rtp = new std::pair<std::vector<Relation>, std::vector<Relation> >();
+ try {
+ rtp->first.push_back(*$1);
+ rtp->second.push_back(*$3);
+ }
+ catch (const std::exception &e) {
+ delete rtp;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ $$ = rtp;
+ }
+ | relation {
+ std::pair<std::vector<Relation>, std::vector<Relation> > *rtp = new std::pair<std::vector<Relation>, std::vector<Relation> >();
+ try {
+ rtp->first.push_back(Identity($1->n_set()));
+ rtp->second.push_back(*$1);
+ }
+ catch (const std::exception &e) {
+ delete rtp;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ $$ = rtp;
+ }
+;
+
+relation : OPEN_BRACE {need_coef = true; relationDecl = new Declaration_Site();}
+ builtRelation CLOSE_BRACE {
+ need_coef = false;
+ $$ = $3;
+ current_Declaration_Site = globalDecls;
+ delete relationDecl;
+ relationDecl = NULL;
+ }
+ | VAR {
+ Relation *r = relationMap[std::string($1)];
+ if (r == NULL) {
+ yyerror(std::string("relation ") + to_string($1) + std::string(" not declared"));
+ delete []$1;
+ YYERROR;
+ }
+ $$ = new Relation(*r);
+ delete []$1;
+ }
+ | '(' relation ')' {$$ = $2;}
+ | relation '+' %prec p9 {
+ $$ = new Relation();
+ try {
+ *$$ = TransitiveClosure(*$1, 1, Relation::Null());
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation '*' %prec p9 {
+ $$ = new Relation();
+ try {
+ int vars = $1->n_inp();
+ *$$ = Union(Identity(vars), TransitiveClosure(*$1, 1, Relation::Null()));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation '+' WITHIN relation %prec p9 {
+ $$ = new Relation();
+ try {
+ *$$= TransitiveClosure(*$1, 1, *$4);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $4;
+ }
+ | relation '^' '@' %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ApproxClosure(*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation '^' '+' %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = calculateTransitiveClosure(*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | MINIMIZE_RANGE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(r,LexForward($2->n_out()));
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAXIMIZE_RANGE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(r,Inverse(LexForward($2->n_out())));
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MINIMIZE_DOMAIN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(LexForward($2->n_inp()),r);
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAXIMIZE_DOMAIN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation o(*$2);
+ Relation r(*$2);
+ r = Join(Inverse(LexForward($2->n_inp())),r);
+ *$$ = Difference(o,r);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAXIMIZE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation c(*$2);
+ Relation r(*$2);
+ *$$ = Cross_Product(Relation(*$2),c);
+ *$$ = Difference(r,Domain(Intersection(*$$,LexForward($$->n_inp()))));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MINIMIZE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ Relation c(*$2);
+ Relation r(*$2);
+ *$$ = Cross_Product(Relation(*$2),c);
+ *$$ = Difference(r,Range(Intersection(*$$,LexForward($$->n_inp()))));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | FARKAS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2, Basic_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DECOUPLED_FARKAS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2, Decoupled_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | relation '@' %prec p9 {
+ $$ = new Relation();
+ try {
+ *$$ = ConicClosure(*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | PROJECT_AWAY_SYMBOLS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Project_Sym(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | PROJECT_ON_SYMBOLS relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Project_On_Sym(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DIFFERENCE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Deltas(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DIFFERENCE_TO_RELATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = DeltasToRelation(*$2,$2->n_set(),$2->n_set());
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DOMAIN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Domain(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | VENN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = VennDiagramForm(*$2,Relation::True(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | VENN relation GIVEN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = VennDiagramForm(*$2,*$4);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ delete $4;
+ }
+ | CONVEX_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ConvexHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | DECOUPLED_CONVEX_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = DecoupledConvexHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | POSITIVE_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Positive_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | LINEAR_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Linear_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | AFFINE_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Affine_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONVEX_COMBINATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Farkas(*$2,Convex_Combination_Farkas);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | PAIRWISE_CHECK relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = CheckForConvexRepresentation(CheckForConvexPairs(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONVEX_CHECK relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = CheckForConvexRepresentation(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONVEX_REPRESENTATION relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ConvexRepresentation(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | AFFINE_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = AffineHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | CONIC_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = ConicHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | LINEAR_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = LinearHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | QUICK_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = QuickHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | RECT_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = RectHull(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SIMPLE_HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = SimpleHull(*$2, true, true);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | HULL relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Hull(*$2,true,1,Relation::Null());
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | HULL relation GIVEN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Hull(*$2,true,1,*$4);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ delete $4;
+ }
+ | APPROX relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Approximate(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | RANGE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Range(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | INVERSE relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Inverse(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | COMPLEMENT relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Complement(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | GIST relation GIVEN relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Gist(*$2,*$4,1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ delete $4;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ delete $4;
+ }
+ | relation '(' relation ')' {
+ $$ = new Relation();
+ try {
+ *$$ = Composition(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation COMPOSE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Composition(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation CARRIED_BY INT {
+ $$ = new Relation();
+ try {
+ *$$ = After(*$1,$3,$3);
+ (*$$).prefix_print(stdout);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ }
+ | relation JOIN relation {
+ $$ = new Relation();
+ try {
+ *$$ = Composition(*$3,*$1);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation RESTRICT_RANGE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Restrict_Range(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation RESTRICT_DOMAIN relation {
+ $$ = new Relation();
+ try {
+ *$$ = Restrict_Domain(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation INTERSECTION relation {
+ $$ = new Relation();
+ try {
+ *$$ = Intersection(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation '-' relation %prec INTERSECTION {
+ $$ = new Relation();
+ try {
+ *$$ = Difference(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation UNION relation {
+ $$ = new Relation();
+ try {
+ *$$ = Union(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | relation '*' relation {
+ $$ = new Relation();
+ try {
+ *$$ = Cross_Product(*$1,*$3);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $1;
+ delete $3;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $1;
+ delete $3;
+ }
+ | SUPERSETOF relation {
+ $$ = new Relation();
+ try {
+ *$$ = Union(*$2, Relation::Unknown(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SUBSETOF relation {
+ $$ = new Relation();
+ try {
+ *$$ = Intersection(*$2, Relation::Unknown(*$2));
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAKE_UPPER_BOUND relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Upper_Bound(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | MAKE_LOWER_BOUND relation %prec p8 {
+ $$ = new Relation();
+ try {
+ *$$ = Lower_Bound(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SAMPLE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Sample_Solution(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | SYM_SAMPLE relation {
+ $$ = new Relation();
+ try {
+ *$$ = Symbolic_Solution(*$2);
+ }
+ catch (const std::exception &e) {
+ delete $$;
+ delete $2;
+ yyerror(e.what());
+ YYERROR;
+ }
+ delete $2;
+ }
+ | reachable_of { $$ = $1; }
+ | ASSERT_UNSAT relation {
+ if (($2)->is_satisfiable()) {
+ fprintf(stderr,"assert_unsatisfiable failed on ");
+ ($2)->print_with_subs(stderr);
+ exit(1);
+ }
+ $$=$2;
+ }
+;
+
+builtRelation : tupleDeclaration GOES_TO {currentTuple = Output_Tuple;}
+ tupleDeclaration {currentTuple = Input_Tuple;} optionalFormula {
+ Relation * r = new Relation($1->size,$4->size);
+ resetGlobals();
+ F_And *f = r->add_and();
+ for(int i = 1; i <= $1->size; i++) {
+ $1->vars[i-1]->vid = r->input_var(i);
+ if (!$1->vars[i-1]->anonymous)
+ r->name_input_var(i, $1->vars[i-1]->stripped_name);
+ }
+ for(int i = 1; i <= $4->size; i++) {
+ $4->vars[i-1]->vid = r->output_var(i);
+ if (!$4->vars[i-1]->anonymous)
+ r->name_output_var(i, $4->vars[i-1]->stripped_name);
+ }
+ r->setup_names();
+ for (std::set<Exp *>::iterator i = $1->eq_constraints.begin(); i != $1->eq_constraints.end(); i++)
+ install_eq(f, *i, 0);
+ for (std::set<Exp *>::iterator i = $1->geq_constraints.begin(); i != $1->geq_constraints.end(); i++)
+ install_geq(f, *i, 0);
+ for (std::set<strideConstraint *>::iterator i = $1->stride_constraints.begin(); i != $1->stride_constraints.end(); i++)
+ install_stride(f, *i);
+ for (std::set<Exp *>::iterator i = $4->eq_constraints.begin(); i != $4->eq_constraints.end(); i++)
+ install_eq(f, *i, 0);
+ for (std::set<Exp *>::iterator i = $4->geq_constraints.begin(); i != $4->geq_constraints.end(); i++)
+ install_geq(f, *i, 0);
+ for (std::set<strideConstraint *>::iterator i = $4->stride_constraints.begin(); i != $4->stride_constraints.end(); i++)
+ install_stride(f, *i);
+ if ($6) $6->install(f);
+ delete $1;
+ delete $4;
+ delete $6;
+ $$ = r;
+ }
+ | tupleDeclaration optionalFormula {
+ Relation * r = new Relation($1->size);
+ resetGlobals();
+ F_And *f = r->add_and();
+ for(int i = 1; i <= $1->size; i++) {
+ $1->vars[i-1]->vid = r->set_var(i);
+ if (!$1->vars[i-1]->anonymous)
+ r->name_set_var(i, $1->vars[i-1]->stripped_name);
+ }
+ r->setup_names();
+ for (std::set<Exp *>::iterator i = $1->eq_constraints.begin(); i != $1->eq_constraints.end(); i++)
+ install_eq(f, *i, 0);
+ for (std::set<Exp *>::iterator i = $1->geq_constraints.begin(); i != $1->geq_constraints.end(); i++)
+ install_geq(f, *i, 0);
+ for (std::set<strideConstraint *>::iterator i = $1->stride_constraints.begin(); i != $1->stride_constraints.end(); i++)
+ install_stride(f, *i);
+ if ($2) $2->install(f);
+ delete $1;
+ delete $2;
+ $$ = r;
+ }
+ | formula {
+ Relation * r = new Relation(0,0);
+ F_And *f = r->add_and();
+ $1->install(f);
+ delete $1;
+ $$ = r;
+ }
+;
+
+optionalFormula : formula_sep formula {$$ = $2;}
+ | {$$ = 0;}
+;
+
+formula_sep : ':'
+ | VERTICAL_BAR
+ | SUCH_THAT
+;
+
+tupleDeclaration : {currentTupleDescriptor = new tupleDescriptor; tuplePos = 1;}
+ '[' optionalTupleVarList ']'
+ {$$ = currentTupleDescriptor; tuplePos = 0;}
+;
+
+optionalTupleVarList : /* empty */
+ | tupleVar
+ | optionalTupleVarList ',' tupleVar
+;
+
+tupleVar : VAR %prec p10 {
+ Declaration_Site *ds = defined($1);
+ if (!ds)
+ currentTupleDescriptor->extend($1,currentTuple,tuplePos);
+ else {
+ Variable_Ref *v = lookupScalar($1);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$1;
+ YYERROR;
+ }
+ if (ds != globalDecls)
+ currentTupleDescriptor->extend($1, new Exp(v));
+ else
+ currentTupleDescriptor->extend(new Exp(v));
+ }
+ tuplePos++;
+ delete []$1;
+ }
+ | '*' {currentTupleDescriptor->extend(); tuplePos++;}
+ | exp %prec p1 {
+ currentTupleDescriptor->extend($1);
+ tuplePos++;
+ }
+ | exp ':' exp %prec p1 {
+ currentTupleDescriptor->extend($1,$3);
+ tuplePos++;
+ }
+ | exp ':' exp ':' COEF %prec p1 {
+ currentTupleDescriptor->extend($1,$3,$5);
+ tuplePos++;
+ }
+;
+
+varList : varList ',' VAR {$$ = $1; $$->insert($3); $3 = NULL;}
+ | VAR {$$ = new std::set<char *>(); $$->insert($1); $1 = NULL;}
+;
+
+varDecl : varList {
+ $$ = current_Declaration_Site = new Declaration_Site($1);
+ for (std::set<char *>::iterator i = $1->begin(); i != $1->end(); i++)
+ delete [](*i);
+ delete $1;
+ }
+;
+
+varDeclOptBrackets : varDecl {$$ = $1;}
+ |'[' varDecl ']' {$$ = $2;}
+;
+
+globVarList : globVarList ',' globVar
+ | globVar
+;
+
+globVar : VAR '(' INT ')' {globalDecls->extend_both_tuples($1, $3); delete []$1;}
+ | VAR {
+ globalDecls->extend($1);
+ delete []$1;
+ }
+;
+
+formula : formula AND formula {$$ = new AST_And($1,$3);}
+ | formula OR formula {$$ = new AST_Or($1,$3);}
+ | constraintChain {$$ = $1;}
+ | '(' formula ')' {$$ = $2;}
+ | NOT formula {$$ = new AST_Not($2);}
+ | start_exists varDeclOptBrackets exists_sep formula end_quant {$$ = new AST_exists($2,$4);}
+ | start_forall varDeclOptBrackets forall_sep formula end_quant {$$ = new AST_forall($2,$4);}
+;
+
+start_exists : '(' EXISTS
+ | EXISTS '('
+;
+
+exists_sep : ':'
+ | VERTICAL_BAR
+ | SUCH_THAT
+;
+
+start_forall : '(' FORALL
+ | FORALL '('
+;
+
+forall_sep : ':'
+;
+
+end_quant : ')' {popScope();}
+;
+
+expList : exp ',' expList {$$ = $3; $$->insert($1);}
+ | exp {$$ = new std::set<Exp *>(); $$->insert($1);}
+;
+
+constraintChain : expList REL_OP expList {$$ = new AST_constraints($1,$2,$3);}
+ | expList REL_OP constraintChain {$$ = new AST_constraints($1,$2,$3);}
+;
+
+simpleExp : VAR %prec p9 {
+ Variable_Ref *v = lookupScalar($1);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$1;
+ YYERROR;
+ }
+ $$ = new Exp(v);
+ delete []$1;
+ }
+ | VAR '(' {argCount = 1;} argumentList ')' %prec p9 {
+ Variable_Ref *v;
+ if ($4 == Input_Tuple)
+ v = functionOfInput[$1];
+ else
+ v = functionOfOutput[$1];
+ if (v == NULL) {
+ yyerror(std::string("Function ") + to_string($1) + std::string(" not declared"));
+ delete []$1;
+ YYERROR;
+ }
+ $$ = new Exp(v);
+ delete []$1;
+ }
+ | '(' exp ')' { $$ = $2; }
+;
+
+argumentList : argumentList ',' VAR {
+ Variable_Ref *v = lookupScalar($3);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$3;
+ YYERROR;
+ }
+ if (v->pos != argCount || v->of != $1 || (v->of != Input_Tuple && v->of != Output_Tuple)) {
+ yyerror("arguments to function must be prefix of input or output tuple");
+ delete []$3;
+ YYERROR;
+ }
+ $$ = v->of;
+ argCount++;
+ delete []$3;
+ }
+ | VAR {
+ Variable_Ref *v = lookupScalar($1);
+ if (v == NULL) {
+ yyerror(std::string("cannot find declaration for variable ") + to_string($1));
+ delete []$1;
+ YYERROR;
+ }
+ if (v->pos != argCount || (v->of != Input_Tuple && v->of != Output_Tuple)) {
+ yyerror("arguments to function must be prefix of input or output tuple");
+ delete []$1;
+ YYERROR;
+ }
+ $$ = v->of;
+ argCount++;
+ delete []$1;
+ }
+;
+
+exp : COEF {$$ = new Exp($1);}
+ | COEF simpleExp %prec '*' {$$ = multiply($1,$2);}
+ | simpleExp {$$ = $1; }
+ | '-' exp %prec '*' {$$ = negate($2);}
+ | exp '+' exp {$$ = add($1,$3);}
+ | exp '-' exp {$$ = subtract($1,$3);}
+ | exp '*' exp {
+ try {
+ $$ = multiply($1,$3);
+ }
+ catch (const std::exception &e) {
+ yyerror(e.what());
+ YYERROR;
+ }
+ }
+;
+
+
+reachable : REACHABLE_FROM nodeNameList nodeSpecificationList {
+ Dynamic_Array1<Relation> *final = Reachable_Nodes(reachable_info);
+ $$ = final;
+ }
+;
+
+reachable_of : REACHABLE_OF VAR IN nodeNameList nodeSpecificationList {
+ Dynamic_Array1<Relation> *final = Reachable_Nodes(reachable_info);
+ int index = reachable_info->node_names.index(std::string($2));
+ if (index == 0) {
+ yyerror(std::string("no such node ") + to_string($2));
+ delete []$2;
+ delete final;
+ delete reachable_info;
+ YYERROR;
+ }
+ $$ = new Relation;
+ *$$ = (*final)[index];
+ delete final;
+ delete reachable_info;
+ delete []$2;
+ }
+;
+
+nodeNameList : '(' realNodeNameList ')' {
+ int sz = reachable_info->node_names.size();
+ reachable_info->node_arity.reallocate(sz);
+ reachable_info->transitions.resize(sz+1,sz+1);
+ reachable_info->start_nodes.resize(sz+1);
+ }
+;
+
+realNodeNameList : realNodeNameList ',' VAR {
+ reachable_info->node_names.append(std::string($3));
+ delete []$3;
+ }
+ | VAR {
+ reachable_info = new reachable_information;
+ reachable_info->node_names.append(std::string($1));
+ delete []$1;
+ }
+;
+
+
+nodeSpecificationList : OPEN_BRACE realNodeSpecificationList CLOSE_BRACE {
+ int i,j;
+ int n_nodes = reachable_info->node_names.size();
+ Tuple<int> &arity = reachable_info->node_arity;
+ Dynamic_Array2<Relation> &transitions = reachable_info->transitions;
+
+ /* fixup unspecified transitions to be false */
+ /* find arity */
+ for(i = 1; i <= n_nodes; i++) arity[i] = -1;
+ for(i = 1; i <= n_nodes; i++)
+ for(j = 1; j <= n_nodes; j++)
+ if(! transitions[i][j].is_null()) {
+ int in_arity = transitions[i][j].n_inp();
+ int out_arity = transitions[i][j].n_out();
+ if(arity[i] < 0) arity[i] = in_arity;
+ if(arity[j] < 0) arity[j] = out_arity;
+ if(in_arity != arity[i] || out_arity != arity[j]) {
+ yyerror(std::string("arity mismatch in node transition: ") + to_string(reachable_info->node_names[i]) + std::string(" -> ") + to_string(reachable_info->node_names[j]));
+ delete reachable_info;
+ YYERROR;
+ }
+ }
+ for(i = 1; i <= n_nodes; i++)
+ if(arity[i] < 0) arity[i] = 0;
+ /* Fill in false relations */
+ for(i = 1; i <= n_nodes; i++)
+ for(j = 1; j <= n_nodes; j++)
+ if(transitions[i][j].is_null())
+ transitions[i][j] = Relation::False(arity[i],arity[j]);
+
+ /* fixup unused start node positions */
+ Dynamic_Array1<Relation> &nodes = reachable_info->start_nodes;
+ for(i = 1; i <= n_nodes; i++)
+ if(nodes[i].is_null())
+ nodes[i] = Relation::False(arity[i]);
+ else
+ if(nodes[i].n_set() != arity[i]){
+ yyerror(std::string("arity mismatch in start node ") + to_string(reachable_info->node_names[i]));
+ delete reachable_info;
+ YYERROR;
+ }
+ }
+;
+
+realNodeSpecificationList : realNodeSpecificationList ',' VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int index = reachable_info->node_names.index($3);
+ if (!(index > 0 && index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($3));
+ delete $5;
+ delete []$3;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->start_nodes[index] = *$5;
+ delete $5;
+ delete []$3;
+ }
+ | realNodeSpecificationList ',' VAR GOES_TO VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int from_index = reachable_info->node_names.index($3);
+ if (!(from_index > 0 && from_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($3));
+ delete $7;
+ delete []$3;
+ delete []$5;
+ delete reachable_info;
+ YYERROR;
+ }
+ int to_index = reachable_info->node_names.index($5);
+ if (!(to_index > 0 && to_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($5));
+ delete $7;
+ delete []$3;
+ delete []$5;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->transitions[from_index][to_index] = *$7;
+ delete $7;
+ delete []$3;
+ delete []$5;
+ }
+ | VAR GOES_TO VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int from_index = reachable_info->node_names.index($1);
+ if (!(from_index > 0 && from_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($1));
+ delete $5;
+ delete []$1;
+ delete []$3;
+ delete reachable_info;
+ YYERROR;
+ }
+ int to_index = reachable_info->node_names.index($3);
+ if (!(to_index > 0 && to_index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($3));
+ delete $5;
+ delete []$1;
+ delete []$3;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->transitions[from_index][to_index] = *$5;
+ delete $5;
+ delete []$1;
+ delete []$3;
+ }
+ | VAR ':' relation {
+ int n_nodes = reachable_info->node_names.size();
+ int index = reachable_info->node_names.index($1);
+ if (!(index > 0 && index <= n_nodes)) {
+ yyerror(std::string("no such node ")+to_string($1));
+ delete $3;
+ delete []$1;
+ delete reachable_info;
+ YYERROR;
+ }
+ reachable_info->start_nodes[index] = *$3;
+ delete $3;
+ delete []$1;
+ }
+;
+
+%%
+
+void yyerror(const std::string &s) {
+ std::stringstream ss;
+ if (is_interactive)
+ ss << s << "\n";
+ else
+ ss << s << " at line " << mylexer.lineno() << "\n";
+ err_msg = ss.str();
+}
+
+
+int main(int argc, char **argv) {
+ if (argc > 2){
+ fprintf(stderr, "Usage: %s [script_file]\n", argv[0]);
+ exit(1);
+ }
+
+ if (argc == 2) {
+ std::ifstream *ifs = new std::ifstream;
+ ifs->open(argv[1], std::ifstream::in);
+ if (!ifs->is_open()) {
+ fprintf(stderr, "can't open input file %s\n", argv[1]);
+ exit(1);
+ }
+ yy_buffer_state *bs = mylexer.yy_create_buffer(ifs, 8092);
+ mylexer.yypush_buffer_state(bs);
+ }
+
+ //yydebug = 1;
+ is_interactive = false;
+ if (argc == 1) {
+#if defined __USE_POSIX
+ if (isatty((int)fileno(stdin)))
+ is_interactive = true;
+#elif defined __WIN32
+ if (_isatty(_fileno(stdin)))
+ is_interactive = true;
+#endif
+ }
+
+ if (is_interactive) {
+#ifdef BUILD_CODEGEN
+ std::cout << "Omega+ and CodeGen+ ";
+#else
+ std::cout << "Omega+ ";
+#endif
+ std::cout << "v2.2.3 (built on " OMEGA_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;
+}
--
cgit v1.2.3-70-g09d2