/**CFile***********************************************************************

  FileName    [satBDD.c]

  PackageName [sat]

  Synopsis    [Routines for using BDD.]

  Author      [HoonSang Jin]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]


******************************************************************************/

#include "satInt.h"
#ifdef BDDcu
#include "cuddInt.h"
#endif

static char rcsid[] UNUSED = "$Id: satBDD.c,v 1.30 2009/04/11 18:26:37 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifdef BDDcu
/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int heapCostCompare(const void *c1, const void *c2);
static int sat_ConvertCNF2BDD(satManager_t *cm, DdManager *mgr, int conflictFlag);
static void sat_FreeLinearHead(satLinearHead_t *head);
static int linearVarCompare(const void * node1, const void * node2);
static int linearElemCompare(const void * node1, const void * node2);
static void sat_GetArrangementByForce(satManager_t *cm, satLinearHead_t *head);
static int sat_PrintCutProfile(satManager_t *cm, satLinearHead_t *head, char *baseName, int printFlag);
static int sat_ClusteringElementMain(satManager_t *cm, satLinearHead_t *head);
static void sat_ComputeVariableRange(satManager_t *cm, satLinearHead_t *head);
static void sat_InitClusteringElement(satManager_t *cm, satLinearHead_t *head);
static void sat_PrintSupportVariable(satLinearHead_t *head, satLinearElem_t *e1);
static void sat_ClusteringGetCandidate(satManager_t *cm, satLinearHead_t *head);
static DdNode *sat_SmoothWithDeadVariable(DdManager *mgr, satArray_t *deadArray, DdNode *bdd1, DdNode *bdd2, int bddAndLimit);
static int sat_ClusteringElement(satManager_t *cm, satLinearHead_t *head);
static void sat_FreeCluster(DdManager *mgr, satLinearCluster_t *clu);
static void sat_CheckDeadNode(satLinearHead_t *head, satLinearCluster_t *clu);

/**AutomaticEnd***************************************************************/
#endif


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

#ifdef BDDcu

/**Function********************************************************************

  Synopsis    [Build monolithic BDD.]

  Description [Try to build a monolithic BDD from the set of clauses.
	       If it is succeeded then we can conclude whether given CNF is
	       satisfiable of not.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_TryToBuildMonolithicBDD(satManager_t *cm)
{
DdManager *mgr;
int nVariables, flag;

  nVariables = cm->initNumVariables - cm->implicatedSoFar;

  if(nVariables
	  > cm->option->maxLimitOfVariablesForMonolithicBDD)	return;

  mgr = Cudd_Init((unsigned int)(nVariables+1), 0, CUDD_UNIQUE_SLOTS,
		   CUDD_CACHE_SLOTS, getSoftDataLimit() / 10 * 9);
  cm->mgr = mgr;
  flag = sat_ConvertCNF2BDD(cm, mgr, 0);

  Cudd_Quit(mgr);
  cm->mgr = 0;

  if(flag == SAT_BDD_UNSAT)
    cm->status = SAT_UNSAT;

  return;
}


/**Function********************************************************************

  Synopsis    [Apply cofactoring to the set of BDDs.]

  Description [Apply cofactoring to the set of BDDs.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode *
sat_CofactorBDDArray(
	satLinearHead_t *head,
	DdManager *mgr,
	DdNode *l1,
	satArray_t *satArr)
{
int i, vid, inverted;
long v;
DdNode *bdd, *result, *nresult;
satLinearVar_t *var;

  result = l1;
  cuddRef(result);
  for(i=0; i<satArr->num; i++) {
    v = satArr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    vid = head->edge2vid[SATnodeID(v)];
    var = &(head->varHead[vid]);
    bdd = inverted ? Cudd_Not(var->bdd) : var->bdd;

    nresult = Cudd_bddConstrain(mgr, result, bdd);
    cuddRef(nresult);
    Cudd_RecursiveDeref(mgr, result);
    result = nresult;
  }
  return(result);
}

/**Function********************************************************************

  Synopsis    [Extract satisfying assignment from BDD.]

  Description [Since we quantify the variables if they are isolated,
	       the resulting BDD is ONE or ZERO. If BDD is ONE then the satisfying
	       assignments are extracted from the set of BDDs saved during clustering.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ExtractAssignmentFromBDD(
	satLinearHead_t *head,
	DdManager *mgr,
	satArray_t *arr,
	DdNode *cube)
{
DdNode *C, *T, *E, *zero;

  C = Cudd_Regular(cube);
  zero = Cudd_Not(DD_ONE(mgr));
  if (!cuddIsConstant(C)) {
    while (!cuddIsConstant(C)) {
      T = cuddT(C);
      E = cuddE(C);
      if (Cudd_IsComplement(cube)) {
	T = Cudd_Not(T);
	E = Cudd_Not(E);
      }
      if (T == zero)  { /** T == 0 **/
	  sat_ArrayInsert(arr, ((head->id2edge[C->index]) + 1));
	  cube = E;
      }
      else {                   /** E == 0 **/
	  sat_ArrayInsert(arr, (head->id2edge[C->index]));
	  cube = T;
      }
      C = Cudd_Regular(cube);
    }
  }
  return;
}


