#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