src/puresat/puresatUtil.c

Go to the documentation of this file.

#include "puresatInt.h"
#include "sat.h"

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

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

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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static array_t *RCArray;

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

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


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


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


static int DfsLevel = 0;
static array_t *NumInCone;
static array_t *NumInAbs;
static array_t *DfsArray;
/*static array_t *RCArray;*/


PureSat_Manager_t * PureSatManagerAlloc(void)
{
  PureSat_Manager_t * pm = ALLOC(PureSat_Manager_t,1);
  memset(pm,0,sizeof(PureSat_Manager_t));
  pm->incre = TRUE;
  pm->ltlFileName = ALLOC(char,200);
  pm->timeOutPeriod = 10000000;
  pm->Arosat = TRUE;;
  pm->CoreRefMin = TRUE;
  pm->RefPredict = TRUE;
  pm->Switch = TRUE;
  return pm;
}

void
PureSatManagerFree(PureSat_Manager_t * pm){
  if(pm->latchToTableBaigNodes)
    st_free_table(pm->latchToTableBaigNodes);
  if(pm->ClsidxToLatchTable)
    st_free_table(pm->ClsidxToLatchTable);
  if(pm->CoiTable)
    st_free_table(pm->CoiTable);
  if(pm->AbsTable)
    st_free_table(pm->AbsTable);
  if(pm->vertexTable)
    st_free_table(pm->vertexTable);
  if(pm->SufAbsTable)
    st_free_table(pm->SufAbsTable);;
  if(pm->supportTable)
    st_free_table(pm->supportTable);
  if(pm->node2dfsTable)
    st_free_table(pm->node2dfsTable);
  if(pm->result!=NIL(array_t))
    array_free(pm->result);
  FREE(pm->ltlFileName);
  FREE(pm);

}

PureSat_IncreSATManager_t * PureSatIncreSATManagerAlloc(PureSat_Manager_t * pm)
{
  PureSat_IncreSATManager_t * pism = ALLOC(PureSat_IncreSATManager_t,1);
  pism->beginPosition = 0;
  pism->Length = 0;
  pism->oldLength = 0;
  pism->propertyPos = 0;
  memset(pism,0,sizeof(PureSat_IncreSATManager_t));
  if(pm->sss){
    pism->cnfClauses = BmcCnfClausesAlloc();
    pism->cm = sat_InitManager(0);
    pism->cm->comment = ALLOC(char, 2);
    pism->cm->comment[0] = ' ';
    pism->cm->comment[1] = '\0';

    pism->cm->maxNodesArraySize = 1;
    pism->cm->nodesArray = ALLOC(long, pism->cm->maxNodesArraySize );
    pism->cm->nodesArraySize = satNodeSize;
    pism->cm->stdErr = vis_stderr;
    pism->cm->stdOut = vis_stdout;
    pism->cm->unitLits = sat_ArrayAlloc(16);
    pism->cm->pureLits = sat_ArrayAlloc(16);
    pism->cm->each = sat_InitStatistics();
    pism->cm->option = sat_InitOption();
    pism->cm->option->ForceFinish = 1;
    pism->cm->option->incTraceObjective = 1;
    pism->cm->option->includeLevelZeroLiteral = 1;
    pism->cm->option->minimizeConflictClause = 0;
    pism->cm->option->SSS = 1;
  }
  return pism;
}

void
PureSatIncreSATManagerFree(PureSat_Manager_t *pm,
                           PureSat_IncreSATManager_t * pism)
{
  if(pm->sss){
    BmcCnfClausesFree(pism->cnfClauses);
    FREE(pism->cm->nodesArray);
    sat_ArrayFree(pism->cm->unitLits);
    sat_ArrayFree(pism->cm->pureLits);
    sat_FreeStatistics(pism->cm->each);
    sat_FreeOption(pism->cm->option);
    FREE(pism->cm);
  }
  FREE(pism);
}

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

  if(node == NIL(Ntk_Node_t)){
    return;
  }
  if(Ntk_NodeTestIsLatch(node)){
    DfsLevel++;
    if (st_lookup_int(CoiTable, node, &j)&&j<=DfsLevel){
      DfsLevel--;
      return;
    }
  }

  if (st_lookup_int(visited,  node, &j)&&j<=DfsLevel){
    if(Ntk_NodeTestIsLatch(node))
      DfsLevel--;
    return;
  }
  st_insert(visited, node, (char *)(long)DfsLevel);
  if (Ntk_NodeTestIsLatch(node)){
    st_insert(CoiTable,  node, (char *)(long)DfsLevel);
  }

  if(Ntk_NodeTestIsInput(node))
    {
      return;
    }

  Ntk_NodeForEachFanin(node, i, faninNode) {
    PureSatBmcGetCoiForNtkNode(faninNode, CoiTable, visited);
  }
  if(Ntk_NodeTestIsLatch(node))
    DfsLevel--;
  return;
}