/**Function********************************************************************

  Synopsis    [Create  satLinearHead_t structure.]

  Description [Build initial data structure for linear arrangement and clustering.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satLinearHead_t *
sat_CreateLinearHead(
	satManager_t *cm,
	int conflictFlag)
{
satLinearHead_t *head;
satLinearElem_t *elem;
satLinearVar_t *lvar;
satArray_t *cArray, *vArray;
int nVars, nCls, varId;
int j, size, satisfied, inverted;
int value;
long v, *plit, i;
int elemIndex, varIndex;
int clauseLimit;

  nVars = 0;
  nCls = 0;
  cArray = sat_ArrayAlloc(1024);
  vArray = sat_ArrayAlloc(1024);
  for(i=satNodeSize; i<cm->initNodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & IsCNFMask))	continue;
    if(SATreadInUse(i) == 0)	continue;
  /**  CONSIDER conflict clause...   **/
    size = SATnumLits(i);
    satisfied = 0;
    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value == 1) {
	satisfied = 1;
	break;
      }
    }
    if(satisfied)	continue;

    nCls++;
    SATflags(i) |= VisitedMask;
    sat_ArrayInsert(cArray, i);

    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      v = SATnormalNode(v);
      if(SATvalue(v) < 2)	continue;
      if(!(SATflags(v) & VisitedMask)) {
	nVars++;
	SATflags(v) |= VisitedMask;
	sat_ArrayInsert(vArray, v);
      }
    }
  }

  if(conflictFlag)
    clauseLimit = cm->option->maxLimitOfClausesForBDDDPLL;
  else
    clauseLimit = cm->option->maxLimitOfClausesForMonolithicBDD;

  if(nCls > clauseLimit) {
    if(nVars > 100) {
      for(i=0; i<cArray->num; i++) {
	v = cArray->space[i];
	SATflags(v) &= ResetVisitedMask;
      }
      sat_ArrayFree(cArray);
      for(i=0; i<vArray->num; i++) {
	v = vArray->space[i];
	SATflags(v) &= ResetVisitedMask;
      }
      sat_ArrayFree(vArray);
      return(0);
    }
  }

  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "NOTICE : Apply BDD based method at level %d with %d vars %d cls\n", cm->currentDecision, nVars, nCls);
    fflush(cm->stdOut);
  }
  head = ALLOC(satLinearHead_t, 1);
  memset(head, 0, sizeof(satLinearHead_t));
  head->clausesArray = cArray;
  head->variablesArray = vArray;
  head->reordering = 1;
  head->nVars = nVars;
  head->nCls = nCls;
  head->bddLimit = 5000;
  head->bddAndLimit = 10000;

  head->elemHead = ALLOC(satLinearElem_t, nCls);
  memset(head->elemHead, 0, sizeof(satLinearElem_t)*nCls);
  head->varHead = ALLOC(satLinearVar_t, nVars);
  memset(head->varHead, 0, sizeof(satLinearVar_t)*nVars);

  head->elemArray = sat_ArrayAlloc(nCls);
  head->varArray = sat_ArrayAlloc(nVars);
  head->latestClusterArray = sat_ArrayAlloc(32);
  head->deadArray = sat_ArrayAlloc(nVars);

  head->id2edge = ALLOC(long, nVars+1);
  head->edge2id = ALLOC(int, cm->initNumVariables+1);
  head->edge2vid = ALLOC(int, cm->initNumVariables+1);

  varIndex = 0;
  for(i=0; i<vArray->num; i++) {
    v = vArray->space[i];
    SATflags(v) &= ResetVisitedMask;
    lvar = &(head->varHead[varIndex]);
    head->edge2vid[SATnodeID(v)] = varIndex;
    sat_ArrayInsert(head->varArray, (long)lvar);
    lvar->order = varIndex++;
    lvar->node = v;
    lvar->bQuantified = 1;
    lvar->clauses = sat_ArrayAlloc(4);
  }

  elemIndex = 0;
  for(i=0; i<cArray->num; i++) {
    v = cArray->space[i];
    SATflags(v) &= ResetVisitedMask;
    elem = &(head->elemHead[elemIndex]);
    sat_ArrayInsert(head->elemArray, (long)elem);
    elem->node = v;
    elem->order = elemIndex++;

    size = SATnumLits(v);
    elem->support = sat_ArrayAlloc(size);
    plit = (long *)SATfirstLit(v);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value == 0)	{
	continue;
      }
      varId = head->edge2vid[SATnodeID(v)];
      lvar = &(head->varHead[varId]);

      sat_ArrayInsert(lvar->clauses, (long)elem);
      if(inverted)	lvar = (satLinearVar_t *)SATnot((unsigned long)lvar);
      sat_ArrayInsert(elem->support, (long)lvar);
    }
  }
  return(head);
}


