source: vis_dev/vis-2.3/src/part/partFrontier.c

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

  FileName    [partFrontier.c]

  PackageName [part]

  Synopsis [Implements the partition of the network based on the strategy of
  creating a node whenever the size of the BDD representing the functionality
  of the node increases the threshold value.]

  Description [The network is composed of an arbitrary set of nodes each of
  them implementing some simple function.  This method will create a graph such
  that every vertex in that graph represents a node in the network.  Each node 
  in the primary he result
  is a graph with exactly the same topology as the network and such that every
  node has an MddId and a corresponding function.]

  SeeAlso     [part.h]

  Author      [Rajeev K. Ranjan, Chao Wang]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  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.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
******************************************************************************/
#include "partInt.h"

static char rcsid[] UNUSED = "$Id: partFrontier.c,v 1.25 2005/05/11 20:50:32 jinh Exp $";

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


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

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


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

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


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

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

static void PartitionCreateEdges(graph_t *partition);
static Mvf_Function_t * NodeBuildMvf(Ntk_Node_t * node, st_table * nodeToMvfTable);
static Mvf_Function_t * NodeBuildMvf2(Ntk_Node_t * node, st_table * nodeToMvfTable, st_table *faninNumberTable);
static Mvf_Function_t * NodeBuildPseudoInputMvf(Ntk_Node_t * node);
static void PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int indent);

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


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

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

  Synopsis    [Read or create the Boolean network variables (BNVs).]

  Description [Read or create the Boolean network variables. If the
  partition is available, find the BNVs directly inside the
  graph. Otherwise, sweep the network with the Frontier partition
  method, and selectively insert BNVs. In both cases, the BNVs are put
  into the hash table coiBnvTable.]

  SideEffects []

******************************************************************************/
void 
Part_PartitionReadOrCreateBnvs(
  Ntk_Network_t *network,
  st_table *coiLatchTable,
  st_table *coiBnvTable)
{
  graph_t    *partition;
  lsGen      lsgen;
  vertex_t   *vertex;
  long       mddId;
  Ntk_Node_t *node;

  /* if the partition is not available, sweep the network  */
  partition = Part_NetworkReadPartition(network);
  if (partition == NIL(graph_t)) {
    PartInsertBnvs(network, coiLatchTable, coiBnvTable);
    return;
  }

  /* otherwise, go through the vertices */
  foreach_vertex(partition, lsgen, vertex) {
    mddId = PartVertexReadMddId(vertex);
    if (mddId == -1) continue;

    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    assert(node != NIL(Ntk_Node_t));

    if ( !Ntk_NodeTestIsCombInput(node) &&
         Ntk_NodeReadNumFanouts(node)!=0 )
      st_insert(coiBnvTable, (char *)node, NIL(char));
  }
 
}

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

  Synopsis    [Read or create the Boolean network variables (BNVs).]

  Description [Read or create the Boolean network variables. If the
  partition is available, find the BNVs directly inside the
  graph. Otherwise, sweep the network with the Frontier partition
  method, and selectively insert BNVs. In both cases, the BNVs are put
  into the hash table coiBnvTable.]

  SideEffects []

******************************************************************************/
void
Part_PartitionWithExistingBnvs(
  Ntk_Network_t *network,
  graph_t *partition,
  st_table *coiBnvTable,
  st_table *absLatchTable,
  st_table *absBnvTable)
{

  PartPartitionWithExistingBnvs(network, partition, coiBnvTable, 
                                absLatchTable, absBnvTable);
}

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

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

  Synopsis [Creates the graph representing the combinational outputs
  as functions of the combinational inputs as well as possibly some
  intermediate variables.]

  Description [The idea behind this partition method is representing
  the functionality of combinational outputs in terms of combinational
  inputs as well as some intermediate variables. Using intermediate
  variables helps in controlling size of the BDDs for the combinational
  outputs. These intermediate variables themselves may depend on other
  intermediate variables and priamry inputs. Ultimately, the
  functionality is realized in terms of combinational inputs alone.

  The procedure works as follows:

  i) First a topological order of the nodes is computed.
  ii) A table mapping node to mvf is initialized for combinational
  inputs.
  iii) The functionality of nodes is computed in topological order in
  terms of the fanin functions.
  iii) If the bdd size of the mvf for a node exceeds the given bdd size
  limit (set by partition_threshold), and the node has non-zero
  fanouts, an mdd variable corresponding to that node is created and
  node-mvf table is updated appropriately.
  iv) For all the nodes in the fanouts of that node, the given node is
  treated as primary input.
  ]
  

  SideEffects [Partition is changed.]

  SeeAlso     [Part_NetworkCreatePartition PartPartitionTotal PartPartitionInputsOutputs]

