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