void
PureSatBmcGetCoiForLtlFormulaRecursive(
  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, node, &tmp)){
      /* Node already visited */
      return;
    }
    PureSatBmcGetCoiForNtkNode(node, ltlCoiTable, visited);
    return;
  }
  PureSatBmcGetCoiForLtlFormulaRecursive(network, formula->left,  ltlCoiTable, visited);
  PureSatBmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited);

  return;
}

DfsColor
PureSatNodeReadColor(
  Ntk_Node_t * node)
{
  return ((DfsColor) (long) Ntk_NodeReadUndef(node));
}

void
PureSatNodeSetColor(
  Ntk_Node_t * node,
  DfsColor  color)
{
  Ntk_NodeSetUndef(node, (void *) (long) color);
}

void
PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes(
  Ntk_Node_t *node,
  int * NumofSupports,
  boolean stopAtLatches)
{
  int i;
  Ntk_Node_t * fanin;

  /* test if we have already started processing this node */
  if ( PureSatNodeReadColor( node ) == dfsBlack_c ) {
        return;
  }
  PureSatNodeSetColor( node, dfsBlack_c );

  /* if ( Ntk_NodeTestIsCombInput( node ) ) {
  st_insert( resultTable, (char *) node, (char *) 0 );
         }*/

  (*NumofSupports)++;

  if ( Ntk_NodeTestIsInput(node) || ((stopAtLatches == TRUE)&&(Ntk_NodeTestIsLatch(node))) ) {
        return;
  }

  Ntk_NodeForEachFanin( node, i, fanin ) {
        PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( fanin, NumofSupports, stopAtLatches );
  }
}

int
PureSatNodeComputeCombinationalSupport_AllNodes(
  Ntk_Network_t *network,
  array_t * nodeArray,
  boolean stopAtLatches )
{
  lsGen gen;
  int i, NumofSupports=0;
  Ntk_Node_t *node;

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

/* for each lacthes(node) in the nodeArray, compute the number of gates in
   the cone of this latch, put the number in NumofSupports*/
  arrayForEachItem( Ntk_Node_t *, nodeArray, i, node ) {
    NumofSupports = 0;
    PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( node, &NumofSupports, stopAtLatches );
  }

  return NumofSupports;
}

/*build a supportTable, each value associated with a latch is NumofGatesInCone*/
void PureSatGenerateSupportTable(
  Ntk_Network_t   *network,
  PureSat_Manager_t *pm)
{
  array_t    *roots = array_alloc(Ntk_Node_t *,0); /*supports;*/
  st_generator *stgen;
  Ntk_Node_t *node,*DataNode=(Ntk_Node_t *)0;
  int        count, NumofSupports;

  st_foreach_item_int(pm->CoiTable, stgen, &node, &count) {
    if (Ntk_NodeTestIsLatch(node))
      DataNode = Ntk_LatchReadDataInput(node);
    array_insert(Ntk_Node_t *, roots, 0, DataNode);
    NumofSupports = PureSatNodeComputeCombinationalSupport_AllNodes(network, roots,FALSE);

    st_insert(pm->supportTable,node, (char *)(long)NumofSupports);
  }
  array_free(roots);
}

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

  PureSatBmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited);
  st_free_table(visited);
  return;
}


void
PureSatGetFormulaNodes(
  Ntk_Network_t *network,
  Ctlsp_Formula_t *F,
  array_t *formulaNodes)
{

  if (F == NIL(Ctlsp_Formula_t))
    return;

  if (Ctlsp_FormulaReadType(F) == Ctlsp_ID_c) {
    char *nodeNameString = Ctlsp_FormulaReadVariableName(F);
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
    assert(node);
    array_insert_last(Ntk_Node_t *, formulaNodes, node);
    return;
  }

  PureSatGetFormulaNodes(network, Ctlsp_FormulaReadRightChild(F), formulaNodes);
  PureSatGetFormulaNodes(network, Ctlsp_FormulaReadLeftChild(F),  formulaNodes);
}