/**Function********************************************************************

  Synopsis    [Create  satLinearCluster_t  for each clutering candidate]

  Description [Create  satLinearCluster_t  for each clutering candidate]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satLinearCluster_t *
sat_CreateCluster(
	satLinearHead_t *head,
	satLinearElem_t *e1,
	satLinearElem_t *e2,
	int flagIndex,
	int *idArr)
{
satLinearCluster_t *clu;
satLinearVar_t *var;
satArray_t *support, *deadArray;
int from, to, nDead;
int nv, bddid;
int overlap, bddsize, j;

  memset(idArr, 0, sizeof(int)*(head->nVars));
  clu = ALLOC(satLinearCluster_t, 1);
  clu->elem1 = e1;
  clu->elem2 = e2;
  clu->deadArray = 0;
  from = e1->order;
  to = e2->order;
  nDead = 0;
  support = e1->support;
  for(j=0; j<support->num; j++) {
    var = (satLinearVar_t *)support->space[j];
    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
    nv = var->node;
    bddid = head->edge2id[SATnodeID(nv)];
    idArr[bddid] = 1;

    if(var->bQuantified && from <= var->from && var->to <= to) {
      nDead++;
      if(clu->deadArray == 0) {
	deadArray = sat_ArrayAlloc(2);
	clu->deadArray = deadArray;
      }
      else
	deadArray = clu->deadArray;
      sat_ArrayInsert(deadArray, (long)var);
    }
  }

  overlap = 0;
  support = e2->support;
  for(j=0; j<support->num; j++) {
    var = (satLinearVar_t *)support->space[j];
    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
    nv = var->node;
    bddid = head->edge2id[SATnodeID(nv)];
    if(idArr[bddid]) {
      if(from <= var->from && var->to <= to);
      else
	overlap++;
    }
    else {
      if(var->bQuantified && from <= var->from && var->to <= to) {
	nDead++;
	if(clu->deadArray == 0) {
	  deadArray = sat_ArrayAlloc(2);
	  clu->deadArray = deadArray;
	}
	else
	  deadArray = clu->deadArray;
	sat_ArrayInsert(deadArray, (long)var);
      }
    }
  }

  bddsize = Cudd_DagSize(e1->bdd) + Cudd_DagSize(e2->bdd);
  clu->overlap = overlap;
  clu->cost = (nDead<<7) + (overlap*(1024/bddsize)) + 10000/bddsize;
  clu->flag = flagIndex;

  return(clu);
}

/**Function********************************************************************

  Synopsis    [Print support variables of element(clause).]

  Description [Print support variables of element(clause).]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_PrintSupportVariable(
	satLinearHead_t *head,
	satLinearElem_t *e1)
{
satArray_t *support;
satLinearVar_t *var;
int j;
long nv;


  support = e1->support;
  for(j=0; j<support->num; j++) {
    var = (satLinearVar_t *)support->space[j];
    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
    nv = var->node;
/**    bddid = head->edge2id[SATnodeID(nv)]; **/
    fprintf(stdout, " %ld", nv);
  }
  fprintf(stdout, "\n");
}

