src/puresat/puresatIPUtil.c

Go to the documentation of this file.

#include "puresatInt.h"

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

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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


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


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

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

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

static int
StringCheckIsInteger(
  char *string,
  int *value)
{
  char *ptr;
  long l;

  l = strtol (string, &ptr, 0) ;
  if(*ptr != '\0')
    return 0;
  if ((l > MAXINT) || (l < -1 - MAXINT))
    return 1 ;
  *value = (int) l;
  return 2 ;
}


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
RTnode_t RTCreateNode(RTManager_t * rm)
{
  RTnode_t node;

  if(rm->nArray==0){
    rm->nArray = ALLOC(long, RTnodeSize*RT_BLOCK);
    rm->maxSize = RTnodeSize*RT_BLOCK;
    rm->aSize = 0;
  }

  if(rm->maxSize<=rm->aSize+RTnodeSize){
    rm->nArray = REALLOC(long, rm->nArray,rm->maxSize+RTnodeSize*RT_BLOCK);
    if(rm->nArray == 0){
      fprintf(vis_stdout,"memout when alloc %ld bytes\n",
             (rm->maxSize+RTnodeSize*RT_BLOCK)*4);
      exit(0);
    }
    rm->maxSize = rm->maxSize+RTnodeSize*1000;
  }
  rm->aSize += RTnodeSize;
  node = rm->aSize;

  RT_fSize(node) = 0;
  RT_formula(node) = 0;
  RT_oriClsIdx(node) = 0;
  RT_pivot(node) = 0;
  RT_flag(node) = 0;
  RT_IPnode(node) = -1;
  RT_left(node) = 0;
  RT_right(node) = 0;

  if(rm->fArray==0){
    rm->fArray = ALLOC(long,FORMULA_BLOCK);

    rm->cpos = 0;
    rm->maxpos = FORMULA_BLOCK;
  }

  return node;
}

IP_Manager_t * IPManagerAlloc()
{
  IP_Manager_t * ipm = ALLOC(IP_Manager_t, 1);
  memset(ipm,0,sizeof(IP_Manager_t));
  return ipm;
}


void IPManagerFree(IP_Manager_t *ipm)
{
  FREE(ipm);
}

int PureSat_IdentifyConflict(
  satManager_t *cm,
  long left,
  bAigEdge_t right,
  bAigEdge_t node)
{
  int result; /*1:left 2:right 3:both*/
  int value = SATgetValue(left,right,node);
  switch(value){
  case 1:
  case 5:
  case 9:
  case 13:
    result = 1;
    break;
  case 17:
  case 33:
  case 49:
    result = 2;
    break;
  case 20:
    result = 3;
    break;
  default:
    fprintf(vis_stdout,"can't identify the conflict, exit\n");
    exit(0);
  }

  return result;
}

void
PureSatBmcGetCoiForNtkNode_New(
  Ntk_Node_t  *node,
  st_table    *CoiTable,
  st_table    *visited)
{
  int        i;
  Ntk_Node_t *faninNode;

  if(node == NIL(Ntk_Node_t)){
    return;
  }


  if (st_lookup_int(visited, (char *) node, NIL(int))){
    return;
  }
  st_insert(visited, (char *) node, (char *) 0);

  if(Ntk_NodeTestIsInput(node))
    return;

  if (Ntk_NodeTestIsLatch(node)){
    st_insert(CoiTable, (char *) node, (char *)0);
  }

  Ntk_NodeForEachFanin(node, i, faninNode) {
    PureSatBmcGetCoiForNtkNode_New(faninNode, CoiTable, visited);
  }

  return;
}

void
PureSatBmcGetCoiForLtlFormulaRecursive_New(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *formula,
  st_table        *ltlCoiTable,
  st_table        *visited)
{
  if (formula == NIL(Ctlsp_Formula_t)) {
    return;
  }
  /* leaf node */
  if (formula->type == Ctlsp_ID_c){
    char       *name = Ctlsp_FormulaReadVariableName(formula);
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
    int        tmp;

    if (st_lookup_int(visited, (char *) node, &tmp)){
      /* Node already visited */
      return;
    }
    PureSatBmcGetCoiForNtkNode_New(node, ltlCoiTable, visited);
    return;
  }
  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->left,  ltlCoiTable, visited);
  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->right, ltlCoiTable, visited);

  return;
}

void
PureSatBmcGetCoiForLtlFormula_New(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *formula,
  st_table        *ltlCoiTable)
{
  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);

  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula, ltlCoiTable, visited);
  st_free_table(visited);
  return;
} /* BmcGetCoiForLtlFormula() */


