1 files changed, 339 insertions, 0 deletions
diff --git a/omega/omega_lib/src/evac.cc b/omega/omega_lib/src/evac.cc
new file mode 100644
index 0000000..ff872c9
--- /dev/null
+++ b/omega/omega_lib/src/evac.cc
@@ -0,0 +1,339 @@
+#if defined STUDY_EVACUATIONS
+
+#include <omega/Relations.h>
+#include <omega/pres_conj.h>
+#include <omega/evac.h>
+#include <omega/omega_core/debugging.h>
+#include <omega/omega_core/oc_i.h>
+
+namespace omega {
+
+int evac_debug = 0;
+
+char *evac_names[] = { "trivial",
+                       "offset",
+                       "subseq",
+                       "off_sub",
+//         "perm.",
+                       "affine",
+                       "nasty" };
+ 
+int single_evacs[evac_nasty+1];
+int double_evacs[evac_nasty+1][evac_nasty+1];
+
+/*
+ * We're going to try to describe the equalities among a set of variables
+ * We want to perform some substitutions to ensure that we don't miss
+ *   v_1 = v_2 due to its expression as v_1 = v_3 && v_2 = v_3
+ * We therefore try to substitute out all variables that we don't care
+ *   about (e.g., v_3 in the above example).
+ */
+
+static bool try_to_sub(Problem *p, int col) {
+  int e, i;
+
+  if (!p->variablesInitialized) {
+    p->initializeVariables();
+  }
+
+  assert(col <= p->nVars);
+  assert(!inApproximateMode);
+
+  for(e=0;e<p->nEQs;e++)
+    if (p->EQs[e].coef[col] == 1 || p->EQs[e].coef[col] == -1) {
+      int var = p->var[col];
+      p->doElimination(e, col);
+      if (col != p->nVars + 1)
+        p->forwardingAddress[p->var[p->nVars+1]] = col;
+      assert(p->SUBs[p->nSUBs-1].key = var);
+      p->forwardingAddress[var] = -p->nSUBs;
+      break;
+    }
+ 
+  if (e == p->nEQs)
+    return false;
+
+  for (int c=0;c<=p->nVars;c++) {
+    assert(p->EQs[e].coef[c] == 0);
+  }
+
+  p->nEQs--;
+  if (e < p->nEQs) eqnncpy(&p->EQs[e], &p->EQs[p->nEQs], p->nVars);
+
+  for (i = 0; i < p->nSUBs; i++) {
+    assert(p->forwardingAddress[p->SUBs[i].key] == -i - 1);
+  }
+
+  return true;
+}
+
+
+// should be static, but must be a 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) {
+  // check each position v to see if from[v] == to[v+n] (+ offset)
+    
+  assert(max_arity + n <= n_to);
+
+  for (int v = 1; v <= max_arity; v++){
+    // first, get rid of possible interlopers:
+    int col;
+    Conjunct *d = c->copy_conj_same_relation();
+    for (int tv = 1; tv <= n_to; tv++)
+      if (tv != v+n)
+        if ((col = d->find_column(evac_to[tv])) > 0)
+          try_to_sub(d->problem, col);
+    for (int fv = 1; fv <= n_from; fv++)
+      if (fv != v)
+        if ((col = d->find_column(evac_from[fv])) > 0)
+          try_to_sub(d->problem, col);
+
+    int c_to = d->find_column(evac_to[v+n]);
+    int c_from = d->find_column(evac_from[v]);
+    assert(c_to > 0);
+    assert(c_from > 0);
+    assert(c_to != c_from);
+
+    // now, just look for an equality c_to = c_from + offset
+
+    bool found_needed_eq = false;
+
+    for (int e = 0; e < d->problem->nEQs; e++) {
+      if (d->problem->EQs[e].coef[c_from] != 0) {
+        for (int k = allow_offset?1:0; k < d->problem->nVars; k++)
+          if (k!=c_to && k!=c_from && d->problem->EQs[e].coef[k]!=0)
+            break;  // this EQ is not what we need
+        if (k == d->problem->nVars) { // this EQ is what we need
+          found_needed_eq = true;
+          break;
+        }
+      }
+    }
+
+    delete d;
+
+    if (!found_needed_eq)
+      return false;  // no EQ did what we need
+  }
+
+  return true;
+}
+
+void assert_subbed_syms(Conjunct *c) {
+  int v, col;
+
+  // where possible, symbolic constants must have been subbed out
+  for (v = 1; v <= c->relation()->global_decls()->length(); v++)
+    if ((col = c->find_column((*c->relation()->global_decls())[v]))>0)
+      assert(!try_to_sub(c->problem, col));
+}
+
+
+static bool check_offset(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity) {
+  assert_subbed_syms(c);
+
+  return check_subseq_n(c,evac_from,evac_to,n_from,n_to,max_arity,0,true);
+}
+
+static bool check_subseq(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity) {
+  assert_subbed_syms(c);
+
+  for (int i = 0; i <= n_to - max_arity; i++)
+    if (check_subseq_n(c,evac_from,evac_to,n_from,n_to,max_arity,i,false))
+      return true;
+
+  return false;
+}
+
+static bool check_offset_subseq(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity) {
+  assert_subbed_syms(c);
+
+  for (int i = 0; i <= n_to - max_arity; i++)
+    if (check_subseq_n(c,evac_from,evac_to,n_from,n_to,max_arity,i,true))
+      return true;
+
+  return false;
+}
+
+bool check_affine(Conjunct *d, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity) {
+  int v, col;
+  Conjunct *c = d->copy_conj_same_relation();
+  assert_subbed_syms(c);
+
+  // try to find substitutions for all evac_to variables
+  for (v = 1; v <= max_arity; v++)
+    if ((col = c->find_column(evac_to[v])) > 0)
+      try_to_sub(c->problem, col);
+    
+  // any that didn't have substitutions, aren't affine
+  for (v = 1; v <= max_arity; v++)
+    if (c->find_column(evac_to[v]) >= 0) {
+      delete c;
+      return false;
+    }
+
+  // FERD - disallow symbolic constants?
+  delete c;
+  return true;
+}
+
+
+evac study(Conjunct *C, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity) {
+  assert(max_arity > 0);
+  assert(max_arity <= C->relation()->n_inp());
+  assert(max_arity <= C->relation()->n_out());
+
+  assert((&evac_from == &input_vars && &evac_to == &output_vars) ||
+         (&evac_from == &output_vars && &evac_to == &input_vars));
+
+  evac ret = evac_nasty;
+
+  if (C->query_guaranteed_leading_0s() >= max_arity)
+    ret = evac_trivial;
+  else {
+    Conjunct *c = C->copy_conj_same_relation();
+    assert(c->relation() == C->relation());
+
+    if (evac_debug >= 3) {
+      fprintf(DebugFile, "About to study %s evacuation for conjunct\n",
+              &evac_from == &input_vars ? "In-->Out" : "Out-->In");
+      use_ugly_names++;
+      C->prefix_print(DebugFile);
+      use_ugly_names--;
+    }
+
+    bool sat = simplify_conj(c, true, 4, black);
+    assert(sat);  // else c is deleted
+
+    int v, col;
+
+    // Substitute out all possible symbolic constants
+    assert(c->problem->nSUBs == 0);
+    for (v = 1; v <= c->relation()->global_decls()->length(); v++)
+      if ((col = c->find_column((*c->relation()->global_decls())[v]))>0)
+        try_to_sub(c->problem, col);
+
+    if (check_offset(c, evac_from, evac_to, n_from, n_to, max_arity))
+      ret = evac_offset;
+    else if (check_subseq(c, evac_from, evac_to, n_from, n_to, max_arity))
+      ret = evac_subseq;
+    else if (check_offset_subseq(c, evac_from, evac_to, n_from, n_to, max_arity))
+      ret = evac_offset_subseq;
+    else if (check_affine(c, evac_from, evac_to, n_from, n_to, max_arity))
+      ret = evac_affine;
+
+    delete c;
+  }
+
+  if (evac_debug >= 2) {
+    if ((evac_debug == 2 && ret != evac_trivial && ret != evac_nasty)) {
+      fprintf(DebugFile, "Studied %s evacuation for conjunct\n",
+              &evac_from == &input_vars ? "In-->Out" : "Out-->In");
+      use_ugly_names++;
+      C->prefix_print(DebugFile);
+      use_ugly_names--;
+    }
+
+    fprintf(DebugFile, "Saw evacuation type %s\n", evac_names[ret]);
+  }
+
+  return ret;
+}
+
+
+void study_evacuation(Conjunct *C, which_way dir, int max_arity) {
+  if (evac_debug > 0) {
+    assert(max_arity >= 0);
+
+    if (max_arity > 0)
+      if (dir == in_to_out) {
+        assert(max_arity <= C->relation()->n_inp());
+        if (max_arity <= C->relation()->n_out())
+          single_evacs[study(C, input_vars, output_vars,
+                             C->relation()->n_inp(),
+                             C->relation()->n_out(),
+                             max_arity)]++;
+      }
+      else {
+        assert(max_arity <= C->relation()->n_out());
+        if (max_arity <= C->relation()->n_inp())
+          single_evacs[study(C, output_vars, input_vars,
+                             C->relation()->n_out(),
+                             C->relation()->n_inp(),
+                             max_arity)]++;
+      }
+  }
+}
+
+void study_evacuation(Conjunct *C1, Conjunct *C2, int max_arity) {
+  if (evac_debug > 0) {
+    assert(max_arity >= 0);
+    assert(max_arity <= C1->relation()->n_inp());
+    assert(C2->relation()->n_out() == C1->relation()->n_inp());
+
+    if (max_arity > 0)
+      if (max_arity <= C1->relation()->n_out() &&
+          max_arity <= C2->relation()->n_inp()) {
+        double_evacs[study(C1, input_vars, output_vars, 
+                           C1->relation()->n_inp(),
+                           C1->relation()->n_out(),
+                           max_arity)]
+          [study(C2, output_vars, input_vars,
+                 C2->relation()->n_out(),
+                 C2->relation()->n_inp(),
+                 max_arity)]++;
+      }
+      else if (max_arity <= C1->relation()->n_out()) {
+        single_evacs[study(C1, input_vars, output_vars,
+                           C1->relation()->n_inp(),
+                           C1->relation()->n_out(),
+                           max_arity)]++;
+      }
+      else if (max_arity <= C2->relation()->n_inp()) {
+        single_evacs[study(C2, output_vars, input_vars,
+                           C2->relation()->n_out(),
+                           C2->relation()->n_inp(),
+                           max_arity)]++;
+      }
+  }
+}
+
+class Evac_info_printer {
+public:
+  ~Evac_info_printer();
+};
+
+Evac_info_printer::~Evac_info_printer() {
+  if (evac_debug > 0) {
+    int i, j;
+
+    fprintf(DebugFile, "\n");
+
+    fprintf(DebugFile, "SINGLE");
+    for (i = 0; i <= evac_nasty; i++)
+      fprintf(DebugFile, "\t%s", evac_names[i]);
+    fprintf(DebugFile, "\n");
+ 
+    for (i = 0; i <= evac_nasty; i++)
+      fprintf(DebugFile, "\t%d", single_evacs[i]);
+    fprintf(DebugFile, "\n\n");
+ 
+ 
+    fprintf(DebugFile, "DOUBLE");
+    for (i = 0; i <= evac_nasty; i++)
+      fprintf(DebugFile, "\t%s", evac_names[i]);
+    fprintf(DebugFile, "\n");
+ 
+    for (i = 0; i <= evac_nasty; i++) {
+      fprintf(DebugFile, "%s\t", evac_names[i]);
+      for (j = 0; j <= evac_nasty; j++)
+        fprintf(DebugFile, "%d\t", double_evacs[i][j]);
+      fprintf(DebugFile, "\n");
+    }
+  }
+}
+
+static Evac_info_printer print_stats_at_exit;
+
+} // namespace
+
+#endif