void
PureSatGetFaninLatches(
  Ntk_Node_t *node,
  st_table *visited,
  st_table *vertexTable)
{
  if (st_is_member(visited, node))
    return;

  st_insert(visited, node, (char *)0);

  if (Ntk_NodeTestIsLatch(node))
    st_insert(vertexTable, Ntk_NodeReadName(node), (char *)0);
  else {
    int i;
    Ntk_Node_t *fanin;
    Ntk_NodeForEachFanin(node, i, fanin) {
      PureSatGetFaninLatches(fanin, visited, vertexTable);
    }
  }
}
st_table *
PureSatCreateInitialAbstraction(
  Ntk_Network_t *network,
  Ctlsp_Formula_t *invFormula,
  int * Num,
  PureSat_Manager_t *pm)
{
  array_t *formulaNodes = array_alloc(Ntk_Node_t *, 0);
  Ntk_Node_t *node;
  int i;

  st_table *vertexTable = st_init_table(strcmp, st_strhash);
  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
  *Num=0;

  PureSatGetFormulaNodes(network, invFormula, formulaNodes);
  arrayForEachItem(Ntk_Node_t *, formulaNodes, i, node) {
    PureSatGetFaninLatches(node, visited, vertexTable);
  }

  st_free_table(visited);
  array_free(formulaNodes);

  if (1) {
    st_generator *stgen;
    char *nodeNameString;

    if(pm->verbosity>=1)
      fprintf(vis_stdout, "\n Create_InitialAbstraction() =\n");
    st_foreach_item(vertexTable, stgen, &nodeNameString, 0) {
      if(pm->verbosity>=1)
        fprintf(vis_stdout, "%s\n", nodeNameString);
      (*Num)++;
    }
    if(pm->verbosity>=1){
      fprintf(vis_stdout, "\n");
      fflush(vis_stdout);
    }
  }


  return vertexTable;
}


void
PureSatRecursivelyComputeTableForLatch(Ntk_Network_t * network,
                                       st_table *Table,
                                       Ntk_Node_t * node)
{
  int i;
  Ntk_Node_t * fanin;

  //want input to be in the Table
  if(Ntk_NodeTestIsLatch(node))
    return;

  if(!st_lookup(Table,node,NIL(char *)))
    st_insert(Table,node, (char *)0);
  else
    return;

   if ( Ntk_NodeTestIsCombInput(node)) {
        return;
  }

  Ntk_NodeForEachFanin( node,i,fanin)
   PureSatRecursivelyComputeTableForLatch(network,Table,fanin);
}


/* put all the gates of Abs model to the Table */
void
PureSatComputeTableForLatch(Ntk_Network_t * network,
                            st_table * Table,
                            Ntk_Node_t * Latch)
{
  Ntk_Node_t * fanin;
  int i;

  if(!Ntk_NodeTestIsLatch(Latch))
    {
      char * name = Ntk_NodeReadName(Latch);
      fprintf(vis_stdout,"%s is not a latch!\n",name);
      exit (0);
    }

  if(!st_lookup(Table,Latch,NIL(char *)))
    {
      st_insert(Table,Latch, (char *)0);
      Ntk_NodeForEachFanin(Latch,i,fanin)
        PureSatRecursivelyComputeTableForLatch(network,Table,fanin);
    }
}


void
PureSatGetCoiForVisibleArray_Ring(
  Ntk_Network_t   *network,
  array_t *visibleArray,
  int             position,
  st_table        *ltlCoiTable)
{
  int i;
  char * name;
  Ntk_Node_t * node;

  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);


  for(i=position;i<array_n(visibleArray);i++){
    name = array_fetch(char *,visibleArray,i);
    node = Ntk_NetworkFindNodeByName(network,name);
    DfsLevel = 0;
    PureSatBmcGetCoiForNtkNode(node,ltlCoiTable, visited);
  }
  st_free_table(visited);
  return;
}


int
NumInConeCompare(int *ptrX,
                 int *ptrY)
{
  int a,b;
  int c,d;
  double e,f;
  a = array_fetch(int,NumInCone,(int)*ptrX);
  b = array_fetch(int,NumInCone,(int)*ptrY);
  c = array_fetch(int,NumInAbs,(int)*ptrX);
  d = array_fetch(int,NumInAbs,(int)*ptrY);
  e = (double)c/(double)a;
  f = (double)d/(double)b;
  if(e > f)
    return -1;
  if( e < f)
    return 1;
  return 0;
}


