src/grab/grabUtil.c

Go to the documentation of this file.

#include "grabInt.h"

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

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

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

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

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

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

static void GetFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *F, array_t *formulaNodes);
static void GetFaninLatches(Ntk_Node_t *node, st_table *visited, st_table *absVarTable);
static void NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable);

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

st_table *
GrabComputeCOIAbstraction(
  Ntk_Network_t *network,
  Ctlp_Formula_t *invFormula)
{
  st_table     *formulaNodes;
  array_t      *formulaCombNodes;
  Ntk_Node_t   *node;
  array_t      *nodeArray;
  int          i;
  st_generator *stGen;
  st_table *absVarTable;

  /* find network nodes in the immediate support of the property */
  formulaNodes = st_init_table(st_ptrcmp, st_ptrhash);
  NodeTableAddCtlFormulaNodes(network, invFormula, formulaNodes);

  /* find network nodes in the transitive fan-in */
  nodeArray = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(formulaNodes, stGen,  & node, NIL(char *)) {
    array_insert_last( Ntk_Node_t *, nodeArray, node);
  }
  st_free_table(formulaNodes);
  formulaCombNodes = Ntk_NodeComputeTransitiveFaninNodes(network, nodeArray,
                                                         FALSE, TRUE);
  array_free(nodeArray);

  /* extract all the latches */
  absVarTable = st_init_table(st_ptrcmp, st_ptrhash);
  arrayForEachItem(Ntk_Node_t *, formulaCombNodes, i, node) {
    if (Ntk_NodeTestIsLatch(node) == TRUE) {
      st_insert(absVarTable, node, (char *)0);
    }
  }
  array_free(formulaCombNodes);
  
  return absVarTable;
}

st_table *
GrabComputeInitialAbstraction(
  Ntk_Network_t *network, 
  Ctlp_Formula_t *invFormula)
{
  array_t    *formulaNodes = array_alloc(Ntk_Node_t *, 0);
  Ntk_Node_t *node;
  int        i;
  st_table   *absVarTable, *visited;

  GetFormulaNodes(network, invFormula, formulaNodes);

  absVarTable = st_init_table(st_ptrcmp, st_ptrhash);
  visited = st_init_table(st_ptrcmp, st_ptrhash);
  arrayForEachItem(Ntk_Node_t *, formulaNodes, i, node) {
    GetFaninLatches(node, visited, absVarTable);
  }

  st_free_table(visited);
  array_free(formulaNodes);
  
  return absVarTable;
}

void
GrabUpdateAbstractPartition(
  Ntk_Network_t *network,
  st_table *coiBnvTable,
  st_table *absVarTable,
  st_table *absBnvTable,
  int partitionFlag)
{
  graph_t *newPart;
  st_table *useAbsBnvTable = absBnvTable? absBnvTable:coiBnvTable;
  
  if (partitionFlag == GRAB_PARTITION_BUILD) {

    /* free the existing partition */
    Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY);

    /* insert bnvs whenever necessary. Note that when the current
     * partition is not available, this function will create new bnvs
     * and put them into the coiBnvTable. Otherwise, it retrieves
     * existing bnvs from the current partiton */
    Part_PartitionReadOrCreateBnvs(network, absVarTable, coiBnvTable);

    /* create the new partition */
    newPart = g_alloc();
    newPart->user_data = (gGeneric)PartPartitionInfoCreate("default",
                                        Ntk_NetworkReadMddManager(network),
                                                           Part_Frontier_c);
    Part_PartitionWithExistingBnvs(network, newPart, coiBnvTable, 
                                   absVarTable, useAbsBnvTable);
    Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
                           (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                           (void *) newPart);

  }else if (partitionFlag == GRAB_PARTITION_UPDATE) {
    fprintf(vis_stdout, 
            "\n ** grab error: GRAB_PARTITION_UPDATE not implemented\n");
    assert(0);
  }

}

