/*****************************************************************************
 Copyright (C) 1994-2000 the Omega Project Team
 Copyright (C) 2005-2011 Chun Chen
 All Rights Reserved.

 Purpose:
   class Conjunct.

 Notes:

 History:
*****************************************************************************/

#include <omega/omega_core/oc.h>
#include <omega/pres_conj.h>
#include <omega/pres_cmpr.h>
#include <omega/Relation.h>
#include <omega/omega_i.h>
#include <set>

namespace omega {

int NR_CONJUNCTS, MAX_CONJUNCTS;

/*
 * Make a new wildcard variable, return WC number.
 * Should be static to this file, but must be a friend of conjunct.
 */
int new_WC(Conjunct *nc, Problem *) {
  Variable_ID wc = nc->declare();
  int wc_no = nc->map_to_column(wc);
  return(wc_no);
}


const char* get_var_name(unsigned int col, void * void_conj) {
#if defined PRINT_COLUMN_NUMBERS
  static char scum[512];
#endif
  Conjunct *c = (Conjunct *) void_conj;
  if (col == 0)
    return 0;
  Variable_ID v = c->mappedVars[col];
  assert(v!=0);
#if defined PRINT_COLUMN_NUMBERS
  strcpy(scum, v->char_name());
  sprintf(scum + strlen(scum), "(%d)", col);
  return scum;
#endif
  return v->char_name();
}

void Conjunct::promise_that_ub_solutions_exist(Relation &R) {
#ifndef NDEBUG
  Relation verify=Relation(R, this);
  assert(verify.is_upper_bound_satisfiable());
#endif 
  verified = true;
}


int Conjunct::max_ufs_arity_of_set() {
  int ma = 0, a;
  for (Variable_ID_Iterator v(mappedVars); v; v++)
    if ((*v)->kind() == Global_Var && (*v)->function_of() == Set_Tuple 
        && query_variable_used(*v)) {
      a = (*v)->get_global_var()->arity();
      if (a > ma)
        ma = a;
    }
  return ma;
}


int Conjunct::max_ufs_arity_of_in() {
  int ma = 0, a;
  for (Variable_ID_Iterator v(mappedVars); v; v++)
    if ((*v)->kind() == Global_Var && (*v)->function_of() == Input_Tuple
        && query_variable_used(*v)) {
      a = (*v)->get_global_var()->arity();
      if (a > ma)
        ma = a;
    }
  return ma;
}


int Conjunct::max_ufs_arity_of_out() {
  int ma = 0, a;
  for (Variable_ID_Iterator v(mappedVars); v; v++)
    if ((*v)->kind() == Global_Var &&  (*v)->function_of() == Output_Tuple
        && query_variable_used(*v)) {
      a = (*v)->get_global_var()->arity();
      if (a > ma)
        ma = a;
    }
  return ma;
}


bool Conjunct::is_unknown() const { 
  assert(problem || comp_problem);
  return !exact && ((problem && problem->nEQs==0 && problem->nGEQs==0) ||
                    (comp_problem && comp_problem->no_constraints()));
}


/*
 * Remove black constraints from the problem.
 * Make all the remaining red constraints black.
 */
void Conjunct::rm_color_constrs() {
  int geqs = 0, eqs = 0;

  possible_leading_0s = -1;
  guaranteed_leading_0s = -1;
  leading_dir = 0;

  for(int i=0; i<problem->nGEQs; i++) {
    if(problem->GEQs[i].color) {
      if(geqs!=i)
        eqnncpy(&problem->GEQs[geqs], &problem->GEQs[i], problem->nVars);
      problem->GEQs[geqs].color = EQ_BLACK;
      geqs++;
    }
  }
  problem->nGEQs = geqs;
  
  for(int i=0; i<problem->nEQs; i++) {
    if(problem->EQs[i].color) {
      if(eqs!=i)
        eqnncpy(&problem->EQs[eqs], &problem->EQs[i], problem->nVars);
      problem->EQs[eqs].color = EQ_BLACK;
      eqs++;
    }
  }
  problem->nEQs = eqs;
}



//
// Conjunct constructors.
//
Conjunct::Conjunct() : 
  F_Declaration(NULL, NULL),
  mappedVars(0),
  n_open_constraints(0),
  cols_ordered(false),
  simplified(false),
  verified(false),
  guaranteed_leading_0s(-1),
  possible_leading_0s(-1),
  leading_dir(0),
  exact(true),
  r_constrs(0) {
  NR_CONJUNCTS++;
  if (NR_CONJUNCTS>MAX_CONJUNCTS) MAX_CONJUNCTS = NR_CONJUNCTS;
  problem = new Problem;
  comp_problem = NULL;
  problem->get_var_name = get_var_name;
  problem->getVarNameArgs = (void *) this;
}


Conjunct::Conjunct(Formula *f, Rel_Body *r) : 
  F_Declaration(f,r),
  mappedVars(0),
  n_open_constraints(0),
  cols_ordered(false),
  simplified(false),
  verified(false),
  guaranteed_leading_0s(-1),
  possible_leading_0s(-1),
  leading_dir(0),
  exact(true),
  r_constrs(0) { 
  NR_CONJUNCTS++;
  if (NR_CONJUNCTS>MAX_CONJUNCTS) MAX_CONJUNCTS = NR_CONJUNCTS;
  problem = new Problem;
  comp_problem = NULL;
  problem->get_var_name = get_var_name;
  problem->getVarNameArgs = (void *) this ;
}

void internal_copy_conjunct(Conjunct* to, Conjunct* fr);

//
// Copy Conjunct.
//
Conjunct* Conjunct::copy_conj_diff_relation(Formula *parent, Rel_Body *rel_body) {
  Conjunct *new_conj;
  if(problem && comp_problem==NULL) {
    new_conj = new Conjunct(parent, rel_body);
    internal_copy_conjunct(new_conj, this);
  }
  else if (problem==NULL && comp_problem) {
    /* copy compressed conjunct */
    assert(0 && "copy compressed conjunct");
    new_conj = 0;
  }
  else {
    assert(0 && "problem == NULL");
    new_conj = 0;
  }
  return new_conj;
}


void internal_copy_conjunct(Conjunct* to, Conjunct* fr) {
  copy_conj_header(to, fr);

  // 
  // We repeat part of what is done by copy_conj_header(to, fr) by
  // calling Problem::operator=(const Problem &).  
  // copy_conj_header should go away, but there is some code that still needs 
  // it in negate_conj.  
  //
  to->r_constrs = fr->r_constrs;
  to->simplified = fr->simplified;
  to->verified = fr->verified;
  to->guaranteed_leading_0s = fr->guaranteed_leading_0s;
  to->possible_leading_0s = fr->possible_leading_0s;
  to->leading_dir = fr->leading_dir;
  // the following duplicates some work of the "copy_conj_header" brain damage
  *to->problem = *fr->problem; 
  to->problem->getVarNameArgs = (void *)to;   // important
}


//
// Copy Conjunct variable declarations
// and problem parameters but not problem itself.
//
void copy_conj_header(Conjunct* to, Conjunct* fr) {
  free_var_decls(to->myLocals);  to->myLocals.clear();

  copy_var_decls(to->myLocals, fr->myLocals);
  to->mappedVars = fr->mappedVars;
  to->remap();
  reset_remap_field(fr->myLocals);

  to->cols_ordered = fr->cols_ordered;
  to->r_constrs = fr->r_constrs;
  to->simplified = fr->simplified;
  to->verified = fr->verified;
  to->guaranteed_leading_0s = fr->guaranteed_leading_0s;
  to->possible_leading_0s = fr->possible_leading_0s;
  to->leading_dir = fr->leading_dir;
  to->n_open_constraints = fr->n_open_constraints;
  to->exact=fr->exact;

  Problem *fp = fr->problem;
  Problem *tp = to->problem;
  tp->nVars = fp->nVars;
  tp->safeVars = fp->safeVars;
  tp->variablesInitialized = fp->variablesInitialized;
  tp->variablesFreed = fp->variablesFreed;
  for(int i=1; i<=maxVars; i++) {  // only need nVars of var
    tp->forwardingAddress[i] = fp->forwardingAddress[i];
    tp->var[i] = fp->var[i];
  }
  to->problem->get_var_name = get_var_name;
  to->problem->getVarNameArgs = (void *)to ;
}


void Conjunct::reverse_leading_dir_info() {
  leading_dir *= -1;
}


void Conjunct::enforce_leading_info(int guaranteed, int possible, int dir) {
  skip_finalization_check++;
  guaranteed_leading_0s = guaranteed;

  int d = min(relation()->n_inp(),relation()->n_out());

  assert(0 <= guaranteed);
  assert(guaranteed <= possible);
  assert(possible <= d);

  for(int i = 1; i <= guaranteed; i++) {
    EQ_Handle e = add_EQ();
    e.update_coef_during_simplify(input_var(i), -1);
    e.update_coef_during_simplify(output_var(i), 1);
    e.finalize();
  }


  if (guaranteed == possible && guaranteed >= 0  && possible+1 <= d && dir) {
    GEQ_Handle g = add_GEQ();
    if (dir > 0) {
      g.update_coef_during_simplify(input_var(possible+1), -1);
      g.update_coef_during_simplify(output_var(possible+1), 1);
    }
    else {
      g.update_coef_during_simplify(input_var(possible+1), 1);
      g.update_coef_during_simplify(output_var(possible+1), -1);
    }
    g.update_const_during_simplify(-1);
    g.finalize();
    possible_leading_0s = possible;
    leading_dir = dir;
  }
	else {
    possible_leading_0s = d;
    leading_dir = 0;
  }

  skip_finalization_check--;
#if ! defined NDEBUG
  assert_leading_info();
#endif
}
	

void Conjunct::invalidate_leading_info(int changed) {
  if (changed == -1) {
    guaranteed_leading_0s = possible_leading_0s = -1;
    leading_dir = 0;
	}
  else {
    int d = min(relation()->n_inp(), relation()->n_out());
    assert(1 <= changed && changed <= d);
    if (possible_leading_0s == changed -1) {
      possible_leading_0s  = d;
		}
    guaranteed_leading_0s = min(guaranteed_leading_0s,changed-1);
	}
#if ! defined NDEBUG
  assert_leading_info();
#endif
}


int Conjunct::leading_dir_valid_and_known() {
  if (relation()->is_set()) {
    return 0;
	}
  // if we know leading dir, we can rule out extra possible 0's
  assert(leading_dir == 0 ||
         possible_leading_0s == guaranteed_leading_0s);

  return (possible_leading_0s == guaranteed_leading_0s &&
          possible_leading_0s >= 0 &&
          possible_leading_0s < min(relation()->n_inp(),relation()->n_out())
          && leading_dir);
}


#if ! defined NDEBUG
void Conjunct::assert_leading_info() {
  if (relation()->is_set()) {
    return;
	}

  int d = min(relation()->n_inp(), relation()->n_out());

  if ( guaranteed_leading_0s == -1
       && guaranteed_leading_0s == possible_leading_0s)
    assert(leading_dir == 0);
 
  if(leading_dir != 0 && 
	   possible_leading_0s != guaranteed_leading_0s) {
    use_ugly_names++;
    prefix_print(DebugFile);
    use_ugly_names--;
	}
	
  assert(leading_dir == 0 || possible_leading_0s == guaranteed_leading_0s);

  assert(possible_leading_0s <= d && guaranteed_leading_0s <= d);

  assert(possible_leading_0s == -1 || guaranteed_leading_0s <= possible_leading_0s);

  // check that there must be "guaranteed_leading_0s" 0s
  int carried_level;
  for (carried_level = 1; carried_level <= guaranteed_leading_0s; carried_level++) {
    Variable_ID in = input_var(carried_level),
	    out = output_var(carried_level);
    coef_t lb, ub;
    bool guar;
    query_difference(out, in, lb, ub, guar);
    if (lb != 0 && ub != 0) {
	    // probably "query_difference" is just approximate
	    // add the negation of leading_dir and assert that
	    // the result is unsatisfiable;
	    // add in > out (in-out-1>=0) and assert unsatisfiable.

	    Conjunct *test = copy_conj_same_relation();
	    test->problem->turnRedBlack();
	    skip_finalization_check++;
	    
	    GEQ_Handle g = test->add_GEQ();
	    g.update_coef_during_simplify(in, -1);
	    g.update_coef_during_simplify(out, 1);
	    g.update_const_during_simplify(-1);
	    g.finalize();
	    assert(!simplify_conj(test, true, 0, 0));
	    // test was deleted by simplify_conj, as it was FALSE

	    test = copy_conj_same_relation();
	    test->problem->turnRedBlack();
	    g = test->add_GEQ();
	    g.update_coef_during_simplify(in, 1);
	    g.update_coef_during_simplify(out, -1);
	    g.update_const_during_simplify(-1);
	    g.finalize();
	    assert(!simplify_conj(test, true, 0, 0));
	    // test was deleted by simplify_conj, as it was FALSE

	    skip_finalization_check--;
    }
	}

  carried_level = possible_leading_0s+1;

  // check that there can't be another
  if (guaranteed_leading_0s == possible_leading_0s
      && possible_leading_0s >= 0 &&
      carried_level <= min(relation()->n_inp(), relation()->n_out()))	{
    Variable_ID in = input_var(carried_level),
	    out = output_var(carried_level);
    coef_t lb, ub;
    bool guar;
    query_difference(out, in, lb, ub, guar);
    if (lb <= 0 && ub >= 0) {
	    // probably "query_difference" is just approximate
	    // add a 0 and see if its satisfiable

	    Conjunct *test = copy_conj_same_relation();
	    test->problem->turnRedBlack();
	    skip_finalization_check++;

	    EQ_Handle e = test->add_EQ();
	    e.update_coef_during_simplify(in, -1);
	    e.update_coef_during_simplify(out, 1);
	    e.finalize();
	    assert(!simplify_conj(test, true, 0, 0));
	    // test was deleted by simplify_conj, as it was FALSE

	    skip_finalization_check--;
    }
	}

  // check leading direction info
  if (leading_dir_valid_and_known()) {
    Variable_ID in = input_var(guaranteed_leading_0s+1),
	    out = output_var(guaranteed_leading_0s+1);
    coef_t lb, ub;
    bool guar;
    query_difference(out, in, lb, ub, guar);
    if ((leading_dir < 0 && ub >= 0) ||
        (leading_dir > 0 && lb <= 0)) {
	    // probably "query_difference" is just approximate
	    // add the negation of leading_dir and assert that
	    // the result is unsatisfiable;
	    // eg for leading_dir = +1 (in must be < out),
	    // add in >= out (in-out>=0) and assert unsatisfiable.

	    Conjunct *test = copy_conj_same_relation();
	    test->problem->turnRedBlack();
	    skip_finalization_check++;
	    
	    GEQ_Handle g = test->add_GEQ();
	    g.update_coef_during_simplify(in, leading_dir);
	    g.update_coef_during_simplify(out, -leading_dir);
	    g.finalize();

	    assert(!simplify_conj(test, true, 0, 0));
	    // test was deleted by simplify_conj, as it was FALSE

	    skip_finalization_check--;
    }
	}
}
#endif


Variable_ID Conjunct::declare(Const_String s) {
  return do_declare(s, Wildcard_Var);
}

Variable_ID Conjunct::declare() {
  return do_declare(Const_String(), Wildcard_Var);
}

Variable_ID Conjunct::declare(Variable_ID v) {
  return do_declare(v->base_name, Wildcard_Var);
}

Conjunct* Conjunct::really_conjunct() {
  return this;
}


Variable_ID_Tuple* Conjunct::variables() {
  return &mappedVars;
}

Stride_Handle Conjunct::add_stride(int step, int preserves_level) {
  assert_not_finalized();
  Variable_ID wild = declare();
  int c;
  c = problem->newEQ();
  simplified = false;
  verified = false;
  if (! preserves_level) {
    if (leading_dir == 0)
	    possible_leading_0s = -1;
    // otherwise we must still have leading_dir, and thus no more 0's
	}
  problem->EQs[c].color = EQ_BLACK;
  eqnnzero(&problem->EQs[c],problem->nVars);
  n_open_constraints++;
  EQ_Handle h = EQ_Handle(this, c);
  h.update_coef(wild,step);
  return h;
}

// This should only be used to copy constraints from simplified relations, 
// i.e. there are no quantified variables in c except wildcards.
EQ_Handle Conjunct::add_EQ(const Constraint_Handle &c, int /*preserves_level, currently unused*/) {
  EQ_Handle e = add_EQ();
  copy_constraint(e,c);
  return e;
}


EQ_Handle Conjunct::add_EQ(int preserves_level) {
  assert_not_finalized();
  int c;
  c = problem->newEQ();
  simplified = false;
  verified = false;
  if (!preserves_level)	{
    if (leading_dir == 0)
	    possible_leading_0s = -1;
    // otherwise we must still have leading_dir, and thus no more 0's
	}
  problem->EQs[c].color = EQ_BLACK;
  eqnnzero(&problem->EQs[c],problem->nVars);
  n_open_constraints++;
  return EQ_Handle(this, c);
}


// This should only be used to copy constraints from simplified relations, 
// i.e. there are no quantified variables in c except wildcards.
GEQ_Handle Conjunct::add_GEQ(const Constraint_Handle &c, int /*preserves_level, currently unused */) {
  GEQ_Handle g = add_GEQ();
  copy_constraint(g,c);
  return g;
}


GEQ_Handle Conjunct::add_GEQ(int preserves_level) {
  assert_not_finalized();
  int c;
  c = problem->newGEQ();
  simplified = false;
  verified = false;
  if (!preserves_level)	{
    if (leading_dir == 0)
	    possible_leading_0s = -1;
    // otherwise we must still have leading_dir, and thus no more 0's
	}
  problem->GEQs[c].color = EQ_BLACK;
  eqnnzero(&problem->GEQs[c],problem->nVars);
  n_open_constraints++;
  return GEQ_Handle(this, c);
}


Conjunct *Conjunct::find_available_conjunct() {
	return this;
}


bool Conjunct::can_add_child() {
  return false;
}


void Conjunct::combine_columns() {
  int nvars = mappedVars.size(),i,j,k;

  for(i=1; i<=nvars; i++)
    for(j=i+1; j<=nvars; j++) {
      // If they are the same, copy into the higher numbered column.
      // That way we won't have problems with already-merged columns later
      assert(i != j);
      if(mappedVars[i] == mappedVars[j]) {
        if (pres_debug)
          fprintf(DebugFile, "combine_col:Actually combined %d,%d\n",
                  j,i);
        for(k=0; k<problem->nEQs; k++)
          problem->EQs[k].coef[j] += problem->EQs[k].coef[i];
        for(k=0; k<problem->nGEQs; k++)
          problem->GEQs[k].coef[j] += problem->GEQs[k].coef[i];
        zero_column(problem, i, 0, 0, problem->nEQs, problem->nGEQs);
        // Create a wildcard w/no constraints.  temporary measure, 
        // so we don't have to shuffle columns
        Variable_ID zero_var = declare();
        mappedVars[i] = zero_var;
        break;
      }
    }
}


void Conjunct::finalize() {
// Debugging version of finalize; copy the conjunct and free the old one,
// so that purify will catch accesses to finalized constraints
//    assert(n_open_constraints == 0);
//    Conjunct *C = this->copy();
//    parent().replace_child(this, C);
//    delete this;
}

Conjunct::~Conjunct() {
  NR_CONJUNCTS--;
  delete problem;
  delete comp_problem;
}


//
// Cost = # of terms in DNF when negated
//  or CantBeNegated if too bad (i.e. bad wildcards)
//  or AvoidNegating if it would be inexact
//
// Also check pres_legal_negations --
//   If set to any_negation, just return the number
//   If set to one_geq_or_stride, return CantBeNegated if c > 1
//   If set to one_geq_or_eq, return CantBeNegated if not a single geq or eq
//

int Conjunct::cost() {
  int c;
  int i;
  int wc_no;
  int wc_j = 0;  // initialize to shut up the compiler

  // cost 1 per GEQ, and if 1 GEQ has wildcards, +2 for each of them

  c = problem->nGEQs;
  for(i=0; i<problem->nGEQs; i++) {
    wc_no = 0;
    for(int j=1; j<=problem->nVars; j++) if(problem->GEQs[i].coef[j]!=0) {
        Variable_ID v = mappedVars[j];
        if(v->kind()==Wildcard_Var) {
          wc_no++;
          c+=2;
          wc_j = j;
        }
      }
    if (wc_no > 1) return CantBeNegated;
  }

  for(i=0; i<problem->nEQs; i++) {
    wc_no = 0;
    for(int j=1; j<=problem->nVars; j++) if(problem->EQs[i].coef[j]!=0) {
        Variable_ID v = mappedVars[j];
        if(v->kind()==Wildcard_Var) {
          wc_no++;
          wc_j = j;
        }
      }

    if (wc_no == 0)	  // no wildcards
      c+=2;
    else if (wc_no == 1) { // one wildcard - maybe we can negate it
      int i2;
      for(i2=0; i2<problem->nEQs; i2++)
        if(i != i2 && problem->EQs[i2].coef[wc_j]!=0)  break;
      if (i2 >= problem->nEQs)  // Stride constraint
        c++;
      else   // We are not ready to handle this
        return CantBeNegated;
    }
    else		  // Multiple wildcards
      return CantBeNegated;
  }
  if (!exact) return AvoidNegating;

  if (pres_legal_negations == any_negation) {
    return c;
  }
  else {
    // single GEQ ok either way as long as no wildcards
    // (we might be able to handle wildcards, but I haven't thought about it)
    if (problem->nEQs==0 && problem->nGEQs<=1) {
      if (c>1) { // the GEQ had a wildcard -- I'm not ready to go here.
	      if (pres_debug > 0) {
          fprintf(DebugFile,
                  "Refusing to negate a GEQ with wildcard(s)"
                  " under restricted_negation;  "
                  "It may be possible to fix this.\n");
        }
	      return CantBeNegated;
	    }
      return c;
    }
    else if (problem->nEQs==1 && problem->nGEQs==0) {
      assert(c == 1 || c == 2);

      if (pres_legal_negations == one_geq_or_stride) {
	      if (c == 1)
          return c;     // stride constraint is ok
	      else {
          if (pres_debug > 0) {
            fprintf(DebugFile, "Refusing to negate a non-stride EQ under current pres_legal_negations.\n");
          }
          return CantBeNegated;
        }
	    }
      else {
	      assert(pres_legal_negations == one_geq_or_eq);
	      return c;
	    }
    }
    else {
      if (pres_debug > 0) {
	      fprintf(DebugFile, "Refusing to negate multiple constraints under current pres_legal_negations.\n");
	    }
      return CantBeNegated;
    }
  }
}


//
// Merge CONJ1 & CONJ2 -> CONJ.
// Action: MERGE_REGULAR or MERGE_COMPOSE: regular merge.
//         MERGE_GIST    make constraints from conj2 red, i.e.
//                        Gist Conj2 given Conj1 (T.S. comment). 
// Reorder columns as we go.
// Merge the columns for identical variables.  
// We assume we know nothing about the ordering of conj1, conj2.
//
// Does not consume its arguments
//
// Optional 4th argument gives the relation for the result - if
//  null, conj1 and conj2 must have the same relation, which will
//  be used for the result
//
// The only members of conj1 and conj2 that are used are: problem,
//  mappedVars and declare(), and the leading_0s/leading_dir members
//  and exact.
//
// NOTE: variables that are shared between conjuncts are necessarily 
// declared above, not here; so we can simply create columns for the 
// locals of each conj after doing the protected vars.  
//
Conjunct* merge_conjs(Conjunct* conj1, Conjunct* conj2,
                      Merge_Action action, Rel_Body *body) {
  // body must be set unless both conjuncts are from the same relation
  assert(body || conj1->relation() == conj2->relation());

  if (body == conj1->relation() && body == conj2->relation())
    body = 0;  // we test this later to see if there is a new body

  Conjunct *conj3 = new Conjunct(NULL, body ? body : conj2->relation());
  Problem *p1 = conj1->problem;
  Problem *p2 = conj2->problem;
  Problem *p3 = conj3->problem;
  int i;

  if (action != MERGE_COMPOSE) {
    conj1->assert_leading_info();
    conj2->assert_leading_info();
	}

  if(pres_debug>=2) {
    use_ugly_names++;
    fprintf(DebugFile, ">>> Merge conjuncts: Merging%s:\n",
            (action == MERGE_GIST ? " for gist" :
             (action == MERGE_COMPOSE ? " for composition" : "")));
    conj1->prefix_print(DebugFile);
    conj2->prefix_print(DebugFile);
    fprintf(DebugFile, "\n");
    use_ugly_names--;
	}



  switch(action) {
  case MERGE_REGULAR:
  case MERGE_COMPOSE:
    conj3->exact=conj1->exact && conj2->exact;
    break;
  case MERGE_GIST:
    conj3->exact=conj2->exact;
    break;
	}

  if (action == MERGE_COMPOSE) {
    conj3->guaranteed_leading_0s=min(conj1->guaranteed_leading_0s,
                                     conj2->guaranteed_leading_0s);
    conj3->possible_leading_0s=min((unsigned int) conj1->possible_leading_0s,
                                   (unsigned int) conj2->possible_leading_0s);

    assert( conj3->guaranteed_leading_0s <= conj3->possible_leading_0s);

    // investigate leading_dir - not well tested code
    if (conj1->guaranteed_leading_0s<0 || conj2->guaranteed_leading_0s<0) {
	    conj3->leading_dir = 0;
    }
    else if (conj1->guaranteed_leading_0s == conj2->guaranteed_leading_0s)
	    if (conj1->leading_dir == conj2->leading_dir)
        conj3->leading_dir = conj1->leading_dir;
	    else
        conj3->leading_dir = 0;
    else if (conj1->guaranteed_leading_0s < conj2->guaranteed_leading_0s) {
	    conj3->leading_dir = conj1->leading_dir;
    }
    else { // (conj1->guaranteed_leading_0s > conj2->guaranteed_leading_0s)
	    conj3->leading_dir = conj2->leading_dir;
    }

    if (conj3->leading_dir == 0)
	    conj3->possible_leading_0s = min(conj3->relation()->n_inp(),
                                       conj3->relation()->n_out());

    assert(conj3->guaranteed_leading_0s <= conj3->possible_leading_0s);
    assert(conj3->guaranteed_leading_0s == conj3->possible_leading_0s
           || !conj3->leading_dir);
	}
  else if (!body) { // if body is set, who knows what leading 0's mean?
    assert(action == MERGE_REGULAR || action == MERGE_GIST);

    int feasable = 1;

    int redAndBlackGuarLeadingZeros = max(conj1->guaranteed_leading_0s,
                                          conj2->guaranteed_leading_0s);
    if (action == MERGE_REGULAR) 
	    conj3->guaranteed_leading_0s= redAndBlackGuarLeadingZeros;
    else conj3->guaranteed_leading_0s=conj1->guaranteed_leading_0s;

    conj3->possible_leading_0s=min((unsigned)conj1->possible_leading_0s,
                                   (unsigned)conj2->possible_leading_0s);
    if (conj3->possible_leading_0s < redAndBlackGuarLeadingZeros)
	    feasable = 0;
    else if (conj3->guaranteed_leading_0s == -1 
             || conj3->possible_leading_0s > redAndBlackGuarLeadingZeros)
	    conj3->leading_dir = 0;
    else {
	    if (conj1->guaranteed_leading_0s == conj2->guaranteed_leading_0s)
        if (!conj1->leading_dir_valid_and_known())
          conj3->leading_dir = conj2->leading_dir;
        else if (!conj2->leading_dir_valid_and_known())
          conj3->leading_dir = conj1->leading_dir;
        else if (conj1->leading_dir * conj2->leading_dir > 0)
          conj3->leading_dir = conj1->leading_dir; // 1,2 same dir
        else
          feasable = 0;  // 1 and 2 go in opposite directions
	    else if (conj3->possible_leading_0s != conj3->guaranteed_leading_0s)
        conj3->leading_dir = 0;
	    else if (conj1->guaranteed_leading_0s<conj2->guaranteed_leading_0s) {
        assert(!conj1->leading_dir_valid_and_known());
        conj3->leading_dir = conj2->leading_dir;
      }
	    else {
        assert(!conj2->leading_dir_valid_and_known());
        conj3->leading_dir = conj1->leading_dir;
      }
    }

    if (!feasable) {
	    if(pres_debug>=2)
        fprintf(DebugFile, ">>> Merge conjuncts: quick check proves FALSE.\n");

	    // return 0 = 1

	    int e = p3->newEQ(); 
	    p3->EQs[e].color   = EQ_BLACK;
	    p3->EQs[e].touched = 1;
	    p3->EQs[e].key     = 0;
	    p3->EQs[e].coef[0] = 1;

	    // Make sure these don't blow later assertions
	    conj3->possible_leading_0s = conj3->guaranteed_leading_0s = -1;
	    conj3->leading_dir = 0;

	    return conj3;
    }
	}
  else { // provided "body" argument but not composing, leading 0s meaningless
    conj3->guaranteed_leading_0s = conj3->possible_leading_0s = -1;
    conj3->leading_dir = 0;
	}

  // initialize omega stuff

  for(i=0; i<p1->nGEQs+p2->nGEQs; i++) {
    int e = p3->newGEQ();
    assert(e == i);
    p3->GEQs[e].color   = EQ_BLACK;
    p3->GEQs[e].touched = 1;
    p3->GEQs[e].key     = 0;
	}
  for(i=0; i<p1->nEQs+p2->nEQs; i++) {
    int e = p3->newEQ();
    assert(e == i);
    p3->EQs[e].color   = EQ_BLACK;
    p3->EQs[e].touched = 1;
    p3->EQs[e].key     = 0;
	}

  assert(p3->nGEQs == p1->nGEQs + p2->nGEQs);
  assert(p3->nEQs == p1->nEQs + p2->nEQs);

  // flag constraints from second constraint as red, if necessary  
  if (action == MERGE_GIST) {
    for(i=0; i<p2->nEQs; i++) {
	    p3->EQs[i+p1->nEQs].color = EQ_RED;
    }
    for(i=0; i<p2->nGEQs; i++) {
	    p3->GEQs[i+p1->nGEQs].color = EQ_RED;
    }
	}

  // copy constant column
  copy_column(p3, 0, p1, 0, 0, 0);
  copy_column(p3, 0, p2, 0, p1->nEQs, p1->nGEQs);
  
  // copy protected variables column from conj1
  int new_col = 1;
  Variable_Iterator VI(conj1->mappedVars);
  for(i=1; VI; VI++, i++) {
    Variable_ID v = *VI;
    if(v->kind() != Wildcard_Var) {
	    conj3->mappedVars.append(v);
	    int fr_ix = i;
	    copy_column(p3, new_col, p1, fr_ix, 0, 0);
	    zero_column(p3, new_col, p1->nEQs, p1->nGEQs,
                  p2->nEQs, p2->nGEQs);
	    new_col++;
    }
	}
  
  // copy protected variables column from conj2,
  // checking if conj3 already has this variable from conj1
  for(i=1; i <= conj2->mappedVars.size(); i++) {
    Variable_ID v = conj2->mappedVars[i];
    if(v->kind() != Wildcard_Var) {
	    int to_ix = conj3->mappedVars.index(v);
	    int fr_ix = i;
	    if(to_ix > 0) {
        // use old column
        copy_column(p3, to_ix, p2, fr_ix, p1->nEQs, p1->nGEQs);
      }
	    else {
        // create new column
        conj3->mappedVars.append(v);
        zero_column(p3, new_col, 0, 0, p1->nEQs, p1->nGEQs);
        copy_column(p3, new_col, p2, fr_ix, p1->nEQs, p1->nGEQs);
        new_col++;
      }
    }
	}

  p3->safeVars = new_col-1;
  
  // copy wildcards from conj1
  for(i=1; i <= conj1->mappedVars.size(); i++) {
    Variable_ID v = conj1->mappedVars[i];
    if(v->kind() == Wildcard_Var) {
	    Variable_ID nv = conj3->declare(v);
	    conj3->mappedVars.append(nv);
	    int fr_ix = i;
	    copy_column(p3, new_col, p1, fr_ix, 0, 0);
	    zero_column(p3, new_col, p1->nEQs, p1->nGEQs,
                  p2->nEQs, p2->nGEQs);
	    new_col++;
    }
	}
  
  // copy wildcards from conj2
  for(i=1; i <= conj2->mappedVars.size(); i++) {
    Variable_ID v = conj2->mappedVars[i];
    if(v->kind() == Wildcard_Var) {
	    Variable_ID nv = conj3->declare(v);
	    conj3->mappedVars.append(nv);
	    int fr_ix = i;
	    zero_column(p3, new_col, 0, 0, p1->nEQs, p1->nGEQs);
	    copy_column(p3, new_col, p2, fr_ix, p1->nEQs, p1->nGEQs);
	    new_col++;
    }
	}
 
  p3->nVars = new_col-1;
  checkVars(p3->nVars);
  p3->variablesInitialized = 1;
  for(i=1; i<=p3->nVars; i++)
    p3->var[i] = p3->forwardingAddress[i] = i;
    
  conj3->cols_ordered = true;
  conj3->simplified = false;
  conj3->verified = false;
    
  if(pres_debug>=2) {
    use_ugly_names++;
    fprintf(DebugFile, ">>> Merge conjuncts: result is:\n");
    conj3->prefix_print(DebugFile);
    fprintf(DebugFile, "\n");
    use_ugly_names--;
	}

  conj3->assert_leading_info();

  return conj3;
}




//
// Reorder variables by swapping.
// cols_ordered is just a hint that thorough check needs to be done.
// Sets _safeVars.
// 
void Conjunct::reorder() {
  if(!cols_ordered) {
    int var_no = mappedVars.size();
    int first_wild = 1;
    int last_prot = var_no;
    while(first_wild < last_prot) {
      for(; first_wild<=var_no && mappedVars[first_wild]->kind()!=Wildcard_Var;
          first_wild++) ;
      for(; last_prot>=1 && mappedVars[last_prot]->kind()==Wildcard_Var;
          last_prot--) ;
      if(first_wild < last_prot) {
        problem->swapVars(first_wild, last_prot);
        problem->variablesInitialized = false;
        Var_Decl *t = mappedVars[first_wild];
        mappedVars[first_wild] = mappedVars[last_prot];
        mappedVars[last_prot] = t;
        if(pres_debug) {
          fprintf(DebugFile, "<<<OrderConjCols>>>: swapped var-s %d and %d\n", first_wild, last_prot);
        }
      }
    }

    int safe_vars;
    for(safe_vars=0;
        safe_vars<var_no && mappedVars[safe_vars+1]->kind()!=Wildcard_Var;
        safe_vars++) ;

#if ! defined NDEBUG
    for(int s = safe_vars ; s<var_no ; s++ ) {
      assert(mappedVars[s+1]->kind() == Wildcard_Var);
    }
#endif

    problem->safeVars = safe_vars;
    cols_ordered = true;
  }
}



// Wherever possible, move function symbols to input tuple.
// This ensures that if in == out, red F(in) = x is redundant
// with black F(out) = x

void Conjunct::move_UFS_to_input() {  
  if (guaranteed_leading_0s > 0) {
    std::set<Global_Var_ID> already_done;
    int remapped = 0;
    skip_finalization_check++;
    Rel_Body *body = relation();

    assert(body);
	
    for (Variable_ID_Iterator func(*body->global_decls()); func; func++) {
	    Global_Var_ID f = (*func)->get_global_var();
	    if (f->arity() <= guaranteed_leading_0s)
        if (already_done.find(f) == already_done.end() &&
            body->has_local(f, Input_Tuple) &&
            body->has_local(f, Output_Tuple)) {
          already_done.insert(f);

          // equatE f(in) = f(out)
          Variable_ID f_in  = body->get_local(f, Input_Tuple);
          Variable_ID f_out = body->get_local(f, Output_Tuple);
          if (f_in != f_out) {
            EQ_Handle e = add_EQ(1);
		
            e.update_coef_during_simplify(f_in, -1);
            e.update_coef_during_simplify(f_out, 1);
		
            f_out->remap = f_in;
            remapped = 1;
          }
        }	    
    }

    if (remapped) {
	    remap();
	    combine_columns();
	    reset_remap_field(*body->global_decls());
	    remapped = 0;
    }
	
    skip_finalization_check--;
	}
}





//
// Simplify CONJ.
// Return TRUE if there are solutions, FALSE -- no solutions.
//
int simplify_conj(Conjunct* conj, int ver_sim, int simplificationEffort, int color) {
  if (conj->verified 
      && simplificationEffort <= conj->r_constrs 
      && (conj->simplified  || simplificationEffort < 0)
      && !color) {
	  if(pres_debug) {
	    fprintf(DebugFile, "$$$ Redundant simplify_conj ignored (%d,%d,%d)\n",ver_sim,simplificationEffort,color);
	    conj->prefix_print(DebugFile);
    }
	  return 1;
  }

  if (simplificationEffort < 0) simplificationEffort = 0;
  conj->move_UFS_to_input();
  conj->reorder();

  Problem *p = conj->problem;

  use_ugly_names++;

  int i;
  for(i=0; i<p->nGEQs; i++) {
    p->GEQs[i].touched = 1;
  }
  for(i=0; i<p->nEQs; i++) {
    p->EQs[i].touched = 1;
  }

  if(pres_debug) {
    fprintf(DebugFile, "$$$ simplify_conj (%d,%d,%d)[\n",ver_sim,simplificationEffort,color);
    conj->prefix_print(DebugFile);
  }

  assert(conj->cols_ordered);

  int ret_code;
  assert(p == conj->problem);
  if(!color) {
    ret_code = conj->simplifyProblem(ver_sim && ! conj->verified,0,simplificationEffort);
  }
  else {
    ret_code = conj->redSimplifyProblem(simplificationEffort,1);
    ret_code = (ret_code==redFalse ? 0 : 1);
  }
  assert(p->nSUBs==0);

  if(ret_code == 0) {
    if(pres_debug)
      fprintf(DebugFile, "] $$$ simplify_conj : false\n\n");
    delete conj;
    use_ugly_names--;
    return(false);
  }


  //
  // mappedVars is mapping from columns to Variable_IDs.
  // Recompute mappedVars for problem returned from ip.c
  //
  Variable_ID_Tuple new_mapped(0);  // This is expanded by "append"
  for (i=1; i<=p->safeVars; i++) {
    // what is now in column i used to be in column p->var[i]
    Variable_ID v = conj->mappedVars[p->var[i]];
    assert(v->kind() != Wildcard_Var);
    new_mapped.append(v);
  }

  /* Redeclare all wildcards that weren't eliminated. */
  free_var_decls(conj->myLocals);  conj->myLocals.clear();

  conj->mappedVars = new_mapped;  
  for (i = p->safeVars+1; i<=p->nVars; i++) {
    Variable_ID v = conj->declare();
    conj->mappedVars.append(v);
  }

  // reset var and forwarding address if desired.
  p->variablesInitialized = 1;
  for(i=1; i<=conj->problem->nVars; i++)
    conj->problem->var[i] = conj->problem->forwardingAddress[i] = i;
      
  if(pres_debug) {
    fprintf(DebugFile, "] $$$ simplify_conj\n");
    conj->prefix_print(DebugFile);
    fprintf(DebugFile, "\n");
  }


  use_ugly_names--;
  conj->simplified = true;
  conj->setup_anonymous_wildcard_names();

  return(true);
}


int Conjunct::rank() {
  Conjunct *C = this->copy_conj_same_relation();
  C->reorder();
  C->ordered_elimination(C->relation()->global_decls()->size());
  int C_rank = 0;
  for(Variable_Iterator vi = C->mappedVars; vi; vi++)
    if(C->find_column(*vi) > 0) C_rank++;
  delete C;
  return C_rank;

}


void Conjunct::query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) {
  int c1 = get_column(v1);
  int c2 = get_column(v2);
  assert(c1 && c2);
  problem->query_difference(c1, c2, lowerBound, upperBound, guaranteed);
}