int
NumInConeCompare_Ring(int *ptrX,
                      int *ptrY)
{
  int a,b;
  double c,d;
  double e,f;
  a = array_fetch(int,DfsArray,(int)*ptrX);
  b = array_fetch(int,DfsArray,(int)*ptrY);
  c = array_fetch(double,RCArray,(int)*ptrX);
  d = array_fetch(double,RCArray,(int)*ptrY);
  e = (double)((a)*1000000)-c;
  f = (double)((b)*1000000)-d;
  if(e > f)
    return 1;
  if( e < f)
    return -1;
  return 0;
}


void PureSatRecursivelyComputeCorrelationforLatch(Ntk_Network_t *network,
                                                  st_table *AbsTable,
                                                  st_table * visited,
                                                  Ntk_Node_t *node,
                                                  int *count)
{
  Ntk_Node_t * fanin;
  int i;

  if(!st_lookup(visited,node,NIL(char *)))
  {
    st_insert(visited,node,(char *)0);
    if(st_lookup(AbsTable,node,NIL(char *)))
      {
        (*count)++;
      }
  }
  else
    return;

  if(Ntk_NodeTestIsCombInput(node))
    return;

  Ntk_NodeForEachFanin(node,i,fanin)
    PureSatRecursivelyComputeCorrelationforLatch(network,AbsTable,visited,fanin,count);
}



int PureSatComputeCorrelationforLatch(Ntk_Network_t * network, st_table *
                              AbsTable, Ntk_Node_t *Latch)
{
  int count =0,i;
  Ntk_Node_t * fanin;

  st_table *visited = st_init_table(st_ptrcmp,st_ptrhash);
  Ntk_NodeForEachFanin(Latch,i,fanin)
    PureSatRecursivelyComputeCorrelationforLatch(network,AbsTable,visited,fanin,&count);
  st_free_table(visited);
  return count*10000;
}