Fsm_Fsm_t *
GrabCreateAbstractFsm( 
  Ntk_Network_t *network,
  st_table *coiBnvTable,
  st_table *absVarTable,
  st_table *absBnvTable,
  int partitionFlag,
  int independentFlag)
{
  Fsm_Fsm_t    *fsm;
  array_t *absLatches = array_alloc(Ntk_Node_t *, 0);
  array_t *invisibleVars = array_alloc(Ntk_Node_t *, 0);
  array_t *absInputs = array_alloc(Ntk_Node_t *, 0);
  array_t *rootNodesArray = array_alloc(Ntk_Node_t *, 0);
  st_table *rawLeafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsList topologicalNodeList;
  lsGen  lsgen;
  st_generator *stgen;
  Ntk_Node_t *node;

  GrabUpdateAbstractPartition(network, coiBnvTable, absVarTable, absBnvTable,
                              partitionFlag);

  /* first, compute the absLatches, invisibleVars, and absInputs:
   * absLatches includes all the visible latch variables;
   * invisibleVars includes all the invisible latches variables; 
   * absInputs includes all the primary and pseudo inputs.
   */
  st_foreach_item(absVarTable, stgen, &node, NIL(char *)) {
    array_insert_last(Ntk_Node_t *, absLatches, node);
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadInitialInput(node));
  }
    
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    st_insert(rawLeafNodesTable, node, (char *) (long) (-1) );
  }
  st_foreach_item(coiBnvTable, stgen, &node, NIL(char *)) {
    /* unless it blongs to the current Abstract Model */
    if (absBnvTable && !st_is_member(absBnvTable, node))
      st_insert(rawLeafNodesTable, node, (char *) (long) (-1) );
  }

  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           rawLeafNodesTable);
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(rawLeafNodesTable, node) &&
        !st_is_member(absVarTable, node) ) {
      /*if (Ntk_NodeTestIsLatch(node) || 
        coiBnvTable && st_is_member(coiBnvTable, node))*/
      if (Ntk_NodeTestIsLatch(node) || 
          (coiBnvTable && st_is_member(coiBnvTable, node)))
        array_insert_last(Ntk_Node_t *, invisibleVars, node);
      else
        array_insert_last(Ntk_Node_t *, absInputs, node);
    }
  }
  
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
  st_free_table(rawLeafNodesTable);
  array_free(rootNodesArray);


  /* now, create the abstract Fsm according to the value of
   * independentFlag when independentFlag is TRUE, the present state
   * varaibles are absLatches; otherwise, they contain both absLatches
   * and invisibleVars (with such a FSM, preimages may contain
   * invisible vars in their supports)
   */
  fsm = Fsm_FsmCreateAbstractFsm(network, NIL(graph_t), 
                                 absLatches, invisibleVars, absInputs, 
                                 NIL(array_t), independentFlag);

#if 0
  /* for debugging */
  if (partitionFlag == GRAB_PARTITION_NOCHANGE) {
    GrabPrintNodeArray("absLatches", absLatches);
    GrabPrintNodeArray("invisibleVars", invisibleVars);
    GrabPrintNodeArray("absInputs", absInputs);
  }
#endif

  array_free(invisibleVars);
  array_free(absInputs);
  array_free(absLatches);


  return fsm;
}