void Conjunct::query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) {
  int c = get_column(v);
  assert (c);
  problem->query_variable_bounds(c, &lowerBound, &upperBound);
}

coef_t Conjunct::query_variable_mod(Variable_ID v, coef_t factor) {
  int c = get_column(v);
  assert(c);
  return problem->query_variable_mod(c, factor);
}

bool Conjunct::query_variable_used(Variable_ID v) {
  for (GEQ_Iterator g = GEQs(); g.live(); g.next()) {
    if ((*g).get_coef(v)) return true;
	}
  for (EQ_Iterator e = EQs(); e.live(); e.next()) {
    if ((*e).get_coef(v)) return true;
	}
  return false;
}


int Conjunct::simplifyProblem(int verify, int subs, int redundantElimination) {
  if (verified) verify = 0;
  int result = problem->simplifyProblem(verify, subs, redundantElimination);
  if (result == false && !exact)
    exact=true;
  assert(!(verified && verify && result == false));
  if (verify && result) verified = true;
  else if (!result) verified = false;
  return result;
}


// not as confident about this one as the previous:
int Conjunct::redSimplifyProblem(int effort, int computeGist) {
  redCheck result = problem->redSimplifyProblem(effort, computeGist);
  if (result == redFalse && !exact)
    exact=true;
  return result;
}