******************************************************************************/
void
PartPartitionFrontier(Ntk_Network_t *network,
                      graph_t *partition,
                      lsList  rootList,
                      lsList  leaveList,
                      mdd_t   *careSet)
{
  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
  lsGen         gen;                /* To iterate over lists */
  vertex_t      *vertex;          /* Destination of the edge being added */
  char          *name;              /* Name of the node being processed */
  int           mddId;              /* Id of the node being processed */
  int           i;
  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
     mdd for a new variable. */
  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *topoNodeTable;
  Ntk_Node_t *fanoutNode;
  array_t *rootNodesArray;
  long fanoutNumber = 0;
  Mvf_Function_t *nodeMvf; 
  long bddSize;
  int sizeThreshold;
  lsList topologicalNodeList;
  lsGen lsgen;
  st_generator *stgen;
  char *flagValue =  Cmd_FlagReadByName("partition_threshold");

  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put combinational inputs in the leafNodesTable. */
  if (leaveList == (lsList)0) {
    Ntk_NetworkForEachCombInput(network, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of then */ 
  else {
    lsForEachItem(leaveList, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of if-then-else */

  
  /* Take the nodes in rootList as the roots */
  if (rootList == (lsList)0) {
    rootNodesArray = array_alloc(Ntk_Node_t *, 
                               Ntk_NetworkReadNumCombOutputs(network));
    i = 0;
    Ntk_NetworkForEachCombOutput(network, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }

  } /* End of then */ 
  else {
    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
    i = 0;
    lsForEachItem(rootList, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of if-then-else */

  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   

  /* For each node, compute the number of its fanouts */
  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(topologicalNodeList, lsgen, node){
    st_insert(topoNodeTable, (char *)node, NIL(char));
  }
  lsForEachItem(topologicalNodeList, lsgen, node){
    fanoutNumber = 0;
    Ntk_NodeForEachFanout(node, i, fanoutNode) {
      if (st_is_member(topoNodeTable, fanoutNode) &&
          !st_is_member(leafNodesTable, fanoutNode))
        fanoutNumber++;
    }
    st_insert(topoNodeTable, node, (char *) fanoutNumber);
  }

  /* For each leaf nodes, create a vertex in the partition, create the mvf, and
   * a mapping of name to vertex, and mddId to vertex.
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL) {
    if (!st_lookup(topoNodeTable, node, &fanoutNumber)) {
      continue;
    }
    mddId = Ntk_NodeReadMddId(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, vertex);
    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
              vertex); 

    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }

    if (fanoutNumber <= 0) {
      st_insert(nodeToMvfTable, (char *)node, NIL(char));
    }else
      st_insert(nodeToMvfTable, (char *)node, 
                (char *)Mvf_FunctionDuplicate(nodeMvf));

    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                             mddId);
  }

  st_free_table(leafNodesTable);
  

  fflush(vis_stdout);

  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */

  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, (char *)node)) continue;

    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
    bddSize = bdd_size_multiple(nodeMvf);

    if ((bddSize <= sizeThreshold) && !Ntk_NodeTestIsCombOutput(node)) {
      st_insert(nodeToMvfTable, node, nodeMvf);
      continue;
    }

    /* node either is a primary output, or has an mvf exceeding the
     * threshold. 
     */
    st_lookup(topoNodeTable, node, &fanoutNumber);
    if ( (bddSize > sizeThreshold) &&  fanoutNumber > 0 ) {
      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }
      st_insert(nodeToMvfTable, node,
                Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }else {
      if (fanoutNumber <= 0) {
        st_insert(nodeToMvfTable, node, NIL(char));
      }else
        st_insert(nodeToMvfTable, (char *)node, 
                  (char *)Mvf_FunctionDuplicate(nodeMvf));
    }

    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    mddId = Ntk_NodeReadMddId(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */
  

  /* sanity check */
  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
#if 0
    if (nodeMvf != NIL(Mvf_Function_t)) {
      int chk = st_lookup(topoNodeTable, node, &fanoutNumber);
      Ntk_NodeForEachFanout(node, i, fanoutNode) {
        fprintf(vis_stdout, "\nunclean node %s   =>   %s", 
                Ntk_NodeReadName(node),
                Ntk_NodeReadName(fanoutNode));
        if (Ntk_NodeTestIsLatch(fanoutNode))
          fprintf(vis_stdout, "\t(latch)");
      }
    }
#else
    assert (nodeMvf == NIL(Mvf_Function_t)) ;
#endif
  }

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  st_free_table(topoNodeTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}

#if 0
void
PartPartitionFrontierOld(Ntk_Network_t *network,
                      graph_t *partition,
                      lsList  rootList,
                      lsList  leaveList,
                      mdd_t   *careSet)
{
  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
  lsGen         gen;                /* To iterate over lists */
  vertex_t      *vertex;          /* Destination of the edge being added */
  char          *name;              /* Name of the node being processed */
  int           mddId;              /* Id of the node being processed */
  int           i;
  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
     mdd for a new variable. */
  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  array_t *rootNodesArray;
  Mvf_Function_t *nodeMvf; 
  long bddSize;
  int sizeThreshold;
  lsList topologicalNodeList;
  lsGen lsgen;
  st_generator *stgen;
  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put combinational inputs in the leafNodesTable. */
  if (leaveList == (lsList)0) {
    Ntk_NetworkForEachCombInput(network, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of then */ 
  else {
    lsForEachItem(leaveList, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of if-then-else */

  /*
   * For each leaf nodes, create a vertex in the partition, create the mvf, and
   * a mapping of name to vertex, and mddId to vertex.
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL){
    mddId = Ntk_NodeReadMddId(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
              (char *)vertex); 
    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }
    st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                             mddId);
  }

  
  /* Take the nodes in rootList as the roots */
  if (rootList == (lsList)0) {
    rootNodesArray = array_alloc(Ntk_Node_t *, 
                               Ntk_NetworkReadNumCombOutputs(network));
    i = 0;
    Ntk_NetworkForEachCombOutput(network, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of then */ 
  else {
    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
    i = 0;
    lsForEachItem(rootList, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of if-then-else */

  

  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   
  
  st_free_table(leafNodesTable);
  

  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */

  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, (char *)node)) continue;
    nodeMvf = NodeBuildMvf(node, nodeToMvfTable);
    bddSize = bdd_size_multiple(nodeMvf);
    if ((bddSize <= sizeThreshold) &&
        (Ntk_NodeTestIsCombOutput(node) == 0)){
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      continue;
    }
    /* node either is a primary output, or has an mvf exceeding the
       threshold. */
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name,
              (char *)vertex);
    if ((bddSize > sizeThreshold) &&
        (Ntk_NodeReadNumFanouts(node) != 0)){
      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }
      st_insert(nodeToMvfTable, (char *)node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }
    else {
      /* Small mvf, or no fanout */
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
    }
    mddId = Ntk_NodeReadMddId(node);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name,
                                                             nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */
  
  /*
   * Free the Mvfs in nodeToMvfTable not associated with vertices in the
   * partition.  The mvfs of inputs are always in the partition; hence,
   * their mvfs should always be preserved.  For outputs, we have to free
   * the mvf in nodeToMvfTable if the output is also a cutpoint, because in
   * this case the mvf in the partition vertex and the one in the
   * nodeToMvfTable are different.
   */

  lsForEachItem(topologicalNodeList, gen, node){ 
    if (!Ntk_NodeTestIsCombInput(node)){
      if(!Ntk_NodeTestIsCombOutput(node)){ 
        st_lookup(nodeToMvfTable, node, &nodeMvf); 
        assert(nodeMvf != NIL(Mvf_Function_t)); 
        Mvf_FunctionFree(nodeMvf);
      } else {
        Mvf_Function_t *vertexMvf;
        
        name =  Ntk_NodeReadName(node);
        vertex = Part_PartitionFindVertexByName(partition, name);
        st_lookup(nodeToMvfTable, node, &nodeMvf);
        vertexMvf = PartVertexReadFunction(vertex);
        assert(nodeMvf != NIL(Mvf_Function_t) &&
               vertexMvf != NIL(Mvf_Function_t));
        if(vertexMvf != nodeMvf){
          Mvf_FunctionFree(nodeMvf);
        }
      }
    }/* not input */
  }/* for each node */

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}
#endif

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

  Synopsis [Creates the graph representing the combinational outputs
  as functions of the combinational inputs as well as possibly some
  intermediate variables.]

  Description [The same as PartPartitionFrontier, but only add vertices for
  nodes that are not in partition. This function can be used to update the 
  partition after more network nodes are added.]
  
  SideEffects [Partition is changed.]

  SeeAlso     [PartPartitionFrontier]

******************************************************************************/
void
PartUpdateFrontier(Ntk_Network_t *network,
                   graph_t *partition,
                   lsList  rootList,
                   lsList  leaveList,
                   mdd_t   *careSet)
{
  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
  lsGen         gen;                /* To iterate over lists */
  vertex_t      *vertex;          /* Destination of the edge being added */
  char          *name;              /* Name of the node being processed */
  int           mddId;              /* Id of the node being processed */
  int           i, flag;
  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
     mdd for a new variable. */
  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  array_t *rootNodesArray;
  Mvf_Function_t *nodeMvf; 
  long bddSize;
  int sizeThreshold;
  lsList topologicalNodeList;
  lsGen lsgen;
  st_generator *stgen;
  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
  
  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put combinational inputs in the leafNodesTable. */
  if (leaveList == (lsList)0) {
    Ntk_NetworkForEachCombInput(network, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of then */ 
  else {
    lsForEachItem(leaveList, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of if-then-else */

  /*
   * For each leaf nodes, create a vertex in the partition, create the mvf, and
   * a mapping of name to vertex, and mddId to vertex.
   * Notices that: if a vertex exists in the partition, use it instead of 
   * creating a new one.
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL){
    mddId = Ntk_NodeReadMddId(node);
    name  = Ntk_NodeReadName(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);
    flag = st_lookup(PartPartitionReadNameToVertex(partition), 
                     name, &vertex);
    if (flag) {
      nodeMvf = ((PartVertexInfo_t *)(vertex->user_data))->functionality.mvf;
      st_insert(nodeToMvfTable, node, nodeMvf);
      /*
      name = Ntk_NodeReadName(node);
      fprintf(vis_stdout, "warning: node %s already in the partition\n",
              name);
      */
    }else {
      vertex = g_add_vertex(partition);
      st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
      st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
                (char *)vertex); 
      if (Ntk_NodeTestIsPseudoInput(node)){
        nodeMvf = NodeBuildPseudoInputMvf(node);
      }else {
        nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
      }
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                               mddId);
    }
  }
  
  /* Take the nodes in rootList as the roots */
  if (rootList == (lsList)0) {
    rootNodesArray = array_alloc(Ntk_Node_t *, 
                               Ntk_NetworkReadNumCombOutputs(network));
    i = 0;
    Ntk_NetworkForEachCombOutput(network, gen, node) {
      name = Ntk_NodeReadName(node);
      if ( !st_is_member(PartPartitionReadNameToVertex(partition), name) )
        array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of then */ 
  else {
    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
    i = 0;
    lsForEachItem(rootList, gen, node) {
      name = Ntk_NodeReadName(node);
      if ( !st_is_member(PartPartitionReadNameToVertex(partition), name) )
        array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of if-then-else */

  

  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   
  
  st_free_table(leafNodesTable);
  

  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */

  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, node)) continue;
    name = Ntk_NodeReadName(node);
    flag = st_lookup(PartPartitionReadNameToVertex(partition), 
                     name, &vertex);
    if (flag) {
      mddId = Ntk_NodeReadMddId(node);
      if (mddId != -1)
        st_insert(nodeToMvfTable, node,
                  (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
      else {
        nodeMvf = PartVertexReadFunction(vertex);
        st_insert(nodeToMvfTable, node, nodeMvf);
      }
      continue;
    }
    nodeMvf = NodeBuildMvf(node, nodeToMvfTable);
    bddSize = bdd_size_multiple(nodeMvf);
    if ((bddSize <= sizeThreshold) &&
        (Ntk_NodeTestIsCombOutput(node) == 0)){
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      continue;
    }
    /* node either is a primary output, or has an mvf exceeding the
       threshold. */
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name,
              (char *)vertex);
    if ((bddSize > sizeThreshold) &&
        (Ntk_NodeReadNumFanouts(node) != 0)){
      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }
      st_insert(nodeToMvfTable, (char *)node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }
    else {
      /* Small mvf, or no fanout */
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
    }
    mddId = Ntk_NodeReadMddId(node);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name,
                                                             nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */
  
  /*
   * Free the Mvfs in nodeToMvfTable not associated with vertices in the
   * partition.  The mvfs of inputs are always in the partition; hence,
   * their mvfs should always be preserved.  For outputs, we have to free
   * the mvf in nodeToMvfTable if the output is also a cutpoint, because in
   * this case the mvf in the partition vertex and the one in the
   * nodeToMvfTable are different.
   */

  lsForEachItem(topologicalNodeList, gen, node){ 
    if (!Ntk_NodeTestIsCombInput(node)){
      if(!Ntk_NodeTestIsCombOutput(node)){ 
        st_lookup(nodeToMvfTable, node, &nodeMvf); 
        assert(nodeMvf != NIL(Mvf_Function_t)); 
        Mvf_FunctionFree(nodeMvf);
      } else {
        Mvf_Function_t *vertexMvf;
        
        name =  Ntk_NodeReadName(node);
        vertex = Part_PartitionFindVertexByName(partition, name);
        st_lookup(nodeToMvfTable, node, &nodeMvf);
        vertexMvf = PartVertexReadFunction(vertex);
        assert(nodeMvf != NIL(Mvf_Function_t) &&
               vertexMvf != NIL(Mvf_Function_t));
        if(vertexMvf != nodeMvf){
          Mvf_FunctionFree(nodeMvf);
        }
      }
    }/* not input */
  }/* for each node */

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}

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

  Synopsis [Selectively insert Boolean network variables.]

  Description [Selectively insert Boolean network varibles using the
  Frontier partition method---every time the BDD size exceeds the
  partition threshold, a boolean network variable is inserted.

  The added boolean network variables are inserted into the coiBnvTable. ]
  

  SideEffects []

  SeeAlso     [PartPartitionFrontier]

******************************************************************************/
void
PartInsertBnvs(
  Ntk_Network_t *network,
  st_table *coiLatchTable,
  st_table *coiBnvTable)
{
  mdd_manager    *mddManager = Ntk_NetworkReadMddManager(network);
  st_table       *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table       *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsList         topologicalNodeList;
  st_table       *topoNodeTable;
  array_t        *rootNodesArray;
  Ntk_Node_t     *fanoutNode, *node;
  Mvf_Function_t *nodeMvf; 
  long           bddSize, sizeThreshold, fanoutNumber, mddId;
  int            i;
  lsGen          lsgen;
  st_generator   *stgen;
  char           *flagValue;

  flagValue =  Cmd_FlagReadByName("partition_threshold");
  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put latch data inputs in the rootNodesArray */
  rootNodesArray = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(coiLatchTable, stgen, &node, NULL) {
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadInitialInput(node));
  }

  /* Put combinational inputs, as well as the existing coiBnvs, in the
   * leafNodesTable. */
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    st_insert(leafNodesTable, node, (char *) (long) (-1) );
  }
  st_foreach_item(coiBnvTable, stgen, &node, NULL) {
    st_insert(leafNodesTable, node, (char *) (long) (-1) );
  }
  
  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   

  /* For each node, compute the number of fanouts */
  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(topologicalNodeList, lsgen, node){
    st_insert(topoNodeTable, (char *)node, NIL(char));
  }
  lsForEachItem(topologicalNodeList, lsgen, node){
    fanoutNumber = 0;
    Ntk_NodeForEachFanout(node, i, fanoutNode) {
      if (st_is_member(topoNodeTable, (char *)fanoutNode) &&
          !st_is_member(leafNodesTable, (char *)fanoutNode) )
        fanoutNumber++;
    }
    st_insert(topoNodeTable, (char *)node, (char *)fanoutNumber);
  }

  /* assign mddIds to latches if necessary */
  /* chao: this may be too slow! */
  /* chao: this order may not be as good as static_order */
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (Ntk_NodeTestIsInput(node)) {
      Ord_NetworkAssignMddIdForNode(network, node);
    }else if (Ntk_NodeTestIsLatch(node)) {
      Ord_NetworkAssignMddIdForNode(network, node);
      Ord_NetworkAssignMddIdForNode(network, Ntk_NodeReadShadow(node));
    }
  }
  st_foreach_item(coiLatchTable, stgen, &node, NULL) {
    Ord_NetworkAssignMddIdForNode(network, node);
    Ord_NetworkAssignMddIdForNode(network, Ntk_NodeReadShadow(node));
  }

  /* create nodeMvf for leaf nodes */
  st_foreach_item(leafNodesTable, stgen, &node, NULL) {
    if (!st_lookup(topoNodeTable, node, &fanoutNumber)) {
      continue;
    }
    mddId = Ntk_NodeReadMddId(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);

    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }

    if (fanoutNumber <= 0) {
      Mvf_FunctionFree(nodeMvf);
      st_insert(nodeToMvfTable, (char *)node, NIL(char));
    }
    else
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
  }

  st_free_table(leafNodesTable);


  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, node)) 
      continue;

    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
    bddSize = bdd_size_multiple(nodeMvf);
    st_lookup(topoNodeTable, node, &fanoutNumber);

    if ((bddSize <= sizeThreshold) && !Ntk_NodeTestIsCombOutput(node)) {
      assert(fanoutNumber > 0);
      st_insert(nodeToMvfTable, node, nodeMvf);
      continue;
    }
    /* node either is a primary output, or has an mvf exceeding the
       threshold. */
    if ((bddSize > sizeThreshold) && fanoutNumber > 0) {
                                   /*(Ntk_NodeReadNumFanouts(node) != 0)) { */
      /* ADD A bnv !!! */
      st_insert(coiBnvTable, (char *)node, NIL(char));

      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }

      st_insert(nodeToMvfTable, (char *)node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
      Mvf_FunctionFree(nodeMvf);
    }else {
      if (fanoutNumber <= 0) {
        Mvf_FunctionFree(nodeMvf);
        st_insert(nodeToMvfTable, node, NIL(char));
      }
      else
        st_insert(nodeToMvfTable, node, (char *)nodeMvf);
    }

  }/* for each member of topologicalNodeList */
  
  /* sanity check */
  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
#if 0
    if (nodeMvf != NIL(Mvf_Function_t)) {
      st_lookup(topoNodeTable, node, &fanoutNumber);
      fprintf(vis_stdout, "\nunclean node = %s, fanout# = %d",
              Ntk_NodeReadName(node), fanoutNumber);
    }
#else
    assert (nodeMvf == NIL(Mvf_Function_t));
#endif
  }

  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  st_free_table(topoNodeTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}

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

  Synopsis [Update the partition with the given set of internal nodes.]

  Description [Update the partition with the given set of internal
  nodes. Insert intermediate variables, or Boolean Network Variables
  (BNVs) only for the given set of internal nodes
  (coiBnvTable). Intermediate variables (or Bnvs) that do not appear
  in absBnvTable will not be included in the partition---they will be
  treated as inputs.]

  SideEffects []

  SeeAlso     [PartPartitionFrontier PartPartitionInsertBnvs]

******************************************************************************/
void
PartPartitionWithExistingBnvs(
  Ntk_Network_t *network,
  graph_t *partition,
  st_table *coiBnvTable,
  st_table *absLatchTable,
  st_table *absBnvTable)
{
  mdd_manager    *mddManager = PartPartitionReadMddManager(partition);
  st_table       *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table       *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  array_t        *rootNodesArray, *combNodesArray;
  lsList         topologicalNodeList;
  st_table       *topoNodeTable;
  Ntk_Node_t     *fanoutNode, *node;
  Mvf_Function_t *nodeMvf; 
  vertex_t       *vertex;         
  long           mddId, fanoutNumber;
  char           *name;           
  lsGen          lsgen;
  st_generator   *stgen;
  int            i;

  /* Put latch data inputs in the rootNodesArray */
  rootNodesArray = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(absLatchTable, stgen, &node, NULL) {
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadInitialInput(node));
  }

  /* Put also latch initial inputs in the rootNodesArray */
  combNodesArray = Ntk_NodeComputeTransitiveFaninNodes(network,
                                                       rootNodesArray,
                                                       TRUE, TRUE);
  arrayForEachItem(Ntk_Node_t *, combNodesArray, i, node) {
    if ( Ntk_NodeTestIsLatch(node) && 
         !st_is_member(absLatchTable, (char *)node) )
      array_insert_last(Ntk_Node_t *, rootNodesArray, 
                        Ntk_LatchReadInitialInput(node));
  }
  array_free(combNodesArray);


  /* Put combinational inputs in the leafNodesTable. */
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
  }
  /* Put BNVs that are not in absBnvTable in the leafNodesTable */
  st_foreach_item(coiBnvTable, stgen, &node, NULL) {
    if (!st_is_member(absBnvTable, (char *)node))
      st_insert(leafNodesTable, node, (char *) (long) (-1) );
  }

  /* Get an array of nodes sorted in topological order  */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);

  /* For each node, compute the number of fanouts */
  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(topologicalNodeList, lsgen, node){
    st_insert(topoNodeTable, (char *)node, NIL(char));
  }
  lsForEachItem(topologicalNodeList, lsgen, node){
    fanoutNumber = 0;
    Ntk_NodeForEachFanout(node, i, fanoutNode) {
      if (st_is_member(topoNodeTable, (char *)fanoutNode) &&
          !st_is_member(leafNodesTable, (char *)fanoutNode))
        fanoutNumber++;
    }
    st_insert(topoNodeTable, (char *)node, (char *)fanoutNumber);
   }

  /* Create partition vertices for the leaves 
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL){
    if (!st_lookup(topoNodeTable, node, &fanoutNumber))
      continue;
    mddId = Ntk_NodeReadMddId(node);
    if (mddId == NTK_UNASSIGNED_MDD_ID) {
        /* it is a input sign under the fanin cone of the initialInput
         * of some invisible latches */
        assert(Ntk_NodeTestIsInput(node));
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
    }
    /*assert(mddId != NTK_UNASSIGNED_MDD_ID);*/
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
              (char *)vertex); 
    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }

    if (fanoutNumber <= 0) 
      st_insert(nodeToMvfTable, (char *)node, NIL(char));
    else
      st_insert(nodeToMvfTable, (char *)node, 
                (char *)Mvf_FunctionDuplicate(nodeMvf));

    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                             mddId);
  }

  /* Go through the topologicalNodeList, and build Mdds for nodes in
   * the absBnvTable
   */
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, (char *)node)) continue;

    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);

    if ( !st_is_member(absBnvTable,(char *)node) && 
         !Ntk_NodeTestIsCombOutput(node)) {
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      continue;  
    }
    
    /* node is either a primary output, or a boolean network var */
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);

    if (st_is_member(absBnvTable,node)) {
      /* ADD a bnv !!! */
      mddId = Ntk_NodeReadMddId(node);
      assert(mddId != -1);
      st_insert(nodeToMvfTable, node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }else {
      st_lookup(topoNodeTable, node, &fanoutNumber);
      if (fanoutNumber <= 0) 
        st_insert(nodeToMvfTable, node, NIL(char));
      else
        st_insert(nodeToMvfTable, node, 
                  (char *)Mvf_FunctionDuplicate(nodeMvf));
    }

    mddId = Ntk_NodeReadMddId(node);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */

  /* sanity check */
  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
#if 1
    if (nodeMvf != NIL(Mvf_Function_t)) {
      st_lookup(topoNodeTable, node, &fanoutNumber);
      fprintf(vis_stdout, "\nunclean node = %s, fanout# = %ld",
              Ntk_NodeReadName(node), fanoutNumber);
    }
#else
    assert(nodeMvf == NIL(Mvf_Function_t));
#endif
  }

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  st_free_table(topoNodeTable);
  st_free_table(leafNodesTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}


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

  Synopsis    [Prints the integers from a symbol table.]

  Description [Prints the integers from a symbol table.]

  SideEffects []

