1 files changed, 131 insertions, 0 deletions
diff --git a/omegalib/omega_lib/src/pres_subs.cc b/omegalib/omega_lib/src/pres_subs.cc
new file mode 100644
index 0000000..9854b09
--- /dev/null
+++ b/omegalib/omega_lib/src/pres_subs.cc
@@ -0,0 +1,131 @@
+#include <omega/pres_subs.h>
+
+namespace omega {
+
+Substitutions::Substitutions(Relation &input_R, Conjunct *input_c) {
+  int i;
+  r = new Relation(input_R,input_c);
+  c = r->single_conjunct();
+  c->reorder_for_print();
+  c->ordered_elimination(r->global_decls()->length());
+  int num_subs = c->problem->nSUBs; 
+  subs = new eqn[num_subs];
+  for(i = 0; i < num_subs; i++)
+    subs[i] = SUBs[i];
+  subbed_vars.reallocate(num_subs);
+  /* Go through and categorize variables as:
+     1) substituted, 2) not substituted, 3) wildcard
+     Safevars number of variables were not able to be substituted.
+     nVars number of total variables, including wildcards.
+     nSUBs is the number of substitutions.
+     nSUBs + nVars == the number of variables that went in. 
+     Then reset var and forwardingAddress arrays in the problem,
+     so that they will correctly refer to the reconstructed
+     mappedVars. */
+  Variable_ID_Tuple unsubbed_vars(c->problem->safeVars);
+  for(i = 1; i <= c->mappedVars.size(); i++) 
+    if(c->mappedVars[i]->kind() != Wildcard_Var) {
+      int addr = c->problem->forwardingAddress[i];
+      assert(addr == c->find_column(c->mappedVars[i]) && addr != 0);
+      if(addr < 0) {
+        assert(-addr <= subbed_vars.size());
+        subbed_vars[-addr] = c->mappedVars[i];
+      }
+      else {
+        assert(addr <= unsubbed_vars.size());
+        unsubbed_vars[addr] = c->mappedVars[i];
+      }
+    }
+    else {
+      // Here we don't redeclare wildcards, just re-use them.
+      unsubbed_vars.append(c->mappedVars[i]);
+    }
+  assert(unsubbed_vars.size() + subbed_vars.size() == c->mappedVars.size());
+  c->mappedVars = unsubbed_vars; /* These are the variables that remain */
+     
+  for(int col = 1; col <= c->problem->nVars; col++) {
+    c->problem->var[col] = col;
+    c->problem->forwardingAddress[col] = col;
+  }
+}
+
+Substitutions::~Substitutions() {
+  delete [] subs;
+  delete r;
+}
+
+bool Substitutions::substituted(Variable_ID v) {
+  return (subbed_vars.index(v) > 0);
+}
+
+Sub_Handle Substitutions::get_sub(Variable_ID v) {
+  assert(substituted(v) && "No substitution for variable");
+  return Sub_Handle(this,subbed_vars.index(v)-1,v);
+}
+
+bool Substitutions::sub_involves(Variable_ID v, Var_Kind kind) {
+  assert(substituted(v));
+  for(Constr_Vars_Iter i = get_sub(v); i; i++)
+    if ((*i).var->kind() == kind)
+      return true;
+  return false;
+}
+
+
+//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
+
+
+int Sub_Iterator::live() const {
+  return current <= last;
+}
+
+void Sub_Iterator::operator++() { this->operator++(0); }
+
+void Sub_Iterator::operator++(int) {
+  current++;
+}
+
+Sub_Handle Sub_Iterator::operator*() {
+  assert(s && current <= last && "Sub_Iterator::operator*: bad call");
+  return Sub_Handle(s,current,s->subbed_vars[current+1]);
+} 
+
+Sub_Handle Sub_Iterator::operator*() const {
+  assert(s && current <= last && "Sub_Iterator::operator*: bad call");
+  return Sub_Handle(s,current,s->subbed_vars[current+1]);
+} 
+
+
+//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
+
+
+
+Sub_Handle::Sub_Handle(Substitutions *_s, int _e, Variable_ID _v) :
+Constraint_Handle(_s->c,&(_s->subs),_e), v(_v) {}
+
+std::string Sub_Handle::print_to_string() const {
+  relation()->setup_names();
+  return v->name() + " = " +  this->print_term_to_string();
+}
+
+std::string Sub_Handle::print_term_to_string() const {
+  /* The horrible truth is that print_term_to_string is a member
+     function of Conjunct, (and then Problem below it) but uses
+     nothing from there but the names, so you can pass it a pointer to
+     an equation that isn't even part of the conjunct. */
+  relation()->setup_names();
+  return c->print_term_to_string(&((*eqns)[e]));
+}
+
+
+/*
+  String Sub_Handle::print_to_string() const {
+  return c->problem->print_EQ_to_string(&((*eqns)[e]));
+  }
+
+  String Sub_Handle::print_term_to_string() const {
+  return c->print_term_to_string(&(*eqns[e]));
+  }
+*/
+
+} // namespace