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

  FileName    [satUtil.c]

  PackageName [sat]

  Synopsis    [Routines for various utility function.]

  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"

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

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

/**AutomaticStart*************************************************************/

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

static int NodeIndexCompare(const void *x, const void *y);

/**AutomaticEnd***************************************************************/


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


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

  Synopsis    [ Add conflict clause into clause database]

  Description [ Add conflict clause into clause database]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddConflictClause(
	satManager_t *cm,
	satArray_t *clauseArray,
	int objectFlag)
{
satStatistics_t *stats;
satLiteralDB_t *literals;
satVariable_t *var;
long v, c;
int inverted;
long *last;
long *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;

    var = SATgetVariable(v);

    if(inverted){
      (var->litsCount[0])++;
      (var->conflictLits[0])++;
    }
    else	{
      (var->litsCount[1])++;
      (var->conflictLits[1])++;
    }
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
	maxLevel = level;
	maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
	sat_AddWL(cm, c, i, -1);
	break;
      }
      else {
	level = SATlevel(v);
	if(level > maxLevel) {
	  maxLevel = level;
	  maxIndex = i;
	}
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);


  SATflags(c) |= IsConflictMask;

  stats = cm->each;
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
  if(objectFlag) {
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    SATflags(c) |= ObjMask;
  }
  else {
    stats->nNonobjConflictCl++;
    stats->nNonobjConflictLit += clauseArray->num;
    SATflags(c) |= NonobjMask;
  }


  return(c);
}

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

  Synopsis    [ Add conflict clause into clause database without updating score]

  Description [ Add conflict clause into clause database without updating score]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddConflictClauseNoScoreUpdate(
	satManager_t *cm,
	satArray_t *clauseArray,
	int objectFlag)
{
satStatistics_t *stats;
satLiteralDB_t *literals;
satVariable_t *var;
long v, c;
int inverted;
long *last;
long *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;

    var = SATgetVariable(v);

    if(inverted){
      (var->litsCount[0])++;
      (var->conflictLits[0])++;
    }
    else	{
      (var->litsCount[1])++;
      (var->conflictLits[1])++;
    }
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
	maxLevel = level;
	maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
	sat_AddWL(cm, c, i, -1);
	break;
      }
      else {
	level = SATlevel(v);
	if(level > maxLevel) {
	  maxLevel = level;
	  maxIndex = i;
	}
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);


  SATflags(c) |= IsConflictMask;

  stats = cm->each;
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
  if(objectFlag) {
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    SATflags(c) |= ObjMask;
  }
  else {
    stats->nNonobjConflictCl++;
    stats->nNonobjConflictLit += clauseArray->num;
    SATflags(c) |= NonobjMask;
  }


  return(c);
}
/**Function********************************************************************

  Synopsis    [ Add unit conflict clause into clause database]

  Description [ Add unit conflict clause into clause database]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddUnitConflictClause(
	satManager_t *cm,
	satArray_t *clauseArray,
	int objectFlag)
{
satLiteralDB_t *literals;
satStatistics_t *stats;
long c, v;
int inverted;
long *last, *space;
int i, size;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  SATflags(c) |= IsConflictMask;
  stats = cm->each;
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
  if(objectFlag) {
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    SATflags(c) |= ObjMask;
  }
  else {
    stats->nNonobjConflictCl++;
    stats->nNonobjConflictLit += clauseArray->num;
    SATflags(c) |= NonobjMask;
  }

  return(c);
}
/**Function********************************************************************

  Synopsis    [ Add unit blocking clause into clause database]

  Description [ Add unit blocking clause into clause database]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddUnitBlockingClause(
	satManager_t *cm,
	satArray_t *clauseArray)
{
satLiteralDB_t *literals;
satStatistics_t *stats;
long c, v;
int inverted;
long *last, *space;
int i, size;

  literals = cm->literals;
  stats = cm->each;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  SATflags(c) |= IsBlockingMask;

  stats = cm->each;
  stats->nBlockingCl++;
  stats->nBlockingLit += clauseArray->num;
  return(c);
}


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

  Synopsis    [ Add unit conflict clause into clause database]

  Description [ Add unit conflict clause into clause database]

  SideEffects [ UNSAT Core generation]

  SeeAlso     []

******************************************************************************/
long
sat_AddUnitClause(
	satManager_t *cm,
	satArray_t *clauseArray)
{
satLiteralDB_t *literals;
long c = 0, v;
int inverted;
long *last, *space;
int i, size;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }


  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);


  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  return(c);
}

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

  Synopsis    [ Add conflict clause into clause database]

  Description [ Add conflict clause into clause database]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddClauseIncremental(
	satManager_t *cm,
	satArray_t *clauseArray,
	int objectFlag,
	int fromDistill)
{
satLiteralDB_t *literals;
satStatistics_t *stats;
satVariable_t *var;
long c, v;
int inverted;
long *last, *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;
  stats = cm->each;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);

  last = literals->last;
  *(last) = (-c);
  last++;


  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;

    var = SATgetVariable(v);
    if(inverted){
      if(fromDistill)
	(var->litsCount[0])++;
      (var->conflictLits[0])++;
    }
    else	{
      if(fromDistill)
	(var->litsCount[1])++;
      (var->conflictLits[1])++;
    }
  }
  *(last) = (-c);
  last++;

  literals->last = last;


  /* Bing: UNSAT core generation */
 if(clauseArray->num>1){
  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
	maxLevel = level;
	maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
	sat_AddWL(cm, c, i, -1);
	break;
      }
      else {
	level = SATlevel(v);
	if(level > maxLevel) {
	  maxLevel = level;
	  maxIndex = i;
	}
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);
 }

  if(objectFlag)SATflags(c) |= ObjMask;
  else		SATflags(c) |= NonobjMask;
  /*SATflags(c) |= IsConflictMask;*/
  //Bing:change??
  if(!cm->option->coreGeneration)
    SATflags(c) |= IsConflictMask;

  if(objectFlag) {
    stats->nInitObjConflictCl++;
    stats->nInitObjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
  }
  else {
    stats->nInitNonobjConflictCl++;
    stats->nInitNonobjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
  }
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;

  return(c);
}

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

  Synopsis    [ Add clause into clause database]

  Description [ Add clause into clause database]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddClause(
	satManager_t *cm,
	satArray_t *clauseArray)
{
satLiteralDB_t *literals;
long c, v;
int inverted;
long *last, *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }
  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);

  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
	maxLevel = level;
	maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
	sat_AddWL(cm, c, i, -1);
	break;
      }
      else {
	level = SATlevel(v);
	if(level > maxLevel) {
	  maxLevel = level;
	  maxIndex = i;
	}
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);


  return(c);
}

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

  Synopsis    [ Add clause into clause database]

  Description [ Add clause into clause database]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_AddBlockingClause(
	satManager_t *cm,
	satArray_t *clauseArray)
{
satLiteralDB_t *literals;
satStatistics_t *stats;
long c, v;
int inverted;
long *last, *space;
int i, size;
int maxLevel, maxIndex;
int value, level;
int otherWLIndex;

  literals = cm->literals;
  stats = cm->each;

  while(literals->last + clauseArray->num + 2 >= literals->end) {
    if(!sat_EnlargeLiteralDB(cm)) {
      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
	      cm->comment);
      exit(0);
    }
  }

  if(clauseArray->num == 1)
    return(sat_AddUnitBlockingClause(cm, clauseArray));

  c = 0;
  if(cm->unusedAigQueue)
    c = sat_Dequeue(cm->unusedAigQueue);
  if(c == 0)
    c = sat_CreateNode(cm, 2, 2);

  last = literals->last;
  *(last) = (-c);
  last++;

  /**
  SATfirstLit(c) = (int)last;
  **/
  (cm->nodesArray[c+satFirstLit]) = (long)last;
  SATnumLits(c) = clauseArray->num;
  SATflags(c) |= IsCNFMask;
  SATsetInUse(c);
  SATnumConflict(c) = 0;

  size = clauseArray->num;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = !SATisInverted(v);
    v = SATnormalNode(v);

    *(last) = ((v^inverted) << 2);
    last++;
  }
  *(last) = (-c);
  last++;

  literals->last = last;

  maxLevel = -1;
  maxIndex = -1;
  otherWLIndex = -1;
  space = clauseArray->space;
  for(i=0; i<size; i++, space++) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(value == 2) {
      sat_AddWL(cm, c, i, 1);
      otherWLIndex = i;
      break;
    }
    else {
      level = SATlevel(v);
      if(level > maxLevel) {
	maxLevel = level;
	maxIndex = i;
      }
    }
  }
  if(i >= size) {
    sat_AddWL(cm, c, maxIndex, 1);
    otherWLIndex = maxIndex;
  }

  maxLevel = -1;
  maxIndex = -1;
  space = clauseArray->space+size-1;
  for(i=size-1; i>=0; i--, space--) {
    v = *space;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v);
    if(i != otherWLIndex) {
      if(value == 2) {
	sat_AddWL(cm, c, i, -1);
	break;
      }
      else {
	level = SATlevel(v);
	if(level > maxLevel) {
	  maxLevel = level;
	  maxIndex = i;
	}
      }
    }
  }
  if(i < 0)
    sat_AddWL(cm, c, maxIndex, -1);

  SATflags(c) |= IsBlockingMask;

  stats = cm->each;
  stats->nBlockingCl++;
  stats->nBlockingLit += clauseArray->num;

  return(c);
}


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

  Synopsis    [ Make literal watched ]

  Description [ Make literal watched ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_AddWL(
	satManager_t *cm,
	long c,
	int index,
	int dir)
{
long *plit, v;
int inverted;
satVariable_t *var;

  plit = (long*)SATfirstLit(c) + index;
  v = SATgetNode(*plit);
  inverted = !SATisInverted(v);
  v = SATnormalNode(v);
  var = SATgetVariable(v);

  if(var->wl[inverted] == 0)
    var->wl[inverted] = sat_ArrayAlloc(4);
  sat_ArrayInsert(var->wl[inverted], (long)plit);
  SATsetWL(plit, dir);
}


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

  Synopsis    [ Allocate array ]

  Description [ Allocate array ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satArray_t *
sat_ArrayAlloc(long number)
{
satArray_t *array;

  array = ALLOC(satArray_t, 1);
  if (array) {
    array->num = 0;
    array->size = number;
    array->space = ALLOC(long, number);
    if (array->space) {
      return array;
    }
  }
  //Bing: To avoid segmentation fault
  if(array==0 || (number>0&&array->space==0)){
    printf("can't alloc mem, exit\n");
    exit(0);
  }
  return 0;
}

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

  Synopsis    [ Duplicate array ]

  Description [ Duplicate array ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satArray_t *
sat_ArrayDuplicate(satArray_t *old)
{
satArray_t *array;

  array = (satArray_t *)malloc(sizeof(satArray_t));
  if (array) {
    array->num = old->num;
    array->size = old->num;
    array->space = (long *)malloc(sizeof(long) * old->num);
    memcpy(array->space, old->space, sizeof(long)*old->num);
    if (array->space) {
      return array;
    }
  }
  return 0;
}

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

  Synopsis    [ Insert entries to array ]

  Description [ Insert entries to array ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ArrayInsert(satArray_t *array, long datum)
{
  if(array->num < array->size) {
    array->space[array->num++] = datum;
  }
  else {
    array->size <<= 1;
    array->space = REALLOC(long, array->space, array->size);
    if(array->space == 0) {
      fprintf(stdout, "ERROR : Can't allocate memory in sat_ArrayInsert\n");
      exit(0);
    }
    array->space[array->num++] = datum;
  }
}

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

  Synopsis    [ Free array ]

  Description [ Free array ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ArrayFree(satArray_t *array)
{
  free(array->space);
  free(array);
}


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

  Synopsis    [ Create queue ]

  Description [ Create queue ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satQueue_t *
sat_CreateQueue( long MaxElements )
{
satQueue_t *Q;

  Q = ALLOC(satQueue_t, 1);
  if( Q == NULL )
    fprintf(stderr, "Out of space!!!\n" );

  Q->array = ALLOC(long, MaxElements );
  if( Q->array == NULL )
    fprintf(stderr, "Out of space!!!\n" );
  Q->max = MaxElements;
  Q->size = 0;
  Q->front = 1;
  Q->rear = 0;
  return Q;
}

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

  Synopsis    [ Free queue ]

  Description [ Free queue ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FreeQueue( satQueue_t *Q )
{
  if( Q != NULL ) {
    free( Q->array );
    free( Q );
  }
}


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

  Synopsis    [ Enqueue node ]

  Description [ Enqueue node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_Enqueue(satQueue_t *Q, long v)
{
  long *arr, *oarr;
  long rear;

  if(Q->size < Q->max) {
    Q->size++;
    rear = Q->rear;
    rear = (++(rear) == Q->max) ? 0 : rear;
    Q->array[rear] = v;
    Q->rear = rear;
  }
  else {
    arr = ALLOC(long, Q->size * 2 );
    if(arr == NULL )
       fprintf(stderr, "Out of space!!!\n" );
    oarr = Q->array;
    if(Q->front > Q->rear) {
       memcpy(&(arr[1]), &(oarr[Q->front]),
	       sizeof(long) *(Q->max-Q->front));
       memcpy(&(arr[Q->size-Q->front+1]), &(oarr[0]),
	       sizeof(long) *(Q->rear+1));
    }
    else if(Q->front < Q->rear) {
       memcpy(&(arr[1]), &(oarr[Q->front]), sizeof(long) *(Q->size));
    }
    free(oarr);
    Q->array = arr;
    Q->front = 1;
    Q->rear = Q->size;
    Q->max *= 2;

    Q->size++;
    rear = Q->rear;
    rear = (++(rear) == Q->max) ? 0 : rear;
    Q->array[rear] = v;
    Q->rear = rear;
  }
}


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

  Synopsis    [ Dequeue ]

  Description [ Dequeue ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_Dequeue( satQueue_t * Q )
{
  long front;
  long v;

  if(Q->size > 0) {
    Q->size--;
    front = Q->front;
    v = Q->array[front];
    Q->front = (++(front) == Q->max) ? 0 : front;
    return v;
  }
  else
    return(0);
}


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

  Synopsis    [ Allocate decision level ]

  Description [ Allocate decision level ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satLevel_t *
sat_AllocLevel(
	satManager_t *cm)
{
satStatistics_t *stats;
satLevel_t *d;
satArray_t *implied;
int size;

  if(cm->decisionHeadSize == 0) {
    size = cm->currentDecision+2;
    cm->decisionHeadSize = size;
    cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead, size);
    memset(cm->decisionHead, 0, sizeof(satLevel_t) * size);
  }

  if(cm->currentDecision+1 >= cm->decisionHeadSize) {
    size = cm->decisionHeadSize;
    cm->decisionHeadSize <<=1;
    cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead,
			       cm->decisionHeadSize);
    memset(cm->decisionHead+size, 0, sizeof(satLevel_t) * size);
  }

  cm->currentDecision++;
  d = &(cm->decisionHead[cm->currentDecision]);
  implied = d->implied;
  memset(d, 0, sizeof(satLevel_t));
  d->implied = implied;
  if(d->implied == 0){
    d->implied = sat_ArrayAlloc(64);
    //Bing: avoid seg fault
    if(d->implied == 0){
      printf("out of mem, exit\n");
      exit(0);
    }
  }

  d->level = cm->currentDecision;
  d->conflict = 0;

  stats = cm->each;
  if(stats->maxDecisionLevel < d->level)
    stats->maxDecisionLevel = d->level;

  return(d);

}

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

  Synopsis    [ Clean decision level when backtracking ]

  Description [ Clean decision level when backtracking ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CleanLevel(
	satLevel_t *d)
{
  if(d->implied)
    d->implied->num = 0;
  if(d->satisfied)
    d->satisfied->num = 0;
  d->currentVarPos = 0;
}

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

  Synopsis    [ Delete conflict clauses ]

  Description [ Delete conflict clauses ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ClauseDeletion(satManager_t *cm)
{
satLiteralDB_t *literals;
satOption_t *option;
long v, *plit, nv, lit;
int size, n0, n1x, deleteFlag;
int unrelevance;
int inverted, i;
int value;
double ratio;

/**
LATEST_ACTIVITY_DELETION
MAX_UNRELEVANCE_DELETION
SIMPLE_LATEST_DELETION
**/

  option = cm->option;
  if(option->clauseDeletionHeuristic == 0)	return;

  literals = cm->literals;
  for(v=cm->beginConflict; v<cm->nodesArraySize; v+=satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))	continue;
    if(SATreadInUse(v) == 0)		continue;

    if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
      continue;

    size = SATnumLits(v);
    if(size < option->minLitsLimit)	continue;

    plit = (long*)SATfirstLit(v);

    unrelevance = option->unrelevance;
    if(option->clauseDeletionHeuristic & SIMPLE_LATEST_DELETION) {
      ratio = (double)(plit-literals->initialSize)/
	  (double)(literals->last-literals->initialSize);
      if(ratio > 0.8)	unrelevance <<= 3;
    }
    if(!(option->clauseDeletionHeuristic & MAX_UNRELEVANCE_DELETION)) {
      unrelevance = MAXINT;
    }

    n0 = n1x = 0;
    deleteFlag = 0;
    for(i=0; i<size; i++, plit++) {
      lit = *plit;
      nv = SATgetNode(lit);
      inverted = SATisInverted(nv);
      nv = SATnormalNode(nv);
      value = SATvalue(nv) ^ inverted;

      if(value == 0)	n0++;
      else if(value == 1) {
	n1x++;
	if(SATlevel(nv) == 0 && cm->option->coreGeneration == 0)
	  deleteFlag = 1;
      }
      else	n1x++;

      if(deleteFlag) {
	sat_DeleteClause(cm, v);
	sat_Enqueue(cm->unusedAigQueue, v);
	break;
      }
      if((size > option->maxLitsLimit) && (n1x > 1)) {
	sat_DeleteClause(cm, v);
	sat_Enqueue(cm->unusedAigQueue, v);
	break;
      }
      if(n1x > unrelevance) {
	sat_DeleteClause(cm, v);
	sat_Enqueue(cm->unusedAigQueue, v);
	break;
      }
    }

  }
}

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

  Synopsis    [ Delete conflict clauses ]

  Description [ Delete conflict clauses ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_DeleteClause(
	satManager_t *cm,
	long v)
{
satStatistics_t *stats;
int size, i;
long nv, *plit;

  stats = cm->each;
  size = SATnumLits(v);
  stats->nDeletedCl++;
  stats->nDeletedLit += size;

/**  SATresetInUse(v); **/
  SATflags(v) = 0;
  SATflags(v) |= IsCNFMask;

  for(i=0, plit=(long*)SATfirstLit(v); i<size; i++, plit++) {
    nv = SATgetNode(*plit);
    *plit = 0;
  }
}

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

  Synopsis    [ Compact clause database ]

  Description [ Compact clause database ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CompactClauses(satManager_t *cm)
{
satLiteralDB_t *literals;
long *plit, v, lit;
int i, size, index;
int inverted;
satVariable_t *var;

  literals = cm->literals;
  size = literals->last - literals->begin;

  plit = literals->begin;
  index = literals->initialSize-literals->begin;
  for(i=literals->initialSize-literals->begin; i<size; i++) {
    if(i < 2) {
      plit[index] = plit[i];
      index++;
      continue;
    }

    if(plit[i-1] == 0 && plit[i] < 0)	continue;
    else if(plit[i-1] == 0 && plit[i] == 0)	continue;
    else if(plit[i-1] < 0 && plit[i] == 0)	continue;
    else if(plit[i-1] < 0 && plit[i] < 0 && plit[i+1] == 0)	continue;
    else {
      plit[index] = plit[i];
      index++;
    }
  }

  literals->last = literals->begin + index;
  for(v=satNodeSize; v<cm->beginConflict; v+=satNodeSize) {
    if(SATflags(v) & IsCNFMask)	continue;
    var = SATgetVariable(v);
    if(var->wl[0]) var->wl[0]->num = 0;
    if(var->wl[1]) var->wl[1]->num = 0;
  }

  size = literals->last - literals->begin;
  plit = literals->begin;
  for(i=0; i<size; i++) {
    lit = plit[i];
    if(lit > 0 && SATisWL(lit)) {
      v = SATgetNode(lit);
      inverted = !(SATisInverted(v));
      v = SATnormalNode(v);
      var = SATgetVariable(v);
      if(var->wl[inverted] == 0)
	var->wl[inverted] = sat_ArrayAlloc(4);
      sat_ArrayInsert(var->wl[inverted], (long)(&(plit[i])));
    }

    if(lit <= 0) {
      v = -lit;
      /**
      SATfirstLit(v) = (int)(&(plit[i]) - SATnumLits(v));
      **/
      (cm->nodesArray[v+satFirstLit]) = (long)(&(plit[i]) - SATnumLits(v));
    }
  }

  plit = literals->last - 1;
  cm->currentTopConflict = plit;
  cm->currentTopConflictCount = 0;

}

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

  Synopsis    [ Enlarge clause database ]

  Description [ Enlarge clause database ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_EnlargeLiteralDB(satManager_t *cm)
{
satLiteralDB_t *literals;
int nLiveConflictCl, nLiveConflictLit;
double ratio, growRatio;
double memUsage;
long *oldBegin, *oldEnd;
long newSize, oldSize;
int offset, index, size;
int i, j, nodesSize;
long tv;
int arrSize;
satVariable_t *var;
satArray_t *wl;
satStatistics_t *stats;
satOption_t *option;


  literals = cm->literals;
  option = cm->option;
  stats = cm->each;

  size = literals->last - literals->begin;
  nLiveConflictCl = cm->initNumClauses + stats->nConflictCl + stats->nBlockingCl - stats->nDeletedCl;
  nLiveConflictLit = cm->initNumLiterals + stats->nBlockingLit +
		     stats->nConflictLit - stats->nDeletedLit ;
  ratio = (double)(nLiveConflictLit + (nLiveConflictCl << 1)) /
	  (double)(size);

  if(ratio < 0.8) {
    sat_CompactClauses(cm);
    return(1);
  }

  memUsage = (double)sat_MemUsage(cm);
  growRatio = 1.0;
  if(memUsage < (double)option->memoryLimit/4.0)	growRatio = 2.0;
  else if(memUsage < (double)option->memoryLimit/2.0)	growRatio = 1.5;
  else if(memUsage < (double)option->memoryLimit*0.8)	growRatio = 1.2;

  if(growRatio < 1.5) {
    if(ratio < 0.9) {
      sat_CompactClauses(cm);
      return(1);
    }
  }

  oldBegin = literals->begin;
  oldEnd = literals->end;
  oldSize = literals->last - literals->begin;
  newSize = oldSize * (int)growRatio;

  literals->begin = REALLOC(long, oldBegin, newSize);
  literals->last = literals->begin + oldSize;
  literals->end = literals->begin + newSize;

  offset = literals->begin - oldBegin;
  nodesSize = cm->nodesArraySize;
  for(i=satNodeSize; i<nodesSize; i+= satNodeSize) {
    tv = i;
    if(SATflags(tv) & IsCNFMask) {
      if(SATreadInUse(tv))
	(cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
      /**
	SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);
	**/
    }
    else if(SATflags(tv) & IsBDDMask) {
      (cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
	/**
      SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);
      **/
    }
    else {
      var = SATgetVariable(tv);
      wl = var->wl[0];
      if(wl) {
	arrSize = wl->num;
	for(j=0, index=0; j<arrSize; j++) {
	  if(wl->space[j] == 0)	continue;
	  wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
	}
      }
      wl = var->wl[1];
      if(wl) {
	arrSize = wl->num;
	for(j=0, index=0; j<arrSize; j++) {
	  if(wl->space[j] == 0)	continue;
	  wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
	}
      }
    }
  }
  literals->initialSize = literals->initialSize + offset;
  cm->currentTopConflict += offset;

  return(1);
}

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

  Synopsis    [ Allocate clause database ]

  Description [ Allocate clause database ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_AllocLiteralsDB(satManager_t *cm)
{
satLiteralDB_t *literals;
int size;

  literals = cm->literals;
  if(literals)	return;

  literals = ALLOC(satLiteralDB_t, 1);
  cm->literals = literals;

  size = 1024 * 1024;
  literals->begin = ALLOC(long, size);
  *(literals->begin) = 0;
  literals->last = literals->begin + 1;
  literals->end = literals->begin + size;
  /** CONSIDER... **/
  literals->initialSize = literals->last;

}


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

  Synopsis    [ Free clause database ]

  Description [ Free clause database ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FreeLiteralsDB(satLiteralDB_t *literals)
{

  if(literals == 0)	return;
  free(literals->begin);
  literals->begin = 0;
  free(literals);
}

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

  Synopsis    [ clean value and flag of node ]

  Description [ clean value and flag of node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CleanDatabase(satManager_t *cm)
{
long v, i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    SATvalue(v) = 2;
    SATflags(v) &= PreserveMask;
  }
}

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

  Synopsis    [ Compact fanout of AIG node ]

  Description [ Compact fanout of AIG node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CompactFanout(satManager_t *cm)
{
int bufSize, bufIndex;
long *buf, *fan;
long i, v, cur;
int j, size, tsize;

  bufSize = 1024;
  bufIndex = 0;
  buf = ALLOC(long, bufSize);
  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;

    if(!(SATflags(v) & CoiMask))
      continue;

    size = SATnFanout(v);
    if(size >= bufSize) {
      bufSize <<= 1;
      if(size >= bufSize)
	bufSize = size + 1;
      buf = REALLOC(long, buf, bufSize);
    }

    bufIndex = 0;
    for(j=0, fan = SATfanout(v); j<size; j++) {
      cur = fan[j];
      cur >>= 1;
      cur = SATnormalNode(cur);
      if(!(SATflags(cur) & CoiMask))
	continue;
      buf[bufIndex++] = fan[j];
    }

    if(bufIndex > 0) {
      tsize = bufIndex;
      for(j=0, fan=SATfanout(v); j<size; j++) {
	cur = fan[j];
	cur >>= 1;
	cur = SATnormalNode(cur);
	if(!(SATflags(cur) & CoiMask))  {
	  buf[bufIndex++] = fan[j];
	  continue;
	}
      }
      buf[bufIndex] = 0;
      memcpy(fan, buf, sizeof(long)*(size+1));
      SATnFanout(v) = tsize;
    }
    else {
      SATnFanout(v) = 0;
    }
  }

  free(buf);

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if(!(SATflags(v) & CoiMask))
      continue;
    fan = SATfanout(v);
    size = SATnFanout(v);
    qsort(fan, size, sizeof(long), NodeIndexCompare);
  }
}



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

  Synopsis    [ Restore fanout of AIG node ]

  Description [ Restore fanout of AIG node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_RestoreFanout(satManager_t *cm)
{
long i, v;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if((SATflags(v) & IsCNFMask))
      continue;
    SATnFanout(v) = sat_GetFanoutSize(cm, v);
  }
}

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

  Synopsis    [ Get fanout size of AIG node ]

  Description [ Get fanout size of AIG node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_GetFanoutSize(
	satManager_t *cm,
	long v)
{
long *fan;
int i;

  fan = SATfanout(v);
  if(fan == 0)	return(0);

  for(i=0; fan[i]!=0; i++);
  return(i);
}

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

  Synopsis    [ Mark transitive fanin of given array of node ]

  Description [ Mark transitive fanin of given array of node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkTransitiveFaninForArray(
	satManager_t *cm,
	satArray_t *arr,
	unsigned int mask)
{
long v;
int i, size;

  if(arr == 0)	return;
  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    sat_MarkTransitiveFaninForNode(cm, v, mask);
  }
}

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

  Synopsis    [ Mark transitive fanin of given node ]

  Description [ Mark transitive fanin of given node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkTransitiveFaninForNode(
	satManager_t *cm,
	long v,
	unsigned int mask)
{
  if(v == 2)	return;

  v = SATnormalNode(v);

  if(SATflags(v) & mask)	return;

  SATflags(v) |= mask;

  sat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
  sat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
}

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

  Synopsis    [ Unmark transitive fanin of given array of node ]

  Description [ Unmark transitive fanin of given array of node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_UnmarkTransitiveFaninForArray(
	satManager_t *cm,
	satArray_t *arr,
	unsigned int mask,
	unsigned int resetMask)
{
long v;
int i, size;

  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    sat_UnmarkTransitiveFaninForNode(cm, v, mask, resetMask);
  }
}

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

  Synopsis    [ Unmark transitive fanin of given node ]

  Description [ Unmark transitive fanin of given node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_UnmarkTransitiveFaninForNode(
	satManager_t *cm,
	long v,
	unsigned int mask,
	unsigned int resetMask)
{
  if(v == 2)	return;

  v = SATnormalNode(v);

  if(!(SATflags(v) & mask))	return;

  SATflags(v) &= resetMask;
  sat_UnmarkTransitiveFaninForNode(cm, SATleftChild(v), mask, resetMask);
  sat_UnmarkTransitiveFaninForNode(cm, SATrightChild(v), mask, resetMask);
}


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

  Synopsis    [ Set COIMask ]

  Description [ Set COIMask. The COIMask of flags of node has be set to
		apply implication on it ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_SetConeOfInfluence(satManager_t *cm)
{
  sat_MarkTransitiveFaninForArray(cm, cm->assertion, CoiMask);
  sat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
  sat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
  //Bing:
  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
}


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

  Synopsis    [ Allocate manager for SAT solving]

  Description [  Allocate manager for SAT solving]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satManager_t *
sat_InitManager(satInterface_t *interface)
{
satManager_t *cm;

  cm = ALLOC(satManager_t, 1);
  memset(cm, 0, sizeof(satManager_t));

  if(interface) {
    cm->total = interface->total;
    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
    cm->savedConflictClauses = interface->savedConflictClauses;
    cm->trieArray = interface->trieArray;
    cm->objUnitLitArray = sat_ArrayAlloc(8);
  }
  else {
    cm->total = sat_InitStatistics();
    cm->objUnitLitArray = sat_ArrayAlloc(8);
    cm->nonobjUnitLitArray = sat_ArrayAlloc(8);
  }

  return(cm);
}

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

  Synopsis    [ Free manager after SAT solving]

  Description [ Free manager after SAT solving]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FreeManager(satManager_t *cm)
{
satVariable_t *var;
satLevel_t *d;
int i;

  if(cm->option)	sat_FreeOption(cm->option);
  if(cm->total)		sat_FreeStatistics(cm->total);
  if(cm->each)		sat_FreeStatistics(cm->each);

  if(cm->literals)	sat_FreeLiteralsDB(cm->literals);

  if(cm->decisionHead) {
    for(i=0; i<cm->decisionHeadSize; i++) {
      d = &(cm->decisionHead[i]);
      if(d->implied)
	sat_ArrayFree(d->implied);
      if(d->satisfied)
	sat_ArrayFree(d->satisfied);
    }
    free(cm->decisionHead);
    cm->decisionHead = 0;
    cm->decisionHeadSize = 0;
  }

  if(cm->queue)		sat_FreeQueue(cm->queue);
  if(cm->BDDQueue)	sat_FreeQueue(cm->BDDQueue);
  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  if(cm->auxObj)               sat_ArrayFree(cm->auxObj);
  if(cm->obj)                  sat_ArrayFree(cm->obj);
  if(cm->unitLits)             sat_ArrayFree(cm->unitLits);
  if(cm->pureLits)             sat_ArrayFree(cm->pureLits);
  if(cm->assertion)            sat_ArrayFree(cm->assertion);
  if(cm->auxArray)             sat_ArrayFree(cm->auxArray);
  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
  if(cm->clauseIndexInCore)    sat_ArrayFree(cm->clauseIndexInCore);
  cm->auxObj = 0;
  cm->obj = 0;
  cm->unitLits = 0;
  cm->pureLits = 0;
  cm->assertion = 0;
  cm->auxArray = 0;
  cm->nonobjUnitLitArray = 0;
  cm->objUnitLitArray = 0;
  cm->orderedVariableArray = 0;

  if(cm->variableArray) {
    for(i=0; i<=cm->initNumVariables; i++) {
      var = &(cm->variableArray[i]);
      if(var->wl[0]) {
	sat_ArrayFree(var->wl[0]);
	var->wl[0] = 0;
      }
      if(var->wl[1]) {
	sat_ArrayFree(var->wl[1]);
	var->wl[1] = 0;
      }
    }
    free(cm->variableArray);
    cm->variableArray = 0;
  }


  if(cm->comment)	free(cm->comment);

  if(cm->nodesArray)    free(cm->nodesArray);
  free(cm);
}

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

  Synopsis    [ Free option after SAT solving]

  Description [ Free option after SAT solving]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FreeOption(satOption_t * option)
{
  if(option)
    free(option);
}

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

  Synopsis    [ Free statistic after SAT solving]

  Description [ Free statistic after SAT solving]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FreeStatistics(satStatistics_t * stats)
{
  if(stats)
    free(stats);
}


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

  Synopsis    [ Allocate option]

  Description [ Allocate option ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satOption_t *
sat_InitOption()
{
satOption_t *option;

  option = ALLOC(satOption_t, 1);
  memset(option, 0, sizeof(satOption_t));

  option->decisionHeuristic |= LATEST_CONFLICT_DECISION;
/**
  option->decisionHeuristic |= DVH_DECISION;
**/
  option->decisionAgeInterval = 0xff;
  option->decisionAgeRestart = 1;
  option->minConflictForDecision = 50;
  option->maxConflictForDecision = 10000;
  option->skipSatisfiedClauseForDecision = 0;


  /**
  option->clauseDeletionHeuristic |= MAX_UNRELEVANCE_DELETION;
  option->clauseDeletionHeuristic |= SIMPLE_LATEST_DELETION;
  **/
  option->clauseDeletionHeuristic |= LATEST_ACTIVITY_DELETION;
  option->clauseDeletionInterval = 2500;
  option->nextClauseDeletion = option->clauseDeletionInterval*5;
  option->unrelevance = 20;
  option->minLitsLimit = 20;
  option->maxLitsLimit = 1000;

  option->latestUnrelevance = 45;
  option->obsoleteUnrelevance = 20;//6
  option->latestUsage = 100;
  option->obsoleteUsage = 2;
  option->latestRate = 16;

  option->incNumObjLitsLimit = 20; /** 50 **/
  option->incNumNonobjLitsLimit = 50;

  option->incPreserveNonobjective = 1;
  option->minimizeConflictClause = 1;


  option->BDDMonolithic = 0;
  option->BDDDPLL = 0;
  option->maxLimitOfVariablesForMonolithicBDD = 2000;
  option->maxLimitOfClausesForMonolithicBDD = 20000;
  option->maxLimitOfCutSizeForMonolithicBDD = 2000;

  option->maxLimitOfVariablesForBDDDPLL = 200;
  option->maxLimitOfClausesForBDDDPLL = 2000;
  option->maxLimitOfCutSizeForBDDDPLL = 500;

  option->maxLimitOfVariablesForBDD = 50;

  option->memoryLimit = 1024 * 1024 * 1024;

  return(option);
}

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

  Synopsis    [ Report statistics]

  Description [ Report statistics]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ReportStatistics(
	satManager_t *cm,
	satStatistics_t *stats)
{
satOption_t *option;

  option = cm->option;
  fprintf(cm->stdOut, "%s Number of decisions %d\n",
	      cm->comment, stats->nDecisions);
  if(option->decisionHeuristic & DVH_DECISION) {
    fprintf(cm->stdOut, "%s Number of DVH decisions %d\n",
	      cm->comment, stats->nDVHDecisions);
  }
  if(option->decisionHeuristic & LATEST_CONFLICT_DECISION) {
    fprintf(cm->stdOut, "%s Number of latest conflict decisions %d\n",
	      cm->comment, stats->nLatestConflictDecisions);
  }
  fprintf(cm->stdOut, "%s Number of backtracks %d\n",
	      cm->comment, stats->nBacktracks);

  fprintf(cm->stdOut, "%s Number of CNF implications %d\n",
	      cm->comment, stats->nCNFImplications);
  fprintf(cm->stdOut, "%s Number of Aig implications %d\n",
	      cm->comment, stats->nAigImplications);
  fprintf(cm->stdOut, "%s Number of BDD implications %d\n",
	      cm->comment, stats->nBDDImplications);

  fprintf(cm->stdOut, "%s Number of unit conflict clauses %d\n",
	      cm->comment, stats->nUnitConflictCl);
  fprintf(cm->stdOut, "%s Number of conflict clauses %d\n",
	      cm->comment, stats->nConflictCl);
  fprintf(cm->stdOut, "%s Number of conflict literals %d\n",
	      cm->comment, stats->nConflictLit);
  fprintf(cm->stdOut, "%s Number of deleted clauses %d\n",
	      cm->comment, stats->nDeletedCl);
  fprintf(cm->stdOut, "%s Number of deleted literals %d\n",
	      cm->comment, stats->nDeletedLit);

  if(option->incTraceObjective + option->incDistill) {
    fprintf(cm->stdOut, "%s Number of init object conflict clauses %d\n",
	      cm->comment, stats->nInitObjConflictCl);
    fprintf(cm->stdOut, "%s Number of init object conflict literals %d\n",
	      cm->comment, stats->nInitObjConflictLit);
    fprintf(cm->stdOut, "%s Number of init non-object conflict clauses %d\n",
	      cm->comment, stats->nInitNonobjConflictCl);
    fprintf(cm->stdOut, "%s Number of init non-object conflict literals %d\n",
	      cm->comment, stats->nInitNonobjConflictLit);
    fprintf(cm->stdOut, "%s Number of object conflict clauses %d\n",
	      cm->comment, stats->nObjConflictCl);
    fprintf(cm->stdOut, "%s Number of object conflict literals %d\n",
	      cm->comment, stats->nObjConflictLit);
    fprintf(cm->stdOut, "%s Number of non-object conflict clauses %d\n",
	      cm->comment, stats->nNonobjConflictCl);
    fprintf(cm->stdOut, "%s Number of non-object conflict literals %d\n",
	      cm->comment, stats->nNonobjConflictLit);
  }
  if(option->incDistill) {
    fprintf(cm->stdOut, "%s Number of distill object conflict clauses %d\n",
	      cm->comment, stats->nDistillObjConflictCl);
    fprintf(cm->stdOut, "%s Number of distill object conflict literals %d\n",
	      cm->comment, stats->nDistillObjConflictLit);
    fprintf(cm->stdOut, "%s Number of distill non-object conflict clauses %d\n",
	      cm->comment, stats->nDistillNonobjConflictCl);
    fprintf(cm->stdOut, "%s Number of distill non-object conflict literals %d\n",
	      cm->comment, stats->nDistillNonobjConflictLit);
  }
  if(option->allSatMode) {
    fprintf(cm->stdOut, "%s Number of blocking clauses %d\n",
	      cm->comment, stats->nBlockingCl);
    fprintf(cm->stdOut, "%s Number of blocking literals %d\n",
	      cm->comment, stats->nBlockingLit);
  }

  fprintf(cm->stdOut, "%s Maximum decision level %d\n",
	      cm->comment, stats->maxDecisionLevel);
  fprintf(cm->stdOut, "%s Number of low score decisions %d\n",
	      cm->comment, stats->nLowScoreDecisions);
  fprintf(cm->stdOut, "%s Total nonchronological backtracks %d\n",
	      cm->comment, stats->nNonchonologicalBacktracks);
  fprintf(cm->stdOut, "%s Total run time %10g\n", cm->comment, stats->satTime);
  fflush(cm->stdOut);

}

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

  Synopsis    [ Allocate statistics]

  Description [ Allocate statistics]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satStatistics_t *
sat_InitStatistics(void)
{
satStatistics_t *stats;

  stats = ALLOC(satStatistics_t, 1);
  memset(stats, 0, sizeof(satStatistics_t));

  return(stats);
}


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

  Synopsis    [ Set incremental option ]

  Description [ Set incremental option ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_SetIncrementalOption(satOption_t *option, int incFlag)
{
  if(incFlag == 0) return;

  if(incFlag == 1)  { /* TraceObjective */
    option->incTraceObjective = 1;
  }
  else if(incFlag == 2)  { /* Distill */
    option->incDistill = 1;
  }
  else if(incFlag == 3)  { /* TraceObjective & Distill */
    option->incTraceObjective = 1;
    option->incDistill = 1;
  }

}

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

  Synopsis    [ Restore blocking clauses]

  Description [ Restore blocking clauses]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_RestoreBlockingClauses(satManager_t *cm)
{
long *space, *start;
long c, v;
int i;
satArray_t *reached;
satArray_t *clause;
satArray_t *unitLits;

  reached = cm->reached;
  if(reached == 0)
    return;

  unitLits = cm->unitLits;
  if(unitLits == 0)
    unitLits = cm->unitLits = sat_ArrayAlloc(16);

  clause = sat_ArrayAlloc(50);

  for(i=0, space=reached->space; i<reached->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=reached->num)
	break;
      start = space;
      clause->num = 0;
      while(*space > 0) {
	v = (*space);
	sat_ArrayInsert(clause, SATnot(v));
	i++;
	space++;
      }

      c = sat_AddBlockingClause(cm, clause);

      /**
	fprintf(stdout, "NOTICE : forwarded blocking clause\n");
	sat_PrintNode(cm, c);
	**/

      if(clause->num == 1)
	sat_ArrayInsert(unitLits, (v));
      i--;
      space--;
    }
  }
  sat_ArrayFree(clause);
}

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

  Synopsis    [ Restore Frontier clauses]

  Description [ Restore Frontier clauses]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_RestoreFrontierClauses(satManager_t *cm)
{
long *space, *start;
long c, v;
int i;
satArray_t *frontier;
satArray_t *clause;
satArray_t *unitLits;

  frontier = cm->frontier;
  cm->frontierNodesEnd = cm->nodesArraySize;
  if(frontier == 0)
    return;

  unitLits = cm->unitLits;
  if(unitLits == 0)
    unitLits = cm->unitLits = sat_ArrayAlloc(16);

  clause = sat_ArrayAlloc(50);

  for(i=0, space=frontier->space; i<frontier->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=frontier->num)
	break;
      start = space;
      clause->num = 0;
      while(*space > 0) {
	v = (*space);
	sat_ArrayInsert(clause, SATnot(v));
	i++;
	space++;
      }

      c = sat_AddClause(cm, clause);

      /**
      sat_PrintNode(cm, c);
      **/

      cm->initNumClauses++;
      cm->initNumLiterals += clause->num;
      if(clause->num == 1)
	sat_ArrayInsert(unitLits, (v));

      i--;
      space--;
    }
  }
  sat_ArrayFree(clause);
  cm->frontierNodesEnd = cm->nodesArraySize;
}

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

  Synopsis    [ Restore clauses]

  Description [ Restore clauses]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_RestoreClauses(satManager_t *cm, satArray_t *cnfArray)
{
long *space, *start;
long c, v;
int i;
satArray_t *clause;
satArray_t *unitLits;


  unitLits = cm->unitLits;
  if(unitLits == 0)
    unitLits = cm->unitLits = sat_ArrayAlloc(16);

  clause = sat_ArrayAlloc(50);

  for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=cnfArray->num)
	break;
      start = space;
      clause->num = 0;
      while(*space > 0) {
	v = (*space);
	sat_ArrayInsert(clause, SATnot(v));
	i++;
	space++;
      }

      if(clause->num == 1) {
	sat_ArrayInsert(unitLits, (v));
      }
      else {
	c = sat_AddClause(cm, clause);
      }

      cm->initNumClauses++;
      cm->initNumLiterals += clause->num;

      i--;
      space--;
    }
  }
  sat_ArrayFree(clause);
}

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

  Synopsis    [ Collect blocking clauses]

  Description [ Collect blocking clauses]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CollectBlockingClause(satManager_t *cm)
{
satArray_t *reached, *frontier;
long i, v, tv, *plit;
int j, size;
int inverted, num;
int nReachs, nFrontiers;

  if(cm->reached == 0)	cm->reached = sat_ArrayAlloc(1024);
  if(cm->frontier == 0) cm->frontier = sat_ArrayAlloc(1024);

  frontier = cm->frontier;
  reached = cm->reached;

  frontier->num = 0;
  reached->num = 0;
  sat_ArrayInsert(frontier, 0);
  sat_ArrayInsert(reached, 0);
  nReachs = nFrontiers = 0;

  for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & IsBlockingMask))
      continue;

    if(SATreadInUse(i) == 0)		continue;

    if((SATflags(i) & IsFrontierMask)) {

      /**
      fprintf(stdout, "Frontier processed\n");
      sat_PrintNode(cm, i);
      **/
      plit = (long*)SATfirstLit(i);
      size = SATnumLits(i);
      num = frontier->num;
      for(j=0; j<size; j++, plit++) {
	v = SATgetNode(*plit);
	inverted = SATisInverted(v);
	tv = SATnormalNode(v);
	sat_ArrayInsert(frontier, v);
      }
      nFrontiers++;
      sat_ArrayInsert(frontier, 0);
    }

    plit = (long*)SATfirstLit(i);
    size = SATnumLits(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      sat_ArrayInsert(reached, v);
    }
    sat_ArrayInsert(reached, 0);
    nReachs ++;
  }



  cm->frontier = frontier;
  cm->reached = reached;
  fprintf(stdout, "NOTICE : %d frontier are collected\n", nFrontiers);
  fprintf(stdout, "NOTICE : %d blocking clauses are collected\n", nReachs);
}


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

  Synopsis    [ Free interface]

  Description [ Free interface]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FreeInterface(satInterface_t *interface)
{
  if(interface == 0)	return;

  if(interface->total)
    free(interface->total);
  if(interface->nonobjUnitLitArray)
    sat_ArrayFree(interface->nonobjUnitLitArray);
  if(interface->objUnitLitArray)
    sat_ArrayFree(interface->objUnitLitArray);
  if(interface->savedConflictClauses)
    free(interface->savedConflictClauses);
  free(interface);
}

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

  Synopsis    [ Create AIG node ]

  Description [ Create AIG node,
		This function is identical with bAig_CreateNode,
		We have this function here to isolate this package from baig]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_CreateNode(
	satManager_t *cm,
	long left,
	long right)
{
long newNode;

  newNode = cm->nodesArraySize;
  //Bing: to deal with the case that cm->maxNodesArraySize is not multiple of
  // satNodeSize
  cm->nodesArraySize += satNodeSize;

  if(cm->nodesArraySize >= cm->maxNodesArraySize) {
    cm->maxNodesArraySize = 2* cm->maxNodesArraySize;
    cm->nodesArray = REALLOC(long, cm->nodesArray, cm->maxNodesArraySize);
  }
  cm->nodesArray[newNode + satRight] = right;
  cm->nodesArray[newNode + satLeft] = left;

  //cm->nodesArraySize += satNodeSize;

  SATflags(newNode) = 0;
  SATnext(newNode) = 2;
  SATnFanout(newNode) = 0;
  /**
  SATfanout(newNode) = 0;
  **/
  (cm->nodesArray[newNode+satFanout]) = 0;
  //Bing:
  SATvalue(newNode) = 2;

  return(newNode);
}

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

  Synopsis    [ Usage of memory ]

  Description [ Usage of memory ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_MemUsage(satManager_t *cm)
{
satLiteralDB_t *literals;
satStatistics_t *stats;
int aigSize, cnfSize, watchedSize;

  literals = cm->literals;
  stats = cm->each;
  aigSize = sizeof(int) * cm->maxNodesArraySize;
  cnfSize = sizeof(int) * (literals->end - literals->begin);
  watchedSize = sizeof(int) * 2 *
		 (stats->nConflictCl - stats->nDeletedCl);
  return(aigSize + cnfSize + watchedSize);
}



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

  Synopsis    [ Get canonical node ]

  Description [ Get canonical node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_GetCanonical(satManager_t *cm, long v)
{
long nv;
int inverted;

  if(v == 2)	return(2);

  while(!(SATflags(SATnormalNode(v))) & CanonicalBitMask) {
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    nv = SATcanonical(v);
    if(inverted)
      nv = SATnot(nv);
    v = nv;
  }
  return(v);
}


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

  Synopsis    [ Combine statistics of several runs]

  Description [ Combine statistics of several runs]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CombineStatistics(satManager_t *cm)
{
    /* CONSIDER ... */
}

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

  Synopsis    [ Get the number of initial clauses ]

  Description [ Get the number of initial clauses.
		This function works properly only CNF sat case]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_GetNumberOfInitialClauses(satManager_t *cm)
{
  return(cm->initNumClauses);
}

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

  Synopsis    [ Get the number of initial variables ]

  Description [ Get the number of initial variables.
		This function works properly only CNF sat case]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_GetNumberOfInitialVariables(satManager_t *cm)
{
  return(cm->initNumVariables);
}

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

  Synopsis    [ Read forced assignments.]

  Description [ Read forced assignments.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satArray_t *
sat_ReadForcedAssignment(
	char *filename)
{
FILE *fin;
char line[102400], word[1024];
char *lp;
satArray_t *arr;
long v;

  if(!(fin = fopen(filename, "r"))) {
    fprintf(stdout, "ERROR : Can't open file %s\n", filename);
    return(0);
  }

  arr = sat_ArrayAlloc(64);
  while(fgets(line, 102400, fin)) {
    lp = sat_RemoveSpace(line);
    if(lp[0] == '\n')	continue;
    while(1) {
      lp = sat_RemoveSpace(lp);
      lp = sat_CopyWord(lp, word);
      if(strlen(word)) {
	v = atoi(word);
	v *= satNodeSize;
	if(v < 0)	v = SATnot(-v);
	sat_ArrayInsert(arr, v);
      }
      else {
	break;
      }
    }
  }
  fclose(fin);

  return(arr);
}

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

  Synopsis    [ Apply forced assignments.]

  Description [ Apply forced assignments.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_ApplyForcedAssigment(
	satManager_t *cm,
	satArray_t *arr,
	satLevel_t *d)
{
long v;
int i, inverted, errorFlag;

  errorFlag = 0;
  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    SATvalue(v) = !inverted;
    SATmakeImplied(v, d);
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;
    sat_ImplicationMain(cm, d);
    if(d->conflict) {
      fprintf(cm->stdOut,
	      "%s WARNING : conflict happens at level %d while applying forced assignments\n", cm->comment, d->level);
      errorFlag = 1;
      break;
    }
  }
  if(errorFlag)
    return(SAT_UNSAT);
  else
    return(0);
}

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

  Synopsis    [ Apply forced assignments.]

  Description [ Apply forced assignments.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ApplyForcedAssignmentMain(
	satManager_t *cm,
	satLevel_t *d)
{
satArray_t *forcedArr;
int flag;

  forcedArr = cm->option->forcedAssignArr;
  flag = 0;
  if(forcedArr) {
    flag = sat_ApplyForcedAssigment(cm, forcedArr, d);
  }

  if(flag == SAT_UNSAT) {
    cm->status = SAT_UNSAT;
    return;
  }
}

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

  Synopsis    [ Put assignments.]

  Description [ Put assignments.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PutAssignmentValueMain(
	satManager_t *cm,
	satLevel_t *d,
	satArray_t *arr)
{
long v;
int i;
int inverted;

  if(arr == 0)	return;

  if(cm->variableArray == 0) {
    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
    memset(cm->variableArray, 0,
	    sizeof(satVariable_t) * (cm->initNumVariables+1));
  }

  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    SATvalue(v) = !inverted;
  }
}

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

  Synopsis    [ Clause deletion heuristic based on usage of conflict clause ]

  Description [ Clause deletion heuristic based on usage of conflict clause ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ClauseDeletionLatestActivity(satManager_t *cm)
{
satLiteralDB_t *literals;
satOption_t *option;
long nv, v, *plit, *clit;
long usage, totalConflictCl;
long index, lit;

int size, n0, n1x, deleteFlag;
int unrelevance;
int usedLimit;
int inverted, i;
int value;
int nLatestCl;
int nDeletedCl;
double ratio;

/**
 LATEST_ACTIVITY_DELETION
 MAX_UNRELEVANCE_DELETION
 SIMPLE_LATEST_DELETION
**/

  option = cm->option;
  if(option->clauseDeletionHeuristic == 0)	return;

  totalConflictCl = (cm->nodesArraySize - cm->beginConflict)/satNodeSize;
  nDeletedCl = cm->each->nDeletedCl;
  nLatestCl = totalConflictCl/option->latestRate;
  literals = cm->literals;
  index = 0;
  for(clit = literals->last-1; clit > literals->begin; clit--){
    if(*clit == 0)
      continue;
    if(index >= totalConflictCl)
      break;
    v = -(*clit);

    plit = (long*)SATfirstLit(v);
    clit = plit - 1;
    index++;

    if(nLatestCl > 0) {
      nLatestCl--;
      unrelevance = option->latestUnrelevance;
    }
    else {
      unrelevance = option->obsoleteUnrelevance;
    }

    if(!(SATflags(v) & IsConflictMask)) continue;
    if((SATflags(v) & IsFrontierMask))	continue;

    if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
      continue;

    usage = SATconflictUsage(v);
    SATconflictUsage(v) = usage/2;
    size = SATnumLits(v);
//    if(size < option->minLitsLimit)	continue;
    if(size < unrelevance)
      continue;

    usedLimit = option->obsoleteUsage +
	(option->latestUsage-option->obsoleteUsage)*index/totalConflictCl;
    if(usage > usedLimit)
      continue;


    n0 = n1x = 0;
    deleteFlag = 0;
    for(i=0; i<size; i++, plit++) {
      lit = *plit;
      nv = SATgetNode(lit);
      inverted = SATisInverted(nv);
      nv = SATnormalNode(nv);
      value = SATvalue(nv) ^ inverted;

      if(value == 0)	n0++;
      else if(value == 1) {
	n1x++;
	if(SATlevel(nv) == 0)	deleteFlag = 1;
      }
      else	n1x++;

      if(deleteFlag) {
	sat_DeleteClause(cm, v);
	sat_Enqueue(cm->unusedAigQueue, v);
	break;
      }
      if((size > option->maxLitsLimit) && (n1x > 1)) {
	sat_DeleteClause(cm, v);
	sat_Enqueue(cm->unusedAigQueue, v);
	break;
      }
      if(n1x > unrelevance) {
	sat_DeleteClause(cm, v);
	sat_Enqueue(cm->unusedAigQueue, v);
	break;
      }
    }

  }

  cm->each->nDeletedButUncompacted += cm->each->nDeletedCl - nDeletedCl;
  ratio = (double)cm->each->nDeletedButUncompacted/
	  (double)(cm->each->nConflictCl-cm->each->nDeletedCl);

  if(ratio> 0.2) {
    sat_CompactClauses(cm);
    cm->each->nDeletedButUncompacted = 0;
  }

}


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

  Synopsis    [ Find a clause index from literal pointer.]

  Description [ Find a clause index from literal pointer.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_GetClauseFromLit(
	satManager_t *cm,
	long *lit)
{
  while(*lit > 0) {
    lit++;
  }
  return(-(*lit));
}
/**Function********************************************************************

  Synopsis    [ Compare node index to sort ]

  Description [ Compare node index to sort ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
NodeIndexCompare(const void *x, const void *y)
{
long n1, n2;

  n1 = *(long *)x;
  n2 = *(long *)y;
  return(n1 > n2);
}