source: vis_dev/vis-2.3/src/ntk/ntkNtk.c

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

  FileName    [ntkNtk.c]

  PackageName [ntk]

  Synopsis    [Routines to access the network data structure.]

  Author      [Adnan Aziz, Tom Shiple]

  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 "ntkInt.h"
#include "mdd.h"

static char rcsid[] UNUSED = "$Id: ntkNtk.c,v 1.23 2010/04/09 23:44:05 fabio Exp $";

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

  Synopsis    [Structure to store uninterpreted application info.]

  SeeAlso     [Ntk_NetworkAddApplInfo]

******************************************************************************/
typedef struct ApplInfoStruct {
  Ntk_ApplInfoFreeFn  freeFn;  /* application function to free data */
  void               *data;    /* application data */
} ApplInfo_t;


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

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

static char * NodeReadNameFromTable(Ntk_Node_t *node, st_table *name2ToName1);
static Tbl_Table_t * DuplicateTableAndVars(Ntk_Node_t *node, char *name);

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


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

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

  Synopsis    [Returns the name of a network.]

  Description [Returns the name of a network.  Every network must have a name. It
  is an error to call this function on a NULL network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAlloc]

******************************************************************************/
char *
Ntk_NetworkReadName(
  Ntk_Network_t * network)
{
  return (network->name);
}


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

  Synopsis    [Returns the MDD manager of a network.]

  Description [Returns the MDD manager of a network.  The MDD manager is set
  by calling Ntk_NetworkSetMddManager.  If the application frees the returned
  MDD manager, then it should in turn set the network's MDD manager pointer to
  NULL.  If the pointer is non-NULL when Ntk_NetworkFree is called, then the MDD
  manager will be freed. It is an error to call this function on a NULL
  network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkSetMddManager Ntk_NetworkInitializeMddManager]

******************************************************************************/
mdd_manager *
Ntk_NetworkReadMddManager(
  Ntk_Network_t * network)
{
  return (network->mddManager);
}


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

  Synopsis    [Sets the MDD manager of a network.]

  Description [Sets the MDD manager of a network.  This could be useful, for
  example, to force two networks to have the same MDD manager.  However, be
  careful that in the end the manager is only freed once.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadMddManager Ntk_NetworkInitializeMddManager]

******************************************************************************/
void
Ntk_NetworkSetMddManager(
  Ntk_Network_t  * network,
  mdd_manager * mddManager)
{
  network->mddManager = mddManager;
}

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

  Synopsis    [Returns the MAig manager of a network.]

  Description [Returns the MAig manager of a network.  The MAig manager is set
  by calling Ntk_NetworkSetMAigManager.  If the application frees the returned
  MAig manager, then it should in turn set the network's MAig manager pointer to
  NULL.  If the pointer is non-NULL when Ntk_NetworkFree is called, then the MAig
  manager will be freed. It is an error to call this function on a NULL
  network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkSetMAigManager Ntk_NetworkInitializeMAigManager]

******************************************************************************/
mAig_Manager_t *
Ntk_NetworkReadMAigManager(
  Ntk_Network_t * network)
{
  return (network->mAigManager);
}


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

  Synopsis    [Sets the mAig manager of a network and the netowrk for the
               mAig manager.]

  Description [Sets the MAig manager of a network.  This could be useful, for
  example, to force two networks to have the same MAig manager.  However, be
  careful that in the end the manager is only freed once.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadMAigManager Ntk_NetworkInitializeMAigManager]

******************************************************************************/
void
Ntk_NetworkSetMAigManager(
  Ntk_Network_t * network,
  mAig_Manager_t * mAigManager)
{
  network->mAigManager = mAigManager;
}

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

  Synopsis    [Creates and initializes an empty MDD manager for a network.]

  Description [Creates and initializes an empty MDD manager for a
  network. Sets the MDD manager field of the network, and returns a pointer to
  the newly created manager.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadMddManager Ntk_NetworkSetMddManager]

******************************************************************************/
mdd_manager *
Ntk_NetworkInitializeMddManager(
  Ntk_Network_t * network)
{
  network->mddManager = mdd_init_empty();

  return (network->mddManager);
}


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

  Synopsis    [Returns the dynamic variable ordering method of a network.]

  Description [Returns the dynamic variable ordering method of a network.  The
  method is set by calling Ntk_NetworkSetDynamicVarOrderingMethod.  The method
  is set to BDD_REORDER_NONE when the network is first created.  It is an
  error to call this function on a NULL network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkSetDynamicVarOrderingMethod]

******************************************************************************/
bdd_reorder_type_t
Ntk_NetworkReadDynamicVarOrderingMethod(
  Ntk_Network_t * network)
{
  return (network->dynVarOrdMethod);
}


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

  Synopsis    [Sets the dynamic variable ordering method of a network.]

  Description [Sets the dynamic variable ordering method of a
  network. Allowable values of dynVarOrdMethod are BDD_REORDER_SIFT,
  BDD_REORDER_WINDOW, and BDD_REORDER_NONE.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadDynamicVarOrderingMethod]

******************************************************************************/
void
Ntk_NetworkSetDynamicVarOrderingMethod(
  Ntk_Network_t * network,
  bdd_reorder_type_t dynVarOrdMethod,
  bdd_reorder_verbosity_t verbosity)
{
  bdd_dynamic_reordering(network->mddManager, dynVarOrdMethod, verbosity);
  if (bdd_get_package_name() != CUDD) {
    if (dynVarOrdMethod == BDD_REORDER_SIFT ||
        dynVarOrdMethod == BDD_REORDER_WINDOW ||
        dynVarOrdMethod == BDD_REORDER_NONE) {
      network->dynVarOrdMethod = dynVarOrdMethod;
    } else
      network->dynVarOrdMethod = BDD_REORDER_SIFT;
  } else
    network->dynVarOrdMethod = dynVarOrdMethod;
}


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

  Synopsis    [Returns the undef field of a network.]

  Description [Returns the undef field of a network.  There is no restriction on
  how this field is used.  It is an error to call this function on a NULL
  network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAlloc Ntk_NetworkSetUndef]

******************************************************************************/
void *
Ntk_NetworkReadUndef(
  Ntk_Network_t * network)
{
  return (network->undef);
}


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

  Synopsis    [Sets the undef field of a network.]

  Description [Sets the undef field of a network.  There is no restriction on
  how this field is used.  It is an error to call this function on a NULL
  network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAlloc Ntk_NetworkReadUndef]