array_t * PureSatGenerateRingFromAbs(Ntk_Network_t *network,
                                    PureSat_Manager_t *pm,
                                    array_t *invisibleArray,
                                    int * NumInSecondLevel)
{
  st_table *CoiTable = pm->CoiTable;
  st_table *supportTable = pm->supportTable;
  st_table *AbsTable= pm->AbsTable;

  array_t * arrayRC = array_alloc(char *,array_n(invisibleArray)),* NumInConeArray = array_alloc(int,0),* NumInAbsArray = array_alloc(int,0);
  array_t * tmpNumInCone = array_alloc(int,0),* tmpNumInAbs = array_alloc(int,0);
  array_t * tmpDfsArray = array_alloc(int,0), *tmpRCArray = array_alloc(double,0);
  array_t * tmpDfsArray1 = array_alloc(int,0), *tmpRCArray1 = array_alloc(double,0);
  int numincone,i,j,dfs;
  char *name;
  double d1;

  (*NumInSecondLevel) = 0;

  for(i=0;i<array_n(invisibleArray);i++)
   {
     int tmp;
     Ntk_Node_t *tmpnode;
     name = array_fetch(char *,invisibleArray,i);
     tmpnode = Ntk_NetworkFindNodeByName(network,name);
     tmp = PureSatComputeCorrelationforLatch(network,AbsTable,tmpnode);
     tmp = tmp/10000;

     if(!st_lookup_int(CoiTable,tmpnode,&dfs)){
       fprintf(vis_stderr,"not in Coitable,  Wrong");
       exit(0);
     }
     if(!st_lookup_int(supportTable,tmpnode, &numincone)){
       fprintf(vis_stderr,"not in supporttable,  Wrong");
       exit(0);
     }
     d1 = (double)tmp/(double)numincone;
     array_insert_last(double,tmpRCArray,d1);
     array_insert_last(int,tmpDfsArray,dfs);

   }


  DfsArray = tmpDfsArray;
  RCArray = tmpRCArray;
   {
     int tmpvalue;
     double dvalue;
     int nn = array_n(invisibleArray);
     int *tay=ALLOC(int,nn);
     for(j=0;j<nn;j++)
       tay[j]=j;
     qsort((void *)tay, nn, sizeof(int),
           (int (*)(const void *, const void *))NumInConeCompare_Ring);
     for(i=0;i<nn;i++)
       {
         char *str=ALLOC(char,100);
         name = array_fetch(char *,invisibleArray,tay[i]);
         strcpy(str,name);
         array_insert(char *,arrayRC,i,str);
         tmpvalue = array_fetch(int,tmpDfsArray,tay[i]);
         if(tmpvalue == 2)
           (*NumInSecondLevel)++;
         array_insert(int,tmpDfsArray1,i,tmpvalue);
         dvalue = array_fetch(double,tmpRCArray,tay[i]);
         array_insert(double,tmpRCArray1,i,dvalue);
         if(pm->verbosity>=2){
           int i1;
           double d1,d2;
           i1 = array_fetch(int,tmpDfsArray1,i)*1000000;
           d1 = array_fetch(double,tmpRCArray1,i);
           d2 = (double)array_fetch(int,tmpDfsArray1,i)*1000000 - d1;
           if(pm->verbosity>=1)
             fprintf(vis_stdout,"arrayRC %s: %d-%f = %f\n",name,i1,d1,d2);
           /* fprintf(vis_stdout,"arrayRC %s: %d-%f = %f\n",name,array_fetch(int,tmpDfsArray1,i)*1000000,array_fetch(double,tmpRCArray1,i),
              (double)array_fetch(int,tmpDfsArray1,i)*1000000-(double)array_fetch(double,tmpRCArray1,i));*/
         }
       }
     FREE(tay);
   }
   array_free(NumInConeArray);
   array_free(NumInAbsArray);
   array_free(tmpNumInCone);
   array_free(tmpNumInAbs);
   array_free(tmpDfsArray);
   array_free(tmpRCArray);
   array_free(tmpDfsArray1);
   array_free(tmpRCArray1);
   return arrayRC;
}

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

  cm->nodesArraySize = satNodeSize;
  sat_ArrayFree(cm->unitLits);
  sat_ArrayFree(cm->pureLits);
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  memset(cm->each,0,sizeof(satStatistics_t));
  cm->literals->last = cm->literals->begin+1;
  cm->literals->initialSize = cm->literals->last;
  cm->status = 0;
  cm->currentVarPos = 0;
  cm->currentTopConflict = 0;
  cm->lowestBacktrackLevel = 0;
  cm->implicatedSoFar = 0;
  /*cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);*/
  memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
  /* FREE(cm->variableArray);
  cm->variableArray = 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->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;
  }

  sat_FreeQueue(cm->queue);
  cm->queue = 0;
  sat_FreeQueue(cm->BDDQueue);
  cm->BDDQueue = 0;
  sat_FreeQueue(cm->unusedAigQueue);
  cm->unusedAigQueue = 0;
  sat_ArrayFree(cm->auxArray);
  sat_ArrayFree(cm->nonobjUnitLitArray);
  sat_ArrayFree(cm->objUnitLitArray);

}

void PureSatReadClauses(PureSat_IncreSATManager_t * pism,
                        PureSat_Manager_t * pm)
{
  int i,node,nVar = pism->cnfClauses->cnfGlobalIndex - 1;
  satManager_t * cm = pism->cm;
  satArray_t * clauseArray;

  cm->option->verbose = pm->verbosity;
  cm->initNumVariables = nVar;
  cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
  memset(cm->variableArray, 0, sizeof(satVariable_t) *
         (cm->initNumVariables+1));
  if(cm->maxNodesArraySize <= (cm->initNumVariables+2)*satNodeSize){
    cm->nodesArray = ALLOC(long, (cm->initNumVariables+2)*satNodeSize);
    cm->maxNodesArraySize = (cm->initNumVariables+2)*satNodeSize;
  }


  if(pism->cm->option->coreGeneration){
    pism->cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);

    /*the tables stroes entry of (var_node_idx,cls_idx);*/
    pism->cm->anteTable = st_init_table(st_numcmp, st_numhash);

  }
  sat_AllocLiteralsDB(cm);

  for(i=1;i<=nVar;i++){
    node = sat_CreateNode(cm,2,2);
    SATflags(node) |= CoiMask;
    SATvalue(node) = 2;
    /*SATfanout(node) = 0;*/
    cm->nodesArray[node+satFanout] = 0;
    SATnFanout(node) = 0;
  }

  clauseArray = sat_ArrayAlloc(4096);
  for(i=0; i<pism->cnfClauses->nextIndex;i++){
    int k, cls_idx,v;
    k = array_fetch(int,pism->cnfClauses->clauseArray,i);
    if(k!=0){
      int sign = 1;
      if(k<0){
        sign = 0;
        k = -k;
      }
      v = k*satNodeSize + sign;
      sat_ArrayInsert(clauseArray, v);
    }
    else{
      if(clauseArray->num == 1) {
        v = clauseArray->space[0];
        sat_ArrayInsert(cm->unitLits, SATnot(v));
        cls_idx = sat_AddUnitClause(cm, clauseArray);
        if(pism->cm->option->coreGeneration){
          v = SATnormalNode(v);
          st_insert(pism->cm->anteTable,(char *)(long)v,(char *)(long)cls_idx);
        }
      }
      else{
        cls_idx = sat_AddClause(cm, clauseArray);
      }
      cm->initNumClauses++;
      cm->initNumLiterals += clauseArray->num;
      if(i>pism->propertyPos)
        SATflags(cls_idx) |= ObjMask;
      clauseArray->num = 0;
    }
  }
  sat_ArrayFree(clauseArray);

}