void PureSat_MarkTransitiveFaninForNode(
        satManager_t *cm,
        bAigEdge_t v,
        unsigned int mask)
{
  if(v == bAig_NULL)    return;

  v = SATnormalNode(v);

  if(SATflags(v) & mask)        return;

  SATflags(v) |= mask;
  if(SATflags(v) & Visited3Mask) return;

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

void PureSat_MarkTransitiveFaninForArray(
        satManager_t *cm,
        satArray_t *arr,
        unsigned int mask)
{
  int  i, size;
  bAigEdge_t v;

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

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

void PureSat_MarkTransitiveFaninForNode2(
        mAig_Manager_t *manager,
        bAigEdge_t v,
        unsigned int mask)
{
  if(v == bAig_NULL)    return;

  v = SATnormalNode(v);

  if(flags(v) & mask)   return;

  flags(v) |= mask;
  if(flags(v) & Visited3Mask) return;

  PureSat_MarkTransitiveFaninForNode2(manager, leftChild(v), mask);
  PureSat_MarkTransitiveFaninForNode2(manager, rightChild(v), mask);
}

void PureSat_MarkTransitiveFaninForArray2(
        mAig_Manager_t *manager,
        satArray_t *arr,
        unsigned int mask)
{
bAigEdge_t v;
int i, size;

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

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

void PureSat_MarkTransitiveFaninForNode3(
        mAig_Manager_t *manager,
        bAigEdge_t v,
        unsigned int mask)
{
  if(v == 2)    return;

  v = SATnormalNode(v);

  if(flags(v) & mask)   return;

  flags(v) |= mask;

  PureSat_MarkTransitiveFaninForNode3(manager, leftChild(v), mask);
  PureSat_MarkTransitiveFaninForNode3(manager, rightChild(v), mask);
}

void PureSat_MarkTransitiveFaninForArray3(
        mAig_Manager_t *manager,
        satArray_t *arr,
        unsigned int mask)
{
bAigEdge_t v;
int i, size;

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

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


void PureSat_MarkTransitiveFaninForNode4(
        mAig_Manager_t *manager,
        bAigEdge_t v,
        unsigned int mask,
        int bound)
{
  if(v == bAig_NULL)    return;

  v = SATnormalNode(v);

  if(flags(v) & mask)   return;

  flags(v) |= mask;

  if((flags(v)&StateBitMask)&&
     !(flags(v)&VisibleVarMask)&&
     (bAig_Class(v)>0)){

    return;
  }

  PureSat_MarkTransitiveFaninForNode4(manager, leftChild(v), mask,bound);
  PureSat_MarkTransitiveFaninForNode4(manager, rightChild(v), mask,bound);
}

void PureSat_MarkTransitiveFaninForArray4(
        mAig_Manager_t *manager,
        satArray_t *arr,
        unsigned int mask,
        int bound)
{
bAigEdge_t v;
int i, size;

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

  for(i=0; i<size; i++) {
    v = arr->space[i];

    v = SATnormalNode(v);
    PureSat_MarkTransitiveFaninForNode4(manager,v,mask,bound);

  }
}

void PureSat_CleanMask(mAig_Manager_t *manager,
                       unsigned int mask)
{
  bAigEdge_t i;

  for(i=bAigNodeSize; i<manager->nodesArraySize;i+=bAigNodeSize)
    flags(i)&=mask;

}

void PureSat_SetCOI(satManager_t *cm)
{

  PureSat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
  PureSat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
  PureSat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);

}


void PureSat_ResetCoi(satManager_t *cm)
{
  bAigEdge_t i;
  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    if(SATflags(i) & CoiMask)
      SATflags(i) &= ResetCoiMask;
  }
}

void PureSatSetLatchCOI(Ntk_Network_t * network,
                        PureSat_Manager_t *pm,
                        satManager_t * cm,
                        /*deletable*/
                        st_table * AbsTable,
                        int from,
                        int to)
{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);

  bAigTimeFrame_t *tf = manager->timeframeWOI;
  int i,j;
  bAigEdge_t *L0,*L1,*bL0,*bL1;
  satArray_t * assert;
  int nLatches = tf->nLatches, nbLatches = tf->nbLatches;

  if(from>=to) return;

  PureSat_ResetCoi(cm);

  assert = sat_ArrayAlloc(1);
  sat_ArrayInsert(assert,manager->InitState);
  PureSat_MarkTransitiveFaninForArray3(manager,assert,CoiMask);
  sat_ArrayFree(assert);

  for(i=from; i<to; i++){
    assert = sat_ArrayAlloc(1);

    L0 = tf->latchInputs[i];
    L1 = tf->latchInputs[i+1];
    bL0 = tf->blatchInputs[i];
    bL1 = tf->blatchInputs[i+1];

    for(j=0;j<nLatches;j++){
      if(L1[j]!=bAig_One&&L1[j]!=bAig_Zero){
        if(flags(L1[j])&VisibleVarMask)
          sat_ArrayInsert(assert,L1[j]);
      }
      if(L0[j]!=bAig_One&&L0[j]!=bAig_Zero&&
         !(flags(L0[j])&VisibleVarMask))
        flags(L0[j]) |= Visited3Mask;
    }

    for(j=0;j<nbLatches;j++){
      if(bL1[j]!=bAig_One&&bL1[j]!=bAig_Zero){
        if(flags(bL1[j])&VisibleVarMask)
          sat_ArrayInsert(assert,bL1[j]);
      }
      if(bL0[j]!=bAig_One&&bL0[j]!=bAig_Zero&&
         !(flags(bL0[j])&VisibleVarMask))
        flags(bL0[j]) |= Visited3Mask;
    }

    PureSat_MarkTransitiveFaninForArray2(manager,assert,CoiMask);
    sat_ArrayFree(assert);
  }

}

void PureSatSetLatchCOI2(Ntk_Network_t * network,
                         PureSat_Manager_t *pm,
                         satManager_t * cm,
                         bAigEdge_t obj,
                         int bound)
{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  satArray_t * assert;

  PureSat_ResetCoi(cm);

  assert = sat_ArrayAlloc(1);
  sat_ArrayInsert(assert,obj);
  PureSat_MarkTransitiveFaninForArray4(manager,assert,CoiMask,bound);
  PureSat_MarkTransitiveFaninForArray4(manager,cm->assertArray,CoiMask,bound);
  sat_ArrayFree(assert);

}

void PureSatSetCOI(Ntk_Network_t * network,
                   PureSat_Manager_t *pm,
                   satManager_t * cm,
                   st_table * AbsTable,
                   int from,
                   int to,
                   int bound)
{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  bAigEdge_t property;

  if(cm->obj->num>0){
    property = cm->obj->space[0];
    PureSatSetLatchCOI2(network,pm,cm,property,bound);
  }
  else{
    PureSatSetLatchCOI(network,pm,cm,AbsTable,from,to);
    PureSat_CleanMask(manager,ResetVisited3Mask);
  }


}

void PureSatAbstractLatch(bAig_Manager_t *manager,
                          bAigEdge_t v,
                          st_table * tmpTable)
{
  bAigEdge_t nv;

  /*fanin: set left and right to bAig_NULL*/
  nv = bAig_NonInvertedEdge(v);

  if(leftChild(nv)!=bAig_NULL){
    if(!(flags(leftChild(nv))&CoiMask))
      flags(leftChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigLeft]=bAig_NULL;
  }

  if(rightChild(nv)!=bAig_NULL){
    if(!(flags(rightChild(nv))&CoiMask))
      flags(rightChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigRight]=bAig_NULL;
  }

}

void PureSatKillPseudoGVNode(bAig_Manager_t *manager,
                             bAigEdge_t v,
                             st_table * tmpTable)
{
  long size = nFanout(v),i,inv=0;
  bAigEdge_t v1,v2,nv;
  bAigEdge_t  * fan = (bAigEdge_t *)fanout(v),left;

  /*fanin: set left and right to bAig_NULL*/
  nv = bAig_NonInvertedEdge(v);
  flags(nv) |= PGVMask;

  if(leftChild(nv)!=bAig_NULL){
    if(!(flags(leftChild(nv))&CoiMask))
      flags(leftChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigLeft]=bAig_NULL;
  }

  if(rightChild(nv)!=bAig_NULL){
    if(!(flags(rightChild(nv))&CoiMask))
      flags(rightChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigRight]=bAig_NULL;
  }


  manager->class_ = 2;

  /*fanout: connection to vars in next tf is disconnected, and a new pseudo var
    is created, and used as a replacement*/
  for(i=0;i<size;i++){
    v1 = bAig_NonInvertedEdge(fan[i]>>1);
    if(!(flags(v1)&CoiMask))
      continue;
    if(bAig_Class(v1)>1){
      /*igonre invSV since its left and right will be processed to 2*/
      if(!(flags(v1)&VisibleVarMask)&&(flags(v1)&StateBitMask))
        continue;
      /*if nonSV, create new Node as replacement*/
      if(!st_lookup(tmpTable,(char*)nv,&v2)){
        v2 = bAig_CreateNode(manager,bAig_NULL, bAig_NULL);

        flags(v2) |= DummyMask;
        st_insert(tmpTable,(char*)nv,(char*)v2);
      }

      left = 1;
      if(bAig_IsInverted(fan[i]))
        left = 0;
      inv = bAig_IsInverted(fan[i]>>1)?1:0;
      v2 = inv ? bAig_Not(v2) : v2;
      if(left){
#if DBG
        assert(manager->NodesArray[v1+bAigLeft] != v2);
#endif
        manager->NodesArray[v1+bAigLeft] = v2;
        PureSat_connectOutput(manager, v2, v1,0);
        flags(v2) |= CoiMask;
      }
      else{
#if DBG
        assert(manager->NodesArray[v1+bAigRight] != v2);
#endif
        manager->NodesArray[v1+bAigRight] = v2;
        PureSat_connectOutput(manager, v2, v1,1);
        flags(v2) |= CoiMask;
      }
    }
  }

}


void PureSatKillPseudoGV(Ntk_Network_t * network,
                         PureSat_Manager_t *pm,
                         st_table * AbsTable,
                         int from,
                         int to)
{
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  bAigTimeFrame_t *tf = manager->timeframeWOI;
  array_t *bVarList,*mVarList;
  bAigEdge_t * li, *bli,node;
  int i,j;
  st_table * tmpTable, *DoneTable;


  pm->oldPos = manager->nodesArraySize-bAigNodeSize;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  if(from < 1)
    from = 1;

  if(to>pm->Length)
    to=pm->Length;

  li = tf->latchInputs[1];
  bli = tf->blatchInputs[1];
  for(j=0;j<tf->nLatches;j++)
    flags(li[j])&=ResetPGVMask;
  for(j=0;j<tf->nbLatches;j++)
    flags(bli[j])&=ResetPGVMask;

  for(i=from;i<=to;i++){
    li = tf->latchInputs[i];
    bli = tf->blatchInputs[i];
    manager->class_ = i;
    tmpTable = st_init_table(st_numcmp,st_numhash);
    DoneTable = st_init_table(st_numcmp,st_numhash);

    for(j=0; j<tf->nLatches; j++){
      node = bAig_NonInvertedEdge(li[j]);
      if(st_lookup(DoneTable,(char*)node,NIL(char*)))
        continue;
      st_insert(DoneTable,(char*)node,(char*)0);
      if((flags(node)&StateBitMask)&&
         !(flags(node)&VisibleVarMask)&&
         (flags(node)&CoiMask)){
        if(i==1)
          PureSatKillPseudoGVNode(manager,node,tmpTable);
        else
          PureSatAbstractLatch(manager,node,tmpTable);
      }
    }

    for(j=0; j<tf->nbLatches; j++){
      node = bAig_NonInvertedEdge(bli[j]);
      if(st_lookup(DoneTable,(char*)node,NIL(char*)))
        continue;
      st_insert(DoneTable,(char*)node,(char*)0);
      if((flags(node)&StateBitMask)&&
         !(flags(node)&VisibleVarMask)&&
         (flags(node)&CoiMask)){
        if(i==1)
          PureSatKillPseudoGVNode(manager,node,tmpTable);
        else
          PureSatAbstractLatch(manager,node,tmpTable);
      }
    }
    st_free_table(tmpTable);
    st_free_table(DoneTable);
  }
}


int PureSat_CountNodesInCoi(satManager_t* cm)
{
  int ct=0;
  bAigEdge_t i;

  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    if(SATflags(i) & CoiMask){
      ct++;

    }
  }
  /*fprintf(vis_stdout,"There are %d node in COI\n",ct);*/
  return ct;
}

void PureSat_Check(bAig_Manager_t *manager, bAigEdge_t v)
{
  bAigEdge_t *fan,*fan1,nfan1;
  bAigEdge_t nfan,cur,child,tmpchild,v1,other,cur1;
  int size,i,j,find=0,inver,left,left1;

  nfan = nFanout(v);
  fan = (bAigEdge_t *)fanout(v);
  if(fan == 0){
    assert(nfan==0);
    return;
  }

  size = 0;

  for(i=0; fan[i]!=0; i++){
    size++;
    cur = fan[i];
    left = 1;
    inver = 0;
    if(SATisInverted(cur))
      left = 0;
    cur >>= 1;
    if(SATisInverted(cur))
      inver = 1;
    cur = SATnormalNode(cur);
    child = inver? SATnormalNode(v)+1:SATnormalNode(v);
    if(left)
      tmpchild = leftChild(cur);
    else
      tmpchild = rightChild(cur);
    assert(tmpchild == child);

    /*check the other child*/
    find = 0;
    other = left?rightChild(cur):leftChild(cur);
    assert(other!=bAig_NULL);
    v1 = SATnormalNode(other);
    nfan1 = nFanout(v1);
    fan1 = (bAigEdge_t *)fanout(v1);
    assert(nfan1!=0&&fan1!=0);
    for(j=0; fan1[j]!=0; j++){
      cur1 = fan1[j];
      left1 = 1;
      if(SATisInverted(cur1))
        left1 = 0;
      assert(j<nfan1);
      if((SATnormalNode(cur1>>1)==cur)&&(left1!=left)){
        find = 1;

        break;
      }
    }
    assert(find);
  }

  assert(nfan==size);
}