******************************************************************************/
void
PartPrintPartition(graph_t *partition)
{
  vertex_t *vertex;
  lsList vertexList = g_get_vertices(partition);
  lsGen gen;
  st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
  fprintf(vis_stdout,"******* Printing Partition *********\n");
  lsForEachItem(vertexList, gen, vertex){
    PrintPartitionRecursively(vertex,vertexTable,0);
  }
  fprintf(vis_stdout,"******* End Printing Partition *********\n");
  st_free_table(vertexTable);
}

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

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

  Synopsis    [Creates edges in the graph corresponding to a partition.]

  Description [Creates edges in the graph corresponding to a
  partition. An edge exists between node i and node j, if node j is in
  the support of functionality of node i.]

  SideEffects [Partition is changed.]

  SeeAlso     []

******************************************************************************/
static void
PartitionCreateEdges(graph_t *partition)
{
  lsList vertexList;
  lsGen gen;
  vertex_t *toVertex;
  edge_t *edge;

  /* this will be executed only when used inside PartitionUpdateFrontier */
  foreach_edge(partition, gen, edge) {
    g_delete_edge(edge, (void(*)(gGeneric))0);
  }

  vertexList = g_get_vertices(partition);

  lsForEachItem(vertexList, gen, toVertex) {
    st_table     *mddSupport; /* To store the support of the Mvf_Function */
    st_generator *stGen;      /* To iterate over the MddIds of the support */
    vertex_t     *fromVertex; /* Will hold the current vertex in the support */
    Mvf_Function_t *mddFunction;
    long          mddId;
    
    mddFunction = PartVertexReadFunction(toVertex);
    mddSupport = PartCreateFunctionSupportTable(mddFunction);
    st_foreach_item(mddSupport, stGen, &mddId, NULL) {
      st_lookup(PartPartitionReadMddIdToVertex(partition), (char *) mddId,
                &fromVertex);  
      /* 
       * Add the edge to the graph. Make sure a self loop is not added. The
       * self loop may be produced by a mdd that has in its support the same
       * variables that represent the mddId of the node.
       */
      if (fromVertex != toVertex) {
        g_add_edge(fromVertex, toVertex);
      }
    }
    st_free_table(mddSupport);
  } 
}

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

  Synopsis    [Builds the functionality of a node, given the
  functionality of its fanins.]

  Description [The nodeToMvfTable must contain the functionality of
  all the fanins of the node.]

  SideEffects [none.]

  SeeAlso     []