array_t * PureSatGetImmediateSupportLatches(
  Ntk_Network_t *network,
  int            beginPosition,
  array_t       *latchNameArray)
{
  /* old support, form 0 to 'beginPosition'-1*/
  array_t    *dataInputs, *supports;
  /* new support, from 'beginPosition' to array_n(latchNameArray)-1*/
  array_t    *dataInputs2, *supports2, *supportLatches2;
  /* The result should be {new support}-{old support}*/
  st_table   *oldSupportTable;
  Ntk_Node_t *latch, *dataInput;
  int        i;
  char       *latchName;

  dataInputs = array_alloc(Ntk_Node_t *, 0);
  dataInputs2 = array_alloc(Ntk_Node_t *, 0);
  arrayForEachItem(char *, latchNameArray, i, latchName) {
    latch = Ntk_NetworkFindNodeByName(network, latchName);
    assert(latch);
    assert(Ntk_NodeTestIsLatch(latch));
    dataInput = Ntk_LatchReadDataInput(latch);
    if (i < beginPosition)
      array_insert_last(Ntk_Node_t *, dataInputs, dataInput);
    else
      array_insert_last(Ntk_Node_t *, dataInputs2, dataInput);
  }

  supports = Ntk_NodeComputeCombinationalSupport(network, dataInputs, 1);
  supports2 = Ntk_NodeComputeCombinationalSupport(network, dataInputs2, 1);
  array_free(dataInputs);
  array_free(dataInputs2);

  oldSupportTable = st_init_table(st_ptrcmp, st_ptrhash);
  arrayForEachItem(Ntk_Node_t *, supports, i, latch) {
    st_insert(oldSupportTable, latch, NIL(char));
  }
  array_free(supports);

  supportLatches2 = array_alloc(char *, 0);
  arrayForEachItem(Ntk_Node_t *,  supports2, i, latch) {
    if (Ntk_NodeTestIsLatch(latch) &&
        !st_is_member(oldSupportTable,latch))
      array_insert_last(char *, supportLatches2, Ntk_NodeReadName(latch));
  }
  array_free(supports2);

  arrayForEachItem(char *, latchNameArray, i, latchName) {
    if (i < beginPosition) continue;
    latch = Ntk_NetworkFindNodeByName(network, latchName);
    if (!st_is_member(oldSupportTable, latch))
      array_insert_last(char *, supportLatches2, latchName);
  }
  st_free_table(oldSupportTable);

  return supportLatches2;
}


void PureSatWriteClausesToFile(PureSat_IncreSATManager_t * pism,
                               mAig_Manager_t  *maigManager,
                               char *coreFile)
{

  BmcCnfClauses_t *cnfClauses = pism->cnfClauses;
  st_generator *stGen;
  char         *name;
  int          cnfIndex, i, k;
  FILE *cnfFile;

  coreFile = BmcCreateTmpFile();
  cnfFile = fopen(coreFile,"w");

  fprintf(vis_stdout, "coreFile is %s\n", coreFile);
  fprintf(vis_stdout,
          "Number of Variables = %d Number of Clauses = %d\n",
          cnfClauses->cnfGlobalIndex-1,  cnfClauses->noOfClauses);


  st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
    fprintf(cnfFile, "c %s %d\n",name, cnfIndex);
  }
  (void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
                 cnfClauses->noOfClauses);
  if (cnfClauses->clauseArray != NIL(array_t)) {
    for (i = 0; i < cnfClauses->nextIndex; i++) {
      k = array_fetch(int, cnfClauses->clauseArray, i);
      (void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' ');
    }
  }
  fclose(cnfFile);
  FREE(coreFile);
  return;
}


