1 files changed, 230 insertions, 0 deletions
diff --git a/lib/omega/include/omega/pres_var.h b/lib/omega/include/omega/pres_var.h
new file mode 100644
index 0000000..bf60dcb
--- /dev/null
+++ b/lib/omega/include/omega/pres_var.h
@@ -0,0 +1,230 @@
+#if ! defined _pres_var_h
+#define _pres_var_h 1
+
+#include <omega/pres_gen.h>
+#include <map>
+
+namespace omega {
+
+//
+// Variable declaration.
+// Variables are free or quantified.
+// Free variables are classified as input, output and global.
+// Quantified variables are classified as forall, exists and wildcard.
+// All global variables are functions symbols of (possibly 0) arguments
+// Local variables that correspond to >0-ary functions are identified
+//   as functions of a prefix of the input, output, or both tuples
+//
+// 
+// typedef enum {Input_Var, Output_Var, Set_Var,
+//               Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind;
+
+typedef enum {Free_Var, Coef_Var, Bomega_Var} Global_Kind;
+
+// NOW IN PRES_GEN.H, as its used as an argument and can't
+// be forward declared:
+// typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2,
+//     Set_Tuple = Input_Tuple } Argument_Tuple;
+// Only Input, Output, and Set can be passed to get_local,
+// but the values 0 and 3 are also used internally.
+
+
+class Var_Decl {
+public:
+  inline Var_Kind    kind() { return var_kind; }
+  int         get_position();
+  Global_Var_ID      get_global_var();
+  Argument_Tuple     function_of();  // valid iff kind() == Global_var
+
+  Const_String base_name;
+  void name_variable(char *newname);
+
+  // The following should be used with care, as they are only valid
+  // after setup_names has been used on the relation containing this
+  // variable.
+  std::string name();
+  const char* char_name();
+  void set_kind(Var_Kind v) { var_kind = v; }
+
+  // Operation to allow the remap field to be used for
+  // union-find operations on variables.
+  // Be sure to reset the remap fields afterward
+  void         UF_union(Variable_ID v);
+  Variable_ID  UF_owner();
+
+private:
+  Var_Decl(Const_String name, Var_Kind vkind, int pos);
+  Var_Decl(Var_Kind vkind, int pos);
+  Var_Decl(Variable_ID v);
+  Var_Decl(Const_String name, Global_Var_ID v);
+  Var_Decl(Const_String name, Global_Var_ID v, Argument_Tuple function_of);
+
+  friend class F_Declaration;    // creates local variables
+  friend class Global_Var_Decl;  // its constructors create Var_Decls.
+
+  friend class Global_Input_Output_Tuple;
+  friend void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl);
+
+private:
+  int  instance;
+  void setup_name();
+
+  // these set up the names
+  friend class Rel_Body;
+//  friend class F_Declaration; already a friend
+
+private:
+  Variable_ID   remap;          // pointer to new copy of this node
+
+  // lots of things need to get at "remap" - lots of relation ops,
+  // and functions that move UFS's around:
+  //     dnf::make_level_carried_to and Conjunct::move_UFS_to_input()
+  // Also of course Conjunct::remap and push_exists
+  friend_rel_ops;
+  friend class DNF;
+  friend class Conjunct;
+
+  // this prints remap to the debugging output
+  friend void print_var_addrs(std::string &s, Variable_ID v);
+
+  friend void reset_remap_field(Variable_ID v);
+  friend void reset_remap_field(Sequence<Variable_ID> &S);
+  friend void reset_remap_field(Sequence<Variable_ID> &S, int var_no);
+  friend void reset_remap_field(Variable_ID_Tuple &S);
+  friend void reset_remap_field(Variable_ID_Tuple &S, int var_no);
+
+private:
+
+  Var_Kind      var_kind;
+  int           position; // only for Input_Var, Output_Var
+  Global_Var_ID global_var;     // only for Global_Var
+  Argument_Tuple of;  // only for Global_Var
+};
+
+bool rm_variable(Variable_ID_Tuple &vl, Variable_ID v);
+void reset_remap_field(Sequence<Variable_ID> &S);
+void reset_remap_field(Sequence<Variable_ID> &S, int var_no);
+void reset_remap_field(Variable_ID v);
+void reset_remap_field(Variable_ID_Tuple &S);
+void reset_remap_field(Variable_ID_Tuple &S, int var_no);
+
+class Global_Input_Output_Tuple: public Tuple<Variable_ID> {
+public:
+  Global_Input_Output_Tuple(Var_Kind in_my_kind, int init=-1);
+  ~Global_Input_Output_Tuple();
+  virtual Variable_ID &operator[](int index);
+  virtual const Variable_ID &operator[](int index) const;
+private:
+  Var_Kind my_kind;
+  static const int initial_allocation;
+};
+
+extern Global_Input_Output_Tuple input_vars;
+extern Global_Input_Output_Tuple output_vars;
+// This allows the user to refer to set_vars to query sets, w/o knowing
+// they are really inputs.
+extern Global_Input_Output_Tuple &set_vars;
+
+Variable_ID input_var(int nth);
+Variable_ID output_var(int nth);
+Variable_ID set_var(int nth);
+
+
+
+//
+// Global_Var_ID uniquely identifies global var-s through the whole program.
+// Global_Var_Decl is an ADT with the following operations:
+// - create global variable,
+// - find the arity of the variable, (default = 0, for symbolic consts)
+// - get the name of global variable, 
+// - tell if two variables are the same (if they are the same object)
+//
+
+class Global_Var_Decl {
+public:
+  Global_Var_Decl(Const_String baseName);
+
+  virtual Const_String base_name() const
+  {
+    return loc_rep1.base_name;
+  }
+
+  virtual void set_base_name(Const_String newName)
+  {
+    loc_rep1.base_name = newName;
+    loc_rep2.base_name = newName;
+  }
+
+  virtual int arity() const
+  {
+    return 0;   // default compatible with old symbolic constant stuff
+  }
+
+  virtual Omega_Var *really_omega_var();  // until we get RTTI in C++
+  virtual Coef_Var_Decl *really_coef_var();  // until we get RTTI in C++
+  virtual Global_Kind kind() const;
+
+private:
+
+  friend class Rel_Body;  // Rel_Body::get_local calls this get_local
+
+  Variable_ID get_local()
+  {
+    assert(arity() == 0);
+    return &loc_rep1;
+  }
+  Variable_ID get_local(Argument_Tuple of)
+  {
+    assert(arity() == 0 || of == Input_Tuple || of == Output_Tuple);
+    return ((arity() == 0 || of == Input_Tuple) ? &loc_rep1 : &loc_rep2);
+  }
+
+  // local representative, there is just 1 for every 0-ary global variable
+  Var_Decl loc_rep1; // arity == 0, or arity > 0 and of == In
+  Var_Decl loc_rep2; // arity > 0 and of == Out
+
+public:
+//    friend class Rel_Body;  // Rel_Body::setup_names sets instance
+  friend class Var_Decl;
+  int instance;
+};
+
+
+class Coef_Var_Decl : public Global_Var_Decl {
+public:
+  Coef_Var_Decl(int id, int var);
+  int stmt() const;
+  int var() const;
+  virtual Global_Kind kind() const;
+  virtual Coef_Var_Decl *really_coef_var();  // until we get RTTI in C++
+
+private:
+  int i, v;
+};
+
+
+
+//
+// Test subclass for Global_Var: named global variable
+//
+class Free_Var_Decl : public Global_Var_Decl {
+public:
+  Free_Var_Decl(Const_String name);
+  Free_Var_Decl(Const_String name, int arity);
+  int arity() const;
+  virtual Global_Kind kind() const;
+
+private:
+  int _arity;
+};
+
+
+/* === implementation functions === */
+void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl);
+void free_var_decls(Variable_ID_Tuple &vl);
+
+extern int wildCardInstanceNumber;
+
+} // namespace
+
+#endif