/**Function********************************************************************

  Synopsis    [Compare function for heapify]

  Description [Compare function for heapify]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
heapCostCompare(const void *c1, const void *c2)
{
satLinearCluster_t *clu1, *clu2;

  clu1 = (satLinearCluster_t *)c1;
  clu2 = (satLinearCluster_t *)c2;
  return(clu1->cost < clu2->cost);
}

/**Function********************************************************************

  Synopsis    [Create initial clustering candidates]

  Description [Create initial clustering candidates]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_ClusteringGetCandidate(
	satManager_t *cm,
	satLinearHead_t *head)
{
int i, *idArr;
satArray_t *eArr;
satLinearElem_t *e1, *e2;
satLinearCluster_t *clu;

  eArr = head->elemArray;
  head->heap = Heap_HeapInitCompare(eArr->num+2, heapCostCompare);

  idArr = ALLOC(int, head->nVars);
  for(i=0; i<eArr->num; i++) {

    e1 = (satLinearElem_t *)eArr->space[i];
    if(i == eArr->num-1)
      continue;
    else
      e2 = (satLinearElem_t *)eArr->space[i+1];

    e1->flag = 1;
    e2->flag = 1;
    clu = sat_CreateCluster(head, e1, e2, 1, idArr);

    Heap_HeapInsertCompare(head->heap, (void *)clu, (long)clu);
  }

  free(idArr);

}

/**Function********************************************************************

  Synopsis    [Apply existential qunatification for cluster.]

  Description [Apply existential qunatification for cluster.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static DdNode *
sat_SmoothWithDeadVariable(
	DdManager *mgr,
	satArray_t *deadArray,
	DdNode *bdd1,
	DdNode *bdd2,
	int bddAndLimit)
{
satLinearVar_t *var;
DdNode *cube, *ncube;
DdNode *result;
int i;


  cube = DD_ONE(mgr);
  cuddRef(cube);
  for(i=0; i<deadArray->num; i++) {
    var = (satLinearVar_t *)deadArray->space[i];
    ncube = Cudd_bddAnd(mgr,cube,var->bdd);
    if(ncube == NULL) {
      Cudd_RecursiveDeref(mgr, cube);
      return(NULL);
    }
    cuddRef(ncube);
    Cudd_RecursiveDeref(mgr, cube);
    cube = ncube;
  }


  result = Cudd_bddAndAbstractLimit(
	      mgr,bdd1,bdd2,cube,bddAndLimit);
  if(result == NULL) {
    Cudd_RecursiveDeref(mgr, cube);
    return(NULL);
  }
  cuddRef(result);
  Cudd_RecursiveDeref(mgr, cube);
  cuddDeref(result);

  return(result);
}

/**Function********************************************************************

  Synopsis    [Apply clustering.]

  Description [Apply clustering.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
sat_ClusteringElement(
	satManager_t *cm,
	satLinearHead_t *head)
{
int modified, total, size;
int found, i, vid, index;
long v;
int *idArr, *idSupport;
int limit, nElem;
satLinearElem_t *e1, *e2;
satLinearVar_t *lvar;
satLinearCluster_t *clu, *tclu;
satArray_t *support, *deadArray;
satArray_t *neArr, *eArr;
DdManager *mgr;
DdNode *result, *zero;
Heap_t *heap;
long dummy;

  heap = head->heap;
  modified = 0;

  idArr = ALLOC(int, head->nVars);

  mgr = head->mgr;
  eArr = head->elemArray;
  /**
  if(eArr->num <= 5 && head->reordering)
    Cudd_ReduceHeap(mgr,mgr->autoMethod,10);
    **/

  zero = Cudd_Not(DD_ONE(mgr));
  limit = ((eArr->num)>>1);
  nElem = eArr->num;

  if(cm->option->verbose > 3)
    fprintf(cm->stdOut, " ------- %d element\n", nElem);

  while(Heap_HeapExtractMin(heap, &clu, &dummy)) {
    if(modified > limit) {
      sat_FreeCluster(mgr, clu);
      continue;
    }
    e1 = clu->elem1;
    e2 = clu->elem2;
    if(e1->flag == 0 || e2->flag == 0) {
      sat_FreeCluster(mgr, clu);
      continue;
    }
    if(e1->flag > clu->flag || e2->flag > clu->flag) {
      sat_FreeCluster(mgr, clu);
      continue;
    }
    deadArray = clu->deadArray;
    if(deadArray) {
      cuddRef(e1->bdd);
      cuddRef(e2->bdd);
      result = sat_SmoothWithDeadVariable(
	      mgr, deadArray, e1->bdd, e2->bdd, head->bddAndLimit);
      if(result)
	cuddRef(result);
      Cudd_RecursiveDeref(mgr, e1->bdd);
      Cudd_RecursiveDeref(mgr, e2->bdd);
      for(i=0; i<deadArray->num; i++) {
	lvar = (satLinearVar_t *)deadArray->space[i];
	sat_ArrayInsert(head->deadArray, (long)lvar);
      }
    }
    else {
      result = Cudd_bddAndLimit(mgr,e1->bdd,e2->bdd,head->bddAndLimit);
      if(result)
	cuddRef(result);
    }

    total = Cudd_ReadKeys(mgr) - Cudd_ReadDead(mgr);
    if(total > 100000 && head->reordering) {
      head->reordering = 0;
      Cudd_AutodynDisable(mgr);
    }

    if(result) {
	/**  CONSIDER the case that result is DD_ZERO... **/
      nElem--;
      if(cm->option->verbose > 3) {
	fprintf(cm->stdOut, " (%4d %4d) %4d(%3d, %3ld): %d X %d = %d\n",
	      e1->order, e2->order,
	      clu->cost, clu->overlap, deadArray ? deadArray->num : 0,
	      Cudd_DagSize(e1->bdd), Cudd_DagSize(e2->bdd),
	      Cudd_DagSize(result));
	sat_PrintSupportVariable(head, e1);
	sat_PrintSupportVariable(head, e2);
	if(deadArray) {
	for(i=0; i<deadArray->num; i++) {
	  lvar = (satLinearVar_t *)deadArray->space[i];
	  fprintf(cm->stdOut, "%ld ", lvar->node);
	}
	}
	fprintf(cm->stdOut, "\n");
      }
      modified++;
      e1->flag += 1;
      e2->flag = 0;

      if(nElem < 50) {
	sat_ArrayInsert(head->latestClusterArray, (long)(e1->bdd));
	cuddRef(e1->bdd);
	sat_ArrayInsert(head->latestClusterArray, (long)(e2->bdd));
	cuddRef(e2->bdd);
      }

      Cudd_RecursiveDeref(mgr, e1->bdd);
      Cudd_RecursiveDeref(mgr, e2->bdd);
      e1->bdd = result;
      e2->bdd = 0;
      sat_ArrayFree(e1->support);
      e1->support = 0;
      support = e2->support;
      for(i=0; i<support->num; i++) {
	lvar = (satLinearVar_t *)support->space[i];
	if(lvar->to == e2->order)
	  lvar->to = e1->order;
	if(lvar->from == e2->order)
	  lvar->from = e1->order;
      }
      sat_ArrayFree(e2->support);
      e2->support = 0;

      size = (unsigned int)Cudd_ReadSize(mgr);
      idSupport = Cudd_SupportIndex(mgr,result);
      e1->support = support = sat_ArrayAlloc(10);
      for (i = 0; i < size; i++) {
	if(idSupport[i]) {
	  v = head->id2edge[i];
	  vid = head->edge2vid[SATnodeID(v)];
	  lvar = &(head->varHead[vid]);
	  sat_ArrayInsert(support, (long)lvar);
	  /**
	  if(lvar->to == e2->order)
	    lvar->to = e1->order;
	  if(lvar->from == e2->order)
	    lvar->from = e1->order;
	    **/
	}
      }
      free(idSupport);

      found = 0;
      for(i=e1->order-1; i>=0; i--)  {
	e2 = (satLinearElem_t *)eArr->space[i];
	if(e2->flag)	{
	  found = 1;
	  break;
	}
      }
      if(found) {
	tclu = sat_CreateCluster(head, e2, e1, e1->flag, idArr);
	Heap_HeapInsertCompare(head->heap, (void *)tclu, (long)tclu);
      }

      found = 0;
      for(i=e1->order+1; i<eArr->num; i++)  {
	e2 = (satLinearElem_t *)eArr->space[i];
	if(e2->flag)	{
	  found = 1;
	  break;
	}
      }
      if(found) {
	tclu = sat_CreateCluster(head, e1, e2, e1->flag, idArr);
	Heap_HeapInsertCompare(head->heap, (void *)tclu, (long)tclu);
      }
    }
    sat_FreeCluster(mgr, clu);
  }

  Heap_HeapFree(heap);
  head->heap = 0;

  free(idArr);

  if(modified) {
    eArr = head->elemArray;
    neArr = sat_ArrayAlloc(eArr->num);
    index = 0;
    for(i=0; i<eArr->num; i++) {
      e1 = (satLinearElem_t *)eArr->space[i];
      if(e1->flag == 0)	continue;

      e1->order = index++;
      sat_ArrayInsert(neArr, (long)e1);
    }
    sat_ArrayFree(eArr);
    head->elemArray = neArr;
  }

  if(head->elemArray->num == 1)
    modified = 0;

  return(modified);
}