mdd_t *
GrabComputeInitialStates(
  Ntk_Network_t *network,
  array_t *psVars)
{
  int            i = 0;
  mdd_t         *initStates;
  Ntk_Node_t    *node;
  array_t       *initRelnArray;
  array_t       *initMvfs;
  array_t       *initNodes;
  array_t       *initVertices;
  array_t       *latchMddIds;
  array_t       *inputVars = array_alloc(int, 0);
  array_t       *combArray;
  st_table      *supportNodes;
  st_table      *supportVertices;
  mdd_manager   *mddManager = Ntk_NetworkReadMddManager(network);
  graph_t       *partition  =
    (graph_t *) Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY);
  int            numLatches;
  Img_MethodType imageMethod;
  
  numLatches = array_n(psVars);

  /* Get the array of initial nodes, both as network nodes and as
   * partition vertices.
   */
  initNodes    = array_alloc(Ntk_Node_t *, numLatches);
  initVertices = array_alloc(vertex_t *, numLatches);
  latchMddIds  = array_alloc(int, numLatches);
  for (i=0; i<numLatches; i++){
    int latchMddId = array_fetch(int, psVars, i);
    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
    vertex_t   *initVertex = Part_PartitionFindVertexByName(partition,
                                Ntk_NodeReadName(initNode));
    array_insert(Ntk_Node_t *, initNodes, i, initNode);
    array_insert(vertex_t *, initVertices, i, initVertex);
    array_insert(int, latchMddIds, i, Ntk_NodeReadMddId(latch));
  }

  /* Get the table of legal support nodes, both as network nodes and
   * as partition vertices. Inputs (both primary and pseudo) and
   * constants constitute the legal support nodes.
   */
  supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
  supportVertices = st_init_table(st_ptrcmp, st_ptrhash);
  combArray = Ntk_NodeComputeTransitiveFaninNodes(network, initNodes, TRUE,
                                                  TRUE);
  arrayForEachItem(Ntk_Node_t *, combArray, i, node) {
    vertex_t *vertex = Part_PartitionFindVertexByName(partition,
                                                      Ntk_NodeReadName(node));
    if (Ntk_NodeTestIsConstant(node) || Ntk_NodeTestIsInput(node)) {
      st_insert(supportNodes,  node, NIL(char));
      st_insert(supportVertices,  vertex, NIL(char));
    }
    if (Ntk_NodeTestIsInput(node)) {
      assert(Ntk_NodeReadMddId(node) != -1);
      array_insert_last(int, inputVars, Ntk_NodeReadMddId(node));
    }
  }
  array_free(combArray);
  array_free(initNodes);
  st_free_table(supportNodes);

  /* Compute the initial states 
   */
  initMvfs = Part_PartitionCollapse(partition, initVertices,
                                    supportVertices, NIL(mdd_t)); 
  array_free(initVertices);
  st_free_table(supportVertices);

  /* Compute the relation (x_i = g_i(u)) for each latch. */
  initRelnArray = array_alloc(mdd_t*, numLatches);
  for (i = 0; i < numLatches; i++) {
    int latchMddId = array_fetch(int, latchMddIds, i);
    Mvf_Function_t *initMvf = array_fetch(Mvf_Function_t *, initMvfs, i);
    mdd_t *initLatchReln = Mvf_FunctionBuildRelationWithVariable(initMvf,
                                                                latchMddId);
    array_insert(mdd_t *, initRelnArray, i, initLatchReln);
  }

  array_free(latchMddIds);
  Mvf_FunctionArrayFree(initMvfs);

  imageMethod = Img_UserSpecifiedMethod();
  if (imageMethod != Img_Iwls95_c && imageMethod != Img_Mlp_c)
    imageMethod = Img_Iwls95_c;

  initStates = Img_MultiwayLinearAndSmooth(mddManager, initRelnArray,
                                           inputVars, psVars,
                                           imageMethod, Img_Forward_c); 
  
  mdd_array_free(initRelnArray); 
  
  array_free(inputVars);
  
  return (initStates);
}

mdd_t *
GrabFsmComputeReachableStates(
  Fsm_Fsm_t *absFsm,
  st_table  *absVarTable,
  st_table  *absBnvTable,
  array_t   *invStatesArray,
  int       verbose)
{
  mdd_manager     *mddManager = Fsm_FsmReadMddManager(absFsm);
  Img_ImageInfo_t *imageInfo;
  array_t         *fwdOnionRings;
  mdd_t           *initStates, *mdd1,  *mddOne, *rchStates, *frontier;
  
  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 0, 1);

  fwdOnionRings = array_alloc(mdd_t *, 0);
  mddOne = mdd_one(mddManager);
  initStates = Fsm_FsmComputeInitialStates(absFsm);
  array_insert_last(mdd_t *, fwdOnionRings, initStates);
  rchStates = mdd_dup(initStates);

  frontier = initStates;
  while(TRUE) {
    mdd1 = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, frontier,
                                                 rchStates, mddOne);
    frontier = mdd_and(mdd1, rchStates, 1, 0);
    mdd_free(mdd1);

    mdd1 = rchStates;
    rchStates = mdd_or(rchStates, frontier, 1, 1);
    mdd_free(mdd1);

    if (mdd_is_tautology(frontier, 0)) {
      mdd_free(frontier);
      break;
    }
    array_insert_last(mdd_t *, fwdOnionRings, frontier);

    /* if this happens, the invariant is voilated */
    if (!mdd_lequal_array(frontier, invStatesArray, 1, 1))
      break;
  }

  mdd_free(mddOne);

  FsmSetReachabilityOnionRings(absFsm, fwdOnionRings);

  return rchStates;
}

