source: vis_dev/vis-2.3/src/grab/grabUtil.c @ 23

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

  FileName    [grabUtil.c]

  PackageName [grab]

  Synopsis    [The utility functions for abstraction refinement.]

  Description [This file contains the functions to check invariant
  properties by the GRAB abstraction refinement algorithm. GRAB stands
  for "Generational Refinement of Ariadne's Bundle," in which the
  automatic refinement is guided by all shortest abstract
  counter-examples. For more information, please check the ICCAD'03
  paper of Wang et al., "Improving Ariadne's Bundle by Following
  Multiple Counter-Examples in Abstraction Refinement." ]
  
  Author      [Chao Wang]

  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 "grabInt.h"

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

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

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

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

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

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

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

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

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

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

  Synopsis    [Compute the Cone-Of-Influence abstract model.]

  Description [Compute the Cone-Of-Influence abstraction, which
  consists of latches in the transitive supprot of the property.]

  SideEffects []

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

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

  Synopsis    [Compute the initial abstract model.]

  Description [Compute the he initial abstraction, which consists of
  latches in the immediate supprot of the property.]

  SideEffects []

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

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

  Synopsis    [Build or update partition for the current abstract model.]

  Description [Build or update partition for the current abstract
  model. It is a two-phase process, in which the first phase generated
  the Bnvs---intermediate variables that should be created; while the
  second phase actually create the BDDs. 

  When a non-empty hash table 'absBnvTable' is given, BNVs not in this
  table should be treated as inputs---they should not appear in the
  partition either.

  When 'absBnvTable' is not provided (e.g. when fine-grain abstraction
  is disabled), all relevant BNVs should appear in the partition.]

  SideEffects []

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

}

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

  Synopsis    [Create the abstract FSM.]

  Description [Create the abstract FSM. Table 'coiBnvTable' contains
  all the BNVs (i.e. intermediate variables), while Table
  'absBnvTable' contains all the visible BNVs. BNVs not in absBnvTable
  should be treated as inputs.

  When absBnvTable is NULL (e.g. fine-grain abstraction is disabled),
  no BNV is treated as input.

  If independentFlag is TRUE, invisible latches are regarded as
  inputs; otherwise, they are regarded as latches.]

  SideEffects []

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

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

  Synopsis [Computes the set of initial states of set of latches.]

  Description [Computes the set of initial states of a set of latches.
  The nodes driving the initial inputs of the latches, called the
  initial nodes, must not have latches in their support.  If an
  initial node is found that has a latch in its transitive fanin, then
  a NULL MDD is returned, and a message is written to the
  error_string.<p>
  
  The initial states are computed as follows. For each latch i, the relation
  (x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
  and g_i(u) is the multi-valued initialization function of latch i, in terms
  of the input variables u.  These relations are then conjuncted, and the
  input variables are existentially quantified from the result
  (i.e. init_states(x) = \exists u \[\prod (x_i = g_i(u))\]).]

  SideEffects [The result of the initial state computation is stored with
  the FSM.]

  SeeAlso [Fsm_FsmComputeReachableStates]
  
******************************************************************************/
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);
}

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

  Synopsis [Compute the reachable states of the abstract model.]

  Description [Compute the reachable states of the abstract model.]
  
  SideEffects []

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

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

  Synopsis [Compute the reachable states inside the SORs.]

  Description [Compute the reachable states inside the SORs.]
  
  SideEffects []

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

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

  Synopsis [Compute the Synchronous Onion Rings (SORs).]

  Description [Compute the Synchronous Onion Rings (SORs) with
  backward reachability analysis. The SORs capture all the shortest
  counter-examples to an invariant property. If the forward
  reachability onion rings is not provided (as oldRings), it will be
  retrived from absFsm.

  cexType controls the type of the counter-example envelope:
      GRAB_CEX_MINTERM, a single-state path,
      GRAB_CEX_CUBE, a cube-states path,
      GRAB_CEX_SOR, the SORs.
  ]
  
  SideEffects []

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

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

  Synopsis    [Get the visible variable mddIds of the current abstraction.]

  Description [Get the visible variable mddIds of the current
  abstraction. Note that they are the state variables.]

  SideEffects []

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


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

  Synopsis    [Get the invisible variable mddIds of the current abstraction.]

  Description [Get the invisible variable mddIds of the current
  abstraction. Note that they include both state variables and boolean
  network variables.]

  SideEffects []

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

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

  Synopsis    [Test whether the refinement set of latches is sufficient.]

  Description [Test whether the refinement set of latches is sufficient.]

  SideEffects []

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

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

  Synopsis    [Test whether the refinement set of BNVs is sufficient.]

  Description [Test whether the refinement set of BNVs is sufficient.]

  SideEffects []

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

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

  Synopsis    [Minimize the refinement set of latch variable.]

  Description [Minimize the refinement set of latch variable. After
  that, also prune away the boolean network variables that are no
  longer in the transitive fan-in.]

  SideEffects []

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


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

  Synopsis    [Minimize the refinement set of latch variable.]

  Description [Minimize the refinement set of latch variable. After
  that, also prune away the boolean network variables that are no
  longer in the transitive fan-in.]

  SideEffects []

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

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

  Synopsis    [Clear the fields of mddId for all network nodes.]

  Description [Clear the fields of mddId for all network nodes.]

  SideEffects []

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

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

  Synopsis    [Print an array of network nodes.]

  Description [Print an array of network nodes.]
  
  SideEffects []

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

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

  Synopsis    [Print an array of network nodes.]

  Description [Print an array of network nodes.]
  
  SideEffects []

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

}

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

  Synopsis    [Print a list of network nodes.]

  Description [Print a list of network nodes.]
  
  SideEffects []

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

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

  Synopsis    [Print a hash table of network nodes.]

  Description [Print a hash table of network nodes.]
  
  SideEffects []

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

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

  Synopsis    [Get network nodes that are mentioned by the formula.]

  Description [Get network nodes that are mentioned by the formula.]

  SideEffects []

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


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

  Synopsis    [Get the fan-in latches of those already in the table.]

  Description [Get the fan-in latches of those already in the table.]

  SideEffects []

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

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

  Synopsis [Add nodes for wires referred to in formula to nodesTable.]

  SideEffects []

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