void PureSat_CheckFanoutFanin(bAig_Manager_t *manager)
{
  bAigEdge_t  i,v;

  for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
    v = i;
    if((flags(v) & IsCNFMask))
      continue;
    PureSat_Check(manager,v);
  }
}

/*1. eliminate concls, 2. free variableArray
  3. adjust nodeArray(size and new nodes)*/
void PureSat_ResetManager(mAig_Manager_t *manager,
                          satManager_t *cm, int clean)
{

  int i;
  satVariable_t var;
  satLevel_t *d;

  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->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;
    cm->currentDecision = 0;
  }

  if(cm->literals){
    sat_FreeLiteralsDB(cm->literals);
    cm->literals=0;
    sat_AllocLiteralsDB(cm);
  }
  if(cm->each){
    FREE(cm->each);
    cm->each = sat_InitStatistics();
  }

  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->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
  if(cm->dormantConflictArray) sat_ArrayFree(cm->dormantConflictArray);
  if(cm->shrinkArray)          sat_ArrayFree(cm->shrinkArray);

  cm->nonobjUnitLitArray = 0;
  cm->objUnitLitArray = 0;
  cm->orderedVariableArray = 0;
  cm->dormantConflictArray = 0;
  cm->shrinkArray = 0;

  /*change initNumVariable after cm->variableArray has been freed,
    otherwise, initNumVariable may change*/
  cm->nodesArray = manager->NodesArray;
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;

  cm->ipm = manager->ipm;
  cm->assertArray = manager->assertArray;
  cm->assertArray2 = manager->assertArray2;
  cm->InitState = manager->InitState;
  cm->CoiAssertArray = manager->CoiAssertArray;
  cm->EqArray = manager->EqArray;

  cm->currentVarPos = 0;
  cm->currentTopConflict = 0;
  cm->currentTopConflictCount = 0;
  cm->lowestBacktrackLevel = 0;
  cm->implicatedSoFar = 0;
  //cm->status = 0;

  if(clean){
    for(i=bAigNodeSize;i<cm->nodesArraySize;i+=bAigNodeSize)
      cm->nodesArray[i] = 2;
  }
}


void PureSat_RestoreAigForDummyNode(mAig_Manager_t *manager,
                                    int oldPosition)
{

  bAigEdge_t  i;

  for(i=manager->nodesArraySize-bAigNodeSize;
      i>oldPosition;i=i-bAigNodeSize){
#if DBG
    assert(leftChild(i)==bAig_NULL&&
           rightChild(i)==bAig_NULL);
    assert(flags(i)&DummyMask);
#endif
    FREE(fanout(i));
  }

  manager->nodesArraySize = oldPosition+bAigNodeSize;

  return;

}

/*after this funct, all nodes' fanout, either COI or not
  are in COI, not InvSV, and if this node is InvSV, not to a node in the next tf*/
void PureSatProcessFanout(satManager_t * cm)
{

long bufSize, bufIndex;
bAigEdge_t *buf,left,right,*fan,v,cur;
int i, j;
long size, tsize;

int InvStateVar,l;


  bufSize = 1024;
  bufIndex = 0;
  buf = malloc(sizeof(bAigEdge_t) * bufSize);
  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;

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

    InvStateVar = 0;
    if((SATflags(v)&StateBitMask)&&
       !(SATflags(v)&VisibleVarMask))
      InvStateVar = 1;

    size = SATnFanout(v);
    if(size >= bufSize) {
      bufSize <<= 1;
      if(size >= bufSize)
        bufSize = size + 1;
      buf = realloc(buf, sizeof(bAigEdge_t) * bufSize);
    }

    bufIndex = 0;
    for(j=0, fan = SATfanout(v); j<size; j++) {
      cur = fan[j];
      cur >>= 1;
      cur = SATnormalNode(cur);
      /*Not in COI , pass */
      if(!(SATflags(cur) & CoiMask))
        continue;
      /*cur is invisible var*/
      left = SATleftChild(cur);
      right = SATrightChild(cur);
      if(left==bAig_NULL||right==bAig_NULL){
#if DBG

        assert(left==bAig_NULL&&right==bAig_NULL);
        assert((SATflags(cur)&StateBitMask)&&
               !(SATflags(cur)&VisibleVarMask));
#endif
        continue;
      }
      /*v itself is InvStateVar and cur is not InvSV*/

      if(SATflags(v)&PGVMask){

         if(SATclass(cur)>=2){
          l = SATisInverted(fan[j]) ? 0 : 1;
          if(l){
#if DBG
            bAigEdge_t v1 = SATnormalNode(SATleftChild(cur));
            assert(v1!=v);
            assert(SATflags(v1)&DummyMask);
#endif
          }
          else{
#if DBG
            bAigEdge_t v1 = SATnormalNode(SATrightChild(cur));
            assert(v1!=v);
            assert(SATflags(v1)&DummyMask);
#endif
          }
          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;
        }

        left = SATleftChild(cur);
        right = SATrightChild(cur);

        if(left==bAig_NULL||right==bAig_NULL){
          buf[bufIndex++] = fan[j];
          continue;
        }


        if(SATflags(v)&PGVMask){
          if(SATclass(cur)>=2){
            buf[bufIndex++] = fan[j];
            continue;
          }
        }

      }/*for(j=0, fan=SATfanout(v); j<size; j++) {*/
      buf[bufIndex] = 0;
      memcpy(fan, buf, sizeof(bAigEdge_t)*(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(bAigEdge_t), NodeIndexCompare);
  }
}
long PureSatRecoverFanoutNode(satManager_t * cm,
                              bAigEdge_t v)
{
  bAigEdge_t *fan,nfan,child,cur;
  long i;
  int left,inver;
  int InvStateVar = 0;

  if(!(SATflags(v)&VisibleVarMask)&&(SATflags(v)&StateBitMask))
    InvStateVar = 1;

  nfan = SATnFanout(v);

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

  /*recover left and right children for latch nodes*/

  for(i=nfan; fan[i]!=0; i++){
    cur = fan[i];
    if(!(SATflags(SATnormalNode(cur>>1))&CoiMask))
      continue;
    /*cur is InvSV*/
    if((SATleftChild(SATnormalNode(cur>>1))==bAig_NULL)||
       (SATrightChild(SATnormalNode(cur>>1))==bAig_NULL)){
#if DBG
      assert((SATflags(SATnormalNode(cur>>1))&StateBitMask)&&
             !(SATflags(SATnormalNode(cur>>1))&VisibleVarMask));
#endif
      left = 1;
      inver = 0;
      if(SATisInverted(cur))
        left = 0;
      cur >>= 1;
      if(SATisInverted(cur))
        inver = 1;
      cur = SATnormalNode(cur);
      child = inver? SATnormalNode(v)+1:SATnormalNode(v);
      if(left)
        SATleftChild(cur)=child;
      else
        SATrightChild(cur)=child;
      continue;
    }

    /*v is InvSV, cur is not InvSV*/

    if(SATflags(v)&PGVMask){

      if(SATclass(SATnormalNode(cur>>1))>=2){
        left = 1;
        inver = 0;
        if(SATisInverted(cur))
          left = 0;
        cur >>= 1;
        if(SATisInverted(cur))
          inver = 1;
        cur = SATnormalNode(cur);
        child = inver? SATnormalNode(v)+1:SATnormalNode(v);
        if(left)
          SATleftChild(cur)=child;
        else
          SATrightChild(cur)=child;
      }
    }
  }
  //recover all fanout
  return(i);
}

void
PureSatRecoverISVNode(satManager_t *cm,
                      bAigEdge_t v)
{

  bAigEdge_t size = SATnFanout(v),cur,node,child;
  bAigEdge_t  * fan = SATfanout(v);
  int inv,i,left;

  for(i=0;i<size;i++){
    cur = fan[i]>>1;
    node = SATnormalNode(cur);
    /*not in coi*/
    if(!(SATflags(node)&CoiMask))
      continue;
    /*not invisible var*/
    if(!((SATflags(node)&StateBitMask)&&
         !(SATflags(node)&VisibleVarMask)))
      continue;

    left=SATisInverted(fan[i])?0:1;
    inv=SATisInverted(cur)?1:0;
    child = inv?SATnormalNode(v)+1:SATnormalNode(v);
    if(left)
      SATleftChild(node) = child;
    else
      SATrightChild(node) = child;
  }
}

void PureSatRecoverFanout(satManager_t * cm,
                          PureSat_Manager_t *pm)
{
  bAigEdge_t i, v;

  /*dummy node can't be recovered*/
  for(i=satNodeSize; i<=pm->oldPos; i+=satNodeSize) {
    v = i;
    if(SATflags(v) & IsCNFMask)
      continue;

    if((SATflags(v)&CoiMask)){
       SATnFanout(v) = PureSatRecoverFanoutNode(cm, v);
       continue;
    }
    /*for some node not in coi, but a child of one coi(ISV) node*/
    if(SATflags(v)&Visited3Mask){
      PureSatRecoverISVNode(cm,v);
      continue;
    }
  }

}

void PureSatCheckCoiNode(bAig_Manager_t * manager,
                         bAigEdge_t node)
{
  int i;
  long *fan;
  long  nfan,child, cur;
  int left,inv;

  nfan = nFanout(node);
  fan = (bAigEdge_t*)fanout(node);
  if(fan==0) return;
  /*check child*/
  assert((leftChild(node)==bAig_NULL)||
   (flags(leftChild(node))&CoiMask));
  assert((rightChild(node)==bAig_NULL)||
   (flags(rightChild(node))&CoiMask));
  if((leftChild(node)==bAig_NULL)||(rightChild(node)==bAig_NULL))
    assert((leftChild(node)==bAig_NULL)&&(rightChild(node)==bAig_NULL));
  /*check fanout*/
  for(i=0; i<nfan; i++){
    cur = fan[i]>>1;
    assert(flags(cur)&CoiMask);
    left=SATisInverted(fan[i])?0:1;
    inv=SATisInverted(cur)?1:0;
    child = inv?SATnormalNode(node)+1:SATnormalNode(node);
    if(left){
     assert(child==leftChild(cur));
    }
    else{
      assert(child==rightChild(cur));
    }
  }

}

void PureSatCheckCoi(bAig_Manager_t *manager)
{
  long i;
  for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
    if(flags(i) & IsCNFMask)
      continue;
    if(!(flags(i) & CoiMask))
      continue;
    PureSatCheckCoiNode(manager,i);
  }

}