mdd_t *
GrabFsmComputeConstrainedReachableStates(
  Fsm_Fsm_t *absFsm,
  st_table *absVarTable,
  st_table *absBnvTable,
  array_t *SORs,
  int verbose)
{
  mdd_manager     *mddManager = Fsm_FsmReadMddManager(absFsm);
  Img_ImageInfo_t *imageInfo;
  array_t         *rchOnionRings;
  mdd_t           *mdd1, *mdd2, *mdd3, *mdd4;
  mdd_t           *mddOne, *initStates, *rchStates;
  int             i;

  assert (SORs != NIL(array_t));

  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 0, 1);

  rchOnionRings = array_alloc(mdd_t *, 0);
  mddOne = mdd_one(mddManager);

  /* the new initial states */
  mdd2 = array_fetch(mdd_t *, SORs, 0);
  mdd1 = Fsm_FsmComputeInitialStates(absFsm);
  initStates = mdd_and(mdd1, mdd2, 1, 1);
  mdd_free(mdd1);
  array_insert(mdd_t *, rchOnionRings, 0, initStates);

  /* compute the reachable states inside the previous SORs */
  rchStates = mdd_dup(initStates);
  for (i=0; i<array_n(SORs)-1; i++) {
    mdd1 = array_fetch(mdd_t *, rchOnionRings, i);
    mdd2 = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
                                                 mdd1,
                                                 rchStates,
                                                 mddOne);

    mdd3 = array_fetch(mdd_t *, SORs, i+1);
    mdd4 = mdd_and(mdd2, mdd3, 1, 1);
    mdd_free(mdd2);

    /* if this happens, the last ring is no longer reachable */
    if (mdd_is_tautology(mdd4, 0)) {
      mdd_free(mdd4);
      break;
    }
    array_insert(mdd_t *, rchOnionRings, i+1, mdd4);

    mdd1 = rchStates;
    rchStates = mdd_or(rchStates, mdd4, 1, 1);
    mdd_free(mdd1);
  }

  mdd_free(mddOne);

  FsmSetReachabilityOnionRings(absFsm, rchOnionRings);

  return rchStates;
}