******************************************************************************/
void
Ntk_NetworkSetUndef(
  Ntk_Network_t * network,
  void * value)
{
  network->undef = value;
}


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

  Synopsis    [Finds a node in a network by its MDD id.]

  Description [Finds a node in a network by its MDD id.  The MDD id of a node
  is the MDD id returned by Ntk_NodeReadMddId. If the MDD id doesn't
  correspond to an existing node in the network, a NULL pointer is returned.
  Also, if MDD id is equal to NTK_UNASSIGNED_MDD_ID, a NULL pointer is
  returned.]

  SideEffects []

  SeeAlso     [Ntk_NodeSetMddId Ntk_NodeReadMddId]

******************************************************************************/
Ntk_Node_t *
Ntk_NetworkFindNodeByMddId(
  Ntk_Network_t * network,
  int             mddId)
{
  Ntk_Node_t *node = NIL(Ntk_Node_t);

  if (mddId != NTK_UNASSIGNED_MDD_ID) {
    st_lookup(network->mddIdToNode, (char *) (long) mddId, &node);
  }

  return (node);
}


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

  Synopsis    [Finds a node in a network by its actual name.]

  Description [Finds a node in a network by its actual name.  The actual name
  of a node is the name stored with the node (i.e returned by
  Ntk_NodeReadName). If the name doesn't correspond to an existing node in the
  network, a NULL pointer is returned.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadActualNameFromFormalName Ntk_NodeReadName]

******************************************************************************/
Ntk_Node_t *
Ntk_NetworkFindNodeByActualName(
  Ntk_Network_t * network,
  char * name)
{
  Ntk_Node_t *node = NIL(Ntk_Node_t);

  st_lookup(network->actualNameToNode, name, &node);

  return (node);
}


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

  Synopsis    [Finds a node in a network by its formal name, or actual name.]

  Description [Finds a node in a network by its name.  First, the formal name
  to actual name table is checked to see if there is an actual name
  corresponding to the name.  If so, then the node corresponding to the actual
  name is returned.  If there is no corresponding actual name, then it's
  assumed that the name is an actual name, and the corresponding node is
  returned.  If no corresponding node is found, then a NULL pointer is
  returned.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadActualNameFromFormalName
  Ntk_NetworkFindNodeByActualName]

******************************************************************************/
Ntk_Node_t *
Ntk_NetworkFindNodeByName(
  Ntk_Network_t * network,
  char * name)
{
  Ntk_Node_t *node = NIL(Ntk_Node_t);
  char *actualName = Ntk_NetworkReadActualNameFromFormalName(network, name);

  /*
   * If there was no actual name corresponding to name in the formal to actual
   * table, then treat name as an actualName.
   */
  if (actualName == NIL(char)) {
    actualName = name;
  }

  st_lookup(network->actualNameToNode, actualName, &node);

  return (node);
}


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

  Synopsis    [Returns the actual name corresponding to a formal name.]

  Description [Returns the actual name corresponding to a formal name in a
  network.  The actual name is unique in a network.  Nodes of a network are
  identified by their actual names. If the formal name doesn't correspond to
  an actual name in the network, a NULL pointer is returned.]

  SideEffects []

  SeeAlso     [Ntk_NetworkFindNodeByActualName
  Ntk_NetworkInsertFormalNameToActualName]

******************************************************************************/
char *
Ntk_NetworkReadActualNameFromFormalName(
  Ntk_Network_t * network,
  char * formalName)
{
  char *actualName = NIL(char);

  st_lookup(network->formalNameToActualName, formalName, &actualName);

  return (actualName);
}


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

  Synopsis    [Creates correspondence from formalName to actualName.]

  Description [Creates correspondence from formalName to actualName. Copies
  are made of formalName and actualName before storing them.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadActualNameFromFormalName]

******************************************************************************/
void
Ntk_NetworkInsertFormalNameToActualName(
  Ntk_Network_t * network,
  char * formalName,
  char * actualName)
{
  char *formalNameCopy = util_strsav(formalName);
  char *actualNameCopy = util_strsav(actualName);

  st_insert(network->formalNameToActualName, formalNameCopy, actualNameCopy);
}


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

  Synopsis    [Returns the number of nodes of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPrimaryInputs Ntk_NetworkReadNumLatches]

******************************************************************************/
int
Ntk_NetworkReadNumNodes(
  Ntk_Network_t * network)
{
  return (lsLength(network->nodes));
}


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

  Synopsis    [Returns the number of latches of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumNodes Ntk_NetworkReadNumPrimaryInputs]

******************************************************************************/
int
Ntk_NetworkReadNumLatches(
  Ntk_Network_t * network)
{
  return (lsLength(network->latches));
}


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

  Synopsis    [Returns the number of combinational inputs of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumNodes Ntk_NetworkReadNumLatches]

******************************************************************************/
int
Ntk_NetworkReadNumCombInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->combInputs));
}


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

  Synopsis    [Returns the number of combinational outputs of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadCombOutputs Ntk_NetworkReadNumNodes
  Ntk_NetworkReadNumLatches]

******************************************************************************/
int
Ntk_NetworkReadNumCombOutputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->combOutputs));
}


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

  Synopsis    [Returns the number of primary inputs of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPseudoInputs Ntk_NetworkReadNumInputs]

******************************************************************************/
int
Ntk_NetworkReadNumPrimaryInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->primaryInputs));
}


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

  Synopsis    [Returns the number of pseudo inputs of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPrimaryInputs Ntk_NetworkReadNumInputs]

******************************************************************************/
int
Ntk_NetworkReadNumPseudoInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->pseudoInputs));
}


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

  Synopsis    [Returns the number of inputs (primary plus pseudo) of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPrimaryInputs Ntk_NetworkReadNumPseudoInputs]

******************************************************************************/
int
Ntk_NetworkReadNumInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->inputs));
}


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

  Synopsis    [Returns the number of primary outputs of a network.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumNodes Ntk_NetworkReadNumLatches]

******************************************************************************/
int
Ntk_NetworkReadNumPrimaryOutputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->primaryOutputs));
}


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

  Synopsis    [Returns the list of nodes of a network.]

  Description [Returns the list of all the nodes of a network.  The application
  must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumNodes]