void PureSatWriteAllClausesToFile(PureSat_IncreSATManager_t * pism,
                                  char *coreFile)
{
  satManager_t *cm = pism->cm;
  char *tmpallcnfFile = BmcCreateTmpFile();
  FILE *fp1 = fopen(coreFile,"r");
  FILE *fp2 = fopen(tmpallcnfFile,"w");
  char buffer[1024], buffer1[1024];
  long *space;
  int i, numOfConCls=0, numOfVar, sign,var;
  satArray_t *saved = cm->savedConflictClauses;

  for(i=0, space=saved->space; i<saved->num; i++,space++){
    if(*space<0)
      numOfConCls++;
  }
  if(numOfConCls%2!=0){
    fprintf(vis_stdout,"should be times of 2\n");
    exit(0);
  }
  numOfConCls/=2;

  numOfConCls += cm->initNumClauses;
  numOfVar = cm->initNumVariables;
  i=0;
  /*sprintf(buffer,"p cnf %d %d 0\n", numOfConCls, numOfVar);
    fputs(buffer, fp2);*/
  while(fgets(buffer,1024,fp1)){
    if(strncmp(buffer,"c ",2)!=0){
      if(strncmp(buffer,"p cnf ",6)==0){
        sprintf(buffer1,"p cnf %d %d 0\n", numOfVar, numOfConCls);
        fputs(buffer1, fp2);
      }
      else
        fputs(buffer, fp2);
    }
  }

  saved = cm->savedConflictClauses;

  for(i=0, space=saved->space; i<saved->num; i++){
    if(*space<0){
      space++;
      i++;
      while(*space>0){
        sign = !SATisInverted(*space);
        var = SATnormalNode(*space);
        if(sign == 0)
          var = -var;
        fprintf(fp2,"%d ",var);
        space++;
        i++;
      }
      fprintf(fp2,"0\n");
      space++;
      i++;
    }
  }
  fclose(fp1);
  fclose(fp2);
  FREE(tmpallcnfFile);
}



array_t * PureSatGetLatchFromTable(Ntk_Network_t *network,
                                  PureSat_Manager_t * pm,
                                  char *coreFile)
{
  FILE *fp;
  char buffer[1024],*nodeName;
  int idx;
  st_table * localTable = st_init_table(strcmp,st_strhash);
  array_t * refinement = array_alloc(char *,0);
  st_table *ClsidxToLatchTable = pm->ClsidxToLatchTable;
  st_table *vertexTable = pm->vertexTable;

  fp = fopen(coreFile,"r");
  while(fgets(buffer,1024,fp)){
    if(strncmp(buffer,"#clause index:",14)==0){
      sscanf(buffer,"#clause index:%d\n",&idx);
      if(st_lookup(ClsidxToLatchTable,(char *)(long)idx,&nodeName))
        if(!st_lookup(vertexTable,nodeName,NIL(char *))&&!st_lookup(localTable,nodeName,NIL(char *)))
          {
            st_insert(localTable,nodeName,(char *)0);
            array_insert_last(char *,refinement,nodeName);
          }
    }
  }
  st_free_table(localTable);
  return refinement;
}



array_t * PureSatRemove_char(array_t * array1, int i)
{
  int j;
  char * str;
  array_t * array2=array_alloc(char *,0);
  assert(i<array_n(array1));
  arrayForEachItem(char *,array1,j,str)
    {
      if(j!=i)
        {

          array_insert_last(char *,array2,str);
        }
    }
      return array2;
}


void PureSatComputeNumGatesInAbsForNode(Ntk_Network_t * network,
                                        PureSat_Manager_t * pm,
                                        Ntk_Node_t * node,
                                        st_table * visited,
                                        int  * ct,
                                        int  * ct1)
{
  int i;
  Ntk_Node_t *fanin;


  st_insert(visited,node,(char *)0);

  (*ct1)++;
  if(st_lookup(pm->AbsTable,node,NIL(char*)))
    (*ct)++;

  if(Ntk_NodeTestIsCombInput(node))
    return;

  Ntk_NodeForEachFanin(node,i,fanin){
    if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
        !Ntk_NodeTestIsLatch(fanin))
      PureSatComputeNumGatesInAbsForNode(network,pm,fanin,visited,ct,ct1);
  }
  return;

}


void PureSatComputeNumGatesInAbs(Ntk_Network_t *network,
                                PureSat_Manager_t *pm,
                                array_t * invisibleArray)
{
  int i,ct,ct1,j;
  char * name;
  Ntk_Node_t * node,*fanin;
  st_table * visited;


  arrayForEachItem(char*,invisibleArray,i,name){
    node = Ntk_NetworkFindNodeByName(network,name);
    ct = 0;
    ct1 = 0;
    visited = st_init_table(st_ptrcmp,st_ptrhash);
    st_insert(visited,node,(char *)0);

    ct1++;

    Ntk_NodeForEachFanin(node,j,fanin){
      if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
         !Ntk_NodeTestIsLatch(fanin))
        PureSatComputeNumGatesInAbsForNode(network,pm,
                                      fanin,visited,&ct,&ct1);
    }
    st_insert(pm->niaTable,name,(char*)(long)ct);

    st_free_table(visited);
  }
  return;

}