array_t *
GrabFsmComputeSynchronousOnionRings(
  Fsm_Fsm_t *absFsm,
  st_table  *absVarTable,
  st_table  *absBnvTable,
  array_t   *oldRings,
  mdd_t     *inv_states,
  int       cexType,
  int       verbose)
{
  mdd_manager     *mddManager = Fsm_FsmReadMddManager(absFsm);
  Img_ImageInfo_t *imageInfo;
  array_t         *onionRings, *synOnionRings;
  array_t         *allPSVars;
  mdd_t           *mddOne, *ring;
  mdd_t           *mdd1, *mdd2, *mdd3, *mdd4;
  int             j;

  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 1, 0);

  /* get the forward reachability onion rings */
  onionRings = oldRings;
  if (onionRings == NIL(array_t))
    onionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
  assert(onionRings);

  synOnionRings = array_alloc(mdd_t *, array_n(onionRings));

  mddOne = mdd_one(mddManager);
  allPSVars = Fsm_FsmReadPresentStateVars(absFsm);

  /* the last ring */
  mdd2 = array_fetch_last(mdd_t *, onionRings);
  mdd1 = mdd_and(mdd2, inv_states, 1, 0);
  if (cexType == GRAB_CEX_MINTERM)
    ring = Mc_ComputeAMinterm(mdd1, allPSVars, mddManager);
  else if (cexType == GRAB_CEX_CUBE) {
    array_t *bddIds = mdd_get_bdd_support_ids(mddManager, mdd1);
    int nvars = array_n(bddIds);
    array_free(bddIds);
    ring = bdd_approx_remap_ua(mdd1, (bdd_approx_dir_t)BDD_UNDER_APPROX,
                               nvars, 1024, 1);
    if (ring == NIL(mdd_t)) 
      ring = mdd_dup(mdd1);   
  }else 
    ring = mdd_dup(mdd1);
  mdd_free(mdd1);
  array_insert(mdd_t *, synOnionRings, array_n(onionRings)-1, ring);

  /* the rest rings */
  for (j=array_n(onionRings)-2; j>=0; j--) {
    mdd1 = array_fetch(mdd_t *, synOnionRings, j+1);
    mdd2 = Img_ImageInfoComputeBwdWithDomainVars(imageInfo,
                                                 mdd1,
                                                 mdd1,
                                                 mddOne);

    mdd3 = array_fetch(mdd_t *, onionRings, j);
    mdd4 = mdd_and(mdd2, mdd3, 1, 1);
    mdd_free(mdd2);

    if (cexType == GRAB_CEX_MINTERM) 
      ring = Mc_ComputeAMinterm(mdd4, allPSVars, mddManager);
    else if (cexType == GRAB_CEX_CUBE) {
      array_t *bddIds = mdd_get_bdd_support_ids(mddManager, mdd4);
      int nvars = array_n(bddIds);
      array_free(bddIds);
      ring = bdd_approx_remap_ua(mdd4, (bdd_approx_dir_t)BDD_UNDER_APPROX,
                                 nvars, 1024, 1);
      if (ring == NIL(mdd_t)) 
        ring = mdd_dup(mdd4);   
    }else 
      ring = mdd_dup(mdd4);
    mdd_free(mdd4);
    array_insert(mdd_t *, synOnionRings, j, ring);
  }
  
  mdd_free(mddOne);

  return synOnionRings;
}

array_t *
GrabGetVisibleVarMddIds (
  Fsm_Fsm_t *absFsm,
  st_table *absVarTable)
{
  array_t       *visibleVarMddIds = array_alloc(int, 0);
  st_generator  *stgen;
  Ntk_Node_t    *node;
  int           mddId;

  st_foreach_item(absVarTable, stgen, &node, NIL(char *)) {
    mddId = Ntk_NodeReadMddId(node);
    array_insert_last(int, visibleVarMddIds, mddId);
  }

  return visibleVarMddIds;
}


array_t *
GrabGetInvisibleVarMddIds(
  Fsm_Fsm_t *absFsm,
  st_table *absVarTable,
  st_table *absBnvTable)
{
  Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm);
  array_t       *inputVars = Fsm_FsmReadInputVars(absFsm);
  array_t       *invisibleVarMddIds = array_alloc(int, 0);
  Ntk_Node_t    *node;
  int           i, mddId;

  arrayForEachItem(int, inputVars, i, mddId) {
    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    if ( !Ntk_NodeTestIsInput(node) && 
         !st_is_member(absVarTable, node) ) {
      if (absBnvTable != NIL(st_table)) {
        if (!st_is_member(absBnvTable, node)) {
          array_insert_last(int, invisibleVarMddIds, mddId);
        }
      }else
        array_insert_last(int, invisibleVarMddIds, mddId);
    }
  }

  return invisibleVarMddIds;
}

int
GrabTestRefinementSetSufficient(
  Ntk_Network_t *network,
  array_t *SORs,
  st_table *absVarTable,
  int verbose)
{
  int  is_sufficient;

  is_sufficient = !Bmc_AbstractCheckAbstractTraces(network,
                                                   SORs,
                                                   absVarTable,
                                                   0, 0, 0);
  return is_sufficient;
}