******************************************************************************/
lsList
Ntk_NetworkReadNodes(
  Ntk_Network_t * network)
{
  return (network->nodes);
}


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

  Synopsis    [Returns the list of combinational inputs of a network.]

  Description [Returns the list of combinational inputs of a network.  The
  application must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumCombInputs]

******************************************************************************/
lsList
Ntk_NetworkReadCombInputs(
  Ntk_Network_t * network)
{
  return (network->combInputs);
}


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

  Synopsis    [Returns the list of combinational outputs of a network.]

  Description [Returns the list of combinational outputs of a network.  A node
  can appear at most once in this list (e.g. even if a node serves as the data
  input for more than one latch, it appears just once in this list). The
  application must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumCombOutputs]

******************************************************************************/
lsList
Ntk_NetworkReadCombOutputs(
  Ntk_Network_t * network)
{
  return (network->combOutputs);
}


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

  Synopsis    [Returns the list of latches of a network.]

  Description [Returns the list of latches of a network.  The application must
  not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumLatches]

******************************************************************************/
lsList
Ntk_NetworkReadLatches(
  Ntk_Network_t * network)
{
  return (network->latches);
}


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

  Synopsis    [Returns the list of primary inputs of a network.]

  Description [Returns the list of primary inputs of a network.  The application
  must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPrimaryInputs]

******************************************************************************/
lsList
Ntk_NetworkReadPrimaryInputs(
  Ntk_Network_t * network)
{
  return (network->primaryInputs);
}


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

  Synopsis    [Returns the list of pseudo inputs of a network.]

  Description [Returns the list of pseudo inputs of a network.  The application
  must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPseudoInputs]

******************************************************************************/
lsList
Ntk_NetworkReadPseudoInputs(
  Ntk_Network_t * network)
{
  return (network->pseudoInputs);
}


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

  Synopsis    [Returns the list of primary and pseudo inputs of a network.]

  Description [Returns the list of primary and pseudo inputs of a network.  The
  application must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumInputs]

******************************************************************************/
lsList
Ntk_NetworkReadInputs(
  Ntk_Network_t * network)
{
  return (network->inputs);
}


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

  Synopsis    [Returns the list of primary outputs of a network.]

  Description [Returns the list of primary outputs of a network.  The application
  must not free or modify this list in any way.]

  SideEffects []

  SeeAlso     [Ntk_NetworkReadNumPrimaryOutputs]

******************************************************************************/
lsList
Ntk_NetworkReadPrimaryOutputs(
  Ntk_Network_t * network)
{
  return (network->primaryOutputs);
}


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

  Synopsis    [Associates application specified data with a network.]

  Description [Adds the key/data pair to the network's applInfoTable. Key may
  be an arbitrary string; to avoid possible conflicts with other applications,
  key should be prefixed with the application's package name, for example
  "Pkg_NetworkApplKey".  The contents of data are arbitrary; the network
  package does not interpret the data. The freeFn is called on data when a
  network is freed, or when Ntk_NetworkFreeApplInfo is called with the same
  value of key. The freeFn takes (void *) as its only argument, and returns
  void.  A copy is made of the string key before it is inserted into
  applInfoTable.<p>

  If this function is called with a key that already exists in the
  applInfoTable, then the data for the previous entry is freed using the
  freeFn, a new entry is created using the freeFn and data supplied as
  arguments, and TRUE is returned. Otherwise, FALSE is returned.<p>

  WARNING:  This function does not make a copy of data before inserting it
  into the table.  By calling this function, the application is surrendering
  responsibility to the network to free the data.  Once this function is
  called on data, the data should be freed only by calling
  Ntk_NetworkFreeApplInfo or Ntk_NetworkFree.  In other words, it is an error
  for the application to explicitly free the data without using one of these
  two functions. </p>]

  SideEffects []

  SeeAlso     [Ntk_NetworkFreeApplInfo Ntk_NetworkReadApplInfo]

******************************************************************************/
boolean
Ntk_NetworkAddApplInfo(
  Ntk_Network_t * network,
  char * key,
  Ntk_ApplInfoFreeFn  freeFn,
  void * data)
{
  ApplInfo_t *applInfo;
  boolean     status;

  if (st_lookup(network->applInfoTable, key, &applInfo)) {
    (*applInfo->freeFn)(applInfo->data);
    status = TRUE;
  }
  else {
    char *keyCopy = util_strsav(key);

    applInfo = ALLOC(ApplInfo_t, 1);
    st_insert(network->applInfoTable, keyCopy, (char *) applInfo);
    status = FALSE;
  }

  applInfo->freeFn = freeFn;
  applInfo->data   = data;
  return status;
}

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

  Synopsis    [Set application specified data with a network.]

  Description [Same as Ntk_NetworkAddApplInfo, but this function simply set
  the ApplInfo without checking/freeing if there already exists one. Instead,
  the caller should take care of that case.]

  SeeAlso     [Ntk_NetworkFreeApplInfo Ntk_NetworkAddApplInfo]

  SideEffects [ApplInfo of the argument network is modified]

******************************************************************************/
boolean
Ntk_NetworkSetApplInfo(
  Ntk_Network_t * network,
  char * key,
  Ntk_ApplInfoFreeFn  freeFn,
  void * data)
{
  ApplInfo_t *applInfo;
  boolean     status;

  if (st_lookup(network->applInfoTable, key, &applInfo)) {
    status = TRUE;
  }
  else {
    char *keyCopy = util_strsav(key);

    applInfo = ALLOC(ApplInfo_t, 1);
    st_insert(network->applInfoTable, keyCopy, (char *) applInfo);
    status = FALSE;
  }

  applInfo->freeFn = freeFn;
  applInfo->data   = data;
  return status;
}


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

  Synopsis    [Returns data corresponding to key if it exists, else returns NULL.]

  Description [If data corresponding to key is associated to the network, then
  returns a pointer to data (as void *).  Otherwise, returns NULL.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAddApplInfo Ntk_NetworkFreeApplInfo]