//
// Add given list of wildcards S to this Conjunct.
// Clears argument. (That's very important, otherwise those var_id's get freed)
// Push_exists takes responsibility for reusing or deleting Var_ID's;
//  here we reuse them.  Must also empty out the Tuple when finished (joins).
void Conjunct::push_exists(Variable_ID_Tuple &S) {
  for(Tuple_Iterator<Variable_ID> VI(S); VI; VI++) {
    (*VI)->var_kind = Wildcard_Var;
  }
  myLocals.join(S);       // Sets S to be empty.
  cols_ordered = false;
  simplified = false;
}


Conjunct *Formula::add_conjunct() {
  assert_not_finalized();
  assert(can_add_child());
  Conjunct *f = new Conjunct(this, myRelation);
  myChildren.append(f);
  return f;
}

// Compress/uncompress functions

bool Conjunct::is_compressed() {
  if(problem!=NULL && comp_problem==NULL) {
    return false;
  }
  else if(problem==NULL && comp_problem!=NULL) {
    return true;
  }
  else {
    assert(0 && "Conjunct::is_compressed: bad conjunct");
    return false;
  }
}


void Conjunct::compress() {
  if(!is_compressed()) {    // compress
    comp_problem = new Comp_Problem(problem);
    delete problem;
    problem = NULL;
  }
}