/**Function********************************************************************

  Synopsis    [Free satLinearCluster_t]

  Description [Free satLinearCluster_t]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_FreeCluster(DdManager *mgr, satLinearCluster_t *clu)
{
satArray_t *deadArray;

  deadArray = clu->deadArray;
  if(deadArray) {
    sat_ArrayFree(deadArray);
  }
  free(clu);
}


/**Function********************************************************************

  Synopsis    [Sanity check for dead node]

  Description [Sanity check for dead node]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_CheckDeadNode(
	satLinearHead_t *head,
	satLinearCluster_t *clu)
{
satArray_t *deadArray, *eArr;
satArray_t *support;
satLinearVar_t *var, *tvar;
satLinearElem_t *elem;
int i, j, k;


  if(clu->deadArray) {
    deadArray = clu->deadArray;
    for(i=0; i<deadArray->num; i++) {
      var = (satLinearVar_t *)deadArray->space[i];
      eArr = head->elemArray;
      for(j=0; j<var->from; j++) {
	elem = (satLinearElem_t *)eArr->space[j];
	if(elem->flag == 0)	continue;
	support = elem->support;
	for(k=0; k<support->num; k++) {
	  tvar = (satLinearVar_t *)support->space[k];
	  tvar = (satLinearVar_t *)SATnormalNode((unsigned long)tvar);
	  if(var == tvar) {
	    fprintf(stdout, "Error : wrong variable range\n");
	  }
	}
      }
      for(j=var->to+1; j<eArr->num; j++) {
	elem = (satLinearElem_t *)eArr->space[j];
	if(elem->flag == 0)	continue;
	support = elem->support;
	for(k=0; k<support->num; k++) {
	  tvar = (satLinearVar_t *)support->space[k];
	  tvar = (satLinearVar_t *)SATnormalNode((unsigned long)tvar);
	  if(var == tvar) {
	    fprintf(stdout, "Error : wrong variable range\n");
	  }
	}
      }
    }
  }
}

/**Function********************************************************************

  Synopsis    [Convert CNF into BDD.]

  Description [First, the force based clauses arrangement is applied to get
	       a min max -cut arrangement of clauses.
	       Then apply the iterative clustering algorithm to get a monolithic
	       BDD.]

  SideEffects []

  SeeAlso     [sat_TryToBuildMonolithicBDD]

******************************************************************************/
static int
sat_ConvertCNF2BDD(
	satManager_t *cm,
	DdManager *mgr,
	int conflictFlag)
{
satLinearHead_t *head;
DdNode *result, *cube;
DdNode *l1, *l2;
DdNode *nl1, *nl2;
satArray_t *satArr, *arr;
int limitCut;
int flag, length;
int cut, i;

  head = sat_CreateLinearHead(cm, conflictFlag);

  if(head == 0)	return(0);

  head->mgr = mgr;

  sat_GetArrangementByForce(cm, head);

  if(cm->option->verbose > 3)
    cut = sat_PrintCutProfile(cm, head, "final", 1);
  else
    cut = sat_PrintCutProfile(cm, head, "final", 0);

  if(conflictFlag)
    limitCut = cm->option->maxLimitOfCutSizeForBDDDPLL;
  else
    limitCut = cm->option->maxLimitOfCutSizeForMonolithicBDD;
  if(cut > limitCut) {
    sat_FreeLinearHead(head);
    return(SAT_BDD_BACKTRACK);
  }

  flag = sat_ClusteringElementMain(cm, head);

  if(flag == SAT_BDD_SAT) {
    arr = head->latestClusterArray;
    satArr = sat_ArrayAlloc(16);
    for(i=arr->num-1; i>=0; i--) {
      l1 = (DdNode *)arr->space[i];
      i--;
      l2 = (DdNode *)arr->space[i];
      nl1 = sat_CofactorBDDArray(head, mgr, l1, satArr);
      nl2 = sat_CofactorBDDArray(head, mgr, l2, satArr);
      result = Cudd_bddAndLimit(mgr, nl1, nl2, head->bddAndLimit);
      cuddRef(result);
      Cudd_RecursiveDeref(mgr, nl1);
      Cudd_RecursiveDeref(mgr, nl2);
      cube = Cudd_LargestCube(mgr, result, &length);
      cuddRef(cube);
      sat_ExtractAssignmentFromBDD(head, mgr, satArr, cube);
      Cudd_RecursiveDeref(mgr, cube);
      Cudd_RecursiveDeref(mgr, result);
    }
    cm->assignByBDD = satArr;
  }
  sat_FreeLinearHead(head);

  return(flag);
}

