diff options
Diffstat (limited to 'omegalib/omegacalc/include/omega_calc')
-rw-r--r-- | omegalib/omegacalc/include/omega_calc/AST.h | 310 | ||||
-rw-r--r-- | omegalib/omegacalc/include/omega_calc/PT-omega.c | 81 | ||||
-rwxr-xr-x | omegalib/omegacalc/include/omega_calc/myflex.h | 27 |
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 |