remove include & rename

1 files changed, 310 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