******************************************************************************/
static Mvf_Function_t *
NodeBuildMvf(Ntk_Node_t * node, st_table * nodeToMvfTable)
{
  int i;
  Mvf_Function_t *resultMvf;
  Ntk_Node_t *faninNode;
  array_t *faninMvfs = array_alloc(Mvf_Function_t *,
                                            Ntk_NodeReadNumFanins(node));
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node)); 
  int columnIndex = Ntk_NodeReadOutputIndex(node);
  Tbl_Table_t *table = Ntk_NodeReadTable(node);
  
  Ntk_NodeForEachFanin(node, i, faninNode) {
    Mvf_Function_t *tmpMvf;
    st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
    assert(tmpMvf);
    array_insert(Mvf_Function_t *, faninMvfs, i, tmpMvf);
  }
  
  resultMvf = Tbl_TableBuildMvfFromFanins(table, columnIndex,
                                          faninMvfs, mddMgr);    
  
  /* Don't free the MVFs themselves, but just free the array. */
  array_free(faninMvfs);
  return resultMvf;
}
    
/**Function********************************************************************

  Synopsis    [Builds the functionality of a node, given the
  functionality of its fanins.]

  Description [The nodeToMvfTable must contain the functionality of
  all the fanins of the node. When the faninNumber counter is
  decreased to 0, free the corresponding MVF in the nodeToMvfTable.]

  SideEffects [none.]

  SeeAlso     []

******************************************************************************/
static Mvf_Function_t *
NodeBuildMvf2(
  Ntk_Node_t * node, 
  st_table * nodeToMvfTable,
  st_table * faninNumberTable)
{
  long faninNumber;
  int i;
  Mvf_Function_t *resultMvf;
  Ntk_Node_t *faninNode;
  array_t *faninMvfs = array_alloc(Mvf_Function_t *,
                                   Ntk_NodeReadNumFanins(node));
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node)); 
  int columnIndex = Ntk_NodeReadOutputIndex(node);
  Tbl_Table_t *table = Ntk_NodeReadTable(node);
  
  Ntk_NodeForEachFanin(node, i, faninNode) {
    Mvf_Function_t *tmpMvf;
    st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
    assert(tmpMvf);
    array_insert(Mvf_Function_t *, faninMvfs, i, tmpMvf);
  }
  
  resultMvf = Tbl_TableBuildMvfFromFanins(table, columnIndex,
                                          faninMvfs, mddMgr);    
  
  /* Don't free the MVFs themselves, but just free the array. */
  array_free(faninMvfs);

  /* if the fanin node is no longer useful, remove its Mvfs */
  Ntk_NodeForEachFanin(node, i, faninNode) {
    st_lookup(faninNumberTable, faninNode, &faninNumber);
    assert(faninNumber > 0);
    faninNumber--;
    st_insert(faninNumberTable, faninNode, (char *)faninNumber);

    if (faninNumber <= 0) {
      Mvf_Function_t *tmpMvf;
      st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
      Mvf_FunctionFree(tmpMvf);
      st_insert(nodeToMvfTable, faninNode, NIL(char));
    }
  }

  return resultMvf;
}
    
      

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

  Synopsis    [Builds MVF for a node that is a pseudo input.]

  Description [Builds MVF for a node that is a pseudo input.  This node has a
  single output and no inputs. Its table has several row entries.  We build an
  MVF whose components correspond exactly to possible table outputs.]

  SideEffects []

  Comment [Although pseudo inputs, constants, and internal nodes all have
  tables, a single procedure cannot be used to build their MVF.  A pseudo
  input MVF is built in terms of its mddId, whereas a constant or internal is
  not.  A constant or pseudo input doesn't have any inputs, whereas an
  internal does.]
  
  SeeAlso     [Tbl_TableBuildMvfForNonDetConstant]