int
GrabTestRefinementBnvSetSufficient(
  Ntk_Network_t   *network,
  st_table        *coiBnvTable,
  array_t         *SORs,
  st_table        *absVarTable,
  st_table        *absBnvTable,
  int             verbose)
{
  int     is_sufficient;
  
  assert(absBnvTable && coiBnvTable);

  is_sufficient = 
    !Bmc_AbstractCheckAbstractTracesWithFineGrain(network,
                                                  coiBnvTable,
                                                  SORs,
                                                  absVarTable,
                                                  absBnvTable);
  return is_sufficient;
}

void
GrabMinimizeLatchRefinementSet(
  Ntk_Network_t *network,
  st_table **absVarTable,
  st_table **absBnvTable,
  array_t *newlyAddedLatches,  
  array_t **newlyAddedBnvs,  
  array_t *SORs,
  int verbose)
{
  st_table      *newVertexTable, *oldBnvTable, *transFaninTable;
  array_t       *rootArray, *transFanins, *oldNewlyAddedBnvs;
  st_generator  *stgen;
  Ntk_Node_t    *node;
  int           i, flag, n_size, mddId;
  
  n_size = array_n(newlyAddedLatches);

  if (verbose >= 3) 
    fprintf(vis_stdout,
            "-- grab: minimize latch refinement set: previous size is %d\n", 
            n_size);

  arrayForEachItem(int, newlyAddedLatches, i, mddId) {
    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    /* first, try to drop it */
    newVertexTable = st_copy(*absVarTable);
    flag = st_delete(newVertexTable, &node, NIL(char *));
    assert(flag);
    /* if the counter-example does not come back, drop it officially */
    flag = Bmc_AbstractCheckAbstractTraces(network,SORs,
                                           newVertexTable, 0, 0, 0);
    if (!flag) {
      st_free_table(*absVarTable);
      *absVarTable = newVertexTable;
      n_size--;
    }else {
      st_free_table(newVertexTable);
      if (verbose >= 3)
        fprintf(vis_stdout,"         add back %s (latch)\n", 
                Ntk_NodeReadName(node));
    }
  }

  if (verbose >= 3)
    fprintf(vis_stdout,
            "-- grab: minimize latch refinement set: current  size is %d\n", 
            n_size);

  /* prune away irrelevant BNVs */
  if (*absBnvTable != NIL(st_table) && st_count(*absBnvTable)>0) {

    rootArray = array_alloc(Ntk_Node_t *, 0);
    st_foreach_item(*absVarTable, stgen, &node, NIL(char *)) {
      array_insert_last(Ntk_Node_t *, rootArray, Ntk_LatchReadDataInput(node));
      array_insert_last(Ntk_Node_t *, rootArray, 
                        Ntk_LatchReadInitialInput(node));
    }
    transFanins = Ntk_NodeComputeTransitiveFaninNodes(network, rootArray,
                                                      TRUE, /*stopAtLatch*/
                                                      FALSE /*combInputsOnly*/
                                                      );
    array_free(rootArray);

    transFaninTable = st_init_table(st_ptrcmp, st_ptrhash);
    arrayForEachItem(Ntk_Node_t *, transFanins, i, node) {
      st_insert(transFaninTable, node, NIL(char));
    }
    array_free(transFanins);
        
    oldBnvTable = *absBnvTable;
    oldNewlyAddedBnvs = *newlyAddedBnvs;
    *absBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
    *newlyAddedBnvs = array_alloc(int, 0);
    st_foreach_item(oldBnvTable, stgen, &node, NIL(char *)) {
      if (st_is_member(transFaninTable, node))
        st_insert(*absBnvTable, node, NIL(char));
    }
    arrayForEachItem(int, oldNewlyAddedBnvs, i, mddId) {
      node = Ntk_NetworkFindNodeByMddId(network, mddId);
      if (st_is_member(transFaninTable, node))
        array_insert_last(int, *newlyAddedBnvs, mddId);
    }
    st_free_table(transFaninTable);

    if (verbose >= 5) {
      st_foreach_item(oldBnvTable, stgen, &node, NIL(char *)) {
        if (!st_is_member(*absBnvTable, node)) 
          fprintf(vis_stdout, "         prune away BNV %s\n", Ntk_NodeReadName(node));
      }
    }
    
    array_free(oldNewlyAddedBnvs);
    st_free_table(oldBnvTable);
  }
  
}