void PureSatPreprocess(Ntk_Network_t * network,
                       satManager_t *cm,
                       PureSat_Manager_t *pm,
                       st_table *vertexTable,
                       int Length)

{
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);

  PureSatSetCOI(network,pm,cm,vertexTable,0, Length,Length);
  /*for interpolation*/
  PureSatKillPseudoGV(network,pm,vertexTable,1,Length);
  PureSat_ResetManager(manager,cm,0);
  /*for abstraction*/
  PureSatProcessFanout(cm);
}

void PureSatPostprocess(bAig_Manager_t *manager,
                        satManager_t *cm,
                        PureSat_Manager_t *pm)
{

  PureSatRecoverFanout(cm,pm);
  PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
  PureSat_CleanMask(manager,ResetVisited3Mask);
}


/*test if state1 contains state2*/
int PureSat_TestConvergeForIP(mAig_Manager_t *manager,
                              PureSat_Manager_t *pm,
                              satManager_t *cm,
                              bAigEdge_t state1,
                              bAigEdge_t state2)
{
  satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
  int status, nodes_in_coi = 0;

 if(state2 == bAig_Zero)
    return 1;
  if(state1 == bAig_One)
    return 1;
  if(state1 == bAig_Zero && state2 != bAig_Zero)
    return 0;
  if(state1 != bAig_One && state2 == bAig_One)
    return 0;

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"Test convergence:\n");
  PureSat_ResetCoi(cm);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after reset COI\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  tmp1 = cm->obj;
  tmp2 = cm->auxObj;
  tmp3 = cm->assertion;
  tmp4 = cm->assertArray;
  //Bing:
  tmp5 = cm->unitLits;
  tmp6 = cm->pureLits;
  tmp7 = cm->nonobjUnitLitArray;
  cm->obj = 0;
  cm->auxObj = 0;
  cm->assertion = 0;
  //cm->assertArray2 = 0;
  cm->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(cm->assertArray,SATnot(state1));
  sat_ArrayInsert(cm->assertArray,state2);
  sat_SetConeOfInfluence(cm);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after add new init states:\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  cm->option->coreGeneration = 0;
  //cm->option->effIP = 0;
  cm->option->IP = 0;
  cm->status = 0;
  sat_Main(cm);
  if(manager->NodesArray!=cm->nodesArray)
    /*cm->nodesArray may be reallocated*/
    manager->NodesArray = cm->nodesArray;
  cm->obj = tmp1;
  cm->auxObj = tmp2;
  cm->assertion = tmp3;
  sat_ArrayFree(cm->assertArray);
  cm->assertArray = tmp4;

  cm->unitLits = tmp5;
  cm->pureLits = tmp6;
  cm->nonobjUnitLitArray = tmp7;

  cm->option->coreGeneration = 1;

  cm->option->IP = 1;
  status = cm->status;
#if DBG
  assert(cm->currentDecision>=-1);
#endif
  if(cm->currentDecision!=-1)
    sat_Backtrack(cm,-1);
  cm->status = 0;

  if(status == SAT_UNSAT)
    /*state2 contains state1, reach convergence*/
    return 1;
  else
    return 0;
}

/*test if state1 contains state2 for abstract refinement*/
int PureSat_TestConvergeForIP_AbRf(Ntk_Network_t *network,
                                   satManager_t *cm,
                                   PureSat_Manager_t *pm,
                                   array_t  * CoiArray,
                                   bAigEdge_t state1,
                                   bAigEdge_t state2)
{
  satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
  int status, nodes_in_coi = 0;
  mAig_Manager_t * manager;


  if(state2 == bAig_Zero)
    return 1;
  if(state1 == bAig_One)
    return 1;
  if(state1 == bAig_Zero && state2 != bAig_Zero)
    return 0;
  if(state1 != bAig_One && state2 == bAig_One)
    return 0;


  manager = Ntk_NetworkReadMAigManager(network);

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"Test convergence:\n");
  PureSat_ResetCoi(cm);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after reset COI\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  tmp1 = cm->obj;
  tmp2 = cm->auxObj;
  tmp3 = cm->assertion;
  tmp4 = cm->assertArray;

  tmp5 = cm->unitLits;
  tmp6 = cm->pureLits;
  tmp7 = cm->nonobjUnitLitArray;
  cm->obj = 0;
  cm->auxObj = 0;
  cm->assertion = 0;
  cm->unitLits = 0;
  cm->pureLits = 0;
  cm->nonobjUnitLitArray = 0;
  cm->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(cm->assertArray,SATnot(state1));
  sat_ArrayInsert(cm->assertArray,state2);

  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);

  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after add new init states:\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  cm->option->coreGeneration = 0;
  cm->status = 0;
  cm->option->AbRf = 0;
  sat_Main(cm);
  cm->option->AbRf = 1;
  if(manager->NodesArray!=cm->nodesArray)
    /*cm->nodesArray may be reallocated*/
    manager->NodesArray = cm->nodesArray;
  sat_ArrayFree(cm->assertArray);
  manager->assertArray = tmp4;
  cm->obj = tmp1;
  cm->auxObj = tmp2;
  cm->assertion = tmp3;
  cm->assertArray = tmp4;

  cm->unitLits = tmp5;
  cm->pureLits = tmp6;
  cm->nonobjUnitLitArray = tmp7;
  cm->option->coreGeneration = 1;
  status = cm->status;
  if(cm->currentDecision!=-1)
    sat_Backtrack(cm,-1);
  cm->status = 0;

  if(status == SAT_UNSAT)
    /*state2 contains state1, reach convergence*/
    return 1;
  else
    return 0;
}

satManager_t * PureSat_SatManagerAlloc(bAig_Manager_t *manager,
                                       PureSat_Manager_t *pm,
                                       bAigEdge_t     object,
                                       array_t        *auxObjectArray)
{
  satManager_t * cm;
  satOption_t *option;
  int i,size;
  bAigEdge_t tv;

  cm = ALLOC(satManager_t, 1);
  memset(cm, 0, sizeof(satManager_t));
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->nodesArray = manager->NodesArray;

  cm->HashTable = manager->HashTable;
  cm->literals = manager->literals;

  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdErr = vis_stderr;
  cm->stdOut = vis_stdout;
  cm->status = 0;
  cm->orderedVariableArray = 0;
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  cm->option = 0;
  cm->each = 0;
  cm->decisionHead = 0;
  cm->variableArray = 0;
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  cm->ipm = manager->ipm;
  cm->assertArray = manager->assertArray;
  cm->assertArray2 = manager->assertArray2;
  cm->InitState = manager->InitState;
  cm->CoiAssertArray = manager->CoiAssertArray;
  cm->EqArray = manager->EqArray;

  if(auxObjectArray) {
    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
    size = auxObjectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->auxObj, tv);
    }
  }
  if(object == 0)      cm->status = SAT_UNSAT;
  else if(object == 1) cm->status = SAT_SAT;


  if(cm->status == 0) {
    if(object!=-1){
      cm->obj = sat_ArrayAlloc(1);
      sat_ArrayInsert(cm->obj, object);
    }
    /* initialize option*/
    option = sat_InitOption();

    option->coreGeneration = 1;
    option->ForceFinish = 1;

    option->clauseDeletionHeuristic = 0;
    option->includeLevelZeroLiteral = 1;
    option->minimizeConflictClause = 0;
    option->IP = 1;
    option->RT = 1;
    option->verbose = pm->verbosity;

    cm->anteTable = st_init_table(st_numcmp,st_numhash);
    cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager,cm);

    /* value reset..*/
    sat_CleanDatabase(cm);

    /* set cone of influence*/
    sat_SetConeOfInfluence(cm);
    sat_AllocLiteralsDB(cm);
  }
  return cm;
}