/**Function********************************************************************

  Synopsis    [Free  satLinearHead_t structure.]

  Description [Free  satLinearHead_t structure.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_FreeLinearHead(satLinearHead_t *head)
{
satLinearElem_t *elem;
satLinearVar_t *var;
satArray_t *eArr, *vArr, *arr;
satArray_t *support, *clauses;
DdNode *bdd;
int i;

  eArr = head->elemArray;
  if(eArr) {
    for(i=0; i<eArr->num; i++) {
      elem = (satLinearElem_t *)(eArr->space[i]);
      support = elem->support;
      if(support)
	sat_ArrayFree(support);
      if(elem->bdd)
	Cudd_RecursiveDeref(head->mgr, elem->bdd);
    }
  }
  vArr = head->varArray;
  if(vArr) {
    for(i=0; i<vArr->num; i++) {
      var = (satLinearVar_t *)vArr->space[i];
      clauses = var->clauses;
      if(clauses)
	sat_ArrayFree(clauses);
      if(var->bdd)
	Cudd_RecursiveDeref(head->mgr, var->bdd);
    }
  }

  if(head->variablesArray)
    sat_ArrayFree(head->variablesArray);
  if(head->clausesArray)
    sat_ArrayFree(head->clausesArray);

  if(head->elemHead)
    free(head->elemHead);
  if(head->varHead)
    free(head->varHead);
  if(head->id2edge)
    free(head->id2edge);
  if(head->edge2id)
    free(head->edge2id);
  if(head->edge2vid)
    free(head->edge2vid);

  if(head->latestClusterArray)	{
    arr = head->latestClusterArray;
    for(i=0; i<arr->num; i++) {
      bdd = (DdNode *)arr->space[i];
      Cudd_RecursiveDeref(head->mgr, bdd);
    }
    sat_ArrayFree(arr);
    head->latestClusterArray = 0;
  }

  if(head->deadArray)
    free(head->deadArray);
  free(head);
}


/**Function********************************************************************

  Synopsis    [Variable comparing function for sorting.]

  Description [Variable comparing function for sorting.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
linearVarCompare(
  const void * node1,
  const void * node2)
{
  satLinearVar_t *d1;
  satLinearVar_t *d2;

  d1 = *(satLinearVar_t **)(node1);
  d2 = *(satLinearVar_t **)(node2);

  return (d1->pos > d2->pos);
}

/**Function********************************************************************

  Synopsis    [Element comparing function for sorting.]

  Description [Element comparing function for sorting.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
linearElemCompare(
  const void * node1,
  const void * node2)
{
  satLinearElem_t *d1;
  satLinearElem_t *d2;

  d1 = *(satLinearElem_t **)(node1);
  d2 = *(satLinearElem_t **)(node2);

  return (d1->pos > d2->pos);
}

/**Function********************************************************************

  Synopsis    [Generate linear arrangement by force relaxation.]

  Description [Generate linear arrangement by force relaxation.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_GetArrangementByForce(
	satManager_t *cm,
	satLinearHead_t *head)
{
int iteration;
double prespan, span;
int from, to, sum;
int i, j, inverted;
satLinearElem_t *elem;
satLinearVar_t *var;
satArray_t *eArr, *vArr;
satArray_t *support, *clauses;

  iteration = 0;
  prespan = MAXINT;
  eArr = head->elemArray;
  vArr = head->varArray;
  while(1) {
    iteration++;
    if(iteration > 200)	break;

    span = 0;
    for(i=0; i<eArr->num; i++) {
      elem = (satLinearElem_t *)(eArr->space[i]);
      support = elem->support;
      sum = 0;
      from = MAXINT;
      to = -1;
      for(j=0; j<support->num; j++) {
	var = (satLinearVar_t *)(support->space[j]);
	inverted = SATisInverted((unsigned long)var);
	var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
	sum += var->order;
	if(var->order < from)	from = var->order;
	if(to < var->order)	to = var->order;
      }
      if(from != MAXINT && to != -1)
	span += (double)(to - from);
      elem->pos = sum / (double)(support->num);
    }

    if(iteration > 2 && (prespan * 0.9999) < span)
      break;
    prespan = span;

    qsort(eArr->space, eArr->num, sizeof(satLinearElem_t *), linearElemCompare);
    for(i=0; i<eArr->num; i++) {
      elem = (satLinearElem_t *)eArr->space[i];
      elem->order = i;
    }

    for(i=0; i<vArr->num; i++) {
      var = (satLinearVar_t *)vArr->space[i];
      clauses = var->clauses;
      sum = 0;
      for(j=0; j<clauses->num; j++) {
	elem = (satLinearElem_t *)clauses->space[j];
	sum += elem->order;
      }
      var->pos = sum / (double)(clauses->num);
    }

    qsort(vArr->space, vArr->num, sizeof(satLinearVar_t *), linearVarCompare);
    for(i=0; i<vArr->num; i++) {
      var = (satLinearVar_t *)vArr->space[i];
      var->order = i;
    }
  }
  if(cm->option->verbose > 3)
    fprintf(cm->stdOut, "NOTICE : %d iteration for force based arrangement\n", iteration);
}

/**Function********************************************************************

  Synopsis    [Print profile of cur from linear arrangement.]

  Description [Print profile of cur from linear arrangement.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
sat_PrintCutProfile(
	satManager_t *cm,
	satLinearHead_t *head,
	char *baseName,
	int printFlag)
{
st_table *cutTable;
st_generator *gen;
FILE *fout = NIL(FILE);
int i, j, cut, sum;
int to, from;
char filename[1024];
satArray_t *support, *clauses, *eArr, *vArr;
satLinearElem_t *elem;
satLinearVar_t *var;
double span;

  eArr = head->elemArray;
  span = 0;
  for(i=0; i<eArr->num; i++) {
    elem = (satLinearElem_t *)eArr->space[i];
    support = elem->support;
    sum = 0;
    to = -1;
    from = MAXINT;
    for(j=0; j<support->num; j++) {
      var = (satLinearVar_t *)support->space[j];
      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
      sum += var->order;
      if(to < var->order)	to = var->order;
      if(var->order < from)	from = var->order;
    }
    elem->to = to;
    if(from != MAXINT && to != -1)
      span += (double)(to - from);
  }

  cut = 0;
  if(printFlag) {
    sprintf(filename, "%s.data", baseName);
    fout = fopen(filename, "w");
  }
  cutTable = st_init_table(st_ptrcmp, st_ptrhash);
  vArr = head->varArray;
  for(i=0; i<vArr->num; i++) {
    var = (satLinearVar_t *)vArr->space[i];
    clauses = var->clauses;
    for(j=0; j<clauses->num; j++) {
      elem = (satLinearElem_t *)clauses->space[j];
      st_insert(cutTable, (char *)elem, (char *)elem);
    }
    st_foreach_item(cutTable, gen, &elem, &elem) {
      if(elem->to <= i)
	st_delete(cutTable, &elem, NIL(char *));
    }
    if(cut < cutTable->num_entries)
      cut = cutTable->num_entries;
    if(printFlag)
      fprintf(fout, "%d %d\n", i, cutTable->num_entries);
  }
  st_free_table(cutTable);

  if(printFlag) {
    fclose(fout);
    sprintf(filename, "%s.gnu", baseName);
    fout = fopen(filename, "w");
    fprintf(fout, "set terminal postscript \n");
    fprintf(fout, "set output \"%s.ps\"\n", baseName);
    fprintf(fout, "set title \"profile of live variable span %f cut %d\"\n",
	    span, cut);
    fprintf(fout, "plot \"%s.data\" using 1:2 title \"%s\" with lines\n", baseName, "cut");
    fclose(fout);
  }

  return cut;

}

/**Function********************************************************************

  Synopsis    [Clustering on linear arrangement.]

  Description [Clustering on linear arrangement.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
sat_ClusteringElementMain(
	satManager_t *cm,
	satLinearHead_t *head)
{
int modified;
satLinearElem_t *elem;
DdNode *one;

  Cudd_AutodynEnable(head->mgr, CUDD_REORDER_SIFT);

  sat_InitClusteringElement(cm, head);

  while(1) {
    sat_ComputeVariableRange(cm, head);
    sat_ClusteringGetCandidate(cm, head);
    modified = sat_ClusteringElement(cm, head);
    if(modified == 0)	break;
  }

  if(head->elemArray->num == 1) {
    one = DD_ONE(head->mgr);
    elem = (satLinearElem_t *)(head->elemArray->space[0]);
    if(elem->bdd == one)		return(SAT_BDD_SAT);
    else if(elem->bdd == Cudd_Not(one))	return(SAT_BDD_UNSAT);
    else				return(SAT_BDD_BACKTRACK);
  }
  else {
    return(SAT_BDD_BACKTRACK);
  }
}

/**Function********************************************************************

  Synopsis    [Compute the range of variables.]

  Description [Compute the range of variables.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_ComputeVariableRange(
	satManager_t *cm,
	satLinearHead_t *head)
{
satArray_t *support, *vArr, *eArr;
satLinearElem_t *elem;
satLinearVar_t *var;
int i, j;

  vArr = head->varArray;
  eArr = head->elemArray;

  for(i=0; i<vArr->num; i++) {
    var = (satLinearVar_t *)vArr->space[i];
    var->from = MAXINT;
    var->to = -1;
  }

  for(i=0; i<eArr->num; i++) {
    elem = (satLinearElem_t *)eArr->space[i];
    support = elem->support;
    for(j=0; j<support->num; j++) {
      var = (satLinearVar_t *)support->space[j];
      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
      if(elem->order < var->from)	var->from = elem->order;
      if(var->to < elem->order)		var->to = elem->order;
    }
  }
}

/**Function********************************************************************

  Synopsis    [Preparation for the clutering.]

  Description [Preparation for the clutering.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
sat_InitClusteringElement(
	satManager_t *cm,
	satLinearHead_t *head)
{
DdNode *sum, *nsum, *one;
DdManager *mgr;
satLinearElem_t *elem;
satLinearVar_t *var;
satArray_t *support, *vArr, *eArr;
int i, j, index;
long nv;
int inverted;

  mgr = head->mgr;
  vArr = head->varArray;
  eArr = head->elemArray;
  index = 0;
  one = DD_ONE(mgr);

  for(i=0; i<vArr->num; i++) {
    var = (satLinearVar_t *)vArr->space[i];
    nv = var->node;
    head->id2edge[index] = nv;
    head->edge2id[SATnodeID(nv)] = index;
    var->bdd = cuddUniqueInter(mgr,index,one,Cudd_Not(one));
    cuddRef(var->bdd);
    index++;
  }

  for(i=0; i<eArr->num; i++) {
    elem = (satLinearElem_t *)eArr->space[i];
    support = elem->support;
    sum = Cudd_Not(one);
    cuddRef(sum);
    for(j=0; j<support->num; j++) {
      var = (satLinearVar_t *)support->space[j];
      inverted = SATisInverted((unsigned long)var);
      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
      nsum = Cudd_bddAnd(mgr,Cudd_Not(sum),
			     (inverted ? var->bdd : Cudd_Not(var->bdd)));
      nsum = Cudd_Not(nsum);
      cuddRef(nsum);

      Cudd_RecursiveDeref(mgr,sum);
      sum = nsum;
    }
    elem->bdd = sum;
  }
}

#endif
#ifndef BDDcu
/**Function********************************************************************

  Synopsis    [Build monolithic BDD.]

  Description [Try to build a monolithic BDD from the set of clauses.
	       If it is succeeded then we can conclude whether given CNF is
	       satisfiable of not.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_TryToBuildMonolithicBDD(satManager_t *cm)
{
  fprintf(stderr, "Warning : This feature is only availabe with CUDD package\n");
  return;
}
#endif