summaryrefslogtreecommitdiff
path: root/omegalib/omegacalc/include/omega_calc
diff options
context:
space:
mode:
Diffstat (limited to 'omegalib/omegacalc/include/omega_calc')
-rw-r--r--omegalib/omegacalc/include/omega_calc/AST.h310
-rw-r--r--omegalib/omegacalc/include/omega_calc/PT-omega.c81
-rwxr-xr-xomegalib/omegacalc/include/omega_calc/myflex.h27
3 files changed, 418 insertions, 0 deletions
diff --git a/omegalib/omegacalc/include/omega_calc/AST.h b/omegalib/omegacalc/include/omega_calc/AST.h
new file mode 100644
index 0000000..58d74fb
--- /dev/null
+++ b/omegalib/omegacalc/include/omega_calc/AST.h
@@ -0,0 +1,310 @@
+#ifndef _AST_H
+#define _AST_H
+
+#include <assert.h>
+#include <omega.h>
+#include <map>
+#include <set>
+
+typedef enum {eq, lt, gt, geq, leq, neq} Rel_Op;
+
+class tupleDescriptor;
+
+class Variable_Ref {
+public:
+ int anonymous;
+ omega::Const_String name;
+ omega::Const_String stripped_name;
+ omega::Variable_ID vid;
+ omega::Variable_ID id(omega::Rel_Body *R) {
+ if (vid) return vid;
+ if (arity == 0)
+ vid = R->get_local(g);
+ else
+ vid = R->get_local(g,of);
+ return vid;
+ }
+ omega::Variable_ID id(omega::Relation &R) {
+ if (vid) return vid;
+ if (arity == 0)
+ vid = R.get_local(g);
+ else
+ vid = R.get_local(g,of);
+ return vid;
+ }
+ omega::Free_Var_Decl *g;
+ int arity;
+ int pos;
+ omega::Argument_Tuple of;
+ Variable_Ref(char *s, int _arity, omega::Argument_Tuple _of);
+ Variable_Ref(char *s);
+ Variable_Ref();
+ ~Variable_Ref();
+};
+
+extern std::map<omega::Const_String, Variable_Ref *> functionOfInput;
+extern std::map<omega::Const_String, Variable_Ref *> functionOfOutput;
+
+class Declaration_Site {
+public:
+ Declaration_Site();
+ Declaration_Site(std::set<char *> *v);
+ virtual Variable_Ref *extend(char *s);
+ virtual Variable_Ref *extend(char *s, omega::Argument_Tuple, int);
+ virtual ~Declaration_Site();
+
+ Variable_Ref *extend();
+ void print() {
+ for (std::set<Variable_Ref *>::iterator i = declarations.begin(); ;) {
+ printf("%s", static_cast<const char *>((*i)->name));
+ i++;
+ if (i != declarations.end())
+ printf(",");
+ else
+ break;
+ }
+ }
+
+ Declaration_Site *previous;
+ std::set<Variable_Ref *> declarations;
+};
+
+class Global_Declaration_Site: public Declaration_Site {
+public:
+ virtual Variable_Ref *extend(char *s);
+ virtual Variable_Ref *extend() {
+ return Declaration_Site::extend();
+ }
+ virtual Variable_Ref *extend(char *s, omega::Argument_Tuple in_of, int in_arity) {
+ return Declaration_Site::extend(s,in_of,in_arity);
+ }
+ void extend_both_tuples(char *s, int arity);
+ virtual ~Global_Declaration_Site();
+};
+
+extern Declaration_Site *current_Declaration_Site;
+
+inline void popScope() {
+ assert(current_Declaration_Site);
+ current_Declaration_Site = current_Declaration_Site->previous;
+}
+
+Variable_Ref *lookupScalar(char *s);
+Declaration_Site * defined (char *);
+
+class Exp {
+public:
+ Exp(omega::coef_t c);
+ Exp(Variable_Ref *v);
+ friend Exp *multiply (omega::coef_t c, Exp *x);
+ friend Exp *multiply (Exp *x, Exp *y);
+ friend Exp *negate (Exp *x);
+ friend Exp *add (Exp *x, Exp *y);
+ friend Exp *subtract (Exp *x, Exp *y);
+ std::map<Variable_Ref *, omega::coef_t> coefs;
+ omega::coef_t constantTerm;
+protected:
+ void addTerm(omega::coef_t coef, omega::Variable_ID v);
+};
+
+
+typedef struct {
+ Exp *e;
+ int step;
+} strideConstraint;
+
+
+class AST;
+class AST_constraints;
+
+
+class Tuple_Part {
+public:
+ Variable_Ref *from,*to;
+ Tuple_Part(Variable_Ref *f, Variable_Ref *t)
+ { from = f; to = t; }
+ Tuple_Part(Variable_Ref *f)
+ { from = f; to = 0; }
+ Tuple_Part()
+ { from = 0; to = 0; }
+};
+
+
+class AST {
+public:
+ virtual void install(omega::Formula *F) = 0;
+ virtual void print() = 0;
+ virtual ~AST() {}
+};
+
+
+class AST_And: public AST {
+public:
+ AST_And(AST *l, AST *r) { left = l; right = r; }
+ ~AST_And() { delete left; delete right; }
+
+ virtual void install(omega::Formula *F);
+
+ virtual void print() {
+ printf("(");
+ left->print();
+ printf(" && ");
+ right->print();
+ printf(")");
+ }
+
+ AST *left,*right;
+};
+
+
+class AST_Or: public AST {
+public:
+ AST_Or(AST *l, AST *r) { left = l; right = r; }
+ ~AST_Or() { delete left; delete right; }
+
+ virtual void install(omega::Formula *F);
+
+ virtual void print() {
+ printf("(");
+ left->print();
+ printf(" || ");
+ right->print();
+ printf(")");
+ }
+
+
+ AST *left, *right;
+};
+
+
+class AST_Not: public AST {
+public:
+ AST_Not(AST *c) { child = c; }
+ ~AST_Not() { delete child; }
+
+ virtual void install(omega::Formula *F);
+
+ virtual void print() {
+ printf("(!");
+ child->print();
+ printf(")");
+ }
+
+ AST *child;
+};
+
+
+class AST_declare: public AST {
+public:
+ virtual void install(omega::Formula *F) = 0;
+
+ virtual void print() {
+ printf("(");
+ declaredVariables->print();
+ printf(" : ");
+ child->print();
+ printf(")");
+ }
+
+ Declaration_Site *declaredVariables;
+ AST *child;
+};
+
+
+class AST_exists: public AST_declare {
+public:
+ AST_exists(Declaration_Site *dV, AST *c) {declaredVariables = dV, child = c;}
+ ~AST_exists() { delete child; delete declaredVariables; }
+
+ virtual void install(omega::Formula *F);
+
+ virtual void print() {
+ printf("exists ");
+ AST_declare::print();
+ }
+};
+
+
+class AST_forall: public AST_declare {
+public:
+ AST_forall(Declaration_Site *dV, AST *c) {declaredVariables = dV, child = c; }
+ ~AST_forall() { delete child; delete declaredVariables; }
+
+ virtual void install(omega::Formula *F);
+
+ virtual void print() {
+ printf("forall ");
+ AST_declare::print();
+ }
+};
+
+
+
+class AST_constraints: public AST {
+public:
+ AST_constraints(std::set<Exp *> *f, Rel_Op r, AST_constraints *o);
+ AST_constraints(std::set<Exp *> *f, Rel_Op r, std::set<Exp *> *s);
+ AST_constraints(std::set<Exp *> *f);
+ ~AST_constraints();
+
+ virtual void install(omega::Formula *F);
+
+ virtual void print();
+
+ AST_constraints *others;
+ std::set<Exp *> *first;
+ Rel_Op rel_op;
+};
+
+void install_stride(omega::F_And *F, strideConstraint *c);
+void install_eq(omega::F_And *F, Exp *e1, Exp *e2);
+void install_geq(omega::F_And *F, Exp *e1, Exp *e2);
+void install_gt(omega::F_And *F, Exp *e1, Exp *e2);
+void install_neq(omega::F_And *F, Exp *e1, Exp *e2);
+
+
+
+class tupleDescriptor {
+public:
+ tupleDescriptor() { size = 0; }
+ void extend();
+ void extend(Exp * e);
+ void extend(Exp * lb, Exp *ub);
+ void extend(Exp * lb, Exp *ub, omega::coef_t stride);
+ void extend(char * s, Exp *e);
+ void extend(char * s);
+ void extend(char * s, omega::Argument_Tuple, int);
+
+ int size;
+ std::vector<Variable_Ref *> vars;
+ std::set<Exp *> eq_constraints;
+ std::set<Exp *> geq_constraints;
+ std::set<strideConstraint *> stride_constraints;
+ ~tupleDescriptor() {
+ for (std::set<Exp *>::iterator i = eq_constraints.begin(); i != eq_constraints.end(); i++)
+ delete *i;
+ for (std::set<Exp *>::iterator i = geq_constraints.begin(); i != geq_constraints.end(); i++)
+ delete *i;
+ for (std::set<strideConstraint *>::iterator i = stride_constraints.begin(); i != stride_constraints.end(); i++) {
+ delete (*i)->e;
+ delete *i;
+ }
+ }
+};
+
+extern Global_Declaration_Site *globalDecls;
+extern Declaration_Site *relationDecl;
+extern tupleDescriptor *currentTupleDescriptor;
+
+void resetGlobals();
+
+
+// Used to parse a list of paired relations for code generation commands
+// class RelTuplePair {
+// public:
+// RelTuplePair() : ispaces(0), mappings(0) {}
+// omega::Tuple<omega::Relation> ispaces;
+// omega::Tuple<omega::Relation> mappings;
+// };
+
+#endif
diff --git a/omegalib/omegacalc/include/omega_calc/PT-omega.c b/omegalib/omegacalc/include/omega_calc/PT-omega.c
new file mode 100644
index 0000000..ad6b979
--- /dev/null
+++ b/omegalib/omegacalc/include/omega_calc/PT-omega.c
@@ -0,0 +1,81 @@
+#undef DONT_INCLUDE_TEMPLATE_CODE
+
+#include <basic/bool.h>
+#include <basic/util.h>
+#include <basic/List.h>
+#include <basic/SimpleList.h>
+#include <basic/Bag.h>
+#include <basic/Map.h>
+#include <basic/Tuple.h>
+#include <basic/Section.h>
+#include <basic/Exit.h>
+#include <basic/Dynamic_Array.h>
+#include <omega.h>
+#include <omega/AST.h>
+
+template int max(int, int);
+template int min(int, int);
+template unsigned int min(unsigned int, unsigned int);
+template void set_max(int&,int);
+template void set_min(int&,int);
+template void swap(int&,int&);
+template void swap(short&,short&);
+template void swap(signed char&,signed char&);
+template Relation copy(const Relation &);
+
+instantiate_Set(int);
+instantiate_Set(Global_Var_ID);
+instantiate_Set(Variable_ID);
+
+instantiate_List(int);
+instantiate_List(exit_func);
+instantiate_List(Formula *);
+instantiate_List(Conjunct *);
+instantiate_List(DNF *);
+instantiate_List(Relation *);
+instantiate_Simple_List(Relation);
+
+typedef Tuple<Relation> RelationTuple;
+instantiate_Tuple(bool);
+instantiate_Tuple(int);
+instantiate_Tuple(coef_t);
+instantiate_Tuple(char *);
+instantiate_Tuple(Const_String);
+instantiate_Tuple(Conjunct *);
+instantiate_Tuple(Relation);
+instantiate_Tuple(RelationTuple);
+instantiate_Tuple(Variable_ID);
+instantiate_Tuple(Free_Var_Decl *);
+instantiate_Tuple(std::string);
+instantiate_Tuple(GEQ_Handle);
+
+instantiate_Section(Variable_ID);
+
+instantiate_Generator(Variable_Info);
+instantiate_Generator(GEQ_Handle);
+instantiate_Generator(EQ_Handle);
+instantiate_Generator(Constraint_Handle);
+instantiate_Generator(Sub_Handle);
+
+instantiate_Map(Variable_ID,int);
+instantiate_Map(Global_Var_ID, Variable_ID);
+instantiate_Map(GEQ_Handle,Variable_ID);
+instantiate_Map(EQ_Handle,Variable_ID);
+instantiate_Map(Variable_ID,Set<Variable_ID>);
+instantiate_Map(Const_String, Relation *);
+
+instantiate_Dynamic_Array1(Coef_Var_Decl *);
+instantiate_Dynamic_Array1(Relation);
+instantiate_Dynamic_Array2(Relation);
+
+
+/* Stuff required by calculator: */
+instantiate_Bag(Exp *);
+instantiate_Bag(strideConstraint *);
+instantiate_Bag(Variable_Ref *);
+instantiate_Bag(char *);
+instantiate_Map(Variable_Ref *, int);
+instantiate_Map(Variable_Ref *, Variable_Ref *);
+instantiate_Map(Const_String, Variable_Ref *);
+instantiate_Set(Free_Var_Decl *);
+instantiate_Tuple(Variable_Ref *);
diff --git a/omegalib/omegacalc/include/omega_calc/myflex.h b/omegalib/omegacalc/include/omega_calc/myflex.h
new file mode 100755
index 0000000..d472e51
--- /dev/null
+++ b/omegalib/omegacalc/include/omega_calc/myflex.h
@@ -0,0 +1,27 @@
+#ifndef _MYFLEX_H
+#define _MYFLEX_H
+
+#ifndef yyFlexLexerOnce
+#include <FlexLexer.h>
+#endif
+#include <iostream>
+#include <string>
+#include <vector>
+
+class myFlexLexer: public yyFlexLexer {
+protected:
+ std::string cur_line;
+ int cur_pos;
+ std::vector<std::string> history;
+ int first_history_pos;
+ int last_history_pos;
+ std::vector<std::string> key_seqs;
+
+public:
+ myFlexLexer(std::istream *arg_yyin = NULL, std::ostream *arg_yyout = NULL);
+ ~myFlexLexer() {}
+protected:
+ int LexerInput(char *buf, int max_size);
+};
+
+#endif