satManager_t * PureSat_SatManagerAlloc_WOCOI(mAig_Manager_t *manager,
                                             PureSat_Manager_t *pm,
                                             bAigEdge_t     object,
                                             array_t        *auxObjectArray)
{
  satManager_t * cm;
  satOption_t *option;
  int i,size;
  bAigEdge_t tv;

  cm = ALLOC(satManager_t, 1);
  memset(cm, 0, sizeof(satManager_t));
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->nodesArray = manager->NodesArray;

  cm->HashTable = manager->HashTable;
  cm->literals = manager->literals;

  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdErr = vis_stderr;
  cm->stdOut = vis_stdout;
  cm->status = 0;
  cm->orderedVariableArray = 0;
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  cm->option = 0;
  cm->each = 0;
  cm->decisionHead = 0;
  cm->variableArray = 0;
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  cm->ipm = manager->ipm;
  cm->assertArray = manager->assertArray;
  cm->assertArray2 = manager->assertArray2;
  cm->InitState = manager->InitState;
  cm->CoiAssertArray = manager->CoiAssertArray;
  cm->EqArray = manager->EqArray;

  if(auxObjectArray) {
    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
    size = auxObjectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->auxObj, tv);
    }
  }
  if(object == 0)      cm->status = SAT_UNSAT;
  else if(object == 1) cm->status = SAT_SAT;


  if(cm->status == 0) {
    if(object!=-1){
      cm->obj = sat_ArrayAlloc(1);
      sat_ArrayInsert(cm->obj, object);
    }

    option = sat_InitOption();
    option->ForceFinish = 1;

    option->coreGeneration = 1;
    option->clauseDeletionHeuristic = 0;
    option->includeLevelZeroLiteral = 1;
    option->minimizeConflictClause = 0;
    option->IP = 0;
    option->RT = 1;
    option->verbose = pm->verbosity;

    cm->anteTable = st_init_table(st_numcmp,st_numhash);
    cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager,cm);

    sat_CleanDatabase(cm);

    /* WOCOI: NO set cone of influence*/
    sat_AllocLiteralsDB(cm);
  }
  return cm;
}

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


  if(cm->option->coreGeneration){
    st_free_table(cm->anteTable);
    st_free_table(cm->RTreeTable);

    cm->anteTable=0;
    cm->RTreeTable=0;
  }

  /*timeframe, timeframeWOI,HashTable can't be freed*/

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

  cm->option=0;
  cm->total=0;
  cm->each=0;
  cm->literals=0;

  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->savedConflictClauses) sat_ArrayFree(cm->savedConflictClauses);

  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);
  cm->comment=0;

  FREE(cm);
}

void PureSat_PrintAigStatus(mAig_Manager_t *manager)
{
  (void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n",
                 manager->maxNodesArraySize/bAigNodeSize);
  (void) fprintf(vis_stdout,"Current number of nodes: %ld\n",
                 manager->nodesArraySize/bAigNodeSize);
  fprintf(vis_stdout,"Current Max Node Index: %ld\n\n",
          manager->nodesArraySize);
}

void PureSat_MarkGlobalVar(bAig_Manager_t *manager,
                           int length)
{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t * li,* bli,node;
  int i;

  li = tf->latchInputs[length];
  bli = tf->blatchInputs[length];

  for(i=0; i<tf->nLatches; i++){
    node = bAig_NonInvertedEdge(li[i]);
    manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }

  for(i=0; i<tf->nbLatches; i++){
    node = bAig_NonInvertedEdge(bli[i]);
    manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }
}

void PureSat_UnMarkGlobalVar(bAig_Manager_t *manager,
                           int length)
{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t * li,* bli,node;
  int i;

  li = tf->latchInputs[length];
  bli = tf->blatchInputs[length];

  for(i=0; i<tf->nLatches; i++){
    node = bAig_NonInvertedEdge(li[i]);
    manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
  }

  for(i=0; i<tf->nbLatches; i++){
    node = bAig_NonInvertedEdge(bli[i]);
    manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
  }
}


void PureSat_MarkGlobalVar_AbRf(bAig_Manager_t *manager,
                                int length)
{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t * li,* bli,node;
  int i;


  li = tf->latchInputs[length];
  bli = tf->blatchInputs[length];

  for(i=0; i<tf->nLatches; i++){
    node = bAig_NonInvertedEdge(li[i]);
    if(flags(node)&VisibleVarMask)
      manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }

  for(i=0; i<tf->nbLatches; i++){
    node = bAig_NonInvertedEdge(bli[i]);
    if(flags(node)&VisibleVarMask)
      manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }

}


