source: vis_dev/vis-2.3/src/puresat/puresatUtil.c @ 36

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

  FileName    [puresatUtil.c]

  PackageName [puresat]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [This file contains the functions to check invariant properties
  by the PureSAT abstraction refinement algorithm, which is entirely based on
  SAT solver, the input of which could be either CNF or AIG. It has several
  parts:

  * Localization-reduction base Abstraction
  * K-induction or interpolation to prove the truth of a property
  * Bounded Model Checking to find bugs
  * Incremental concretization based methods to verify abstract bugs
  * Incremental SAT solver to improve efficiency
  * UNSAT proof based method to obtain refinement
  * AROSAT to bring in only necessary latches into unsat proofs
  * Bridge abstraction to get compact coarse refinement
  * Refinement minization to guarrantee minimal refinements
  * Unsat proof-based refinement minimization to eliminate multiple candidate
    by on SAT test
  * Refinement prediction to decrease the number of refinement iterations
  * Dynamic switching to redistribute computional resources to improve
    efficiency

  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure", "Efficient computation
  of small abstraction refinements", and "Efficient abstraction refinement in
  interpolation-based unbounded model checking"]

  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without
  license or royalty fees, to use, copy, modify, and distribute this
  software and its documentation for any purpose, provided that the
  above copyright notice and the following two paragraphs appear in
  all copies of this software.]

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

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

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

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

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

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

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

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

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


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

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


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


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

  Synopsis    [time out function]

  Description [time out function]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Allocate a puresat manager]

  Description [Allocate a puresat manager]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Free a puresat manager]

  Description [Free a puresat manager]

  SideEffects []

  SeeAlso     []

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

}

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

  Synopsis    [Allocate a puresat incremental SAT manager]

  Description [Allocate a puresat incremental SAT manager]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Free a puresat incremental SAT manager]

  Description [Free a puresat incremental SAT manager]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Get the cone of influence for a network node]

  Description [Get the cone of influence for a network node]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Get the cone of influence for a ltl formula]

  Description [Get the cone of influence for a ltl formula]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Get the color of a node]

  Description [Get the color of a node]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Set the color of a node]

  Description [Set the color of a node]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Recursively compute the transitive fan in nodes of a node]

  Description [Recursively compute the transitive fan in nodes of a node]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Get the number of combination support of a node]

  Description [Get the number of combination support of a node]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Build a support table,each value associated with a latch is the
               number of gates in its cone of influence ]

  Description [Build a support table,each value associated with a latch is the
               number of gates in its cone of influence ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Compute the cone of influence for a ltl formula]

  Description [Compute the cone of influence for a ltl formula]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    []

  Description [recursively compute the nodes in a ltl formula and put them in
               an array]

  SideEffects []

  SeeAlso     []

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

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



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

  Synopsis    [Get direct fan in latches for a node]

  Description [Get direct fan in latches for a node]

  SideEffects []

  SeeAlso     []

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

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);
    }
  }
}
/**Function********************************************************************

  Synopsis    [Build a vertex table which stores all the latches in the
  beginning abstract model]

  Description [The table contains only those immediate fanin latches of the
  given formula.]

  SideEffects []

  SeeAlso     []
******************************************************************************/

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


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

  Synopsis    [Recursively get direct fan in gates of a node]

  Description [Recursively get direct fan in gates of a node]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Get direct fan in gates of a node]

  Description [Get direct fan in gates of a node]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [Take latches in visibleArray as the first level
  compute the DFS level of each latch in ltlCoiTable]

  Description [Take latches in visibleArray as the first level
  compute the DFS level of each latch in ltlCoiTable]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Compare function for quick sort]

  Description [Compare function for quick sort]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Compare function for quick sort]

  Description [Compare function for quick sort]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Recursively compute the relative correlation of a latch.
  For more information of Relative Correlation, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  Description [Recursively compute the relative correlation of a latch.
  For more information of Relative Correlation, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  SideEffects []

  SeeAlso     []

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

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



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

  Synopsis    [Compute the relative correlation of a latch.
  For more information of Relative Correlation, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  Description [Compute the relative correlation of a latch.
  For more information of Relative Correlation, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Generating the ring information needed for the computation of
  the relative correlation of a latch. For more information of Relative
  Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A
  satisfiability-based appraoch to abstraction refinement in model checking",
  and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure]

  Description [Generating the ring information needed for the computation of
  the relative correlation of a latch. For more information of Relative
  Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A
  satisfiability-based appraoch to abstraction refinement in model checking",
  and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Clean the SAT solver after a SAT solving procedure is done]

  Description [Clean the SAT solver after a SAT solving procedure is done]

  SideEffects []

  SeeAlso     []

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

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

}

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

  Synopsis    [Read clauses from a puresat incremental SAT manager to the
  CirCUs SAT solver]

  Description [Read clauses from a puresat incremental SAT manager to the
  CirCUs SAT solver]

  SideEffects []

  SeeAlso     []

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

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

}

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

  Synopsis    [Get immediate latch supports for latches in latchNameArray]

  Description [Get immediate latch supports for latches in latchNameArray]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Dump out clauses to a file]

  Description [Dump out clauses to a file]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [Dump out all the clauses, including conflict clauses, to a file]

  Description [Dump out all the clauses, including conflict clauses, to a file]

  SideEffects []

  SeeAlso     []

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

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



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

  Synopsis    [Generate refinement latches from UNSAT proof]

  Description [Generate refinement latches from UNSAT proof]

  SideEffects []

  SeeAlso     []

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

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



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

  Synopsis    [remove the ith member of a certain array]

  Description [remove the ith member of a certain array]

  SideEffects []

  SeeAlso     []

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


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


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

  Synopsis    [For one node: count number of gates and how many of them are already in abstraction]

  Description []

  SideEffects []

  SeeAlso     []

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

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;

}


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

  Synopsis    [For nodes in one array: count number of gates and how many of
  them are already in abstraction]

  Description []

  SideEffects []

  SeeAlso     []

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

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;

}


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

  Synopsis    [For one node: count how many nodes are in its cone]

  Description []

  SideEffects []

  SeeAlso     []

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

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;

}


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

  Synopsis    [For each node in one array: count how many nodes are in its cone]

  Description []

  SideEffects []

  SeeAlso     []

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

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;

}


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

  Synopsis    [Generate latch candidate array based on BFS ring and RC information]

  Description []

  SideEffects []

  SeeAlso     []

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

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                                            */
/*---------------------------------------------------------------------------*/