void Conjunct::uncompress() {
  if(is_compressed()) {
    problem = comp_problem->UncompressProblem();
    delete comp_problem;
    comp_problem = NULL;
  }
}


Comp_Problem::Comp_Problem(Problem *problem) :
  _nVars(problem->nVars), 
  _safeVars(problem->safeVars),
  _get_var_name(problem->get_var_name), 
  _getVarNameArgs(problem->getVarNameArgs),
  eqs(&problem->EQs[0],problem->nEQs,problem->nVars), 
  geqs(&problem->GEQs[0],problem->nGEQs,problem->nVars) {
}

Comp_Constraints::Comp_Constraints(eqn *constrs, int no_constrs, int no_vars) :
  n_constrs(no_constrs), 
  n_vars(no_vars) {
  coefs = new coef_t[(n_vars+1)*n_constrs];
  int e, v;
  for(e=0; e<n_constrs; e++) {
    for(v=0; v<=n_vars; v++) {
      coefs[coef_index(e,v)] = constrs[e].coef[v];
    }
  }
}


Comp_Constraints::~Comp_Constraints() {
  delete coefs;
}


Problem *Comp_Problem::UncompressProblem() {
  Problem *p = new Problem(eqs.n_constraints(), geqs.n_constraints());
  p->get_var_name     = get_var_name;
  p->getVarNameArgs = _getVarNameArgs;
  p->nVars          = _nVars;
  p->safeVars       = _safeVars;
  for(int i=1; i<=p->nVars; i++) {
		p->forwardingAddress[i] = i;
		p->var[i] = i;
  }
  eqs.UncompressConstr(&p->EQs[0], p->nEQs);
  geqs.UncompressConstr(&p->GEQs[0], p->nGEQs);
  return p;
}