void
GrabMinimizeBnvRefinementSet(
  Ntk_Network_t *network,
  st_table *coiBnvTable,
  st_table *absVarTable,
  st_table **absBnvTable,
  array_t *newlyAddedBnvs,    
  array_t *SORs,
  int verbose)
{
  st_table   *newBnvTable;
  Ntk_Node_t *node;
  int        i, flag, n_size, mddId;
  
  n_size = array_n(newlyAddedBnvs);

  if (verbose >= 3)
    fprintf(vis_stdout,
            "-- grab: minimize bnv refinement set: previous size is %d\n", 
            n_size);

  arrayForEachItem(int, newlyAddedBnvs, i, mddId) {
    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    /* first, try to drop it */
    newBnvTable = st_copy(*absBnvTable);
    flag = st_delete(newBnvTable, &node, NIL(char *));
    assert(flag);
    /* if the counter-example does not come back, drop it officially */
    flag = Bmc_AbstractCheckAbstractTracesWithFineGrain(network,
                                                        coiBnvTable, 
                                                        SORs,
                                                        absVarTable,
                                                        newBnvTable);
    if (!flag) {
      st_free_table(*absBnvTable);
      *absBnvTable = newBnvTable;
      n_size--;
    }else {
      st_free_table(newBnvTable);
      if (verbose >= 3)
        fprintf(vis_stdout,"         add back %s (BNV)\n", 
                Ntk_NodeReadName(node));
    }
  }

  if (verbose >= 3)
    fprintf(vis_stdout,
            "-- grab: minimize bnv refinement set: current  size is %d\n", 
            n_size);
} 

void 
GrabNtkClearAllMddIds(
  Ntk_Network_t *network)
{
#ifndef NDEBUG
  mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
#endif
  Ntk_Node_t *node;
  lsGen lsgen;

  assert(mddManager == NIL(mdd_manager));

  Ntk_NetworkForEachNode(network, lsgen, node) {
    Ntk_NodeSetMddId(node, NTK_UNASSIGNED_MDD_ID);
  }
}

void 
GrabPrintNodeArray(
  char *caption,
  array_t *theArray)
{
  Ntk_Node_t *node;
  char string[32];
  int i;

  fprintf(vis_stdout, "\n%s[%d] =\n", caption, theArray?array_n(theArray):0);

  if (!theArray) return;

  arrayForEachItem(Ntk_Node_t *, theArray, i, node) {
    if (Ntk_NodeTestIsLatch(node))
      strcpy(string, "latch");
    else if (Ntk_NodeTestIsInput(node))
      strcpy(string, "input");
    else if (Ntk_NodeTestIsLatchDataInput(node))
      strcpy(string, "latchDataIn");
    else if (Ntk_NodeTestIsLatchInitialInput(node))
      strcpy(string, "latchInitIn");
    else if (Ntk_NodeTestIsConstant(node))
      strcpy(string, "const");
    else 
      strcpy(string, "BNV");

    fprintf(vis_stdout, "%s\t(%s)\n", Ntk_NodeReadName(node), string);
  }
}

void 
GrabPrintMddIdArray(
  Ntk_Network_t *network,
  char *caption,
  array_t *mddIdArray)
{
  Ntk_Node_t *node;
  array_t *theArray = array_alloc(Ntk_Node_t *, array_n(mddIdArray));
  int i, mddId;

  arrayForEachItem(int, mddIdArray, i, mddId) {
    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    array_insert(Ntk_Node_t *, theArray, i, node);
  }

  GrabPrintNodeArray(caption, theArray);

  array_free(theArray);

}