******************************************************************************/
static Mvf_Function_t *
NodeBuildPseudoInputMvf(
  Ntk_Node_t * node)
{
  mdd_manager  *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node));
  int          mddId = Ntk_NodeReadMddId( node );
  int          columnIndex = Ntk_NodeReadOutputIndex( node );
  Tbl_Table_t  *table = Ntk_NodeReadTable( node );
  Mvf_Function_t *mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex,
                                                        mddId, mddMgr);

  mdd_t *vMdd, *tMdd, *rMdd;
  int lIndex, needProcess, i;

  rMdd = mdd_zero(mddMgr);
  needProcess = 0;
  lIndex = 0;
  for(i=0; i<mvf->num; i++) {
    vMdd = array_fetch(mdd_t *, mvf, i);
    if(mdd_equal(vMdd, rMdd)) {
      needProcess = 1;
    }
    else {
      lIndex = i;
    }
  }
  if(needProcess) {
    for(i=0; i<lIndex; i++) {
      vMdd = array_fetch(mdd_t *, mvf, i);
      tMdd = mdd_or(vMdd, rMdd, 1, 1);
      mdd_free(rMdd);
      rMdd = tMdd;
    }
    vMdd = array_fetch(mdd_t *, mvf, lIndex);
    mdd_free(vMdd);
    tMdd = mdd_not(rMdd);
    mdd_free(rMdd);
    array_insert(mdd_t *, mvf, lIndex, tMdd);
  }
  else {
    mdd_free(rMdd);
  }

  return mvf;
}


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

  Synopsis    [Prints the integers from a symbol table.]

  Description [Prints the integers from a symbol table.]

  SideEffects []

******************************************************************************/
static void
PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int
                          indent)
{
  int i;
  lsList faninEdges;
  lsGen gen;
  vertex_t *faninVertex;
  edge_t *faninEdge;
  
  if (st_is_member(vertexTable, (char *)vertex)) return;
  st_insert(vertexTable, (char *)vertex, NIL(char));
  for(i=0; i<= indent; i++) fprintf(vis_stdout," ");
  fprintf(vis_stdout,"%s %d\n", Part_VertexReadName(vertex),
          Part_VertexReadMddId(vertex)); 
  faninEdges = g_get_in_edges(vertex);
  if (lsLength(faninEdges) == 0) return;
  lsForEachItem(faninEdges, gen, faninEdge){
    faninVertex = g_e_source(faninEdge);
    PrintPartitionRecursively(faninVertex, vertexTable,indent+2);
  }
}