src/sat/satUtil.c

Go to the documentation of this file.

#include "satInt.h"

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

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

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

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

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


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++;

  (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);
}

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++;

  (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);
}
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++;

  (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);
}
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++;

  (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);
}


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++;

  (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);
}

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++;


  (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);
}

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++;

  (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);
}

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++;

  (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);
}


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);
}


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;
}

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;
}

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;
  }
}

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


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;
}

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


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;
  }
}


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);
}


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);

}

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

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;

  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;
      }
    }

  }
}

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;

  SATflags(v) = 0;
  SATflags(v) |= IsCNFMask;

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

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;
      (cm->nodesArray[v+satFirstLit]) = (long)(&(plit[i]) - SATnumLits(v));
    }
  }

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

}

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);
    }
    else if(SATflags(tv) & IsBDDMask) {
      (cm->nodesArray[tv+satFirstLit]) = (long)((long*)(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);
}

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;
  literals->initialSize = literals->last;

}


void
sat_FreeLiteralsDB(satLiteralDB_t *literals)
{

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

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;
  }
}

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);
  }
}



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);
  }
}

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);
}

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);
  }
}

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);
}

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);
  }
}

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);
}


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);
}


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);
}

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);
}

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

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


satOption_t *
sat_InitOption()
{
satOption_t *option;

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

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


  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; 
  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);
}

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);

}

satStatistics_t *
sat_InitStatistics(void)
{
satStatistics_t *stats;

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

  return(stats);
}


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;
  }

}

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);

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

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);

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

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

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);
}

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)) {

      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);
}


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);
}

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;
  (cm->nodesArray[newNode+satFanout]) = 0;
  //Bing:
  SATvalue(newNode) = 2;

  return(newNode);
}

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);
}



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);
}


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

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

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

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);
}

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);
}

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;
  }
}

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;
  }
}

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;

  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;
  }

}


long
sat_GetClauseFromLit(
        satManager_t *cm,
        long *lit)
{
  while(*lit > 0) {
    lit++;
  }
  return(-(*lit));
}
static int
NodeIndexCompare(const void *x, const void *y)
{
long n1, n2;

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