void 
GrabPrintNodeList(
  char *caption,  
  lsList theList)
{
  Ntk_Node_t *node;
  char string[32];
  lsGen lsgen;

  fprintf(vis_stdout, "\n%s[%d] =\n", caption, theList?lsLength(theList):0);
  
  if (!theList) return;

  lsForEachItem(theList, lsgen, node) {
    if (Ntk_NodeTestIsLatch(node))
      strcpy(string, "latch");
    else if (Ntk_NodeTestIsInput(node))
      strcpy(string, "input");
    else if (Ntk_NodeTestIsLatchDataInput(node))
      strcpy(string, "latchDataIn");
    else if (Ntk_NodeTestIsLatchInitialInput(node))
      strcpy(string, "latchInitIn");
    else if (Ntk_NodeTestIsConstant(node))
      strcpy(string, "const");
    else 
      strcpy(string, "BNV");

    fprintf(vis_stdout, "   %s\t %s\n", string, Ntk_NodeReadName(node));
  }
}

void 
GrabPrintNodeHashTable(
  char *caption,
  st_table *theTable)
{
  Ntk_Node_t *node;
  char string[32];
  long  value;
  st_generator *stgen;

  fprintf(vis_stdout, "\n%s[%d] =\n", caption, theTable?st_count(theTable):0);

  if (!theTable) return;

  st_foreach_item(theTable, stgen, &node, &value) {
    if (Ntk_NodeTestIsLatch(node))
      strcpy(string, "latch");
    else if (Ntk_NodeTestIsInput(node))
      strcpy(string, "input");
    else if (Ntk_NodeTestIsLatchDataInput(node))
      strcpy(string, "latchDataIn");
    else if (Ntk_NodeTestIsLatchInitialInput(node))
      strcpy(string, "latchInitIn");
    else if (Ntk_NodeTestIsConstant(node))
      strcpy(string, "const");
    else 
      strcpy(string, "BNV");

    if (value != 0)
      fprintf(vis_stdout, "   %s\t %s\t %ld\n", string, Ntk_NodeReadName(node),
              value);
    else
      fprintf(vis_stdout, "   %s\t %s \n", string, Ntk_NodeReadName(node));
  }
}

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

static void
GetFormulaNodes(
  Ntk_Network_t *network,
  Ctlp_Formula_t *F,
  array_t *formulaNodes)
{

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

  if (Ctlp_FormulaReadType(F) == Ctlp_ID_c) {
    char *nodeNameString = Ctlp_FormulaReadVariableName(F);
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
    assert(node);
    array_insert_last(Ntk_Node_t *, formulaNodes, node);
    return;
  }
  
  GetFormulaNodes(network, Ctlp_FormulaReadRightChild(F), formulaNodes);
  GetFormulaNodes(network, Ctlp_FormulaReadLeftChild(F),  formulaNodes);
}


static void 
GetFaninLatches(
  Ntk_Node_t *node,
  st_table *visited,
  st_table *absVarTable)
{
  if (st_is_member(visited, node))
    return;

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

  if (Ntk_NodeTestIsLatch(node)) 
    st_insert(absVarTable, node, (char *)0);
  else {
    int i;
    Ntk_Node_t *fanin;
    Ntk_NodeForEachFanin(node, i, fanin) {
      GetFaninLatches(fanin, visited, absVarTable);
    }
  }
}

static void
NodeTableAddCtlFormulaNodes( 
  Ntk_Network_t *network,
  Ctlp_Formula_t *formula, 
  st_table * nodesTable )
{
  if (formula == NIL(Ctlp_Formula_t)) 
    return;

  if ( Ctlp_FormulaReadType( formula ) == Ctlp_ID_c ) {
    char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
    if( node ) 
      st_insert( nodesTable, ( char *) node, NIL(char) );
    return;
  }
  
  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadRightChild( formula ), nodesTable );
  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadLeftChild( formula ), nodesTable );
}