cmake build

26 files changed, 2922 insertions, 0 deletions

diff --git a/omegalib/omega_lib/include/omega.h b/omegalib/omega_lib/include/omega.h
new file mode 100644
index 0000000..8aa2c08
--- /dev/null
+++ b/omegalib/omega_lib/include/omega.h
@@ -0,0 +1,71 @@
+/*********************************************************************
+ Old license information from the Omega Project, updated one can be
+ found in LICENSE file. 
+
+    Copyright (C) 1994-1996 by the Omega Project
+    All rights reserved.
+
+    NOTICE:  This software is provided ``as is'', without any
+    warranty, including any implied warranty for merchantability or
+    fitness for a particular purpose.  Under no circumstances shall
+    the Omega Project or its agents be liable for any use of, misuse
+    of, or inability to use this software, including incidental and
+    consequential damages.
+
+    License is hereby given to use, modify, and redistribute this
+    software, in whole or in part, for any purpose, commercial or
+    non-commercial, provided that the user agrees to the terms of this
+    copyright notice, including disclaimer of warranty, and provided
+    that this copyright notice, including disclaimer of warranty, is
+    preserved in the source code and documentation of anything derived
+    from this software.  Any redistributor of this software or
+    anything derived from this software assumes responsibility for
+    ensuring that any parties to whom such a redistribution is made
+    are fully aware of the terms of this license and disclaimer.
+
+    The Omega project can be contacted at omega@cs.umd.edu
+    or http://www.cs.umd.edu/projects/omega
+*********************************************************************/
+
+#ifndef Already_Included_Omega
+#define Already_Included_Omega
+
+/*
+ * The presburger interface is divided into the following parts.
+ * These parts are all included together, but are in separate
+ * files to keep things organized a bit.
+ *
+ * In many files, you can include just some of the following,
+ * specifically: if you are building a presburger tree, just
+ * include "pres_tree.h"; if you are querying it, include
+ * "pres_dnf.d" and "pres_conj.h"; if you are doing relational
+ * operations, include "Relation.h"
+ *
+ * Most of the function definitions are in the .c files with
+ * the same name as the .h that declares them, except:
+ *   the remap and push_exists functions are in pres_var.c
+ *   the DNFize functions are in pres_dnf.c
+ *   the functions involving printing are in pres_print.c
+ *   the beautify functions are in pres_beaut.c
+ *   the rearrange functions are in pres_rear.c
+ *   the compression functions are in pres_cmpr.c
+ */
+
+#include <omega/omega_core/debugging.h>
+#include <omega/pres_var.h>
+#include <omega/pres_cnstr.h>
+#include <omega/pres_subs.h>
+#include <omega/pres_form.h>
+#include <omega/pres_logic.h>
+#include <omega/pres_decl.h>
+#include <omega/pres_quant.h>
+#include <omega/pres_conj.h>
+#include <omega/pres_cmpr.h>
+#include <omega/Relation.h>
+
+#include <omega/Rel_map.h>
+#include <omega/farkas.h>
+#include <omega/hull.h>
+#include <omega/closure.h>
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/RelBody.h b/omegalib/omega_lib/include/omega/RelBody.h
new file mode 100644
index 0000000..3c11702
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/RelBody.h
@@ -0,0 +1,165 @@
+#if ! defined _RelBody_h
+#define _RelBody_h 1
+
+#include <omega/pres_form.h>
+#include <omega/pres_dnf.h>
+
+namespace omega {
+
+typedef enum {under_construction, compressed, uncompressed} Rel_Body_Status;
+typedef unsigned char Rel_Unknown_Uses;
+const Rel_Unknown_Uses no_u = 1;
+const Rel_Unknown_Uses and_u = 2;
+const Rel_Unknown_Uses or_u = 4;
+
+//
+// Relation body.
+// Body and representative are separated to do reference counting.
+//
+
+class Rel_Body : public Formula {
+public:
+  bool is_null() const;
+
+  inline Node_Type node_type() { return Op_Relation; }
+
+  inline bool is_set() const { return number_output == 0; }
+  int n_inp() const;
+  int n_out() const;
+  int n_set() const;
+
+  inline Variable_ID_Tuple *global_decls() { return  &Symbolic; }
+  int max_ufs_arity();
+  int max_shared_ufs_arity();
+  int max_ufs_arity_of_set();
+  int max_ufs_arity_of_in();
+  int max_ufs_arity_of_out();
+
+  Variable_ID input_var(int nth);
+  Variable_ID output_var(int nth);
+  Variable_ID set_var(int nth);
+  Variable_ID get_local(const Variable_ID v);
+  Variable_ID get_local(const Global_Var_ID G);
+  Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of);
+  bool        has_local(const Global_Var_ID G);
+  bool        has_local(const Global_Var_ID G, Argument_Tuple of);
+  void        name_input_var(int, Const_String);
+  void        name_output_var(int, Const_String);
+  void        name_set_var(int, Const_String);
+
+  F_And      *and_with_and();
+  EQ_Handle   and_with_EQ();
+  EQ_Handle   and_with_EQ(const Constraint_Handle &c);
+  GEQ_Handle  and_with_GEQ();
+  GEQ_Handle  and_with_GEQ(const Constraint_Handle &c);
+
+  void   print();
+  void   print(FILE *output_file) { print(output_file, true); }
+  void   print(FILE *output_file, bool printSym);
+  std::string print_variables_to_string(bool printSym);
+  void   print_with_subs(FILE *output_file, bool printSym, bool newline);
+  void   print_with_subs();
+  std::string print_with_subs_to_string(bool printSym, bool newline);
+  std::string print_outputs_with_subs_to_string();
+  std::string print_outputs_with_subs_to_string(int i);
+  std::string print_formula_to_string();
+  void   prefix_print();
+  void   prefix_print(FILE *output_file, int debug = 1);
+
+  bool is_satisfiable();
+  bool is_lower_bound_satisfiable();
+  bool is_upper_bound_satisfiable();
+  bool is_obvious_tautology();
+  bool is_definite_tautology();
+  bool is_unknown();
+  DNF*    query_DNF();
+  DNF*    query_DNF(int rdt_conjs, int rdt_constrs);
+  void    simplify(int rdt_conjs = 0, int rdt_constrs = 0);  
+  void    finalize();
+  inline bool is_finalized() { return finalized; }
+  inline bool is_shared()    { return ref_count > 1; }
+
+  void query_difference(Variable_ID v1, Variable_ID v2,
+                        coef_t &lowerBound, coef_t &upperBound,
+                        bool &quaranteed);
+  void query_variable_bounds(Variable_ID, coef_t &lowerBound, coef_t &upperBound);
+  coef_t query_variable_mod(Variable_ID v, coef_t factor);
+
+  Relation extract_dnf_by_carried_level(int level, int direction);
+  void make_level_carried_to(int level);
+
+  // these are only public to allow the creation of "null_rel"
+  Rel_Body();
+  ~Rel_Body();
+  void setup_names();
+
+private:
+
+  // These are manipulated primarily as parts of Relations
+  friend class Relation;
+  friend_rel_ops;
+
+  friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel);
+
+  Rel_Unknown_Uses unknown_uses();
+
+  inline bool is_simplified() const { return (simplified_DNF!=NULL && get_children().empty()); }
+  bool is_compressed();
+  Conjunct *rm_first_conjunct();
+  Conjunct *single_conjunct();
+  bool has_single_conjunct();
+
+  void beautify();
+  void rearrange();
+
+  friend class EQ_Handle;  // these set up names for printing
+  friend class GEQ_Handle; // and check if simplified
+  friend class Constraint_Handle;  // and update coefficients
+
+  void compress();
+  void uncompress();
+
+  void interpret_unknown_as_true();
+  void interpret_unknown_as_false();
+ 
+  Rel_Body(int n_input, int n_output);
+  /* Rel_Body(Rel_Body *r); */
+  Rel_Body(Rel_Body *r, Conjunct *c);
+  Rel_Body &operator=(Rel_Body &r);
+  Rel_Body *clone();
+
+  inline Formula *formula()    { return children().front(); }
+  inline Formula *rm_formula() { return children().remove_front(); }
+  bool can_add_child();
+    
+  void reverse_leading_dir_info();
+  void invalidate_leading_info(int changed = -1) { Formula::invalidate_leading_info(changed); }
+  void enforce_leading_info(int guaranteed, int possible, int dir) { Formula::enforce_leading_info(guaranteed, possible, dir); }
+  // re-declare this so that Relation (a friend) can call it
+
+  DNF* DNFize();
+  void DNF_to_formula();
+    
+  Conjunct *find_available_conjunct();
+  F_And *find_available_And();
+
+
+/* === data === */
+private:
+
+  int ref_count;
+  Rel_Body_Status status;
+
+  int number_input, number_output;
+  Tuple<Const_String> In_Names, Out_Names;
+  Variable_ID_Tuple Symbolic;
+
+  DNF* simplified_DNF;
+  short r_conjs;  // are redundant conjuncts eliminated?
+  bool finalized;
+  bool _is_set;
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/Rel_map.h b/omegalib/omega_lib/include/omega/Rel_map.h
new file mode 100644
index 0000000..5641cb3
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/Rel_map.h
@@ -0,0 +1,161 @@
+#if ! defined _Rel_map_h
+#define _Rel_map_h 1
+
+#include <omega/pres_gen.h>
+#include <omega/pres_var.h>
+
+namespace omega {
+
+//
+// Mapping for relations
+// When a relation operation needs to re-arrange the variables,
+//  it describes the re-arragement with a mapping, and then calls
+//  align to re-arrange them.
+//
+// In a mapping, map_in (map_out/map_set) gives the new type and
+//  position of each of the old input (output/set) variables.
+// For variables being mapped to Input, Output, or Set variables,
+//  the position is the new position in the tuple.
+// For variables being mapped to Exists_Var, Forall_Var, or
+//  Wildcard_Var, the positions can be used to map multiple
+//  variables to the same quantified variable, by providing
+//  the same position.  Each variable with a negative position
+//  is given a unique quantified variable that is NOT listed
+//  in the seen_exists_ids list.
+// I'm not sure what the positions mean for Global_Vars - perhaps
+//  they are ignored?
+//
+// Currently, align seems to support only mapping to Set, Input,
+//  Output, and Exists vars.
+//
+
+class Mapping {
+public:
+  inline  Mapping(int no_in, int no_out): n_input(no_in), n_output(no_out) {}
+  inline  Mapping(int no_set): n_input(no_set), n_output(0){}
+  inline  Mapping(const Mapping &m): n_input(m.n_input), n_output(m.n_output) {
+    int i;
+    for(i=1; i<=n_input; i++) map_in_kind[i] = m.map_in_kind[i];
+    for(i=1; i<=n_input; i++) map_in_pos[i]  = m.map_in_pos[i];
+    for(i=1; i<=n_output;i++) map_out_kind[i] = m.map_out_kind[i];
+    for(i=1; i<=n_output;i++) map_out_pos[i] = m.map_out_pos[i];
+  }
+
+  inline void set_map (Var_Kind in_kind, int pos, Var_Kind type, int map) {
+    if(in_kind==Input_Var)
+      set_map_in(pos,type,map);
+    else if(in_kind==Set_Var)
+      set_map_in(pos,type,map);
+    else if(in_kind==Output_Var)
+      set_map_out(pos,type,map);
+    else
+      assert(0);
+  }
+
+  inline void set_map_in (int pos, Var_Kind type, int map) {
+    assert(pos>=1 && pos<=n_input);
+    map_in_kind[pos] = type;
+    map_in_pos[pos] = map;
+  }
+  inline void set_map_set (int pos, Var_Kind type, int map) {
+    assert(pos>=1 && pos<=n_input);
+    map_in_kind[pos] = type;
+    map_in_pos[pos] = map;
+  }
+
+  inline void set_map_out(int pos, Var_Kind type, int map) {
+    assert(pos>=1 && pos<=n_output);
+    map_out_kind[pos] = type;
+    map_out_pos[pos] = map;
+  }
+
+  inline Var_Kind get_map_in_kind(int pos)  const {
+    assert(pos>=1 && pos<=n_input);
+    return map_in_kind[pos];
+  }
+
+  inline int get_map_in_pos(int pos)  const {
+    assert(pos>=1 && pos<=n_input);
+    return map_in_pos[pos];
+  }
+
+  inline Var_Kind get_map_out_kind(int pos)  const {
+    assert(pos>=1 && pos<=n_output);
+    return map_out_kind[pos];
+  }
+
+  inline int get_map_out_pos(int pos)  const {
+    assert(pos>=1 && pos<=n_output);
+    return map_out_pos[pos];
+  }
+
+  inline int n_in()  const { return n_input;  }
+  inline int n_out() const { return n_output; }
+
+  // If a tuple as a whole becomes the new Input or Output tuple,
+  //  return the Tuple of they will become (Input, Output)
+  // Return Unknown_Tuple otherwise
+
+  inline Argument_Tuple get_tuple_fate(Argument_Tuple t, int prefix = -1) const {
+    return   t== Input_Tuple ?  get_input_fate(prefix) :
+      (t==Output_Tuple ? get_output_fate(prefix) : Unknown_Tuple); }
+
+  inline Argument_Tuple get_set_fate(int prefix = -1) const {
+    return get_input_fate(prefix); }
+
+  inline Argument_Tuple get_input_fate(int prefix = -1) const {
+    if (prefix < 0) prefix = n_input;
+    assert(n_input >= prefix);
+    if (n_input < prefix)
+      return Unknown_Tuple;
+    Var_Kind vf = map_in_kind[1];
+    for (int i = 1; i<=prefix; i++)
+      if (map_in_pos[i]!=i || map_in_kind[i]!=vf)
+        return Unknown_Tuple;
+
+    return vf == Input_Var  ? Input_Tuple
+      : vf == Set_Var    ? Set_Tuple
+      : vf == Output_Var ? Output_Tuple
+      : Unknown_Tuple;
+  }
+  
+  inline Argument_Tuple get_output_fate(int prefix = -1) const {
+    if (prefix < 0) prefix = n_output;
+    assert(n_output >= prefix);
+    if (n_output < 1)
+      return Unknown_Tuple;
+    Var_Kind vf = map_out_kind[1];
+    for (int i = 1; i<=prefix; i++)
+      if (map_out_pos[i]!=i || map_out_kind[i]!=vf)
+        return Unknown_Tuple;
+    return vf == Input_Var  ? Input_Tuple
+      : vf == Set_Var    ? Set_Tuple
+      : vf == Output_Var ? Output_Tuple
+      : Unknown_Tuple;
+  }
+
+  inline static Mapping Identity(int inp, int outp) {
+    Mapping m(inp, outp); int i;
+    for(i=1; i<=m.n_input; i++) m.set_map(Input_Var, i, Input_Var, i);
+    for(i=1; i<=m.n_output;i++) m.set_map(Output_Var, i, Output_Var, i);
+    return m;
+  }
+
+  inline static Mapping Identity(int setvars) {
+    Mapping m(setvars); int i;
+    for(i=1; i<=setvars; i++) m.set_map(Set_Var, i, Set_Var, i);
+    return m;
+  }
+
+private:
+  int  n_input;
+  int  n_output;
+  Var_Kind map_in_kind[maxVars];
+  int      map_in_pos[maxVars];
+  Var_Kind map_out_kind[maxVars];
+  int      map_out_pos[maxVars];
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/Relation.h b/omegalib/omega_lib/include/omega/Relation.h
new file mode 100644
index 0000000..b41bef5
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/Relation.h
@@ -0,0 +1,299 @@
+#if ! defined _Relation_h
+#define _Relation_h 1
+
+#include <omega/RelBody.h>
+#include <omega/pres_cnstr.h>
+#include <iostream>
+#include <limits.h>
+
+namespace omega {
+
+//
+// Relation representative.
+// Body and representative are separated to do reference counting.
+//
+class Relation {
+public:
+  Relation();
+
+  Relation(int n_input, int n_output = 0);
+  Relation(const Relation &r);
+  Relation(const Relation &r, Conjunct *c);
+  Relation &operator=(const Relation &r);
+  Relation(Rel_Body &r, int foo);
+
+  static Relation Null();
+  static Relation Empty(const Relation &R);
+  static Relation True(const Relation &R);
+  static Relation True(int setvars);
+  static Relation True(int in, int out);
+  static Relation False(const Relation &R);
+  static Relation False(int setvars);
+  static Relation False(int in, int out);
+  static Relation Unknown(const Relation &R);
+  static Relation Unknown(int setvars);
+  static Relation Unknown(int in, int out);
+
+
+  bool is_null() const;
+
+  ~Relation();
+
+  inline F_Forall *add_forall()
+  { return rel_body->add_forall(); }
+  inline F_Exists *add_exists()
+  { return rel_body->add_exists(); }
+  inline F_And    *add_and()
+  { return rel_body->add_and(); }
+  inline F_And    *and_with()
+  { return rel_body->and_with(); }
+  inline F_Or     *add_or()
+  { return rel_body->add_or(); }
+  inline F_Not    *add_not()
+  { return rel_body->add_not(); }
+  inline void finalize()
+  { rel_body->finalize(); }
+  inline bool is_finalized() const
+  { return rel_body->finalized; }
+  inline bool is_set() const
+  { return rel_body->is_set();   }  
+  inline int n_inp() const
+  { return rel_body->n_inp(); }
+  inline int n_out() const
+  { return rel_body->n_out(); }
+  inline int n_set() const
+  { return rel_body->n_set(); }
+
+  inline const Variable_ID_Tuple *global_decls() const
+  { return rel_body->global_decls(); }
+  inline int max_ufs_arity() const
+  { return rel_body->max_ufs_arity(); }
+  inline int max_ufs_arity_of_in() const
+  { return rel_body->max_ufs_arity_of_in(); }
+  inline int max_ufs_arity_of_set() const
+  { return rel_body->max_ufs_arity_of_set(); }
+  inline int max_ufs_arity_of_out() const
+  { return rel_body->max_ufs_arity_of_out(); }
+  inline int max_shared_ufs_arity() const
+  { return rel_body->max_shared_ufs_arity(); }
+
+  inline Variable_ID input_var(int nth)
+  { return rel_body->input_var(nth); }
+  inline Variable_ID output_var(int nth)
+  { return rel_body->output_var(nth); }
+  inline Variable_ID set_var(int nth)
+  { return rel_body->set_var(nth); }
+  inline bool has_local(const Global_Var_ID G)
+  { return  rel_body->has_local(G); } 
+  inline bool has_local(const Global_Var_ID G, Argument_Tuple of)
+  { return  rel_body->has_local(G, of); } 
+  inline Variable_ID get_local(const Variable_ID v)
+  { return split()->get_local(v); }
+  inline Variable_ID get_local(const Global_Var_ID G)
+  { return split()->get_local(G); }
+  inline Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of)
+  { return split()->get_local(G, of); }
+
+  inline void        name_input_var(int nth, Const_String S)
+  { split()->name_input_var(nth, S); }
+  inline void        name_output_var(int nth, Const_String S)
+  { split()->name_output_var(nth, S); }
+  inline void        name_set_var(int nth, Const_String S)
+  { split()->name_set_var(nth, S); }
+
+
+  inline F_And      *and_with_and()
+  { return split()->and_with_and(); }
+  inline EQ_Handle   and_with_EQ()
+  { return split()->and_with_EQ(); }
+  inline EQ_Handle   and_with_EQ(const Constraint_Handle &c)
+  { return split()->and_with_EQ(c); }
+  inline GEQ_Handle  and_with_GEQ()
+  { return split()->and_with_GEQ(); }
+  inline GEQ_Handle  and_with_GEQ(const Constraint_Handle &c)
+  { return split()->and_with_GEQ(c); }
+
+  inline void print()
+  { rel_body->print(); }
+  inline void print(FILE *output_file)
+  { rel_body->print(output_file); }
+  inline void print_with_subs()
+  { rel_body->print_with_subs(); }
+  inline void print_with_subs(FILE *output_file, bool printSym=false, 
+                              bool newline=true)
+  { rel_body->print_with_subs(output_file, printSym, newline); }
+  inline std::string print_with_subs_to_string(bool printSym=false, 
+                                          bool newline=true)
+  { return rel_body->print_with_subs_to_string(printSym, newline); }
+  inline std::string print_outputs_with_subs_to_string()
+  { return rel_body->print_outputs_with_subs_to_string(); }
+  inline std::string print_outputs_with_subs_to_string(int i)
+  { return rel_body->print_outputs_with_subs_to_string(i); }
+  inline void prefix_print()
+  { rel_body->prefix_print(); }
+  inline void prefix_print(FILE *output_file, int debug = 1)
+  { rel_body->prefix_print(output_file, debug); }
+  inline std::string print_formula_to_string() {
+    return rel_body->print_formula_to_string();
+  }
+  void dimensions(int & ndim_all, int &ndim_domain);
+
+  inline bool is_lower_bound_satisfiable()
+  { return rel_body->is_lower_bound_satisfiable(); }
+  inline bool is_upper_bound_satisfiable()
+  { return rel_body->is_upper_bound_satisfiable(); }
+  inline bool is_satisfiable()
+  { return rel_body->is_satisfiable(); }
+
+  inline bool is_tautology()
+  { return rel_body->is_obvious_tautology(); }  // for compatibility
+  inline bool is_obvious_tautology()
+  { return rel_body->is_obvious_tautology(); }
+  inline bool is_definite_tautology()
+  { return rel_body->is_definite_tautology(); }
+
+  // return x s.t. forall conjuncts c, c has >= x leading 0s
+  // for set, return -1 (pass this in, in case there are no conjuncts
+  inline int    number_of_conjuncts()
+  { return rel_body->query_DNF()->length(); }
+
+  // return x s.t. forall conjuncts c, c has >= x leading 0s
+  // for set, return -1 (pass this in, in case there are no conjuncts
+  inline int    query_guaranteed_leading_0s()
+  { return rel_body->query_DNF()->query_guaranteed_leading_0s(this->is_set() ? -1 : 0); }
+
+  // return x s.t. forall conjuncts c, c has <= x leading 0s
+  // if no conjuncts return min of input and output tuple sizes, or -1 if relation is a set
+  inline int    query_possible_leading_0s()
+  { return rel_body->query_DNF()->query_possible_leading_0s(
+      this->is_set()? -1 : min(n_inp(),n_out())); }
+
+  // return +-1 according to sign of leading dir, or 0 if we don't know
+  inline int    query_leading_dir()
+  { return rel_body->query_DNF()->query_leading_dir(); }
+
+  inline DNF*    query_DNF()
+  { return rel_body->query_DNF(); }
+  inline DNF*    query_DNF(int rdt_conjs, int rdt_constrs)
+  { return rel_body->query_DNF(rdt_conjs, rdt_constrs); }
+  inline void    simplify(int rdt_conjs = 0, int rdt_constrs = 0)
+  { rel_body->simplify(rdt_conjs, rdt_constrs); }
+  inline bool is_simplified()
+  { return rel_body->is_simplified(); }
+  inline bool is_compressed() const
+  { return rel_body->is_compressed(); }
+  inline Conjunct *rm_first_conjunct()
+  { return rel_body->rm_first_conjunct(); }
+  inline Conjunct *single_conjunct()
+  { return rel_body->single_conjunct(); }
+  inline bool has_single_conjunct()
+  { return rel_body->has_single_conjunct(); }
+
+
+  void query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) {
+    rel_body->query_difference(v1, v2, lowerBound, upperBound, guaranteed);
+  }
+  void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) {
+    rel_body->query_variable_bounds(v,lowerBound,upperBound);
+  }
+  coef_t query_variable_mod(Variable_ID v, coef_t factor) {
+    assert(factor > 0);
+    return rel_body->query_variable_mod(v, factor);
+  }
+  int query_variable_mod(Variable_ID v, int factor) {
+    assert(sizeof(int) <= sizeof(coef_t));
+    coef_t result = rel_body->query_variable_mod(v, static_cast<coef_t>(factor));
+    if (result == posInfinity)
+      return INT_MAX;
+    else
+      return static_cast<int>(result);
+  }
+  
+
+  inline void make_level_carried_to(int level)
+  {
+    split()->make_level_carried_to(level);
+  }
+
+  inline Relation extract_dnf_by_carried_level(int level, int direction)
+  {
+    return split()->extract_dnf_by_carried_level(level, direction);
+  }
+
+  inline void compress()
+  {
+#if defined(INCLUDE_COMPRESSION)
+    split()->compress(); 
+#endif
+  }
+  void uncompress()
+  { rel_body->uncompress(); }
+
+  inline bool is_exact() const
+  { return !(rel_body->unknown_uses() & (and_u | or_u)) ; }
+  inline bool is_inexact() const
+  { return !is_exact(); }
+  inline bool is_unknown() const
+  { return rel_body->is_unknown(); }
+  inline Rel_Unknown_Uses unknown_uses() const
+  { return rel_body->unknown_uses(); }
+
+  void setup_names() {rel_body->setup_names();}
+  void copy_names(const Relation &r) {
+    copy_names(*r.rel_body);
+  };
+  void copy_names(Rel_Body &r);
+
+private:
+  // Functions that have to create sets from relations:
+  friend class Rel_Body;
+  friend_rel_ops;
+
+  
+  Rel_Body *split();
+
+  DNF* simplified_DNF() {
+    simplify();
+    return rel_body->simplified_DNF;
+  };
+
+  inline void invalidate_leading_info(int changed = -1)
+  { split()->invalidate_leading_info(changed); }
+  inline void enforce_leading_info(int guaranteed, int possible, int dir)
+  {
+    split()->enforce_leading_info(guaranteed, possible, dir);
+  }
+
+
+  void    makeSet();
+  void    markAsSet();
+  void    markAsRelation();
+
+  friend bool operator==(const Relation &, const Relation &);
+
+  void reverse_leading_dir_info()
+  { split()->reverse_leading_dir_info(); }
+  void interpret_unknown_as_true()
+  { split()->interpret_unknown_as_true(); }
+  void interpret_unknown_as_false()
+  { split()->interpret_unknown_as_false(); }
+
+
+  Rel_Body *rel_body;
+
+
+  friend Relation merge_rels(Tuple<Relation> &R, const Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > &mapping, const Tuple<bool> &inverse, Combine_Type ctype, int number_input, int number_output);
+};
+
+inline std::ostream & operator<<(std::ostream &o, Relation &R)
+{
+  return o << R.print_with_subs_to_string();
+}
+
+Relation copy(const Relation &r);
+
+} // namespace
+
+#include <omega/Relations.h>
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/Relations.h b/omegalib/omega_lib/include/omega/Relations.h
new file mode 100644
index 0000000..4fd81e6
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/Relations.h
@@ -0,0 +1,88 @@
+#if ! defined _Relations_h
+#define _Relations_h 1
+
+#include <map>
+#include <omega/Relation.h>
+
+namespace omega {
+
+// UPDATE friend_rel_ops IN pres_gen.h WHEN ADDING TO THIS LIST
+// REMEMBER TO TAKE OUT DEFAULT ARGUMENTS IN THAT FILE
+
+/* The following allows us to avoid warnings about passing 
+   temporaries as non-const references.  This is useful but 
+   has suddenly become illegal.  */
+Relation consume_and_regurgitate(NOT_CONST Relation &R);
+
+//
+// Operations over relations
+//
+Relation  Union(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+Relation  Intersection(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+Relation  Extend_Domain(NOT_CONST Relation &R);
+Relation  Extend_Domain(NOT_CONST Relation &R, int more);
+Relation  Extend_Range(NOT_CONST Relation &R);
+Relation  Extend_Range(NOT_CONST Relation &R, int more);
+Relation  Extend_Set(NOT_CONST Relation &R);
+Relation  Extend_Set(NOT_CONST Relation &R, int more);
+Relation  Restrict_Domain(NOT_CONST Relation &r1, NOT_CONST Relation &r2); // Takes set as 2nd
+Relation  Restrict_Range(NOT_CONST Relation &r1, NOT_CONST Relation &r2);  // Takes set as 2nd
+Relation  Domain(NOT_CONST Relation &r);      // Returns set
+Relation  Range(NOT_CONST Relation &r);       // Returns set
+Relation  Cross_Product(NOT_CONST Relation &A, NOT_CONST Relation &B);  // Takes two sets
+Relation  Inverse(NOT_CONST Relation &r);
+Relation  After(NOT_CONST Relation &r, int carried_by, int new_output,int dir=1);
+Relation  Deltas(NOT_CONST Relation &R);            // Returns set
+Relation  Deltas(NOT_CONST Relation &R, int eq_no); // Returns set
+Relation  DeltasToRelation(NOT_CONST Relation &R, int n_input, int n_output);
+Relation  Complement(NOT_CONST Relation &r);
+Relation  Project(NOT_CONST Relation &R, Global_Var_ID v);
+Relation  Project(NOT_CONST Relation &r, int pos, Var_Kind vkind);
+Relation  Project(NOT_CONST Relation &S, Variable_ID v);
+Relation  Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s);
+Relation  Project_Sym(NOT_CONST Relation &R);
+Relation  Project_On_Sym(NOT_CONST Relation &R,
+                         NOT_CONST Relation &context = Relation::Null());
+Relation  GistSingleConjunct(NOT_CONST Relation &R, NOT_CONST Relation &R2, int effort=0);
+Relation  Gist(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort=0);
+Relation  Difference(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+Relation  Approximate(NOT_CONST Relation &R, bool strides_allowed = false);
+Relation  Identity(int n_inp);
+Relation  Identity(NOT_CONST Relation &r);
+bool      Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+bool      Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+// May is the same as might, just another name
+bool      May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+bool      Is_Obvious_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2);
+Relation  Composition(NOT_CONST Relation &F, NOT_CONST Relation &G);
+bool      prepare_relations_for_composition(Relation &F, Relation &G);
+Relation  Join(NOT_CONST Relation &G, NOT_CONST Relation &F);
+Relation  EQs_to_GEQs(NOT_CONST Relation &, bool excludeStrides=false);
+Relation  Symbolic_Solution(NOT_CONST Relation &S); 
+Relation  Symbolic_Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T);
+Relation  Sample_Solution(NOT_CONST Relation &S);
+Relation  Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T);
+Relation  Upper_Bound(NOT_CONST Relation &r);
+Relation  Lower_Bound(NOT_CONST Relation &r);
+
+Relation merge_rels(Tuple<Relation> &R, const Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > &mapping, const Tuple<bool> &inverse, Combine_Type ctype, int number_input = -1, int number_output = -1);
+
+// The followings might retire in the futrue!!!
+void MapRel1(Relation &inputRel,
+             const Mapping &map,
+             Combine_Type ctype,
+             int number_input=-1, int number_output=-1,
+             bool invalidate_resulting_leading_info = true,
+             bool finalize = true);
+Relation MapAndCombineRel2(Relation &R1, Relation &R2, 
+                           const Mapping &mapping1, const Mapping &mapping2,
+                           Combine_Type ctype,
+                           int number_input=-1, int number_output=-1);
+void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe,
+           Formula *f, const Mapping &mapping, bool &newrIsSet,
+           List<int> &seen_exists,
+           Variable_ID_Tuple &seen_exists_ids);
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/closure.h b/omegalib/omega_lib/include/omega/closure.h
new file mode 100644
index 0000000..67088dd
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/closure.h
@@ -0,0 +1,31 @@
+#if ! defined _closure_h
+#define _closure_h
+
+#include <omega/Relation.h>
+
+namespace omega {
+
+Relation VennDiagramForm(
+                Tuple<Relation> &Rs,
+                NOT_CONST Relation &Context_In);
+Relation VennDiagramForm(
+                NOT_CONST Relation &R_In,
+                NOT_CONST Relation &Context_In = Relation::Null());
+
+// Given a Relation R, returns a relation deltas
+// that correspond to the ConicHull of the detlas of R
+Relation ConicClosure (NOT_CONST Relation &R);
+
+Relation  TransitiveClosure (NOT_CONST Relation &r, 
+                             int maxExpansion = 1,
+                             NOT_CONST Relation &IterationSpace=Relation::Null());
+
+/* Tomasz Klimek */
+Relation calculateTransitiveClosure(NOT_CONST Relation &r);
+
+/* Tomasz Klimek */
+Relation ApproxClosure(NOT_CONST Relation &r);
+
+} // namespace
+ 
+#endif
diff --git a/omegalib/omega_lib/include/omega/evac.h b/omegalib/omega_lib/include/omega/evac.h
new file mode 100644
index 0000000..a561f8c
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/evac.h
@@ -0,0 +1,15 @@
+#if defined STUDY_EVACUATIONS
+
+namespace omega {
+
+// study the evacuation from one side of C to the other for UFS's of
+// arity up to max_arity
+extern void study_evacuation(Conjunct *C, which_way dir, int max_arity);
+
+// study the evacuation from the joined C2's output and C1's input to
+// either of the other possible tuples
+extern void study_evacuation(Conjunct *C1, Conjunct *C2, int max_arity);
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/farkas.h b/omegalib/omega_lib/include/omega/farkas.h
new file mode 100644
index 0000000..e77ed66
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/farkas.h
@@ -0,0 +1,19 @@
+#ifndef Already_Included_Affine_Closure
+#define Already_Included_Affine_Closure
+
+#include <omega/Relation.h>
+
+namespace omega {
+
+enum Farkas_Type {Basic_Farkas, Decoupled_Farkas,
+                  Linear_Combination_Farkas, Positive_Combination_Farkas,
+                  Affine_Combination_Farkas, Convex_Combination_Farkas };
+
+Relation Farkas(NOT_CONST Relation &R, Farkas_Type op, bool early_bailout = false);
+
+extern coef_t farkasDifficulty;
+extern Global_Var_ID coefficient_of_constant_term;
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/hull.h b/omegalib/omega_lib/include/omega/hull.h
new file mode 100644
index 0000000..928d0c6
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/hull.h
@@ -0,0 +1,89 @@
+#ifndef Already_Included_Hull
+#define Already_Included_Hull
+
+#include <omega/farkas.h>
+
+namespace omega {
+
+Relation SimpleHull(const Relation &R, bool allow_stride_constraint = false, bool allow_irregular_constraint = false);
+Relation SimpleHull(const std::vector<Relation> &Rs, bool allow_stride_constraint = false, bool allow_irregular_constraint = false);
+
+
+// All of the following first call approximate on R to
+// eliminate any wildcards and strides.
+
+// x in Convex Hull of R
+// iff
+// exist a_i, y_i s.t. 
+//    x = Sum_i  a_i y_i s.t.
+//    forall i, y_i in R
+//    forall i, a_i >=0
+//    sum_i  a_i = 1
+Relation ConvexHull(NOT_CONST Relation &R);
+
+// DecoupledConvexHull is the same as ConvexHull, 
+// except that it only finds constraints that involve
+// both variables x&y if there is a constraint 
+// that involves both x&y in one of the conjuncts 
+// of R.
+Relation DecoupledConvexHull(NOT_CONST Relation &R);
+
+// The affine hull just consists of equality constraints
+// but is otherwise the tightest hull on R.
+// x in Affine Hull of R
+// iff
+// exist a_i, y_i s.t. 
+//    x = Sum_i  a_i y_i s.t.
+//    forall i, y_i in R
+//    sum_i  a_i = 1
+Relation AffineHull(NOT_CONST Relation &R);
+
+// x in Linear Hull of R
+// iff
+// exist a_i, y_i s.t. 
+//    x = Sum_i  a_i y_i s.t.
+//    forall i, y_i in R
+Relation LinearHull(NOT_CONST Relation &R);
+
+// The conic hull is the tighest cone that contains R
+// x in Conic Hull of R.
+// iff
+// exist a_i, y_i s.t. 
+//    x = Sum_i  a_i y_i s.t.
+//    forall i, y_i in R
+//    forall i, a_i >=0
+Relation ConicHull(NOT_CONST Relation &R);
+
+// RectHull includes readily-available constraints from relation
+// that can be part of hull, plus rectangular bounds calculated
+// from input/output/set variables' range.
+Relation RectHull(NOT_CONST Relation &Rel);
+
+// A constraint is in the result of QuickHull only if it appears in one of
+// the relations and is directly implied by a single constraint in each of
+// the other relations.
+Relation QuickHull(Relation &R); // deprecated
+Relation QuickHull(Tuple<Relation> &Rs); // deprecated
+
+Relation FastTightHull(NOT_CONST Relation &input_R,
+                        NOT_CONST Relation &input_H);
+Relation  Hull(NOT_CONST Relation &R, 
+			bool stridesAllowed = false,
+			int effort=1,
+			NOT_CONST Relation &knownHull = Relation::Null()
+			);
+Relation Hull(Tuple<Relation> &Rs, 
+              const std::vector<bool> &validMask, 
+              int effort = 1, 
+              bool stridesAllowed = false,
+              NOT_CONST Relation &knownHull = Relation::Null());
+
+// If a union of several conjuncts is a convex, their union
+// representaition can be simplified by their convex hull.
+Relation ConvexRepresentation(NOT_CONST Relation &R);
+Relation CheckForConvexPairs(NOT_CONST Relation &S); // deprecated
+Relation CheckForConvexRepresentation(NOT_CONST Relation &R_In); // deprecated
+
+}
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/omega_core/debugging.h b/omegalib/omega_lib/include/omega/omega_core/debugging.h
new file mode 100644
index 0000000..e217ae9
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/omega_core/debugging.h
@@ -0,0 +1,30 @@
+#if !defined(Already_included_debugging)
+#define Already_included_debugging
+
+// Debugging flags.  Can set any of these.
+
+#include <stdio.h>
+#include <ctype.h>
+
+namespace omega {
+
+
+
+extern int omega_core_debug;
+extern int pres_debug;
+extern int relation_debug;
+extern int closure_presburger_debug;
+extern int hull_debug;
+extern int farkas_debug;
+extern int code_gen_debug;
+
+enum negation_control { any_negation, one_geq_or_eq, one_geq_or_stride };
+extern negation_control pres_legal_negations;
+
+#if defined STUDY_EVACUATIONS
+extern int evac_debug;
+#endif
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/omega_core/oc.h b/omegalib/omega_lib/include/omega/omega_core/oc.h
new file mode 100644
index 0000000..e4f5444
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/omega_core/oc.h
@@ -0,0 +1,350 @@
+#ifndef Already_Included_OC
+#define Already_Included_OC 1
+
+#include <stdio.h>
+#include <string>
+#include <basic/util.h>
+#include <omega/omega_core/debugging.h>
+#include <basic/Tuple.h>
+
+namespace omega {
+
+// Manu:: commented the line below  -- fortran bug workaround
+//#define maxVars 256 /* original 56, increased by chun */
+#define maxVars 100 
+
+extern int maxGEQs;
+extern int maxEQs;
+
+// Manu:: commented the lines below  -- fortran bug workaround
+//const int maxmaxGEQs = 2048; // original 512, increaded by chun
+//const int maxmaxEQs = 512;   // original 256, increased by chun
+const int maxmaxGEQs = 512;
+const int maxmaxEQs = 256;
+
+/* #if ! defined maxmaxGEQs */
+/* #define maxmaxGEQs 2048  /\* original 512, increaded by chun *\/ */
+/* #endif */
+/* #if ! defined maxmaxEQs */
+/* #define maxmaxEQs  512  /\* original 256, increased by chun *\/ */
+/* #endif */
+
+
+#if 0
+#if ! defined Already_Included_Portable
+typedef unsigned char bool;  /* what a gross thing to do */
+#endif
+#endif
+
+typedef int EqnKey;
+
+enum {EQ_BLACK = 0, EQ_RED = 1};
+enum {OC_SOLVE_UNKNOWN = 2, OC_SOLVE_SIMPLIFY = 3};
+
+struct eqn {
+  EqnKey  key;
+  coef_t  touched;  // see oc_simple.c
+  int     color;
+  int     essential;
+  int     varCount;
+  coef_t  coef[maxVars + 1];
+};
+
+// typedef eqn * Eqn;
+enum redType {notRed=0, redEQ, redGEQ, redLEQ, redStride};
+enum redCheck {noRed=0, redFalse, redConstraints};
+enum normalizeReturnType {normalize_false, normalize_uncoupled,
+                          normalize_coupled};
+
+extern char wildName[200][20];
+
+extern FILE *outputFile; /* printProblem writes its output to this file */
+#define doTrace (trace && TRACE)
+#define isRed(e) (desiredResult == OC_SOLVE_SIMPLIFY && (e)->color)
+// #define eqnncpy(e1,e2,s) {int *p00,*q00,*r00; p00 = (int *)(e1); q00 = (int *)(e2); r00 = &p00[headerWords+1+s]; while(p00 < r00) *p00++ = *q00++; }
+// #define eqncpy(e1,e2) eqnncpy(e1,e2,nVars)
+// #define eqnnzero(e,s) {int *p00,*r00; p00 = (int *)(e); r00 = &p00[headerWords+1+(s)]; while(p00 < r00) *p00++ = 0;}
+// #define eqnzero(e) eqnnzero(e,nVars)
+
+//void eqnncpy(eqn *dest, eqn *src, int);
+//void eqnnzero(eqn *e, int);
+
+inline void eqnncpy(eqn *dest, eqn *src, int nVars) {
+  dest->key = src->key;
+  dest->touched = src->touched;
+  dest->color = src->color;
+  dest->essential = src->essential;
+  dest->varCount = src->varCount;
+  for (int i = 0; i <= nVars; i++)
+    dest->coef[i] = src->coef[i];
+}
+
+
+inline void eqnnzero(eqn *e, int nVars) {
+  e->key = 0;
+  e->touched = 0;
+  e->color = EQ_BLACK;
+  e->essential = 0;
+  e->varCount = 0;
+  for (int i = 0; i <= nVars; i++)
+    e->coef[i] = 0;
+}
+
+extern int mayBeRed;
+
+#ifdef SPEED
+#define TRACE 0
+#define DBUG 0
+#define DEBUG 0
+#else
+#define TRACE (omega_core_debug)
+#define DBUG  (omega_core_debug > 1)
+#define DEBUG (omega_core_debug > 2)
+#endif
+
+
+class Memory {
+public:
+  int     length;
+  coef_t  stride;
+  redType kind;
+  coef_t  constantTerm;
+  coef_t  coef[maxVars + 1];
+  int     var[maxVars + 1];
+};
+
+/* #define headerWords ((4*sizeof(int) + sizeof(coef_t))/sizeof(int)) */
+
+void check_number_EQs(int);
+void check_number_GEQs(int);
+extern eqn SUBs[];
+extern Memory redMemory[];
+
+class Problem {
+public:
+  short     nVars, safeVars;
+  short     nEQs, nGEQs,nSUBs,nMemories,allocEQs,allocGEQs;
+  short varsOfInterest;
+  bool variablesInitialized;
+  bool variablesFreed;
+  short     var[maxVars+2];
+  short     forwardingAddress[maxVars+2];
+  // int     variableColor[maxVars+2];
+  int  hashVersion;
+  const char *(*get_var_name)(unsigned int var, void *args);
+  void *getVarNameArgs;
+  eqn *GEQs;
+  eqn *EQs;
+  bool isTemporary;
+
+  Problem(int in_eqs=0, int in_geqs=0);
+  Problem(const Problem &);
+  ~Problem();
+  Problem & operator=(const Problem &);
+
+/* Allocation parameters and functions */
+
+  static const int min_alloc,first_alloc_pad;
+  int padEQs(int oldalloc, int newreq) {
+    check_number_EQs(newreq);
+    return min((newreq < 2*oldalloc ? 2*oldalloc : 2*newreq),maxmaxEQs);
+  }
+  int padGEQs(int oldalloc, int newreq) {
+    check_number_GEQs(newreq);
+    return min((newreq < 2*oldalloc ? 2*oldalloc : 2*newreq),maxmaxGEQs);
+  }
+  int padEQs(int newreq) {
+    check_number_EQs(newreq);
+    return min(max(newreq+first_alloc_pad,min_alloc), maxmaxEQs);
+  }
+  int padGEQs(int newreq) {
+    check_number_GEQs(newreq);
+    return min(max(newreq+first_alloc_pad,min_alloc), maxmaxGEQs);
+  }
+
+
+  void zeroVariable(int i);
+
+  void putVariablesInStandardOrder();
+  void noteEssential(int onlyWildcards);
+  int findDifference(int e, int &v1, int &v2);
+  int chainKill(int color,int onlyWildcards);
+
+  int newGEQ();
+  int newEQ();
+  int newSUB(){
+    return nSUBs++;
+  }
+
+
+  void initializeProblem();
+  void initializeVariables() const;
+  void printProblem(int debug = 1) const;
+  void printSub(int v) const;
+  std::string print_sub_to_string(int v) const;
+  void clearSubs();
+  void printRedEquations() const;
+  int  countRedEquations() const;
+  int  countRedGEQs() const;
+  int  countRedEQs() const;
+  int  countRedSUBs() const;
+  void difficulty(int &numberNZs, coef_t &maxMinAbsCoef, coef_t &sumMinAbsCoef) const;
+  int  prettyPrintProblem() const;
+  std::string  prettyPrintProblemToString() const;
+  int  prettyPrintRedEquations() const;
+  int  simplifyProblem(int verify, int subs, int redundantElimination);
+  int  simplifyProblem();
+  int  simplifyAndVerifyProblem();
+  int  simplifyApproximate(bool strides_allowed);
+  void coalesce();
+  void partialElimination();
+  void unprotectVariable(int var);
+  void negateGEQ(int);
+  void convertEQstoGEQs(bool excludeStrides);
+  void convertEQtoGEQs(int eq);
+  void nameWildcard(int i);
+  void useWildNames();
+  void ordered_elimination(int symbolic);
+  int eliminateRedundant (bool expensive);
+  void eliminateRed(bool expensive);
+  void constrainVariableSign(int color, int var, int sign); 
+  void  constrainVariableValue(int color, int var, int value);
+  void query_difference(int v1, int v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed);
+  int solve(int desiredResult);
+  std::string print_term_to_string(const eqn *e, int c) const;
+  void printTerm(const eqn * e, int c) const;
+  std::string printEqnToString(const eqn * e, int test, int extra) const;
+  void sprintEqn(char *str, const eqn * e, int is_geq,int extra) const;
+  void printEqn(const eqn * e, int is_geq, int extra) const;
+  void printEQ(const eqn *e) const {printEqn(e,0,0); }
+  std::string print_EQ_to_string(const eqn *e) const {return printEqnToString(e,0,0);}
+  std::string print_GEQ_to_string(const eqn *e) const {return printEqnToString(e,1,0);}
+  void printGEQ(const eqn *e) const {printEqn(e,1,0); }
+  void printGEQextra(const eqn *e) const {printEqn(e,1,1); }
+  void printSubstitution(int s) const;
+  void printVars(int debug = 1) const;
+  void swapVars(int i, int j);
+  void reverseProtectedVariables();
+  redCheck redSimplifyProblem(int effort, int computeGist);
+  
+  // calculate value of variable mod integer from set of equations -- by chun 12/14/2006
+  coef_t query_variable_mod(int v, coef_t factor, int color=EQ_BLACK, int nModularEQs=0, int nModularVars=0) const;
+  coef_t query_variable_mod(int v, coef_t factor, int color, int nModularEQs, int nModularVars, Tuple<bool> &working_on) const; // helper function
+
+  int queryVariable(int i, coef_t *lowerBound, coef_t *upperBound);
+  int query_variable_bounds(int i, coef_t *l, coef_t *u);
+  void queryCoupledVariable(int i, coef_t *l, coef_t *u, int *couldBeZero, coef_t lowerBound, coef_t upperBound);
+  int queryVariableSigns(int i, int dd_lt, int dd_eq, int dd_gt, coef_t lowerBound, coef_t upperBound, bool *distKnown, coef_t *dist);
+  void addingEqualityConstraint(int e);
+  normalizeReturnType normalize();
+  void normalize_ext();
+  void cleanoutWildcards();
+  void substitute(eqn *sub, int i, coef_t c);
+  void deleteVariable( int i);
+  void deleteBlack();
+  int addNewProtectedWildcard();
+  int addNewUnprotectedWildcard();
+  int protectWildcard( int i);
+  void doMod( coef_t factor, int e, int j);
+  void freeEliminations( int fv);
+  int verifyProblem();
+  void resurrectSubs();
+  int solveEQ();
+  int combineToTighten() ;
+  int quickKill(int onlyWildcards, bool desperate = false);
+  int expensiveEqualityCheck();
+  int expensiveRedKill();
+  int expensiveKill();
+  int smoothWeirdEquations();
+  void quickRedKill(int computeGist);
+  void chainUnprotect();
+  void freeRedEliminations();
+  void doElimination( int e, int i);
+  void analyzeElimination(
+    int &v,
+    int &darkConstraints,
+    int &darkShadowFeasible,
+    int &unit,
+    coef_t &parallelSplinters,
+    coef_t &disjointSplinters,
+    coef_t &lbSplinters,
+    coef_t &ubSplinters,
+    int &parallelLB);
+  int parallelSplinter(int e, int diff, int desiredResult);
+  int solveGEQ( int desiredResult);
+  void setInternals();
+  void setExternals();
+  int reduceProblem();
+  void problem_merge(Problem &);
+  void deleteRed();
+  void turnRedBlack();
+  void checkGistInvariant() const;
+  void check() const;
+  coef_t checkSum() const;
+  void rememberRedConstraint(eqn *e, redType type, coef_t stride);
+  void recallRedMemories();
+  void simplifyStrideConstraints();
+  const char * orgVariable(int i) const { 
+    return ((i == 0) ?   //  cfront likes this form better
+            "1" :
+            ((i < 0) ?
+             wildName[-i] :
+             (*get_var_name)(i,getVarNameArgs)));
+  };
+  const char * variable(int i) const { 
+    return orgVariable(var[i]) ;
+  };
+
+  void deleteGEQ(int e) {
+    if (DEBUG) {
+      fprintf(outputFile,"Deleting %d (last:%d): ",e,nGEQs-1); 
+      printGEQ(&GEQs[e]);
+      fprintf(outputFile,"\n");
+    }; 
+    if (e < nGEQs-1) 
+      eqnncpy (&GEQs[e], &GEQs[nGEQs - 1],(nVars)); 
+    nGEQs--;
+  };
+  void deleteEQ(int e) {
+    if (DEBUG) {
+      fprintf(outputFile,"Deleting %d (last:%d): ",e,nEQs-1); 
+      printGEQ(&EQs[e]);
+      fprintf(outputFile,"\n");
+    }; 
+    if (e < nEQs-1) 
+      eqnncpy (&EQs[e], &EQs[nEQs - 1],(nVars)); 
+    nEQs--;
+  };
+
+};
+
+
+
+/* #define UNKNOWN 2 */
+/* #define SIMPLIFY 3 */
+/* #define _red 1 */
+/* #define black 0 */
+
+
+extern int print_in_code_gen_style;
+
+
+void  initializeOmega(void);
+
+
+/* set extra to 0 for normal use */
+int singleVarGEQ(eqn *e);
+
+void setPrintLevel(int level);
+
+void printHeader();
+
+void setOutputFile(FILE *file);
+
+extern void check_number_EQs(int nEQs);
+extern void check_number_GEQs(int nGEQs);
+extern void checkVars(int nVars);
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/omega_core/oc_i.h b/omegalib/omega_lib/include/omega/omega_core/oc_i.h
new file mode 100644
index 0000000..9533a40
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/omega_core/oc_i.h
@@ -0,0 +1,79 @@
+#if !defined(Already_included_oc_i)
+#define Already_included_oc_i
+
+#include <basic/util.h>
+#include <omega/omega_core/oc.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <string>
+#include <vector>
+
+namespace omega {
+
+#define maxWildcards 18
+
+extern int findingImplicitEqualities;
+extern int firstCheckForRedundantEquations;
+extern int use_ugly_names;
+extern int doItAgain;
+extern int newVar;
+extern int conservative;
+extern FILE *outputFile; /* printProblem writes its output to this file */
+extern int nextWildcard;
+extern int trace;
+extern int depth;
+extern int packing[maxVars];
+extern int headerLevel;
+extern int inApproximateMode;
+extern int inStridesAllowedMode;
+extern int addingOuterEqualities;
+extern int outerColor;
+
+const int keyMult = 31;
+const int hashTableSize =5*maxmaxGEQs;
+const int maxKeys = 8*maxmaxGEQs;
+extern int hashVersion;
+extern eqn hashMaster[hashTableSize];
+extern int fastLookup[maxKeys*2];
+extern int nextKey;
+
+extern int reduceWithSubs;
+extern int pleaseNoEqualitiesInSimplifiedProblems;
+
+#define noProblem ((Problem *) 0)
+
+extern Problem *originalProblem;
+int checkIfSingleVar(eqn *e, int i);
+/* Solve e = factor alpha for x_j and substitute */
+
+void negateCoefficients(eqn * eqn, int nV);
+
+extern int omegaInitialized;
+extern Problem full_answer, context,redProblem;
+
+#if defined BRAIN_DAMAGED_FREE
+static inline void free(const Problem *p)
+{
+  free((char *)p);
+}
+#endif
+
+#if defined NDEBUG 
+#define CHECK_FOR_DUPLICATE_VARIABLE_NAMES 
+#else
+#define CHECK_FOR_DUPLICATE_VARIABLE_NAMES                              \
+  {                                                                     \
+    std::vector<std::string> name(nVars);                               \
+    for(int i=1; i<=nVars; i++) {                                       \
+      name[i-1] = variable(i);                                          \
+      assert(!name[i-1].empty());                                       \
+      for(int j=1; j<i; j++)                                            \
+        assert(!(name[i-1] == name[j-1]));                              \
+    }                                                                   \
+  }
+#endif
+
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/omega_i.h b/omegalib/omega_lib/include/omega/omega_i.h
new file mode 100644
index 0000000..e5d9230
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/omega_i.h
@@ -0,0 +1,30 @@
+#if ! defined _omega_i_h
+#define _omega_i_h 1
+
+#include <omega/pres_var.h>
+
+namespace omega {
+
+/* #define Assert(c,t) if(!(c)) PresErrAssert(t) */
+/* void PresErrAssert(const char *t); */
+
+extern Rel_Body null_rel;
+
+extern int     skip_finalization_check;
+// extern int     skip_set_checks;
+
+// Global input and output variable tuples.
+
+extern Global_Input_Output_Tuple input_vars;
+extern Global_Input_Output_Tuple output_vars;
+extern Global_Input_Output_Tuple &set_vars;
+
+} // namespace
+
+#if ! defined DONT_INCLUDE_TEMPLATE_CODE
+// with g++258, everything will need to make Tuple<Relation>, as a
+// function taking it as an argument is a friend of lots of classes
+#include <omega/Relation.h>
+#endif
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_cmpr.h b/omegalib/omega_lib/include/omega/pres_cmpr.h
new file mode 100644
index 0000000..fb3e6f0
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_cmpr.h
@@ -0,0 +1,49 @@
+#if ! defined _pres_cmpr_h
+#define _pres_cmpr_h 1
+
+#include <omega/omega_core/oc.h>
+
+namespace omega {
+
+//
+// Compressed problem: rectangular non-0 cut from the big problem.
+//
+class Comp_Constraints {
+public:
+  Comp_Constraints(eqn *constrs, int no_constrs, int no_vars);
+  void UncompressConstr(eqn *constrs, short &pn_constrs);
+  ~Comp_Constraints();
+  bool no_constraints() const
+  { return n_constrs == 0; }
+  int n_constraints() const
+  { return n_constrs; }
+
+protected:
+  inline int coef_index(int e, int v)
+  {return e*(n_vars+1) + v;}
+
+private:
+  int n_constrs;
+  int n_vars;
+  coef_t *coefs;
+};
+
+class Comp_Problem {
+public:
+  Comp_Problem(Problem *problem);
+  Problem *UncompressProblem();
+  bool no_constraints() const
+  { return eqs.no_constraints() && geqs.no_constraints(); }
+
+private:
+/* === data === */
+  int             _nVars, _safeVars;
+  const char   *(*_get_var_name)(unsigned int var, void *args);
+  void           *_getVarNameArgs;
+  Comp_Constraints eqs;
+  Comp_Constraints geqs;
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_cnstr.h b/omegalib/omega_lib/include/omega/pres_cnstr.h
new file mode 100644
index 0000000..7b2d98d
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_cnstr.h
@@ -0,0 +1,192 @@
+#if ! defined _pres_cnstr_h
+#define _pres_cnstr_h 1
+
+#include <omega/pres_var.h>
+#include <vector>
+
+namespace omega {
+
+//
+// Constraint handles
+//
+
+
+
+void copy_constraint(Constraint_Handle H, const Constraint_Handle initial);
+
+class Constraint_Handle {
+public:
+  Constraint_Handle() {}
+  virtual ~Constraint_Handle() {}
+  
+  void   update_coef(Variable_ID, coef_t delta);
+  void   update_const(coef_t delta);
+  coef_t get_coef(Variable_ID v) const;
+  coef_t get_const() const;
+  bool   has_wildcards() const;
+  int    max_tuple_pos() const;
+  int    min_tuple_pos() const;
+  bool is_const(Variable_ID v);
+  bool is_const_except_for_global(Variable_ID v);
+
+  virtual std::string print_to_string() const;
+  virtual std::string print_term_to_string() const;
+  
+  Variable_ID get_local(const Global_Var_ID G);
+  Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of);
+  // not sure that the second one can be used in a meaningful
+  // way if the conjunct is in multiple relations
+
+  void   finalize();
+  void   multiply(int multiplier);
+  Rel_Body *relation() const;
+
+
+protected:
+  Conjunct *c;
+  eqn      **eqns;
+  int      e;
+
+  friend class Constr_Vars_Iter;
+  friend class Constraint_Iterator; 
+
+  Constraint_Handle(Conjunct *, eqn **, int);
+
+#if defined PROTECTED_DOESNT_WORK
+  friend class EQ_Handle;
+  friend class GEQ_Handle;
+#endif
+
+  void   update_coef_during_simplify(Variable_ID, coef_t delta);
+  void   update_const_during_simplify(coef_t delta);
+  coef_t    get_const_during_simplify() const;
+  coef_t    get_coef_during_simplify(Variable_ID v) const;
+
+  
+public:
+  friend class Conjunct;  // assert_leading_info updates coef's
+  // as does move_UFS_to_input
+  friend class DNF;       // and DNF::make_level_carried_to
+
+  friend void copy_constraint(Constraint_Handle H,
+                              const Constraint_Handle initial);
+  // copy_constraint does updates and gets at c and e
+
+};
+
+class GEQ_Handle : public Constraint_Handle {
+public:
+  inline GEQ_Handle() {}
+
+  virtual std::string print_to_string() const;
+  virtual std::string print_term_to_string() const;
+  bool operator==(const Constraint_Handle &that);
+
+  void   negate();
+
+private:
+  friend class Conjunct;
+  friend class GEQ_Iterator;
+
+  GEQ_Handle(Conjunct *, int);
+};
+
+
+class EQ_Handle : public Constraint_Handle {
+public:
+  inline EQ_Handle() {}
+
+  virtual std::string print_to_string() const;
+  virtual std::string print_term_to_string() const;
+  bool operator==(const Constraint_Handle &that);
+
+private:
+  friend class Conjunct;
+  friend class EQ_Iterator;
+  
+  EQ_Handle(Conjunct *, int);
+};
+
+
+//
+// Conjuct iterators -- for querying resulting DNF.
+//
+class Constraint_Iterator : public Generator<Constraint_Handle> {
+public:
+  Constraint_Iterator(Conjunct *);
+  int  live() const;
+  void operator++(int);
+  void operator++();
+  Constraint_Handle operator* ();
+  Constraint_Handle operator* () const;
+
+private:
+  Conjunct *c;
+  int current,last;
+  eqn **eqns;
+};
+
+
+class EQ_Iterator : public Generator<EQ_Handle> {
+public:
+  EQ_Iterator(Conjunct *);
+  int  live() const;
+  void operator++(int);
+  void operator++();
+  EQ_Handle operator* ();
+  EQ_Handle operator* () const;
+
+private:
+  Conjunct *c;
+  int current, last;
+};
+
+
+class GEQ_Iterator : public Generator<GEQ_Handle> {
+public:
+  GEQ_Iterator(Conjunct *);
+  int  live() const;
+  void operator++(int);
+  void operator++();
+  GEQ_Handle operator* ();
+  GEQ_Handle operator* () const;
+
+private:
+  Conjunct *c;
+  int current, last;
+};
+
+
+//
+// Variables of constraint iterator.
+//
+struct Variable_Info {
+  Variable_ID var;
+  coef_t      coef;
+  Variable_Info(Variable_ID _var, coef_t _coef)
+    { var = _var; coef = _coef; }
+};
+
+class Constr_Vars_Iter : public Generator<Variable_Info> {
+public:
+  Constr_Vars_Iter(const Constraint_Handle &ch, bool _wild_only = false);
+  int         live() const;
+  void        operator++(int);
+  void        operator++();
+  Variable_Info operator*() const;
+
+  Variable_ID curr_var() const;
+  coef_t      curr_coef() const;
+
+private:
+  eqn               **eqns;
+  int               e;
+  Problem           *prob;
+  Variable_ID_Tuple &vars;
+  bool              wild_only;
+  int               current;
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_conj.h b/omegalib/omega_lib/include/omega/pres_conj.h
new file mode 100644
index 0000000..ea10a2c
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_conj.h
@@ -0,0 +1,299 @@
+#if ! defined _pres_conj_h
+#define _pres_conj_h 1
+
+#include <limits.h>
+#include <omega/pres_decl.h>
+#include <omega/pres_logic.h>
+#include <omega/pres_cnstr.h>
+
+namespace omega {
+
+//
+// Conjunct
+//
+// About variables in Conjunct:
+// All varaibles appear in exactly one declaration.
+// All variables used in Conjunct are referenced in mappedVars.
+// Wildcard variables are referenced both in mappedVars and in myLocals, 
+//   since they are declared in the conjunct.
+// All other variables are declared at the levels above.
+// Column number is: 
+//   in forwardingAddress in Problem if variablesInitialized is set, 
+//   equal to position of Variable_ID in mappedVars list otherwise.
+//
+
+class Conjunct : public F_Declaration {
+public:
+  Constraint_Iterator constraints();
+  Variable_ID_Tuple  *variables();
+  EQ_Iterator         EQs();
+  GEQ_Iterator        GEQs();
+  inline int          n_EQs() { return problem->nEQs; }
+  inline int          n_GEQs() { return problem->nGEQs; }
+
+  void promise_that_ub_solutions_exist(Relation &R);
+
+  inline Node_Type node_type() {return Op_Conjunct;}
+
+  inline int is_true() {return problem->nEQs==0 && problem->nGEQs==0 
+      && exact;}
+
+  void query_difference(Variable_ID v1, Variable_ID v2,
+                        coef_t &lowerBound, coef_t &upperBound, bool &guaranteed);
+  void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound);
+  coef_t query_variable_mod(Variable_ID v, coef_t factor);
+  bool query_variable_used(Variable_ID v);
+
+  int countNonzeros() const {
+    int numberNZs;
+    coef_t maxCoef, SumAbsCoef;
+    problem->difficulty(numberNZs,maxCoef,SumAbsCoef);
+    return numberNZs;
+  }
+
+  void difficulty(int &numberNZs, coef_t &maxCoef, coef_t &SumAbsCoef) const {
+    problem->difficulty(numberNZs,maxCoef,SumAbsCoef);
+  }
+
+  int query_guaranteed_leading_0s() {
+    count_leading_0s();
+    return guaranteed_leading_0s;
+  }
+
+  int query_possible_leading_0s() {
+    count_leading_0s();
+    return possible_leading_0s;
+  }
+
+  int query_leading_dir() {
+    count_leading_0s();
+    return leading_dir;
+  }
+
+  void calculate_dimensions(Relation &R, int &ndim_all, int &ndim_domain);
+  int max_ufs_arity_of_set();
+  int max_ufs_arity_of_in();
+  int max_ufs_arity_of_out();
+
+  int rank();
+
+  ~Conjunct();
+
+  bool is_unknown() const;
+  inline bool is_exact() const { return exact;}
+  inline bool is_inexact() const { return !exact;}
+  inline void make_inexact()   { exact=false;}
+   
+
+#if ! defined NDEBUG
+  void     assert_leading_info();
+#else
+  void     assert_leading_info() {}
+#endif
+
+
+  // PRINTING FUNCTIONS
+  void print(FILE *output_file);
+  void prefix_print(FILE *output_file, int debug = 1);
+  std::string print_to_string(int true_printed);
+  std::string print_EQ_to_string(eqn *e) { return problem->print_EQ_to_string(e); }
+  std::string print_GEQ_to_string(eqn *e) { return problem->print_GEQ_to_string(e); }
+  std::string print_EQ_to_string(int e) 
+  { return problem->print_EQ_to_string(&(problem->EQs[e])); }
+  std::string print_GEQ_to_string(int e) 
+  { return problem->print_GEQ_to_string(&(problem->GEQs[e])); }
+  std::string print_term_to_string(eqn *e) { return problem->print_term_to_string(e,1); }
+  std::string print_EQ_term_to_string(int e) 
+  { return problem->print_term_to_string(&(problem->EQs[e]),1); }
+  std::string print_GEQ_term_to_string(int e) 
+  { return problem->print_term_to_string(&(problem->GEQs[e]),1); }
+  std::string print_sub_to_string(int col) { return problem->print_sub_to_string(col); }
+
+private:
+
+  inline void interpret_unknown_as_true()   { exact=true;}
+
+  friend Relation approx_closure(NOT_CONST Relation &r, int n);
+
+  virtual Conjunct *really_conjunct();
+
+
+  // create new constraints with all co-efficients 0
+  // These are public in F_And, use them from there.
+  EQ_Handle   add_stride(int step, int preserves_level = 0);
+  EQ_Handle   add_EQ(int preserves_level = 0);
+  GEQ_Handle  add_GEQ(int preserves_level = 0);
+  EQ_Handle   add_EQ(const Constraint_Handle &c, int preserves_level = 0);
+  GEQ_Handle  add_GEQ(const Constraint_Handle &c, int preserves_level = 0);
+
+  friend class GEQ_Handle;
+  friend class  EQ_Handle;
+  friend class Sub_Handle;
+  friend class Constraint_Handle;
+  friend class Constraint_Iterator;
+  friend class GEQ_Iterator;
+  friend class  EQ_Iterator;
+  friend class Sub_Iterator;
+  friend class Constr_Vars_Iter;
+
+
+  // FUNCTIONS HAVING TO DO WITH BUILDING FORMULAS/DNFs 
+  bool     can_add_child();
+  void remap();
+  void beautify();
+  DNF* DNFize();
+  int priority();
+  virtual Conjunct *find_available_conjunct();
+  void finalize();
+
+  friend class DNF;
+
+
+
+  // CREATING CONJUNCTS
+  Conjunct();
+  Conjunct(Conjunct &);
+  Conjunct(Formula *, Rel_Body *);
+
+  friend class Formula; // add_conjunct (a private function) creates Conjuncts
+  friend class F_Not;
+  friend class F_Or;
+  //   class F_And; is a friend below
+  
+
+  // VARIOUS FUNCTIONS TO CREATE / WORK WITH VARIABLES
+  Variable_ID declare(Const_String s);
+  Variable_ID declare();
+  Variable_ID declare(Variable_ID v);  
+  
+  friend const char *get_var_name(unsigned int, void *);
+  void push_exists(Variable_ID_Tuple &S);
+  int  get_column(Variable_ID);
+  int  find_column(Variable_ID);
+  int  map_to_column(Variable_ID);
+  void combine_columns();
+  void reorder();
+  void reorder_for_print(bool reverseOrder=false,
+                         int first_pass_input=0,
+                         int first_pass_output=0,
+                         bool sort=false);
+
+  friend void      remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel);
+
+  void localize_var(Variable_ID D);
+
+
+  // this creates variables in conjuncts for us:
+  friend int       new_WC(Conjunct *nc, Problem *np);
+
+
+  // UFS/LEADING ZEROS STUFF
+
+  void move_UFS_to_input();
+
+  void count_leading_0s();
+  void invalidate_leading_info(int changed = -1);
+  void enforce_leading_info(int guaranteed, int possible, int dir);
+
+  void reverse_leading_dir_info();
+
+ 
+
+  // CONJUNCT SPECIFIC STUFF
+
+  void      rm_color_constrs();
+  inline int N_protected() { return problem->safeVars; }
+
+
+  void ordered_elimination(int symLen) { problem->ordered_elimination(symLen);}
+  void convertEQstoGEQs(bool excludeStrides);
+
+  int cost();
+  
+  inline Formula*  copy(Formula *parent, Rel_Body *reln)
+  { return copy_conj_diff_relation(parent,reln); }
+  Conjunct* copy_conj_diff_relation(Formula *parent, Rel_Body *reln);
+  inline Conjunct* copy_conj_same_relation()
+  { return copy_conj_diff_relation(&(parent()), relation()); }
+  friend void internal_copy_conjunct(Conjunct* to, Conjunct* fr);
+  friend void copy_constraint(Constraint_Handle H,
+                              const Constraint_Handle initial);
+
+#if defined STUDY_EVACUATIONS
+  // The core function of "evac.c" does lots of work with conjuncts:
+  friend bool check_subseq_n(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity, int n, bool allow_offset);
+  friend void assert_subbed_syms(Conjunct *c);
+  friend bool check_affine(Conjunct *d, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity);
+  friend evac study(Conjunct *C, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity);
+#endif
+
+  // The relational ops tend to do lots of demented things to Conjuncts:
+  friend class Rel_Body;
+  friend_rel_ops;
+
+  // F_And sometimes absorbs conjuncts
+  friend class F_And;
+
+  // Various DNFize functions also get a the problem:
+
+  friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak);
+  friend class F_Exists;
+
+  // Substitutions are a wrapper around a low-level Problem operation
+  friend class Substitutions;
+
+  // private functions to call problem functions 
+  int simplifyProblem();
+  int simplifyProblem(int verify, int subs, int redundantElimination);
+  int redSimplifyProblem(int effort, int computeGist);
+
+  friend int       simplify_conj(Conjunct* conj, int ver_sim, int elim_red, int color);
+  friend DNF*      negate_conj(Conjunct* conj);
+  friend Conjunct* merge_conjs(Conjunct* conj1, Conjunct* conj2,
+                               Merge_Action action, Rel_Body *body = 0);
+  friend void      copy_conj_header(Conjunct* to, Conjunct* fr);
+
+
+  // === at last, the data ===
+
+  Variable_ID_Tuple mappedVars;
+
+  int              n_open_constraints;
+  bool             cols_ordered;
+  bool             simplified;
+  bool             verified;
+
+  int     guaranteed_leading_0s;  // -1 if unknown
+  int     possible_leading_0s;  // -1 if unknown
+  int     leading_dir; // 0 if unknown, else +/- 1
+  int     leading_dir_valid_and_known();
+
+  bool             exact;
+
+  short     r_constrs; // are redundant constraints eliminated?
+  Problem         *problem;
+
+  bool is_compressed();
+  void compress();
+  void uncompress();
+
+  friend class Comp_Problem;
+  Comp_Problem    *comp_problem;
+};
+
+
+/* === Misc. problem manipulation utilities === */
+
+const int CantBeNegated = INT_MAX-10;
+const int AvoidNegating = INT_MAX-11;
+
+void copy_column(Problem *tp,  int to_col,
+                 Problem *fp,  int fr_col,
+                 int start_EQ, int start_GEQ);
+void zero_column(Problem *tp,  int to_col,
+                 int start_EQ, int start_GEQ,
+                 int no_EQs,   int no_GEQs);
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_decl.h b/omegalib/omega_lib/include/omega/pres_decl.h
new file mode 100644
index 0000000..7fec0bc
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_decl.h
@@ -0,0 +1,55 @@
+#if ! defined _pres_decl_h
+#define _pres_decl_h 1
+
+#include <omega/pres_var.h>
+#include <omega/pres_form.h>
+#include <basic/Section.h>
+
+namespace omega {
+
+//
+// Base class for presburger formula nodes with variables
+//
+
+class F_Declaration : public Formula {
+public:
+  virtual Variable_ID declare(Const_String s)=0;
+  virtual Variable_ID declare()=0;
+  virtual Variable_ID declare(Variable_ID)=0;
+  virtual Section<Variable_ID> declare_tuple(int size);
+
+  void finalize();
+
+  inline Variable_ID_Tuple &locals() {return myLocals;}
+
+protected:
+  F_Declaration(Formula *, Rel_Body *);
+  F_Declaration(Formula *, Rel_Body *, Variable_ID_Tuple &);
+  ~F_Declaration();
+
+  Variable_ID do_declare(Const_String s, Var_Kind var_kind);
+
+  void prefix_print(FILE *output_file, int debug = 1);
+  void print(FILE *output_file);
+
+  void setup_names();
+  void setup_anonymous_wildcard_names();
+
+  Variable_ID_Tuple myLocals;
+  friend class F_Forall; // rearrange needs to access myLocals
+  friend class F_Or;     // push_exists
+
+private:
+  virtual bool can_add_child();
+
+  int priority();
+
+  friend void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe,
+                    Formula *f, const Mapping &mapping, bool &newrIsSet,
+                    List<int> &seen_exists, 
+                    Variable_ID_Tuple &seen_exists_ids);
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_dnf.h b/omegalib/omega_lib/include/omega/pres_dnf.h
new file mode 100644
index 0000000..93d5942
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_dnf.h
@@ -0,0 +1,87 @@
+#if ! defined _pres_dnf_h
+#define _pres_dnf_h 1
+
+#include <omega/pres_gen.h>
+
+namespace omega {
+
+//
+// Disjunctive Normal Form -- list of Conjuncts
+//
+class DNF {
+public:
+  void print(FILE *out_file);
+  void prefix_print(FILE *out_file, int debug = 1, bool parent_names_setup=false);
+
+  bool is_definitely_false() const;
+  bool is_definitely_true() const;
+  int  length() const;
+
+  Conjunct *single_conjunct() const;
+  bool      has_single_conjunct() const;
+  Conjunct *rm_first_conjunct();
+  void clear();
+  int query_guaranteed_leading_0s(int what_to_return_for_empty_dnf);
+  int query_possible_leading_0s(int what_to_return_for_empty_dnf);
+  int query_leading_dir();
+
+private:
+    // all DNFize functions need to access the dnf builders:
+  friend class F_And;
+  friend class F_Or;
+  friend class Conjunct;
+  friend DNF * negate_conj(Conjunct *);
+
+  friend class Rel_Body;
+  friend_rel_ops;
+
+  DNF();
+  ~DNF();
+
+  DNF* copy(Rel_Body *);
+
+  void simplify();
+  void make_level_carried_to(int level);
+  void count_leading_0s();
+
+  void add_conjunct(Conjunct*);
+  void join_DNF(DNF*);
+  void rm_conjunct(Conjunct *c);
+
+  void rm_redundant_conjs(int effort);
+  void rm_redundant_inexact_conjs();
+  void DNF_to_formula(Formula* root);
+
+
+  friend void  remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel);
+  void remap();
+
+  void setup_names();
+
+  void remove_inexact_conj();
+
+    // These may need to get at the conjList itself:
+  friend DNF*  DNF_and_DNF(DNF*, DNF*);
+  friend DNF*  DNF_and_conj(DNF*, Conjunct*);
+  friend DNF*  conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak);
+
+  friend class DNF_Iterator;
+
+  List<Conjunct*> conjList;
+};
+
+DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak=false);
+
+//
+// DNF iterator
+//
+class DNF_Iterator : public List_Iterator<Conjunct*> {
+public:
+    DNF_Iterator(DNF*dnf) : List_Iterator<Conjunct*>(dnf->conjList) {}
+    DNF_Iterator() {}
+    void curr_set(Conjunct *c) { *(*this) = c; }
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_form.h b/omegalib/omega_lib/include/omega/pres_form.h
new file mode 100644
index 0000000..ed3258e
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_form.h
@@ -0,0 +1,112 @@
+#if ! defined _pres_form_h
+#define _pres_form_h 1
+
+#include <omega/pres_gen.h>
+
+namespace omega {
+
+typedef enum {Op_Relation, Op_Not, Op_And, Op_Or,
+              Op_Conjunct, Op_Forall, Op_Exists}  Node_Type;
+
+
+//
+// Presburger Formula base class
+//
+
+class Formula {
+public:
+  virtual Node_Type node_type()=0;
+
+  F_Forall *add_forall();
+  F_Exists *add_exists();
+  virtual F_And  *and_with();
+  F_And  *add_and();
+  F_Or *add_or();
+  F_Not *add_not();
+  void add_unknown();
+
+  virtual void finalize();
+  virtual void print(FILE *output_file);
+
+  Rel_Body *relation() { return myRelation; }
+
+protected:
+  virtual ~Formula();
+private:
+  Formula(Formula *, Rel_Body *);
+
+  // The relational operations need to work with formula trees
+  friend class Relation;
+  friend_rel_ops;
+  // as do the functions that build DNF's
+  friend  class DNF;
+  // or other parts of the tree
+  friend class Conjunct;
+  friend class F_Declaration;
+  friend class F_Exists;
+  friend class F_Forall;
+  friend class F_Or;
+  friend class F_And;
+  friend class F_Not;
+  friend class Rel_Body;
+
+
+  // Operations needed for manipulation of formula trees:
+
+  void remove_child(Formula *);
+  void replace_child(Formula *child, Formula *new_child);
+  virtual bool can_add_child();
+  void add_child(Formula *);
+
+  Conjunct *add_conjunct();
+  virtual Conjunct *find_available_conjunct() = 0;
+
+  virtual Formula *copy(Formula *parent, Rel_Body *reln);
+  F_Exists *add_exists(Variable_ID_Tuple &S); 
+  virtual     void push_exists(Variable_ID_Tuple &S);
+
+  // Accessor functions for tree building
+
+  List<Formula*> &children() {return myChildren;}
+  int n_children() const {return myChildren.length();}
+  const List<Formula*> &get_children() const {return myChildren;}
+  Formula &parent() {return *myParent;}
+  void set_parent(Formula *p) {myParent = p;}
+
+
+  virtual int priority();
+
+  void verify_tree();  // should be const, but iterators are used
+
+  virtual void reverse_leading_dir_info();
+  virtual void invalidate_leading_info(int changed = -1);
+  virtual void enforce_leading_info(int guaranteed, int possible, int dir);
+
+  virtual void remap();   
+  virtual DNF* DNFize() = 0;
+  virtual void beautify();
+  virtual void rearrange();
+  virtual void setup_names();
+
+  virtual void print_separator(FILE *output_file);
+  virtual void combine_columns();
+  virtual void prefix_print(FILE *output_file, int debug = 1);
+  void print_head(FILE *output_file);
+
+  void set_relation(Rel_Body *r);
+  void set_parent(Formula *parent, Rel_Body *reln);
+
+  void assert_not_finalized();
+
+  virtual Conjunct *really_conjunct();  // until we get RTTI
+
+private:
+  List<Formula*>     myChildren;
+  Formula           *myParent;
+  Rel_Body          *myRelation;
+
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_gen.h b/omegalib/omega_lib/include/omega/pres_gen.h
new file mode 100644
index 0000000..ba6a793
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_gen.h
@@ -0,0 +1,192 @@
+#if ! defined _pres_gen_h
+#define _pres_gen_h 1
+
+#include <omega/omega_core/oc.h>
+#include <basic/ConstString.h>
+#include <basic/Iterator.h>
+#include <basic/List.h>
+#include <basic/Tuple.h>
+#include <assert.h>
+#include <stdlib.h>
+
+namespace omega {
+
+//
+// general presburger stuff thats needed everywhere
+//
+
+/* The following allows us to avoid warnings about passing 
+   temporaries as non-const references.  This is useful but 
+   has suddenly become illegal.  */
+
+#if !defined(LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY)
+#if defined(__GNUC__) && (__GNUC__ > 2 || (__GNUC__ == 2 && __GNUC_MINOR__ >= 7))
+#define LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY 1
+#else
+#define LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY 0
+#endif
+#endif
+
+#if LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY
+#define NOT_CONST const
+#else
+#define NOT_CONST 
+#endif
+
+//
+// I/O and error processing and control flags (also in omega_core/debugging.h)
+//
+
+extern FILE *DebugFile;
+extern int   pres_debug;
+
+extern int mega_total;
+extern int use_ugly_names;
+
+extern negation_control pres_legal_negations;
+
+
+//
+// Lots of things refer to each other,
+//  so we forward declare these classes:
+//
+
+class Var_Decl;
+typedef enum {Input_Var, Set_Var = Input_Var, Output_Var,
+              Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind;
+class Global_Var_Decl;
+typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2,
+				 Set_Tuple = Input_Tuple } Argument_Tuple;
+
+class Constraint_Handle;
+class EQ_Handle;
+class GEQ_Handle;
+typedef EQ_Handle Stride_Handle;
+
+class Formula;
+class F_Declaration;
+class F_Forall;
+class F_Exists;
+class F_And;
+class F_Or;
+class F_Not;
+class Conjunct;
+class Relation;
+class Rel_Body;
+class DNF;
+class Mapping;
+class Omega_Var;
+class Coef_Var_Decl;
+
+typedef Var_Decl *Variable_ID;
+typedef Global_Var_Decl *Global_Var_ID;
+
+typedef Tuple<Variable_ID>       Variable_ID_Tuple;
+typedef Sequence<Variable_ID>    Variable_ID_Sequence;  // use only for rvalues
+typedef Tuple_Iterator<Variable_ID>   Variable_ID_Tuple_Iterator;
+typedef Tuple_Iterator<Variable_ID>   Variable_ID_Iterator;
+
+typedef Variable_ID_Iterator Variable_Iterator;
+
+typedef enum {Comb_Id, Comb_And, Comb_Or, Comb_AndNot} Combine_Type;
+
+
+// things that are (hopefully) used only privately
+class Comp_Problem;
+class Comp_Constraints;
+
+// this has to be here rather than in pres_conj.h because
+// MergeConj has to be a friend of Constraint_Handle
+typedef enum {MERGE_REGULAR, MERGE_COMPOSE, MERGE_GIST} Merge_Action;
+
+
+// Conjunct can be exact or lower or upper bound.
+// For lower bound conjunct, the upper bound is assumed to be true;
+// For upper bound conjunct, the lower bound is assumed to be false
+
+typedef enum {EXACT_BOUND, UPPER_BOUND, LOWER_BOUND, UNSET_BOUND} Bound_Type;
+
+
+#if defined STUDY_EVACUATIONS
+typedef enum { in_to_out = 0, out_to_in = 1} which_way;
+
+enum evac { evac_trivial = 0,
+	    evac_offset = 1,
+	    evac_subseq = 2,
+	    evac_offset_subseq = 3,
+//	    evac_permutation = ,
+	    evac_affine = 4,
+	    evac_nasty = 5 };
+
+extern char *evac_names[];
+
+#endif
+
+// the following list should be updated in sync with Relations.h
+
+#define  friend_rel_ops \
+friend Relation  Union(NOT_CONST Relation &r1, NOT_CONST Relation &r2);		\
+friend Relation  Intersection(NOT_CONST Relation &r1, NOT_CONST Relation &r2);	\
+friend Relation  After(NOT_CONST Relation &R, int carried_by, int new_output, int dir);\
+friend Relation  Extend_Domain(NOT_CONST Relation &R);			\
+friend Relation  Extend_Domain(NOT_CONST Relation &R, int more);		\
+friend Relation  Extend_Range(NOT_CONST Relation &R);			\
+friend Relation  Extend_Range(NOT_CONST Relation &R, int more);		\
+friend Relation  Extend_Set(NOT_CONST Relation &R);			\
+friend Relation  Extend_Set(NOT_CONST Relation &R, int more);		\
+friend Relation  Restrict_Domain(NOT_CONST Relation &r1, NOT_CONST Relation &r2);	\
+friend Relation  Restrict_Range(NOT_CONST Relation &r1, NOT_CONST Relation &r2);	\
+friend Relation  Domain(NOT_CONST Relation &r);				\
+friend Relation  Range(NOT_CONST Relation &r);				\
+friend Relation  Cross_Product(NOT_CONST Relation &A, NOT_CONST Relation &B);	\
+friend Relation  Inverse(NOT_CONST Relation &r);				\
+friend Relation  Deltas(NOT_CONST Relation &R);				\
+friend Relation  Deltas(NOT_CONST Relation &R, int eq_no);		\
+friend Relation  DeltasToRelation(NOT_CONST Relation &R, int n_input, int n_output); \
+friend Relation  Complement(NOT_CONST Relation &r);			\
+friend Relation  Project(NOT_CONST Relation &R, Global_Var_ID v);		\
+friend Relation  Project(NOT_CONST Relation &r, int pos, Var_Kind vkind);	\
+friend Relation  Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s); \
+friend Relation  Project_Sym(NOT_CONST Relation &R);			\
+friend Relation  Project_On_Sym(NOT_CONST Relation &R, NOT_CONST Relation &context); \
+friend Relation  GistSingleConjunct(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort); \
+friend Relation  Gist(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort);	\
+friend Relation  Difference(NOT_CONST Relation &r1, NOT_CONST Relation &r2);	\
+friend Relation  Approximate(NOT_CONST Relation &R, bool strides_allowed);	\
+friend Relation  Identity(int n_inp);				\
+friend Relation  Identity(NOT_CONST Relation &r);				\
+friend bool do_subset_check(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \
+friend bool Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \
+friend bool Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \
+friend bool May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \
+friend bool      Is_Obvious_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2);	\
+friend Relation  Join(NOT_CONST Relation &G, NOT_CONST Relation &F);		\
+friend Relation  Composition(NOT_CONST Relation &F, NOT_CONST Relation &G);		\
+friend bool      can_do_exact_composition(NOT_CONST Relation &F, NOT_CONST Relation &G); \
+friend Relation  EQs_to_GEQs(NOT_CONST Relation &, bool excludeStrides);	\
+friend Relation  Symbolic_Solution(NOT_CONST Relation &S);                \
+friend Relation  Symbolic_Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); \
+friend Relation  Sample_Solution(NOT_CONST Relation &S);                  \
+friend Relation  Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); \
+friend void MapRel1(Relation &inputRel, const Mapping &map,	\
+		    Combine_Type ctype, int number_input, 	\
+		    int number_output, bool, bool);		\
+friend Relation MapAndCombineRel2(Relation &R1, Relation &R2, 	\
+				  const Mapping &mapping1,	\
+				  const Mapping &mapping2,	\
+				  Combine_Type ctype,		\
+				  int number_input,		\
+				  int number_output);		\
+friend void align(Rel_Body *, Rel_Body *, F_Exists *,		\
+		  Formula *, const Mapping &, bool &,		\
+		  List<int> &, Variable_ID_Tuple &);            \
+friend Relation  Lower_Bound(NOT_CONST Relation &r);	\
+friend Relation  Upper_Bound(NOT_CONST Relation &r)
+
+
+// REMEMBER - THE LAST LINE OF THE MACRO SHOULD NOT HAVE A ;
+/* TransitiveClosure doesn't need to be in friend_rel_ops */
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_logic.h b/omegalib/omega_lib/include/omega/pres_logic.h
new file mode 100644
index 0000000..27c4553
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_logic.h
@@ -0,0 +1,90 @@
+#if ! defined _pres_logic_h
+#define _pres_logic_h 1
+
+#include <omega/pres_form.h>
+
+namespace omega {
+//
+// Presburger formula classes for logical operations: and, or not
+//
+
+class F_And    : public Formula {
+public:
+    inline Node_Type node_type() {return Op_And;}
+
+    // "preserves level" should be 0 unless we know this will not
+    // change the "level" of the constraints - ie the number of
+    // leading corresponding in,out variables known to be equal
+    GEQ_Handle     add_GEQ(int preserves_level = 0);
+    EQ_Handle      add_EQ(int preserves_level = 0);
+    Stride_Handle  add_stride(int step, int preserves_level = 0);
+    EQ_Handle   add_EQ(const Constraint_Handle &c, int preserves_level = 0);
+    GEQ_Handle  add_GEQ(const Constraint_Handle &c, int preserves_level = 0);
+
+    F_And    *and_with();
+    void add_unknown();
+
+private:
+    friend class Formula;  // add_and()
+    F_And(Formula *p, Rel_Body *r);
+
+private:
+    Formula *copy(Formula *parent, Rel_Body *reln);
+    virtual Conjunct *find_available_conjunct();
+    int priority();
+    void print_separator(FILE *output_file);
+    void prefix_print(FILE *output_file, int debug = 1);
+    void beautify();
+    DNF* DNFize();
+ 
+    Conjunct *pos_conj;
+};
+
+
+class F_Or     : public Formula {
+public:
+    inline Node_Type node_type() {return Op_Or;}
+
+private:
+    friend class Formula; // add_or
+    F_Or(Formula *, Rel_Body *);
+
+private:
+    Formula *copy(Formula *parent, Rel_Body *reln);
+
+    virtual Conjunct *find_available_conjunct();
+    void print_separator(FILE *output_file);
+    void prefix_print(FILE *output_file, int debug = 1);
+    void beautify();
+    int priority();
+    DNF* DNFize();
+    void push_exists(Variable_ID_Tuple &S);
+};
+
+
+class F_Not    : public Formula {
+public:
+    inline Node_Type node_type() {return Op_Not;}
+    void finalize();
+
+private:
+    friend class Formula;
+    F_Not(Formula *, Rel_Body *);
+
+private:
+    Formula *copy(Formula *parent, Rel_Body *reln);
+
+    virtual Conjunct *find_available_conjunct();
+    friend class F_Forall;
+    bool can_add_child();
+    void beautify();
+    void rearrange();
+    int priority();
+    DNF* DNFize();
+    void print(FILE *output_file);
+    void prefix_print(FILE *output_file, int debug = 1);
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_quant.h b/omegalib/omega_lib/include/omega/pres_quant.h
new file mode 100644
index 0000000..98c30df
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_quant.h
@@ -0,0 +1,63 @@
+#if ! defined _pres_quant_h
+#define _pres_quant_h 1
+
+#include <omega/pres_decl.h>
+
+namespace omega {
+
+//
+// Presburger formula nodes for quantifiers
+//
+
+class F_Exists : public F_Declaration {
+public:
+    inline Node_Type node_type() {return Op_Exists;}
+    Variable_ID declare(Const_String s);
+    Variable_ID declare();
+    Variable_ID declare(Variable_ID v);
+    virtual     void push_exists(Variable_ID_Tuple &S);
+
+protected:
+    friend class Formula;
+
+    F_Exists(Formula *, Rel_Body *);
+    F_Exists(Formula *, Rel_Body *, Variable_ID_Tuple &);
+
+private:
+    Formula *copy(Formula *parent, Rel_Body *reln);
+
+    virtual Conjunct *find_available_conjunct();
+    void print(FILE *output_file);
+    void prefix_print(FILE *output_file, int debug = 1);
+    void beautify();
+    void rearrange();
+    DNF* DNFize();
+};
+
+
+class F_Forall : public F_Declaration {
+public:
+    inline Node_Type node_type() {return Op_Forall;}
+    Variable_ID declare(Const_String s);
+    Variable_ID declare();
+    Variable_ID declare(Variable_ID v);
+
+protected:
+    friend class Formula;
+
+    F_Forall(Formula *, Rel_Body *);
+
+private:
+    Formula *copy(Formula *parent, Rel_Body *reln);
+
+    virtual Conjunct *find_available_conjunct();
+    void print(FILE *output_file);
+    void prefix_print(FILE *output_file, int debug = 1);
+    void beautify();
+    void rearrange();
+    DNF* DNFize();
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_subs.h b/omegalib/omega_lib/include/omega/pres_subs.h
new file mode 100644
index 0000000..8a9ee92
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_subs.h
@@ -0,0 +1,88 @@
+#if !defined(pres_subs_h)
+#define pres_subs_h
+
+/* Interface to omega core's substitutions.
+
+   Creating an object of class Substitutions causes ordered elimination, 
+   i.e. variables in the input and output tuples are substituted for by
+   functions of earlier variables.  Could conceivablely create a more 
+   flexible interface to orderedElimination if we developed a way to 
+   specify the desired variable order.  
+
+   This is not an entirely consistent interface, since Sub_Handles
+   shouldn't really permit update_coef on SUBs.  It is not a real
+   problem since subs are now no longer part of a conjunct, but it is
+   a slightly odd situation.
+
+   Don't try to simplify r after performing orderedElimination.
+*/
+
+   
+#include <omega/pres_gen.h>
+#include <omega/Relation.h>
+#include <omega/pres_conj.h>
+#include <omega/pres_cnstr.h>
+
+namespace omega {
+
+class Sub_Handle;
+class Sub_Iterator;
+
+class Substitutions  {
+public: 
+    Substitutions(Relation &input_R, Conjunct *input_c);
+    ~Substitutions();
+    Sub_Handle get_sub(Variable_ID v);
+    bool substituted(Variable_ID v);
+    bool sub_involves(Variable_ID v, Var_Kind kind);
+private:
+    friend class Sub_Iterator;
+    friend class Sub_Handle;
+    Relation *r;
+    Conjunct *c;
+    eqn *subs;
+    Variable_ID_Tuple subbed_vars;
+};
+
+
+//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
+
+
+class Sub_Handle: public Constraint_Handle {
+public:
+    inline Sub_Handle() {}
+
+    virtual std::string print_to_string() const;
+    virtual std::string print_term_to_string() const;
+    Variable_ID variable() {return v;}
+
+private:
+    friend class Substitutions;
+    friend class Sub_Iterator;
+    Sub_Handle(Substitutions *, int, Variable_ID);
+//    Sub_Handle(Substitutions *, int);
+
+    Variable_ID v;
+};
+
+//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
+
+
+class Sub_Iterator : public Generator<Sub_Handle> {
+public:
+    Sub_Iterator(Substitutions *input_s): s(input_s), current(0),
+                                          last(s->c->problem->nSUBs-1) {}
+    int  live() const;
+    void operator++(int);
+    void operator++();
+    Sub_Handle operator* ();
+    Sub_Handle operator* () const;
+
+private:
+    Substitutions *s;
+    int current, last;
+};
+
+} // namespace
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_tree.h b/omegalib/omega_lib/include/omega/pres_tree.h
new file mode 100644
index 0000000..ad78ad0
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_tree.h
@@ -0,0 +1,15 @@
+#if ! defined _pres_tree_h
+#define _pres_tree_h 1
+
+//
+// Header to include if you need all the classes to build
+// a Presburger formula:
+// variables, constraints, nodes for logical operations & quantifiers
+//
+
+#include <omega/pres_var.h>
+#include <omega/pres_cnstr.h>
+#include <omega/pres_logic.h>
+#include <omega/pres_quant.h>
+
+#endif
diff --git a/omegalib/omega_lib/include/omega/pres_var.h b/omegalib/omega_lib/include/omega/pres_var.h
new file mode 100644
index 0000000..bf60dcb
--- /dev/null
+++ b/omegalib/omega_lib/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
diff --git a/omegalib/omega_lib/include/omega/reach.h b/omegalib/omega_lib/include/omega/reach.h
new file mode 100644
index 0000000..ff4bf79
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/reach.h
@@ -0,0 +1,23 @@
+#if ! defined _reach_h
+#define _reach_h 1
+
+namespace omega {
+
+class reachable_information {
+public:
+	Tuple<std::string> node_names;
+	Tuple<int> node_arity;
+	Dynamic_Array1<Relation> start_nodes;
+	Dynamic_Array2<Relation> transitions;
+};
+
+
+Dynamic_Array1<Relation> *
+Reachable_Nodes(reachable_information * reachable_info);
+
+Dynamic_Array1<Relation> *
+I_Reachable_Nodes(reachable_information * reachable_info);
+
+} // namespace
+
+#endif