void PuresatMarkVisibleVarWithVPGV(Ntk_Network_t *network,
                                  array_t * visibleArray,
                                  PureSat_Manager_t *pm,
                                  int from,
                                  int to)
{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  MvfAig_Function_t *mvfAig;
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,k,lmAigId,index,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t node,v, *li, *bli;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  /*Although some SV in tf 0 are not marked as visiblevar,
    //they actually visible since all SV of tf 0 are visible*/
  if(from<0)
    from=0;
  if(to>pm->Length+1)
    to=pm->Length+1;

  /*clean VPGV mask*/
  li = tf->latchInputs[1];
  bli = tf->blatchInputs[1];
  for(j=0;j<tf->nLatches;j++)
    flags(li[j])&=ResetVPGVMask;
  for(j=0;j<tf->nbLatches;j++)
    flags(bli[j])&=ResetVPGVMask;

  for(i=from;i<=to;i++){
    li = tf->latchInputs[i];
    bli = tf->blatchInputs[i];
    arrayForEachItem(char *,visibleArray,k,name){
      int retVal;
      latch = Ntk_NetworkFindNodeByName(network,name);
      st_lookup(node2MvfAigTable,latch,&mvfAig);
      for(j=0;j<mvfAig->num;j++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
        if(v==bAig_Zero||v==bAig_One)
          continue;
        retVal = st_lookup(tf->li2index,(char*)v,&index);
        assert(retVal);
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(li[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
        /*marking PGV*/
        if(i==1){
          if(!st_lookup(pm->vertexTable,name,NIL(char*))){
            flags(node) |= VPGVMask;

          }
        }
      }


      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
        assert(retVal);
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(bli[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
        /*marking PGV*/
        if(i==1){
          if(!st_lookup(pm->vertexTable,name,NIL(char*)))
            flags(node) |= VPGVMask;
        }
      }
    }
  }
  return;

}


void PuresatMarkVisibleVar(Ntk_Network_t *network,
                           array_t * visibleArray,
                           PureSat_Manager_t *pm,
                           int from,
                           int to)
{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  MvfAig_Function_t *mvfAig;
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,k,lmAigId,index,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t node,v, *li, *bli;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);


  if(from<0)
    from=0;
  if(to>pm->Length+1)
    to=pm->Length+1;

  for(i=from;i<=to;i++){
    li = tf->latchInputs[i];
    bli = tf->blatchInputs[i];
    arrayForEachItem(char *,visibleArray,k,name){
      latch = Ntk_NetworkFindNodeByName(network,name);
      st_lookup(node2MvfAigTable,latch,&mvfAig);
      /*multi val var*/
      for(j=0;j<mvfAig->num;j++){
        int retVal;
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
        if(v==bAig_Zero||v==bAig_One)
          continue;
        retVal = st_lookup(tf->li2index,(char*)v,&index);
        assert(retVal);
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(li[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
      }

      /*binary var*/
      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
        assert(retVal);
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(bli[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
      }
    }// arrayForEachItem(char *,visibleArray,k,name)
  }

  return;

}


bAigEdge_t PureSat_MapIPRecur(mAig_Manager_t *manager,
                         bAigEdge_t  node,
                         st_table * tmpTable)
{
  bAigEdge_t v,result,left,right;
  int isInverted;

#if DBG
  assert(node!=bAig_NULL);
#endif
  if(node == bAig_One || node == bAig_Zero){
    return node;
  }

  if(st_lookup(tmpTable,(char *)bAig_NonInvertedEdge(node),&v)){
    if(bAig_IsInverted(node))
      result = bAig_Not(v);
    else
      result = v;

    return result;
  }

  left = PureSat_MapIPRecur(manager,leftChild(node),tmpTable);
  right = PureSat_MapIPRecur(manager,rightChild(node),tmpTable);

  v = PureSat_And(manager,left,right);
  isInverted = bAig_IsInverted(node);
  result = isInverted ? bAig_Not(v) : v;
  st_insert(tmpTable,(char *)bAig_NonInvertedEdge(node),(char *)v);

  //fprintf(vis_stdout,"return %d->%d\n",node,result);
  return result;
}



bAigEdge_t PureSat_MapIP(mAig_Manager_t *manager,
                         bAigEdge_t node,
                         int from,
                         int to)
{
  bAigTimeFrame_t *tf = manager->timeframeWOI;
  st_table *tmpTable = st_init_table(st_numcmp,st_numhash);
  bAigEdge_t * L1,*L0,result,v1,v0;
  int i;

  if(node==bAig_One||node==bAig_Zero)
    return node;

  L1 = tf->latchInputs[from];
  L0 = tf->latchInputs[to];
  for(i=0;i<tf->nLatches;i++){
   v1 = L1[i];
   v0 = L0[i];
   if(SATisInverted(v1)){
     v1 = SATnot(v1);
     v0 = SATnot(v0);
   }
   st_insert(tmpTable,(char*)v1,(char*)v0);

  }
  L1 = tf->blatchInputs[from];
  L0 = tf->blatchInputs[to];
  for(i=0;i<tf->nbLatches;i++){
    v1 = L1[i];
    v0 = L0[i];
    if(SATisInverted(v1)){
      v1 = SATnot(v1);
      v0 = SATnot(v0);
    }
    st_insert(tmpTable,(char*)v1,(char*)v0);

  }

  manager->class_ = to;
  result = PureSat_MapIPRecur(manager,node,tmpTable);

  st_free_table(tmpTable);

  return result;
}


void PureSatProcessDummy(bAig_Manager_t *manager,
                         satManager_t *cm,
                         RTnode_t  RTnode)
{
  int i;
  bAigEdge_t *lp,node;
  RTManager_t *rm = cm->rm;

  if(RT_flag(RTnode)&RT_VisitedMask){
    return;
  }
  RT_flag(RTnode) |= RT_VisitedMask;

  if(RT_pivot(RTnode)==0){ /*leaf*/
#if DBG
    assert(RT_oriClsIdx(RTnode)==0);
#endif
    if(RT_oriClsIdx(RTnode))
      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
    else

      lp = RT_formula(RTnode) + cm->rm->fArray;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      assert(*lp>0);/* not processed yet*/
      if(RT_oriClsIdx(RTnode))/*is CNF*/
        node = SATgetNode(*lp);
      else /*is AIG*/
        node = *lp;
      node = SATnormalNode(node);
      if(node>=manager->nodesArraySize){
#if DBG
        assert(flags(node)&DummyMask);
#endif
        *lp = DUMMY;
      }
    }
  } /*leaf*/

  /*not leaf*/
  else{
    if(RT_pivot(RTnode)>=manager->nodesArraySize){
      int class_ = bAig_Class(RT_pivot(RTnode));
      RT_pivot(RTnode) = DUMMY+class_;
    }
    PureSatProcessDummy(manager,cm,RT_left(RTnode));
    PureSatProcessDummy(manager,cm,RT_right(RTnode));
  }

  return ;

}


bAigEdge_t
PureSat_FindNodeByName(
  bAig_Manager_t *manager,
  nameType_t     *name,
  int bound)
{

  bAigEdge_t node;

  if (!st_lookup(manager->SymbolTableArray[bound], name, &node)){
    node = bAig_NULL;
  }

  return bAig_GetCanonical(manager, node);
}


bAigEdge_t
PureSatCreatebAigOfPropFormula(
    Ntk_Network_t *network,
    bAig_Manager_t *manager,
    int bound,
    Ctlsp_Formula_t *ltl,
    int withInitialState)
{
  int index;
  bAigEdge_t result, left, right, *li;
  bAigTimeFrame_t *timeframe;

  if (ltl == NIL(Ctlsp_Formula_t))      return bAig_NULL;
  if (ltl->type == Ctlsp_TRUE_c)        return bAig_One;
  if (ltl->type == Ctlsp_FALSE_c)       return bAig_Zero;

  assert(Ctlsp_isPropositionalFormula(ltl));

  if(withInitialState) timeframe = manager->timeframe;
  else                 timeframe = manager->timeframeWOI;

  if (ltl->type == Ctlsp_ID_c){
      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);

      Var_Variable_t *nodeVar;
      int             nodeValue;

      MvfAig_Function_t  *tmpMvfAig;
      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */

      if (node == NIL(Ntk_Node_t)) {
        char   *nameKey;
        char   tmpName[100];

        sprintf(tmpName, "%s_%d", nodeNameString, bound);
        nameKey = util_strsav(tmpName);

        result  = PureSat_FindNodeByName(manager, nameKey,bound);
        if(result == bAig_NULL){
           result = PureSat_CreateVarNode(manager, nameKey);
        } else {

          FREE(nameKey);
        }
        return result;
      }

      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
      assert(nodeToMvfAigTable != NIL(st_table));

      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
          array_free(tmpMvfAig);
          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      }

      nodeVar = Ntk_NodeReadVariable(node);
      if (Var_VariableTestIsSymbolic(nodeVar)) {
        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
        if ( nodeValue == -1 ) {
          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return bAig_NULL;
        }
      }
      else {
        int check;
         check = StringCheckIsInteger(nodeValueString, &nodeValue);
         if( check == 0 ) {
          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return bAig_NULL;
         }
         if( check == 1 ) {
          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
          return bAig_NULL;
         }
         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return bAig_NULL;

         }
      }
      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
      result = bAig_GetCanonical(manager, result);
      if(st_lookup(timeframe->li2index, (char *)result, &index)) {
        li = timeframe->latchInputs[bound];
        result = bAig_GetCanonical(manager, li[index]);
      }
      else if(st_lookup(timeframe->o2index, (char *)result, &index)) {
        li = timeframe->outputs[bound];
        result = bAig_GetCanonical(manager, li[index]);

      }
      else if(st_lookup(timeframe->i2index, (char *)result, &index)) {
        li = timeframe->internals[bound];
        result = bAig_GetCanonical(manager, li[index]);

      }
      return result;
  }

  left = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
  if (left == bAig_NULL){
    return bAig_NULL;
  }
  right = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
  if (right == bAig_NULL && ltl->type ==Ctlsp_NOT_c ){
    return bAig_Not(left);
  }
  else if(right == bAig_NULL) {
    return bAig_NULL;
  }

  switch(ltl->type) {

    case Ctlsp_OR_c:
      result = PureSat_Or(manager, left, right);
      break;
    case Ctlsp_AND_c:
      result = PureSat_And(manager, left, right);
      break;
    case Ctlsp_THEN_c:
      result = PureSat_Then(manager, left, right);
      break;
    case Ctlsp_EQ_c:
      result = PureSat_Eq(manager, left, right);
      break;
    case Ctlsp_XOR_c:
      result = PureSat_Xor(manager, left, right);
      break;
    default:
      fail("Unexpected type");
  }
  return result;
} /* BmcCirCUsCreatebAigOfPropFormula */




void PureSatMarkObj(bAig_Manager_t * manager,
                    long from,
                    long to)
{
  long v;

  for(v=from;v<=to;v+=bAigNodeSize)
    flags(v)|=ObjMask;
}



boolean PureSat_ConcretTest(Ntk_Network_t *network,
                            PureSat_Manager_t *pm,
                            array_t *sufArray,
                            bAigEdge_t property,
                            array_t *previousResultArray,
                            int Con,
                            int satStat,
                            int inc)
{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  int status,i,nodes_in_coi=0;
  satManager_t *cm;
  char *name;
  double t1,t2;
  satArray_t *saved;
  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
  bAigEdge_t from,*lp;

   arrayForEachItem(char *,sufArray,i,name){
    st_insert(SufAbsNameTable,name,(char*)0);
   }

   manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);

  cm->option->coreGeneration = 0;
  cm->option->RT = 0;
  cm->option->AbRf = 1;
  if(inc){
    cm->option->incTraceObjective = 1;
    cm->savedConflictClauses = pm->savedConCls;
    pm->savedConCls = 0;
  }
  t1 = util_cpu_ctime();
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVar(network,sufArray,pm,0,pm->Length+1);
  if(!Con){
    from = manager->nodesArraySize;
    PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
    PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
    if(inc){
      PureSatMarkObj(manager,from,manager->nodesArraySize-bAigNodeSize);
    }
    PureSat_ResetManager(manager,cm,0);
    PureSatProcessFanout(cm);
  }
  else{
    sat_MarkTransitiveFaninForNode(cm,property,CoiMask);
    sat_MarkTransitiveFaninForNode(cm,manager->InitState,CoiMask);
    cm->option->AbRf = 0;
  }
  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);
  if(pm->verbosity>=1){
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  st_free_table(SufAbsNameTable);
  manager->assertArray2 = cm->assertArray2;
  sat_Main(cm);
  if(satStat)
    sat_ReportStatistics(cm,cm->each);
  cm->option->AbRf = 1;
  manager->NodesArray = cm->nodesArray;
  t1 = util_cpu_ctime();
  if(!Con){
    PureSatRecoverFanout(cm,pm);
    PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
    PureSat_CleanMask(manager,ResetVisited3Mask);
  }
  /*record conflict*/
  if(inc && cm->savedConflictClauses ){
    if(!Con){
      int num=0;
      saved = cm->savedConflictClauses;
      pm->savedConCls = sat_ArrayAlloc(1);
      for(i=0, lp=saved->space; i<saved->num; i++, lp++){
        sat_ArrayInsert(pm->savedConCls,*lp);
        if(*lp<0)
          num++;
      }
      assert(num%2==0);
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"record %d ConCls for incremental concretization\n",num/2);
    }
    else
      pm->savedConCls = 0;
    sat_ArrayFree(cm->savedConflictClauses);
    cm->savedConflictClauses = 0;
  }
  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);
  sat_ArrayFree(manager->assertArray);
  status = cm->status;
  cm->option->coreGeneration = 1;
  PureSat_SatFreeManager(cm);
  if(status == SAT_SAT){
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"CEX exist\n");
    return FALSE; /* cex exists*/
  }
  else{
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"no CEX\n");
    return TRUE;   /* no cex*/
  }

}