******************************************************************************/
void *
Ntk_NetworkReadApplInfo(
  Ntk_Network_t * network,
  char * key)
{
  int         status;
  ApplInfo_t *applInfo;

  status = st_lookup(network->applInfoTable, key, &applInfo);
  if (status == 1) {
    return (applInfo->data);
  }
  else {
    return (NIL(void));
  }
}


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

  Synopsis    [Frees application-specified data from a network.]

  Description [If data corresponding to key exists in the network, then frees
  the data using the associated free function, removes the key/data pair from
  the network's applInfoTable, and returns TRUE.  If key does not exist, then
  the function does nothing and returns FALSE.
  <p>
  WARNING: This function should be called only if a corresponding call to
  Ntk_NetworkAddApplInfo has already been made.</p>]

  SideEffects []

  SeeAlso     [Ntk_NetworkAddApplInfo Ntk_NetworkReadApplInfo]

******************************************************************************/
boolean
Ntk_NetworkFreeApplInfo(
  Ntk_Network_t * network,
  char * key)
{
  int         status;
  ApplInfo_t *applInfo;

  status = st_lookup(network->applInfoTable, key, &applInfo);

  if (status == 1) {
    st_delete(network->applInfoTable, &key, &applInfo);
    (*applInfo->freeFn)(applInfo->data);
    FREE(key);  /* frees the string contained in the table */
    FREE(applInfo);
  }

  return ((status) ? TRUE : FALSE);
}


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

  Synopsis    [Allocates a network with a name.]

  Description [Allocates a network with a name (a copy of name is made
  first). Name must be non-NULL.  The remaining fields are initialized to
  empty (e.g. empty lists, empty hash tables) or NULL (mddManager). The
  dynVarOrdMethod is set to BDD_REORDER_NONE.]

  SideEffects []

  SeeAlso     [Ntk_NetworkFree]

******************************************************************************/
Ntk_Network_t *
Ntk_NetworkAlloc(
  char * name)
{
  Ntk_Network_t *network = ALLOC(Ntk_Network_t, 1);

  network->name                   = util_strsav(name);
  network->nodes                  = lsCreate();
  network->combInputs             = lsCreate();
  network->combOutputs            = lsCreate();
  network->latches                = lsCreate();
  network->primaryInputs          = lsCreate();
  network->pseudoInputs           = lsCreate();
  network->inputs                 = lsCreate();
  network->primaryOutputs         = lsCreate();
  network->combOutputsTable       = st_init_table(st_ptrcmp, st_ptrhash);
  network->mddIdToNode            = st_init_table(st_numcmp, st_numhash);
  network->actualNameToNode       = st_init_table(strcmp, st_strhash);
  network->formalNameToActualName = st_init_table(strcmp, st_strhash);
  network->applInfoTable          = st_init_table(strcmp, st_strhash);
  network->mddManager             = NIL(mdd_manager);
  network->mAigManager            = NIL(mAig_Manager_t);
  network->dynVarOrdMethod        = BDD_REORDER_NONE;
  network->undef                  = NIL(void);

  return network;
}


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

  Synopsis    [Frees all the memory associated with a network.]

  Description [Calls Ntk_NodeFree on each node of network, and then frees the
  data local to network, and the network itself.  Also frees the MDD manager
  of the network, if it is not NULL. If network is NULL, just returns.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAlloc Ntk_NodeFree]