void PureSatComputeNumGatesInConeForNode(Ntk_Network_t * network,
                                       PureSat_Manager_t * pm,
                                       Ntk_Node_t * node,
                                       st_table * visited,
                                       int  * ct)
{
  int i;
  Ntk_Node_t *fanin;


  st_insert(visited,node,(char *)0);

  (*ct)++;

  if(Ntk_NodeTestIsCombInput(node))
    return;

  Ntk_NodeForEachFanin(node,i,fanin){
    if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
       !Ntk_NodeTestIsLatch(fanin))
      PureSatComputeNumGatesInConeForNode(network,pm,fanin,visited,ct);
  }
  return;

}


void PureSatComputeNumGatesInCone(Ntk_Network_t *network,
                                PureSat_Manager_t *pm,
                                array_t * latchArray)
{
  int i,ct,j;
  char * name;
  Ntk_Node_t * node,* fanin;
  st_table * visited;


  arrayForEachItem(char*,latchArray,i,name){
    node = Ntk_NetworkFindNodeByName(network,name);
    ct = 0;
    visited = st_init_table(st_ptrcmp,st_ptrhash);
    st_insert(visited,node,(char *)0);
    ct++;

    Ntk_NodeForEachFanin(node,j,fanin){
      if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
         !Ntk_NodeTestIsLatch(fanin))
        PureSatComputeNumGatesInConeForNode(network,pm
                                            ,fanin,visited,&ct);
    }
    st_insert(pm->nicTable,name,(char*)(long)ct);

    st_free_table(visited);
  }
  return;

}


array_t * PureSatGenerateRCArray_2(Ntk_Network_t *network,
                                   PureSat_Manager_t *pm,
                                   array_t *invisibleArray,
                                   int *NumInSecondLevel)
{
  array_t * tmpRCArray = array_alloc(double,0);
  array_t * tmpDfsArray = array_alloc(int,0);
  array_t * arrayRC = array_alloc(char*,array_n(invisibleArray));
  int i,j;
  char * name;

  if(pm->RefPredict)
    pm->latchArray = array_alloc(char *,0);

  PureSatComputeNumGatesInAbs(network,pm,invisibleArray);

  for(i=0;i<array_n(invisibleArray);i++){
    int nic,nia,dfs;
    Ntk_Node_t *tmpnode;
    int retVal;
    name = array_fetch(char *,invisibleArray,i);
    tmpnode = Ntk_NetworkFindNodeByName(network,name);
    retVal = st_lookup(pm->node2dfsTable,name,&dfs);
    assert(retVal);
    array_insert_last(int,tmpDfsArray,dfs);
    retVal = st_lookup(pm->nicTable,name,&nic);
    assert(retVal);
    retVal = st_lookup(pm->niaTable,name,&nia);
    assert(retVal);
    array_insert_last(double,tmpRCArray,
                      (double)nia/(double)nic);
  }


  DfsArray = tmpDfsArray;
  RCArray = tmpRCArray;
  *NumInSecondLevel = 0;

   {
     int tmpvalue;
     double rcvalue;
     int nn = array_n(invisibleArray);
     int *tay=ALLOC(int,nn);
     for(j=0;j<nn;j++)
       tay[j]=j;
     qsort((void *)tay, nn, sizeof(int),
           (int (*)(const void *, const void *))NumInConeCompare_Ring);
     for(i=0;i<nn;i++)
       {
         name = array_fetch(char *,invisibleArray,tay[i]);
         array_insert(char *,arrayRC,i,name);
         tmpvalue = array_fetch(int,tmpDfsArray,tay[i]);
         if(tmpvalue == 2)
           (*NumInSecondLevel)++;
         rcvalue = array_fetch(double,tmpRCArray,tay[i]);
         if(pm->verbosity>=1)
           fprintf(vis_stdout,"arrayRC %s: %f-%f = %f\n",name,
                   (double)tmpvalue*1000000,rcvalue,(double)tmpvalue*1000000-rcvalue);

         if(pm->RefPredict){
           if(rcvalue>=0.87&&tmpvalue==2){
             array_insert_last(char*,pm->latchArray,name);
             if(pm->verbosity>=1)
               fprintf(vis_stdout,"add %s into pm->latchArray\n",name);
           }
         }

       }
     FREE(tay);
   }

   array_free(DfsArray);
   array_free(RCArray);

   return arrayRC;
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/