boolean PureSat_ConcretTest_Core(Ntk_Network_t *network,
                                 PureSat_Manager_t *pm,
                                 array_t *sufArray,
                                 bAigEdge_t property,
                                 array_t *previousResultArray,
                                 st_table * junkTable)
{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  int status,i,nodes_in_coi=0;
  satManager_t *cm;
  char *name;
  double t1,t2;
  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
  array_t * tmpRef1;
  st_table *refTable = st_init_table(strcmp,st_strhash);

  arrayForEachItem(char *,sufArray,i,name){
    st_insert(SufAbsNameTable,name,(char*)0);
  }

  manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
  cm->option->coreGeneration = 1;
  cm->option->AbRf = 1;
  cm->option->IP = 1;
  t1 = util_cpu_ctime();
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVarWithVPGV(network,sufArray,pm,0,pm->Length+1);

    PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
    PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
    PureSat_ResetManager(manager,cm,0);
    PureSatProcessFanout(cm);

  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);
  if(pm->verbosity>=1){
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  manager->assertArray2 = cm->assertArray2;
  sat_Main(cm);
  manager->NodesArray = cm->nodesArray;
  t1 = util_cpu_ctime();
    PureSatRecoverFanout(cm,pm);
    PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
    PureSat_CleanMask(manager,ResetVisited3Mask);
    if(cm->status==SAT_UNSAT){
      PureSatProcessDummy(manager,cm,cm->rm->root);
      ResetRTree(cm->rm);
    }
  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);

  if(cm->status==SAT_UNSAT){
    tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);

    arrayForEachItem(char*,tmpRef1,i,name)
      st_insert(refTable,name,(char*)0);

    arrayForEachItem(char*,sufArray,i,name){
      if(!st_lookup(refTable,name,NIL(char*))&&
         !st_lookup(pm->vertexTable,name,NIL(char*))){
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"%s can be gotten rid of\n",name);
        st_insert(junkTable,name,(char*)0);
      }
    }
    array_free(tmpRef1);
  }

  st_free_table(SufAbsNameTable);
  st_free_table(refTable);
  RT_Free(cm->rm);
  sat_ArrayFree(manager->assertArray);
  status = cm->status;
  cm->option->coreGeneration = 1;
  PureSat_SatFreeManager(cm);
  if(status == SAT_SAT){
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"CEX exist\n");
    return FALSE; // cex exists
  }
  else{
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"no CEX\n");
    return TRUE;   // no cex
  }

}


void PureSatGenerateRingForNode(Ntk_Network_t *network,
                                PureSat_Manager_t *pm,
                                Ntk_Node_t * node1,
                                array_t * ringArray,
                                int *dfs)
{
  Ntk_Node_t *node;
  char *name;
  int i;

  if(PureSatNodeReadColor(node1) == dfsBlack_c)
    return;
  PureSatNodeSetColor(node1,dfsBlack_c);
  if(Ntk_NodeTestIsLatch(node1)){
    name = Ntk_NodeReadName(node1);
    st_insert(pm->node2dfsTable,name,(char*)(long)(*dfs));
    array_insert_last(char *,ringArray,name);
    return;
  }

  Ntk_NodeForEachFanin(node1,i,node){
    PureSatGenerateRingForNode(network,pm,node,ringArray,
                               dfs);
  }
  return;
}


array_t * PureSatGenerateRing(Ntk_Network_t *network,
                              PureSat_Manager_t *pm,
                              array_t * coreArray,
                              int * dfs)
{
  array_t * ringArray = array_alloc(char *,0);
  int i,j;
  char *name;
  Ntk_Node_t *node1,*node;

  arrayForEachItem(char *,coreArray,i,name){
    node1 = Ntk_NetworkFindNodeByName(network,name);
    Ntk_NodeForEachFanin(node1,j,node){
      PureSatGenerateRingForNode(network,pm,node,
                                 ringArray,dfs);
    }
  }
  return ringArray;
}


void PureSatGenerateDfs(Ntk_Network_t *network,
                        PureSat_Manager_t *pm,
                        array_t * vertexArray)
{

  int dfs = 1,i,ct=0;
  char *name;
  Ntk_Node_t *node;
  array_t * ringArray = array_alloc(char *,0);
  array_t * coreArray;
  lsGen gen;
  st_generator * stgen;

  Ntk_NetworkForEachNode( network, gen, node ) {
    PureSatNodeSetColor( node, dfsWhite_c );
  }

  arrayForEachItem(char *,vertexArray,i,name){
    st_insert(pm->node2dfsTable,name,(char*)(long)dfs);
    node = Ntk_NetworkFindNodeByName(network,name);
    PureSatNodeSetColor(node,dfsBlack_c);
    ct++;
  }

  coreArray = array_dup(vertexArray);

  while(coreArray->num>0){
    dfs++;
    ringArray = PureSatGenerateRing(network,pm,coreArray,
                                    &dfs);
    arrayForEachItem(char*,ringArray,i,name){
      st_insert(pm->node2dfsTable,name,(char*)(long)dfs);

      ct++;
    }
    array_free(coreArray);
    coreArray = ringArray;
  }

  st_foreach_item(pm->CoiTable,stgen,&node,NIL(char*)){
    name = Ntk_NodeReadName(node);
    if(!st_lookup(pm->node2dfsTable,name,NIL(char*))){
      st_insert(pm->node2dfsTable,name,(char*)LARGEDFS);
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"%s LARGEDFS is inserted into node2dfsTable\n",name);
    }
  }

  return;

}

array_t * PureSatComputeOrder_2(Ntk_Network_t *network,
                              PureSat_Manager_t *pm,
                              array_t * vertexArray,
                              array_t * invisibleArray,
                              int * sccArray,
                              int * NumInSecondLevel)
{

  array_t * RCArray;

  PureSatGenerateDfs(network,pm,vertexArray);
  RCArray = PureSatGenerateRCArray_2(network,pm,invisibleArray,
                                   NumInSecondLevel);

  return RCArray;
}



void PureSatAddIdenLatchToAbs(Ntk_Network_t *network,
                              PureSat_Manager_t *pm,
                              array_t *nameArray)
{
  int i;
  st_generator * stgen;
  st_table* table;
  char *name,*name1;
  st_table *table1 = st_init_table(st_ptrcmp,st_ptrhash);
  array_t * tmpArray = array_alloc(char*,0);

  st_foreach_item(pm->vertexTable,stgen,&name,NIL(char*))
    st_insert(table1,name,(char*)0);
  arrayForEachItem(char*,nameArray,i,name)
    st_insert(table1,name,(char*)0);

  arrayForEachItem(char*,nameArray,i,name){

    if(st_lookup(pm->IdenLatchTable,name,&table)){
      st_foreach_item(table,stgen,&name1,NIL(char*)){
        if(!st_lookup(table1,name1,NIL(char*))){
          st_insert(table1,name1,(char*)0);
          array_insert_last(char*,tmpArray,name1);
        }
      }
    }
  }

  arrayForEachItem(char*,tmpArray,i,name){
    array_insert_last(char*,nameArray,name);
    if(pm->verbosity>=2)
      fprintf(vis_stdout,"add %s to refineArray\n",name);
  }

  array_free(tmpArray);
  st_free_table(table1);
}


void
PureSatCreateInitAbsByAIG(bAig_Manager_t *manager,
                          PureSat_Manager_t *pm,
                          bAigEdge_t node,
                          st_table * tmpTable)
{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  char * name;
  st_table * table;
  st_generator * stgen;

  if(node==bAig_NULL)
    return;

  node = bAig_NonInvertedEdge(node);

  if(flags(node)&VisitedMask)
    return;

  flags(node) |= VisitedMask;


  if(flags(node)&StateBitMask){
    if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
      int retVal = st_lookup(tf->idx2name,(char*)node,&name);
      assert(retVal);
      if(!st_lookup(tmpTable,name,NIL(char*))){
        st_insert(tmpTable,name,(char*)0);

      }
    }
    else{
      st_foreach_item(table,stgen,&name,NIL(char*)){
        if(!st_lookup(tmpTable,name,NIL(char*))){
          st_insert(tmpTable,name,(char*)0);

        }
      }
    }
  }

  if(flags(node)&StateBitMask)
    return;

  PureSatCreateInitAbsByAIG(manager,pm,leftChild(node),tmpTable);
  PureSatCreateInitAbsByAIG(manager,pm,rightChild(node),tmpTable);
}