******************************************************************************/
void
Ntk_NetworkFree(
  Ntk_Network_t * network)
{
  char *formal;
  char *actual;
  char *key;
  ApplInfo_t *applInfo;
  Ntk_Node_t *node;
  lsGen gen;
  st_generator *stGen;


  if (network == NIL(Ntk_Network_t)) {
    return;
  }

  FREE(network->name);

  Ntk_NetworkForEachNode(network, gen, node) {
    Ntk_NodeFree(node);
  }

  (void) lsDestroy(network->nodes,           (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->combInputs,      (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->combOutputs,     (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->latches,         (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->primaryInputs,   (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->pseudoInputs,    (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->inputs,          (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->primaryOutputs,  (void (*) (lsGeneric)) NULL);
  st_free_table(network->combOutputsTable);
  st_free_table(network->mddIdToNode);

  /*
   * The keys in this table are strings representing node names.  The strings
   * are owned by the nodes, so we don't free them here.
   */
  st_free_table(network->actualNameToNode);

  /*
   * Free all the strings in the formalNameToActualName table before freeing
   * the table itself.
   */
  st_foreach_item(network->formalNameToActualName, stGen, &formal, &actual) {
    FREE(formal);
    FREE(actual);
  }

  st_free_table(network->formalNameToActualName);

  /*
   * Free all the key/applInfo pairs in the applInfoTable, and then free the
   * table itself.
   */
  st_foreach_item(network->applInfoTable, stGen, &key, &applInfo) {
    FREE(key);
    (*applInfo->freeFn)(applInfo->data);
    FREE(applInfo);
  }
  st_free_table(network->applInfoTable);

  if (network->mddManager != NIL(mdd_manager)) {
    mdd_quit(network->mddManager);
  }

  if (network->mAigManager != NIL(mAig_Manager_t)) {
    mAig_quit(network->mAigManager);
  }
  FREE(network);
}


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

  Synopsis    [Callback function to free a network.]

  Description [Typecasts data to (Ntk_Network_t *) and then calls
  Ntk_NetworkFree.  This function should only be used as a callback for other
  applications that don't know the network type, for example the Hrc_Node
  ApplInfoTable.]

  SideEffects []

  SeeAlso     [Ntk_NetworkFree]

******************************************************************************/
void
Ntk_NetworkFreeCallback(
  void * data /* an object of type Ntk_Network_t*  type casted to void* */)
{
  Ntk_NetworkFree((Ntk_Network_t *) data);
}


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

  Synopsis    [Write a network in blif-MV format to a file.]

  Description [Work in progress.  Still bogus in one major way:
  Equal entries in tables use formal names.]

  SideEffects [none]

  SeeAlso     [Ntk_NetworkPrint Hrc_ModelWriteBlifMv]

******************************************************************************/
void
Ntk_NetworkWriteBlifMv(
  FILE *fp,
  Ntk_Network_t *network,
  boolean promotePseudo
  )
{
  lsGen gen;
  Ntk_Node_t *node;
  int i;

  (void) fprintf(fp, ".model %s\n", Ntk_NetworkReadName(network));

  /* .inputs */
  if (Ntk_NetworkReadNumPrimaryInputs(network) != 0) {
    (void) fprintf(fp, ".inputs");
    Ntk_NetworkForEachPrimaryInput(network, gen, node) {
      (void) fprintf(fp, " %s", Ntk_NodeReadName(node));
    }
    (void) fprintf(fp, "\n");
  }

  if (promotePseudo && Ntk_NetworkReadNumPseudoInputs(network) != 0) {
    (void) fprintf(fp, "# pseudo inputs\n");
    (void) fprintf(fp, ".inputs");
    Ntk_NetworkForEachPseudoInput(network, gen, node) {
      (void) fprintf(fp, " %s", Ntk_NodeReadName(node));
    }
    (void) fprintf(fp, "\n");
  }

  /* .outputs */
  if (Ntk_NetworkReadNumPrimaryOutputs(network) != 0) {
    (void) fprintf(fp, ".outputs");
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
      (void) fprintf(fp, " %s", Ntk_NodeReadName(node));
    }
    (void) fprintf(fp, "\n");
  }

  /* .mv .names .latch .reset */
  Ntk_NetworkForEachNode(network, gen, node) {
    Var_Variable_t *var = Ntk_NodeReadVariable(node);
    char *nodeName = Ntk_NodeReadName(node);
    boolean is_enum = Var_VariableTestIsEnumerative(var);
    int range = Var_VariableReadNumValues(var);

    if (Ntk_NodeTestIsShadow(node)) continue;
    if (Ntk_NodeTestIsCombinational(node) &&
        Ntk_NodeTestIsLatchInitialInput(node)) continue;

    if (is_enum) {
      if (range != 2) {
        /* Boolean enumerative variables need no .mv declaration. */
        (void) fprintf(fp, ".mv %s %d\n", nodeName, range);
      }
    } else {
      /* Variable is symbolic. */
      (void) fprintf(fp, ".mv %s %d", nodeName, range);
      for (i = 0; i < range; i++) {
        (void) fprintf(fp, " %s",
                       Var_VariableReadSymbolicValueFromIndex(var, i));
      }
      (void) fprintf(fp, "\n");
    }
  }

  if (!promotePseudo && Ntk_NetworkReadNumPseudoInputs(network) != 0) {
    (void) fprintf(fp, "# pseudo inputs start\n");
    Ntk_NetworkForEachPseudoInput(network, gen, node) {
      Tbl_Table_t *dupTable = DuplicateTableAndVars(node,
                                                    Ntk_NodeReadName(node));
      Tbl_TableWriteBlifMvToFile(dupTable, 0, fp);
      Tbl_TableFree(dupTable);
    }
    (void) fprintf(fp, "# pseudo inputs end\n");
  }

  Ntk_NetworkForEachNode(network, gen, node) {

    if (Ntk_NodeTestIsShadow(node)) continue;
    if (Ntk_NodeTestIsCombinational(node) &&
        Ntk_NodeTestIsLatchInitialInput(node)) continue;

    if (Ntk_NodeTestIsCombinational(node)) {
      Tbl_Table_t *dupTable = DuplicateTableAndVars(node,
                                                    Ntk_NodeReadName(node));
      Tbl_TableWriteBlifMvToFile(dupTable, 0, fp);
      Tbl_TableFree(dupTable);
    } else if (Ntk_NodeTestIsLatch(node)) {
      Ntk_Node_t *data = Ntk_LatchReadDataInput(node);
      Ntk_Node_t *reset = Ntk_LatchReadInitialInput(node);
      Tbl_Table_t *dupTable = DuplicateTableAndVars(reset,
                                                    Ntk_NodeReadName(node));
      (void) fprintf(fp, ".latch %s %s\n", Ntk_NodeReadName(data),
                     Ntk_NodeReadName(node));
      Tbl_TableWriteBlifMvToFile(dupTable, 1, fp);
      Tbl_TableFree(dupTable);
    }
  }

  (void) fprintf(fp, ".end\n");

} /* Ntk_NetworkWriteBlifMv */


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

  Synopsis    [Prints information about a network.]

  Description [Prints name of network, and calls Ntk_NodePrint on each node of
  network.]

  SideEffects []

  SeeAlso     [Ntk_NodePrint]

******************************************************************************/
void
Ntk_NetworkPrint(
  FILE * fp,
  Ntk_Network_t * network,
  boolean printIo,
  boolean printTableStats)
{
  Ntk_Node_t *node;
  lsGen       gen;

  (void) fprintf(fp, "Nodes of network %s:\n", Ntk_NetworkReadName(network));

  Ntk_NetworkForEachNode(network, gen, node) {
    Ntk_NodePrint(fp, node, printIo, printTableStats);
    /*
     * It's nice to have a line separating nodes when we print the fanins and
     * fanouts or table stats.
     */
    if (printIo || printTableStats) {
      (void) fprintf(fp, "\n");
    }
  }
}


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

  Synopsis    [Prints statistics about a network.]

  Description [Prints the following information about a network: name, number
  of combinational nodes, number of primary inputs, number of primary outputs,
  number of latches.]

  SideEffects []

******************************************************************************/
void
Ntk_NetworkPrintStats(
  FILE * fp,
  Ntk_Network_t * network)
{
  lsGen          gen;
  Ntk_Node_t     *node;
  int            numConstants     = 0;
  int            numCombinational = 0;
  int            numEdges         = 0;
  mdd_manager  *mddMgr;

  /*
   * Count the number of constants and the number of combinational nodes.
   */
  Ntk_NetworkForEachNode(network, gen, node) {
    numEdges += Ntk_NodeReadNumFanouts(node);
    if (Ntk_NodeTestIsConstant(node)) {
      numConstants++;
    }
    if (Ntk_NodeTestIsCombinational(node)) {
      numCombinational++;
    }
  }

  mddMgr = Ntk_NetworkReadMddManager(network);

  if (mddMgr == NIL(mdd_manager)){
     (void) fprintf(fp, "%s  combinational=%d  pi=%d  po=%d  latches=%d  pseudo=%d  const=%d  edges=%d\n",
                 Ntk_NetworkReadName(network),
                 numCombinational,
                 Ntk_NetworkReadNumPrimaryInputs(network),
                 Ntk_NetworkReadNumPrimaryOutputs(network),
                 Ntk_NetworkReadNumLatches(network),
                 Ntk_NetworkReadNumPseudoInputs(network),
                 numConstants,
                 numEdges
                 );
  }else{
     array_t *bddIdArray;
     lsGen gen;
     Ntk_Node_t *latch;
     int n_boolean_latches;
     array_t *mddIdArray = array_alloc(int, 0);

     Ntk_NetworkForEachLatch(network, gen, latch){
       array_insert_last(int, mddIdArray, Ntk_NodeReadMddId(latch));
     }

     bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, mddIdArray);
     n_boolean_latches = array_n(bddIdArray);
     array_free(mddIdArray);
     array_free(bddIdArray);

     (void) fprintf(fp, "%s  combinational=%d  pi=%d  po=%d  latches=%d (boolean_latches=%d)  pseudo=%d  const=%d  edges=%d\n",
                 Ntk_NetworkReadName(network),
                 numCombinational,
                 Ntk_NetworkReadNumPrimaryInputs(network),
                 Ntk_NetworkReadNumPrimaryOutputs(network),
                 Ntk_NetworkReadNumLatches(network),
                 n_boolean_latches,
                 Ntk_NetworkReadNumPseudoInputs(network),
                 numConstants,
                 numEdges
                 );
  }
}


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

  Synopsis    [Duplicates a network.]

  Description [Duplicates a network.  The network name and all node names are
  preserved.  The new network does not have an MDD manager.  The nodes of the
  new network have unassigned MDD ids.  The tables (Tbl_Table_t) of the new
  nodes are "soft duplicates" of the original tables in oldNetwork; they
  should not be modified.  The application information (ApplInfo) of the new
  network is empty.  The formalNameToActualName table of the new network is
  empty.]

  SideEffects []

  SeeAlso     [Ntk_NetworkFree Ntk_NetworkAppendNetwork]

******************************************************************************/
Ntk_Network_t *
Ntk_NetworkDuplicate(
  Ntk_Network_t * oldNetwork)
{
  int            i;
  lsGen          gen;
  Ntk_Node_t    *oldNode;
  Ntk_Node_t    *oldFaninNode;
  Ntk_Node_t    *oldOriginNode;
  Ntk_Node_t    *newOriginNode;
  array_t       *faninNameArray;
  Ntk_Network_t *newNetwork = Ntk_NetworkAlloc(Ntk_NetworkReadName(oldNetwork));


  /*
   * For each node in oldNetwork, create a node in newNetwork.
   */
  Ntk_NetworkForEachNode(oldNetwork, gen, oldNode) {
    (void) Ntk_NodeCreateInNetwork(newNetwork, Ntk_NodeReadName(oldNode),
                                   Ntk_NodeReadVariable(oldNode));
  }

  /*
   * For each node in oldNetwork, declare the corresponding node in newNetwork
   * using the type of the oldNode.
   */
  Ntk_NetworkForEachNode(oldNetwork, gen, oldNode) {
    char       *nodeName = Ntk_NodeReadName(oldNode);
    Ntk_Node_t *newNode  = Ntk_NetworkFindNodeByActualName(newNetwork, nodeName);
    assert(newNode != NIL(Ntk_Node_t));

    /*
     * Handle items that are independent of node type.
     */
    if (Ntk_NodeTestIsPrimaryOutput(oldNode)) {
      Ntk_NodeDeclareAsPrimaryOutput(newNode);
    }

    switch (oldNode->type) {
      case NtkPrimaryInput_c:
        Ntk_NodeDeclareAsPrimaryInput(newNode);
        break;
      case NtkPseudoInput_c:
        Ntk_NodeDeclareAsPseudoInput(newNode,
                                     Tbl_TableSoftDup(Ntk_NodeReadTable(oldNode)),
                                     Ntk_NodeReadOutputIndex(oldNode));
        break;
      case NtkLatch_c:
        Ntk_NodeDeclareAsLatch(newNode,
                               Ntk_NodeReadName(Ntk_LatchReadDataInput(oldNode)),
                               Ntk_NodeReadName(Ntk_LatchReadInitialInput(oldNode)));
        break;
      case NtkCombinational_c:
        /*
         * Create the array of names of the fanins of oldNode.
         */
        faninNameArray = array_alloc(char *, Ntk_NodeReadNumFanins(oldNode));
        Ntk_NodeForEachFanin(oldNode, i, oldFaninNode) {
          char *faninName = Ntk_NodeReadName(oldFaninNode);
          array_insert(char *, faninNameArray, i, faninName);
        }

        Ntk_NodeDeclareAsCombinational(newNode,
                                       Tbl_TableSoftDup(Ntk_NodeReadTable(oldNode)),
                                       faninNameArray,
                                       Ntk_NodeReadOutputIndex(oldNode));
        array_free(faninNameArray);
        break;
      case NtkShadow_c:
        oldOriginNode = Ntk_ShadowReadOrigin(oldNode);
        newOriginNode = Ntk_NetworkFindNodeByActualName(newNetwork,
                                                        Ntk_NodeReadName(oldOriginNode));
        Ntk_NodeDeclareAsShadow(newNode, newOriginNode);
        break;
      case NtkUnassigned_c:
        fail("Unexpected unassigned node type");
        break;
      default:
        fail("Unexpected type");
        break;
    }
  }

  return (newNetwork);
}


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

  Synopsis    [Appends network2 to network1.]

  Description [Appends network2 to network1. Network2 is not modified, but
  network1 is modified.  Name1ToName2 is a hash table mapping char* keys to
  char* values (the table should use st_strhash and strcmp). The set of keys
  is an arbitrary subset (including empty set) of the set of names of the
  inputs (primary and pseudo) of network2.  The value of each key is the name
  of an arbitrary node in network1.<p>

  The inputs of network2 can be divided into 3 types: I - those appearing in
  name2ToName1 as keys, II - those not appearing in name2ToName1, but which
  have nodes with the same names in network1, and III - all other inputs
  (i.e. those neither appearing in name2ToName1, nor having nodes of the same
  names in network1).  An input of type II could be equivalently specified as a
  type I input, where the key and value are the same.  If there are no type I
  inputs, an empty symbol table should be provided.<p>

  A node of network2 is appended to network1 if it is a type III input, or it
  is not an input.  All appended nodes have the string $NTK2 added to the end
  of their names.  Inputs of type I or II are not appended to network1.  When
  a node of network2 is appended to network1, if there exists a fanin of the
  node that is a type I or II input, then that fanin is modified to refer to
  the node in network1 corresponding to the type I or II.  The MDD ids of the
  appended nodes are unassigned.  The tables of the appended nodes are "soft
  duplicates" of the original tables in network2; they should not be
  modified.<p>

  Note that it is impossible for the set of fanins of a node (originally) in
  network1 to be modified.  The only changes that occur to the original nodes
  of network1 are that the fanout sets will increase for those nodes
  corresponding to type I or II inputs of network2.<p>

  The application information of network1 is not modified; the information
  should be invalidated by the caller as necessary.  The MDD manager of
  network1 is not modified in any way.  The formalNameToActualName table of
  network1 is not updated to reflect the addition of the nodes from network2.
  Currently, it is assumed that type I and II inputs do not have shadow
  nodes.

  !!! Chao Says: I have changed all the FindNodeByActualName with
                 FindNodeByName, since the later one subsume the former.
      replace  Ntk_NetworkFindNodeByActualName(network1, name1);
      with     Ntk_NetworkFindNodeByName(network1, name1);
  ]

  SideEffects [Network1 is modified.]

  SeeAlso     [Ntk_NetworkDuplicate Ntk_NetworkFreeApplInfo]

******************************************************************************/
void
Ntk_NetworkAppendNetwork(
  Ntk_Network_t * network1,
  Ntk_Network_t * network2,
  st_table *name2ToName1)
{
  st_generator *stGen;
  lsGen         gen;
  Ntk_Node_t   *node1;
  Ntk_Node_t   *node2;
  char         *name1;
  char         *name2;
  st_table     *localName2ToName1 = st_init_table(strcmp, st_strhash);


  /*
   * For each node in network2, create a node in network1 as necessary. The
   * undef field of node2 is set to TRUE if a new node is created in network1
   * for it; else, it is set to FALSE. localName2ToName1 is a superset of
   * name2ToName1; in addition to the contents of name2ToName1, it contains
   * the new names (those appended with $NTK2) for those nodes being appended
   * to network2, and type II inputs.
   */
  Ntk_NetworkForEachNode(network2, gen, node2) {
    name1 = NIL(char);
    name2 = Ntk_NodeReadName(node2);
    st_lookup(name2ToName1, name2, &name1);
    if (name1 != NIL(char)) {
      /*
       * Name2 is in name2ToName1 table (type I input).  Hence, we will be
       * using the node in network1 corresponding to name1.  Assert that node2
       * is in fact an input, that name1 refers to an input node in network1, and
       * that node1 and node2 have the same variable domains.
       */
      Ntk_NodeSetUndef(node2, (void *) FALSE);
      st_insert(localName2ToName1, name2, util_strsav(name1));

      assert(Ntk_NodeTestIsInput(node2));
      node1 = Ntk_NetworkFindNodeByName(network1, name1);
      assert(node1 != NIL(Ntk_Node_t));
      assert(Var_VariablesTestHaveSameDomain(Ntk_NodeReadVariable(node1),
                                             Ntk_NodeReadVariable(node2)));
    }
    else {
      /*
       * Name2 is *not* in name2ToName1 table.  There are 2 possibilities: 1)
       * a node with name2 already exists in network1, and node2 is an input
       * (type II input); in this case, a) add map of name2 to name2 in the
       * localName2ToName1, b) assert that node1 is in fact an input, and c)
       * don't create a new node in network1; 2) a node with name2 doesn't
       * exist in network1, or node2 is not an input (type III inputs and
       * non-inputs); in this case, we unconditionally create a new node in
       * network1 using name2$NTK2.
       */
      node1 = Ntk_NetworkFindNodeByName(network1, name2);

      if ((node1 != NIL(Ntk_Node_t)) && Ntk_NodeTestIsInput(node2)) {
        Ntk_NodeSetUndef(node2, (void *) FALSE);
        st_insert(localName2ToName1, name2, util_strsav(name2));
      }
      else {
        char *newName = util_strcat3(name2, "$NTK2", "");
        Ntk_NodeSetUndef(node2, (void *) TRUE);
        st_insert(localName2ToName1, name2, newName);
        (void) Ntk_NodeCreateInNetwork(network1, newName,
                                       Ntk_NodeReadVariable(node2));
      }
    }
  }

  /*
   * For each node in network2 for which a new node was created in network1,
   * declare the corresponding node in network1 using the type of the node2.
   * (NOTE: this section shares a lot with Ntk_NetworkDuplicate, but is
   * sufficiently different that we don't share any code.)
   */
  Ntk_NetworkForEachNode(network2, gen, node2) {
    if (Ntk_NodeReadUndef(node2) == NIL(void)) {
      /*
       * node2 is superseded by a node in network1.
       */
      continue;
    }

    name2 = NodeReadNameFromTable(node2, localName2ToName1);
    node1 = Ntk_NetworkFindNodeByName(network1, name2);
    assert(node1 != NIL(Ntk_Node_t));

    /*
     * Handle items that are independent of node type.
     */
    if (Ntk_NodeTestIsPrimaryOutput(node2)) {
      Ntk_NodeDeclareAsPrimaryOutput(node1);
    }

    switch (node2->type) {
      case NtkPrimaryInput_c:
        Ntk_NodeDeclareAsPrimaryInput(node1);
        break;

      case NtkPseudoInput_c:
        Ntk_NodeDeclareAsPseudoInput(node1,
                                     Tbl_TableSoftDup(Ntk_NodeReadTable(node2)),
                                     Ntk_NodeReadOutputIndex(node2));
        break;

      case NtkLatch_c:
      {
        char *dataName = NodeReadNameFromTable(Ntk_LatchReadDataInput(node2),
                                               localName2ToName1);
        char *initName = NodeReadNameFromTable(Ntk_LatchReadInitialInput(node2),
                                               localName2ToName1);

        Ntk_NodeDeclareAsLatch(node1, dataName, initName);
        break;
      }

      case NtkCombinational_c:
      {
        int         i;
        Ntk_Node_t *faninNode2;
        array_t    *faninNameArray;

        /*
         * Create the array of names of the fanins of node2.
         */
        faninNameArray = array_alloc(char *, Ntk_NodeReadNumFanins(node2));
        Ntk_NodeForEachFanin(node2, i, faninNode2) {
          char *faninName = NodeReadNameFromTable(faninNode2, localName2ToName1);
          array_insert(char *, faninNameArray, i, faninName);
        }

        Ntk_NodeDeclareAsCombinational(node1,
                                       Tbl_TableSoftDup(Ntk_NodeReadTable(node2)),
                                       faninNameArray,
                                       Ntk_NodeReadOutputIndex(node2));
        array_free(faninNameArray);
        break;
      }

      case NtkShadow_c:
      {
        char       *originName;
        Ntk_Node_t *originNode2;
        Ntk_Node_t *originNode1;

        originNode2 = Ntk_ShadowReadOrigin(node2);
        /*
         * Currently, we don't allow a shadow node whose origin in a type I or
         * II input.  This is because, what if the corresponding node in
         * network1 (of the type I or II input), also has a shadow node?  Then
         * we would try to add a shadow node to a node already having a shadow;
         * this is illegal.
         */
        assert((boolean) (long) Ntk_NodeReadUndef(node2));
        originName = NodeReadNameFromTable(originNode2, localName2ToName1);
        originNode1 = Ntk_NetworkFindNodeByName(network1, originName);

        Ntk_NodeDeclareAsShadow(node1, originNode1);
        break;
      }

      case NtkUnassigned_c:
        fail("Unexpected unassigned node type");
        break;
      default:
        fail("Unexpected type");
        break;
    }
  }

  /*
   * Free all the values strings in the localName2ToName1, before freeing
   * the table itself.  The keys are not freed.
   */
  st_foreach_item(localName2ToName1, stGen, &name2, &name1) {
    FREE(name1);
  }
  st_free_table(localName2ToName1);
}


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

  Synopsis [print a description of the topology of the network in dot format]

  Description [The format used for the description is <b>dot</b>, a tool for
  graph visualization developed at AT&T. It can be obtained from <a
  href="http://www.research.att.com/orgs/ssr/book/reuse">
  http://www.research.att.com/orgs/ssr/book/reuse</a>. The function
  receives as a parameter a file pointer in case the print wants to be
  redirected. This function is used by the command routine
  CommandPrintNetworkDot.]

  SideEffects []

******************************************************************************/
int
Ntk_NetworkPrintDot(
  FILE *fp,
  Ntk_Network_t *network)
{
  lsGen       gen;
  int i;
  Ntk_Node_t *nodePtr;
  Ntk_Node_t *fanoutPtr;
  time_t      now           = time(0);
  struct tm  *nowStructPtr  = localtime(& now);
  char       *nowTxt        = asctime(nowStructPtr);
  char       *networkName   = Ntk_NetworkReadName(network);

  /*
   * Write out the header for the output file.
   */

  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
  (void) fprintf(fp, "# network name: %s\n", networkName);
  (void) fprintf(fp, "# generated: %s", nowTxt);
  (void) fprintf(fp, "#\n");

  (void) fprintf(fp, "# Network with %d nodes\n",
                 Ntk_NetworkReadNumNodes(network));

  (void) fprintf(fp, "digraph \"%s\" {\n  rotate=90;\n", networkName);
  (void) fprintf(fp, "  margin=0.5;\n  label=\"%s\";\n", networkName);
  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");

  /* Force the inputs and outputs to be printed at the same level in the graph */
  (void) fprintf(fp, "  { rank=same; ");
  Ntk_NetworkForEachCombInput(network,gen, nodePtr) {
    (void) fprintf(fp, "\"%s\"; ", Ntk_NodeReadName(nodePtr));
  }
  (void) fprintf(fp, "}\n");
  (void) fprintf(fp, "  { rank=same; ");
  Ntk_NetworkForEachCombOutput(network,gen, nodePtr) {
    (void) fprintf(fp, "\"%s\"; ", Ntk_NodeReadName(nodePtr));
  }
  (void) fprintf(fp, "}\n");

  /* Print all the edges */
  Ntk_NetworkForEachNode(network, gen, nodePtr) {

    if (Ntk_NodeReadNumFanouts(nodePtr) == 0 &&
        Ntk_NodeReadNumFanins(nodePtr) == 0) {
      /* Print the dot description for a node */
      (void) fprintf(fp, "  \"%s\";\n", Ntk_NodeReadName(nodePtr));
    } /* End of if */

    /* Print the edges comming out of that node */
    Ntk_NodeForEachFanout(nodePtr, i, fanoutPtr) {
      (void) fprintf(fp, "  \"%s\" -> \"%s\";\n", Ntk_NodeReadName(nodePtr),
                     Ntk_NodeReadName(fanoutPtr));
    }
  }

  (void) fprintf(fp, "}\n");

  return 1;
}

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

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

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

  Synopsis    [Returns node name from table.]

  Description [Given a node, uses the name of the node as key to lookup the
  corresponding (new) name for the node.  If the node does not exist as a key
  in the table, then fails.  The returned string should not be freed.]

  SideEffects []

******************************************************************************/
static char *
NodeReadNameFromTable(
  Ntk_Node_t *node,
  st_table *name2ToName1)
{
  char    *name1  = NIL(char);
  char    *name2  = Ntk_NodeReadName(node);
  boolean  status UNUSED = st_lookup(name2ToName1, name2, &name1);

  assert(status);
  return name1;
}


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

  Synopsis    [Duplicate a table and corresponding variables.]

  Description []

  SideEffects []

  SeeAlso []

******************************************************************************/
static Tbl_Table_t *
DuplicateTableAndVars(
  Ntk_Node_t *node,
  char *name
  )
{
  Var_Variable_t *var, *newVar;
  Tbl_Table_t *dupTable, *tbl;
  int col;
  Tbl_Table_t *table = Ntk_NodeReadTable(node);
  array_t *split = Tbl_TableSplit(table);
  int outIndex = Ntk_NodeReadOutputIndex(node);

  arrayForEachItem(Tbl_Table_t *, split, col, tbl) {
    if (col == outIndex) {
      dupTable = tbl;
    } else {
      Tbl_TableFree(tbl);
    }
  }
  array_free(split);

  Tbl_TableForEachInputVar(dupTable, col, var) {
    Ntk_Node_t *fanin = Ntk_NodeReadFaninNode(node, col);
    char *newName = Ntk_NodeReadName(fanin);
    newVar = Var_VariableDup(var, NIL(Hrc_Node_t));
    Var_VariableChangeName(newVar, newName);
    Tbl_TableSetVar(dupTable, col, newVar, 0);
  }

  var = array_fetch(Var_Variable_t *,Tbl_TableReadOutputVars(dupTable), 0);
  newVar = Var_VariableDup(var, NIL(Hrc_Node_t));
  Var_VariableChangeName(newVar, name);
  Tbl_TableSetVar(dupTable, 0, newVar, 1);

  return dupTable;

} /* DuplicateTableAndVars */