void Comp_Constraints::UncompressConstr(eqn *constrs, short &pn_constrs) {
  int e, v;
  for(e=0; e<n_constrs; e++) {
    eqnnzero(&constrs[e], 0);
    for(v=0; v<=n_vars; v++) {
      constrs[e].coef[v] = coefs[coef_index(e,v)];
    }
    constrs[e].touched = 1;
  }
  pn_constrs = n_constrs;
}


void Conjunct::convertEQstoGEQs(bool excludeStrides) { 
  simplify_conj(this,true,1,EQ_BLACK);  // don't remember why I want to comment this statement out with reason "will cause inconsistency between Conjunct::mappedVars and Problem::nVars",  06/09/2009 by chun
  problem->convertEQstoGEQs(excludeStrides);
}


void Conjunct::calculate_dimensions(Relation &R, int &ndim_all, int &ndim_domain) {

  Conjunct * c = this;
  Relation rc=Relation(R, c);

  if(relation_debug) {
    fprintf(DebugFile,"{{{\nIn Conjunct::calculate_dimensions:\n");
    rc.prefix_print(DebugFile);
  }

  rc=Approximate(rc);
  Relation rd=rc;

  if(relation_debug) {
    fprintf(DebugFile,"Conjunct::calculate_dimensions: Approximated as:\n");
    rc.prefix_print(DebugFile);
  }

  // skip_set_checks++;

  Conjunct * rc_conj=rc.single_conjunct();
  ndim_all=rc.n_inp()+rc.n_out();
  ndim_all-=rc_conj->n_EQs();

  rc = Project_On_Sym(rc);
  rc.simplify();

  if(relation_debug) {
    fprintf(DebugFile, "Conjunct::calculate_dimensions: after project_on_sym\n");
    rc.prefix_print(DebugFile);
  }

  int n_eq_sym = 1000;
  for (DNF_Iterator s(rc.query_DNF()); s.live(); s.next()) 
    n_eq_sym = min(n_eq_sym, s.curr()->n_EQs());
  ndim_all+=n_eq_sym;
  // skip_set_checks--;

  if (R.is_set()) 
    ndim_domain = ndim_all;
  else {
    /* get dimensions for the domain (broadcasting) */

    rd=Domain(rd);
    rd.simplify();

    if(relation_debug) {
      fprintf(DebugFile,"Domain is:\n");
      rd.prefix_print(DebugFile);
    }

    rc_conj=rd.single_conjunct();
    ndim_domain=rd.n_set()-rc_conj->n_EQs()+n_eq_sym;
  }

  if(relation_debug) {
    fprintf(DebugFile,"n_eq_sym=%d \n",n_eq_sym);
    fprintf(DebugFile,"Dimensions: all=%d domain=%d\n}}}\n", ndim_all,ndim_domain);
  }
}

} // namespace