void
PureSat_GetLatchForNode(bAig_Manager_t *manager,
                        PureSat_Manager_t *pm,
                        bAigEdge_t node,
                        array_t * nameArray,
                        st_table *tmpTable,
                        int cut)
{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  char * name;
  st_table * table;
  st_generator * stgen;

  if(node==bAig_NULL)
    return;

  node = bAig_NonInvertedEdge(node);

  if(flags(node)&VisitedMask)
    return;

  flags(node) |= VisitedMask;


  if(flags(node)&StateBitMask){
    if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
      int retVal = st_lookup(tf->idx2name,(char*)node,&name);
      assert(retVal);
      if(!st_lookup(tmpTable,name,NIL(char*))){
        st_insert(tmpTable,name,(char*)0);
        array_insert_last(char *,nameArray,name);
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"insert %s\n",name);
      }
    }
    else{
      st_foreach_item(table,stgen,&name,NIL(char*)){
        if(!st_lookup(tmpTable,name,NIL(char*))){
          st_insert(tmpTable,name,(char*)0);
          array_insert_last(char *,nameArray,name);
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"insert %s\n",name);
        }
      }
    }
  }

  if(cut==2){
    if(flags(node)&Visited2Mask)
      return;
  }
  else{
    if(cut==1){
      if(flags(node)&Visited3Mask)
        return;
    }
    else{
      fprintf(vis_stdout,"wrong cut\n");
      exit(0);
    }
  }

  PureSat_GetLatchForNode(manager,pm,leftChild(node),nameArray,tmpTable,cut);
  PureSat_GetLatchForNode(manager,pm,rightChild(node),nameArray,tmpTable,cut);
}


st_table * PureSatGetAigCoi(Ntk_Network_t *network,
                            PureSat_Manager_t *pm,
                            bAigEdge_t property)
{
  bAig_Manager_t *manager;
  st_table * node2MvfAigTable,*tmpTable;
  array_t * nameArray,*nameArray1;
  bAigTimeFrame_t *tf;
  char * name;
  Ntk_Node_t *latch;
  MvfAig_Function_t *mvfAig;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,lmAigId;
  long index,index1;
  bAigEdge_t v, *li, *bli;

  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout,
                   "** bmc error: run build_partition_maigs command first\n");
    exit(0);;
  }
  node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                    MVFAIG_NETWORK_APPL_KEY);
  tf = manager->timeframeWOI;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  assert(manager->timeframeWOI->currentTimeframe>=2);
  PureSat_CleanMask(manager,ResetVisitedMask);
  PureSat_CleanMask(manager,ResetVisited2Mask);
  PureSat_CleanMask(manager,ResetVisited3Mask);
  li = tf->latchInputs[1];
  for(i=0;i<tf->nLatches;i++)
    flags(li[i])|=Visited3Mask;
  li = tf->blatchInputs[1];
  for(i=0;i<tf->nbLatches;i++)
    flags(li[i])|=Visited3Mask;
  li = tf->latchInputs[2];
  for(i=0;i<tf->nLatches;i++)
    flags(li[i])|=Visited2Mask;
  li = tf->blatchInputs[2];
  for(i=0;i<tf->nbLatches;i++)
    flags(li[i])|=Visited2Mask;

  nameArray = array_alloc(char *,0);
  tmpTable = st_init_table(st_ptrcmp,st_ptrhash);
  PureSat_GetLatchForNode(manager,pm,property,nameArray,tmpTable,2);
  PureSat_CleanMask(manager,ResetVisitedMask);


  li = tf->latchInputs[2];
  bli = tf->blatchInputs[2];
  while(nameArray->num>0){
    nameArray1 = nameArray;
    nameArray = array_alloc(char *,0);
    arrayForEachItem(char*,nameArray1,i,name){
      latch = Ntk_NetworkFindNodeByName(network,name);
      st_lookup(node2MvfAigTable,latch,&mvfAig);
      for(j=0;j<mvfAig->num;j++){
        int retVal;
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
        if(v==bAig_Zero||v==bAig_One)
          continue;
        retVal = st_lookup(tf->li2index,(char*)v,&index);
        assert(retVal);
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        PureSat_GetLatchForNode(manager,pm,li[index],nameArray,tmpTable,1);
      }


      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
        assert(retVal);
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        PureSat_GetLatchForNode(manager,pm,bli[index],nameArray,tmpTable,1);
      }
    }

    array_free(nameArray1);
  }

  array_free(nameArray);
  PureSat_CleanMask(manager,ResetVisitedMask);
  PureSat_CleanMask(manager,ResetVisited2Mask);
  PureSat_CleanMask(manager,ResetVisited3Mask);

  return tmpTable;
}


void PureSatPreProcLatch(Ntk_Network_t *network,
                         PureSat_Manager_t *pm)
{
  st_generator * stgen;
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int j,lmAigId,id,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t v, **li, **bli;
  MvfAig_Function_t *mvfAig;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);
  li = tf->latchInputs;
  bli = tf->blatchInputs;

  st_foreach_item(pm->CoiTable,stgen,&latch,NIL(char*)){
    int checkbin=1;
    st_lookup(node2MvfAigTable,latch,&mvfAig);
    for(j=0;j<mvfAig->num;j++){
      int retVal;
      v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
      if(v==bAig_Zero||v==bAig_One)
        continue;
      retVal = st_lookup(tf->li2index,(char*)v,&id);
      assert(retVal);
      if(li[0][id]==li[1][id]&&li[1][id]==li[2][id]){
        name = Ntk_NodeReadName(latch);
        st_insert(pm->vertexTable,name,(char*)0);
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"preproc: add %s to abs\n",name);
        checkbin = 0;
        break;
      }
    }
    if(checkbin){
      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&id);
        assert(retVal);
        if(bli[0][id]==bli[1][id]&&bli[1][id]==bli[2][id]){
          name = Ntk_NodeReadName(latch);
          st_insert(pm->vertexTable,name,(char*)0);
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"preproc BINARY: add %s to abs\n",name);
          break;
        }
      }
    }
  }

}


void PureSatGetIndenticalLatch(Ntk_Network_t *network,
                               PureSat_Manager_t *pm)
{
  bAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t *li=tf->latchInputs[2],*bli = tf->blatchInputs[2];
  int i;
  bAigEdge_t v;
  st_table *table;
  st_generator *stgen,*stgen1;
  char *name,*name1;
  st_table *table2,*table1=st_init_table(st_ptrcmp,st_ptrhash);

  pm->IdenLatchTable = st_init_table(st_ptrcmp,st_ptrhash);

  for(i=0;i<tf->nLatches;i++){
    v=bAig_NonInvertedEdge(li[i]);
    if(!st_lookup(table1,(char*)v,NIL(char*))){
      if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
        int init=0;
        st_foreach_item(table,stgen,&name,NIL(char*)){
          if(!st_lookup(pm->IdenLatchTable,name,&table2)){
            st_insert(pm->IdenLatchTable,name,table);
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"%s and ",name);
            init = 1;
          }
          /*insert everything in table 2 into table
          name is already in another group, put everything of current group
          into that group*/
          else{
            st_foreach_item(table,stgen1,&name1,NIL(char*)){
              st_insert(table2,name1,(char*)0);
              st_insert(pm->IdenLatchTable,name1,table2);
              if(pm->verbosity>=2)
                fprintf(vis_stdout,"%s and ",name1);
            }
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"are the same\n");
            break;
          }
        }
        if(init){
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"are the same\n");
        }
      }
      st_insert(table1,(char*)v,(char*)0);
    }
  }


  for(i=0;i<tf->nbLatches;i++){
    v=bAig_NonInvertedEdge(bli[i]);
    if(!st_lookup(table1,(char*)v,NIL(char*))){
      if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
        int init=0;
        st_foreach_item(table,stgen,&name,NIL(char*)){

          if(!st_lookup(pm->IdenLatchTable,name,table2)){
            st_insert(pm->IdenLatchTable,name,table);
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"%s and ",name);
            init = 1;
          }
          /*insert everything in table 2 into table
          name is already in another group, put everything of current group
          into that group*/
          else{
            st_foreach_item(table,stgen1,&name1,NIL(char*)){

              st_insert(table2,name1,(char*)0);
              st_insert(pm->IdenLatchTable,name1,table2);
              if(pm->verbosity>=2)
                fprintf(vis_stdout,"%s and ",name1);
            }
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"are the same\n");
            break;
          }
        }
        if(init){
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"are the same\n");
        }
      }
      st_insert(table1,(char*)v,(char*)0);
    }
  }

  st_free_table(table1);
}