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

 Purpose:
   Functions for disjunctive normal form.

 Notes:

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

#include <basic/Bag.h>
#include <omega/pres_dnf.h>
#include <omega/pres_conj.h>
#include <omega/pres_tree.h>  /* all DNFize functions are here */
#include <omega/Relation.h>
#include <omega/omega_i.h>

namespace omega {

void DNF::remap() {
  for(DNF_Iterator DI(this); DI.live(); DI.next()) {
    Conjunct *C = DI.curr();
    C->remap();
  }
}


//
// DNF1 & DNF2 -> DNF.
// Free arguments.
//
DNF* DNF_and_DNF(DNF* dnf1, DNF* dnf2) {
  DNF* new_dnf = new DNF;
  for(DNF_Iterator p(dnf2); p.live(); p.next()) {
    new_dnf->join_DNF(DNF_and_conj(dnf1, p.curr()));
  }
  delete dnf1;
  delete dnf2;
  if(new_dnf->length() > 1) {
    new_dnf->simplify();
  }

  if(pres_debug) {
    fprintf(DebugFile, "+++ DNF_and_DNF OUT +++\n");
    new_dnf->prefix_print(DebugFile);
  }
  return(new_dnf);
}


/*
 * Remove redundant conjuncts from given DNF.
 * If (C1 => C2), remove C1.
 * C1 => C2 is TRUE: when problem where C1 is Black and C2 is Red 
 * Blk   Red       : has no red constraints.
 * It means that C1 is a subset of C2 and therefore C1 is redundant.
 *
 * Exception: C1 => UNKNOWN - leave them as they are
 */
void DNF::rm_redundant_conjs(int effort) {
  if(is_definitely_false() || has_single_conjunct())
    return;

  use_ugly_names++;
  // skip_set_checks++;

  int count = 0;
  for(DNF_Iterator p(this); p.live(); p.next()) count++;

  if(pres_debug) {
    int i = 0;
    fprintf(DebugFile, "@@@ rm_redundant_conjs IN @@@[\n");
    prefix_print(DebugFile);
    for(DNF_Iterator p(this); p.live(); p.next())
      fprintf(DebugFile, "#%d = %p\n", ++i, p.curr());
  }

  DNF_Iterator pdnext;
  DNF_Iterator pdel(this);
  for(; pdel.live(); pdel=pdnext) {
    pdnext = pdel;
    pdnext.next();
    Conjunct *cdel = pdel.curr();
    int del_min_leading_zeros = cdel->query_guaranteed_leading_0s();
    int del_max_leading_zeros = cdel->query_possible_leading_0s();

    for(DNF_Iterator p(this); p.live(); p.next()) {
      Conjunct *c = p.curr();
      if(c != cdel) {
        int c_min_leading_zeros = cdel->query_guaranteed_leading_0s();
        int c_max_leading_zeros = cdel->query_possible_leading_0s();
        if(pres_debug)
          fprintf(DebugFile, "@@@ rm_redundant_conjs @%p => @%p[\n", cdel, c);

        if (c->is_inexact() && cdel->is_exact()) {
          if (pres_debug)
            fprintf(DebugFile, "]@@@ rm_redundant_conjs @@@ Exact Conj => Inexact Conj is not tested\n");
        }
        else if (del_min_leading_zeros  >=0 && c_min_leading_zeros >= 0
                 && c_max_leading_zeros >= 0 && del_max_leading_zeros >=0
                 && (del_min_leading_zeros  > c_max_leading_zeros
                     || c_min_leading_zeros > del_max_leading_zeros)) {
          if (1 || pres_debug)
            fprintf(DebugFile, "]@@@ not redundant due to leading zero info\n");
        }
        else {
          Conjunct *cgist = merge_conjs(cdel, c, MERGE_GIST);

          if (!cgist->redSimplifyProblem(effort,0)) {
            if(pres_debug) {
              fprintf(DebugFile, "]@@@ rm_redundant_conjs @@@ IMPLICATION TRUE @%p\n", cdel);
              cdel->prefix_print (DebugFile);
              fprintf(DebugFile, "=>\n");
              c->prefix_print (DebugFile);
            }
            rm_conjunct(cdel);
            delete cdel;
            delete cgist;
            break;
          }
          else {
            if(pres_debug) {
              fprintf(DebugFile, "]@@@ rm_redundant_conjs @@@ IMPLICATION FALSE @%p\n", cdel);
              if(pres_debug > 1)
                cgist->prefix_print(DebugFile);
            }
            delete cgist;
          }
        }
      }
    }
  }

  if(pres_debug) {
    fprintf(DebugFile, "]@@@ rm_redundant_conjs OUT @@@\n");
    prefix_print(DebugFile);
  }
  // skip_set_checks--;
  use_ugly_names--;
}


/* Remove  inexact conjuncts from given DNF if it contains UNKNOWN
 * conjunct
 */

void DNF::rm_redundant_inexact_conjs() {
  if (is_definitely_false() || has_single_conjunct())
    return;

  bool has_unknown=false;
  bool has_inexact=false;

  Conjunct * c_unknown = 0;  // make compiler shut up
  for (DNF_Iterator p(this); p.live(); p.next()) {
    assert (p.curr()->problem!=NULL);
    if (p.curr()->is_inexact()) {
      if (p.curr()->is_unknown()) {
        has_unknown=true;
        c_unknown = p.curr();
      }
      else
        has_inexact=true;
    }
  }

  if (! has_unknown || ! has_inexact)
    return;

  use_ugly_names++;
  // skip_set_checks++;  

  DNF_Iterator pdnext;
  DNF_Iterator pdel(this);

  for (; pdel.live(); pdel=pdnext) {
    pdnext = pdel;
    pdnext.next();
    Conjunct * cdel=pdel.curr();
    if (cdel->is_inexact() && cdel!=c_unknown) {
      rm_conjunct(cdel);
      delete cdel;
    }
  }

  use_ugly_names--;
  // skip_set_checks--;
}
  


//
// DNF properties.
//
bool DNF::is_definitely_false() const {
  return(conjList.empty());
}

bool DNF::is_definitely_true() const {
  return(has_single_conjunct() && single_conjunct()->is_true());
}

int DNF::length() const {
  return conjList.length();
}

Conjunct *DNF::single_conjunct() const {
  assert(conjList.length()==1);
  return(conjList.front());
}

bool DNF::has_single_conjunct() const {
  return (conjList.length()==1);
}

Conjunct *DNF::rm_first_conjunct() {
  if(conjList.empty()) {
    return NULL;
  }
  else {
    return conjList.remove_front();
  }
}


//
// Convert DNF to Formula and add it root.
// Free this DNF. 
//
void DNF::DNF_to_formula(Formula* root) {
  Formula *new_or;
  if (conjList.length()!=1) {
    skip_finalization_check++;
    new_or = root->add_or();
    skip_finalization_check--;
  }
  else {
    new_or = root;
  }
  while(!conjList.empty()) {
    Conjunct *conj = conjList.remove_front();
    new_or->add_child(conj);
  }
  delete this;
}


//
// DNF functions.
//
DNF::DNF() : conjList() {
}

DNF::~DNF() {
  // for(DNF_Iterator p(this); p.live(); p.next()) {
  //   if(p.curr() != NULL)
  //     delete p.curr();
  // }
  for(List_Iterator<Conjunct *> i(conjList); i.live(); i.next())
    delete *i;
}

//
// Copy DNF
//
DNF* DNF::copy(Rel_Body *rel_body) {
  DNF *new_dnf = new DNF;
  for(DNF_Iterator pd(this); pd.live(); pd.next()) {
    Conjunct *conj = pd.curr();
    if(conj)
      new_dnf->add_conjunct(conj->copy_conj_diff_relation(rel_body,rel_body));
  }
  return(new_dnf);
}

//
// Add Conjunct to DNF
//
void DNF::add_conjunct(Conjunct* conj) {
  conjList.append(conj);
}

//
// Add DNF to DNF.
// The second DNF is reused.
//
void DNF::join_DNF(DNF* dnf) {
  conjList.join(dnf->conjList);
  delete dnf;
}

//
// Remove conjunct from DNF.
// Conjunct itself is not deleted.
//
void DNF::rm_conjunct(Conjunct *c) {
  if(conjList.front() == c) {
    conjList.remove_front();
  }
  else {
    List_Iterator<Conjunct*> p, pp;
    for(p=List_Iterator<Conjunct*> (conjList); p; p++) {
      if((*p)==c) {
        conjList.del_after(pp);
        return;
      }
      pp = p;
    }
    assert(0 && "DNF::rm_conjunct: no such conjunct");
  }
}


// remove (but don't delete) all conjuncts

void DNF::clear() {
  conjList.clear();
}


//
// DNF & CONJ -> new DNF.
// Don't touch arguments.
//
DNF* DNF_and_conj(DNF* dnf, Conjunct* conj) {
  DNF* new_dnf = new DNF;
  for(DNF_Iterator p(dnf); p.live(); p.next()) {
    Conjunct* new_conj = merge_conjs(p.curr(), conj, MERGE_REGULAR);
    new_dnf->add_conjunct(new_conj);
  }
  if(new_dnf->length() > 1) {
    new_dnf->simplify();
  }
  return(new_dnf);
}

//
// Compute C0 and not (C1 or C2 or ... CN).
// Reuse/delete its arguments.
//
DNF* conj_and_not_dnf(Conjunct *positive_conjunct, DNF *neg_conjs, bool weak) {
  DNF *ret_dnf = new DNF;
  int recursive = 0;
  use_ugly_names++;

  if(pres_debug) {
    fprintf(DebugFile, "conj_and_not_dnf [\n");
    fprintf(DebugFile, "positive_conjunct:\n");
    positive_conjunct->prefix_print(DebugFile);
    fprintf(DebugFile, "neg_conjs:\n");
    neg_conjs->prefix_print(DebugFile);
    fprintf(DebugFile, "\n\n");
  }

  if (simplify_conj(positive_conjunct, true, false, EQ_BLACK) == false) {
    positive_conjunct = NULL;
    goto ReturnDNF;
  }

  /* Compute gists of negative conjuncts given positive conjunct */


  int c0_updated;
  c0_updated = true;
  while(c0_updated) {
    c0_updated = false;
    for(DNF_Iterator p(neg_conjs); p.live(); p.next()) {
      Conjunct *neg_conj = p.curr();
      if(neg_conj==NULL) continue;
      if (!positive_conjunct->is_exact()
          && !neg_conj->is_exact()) {
        // C1 and unknown & ~(C2 and unknown) = C1 and unknown
        delete neg_conj;
        p.curr_set(NULL);
        continue;
      }
      Conjunct *cgist = merge_conjs(positive_conjunct, neg_conj, MERGE_GIST);
      if(simplify_conj(cgist, false, true, EQ_RED) == false) {
        // C1 & ~FALSE = C1
        delete neg_conj;
        p.curr_set(NULL);
      } 
      else {
        cgist->rm_color_constrs();
        if(cgist->is_true()) {
          // C1 & ~TRUE = FALSE
          delete cgist;
          goto ReturnDNF;
        } 
        else {
          if(cgist->cost()==1) {        // single inequality
            DNF *neg_dnf = negate_conj(cgist);
            delete cgist;
            Conjunct *conj =
              merge_conjs(positive_conjunct, neg_dnf->single_conjunct(), MERGE_REGULAR);
            delete positive_conjunct;
            delete neg_dnf;
            positive_conjunct = conj;
            delete neg_conj;
            p.curr_set(NULL);
            if(!simplify_conj(positive_conjunct, false, false, EQ_BLACK)) {
              positive_conjunct = NULL;
              goto ReturnDNF;
            }
            c0_updated = true;
          } 
          else {
            delete neg_conj;
            p.curr_set(cgist);
          }
        }
      }
    }
  }

  if(pres_debug) {
    fprintf(DebugFile, "--- conj_and_not_dnf positive_conjunct NEW:\n");
    positive_conjunct->prefix_print(DebugFile);
    fprintf(DebugFile, "--- conj_and_not_dnf neg_conjs GISTS:\n");
    neg_conjs->prefix_print(DebugFile);
    fprintf(DebugFile, "--- conj_and_not_dnf ---\n\n");
  }

  /* Find minimal negative conjunct */
  {
    Conjunct *min_conj = NULL;
    int min_cost = INT_MAX;
    DNF_Iterator min_p;
    int live_count = 0;
    for(DNF_Iterator q(neg_conjs); q.live(); q.next()) {
      Conjunct *neg_conj = q.curr();
      if(neg_conj!=NULL) {
        live_count++;
        if(neg_conj->cost() < min_cost) {
          min_conj = neg_conj;
          min_cost = neg_conj->cost();
          min_p = q;
        }
      }
    }

    /* Negate minimal conjunct, AND result with positive conjunct */
    if(weak || min_conj==NULL) {
      ret_dnf->add_conjunct(positive_conjunct);
      positive_conjunct = NULL;
    }
    else if (min_cost == CantBeNegated) {
      static int OMEGA_WHINGE = -1;
      if (OMEGA_WHINGE < 0) {
        OMEGA_WHINGE = getenv("OMEGA_WHINGE") ? atoi(getenv("OMEGA_WHINGE")) : 0;
      }
      if (OMEGA_WHINGE) {
        fprintf(stderr, "Ignoring negative clause that can't be negated and generating inexact result\n");
        if (!pres_debug) fprintf(DebugFile, "Ignoring negative clause that can't be negated and generating inexact result\n");
      }

      positive_conjunct->make_inexact();
      ret_dnf->add_conjunct(positive_conjunct);
      positive_conjunct = NULL;
      if(pres_debug) 
        fprintf(DebugFile, "Ignoring negative clause that can't be negated and generating inexact upper bound\n");
    }
    else {
      DNF *neg_dnf = negate_conj(min_conj);
      delete min_conj;
      min_p.curr_set(NULL);
      DNF *new_pos = DNF_and_conj(neg_dnf, positive_conjunct);
      delete neg_dnf;
      delete positive_conjunct;
      positive_conjunct = NULL;
      // new_dnf->rm_redundant_conjs(2);
      if(live_count>1) {
        recursive = 1;
        for(DNF_Iterator pd(new_pos); pd.live(); pd.next()) {
          Conjunct *conj = pd.curr();
          ret_dnf->join_DNF(conj_and_not_dnf(conj, neg_conjs->copy(conj->relation())));
          pd.curr_set(NULL);
        }
        delete new_pos;
      }
      else {
        ret_dnf->join_DNF(new_pos);
      }
    }
  }

ReturnDNF:;
  delete positive_conjunct;
  delete neg_conjs;

  //if (recursive) ret_dnf->rm_redundant_conjs(1);

  if(pres_debug) {
    fprintf(DebugFile, "] conj_and_not_dnf RETURN:\n");
    ret_dnf->prefix_print(DebugFile);
    fprintf(DebugFile, "\n\n");
  }
  use_ugly_names--;
  return ret_dnf;
}

/* first some functions for manipulating oc "problems" */

static void EqnnZero(eqn *e, int s) {
//   memset((char*)e, 0, (headerWords+1+s)*sizeof(int));
  e->key = 0;
  e->touched = 0;
  e->color = EQ_BLACK;
  e->essential = 0;
  e->varCount = 0;
  for (int i = 0; i <= s; i++)
    e->coef[i] = 0;    
}

/*
 * Make a new black equation in a given problem 
 */
static int NewEquation(Problem *p) {
  int e = p->newEQ();
  EqnnZero(&p->EQs[e], p->nVars);
  return e;
}

/*
 * Make a new black inequality in a given problem 
 */
static int NewInequality(Problem *p) {
  int g = p->newGEQ();
  EqnnZero(&p->GEQs[g], p->nVars);
  return g;
}

//
// ~CONJ -> DNF
//
DNF* negate_conj(Conjunct* conj) {
  if(pres_debug) {
    fprintf(DebugFile, "%%%%%% negate_conj IN %%%%%%\n");
    conj->prefix_print(DebugFile);
    fprintf(DebugFile, "\n");
  }

  DNF* new_dnf = new DNF;
  Problem *p = conj->problem;
  int i, j,k;

  if (!conj->is_exact()) new_dnf->add_conjunct(conj->copy_conj_same_relation());

  Conjunct* true_part = new Conjunct(NULL, conj->relation());
  Problem *tp = true_part->problem;
  copy_conj_header(true_part, conj);
  true_part->invalidate_leading_info();
  int *wildCard = new int[p->nGEQs];
  int *handleIt = new int[p->nVars+1];
  for(j=1; j<=p->nVars; j++) handleIt[j] = false;

  for(i=0; i<p->nGEQs; i++) {
    wildCard[i] = 0;
    for(j=1; j<=p->nVars; j++) {
      Variable_ID v = conj->mappedVars[j];
      if(v->kind()==Wildcard_Var && p->GEQs[i].coef[j]!=0) {
        assert(wildCard[i] == 0);
        handleIt[j] = true;
        if (p->GEQs[i].coef[j] > 0) wildCard[i] = j;
        else wildCard[i] = -j;
      }
    }
  }

  for(i=0; i<p->nGEQs; i++) if (wildCard[i] == 0) {
      /* ~(ax + by + c >= 0) = (-ax -by -c-1 >= 0) */
      Conjunct* new_conj = true_part->copy_conj_same_relation();
      Problem *np = new_conj->problem;
      new_conj->exact=true;
      int n_e = NewInequality(np);
      int t_e = NewInequality(tp);
      np->GEQs[n_e].coef[0] = -p->GEQs[i].coef[0]-1;
      tp->GEQs[t_e].coef[0] = p->GEQs[i].coef[0];
      for(j=1; j<=p->nVars; j++) {
        Variable_ID v = conj->mappedVars[j];
        if(v->kind()==Wildcard_Var && p->GEQs[i].coef[j]!=0) {
          assert(0 && "negate_conj: wildcard in inequality");
        }
        np->GEQs[n_e].coef[j] = -p->GEQs[i].coef[j];
        tp->GEQs[t_e].coef[j] = p->GEQs[i].coef[j];

      }
      assert(j-1 == p->nVars);
      assert(j-1 == conj->mappedVars.size());
      new_dnf->add_conjunct(new_conj);
    }


  for(i=0; i<p->nEQs; i++) {
    int wc_no = 0;
    int wc_j = 0;  // make complier shut up
    for(j=1; j<=p->nVars; j++) {
      Variable_ID v = conj->mappedVars[j];
      if(v->kind()==Wildcard_Var && p->EQs[i].coef[j]!=0) {
        wc_no++;
        wc_j = j;
      }
    }

    if(wc_no!=0) {
#if ! defined NDEBUG
      int i2;
      assert(!handleIt[wc_j]);
      for(i2=0; i2<p->nEQs; i2++)
        if(i != i2 && p->EQs[i2].coef[wc_j] != 0)  break;
      assert(i2 >= p->nEQs);
#endif
      assert(wc_no == 1 && "negate_conj: more than 1 wildcard in equality");

      // === Negating equality with a wildcard for K>0 ===
      // ~(exists v st expr + K v  + C = 0) =
      //  (exists v st 1 <= - expr - K v - C <= K-1)

      Conjunct *nc = true_part->copy_conj_same_relation();
      Problem *np = nc->problem;
      nc->exact=true;

      // -K alpha = expr  <==>  K alpha = expr
      if(p->EQs[i].coef[wc_j]<0)
        p->EQs[i].coef[wc_j] = -p->EQs[i].coef[wc_j];

      if(p->EQs[i].coef[wc_j]==2) {
        // ~(exists v st  expr +2v +C = 0) =
        //  (exists v st -expr -2v -C = 1)
        // That is (expr +2v +C+1 = 0)
        int e = NewEquation(np);
        np->EQs[e].coef[0] = p->EQs[i].coef[0] +1;
        for(j=1; j<=p->nVars; j++) {
          np->EQs[e].coef[j] = p->EQs[i].coef[j];
        }
      }
      else {
        // -expr -Kv -C-1 >= 0
        int e = NewInequality(np);
        np->GEQs[e].coef[0] = -p->EQs[i].coef[0] -1;
        for(j=1; j<=p->nVars; j++) {
          np->GEQs[e].coef[j] = -p->EQs[i].coef[j];
        }

        // +expr +Kv +C+K-1 >= 0
        e = NewInequality(np);
        np->GEQs[e].coef[0] = p->EQs[i].coef[0] +p->EQs[i].coef[wc_j] -1;
        for(j=1; j<=p->nVars; j++) {
          np->GEQs[e].coef[j] = p->EQs[i].coef[j];
        }
      }

      new_dnf->add_conjunct(nc);

    }
    else {
      /* ~(ax + by + c = 0) = (-ax -by -c-1 >= 0) Or (ax + by + c -1 >= 0) */
      Conjunct *nc1 = true_part->copy_conj_same_relation();
      Conjunct *nc2 = true_part->copy_conj_same_relation();
      Problem* np1 = nc1->problem;
      Problem* np2 = nc2->problem;
      nc1->invalidate_leading_info();
      nc2->invalidate_leading_info();
      nc1->exact=true;
      nc2->exact=true;
      int n_e1 = NewInequality(np1);
      int n_e2 = NewInequality(np2);
      np1->GEQs[n_e1].coef[0] = -p->EQs[i].coef[0]-1;
      np2->GEQs[n_e2].coef[0] =  p->EQs[i].coef[0]-1;
      for(j=1; j<=p->nVars; j++) {
        coef_t coef = p->EQs[i].coef[j];
        np1->GEQs[n_e1].coef[j] = -coef;
        np2->GEQs[n_e2].coef[j] =  coef;
      }
      new_dnf->add_conjunct(nc1);
      new_dnf->add_conjunct(nc2);
    }
    {
      int e = NewEquation(tp);
      tp->EQs[e].coef[0] =  p->EQs[i].coef[0];
      for(j=1; j<=p->nVars; j++) 
        tp->EQs[e].coef[j] = p->EQs[i].coef[j];
    }
  }

  for(j=1; j<=p->nVars; j++)
    if (handleIt[j]) {
      for(i=0; i<p->nGEQs; i++)
        if (wildCard[i] == j)
          for(k=0; k<p->nGEQs; k++) if (wildCard[k] == -j){
              // E_i <= c_i alpha
              //        c_k alpha <= E_k
              // c_k E_i <= c_i c_k alpha <= c_i E_k
              // c_k E_i <= c_i c_k floor (c_i E_k / c_i c_k)
              // negating:
              // c_k E_i > c_i c_k floor (c_i E_k / c_i c_k)
              // c_k E_i > c_i c_k beta > c_i E_k - c_i c_k
              // c_k E_i - 1 >= c_i c_k beta >= c_i E_k - c_i c_k + 1
              Conjunct* new_conj = true_part->copy_conj_same_relation();
              Problem *np = new_conj->problem;
              coef_t c_k = - p->GEQs[k].coef[j];
              coef_t c_i = p->GEQs[i].coef[j];
              assert(c_k > 0);
              assert(c_i > 0);
              new_conj->exact=true;
              int n_e = NewInequality(np);
              // c_k E_i - 1 >= c_i c_k beta 
              int v;
              for(v=0; v<=p->nVars; v++) {
                np->GEQs[n_e].coef[v] = - c_k * p->GEQs[i].coef[v];
              }
              np->GEQs[n_e].coef[j] = -c_i * c_k;
              np->GEQs[n_e].coef[0]--;

              n_e = NewInequality(np);
              // c_i c_k beta >= c_i E_k - c_i c_k + 1
              // c_i c_k beta + c_i c_k -1 >= c_i E_k 
              for(v=0; v<=p->nVars; v++) {
                np->GEQs[n_e].coef[v] = - c_i * p->GEQs[k].coef[v];
              }
              np->GEQs[n_e].coef[j] = c_i * c_k;
              np->GEQs[n_e].coef[0] += c_i * c_k -1;

              new_dnf->add_conjunct(new_conj);
            }
    }

  if(pres_debug) {
    fprintf(DebugFile, "%%%%%% negate_conj OUT %%%%%%\n");
    new_dnf->prefix_print(DebugFile);
  }
  delete true_part;
  delete[] wildCard;
  delete[] handleIt;
  return(new_dnf);
}




///////////////////////////////////////////////////////
// DNFize formula -- this is the real simplification //
// It also destroys the formula it simplifies        //
///////////////////////////////////////////////////////



//
// Try to separate positive and negative clauses below the AND,
// letting us use the techniques described in Pugh & Wonnacott:
// "An Exact Method for Value-Based Dependence Analysis"
//


DNF* F_And::DNFize() {
  Conjunct *positive_conjunct = NULL;
  DNF *neg_conjs = new DNF;
  List<DNF*> pos_dnfs;
  List_Iterator<DNF*> pos_dnf_i;
  DNF *new_dnf = new DNF;
  int JustReturnDNF = 0;

  use_ugly_names++;

  if(pres_debug) {
    fprintf(DebugFile, "\nF_And:: DNFize [\n");
    prefix_print(DebugFile);
  }

  if(children().empty()) {
    Conjunct * c=new Conjunct(NULL, relation());
    new_dnf->add_conjunct(c);
  }
  else {
    while(!children().empty()) {
      Formula* carg = children().remove_front();
      if(carg->node_type()==Op_Not) {
        // DNF1 & ~DNF2 -> DNF
        DNF *dnf = carg->children().remove_front()->DNFize();
        delete carg;
        neg_conjs->join_DNF(dnf);       // negative conjunct
      }
      else {
        // DNF1 & DNF2 -> DNF
        DNF *dnf = carg->DNFize();
        int dl = dnf->length();
        if(dl==0) {
          // DNF & false -> false
          delete this;
          JustReturnDNF = 1;
          break;
        }
        else if(dl==1) {
          // positive conjunct
          Conjunct *conj = dnf->rm_first_conjunct();
          delete dnf;
          if(positive_conjunct==NULL) {
            positive_conjunct = conj;
          }
          else {
            Conjunct *new_conj = merge_conjs(positive_conjunct, conj, MERGE_REGULAR);
            delete conj;
            delete positive_conjunct;
            positive_conjunct = new_conj;
          }
        }
        else {
          // positive DNF
          pos_dnfs.append(dnf);
        }
      }
    }

    if (!JustReturnDNF) {
      Rel_Body * my_relation = relation();
      delete this;

      // If we have a positive_conjunct, it can serve as the 1st arg to
      // conj_and_not_dnf.  Otherwise, if pos_dnfs has one DNF,
      // use each conjunct there for this purpose.
      // Only pass "true" here if there is nothing else to try,
      // as long as TRY_TO_AVOID_TRUE_AND_NOT_DNF is set.
      //
      // Perhaps we should even try to and multiple DNF's?

      if (!positive_conjunct && pos_dnfs.length() == 1) {
        if(pres_debug) {
          fprintf(DebugFile, "--- F_AND::DNFize() Single pos_dnf:\n");
          pos_dnfs[1]->prefix_print(DebugFile);
          fprintf(DebugFile, "--- F_AND::DNFize() vs neg_conjs:\n");
          neg_conjs->prefix_print(DebugFile);
        }

        DNF *real_neg_conjs = new DNF;
        for (DNF_Iterator nc(neg_conjs); nc; nc++) {
          if (simplify_conj((*nc), true, false, EQ_BLACK) != false)
            real_neg_conjs->add_conjunct(*nc);
          (*nc) = 0;
        }
        delete neg_conjs;
        neg_conjs = real_neg_conjs;

        for(DNF_Iterator pc(pos_dnfs[1]); pc; pc++) {
          new_dnf->join_DNF(conj_and_not_dnf((*pc), neg_conjs->copy((*pc)->relation())));
          (*pc) = 0;
        }
      }
      else if(positive_conjunct==NULL && neg_conjs->is_definitely_false()) {
        pos_dnf_i = List_Iterator<DNF*>(pos_dnfs);
        delete new_dnf;
        new_dnf = *pos_dnf_i;
        *pos_dnf_i = NULL;
        pos_dnf_i++;
        for ( ; pos_dnf_i; pos_dnf_i++) {
          DNF *pos_dnf = *pos_dnf_i;
          new_dnf = DNF_and_DNF(new_dnf, pos_dnf);
          *pos_dnf_i = NULL;
        }
      } 
      else {
        if(positive_conjunct==NULL) {  
          static int OMEGA_WHINGE = -1;
          if (OMEGA_WHINGE < 0) {
            OMEGA_WHINGE = getenv("OMEGA_WHINGE") ? atoi(getenv("OMEGA_WHINGE")) : 0;
          }

          if (pres_debug || OMEGA_WHINGE) {
            fprintf(DebugFile, "Uh-oh: F_AND::DNFize() resorting to TRUE and not DNF\n");
            fprintf(DebugFile, "--- F_AND::DNFize() neg_conjs\n");
            neg_conjs->prefix_print(DebugFile);
            fprintf(DebugFile, "--- F_AND::DNFize() pos_dnfs:\n");
            for (pos_dnf_i=List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++) {
              (*pos_dnf_i)->prefix_print(DebugFile);
              fprintf(DebugFile,"---- --\n");
            }
          }
          if (OMEGA_WHINGE) {
            fprintf(stderr, "Uh-oh: F_AND::DNFize() resorting to TRUE and not DNF\n");
            fprintf(stderr, "--- F_AND::DNFize() neg_conjs\n");
            neg_conjs->prefix_print(stderr);
            fprintf(stderr, "--- F_AND::DNFize() pos_dnfs:\n");
            for (pos_dnf_i=List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++) {
              (*pos_dnf_i)->prefix_print(stderr);
              fprintf(stderr,"---- --\n");
            }
          }
          positive_conjunct = new Conjunct(NULL, my_relation);
        }
 
        if(!neg_conjs->is_definitely_false()) {
          new_dnf->join_DNF(conj_and_not_dnf(positive_conjunct, neg_conjs));
          neg_conjs = NULL;
        }
        else {
          new_dnf->add_conjunct(positive_conjunct);
        }
        positive_conjunct = NULL;

        //
        // AND it with positive DNFs
        //
        if(pres_debug) {
          fprintf(DebugFile, "--- F_AND::DNFize() pos_dnfs:\n");
          for (pos_dnf_i=List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++)
            (*pos_dnf_i)->prefix_print(DebugFile);
        }
        for (pos_dnf_i = List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++) {
          DNF *pos_dnf = *pos_dnf_i;
          new_dnf = DNF_and_DNF(new_dnf, pos_dnf);
          *pos_dnf_i = NULL;
        }
      }
    }
  }

  delete positive_conjunct;
  delete neg_conjs;
  for (pos_dnf_i = List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++)
    delete *pos_dnf_i;

  if(pres_debug) {
    fprintf(DebugFile, "] F_AND::DNFize() OUT \n");
    new_dnf->prefix_print(DebugFile);
  }

  use_ugly_names--;

  return new_dnf;
}

//
// ~ dnf  = true ^ ~ dnf, so just call conj_and_not_dnf
//

DNF* F_Not::DNFize() {
  Conjunct *positive_conjunct = new Conjunct(NULL, relation());  
  DNF *neg_conjs = children().remove_front()->DNFize();
  delete this;
  DNF *new_dnf = conj_and_not_dnf(positive_conjunct, neg_conjs);

  if(pres_debug) {
    fprintf(DebugFile, "=== F_NOT::DNFize() OUT ===\n");
    new_dnf->prefix_print(DebugFile);
  }
  return new_dnf;
}


//
// or is almost in DNF already:
//

DNF* F_Or::DNFize() {
  DNF* new_dnf = new DNF;
  bool empty_or=true;

  while(!children().empty()) {
    DNF* c_dnf = children().remove_front()->DNFize();
    new_dnf->join_DNF(c_dnf);
    empty_or=false; 
  }

    
  delete this;

  if(pres_debug) {
    fprintf(DebugFile, "=== F_OR::DNFize() OUT ===\n");
    new_dnf->prefix_print(DebugFile);
  }
  return(new_dnf);
}


//
// exists x : (c1 v c2 v ...) --> (exists x : c1) v (exists x : c2) v ...
//

DNF* F_Exists::DNFize() {
  DNF *dnf = children().remove_front()->DNFize();

  for (DNF_Iterator pd(dnf); pd.live(); pd.next()) {
    Conjunct *conj = pd.curr();

    // can simply call localize_vars for DNF with a single conjunct
    Variable_ID_Tuple locals_copy(myLocals.size());
    copy_var_decls(locals_copy, myLocals);
    conj->push_exists(locals_copy);
    conj->remap();
    reset_remap_field(myLocals);

    conj->r_constrs = 0;
    conj->simplified = false; // who knows
    conj->cols_ordered = false;
  }
  delete this;

  if(pres_debug) {
    fprintf(DebugFile, "=== F_EXISTS::DNFize() OUT ===\n");
    dnf->prefix_print(DebugFile);
  }
  return(dnf);
}


//
// Single conjunct is already in DNF.
//

DNF* Conjunct::DNFize() {
  assert(!is_compressed());
  DNF *results = new DNF;

  if (is_true()) {
    simplified = true;
    verified = true;
    results->add_conjunct(this);
  }
  else {
    results->add_conjunct(this);
  }

  return results;
}


//
// Foralls should have been removed before we get to DNFize
//

DNF* F_Forall::DNFize() {
  assert(0);
  return(NULL);
}

void DNF::count_leading_0s() {
  if (conjList.empty())
    return;

  for (DNF_Iterator conj(this); conj; conj++) {
    (*conj)->count_leading_0s();
  }
}


// return x s.t. forall conjuncts c, c has >= x leading 0s
// if set, always returns -1; arg tells you if it's a set or relation.

int DNF::query_guaranteed_leading_0s(int what_to_return_for_empty_dnf) {
  count_leading_0s();
  int result = what_to_return_for_empty_dnf; // if set, -1; if rel, 0
  bool first = true;

  for (DNF_Iterator conj(this); conj; conj++) {
    int tmp = (*conj)->query_guaranteed_leading_0s();
    assert(tmp >= 0 || ((*conj)->relation()->is_set() && tmp == -1));
    if (first || tmp < result) result = tmp;
    first = false;
  }
    
  return result;
}

// return x s.t. forall conjuncts c, c has <= x leading 0s
// if no conjuncts, return the argument

int DNF::query_possible_leading_0s(int n_input_and_output) {
  count_leading_0s();
  int result = n_input_and_output;
  bool first = true;

  for (DNF_Iterator conj(this); conj; conj++) {
    int tmp = (*conj)->query_possible_leading_0s();
    assert(tmp >= 0 || (tmp == -1 && (*conj)->relation()->is_set()));
    if (first || tmp > result) result = tmp;
    first = false;
  }

  return result;
}


// return 0 if we don't know, or +-1 if we do

int DNF::query_leading_dir() {
  count_leading_0s();
  int result = 0;
  bool first = true;

  for (DNF_Iterator conj(this); conj; conj++) {
    int glz = (*conj)->query_guaranteed_leading_0s();
    int plz = (*conj)->query_possible_leading_0s();
    int rlz = 0; // shut the compiler up
    if (glz != plz)
      return 0;

    if (first) {
      rlz = glz;
      result = (*conj)->query_leading_dir();
      first = false;
    }
    else
      if (glz != rlz || result != (*conj)->query_leading_dir())
        return 0;
  }

  return result;
}

void Conjunct::count_leading_0s() {
  Rel_Body *body = relation();
  int max_depth = min(body->n_inp(), body->n_out());
  if(body->is_set()) {
    assert(guaranteed_leading_0s == -1 && possible_leading_0s == -1);
// guaranteed_leading_0s = possible_leading_0s = -1;
    leading_dir = 0;
    return;
  }


#if ! defined NDEBUG
  assert_leading_info();
#endif
  if (guaranteed_leading_0s < 0) {
    int L;
    for (L=1; L <= max_depth; L++) {
      Variable_ID in = body->input_var(L), out = body->output_var(L);
      coef_t min, max;
      bool guaranteed;
     
      query_difference(out, in, min, max, guaranteed);
      if (min < 0 || max > 0) {
        if (min > 0 || max < 0) { // we know guaranteed & possible
          guaranteed_leading_0s = possible_leading_0s = L-1;
          if (min > 0) // We know its 0,..,0,+
            leading_dir = 1;
          else  // We know its 0,..,0,-
            leading_dir = -1;
          return;
        }
        break;
      }
    }
    guaranteed_leading_0s = L-1;
    for ( ; L <= max_depth; L++) {
      Variable_ID in = body->input_var(L),
        out = body->output_var(L);
      coef_t min, max;
      bool guaranteed;
     
      query_difference(out, in, min, max, guaranteed);
     
      if (min > 0 || max < 0) break;
    }
    possible_leading_0s = L-1;
  }
#if ! defined NDEBUG
  assert_leading_info();
#endif
}

//
// add level-carried DNF form out to level "level"
//


void DNF::make_level_carried_to(int level) {
  count_leading_0s();
  Rel_Body *body = 0;  // make compiler shut up
  if (length() > 0 && !(body = conjList.front()->relation())->is_set()) {
    // LCDNF makes no sense otherwise
    Relation tmp;
#ifndef NDEBUG
    tmp = Relation(*body,42);
#endif

    DNF *newstuff = new DNF;
    int shared_depth = min(body->n_inp(), body->n_out());
    int split_to     = level >= 0 ? min(shared_depth,level) : shared_depth;

    skip_finalization_check++;
    EQ_Handle e;

    for (DNF_Iterator conj(this); conj; conj++) {
      assert(body = (*conj)->relation());
      int leading_eqs;

      bool is_guaranteed = (*conj)->verified;

      for (leading_eqs=1; leading_eqs <= split_to; leading_eqs++) {
        Variable_ID in = body->input_var(leading_eqs),
          out = body->output_var(leading_eqs);
        coef_t min, max;
        bool guaranteed;

        if (leading_eqs > (*conj)->possible_leading_0s &&
            (*conj)->leading_dir_valid_and_known()) {
          leading_eqs--;
          break;
        }

        if (leading_eqs > (*conj)->guaranteed_leading_0s) {
          (*conj)->query_difference(out, in, min, max, guaranteed);
          if (min > 0 || max < 0) guaranteed = true;
//      fprintf(DebugFile,"Make level carried, %d <= diff%d <= %d (%d):\n",
//    min,leading_eqs,max,guaranteed); 
//      use_ugly_names++;
//      (*conj)->prefix_print(DebugFile);
//       use_ugly_names--;
          if (!guaranteed) is_guaranteed = false;
          bool generateLTClause = min < 0;
          bool generateGTClause = max > 0;
          bool retainEQClause = (leading_eqs <= (*conj)->possible_leading_0s &&
                                 min <= 0 && max >= 0);
          if (!(generateLTClause || generateGTClause || retainEQClause)) {
            // conjunct is infeasible
            if (pres_debug) {
              fprintf(DebugFile, "Conjunct discovered to be infeasible during make_level_carried_to(%d):\n", level);
              (*conj)->prefix_print(DebugFile);
            }
#if ! defined NDEBUG
            Conjunct *cpy = (*conj)->copy_conj_same_relation();
            assert(!simplify_conj(cpy, true, 32767, 0));
#endif
          }

          if (generateLTClause) {
            Conjunct *lt;
            if (!generateGTClause && !retainEQClause)
              lt = *conj;
            else
              lt = (*conj)->copy_conj_same_relation();
            if (max >= 0) {
              GEQ_Handle l = lt->add_GEQ(); // out<in ==> in-out-1>=0
              l.update_coef_during_simplify(in, 1);
              l.update_coef_during_simplify(out, -1);
              l.update_const_during_simplify(-1);
            }
            lt->guaranteed_leading_0s 
              = lt->possible_leading_0s = leading_eqs-1;
            lt->leading_dir = -1;
            if (is_guaranteed) {
              /*
                fprintf(DebugFile,"Promising solutions to: %d <= diff%d <= %d (%d):\n",
                min,leading_eqs,max,guaranteed); 
                use_ugly_names++;
                lt->prefix_print(DebugFile);
                use_ugly_names--;
              */
              lt->promise_that_ub_solutions_exist(tmp);
            }
            else if (0) {
              fprintf(DebugFile,"Can't guaranteed solutions to:\n");
              use_ugly_names++;
              lt->prefix_print(DebugFile);
              use_ugly_names--;
            }
            if (generateGTClause || retainEQClause)
              newstuff->add_conjunct(lt);
          }

          if (generateGTClause) {
            Conjunct *gt;
            if (retainEQClause) gt = (*conj)->copy_conj_same_relation();
            else gt = *conj;
            if (min <= 0) {
              GEQ_Handle g = gt->add_GEQ(); // out>in ==> out-in-1>=0
              g.update_coef_during_simplify(in, -1);
              g.update_coef_during_simplify(out, 1);
              g.update_const_during_simplify(-1);
            }
            gt->guaranteed_leading_0s =
              gt->possible_leading_0s = leading_eqs-1;
            gt->leading_dir = 1;
            if (is_guaranteed) {
              /*
                fprintf(DebugFile,"Promising solutions to: %d <= diff%d <= %d (%d):\n",
                min,leading_eqs,max,guaranteed); 
                use_ugly_names++;
                gt->prefix_print(DebugFile);
                use_ugly_names--;
              */
              gt->promise_that_ub_solutions_exist(tmp);
            }
            else if (0) {
              fprintf(DebugFile,"Can't guaranteed solutions to:\n");
              use_ugly_names++;
              gt->prefix_print(DebugFile);
              use_ugly_names--;
            }
            if (retainEQClause) newstuff->add_conjunct(gt);
          }

          if (retainEQClause) {
            assert(min <= 0 && 0 <= max);

            if (min < 0 || max > 0) {
              e = (*conj)->add_EQ(1);
              e.update_coef_during_simplify(in, -1);
              e.update_coef_during_simplify(out, 1);
            }

            assert((*conj)->guaranteed_leading_0s == -1
                   || leading_eqs > (*conj)->guaranteed_leading_0s);
            assert((*conj)->possible_leading_0s == -1
                   || leading_eqs <= (*conj)->possible_leading_0s);

            (*conj)->guaranteed_leading_0s = leading_eqs;
          }
          else break;
        }

        {
          Set<Global_Var_ID> already_done;
          int remapped = 0;

          assert((*conj)->guaranteed_leading_0s == -1
                 || leading_eqs <= (*conj)->guaranteed_leading_0s);

          for (Variable_ID_Iterator func(*body->global_decls()); func; func++) {
            Global_Var_ID f = (*func)->get_global_var();
            if (!already_done.contains(f) &&
                body->has_local(f, Input_Tuple) &&
                body->has_local(f, Output_Tuple) &&
                f->arity() == leading_eqs) {
              already_done.insert(f);

              // add f(in) = f(out), project one away
              e = (*conj)->add_EQ(1);
              Variable_ID f_in  =body->get_local(f,Input_Tuple);
              Variable_ID f_out =body->get_local(f,Output_Tuple);

              e.update_coef_during_simplify(f_in, -1);
              e.update_coef_during_simplify(f_out, 1);

              f_out->remap = f_in;
              remapped = 1;
              is_guaranteed = false;
            }     
          }

          if (remapped) {
            (*conj)->remap();
            (*conj)->combine_columns();
            reset_remap_field(*body->global_decls());
            remapped = 0;
          }
        }
      }
      if (is_guaranteed) 
        (*conj)->promise_that_ub_solutions_exist(tmp); 
      else if (0) {
        fprintf(DebugFile,"Can't guaranteed solutions to:\n");
        use_ugly_names++;
        (*conj)->prefix_print(DebugFile);
        use_ugly_names--;
      }
    }

    skip_finalization_check--;
    join_DNF(newstuff);
  }

#if ! defined NDEBUG
  for (DNF_Iterator c(this); c; c++)
    (*c)->assert_leading_info();
#endif

  simplify();
}

void DNF::remove_inexact_conj() {
  bool found_inexact=false;

  do {
    bool first=true;
    found_inexact=false;
    DNF_Iterator c_prev;
    for (DNF_Iterator c(this); c; c++) {
      if (!(*c)->is_exact()) { // remove it from the list
        found_inexact=true;
        delete (*c);
        if (first)
          conjList.del_front();
        else
          conjList.del_after(c_prev);
        break;
      }  
      else {
        first=false;
        c_prev=c;
      }
    }
  } 
  while (found_inexact);
}


int s_rdt_constrs;

//
// Simplify all conjuncts in a DNF
//
void DNF::simplify() {
  for (DNF_Iterator pd(this); pd.live(); ) {
    Conjunct *conj = pd.curr();
    pd.next();
    if(s_rdt_constrs >= 0 && !simplify_conj(conj, true, s_rdt_constrs, EQ_BLACK)) {
      rm_conjunct(conj);
    }
  }
}

} // namespace