source: vis_dev/vis-2.3/src/ord/ordMain.c @ 36

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

  FileName    [ordMain.c]

  PackageName [ord]

  Synopsis    [Routines for static ordering of MDD variables.]

  Author      [Adnan Aziz, Tom Shiple, Serdar Tasiran]

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

static char rcsid[] UNUSED = "$Id: ordMain.c,v 1.17 2005/04/16 06:15:25 fabio Exp $";

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

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

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

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

static int NodesCompareDepth(Ntk_Node_t *node1, Ntk_Node_t *node2);
static long NodeComputeDepth(Ntk_Node_t * node);
static void NetworkAddDanglingNodesToOrderList(Ntk_Network_t * network, lsList nodeOrderList, st_table *nodeToHandle);
static void NetworkAddNSVarsToOrderList(Ntk_Network_t * network, lsList nodeOrderList, st_table *nodeToHandle, boolean nsAfterSupport);
static lsList LatchNSListConvertToLatchDataInputList(lsList latchNSList);
static void NodeSetDepth(Ntk_Node_t * node, long depth);
static void MddGroupVariables(mdd_manager *mddMgr, int initMddId, int blockSize);

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


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

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

  Synopsis    [Orders the MDD variables of a network.]

  Description [Orders the MDD variables of a network.  The ordering is based
  solely on the topology of the network; the binary variables that make up the
  MDD variables are not interleaved. OutputOrderType can be either Ord_All_c
  or Ord_InputAndLatch_c. If it is Ord_All_c, then every node (and latch NS)
  in the network is assigned an MDD id.  If it is Ord_InputAndLatch_c, then
  every primary input, pseudo input, latch, and latch NS is assigned an MDD
  id.<p>

  SuppliedOrderType can be any value of Ord_OrderType.  If it is Ord_All_c or
  Ord_InputAndLatch_c, then suppliedNodeList must give an ordering of the
  network nodes (included in the set specified by suppliedOrderType).
  Otherwise, Ord_NetworkOrderNodes is called, with the same arguments as this
  function, to compute an ordering of the network nodes.  In any case, the
  ordering of nodes is projected onto the set specified by generatedOrderType,
  and MDD ids are assigned (in order) to the nodes in the projection.  The
  starting MDD id is the total number of variables currently in the MDD
  manager of the network.  An MDD manager is created for the network if one
  doesn't already exist.<p>

  No checks are made to insure that suppliedNodeList contains what is implied
  by the value of suppliedOrderType.  The MDD ids of nodes not specified by
  generatedOrderType are unaffected.<p>

  If nsAfterSupport is TRUE, then for a given latch, its next state variable
  is ordered just after the variables in the support of the latch's
  corresponding dataInput function. <p>

  If nsAfterSupport is FALSE, then for a given latch, its NS variable is
  ordered just after the corresponding present state variable. In this case,
  the ps variable and the ns variable are grouped together in the variable
  ordering, so that when reordering is performed they remain adjacent in the
  new variable ordering. Similarly, when an ordering is read from a file, NS
  variables immediately following corresponding PS variables are grouped
  together.<p>]

  SideEffects [Writes over the MDD id field of nodes.]

  SeeAlso [Ord_NetworkOrderNodes]
  
******************************************************************************/
void
Ord_NetworkOrderVariables(
  Ntk_Network_t *network,
  Ord_RootMethod rootOrderMethod,
  Ord_NodeMethod nodeOrderMethod,
  boolean        nsAfterSupport,
  Ord_OrderType  generatedOrderType /* Ord_All_c or Ord_InputAndLatch_c */,
  Ord_OrderType  suppliedOrderType /* no restrictions */,
  lsList         suppliedNodeList /* list of nodes Ntk_Node_t* from ordering file */,
  int            verbose)
{
  lsList totalOrderList;      /* list of nodes (Ntk_Node_t *) */
  long   initialTime = util_cpu_time();
  
  /*
   * The condition where suppliedOrderType==InputAndLatch and
   * generatedOrderType==All is not currently allowed because we're not sure
   * if it's useful.
   */
  assert(!((suppliedOrderType == Ord_InputAndLatch_c)
           && (generatedOrderType == Ord_All_c))); 

  /*
   * Either get a total ordering of the network nodes from suppliedNodeList,
   * or compute it working from the network.
   */
  if ((suppliedOrderType == Ord_All_c)
      || (suppliedOrderType == Ord_InputAndLatch_c)) {
    totalOrderList = lsCopy(suppliedNodeList,
                            (lsGeneric (*) (lsGeneric)) NULL);
  }
  else {
    totalOrderList = Ord_NetworkOrderNodes(network, rootOrderMethod,
                                           nodeOrderMethod, nsAfterSupport,
                                           generatedOrderType,
                                           suppliedOrderType,
                                           suppliedNodeList, 
                                           verbose);
  }
    

  OrdNetworkAssignMddIds(network, generatedOrderType, totalOrderList, nsAfterSupport);
  (void) lsDestroy(totalOrderList, (void (*) (lsGeneric)) NULL);

  /*
   * If nsAfterSupport is FALSE, this implies that NS comes right after PS.
   *
   */
  if ( nsAfterSupport == FALSE ) {
    lsGen tmpGen;
    Ntk_Node_t *tmpLatch;
 
   /*
    * Iterate over each latch, and group the PS variable with the next
    * variable in the ordering, which is guaranteed to be the corresponding NS
    * variable.
    */
    Ntk_NetworkForEachLatch(network, tmpGen, tmpLatch) {
      mdd_manager *mddMgr = Ntk_NetworkReadMddManager( network );
          Ntk_Node_t *nsNode = Ntk_NodeReadShadow( tmpLatch );
      int psMddId = Ntk_NodeReadMddId( tmpLatch );
      int nsMddId = Ntk_NodeReadMddId( nsNode );

      /* 
       * Group size = 2 ( ps and ns )
       */
      if (nsMddId == (psMddId+1)) {
        MddGroupVariables(mddMgr, psMddId, 2);
      }
      /* Adnan's fix: See his mail to vis@ic on Oct 24, 1997 */
      if (nsMddId == (psMddId-1)) {
        MddGroupVariables(mddMgr, nsMddId, 2);
      }
    }
  }

  if (verbose > 0) {
    long finalTime = util_cpu_time();
    (void) fprintf(vis_stdout, "\nTotal ordering time = %2.1f\n",
                   (finalTime-initialTime)/1000.0);
  }
}


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

  Synopsis    [Orders the nodes of a network.]

  Description [Orders the nodes of a network. The ordering is based solely on
  the topology of the network, and is intended to be suitable for deriving an
  MDD variable ordering by extracting those nodes for which MDD variables are
  needed.  GeneratedOrderType can be either Ord_All_c or
  Ord_InputAndLatch_c. If it is Ord_All_c, then every node (and latch NS) in
  the network is ordered.  If it is Ord_InputAndLatch_c, then every primary
  input, pseudo input, latch, and latch NS is ordered. <p>

  SuppliedOrderType can be any of the following values: Ord_NextStateNode_c,
  Ord_Partial_c, or Ord_Unassigned_c.  If it is Ord_Unassigned_c, then
  suppliedNodeList is ignored, and there is no effect.  If it is *not*
  Ord_Unassigned_c, then suppliedNodeList must be a non-empty list of
  (pointers to) nodes. SuppliedNodeList can be used to specify the relative
  order of some or the nodes.<p>

  If suppliedOrderType is Ord_NextStateNode_c, then suppliedNodeList should
  contain a complete list of next state nodes; the transitive fanins of the
  latches are visited according to the order of the next state nodes in
  suppliedNodeList.  If suppliedOrderType is Ord_Partial_c, then
  suppliedNodeList may contain an arbitrary subset of network nodes; in this
  case, an ordering is found disregarding suppliedNodeList, and then this
  ordering is merged into the suppliedNodeList.  No checks are made to insure
  that suppliedNodeList contains what is implied by the value of
  suppliedOrderType.<p>

  If nsAfterSupport is TRUE, then for a given latch, its next state variable
  is ordered just after the latch's corresponding dataInput node. If
  nsAfterSupport is FALSE, then for a given latch, its next state variable is
  ordered just after the latch (i.e. its present state variable). (If the
  latch itself is not present yet in the nodeOrderList, then first adds latch
  to the end of the ordering.)]

  SideEffects []

  SeeAlso [Ord_NetworkOrderVariables]

******************************************************************************/
lsList
Ord_NetworkOrderNodes(
  Ntk_Network_t *network,
  Ord_RootMethod rootOrderMethod,
  Ord_NodeMethod nodeOrderMethod,
  boolean        nsAfterSupport,
  Ord_OrderType  generatedOrderType /* Ord_All_c or Ord_InputAndLatch_c */,
  Ord_OrderType  suppliedOrderType  /* Ord_NextStateNode_c, Ord_Partial_c, or
                                        Ord_Unassigned_c */, 
  lsList         suppliedNodeList   /* list of nodes Ntk_Node_t* from ordering file */,
  int            verbose)
{
  lsList      partialRootOrder;   /* list of nodes (Ntk_Node_t *) */
  lsList      roots;              /* list of nodes (Ntk_Node_t *) */
  lsList      nodeOrderList;      /* list of nodes (Ntk_Node_t *) */
  st_table   *nodeToHandle;       /* Ntk_Node_t* to lsHandle */

  /*
   * Check the input arguments.
   */
  assert(   (generatedOrderType == Ord_All_c)
         || (generatedOrderType == Ord_InputAndLatch_c));

  assert(   (suppliedOrderType == Ord_NextStateNode_c)
         || (suppliedOrderType == Ord_Partial_c)
         || (suppliedOrderType == Ord_Unassigned_c));
  

  /*
   * Compute an ordering on the roots. The nodes of the network are explored
   * in DFS order from the roots, in the root order computed.  If
   * suppliedOrderType is Ord_NextStateNode_c, then suppliedNodeList contains
   * the next state nodes; this list serves as a seed to compute the root
   * ordering.
   */
  partialRootOrder = (suppliedOrderType == Ord_NextStateNode_c)
      ? LatchNSListConvertToLatchDataInputList(suppliedNodeList)
      : (lsList) NULL;
  roots = Ord_NetworkOrderRoots(network, rootOrderMethod,
                                partialRootOrder, verbose);
  if (suppliedOrderType == Ord_NextStateNode_c) {
    (void) lsDestroy(partialRootOrder, (void (*) (lsGeneric)) NULL);
  }
  if (verbose > 0) {
    (void) fprintf(vis_stdout, "\nOrder in which roots are visited:\n");
    OrdNodeListWrite(vis_stdout, roots);
  }
  
  /*
   * Compute an order on all nodes in the transitive fanin of roots, including
   * the roots themselves. Pass in an empty nodeToHandle table.
   */
  nodeToHandle  = st_init_table(st_ptrcmp, st_ptrhash);
  nodeOrderList = OrdNetworkOrderTFIOfRoots(network, roots, nodeOrderMethod,
                                            nodeToHandle, verbose);
  (void) lsDestroy(roots, (void (*) (lsGeneric)) NULL);

  if (verbose > 0) {
    (void) fprintf(vis_stdout, "\nOrder of network nodes without NS:\n");
    OrdNodeListWrite(vis_stdout, nodeOrderList);
  }
  
  /*
   * Add in the next state variables (represented by the shadow nodes of
   * latches).
   */
  NetworkAddNSVarsToOrderList(network, nodeOrderList, nodeToHandle, nsAfterSupport);
  if (verbose > 2) {
    (void) fprintf(vis_stdout, "\nOrder of network nodes with NS:\n");
    OrdNodeListWrite(vis_stdout, nodeOrderList);
  }
  
  
  /*
   * There may be some nodes that are not in the TFI of any root. Put such
   * nodes at the end of nodeOrderList (in no particular order).
   */
  NetworkAddDanglingNodesToOrderList(network, nodeOrderList, nodeToHandle);
  st_free_table(nodeToHandle);
  
  /*
   * If the suppliedOrderType is Partial, then merge (left, arbitrarily) the
   * computed node order into the supplied node order and return the result.
   * Otherwise, just return the nodeOrderList computed.
   */
  if (suppliedOrderType == Ord_Partial_c) {
    lsList suppliedNodeListCopy = lsCopy(suppliedNodeList,
                                         (lsGeneric (*) (lsGeneric)) NULL);

    Ord_ListMergeList(suppliedNodeListCopy, nodeOrderList, Ord_ListMergeLeft_c);
    (void) lsDestroy(nodeOrderList, (void (*) (lsGeneric)) NULL);
    return suppliedNodeListCopy;
  }
  else {
    return nodeOrderList;
  }
}


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

  Synopsis    [Assigns an mddId to a node.]

  Description [Assigns an mddId to a node.  If the node already has a valid
  mddId (i.e. it is not NTK_UNASSIGNED_MDD_ID), then nothing is done.
  Otherwise, the node is assigned an mddId, and this Id is created within the
  MDD manager of the network. (An MDD manager is created for the network if
  the network doesn't already have one.) ]

  SideEffects []

  Comment [(Tom): this should be more intelligent, and get the id from the
  total ordering on all the network nodes, and then do insertion into variable
  ordering.  Use ntk appl info to store total node order.]
  
******************************************************************************/
void
Ord_NetworkAssignMddIdForNode(
  Ntk_Network_t *network,
  Ntk_Node_t    *node)
{
  if (Ntk_NodeReadMddId(node) != NTK_UNASSIGNED_MDD_ID) {
    return;
  }
  else {
    int          mddId;
    mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
    array_t     *mvarValues = array_alloc(int, 0);
    array_t     *mvarNames  = array_alloc(char *, 0);
  
    /*
     * If the network doesn't already have an MDD manager, then create one.  In
     * any case, set mddId to be the number of variables currently existing in
     * the manager.
     */
    if (mddManager == NIL(mdd_manager)) {
      mddManager = Ntk_NetworkInitializeMddManager(network);
      mddId = 0;
    }
    else {
      array_t *mvarArray  = mdd_ret_mvar_list(mddManager);
      mddId = array_n(mvarArray);
    }
  
    Ntk_NodeSetMddId(node, mddId);

    array_insert_last(int, mvarValues,
                      Var_VariableReadNumValues(Ntk_NodeReadVariable(node)));
    array_insert_last(char *, mvarNames, Ntk_NodeReadName(node));

    /*
     * Create the variable in the MDD manager.  The last argument being NIL
     * means that the variable will not be interleaved.
     */
    mdd_create_variables(mddManager, mvarValues, mvarNames, NIL(array_t));

    array_free(mvarValues);
    array_free(mvarNames);
  }
}


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

  Synopsis    [Merges left list2 into list1, using the provided table for efficiency.]

  Description [Merges left list2 into list1, using the provided table for
  efficiency. dataToHandle1 is a hash table mapping each item in list1 to its
  handle in list1. <p>

  This function implements the merge described in Algorithm 1 by Fujii et al.,
  "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993, p. 38.
  For each item in list2: if item is already present in list1, do nothing;
  else if item is the head of list2, then insert item at the head of list1;
  else, insert item into list1 immediately following the location in list1 of
  the item's predessor item in list2. This has the effect of locating the
  items in list2 as far to the left as possible in list1, while still
  preserving the partial order for those elements of list2 not initially
  appearing in list1 (a "merge left"). Examples:

  <pre>
  list1=abc, list2=dbe --> list1=dabec
  list1=abc, list2=deb --> list1=deabc.
  </pre>

  Note that this merging is not commutative.  That is, Ord_ListMergeLeftList(l1,l2)
  may give a different ordering than Ord_ListMergeLeftList(l2,l1).]
  
  SideEffects [List1 is modified, and dataToHandle1 is modified to reflect the
  newly inserted items.]

  Comment     [All references to "handle" in the code are references to
  handles in list1.  We never reference or care about handles in list2. ]

  SeeAlso [Ord_ListMergeRightListUsingTable]

******************************************************************************/
void
Ord_ListMergeLeftListUsingTable(
  lsList    list1,
  lsList    list2,
  st_table *dataToHandle1)
{
  lsGen      gen1;   /* generator for list1 */
  lsGen      gen2;   /* generator for list2 */
  lsHandle   handle; /* handle of an item in list1 */
  lsGeneric  data;   
  lsGeneric  prevData;

  /*
   * Walk through list2 forwards, keeping track of the previous item just visited.
   */
  gen2 = lsStart(list2);
  prevData = NULL;
  while (lsNext(gen2, &data, LS_NH) == LS_OK) {

    if (!st_is_member(dataToHandle1, (char *) data)) {
      /*
       * Data is not present in list1, so we must insert it at the proper
       * location.
       */
      if (prevData == NULL) {
        /*
         * Data is the head of list2, so insert it at the head of list1.
         */
        (void) lsNewBegin(list1, data, &handle);
      }
      else {
        lsGeneric dummyData;
        lsHandle  prevHandle;

        /*
         * Data is not the head of list1.  Hence, insert it just to the right
         * of the location of prevData in list1 (by induction, prevData must
         * currently exist in list1). Do this by getting the handle of
         * prevData in list1, creating a generator initialized to just after
         * prevData, and then inserting data at this point. Note that
         * lsInAfter and lsInBefore are equivalent in this case, since we
         * immediately kill gen1. 
         */
        st_lookup(dataToHandle1, prevData, &prevHandle);
        gen1 = lsGenHandle(prevHandle, &dummyData, LS_AFTER);
        (void) lsInAfter(gen1, data, &handle);
        (void) lsFinish(gen1);
      }
      st_insert(dataToHandle1, data, handle);

    } /* else, data already present in list1, so do nothing */

    prevData = data;

  } /* end while */
  (void) lsFinish(gen2);
}


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

  Synopsis    [Merges right list2 into list1, using the provided table for efficiency.]

  Description [Merges right list2 into list1, using the provided table for
  efficiency. This function is the same as Ord_ListMergeLeftListUsingTable,
  except that a "merge right" is done, rather than a "merge left".  For each
  item in list2: if item is already present in list1, do nothing; else if item
  is the tail of list2, then insert item at the tail of list1; else, insert
  item into list1 immediately preceeding the location in list1 of the item's
  successor item in list2. This has the effect of locating the items in list2
  as far to the right as possible in list1, while still preserving the partial
  order for those elements of list2 not initially appearing in list1 (a "merge
  right"). Examples:

  <pre>
  list1=abc, list2=dbe --> list1=adbce
  list1=abc, list2=deb --> list1=adebc.
  </pre>

  ]
  
  SideEffects [List1 is modified, and dataToHandle1 is modified to reflect the
  newly inserted items.]

  Comment     [All references to "handle" in the code are references to
  handles in list1.  We never reference or care about handles in list2. ]
  
  SeeAlso [Ord_ListMergeLeftListUsingTable]

******************************************************************************/
void
Ord_ListMergeRightListUsingTable(
  lsList    list1,
  lsList    list2,
  st_table *dataToHandle1)
{
  lsGen      gen1;   /* generator for list1 */
  lsGen      gen2;   /* generator for list2 */
  lsHandle   handle; /* handle of an item in list1 */
  lsGeneric  data;   
  lsGeneric  succData;

  /*
   * Walk through list2 backwards, keeping track of the successor item just visited.
   */
  gen2 = lsEnd(list2);
  succData = NULL;
  while (lsPrev(gen2, &data, LS_NH) == LS_OK) {

    if (!st_is_member(dataToHandle1, (char *) data)) {
      /*
       * Data is not present in list1, so we must insert it at the proper
       * location.
       */
      if (succData == NULL) {
        /*
         * Data is the tail of list2, so insert it at the tail of list1.
         */
        (void) lsNewEnd(list1, data, &handle);
      }
      else {
        lsGeneric dummyData;
        lsHandle  succHandle;

        /*
         * Data is not the tail of list1.  Hence, insert it just to the left
         * of the location of succData in list1 (by induction, succData must
         * currently exist in list1). Do this by getting the handle of
         * succData in list1, creating a generator initialized to just before
         * succData, and then inserting data at this point. Note that
         * lsInAfter and lsInBefore are equivalent in this case, since we are
         * immediately kill gen1. 
         */
        st_lookup(dataToHandle1, succData, &succHandle);
        gen1 = lsGenHandle(succHandle, &dummyData, LS_BEFORE);
        (void) lsInAfter(gen1, data, &handle);
        (void) lsFinish(gen1);
      }
      st_insert(dataToHandle1, data, handle);

    } /* else, data already present in list1, so do nothing */

    succData = data;

  } /* end while */
  (void) lsFinish(gen2);
}


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

  Synopsis    [Merges list2 into list1, using the provided table for efficiency.]

  Description [Merges list2 into list1, using the provided table for
  efficiency. Calls Ord_ListMergeLeftListUsingTable or
  Ord_ListMergeRightListUsingTable depending on the value of method.]

  SideEffects [list1 is modified]

  SeeAlso [Ord_ListMergeLeftListUsingTable Ord_ListMergeRightListUsingTable]

******************************************************************************/
void
Ord_ListMergeListUsingTable(
  lsList               list1,
  lsList               list2,
  st_table            *dataToHandle1,
  Ord_ListMergeMethod  method)
{
  if (method == Ord_ListMergeLeft_c) {
    Ord_ListMergeLeftListUsingTable(list1, list2, dataToHandle1);
  }
  else if (method == Ord_ListMergeRight_c) {
    Ord_ListMergeRightListUsingTable(list1, list2, dataToHandle1);
  }
  else {
    fail("unrecognized method");
  }
}
    

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

  Synopsis    [Merges list2 into list1.]

  Description [Merges list2 into list1. Creates a hash table mapping the items
  of list1 to their handles in list1, and then calls Ord_ListMergeListUsingTable.]

  SideEffects [list1 is modified]

  SeeAlso     [Ord_ListMergeListUsingTable]

******************************************************************************/
void
Ord_ListMergeList(
  lsList              list1,
  lsList              list2,
  Ord_ListMergeMethod method)
{
  lsGen      gen1;   /* generator for list1 */
  lsHandle   handle; /* handle of an item in list1 */
  lsGeneric  data;   
  st_table  *dataToHandle1 = st_init_table(st_ptrcmp, st_ptrhash);

  /*
   * Load a hash table mapping each item in list1 to its handle in list1.
   */
  gen1 = lsStart(list1);
  while (lsNext(gen1, &data, &handle) == LS_OK) {
    st_insert(dataToHandle1, (char *) data, (char *) handle);
  }
  (void) lsFinish(gen1);

  Ord_ListMergeListUsingTable(list1, list2, dataToHandle1, method);

  st_free_table(dataToHandle1);
}

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

  Synopsis    [Appends list2 into list1.]

  Description [Appends list2 into list1. List1 is modified; list2 is not
  changed.]

  SideEffects [list1 is modified]

******************************************************************************/
void
Ord_ListAppendList(
  lsList list1,
  lsList list2)
{
  lsGen gen;
  lsHandle handle; /* unused */
  lsGeneric data;   

  /*
   * Walk through list2 forwards, inserting each element to the end of list1.
   */
  gen = lsStart(list2);
  while (lsNext(gen, &data, LS_NH) == LS_OK) {
    (void) lsNewEnd(list1, data, &handle);
  } 
  (void) lsFinish(gen);
}

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

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

  Synopsis    [Compares the depth of two nodes in an lsList.]

  Description [Compares the depth of two nodes in an lsList. Greater depth
  node should appear before a lower depth node.]

  SideEffects []

******************************************************************************/
int
OrdNodesFromListCompareDepth(
  lsGeneric node1,
  lsGeneric node2)
{
  return NodesCompareDepth((Ntk_Node_t *) node1, (Ntk_Node_t *) node2);
}


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

  Synopsis    [Compares the depth of two nodes in an array_t.]

  Description [Compares the depth of two nodes in an array_t. Greater depth
  node should appear before a lower depth node.]

  SideEffects []

******************************************************************************/
int
OrdNodesFromArrayCompareDepth(
  const void * node1,
  const void * node2)
{
  return NodesCompareDepth(*(Ntk_Node_t **) node1, *(Ntk_Node_t **) node2);
}


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

  Synopsis    [Computes the depth of each node in the TFI of roots.]

  Description [Computes the depth of each node in the transitive fanin of the
  list of roots. The depth of a node is defined inductively: latches, and
  nodes with no inputs, have depth 0. Otherwise, the depth of a node is 1 more
  than the maximum depth over the node's fanins.  Intuitively, the depth of a
  node is the length of the longest (backward) path from the node to a latch,
  primary input, pseudo input, or constant.]

  SideEffects [Uses undef field of Ntk_Node_t.]

  SeeAlso     [Ord_NetworkOrderVariables]

******************************************************************************/
void
OrdNetworkComputeNodeDepths(
  Ntk_Network_t * network,
  lsList  roots /* list of Ntk_Node_t  */)
{
  lsGen       gen;
  Ntk_Node_t *node;
  Ntk_Node_t *root;

  /*
   * Initialize the depth of each node to unassigned.
   */
  Ntk_NetworkForEachNode(network, gen, node) {
    NodeSetDepth(node, ORDUNASSIGNED_DEPTH);
  }

  /*
   * Start the recursive computation from each root.
   */
  lsForEachItem(roots, gen, root) {
    (void) NodeComputeDepth(root);
  }
}


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

  Synopsis    [Prints the names of a list of nodes, one per line.]

  SideEffects []

******************************************************************************/
void
OrdNodeListWrite(
  FILE *fp,
  lsList nodeList)
{
  lsGen gen;
  Ntk_Node_t *node;

  lsForEachItem(nodeList, gen, node) {
    (void) fprintf(fp, "%s\n", Ntk_NodeReadName(node));
  }
}


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

  Synopsis    [Reads the depth of a node.]

  SideEffects []

  Comment [The depth is not stored in a hash table of orderingState, because,
  for OrdNodesFromArrayCompareDepth, we need to be able to access the depth of
  a node given *just* the node.]

  SeeAlso     [NodeSetDepth OrdNodesFromArrayCompareDepth
  OrdNodesFromListCompareDepth] 

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


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

  Synopsis    [Assigns consecutive MDD ids to nodes in orderList.]

  Description [Assigns consecutive MDD ids to nodes in orderList.  Ids are
  assigned starting from the number of variables in the MDD manager of
  network.  (An MDD manager is created for the network if the network doesn't
  already have one.) OrderType can be Ord_All_c or Ord_InputAndLatch_c.  If
  orderType is Ord_All_c, then all nodes in orderList are assigned an id.  If
  orderType is Ord_InputAndLatch_c only primary inputs, pseudo input, latches,
  and latch NSs are assigned ids. Presently, nsAfterSupport is unused.<p>]

  SideEffects []

  SeeAlso     [OrdNetworkOrderTFIOfRoots Ntk_NetworkInitializeMddManager]

******************************************************************************/
void
OrdNetworkAssignMddIds(
  Ntk_Network_t * network,
  Ord_OrderType  orderType,
  lsList  orderList,
  boolean nsAfterSupport)
{
  lsGen        gen;
  Ntk_Node_t  *node;
  int          mddId;
  mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
  array_t     *mvarValues = array_alloc(int, lsLength(orderList));
  array_t     *mvarNames  = array_alloc(char *, lsLength(orderList));

  assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c));

  /*
   * If the network doesn't already have an MDD manager, then create one.  In
   * any case, set mddId to be the number of variables currently existing in
   * the manager.
   */
  if (mddManager == NIL(mdd_manager)) {
    mddManager = Ntk_NetworkInitializeMddManager(network);
    mddId = 0;
  }
  else {
    array_t *mvarArray  = mdd_ret_mvar_list(mddManager);
    mddId = array_n(mvarArray);
  }
  
  lsForEachItem(orderList, gen, node) {
    /*
     * A node gets an MDD id if node is a combinational input, next state
     * node, or orderType is Ord_All_c.
     */
    if (Ntk_NodeTestIsCombInput(node) || Ntk_NodeTestIsNextStateNode(node)
        || (orderType == Ord_All_c) ) {

      Ntk_NodeSetMddId(node, mddId);
      mddId++;

      array_insert_last(int, mvarValues,
                        Var_VariableReadNumValues(Ntk_NodeReadVariable(node)));
      array_insert_last(char *, mvarNames, Ntk_NodeReadName(node));
    }
  }

  /*
   * Create the variables in the MDD manager.  The last argument being NIL
   * means that the variables will not be interleaved.
   */
  mdd_create_variables(mddManager, mvarValues, mvarNames, NIL(array_t));

  array_free(mvarValues);
  array_free(mvarNames);
}
    

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

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

  Synopsis    [Compares depths of node1 and node2 for sorting; greater depth
  node should appear before a lower depth node.  Ties are broken based on the
  node names; it's an error if the two nodes have the same name.]

  SideEffects []

******************************************************************************/
static int
NodesCompareDepth(
  Ntk_Node_t *node1,
  Ntk_Node_t *node2)
{
  long depth1 = OrdNodeReadDepth(node1);
  long depth2 = OrdNodeReadDepth(node2);

  if (depth1 > depth2) {
    return -1;
  }
  else if (depth1 < depth2) {
    return 1;
  }
  else {
    char *name1 = Ntk_NodeReadName(node1);
    char *name2 = Ntk_NodeReadName(node2);

    /*
     * As a tiebreaker, sort based on name, so that the sorted result is not
     * sensitive to the order in which the nodes are passed to the compare
     * function. When sorting based on name, the order doesn't really matter,
     * but right now it's done so that "foo<i>" will come before "foo<j>" in
     * the ordering, where i < j.  This is just a little heuristic to put lower
     * order bits first. */
    if (strcmp(name1, name2) < 0) {
      return -1;
    }
    else if (strcmp(name1, name2) > 0) {
      return 1;
    }
    else {
      return 0;
    }
  }
}


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

  Synopsis    [Computes the depth of a node.]

  SideEffects []

  SeeAlso     [OrdNetworkComputeNodeDepths]

******************************************************************************/
static long
NodeComputeDepth(
  Ntk_Node_t * node)
{
  long depth = OrdNodeReadDepth(node);

  /*
   * If the node's depth has already been computed (i.e. it's not unassigned),
   * then just return it below.  If it's unassigned, then recursively compute
   * it.
   */
  if (depth == ORDUNASSIGNED_DEPTH) {

    if (Ntk_NodeTestIsCombInput(node) || Ntk_NodeTestIsConstant(node)) {
      /*
       * Latches, and nodes with no fanins, get depth 0. This is the terminal
       * case of recursion. 
       */
      depth = 0;
    }
    else {
      int         i;
      Ntk_Node_t *fanin;
      /*
       * Compute the depth of each fanin node in the support of node, and
       * maintain the maximum.  We start depth at 0 for max calculation.
       */
      depth = 0;
      Ntk_NodeForEachFanin(node, i, fanin) {  
        long faninDepth = NodeComputeDepth(fanin);

        depth = (depth > faninDepth) ? depth : faninDepth;
      }
      
      /*
       * The depth of node is one more than the max depths of its fanins.
       */
      depth++;
    }

    /*
     * Store the depth.
     */
    NodeSetDepth(node, depth);
  }
  
  return depth;
}

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

  Synopsis    [Adds to nodeOrderList all network nodes not currently in the list.]

  Description [Adds to the end of nodeOrderList all network nodes that are not
  yet present in nodeOrderList.  This is used to pick up those (dangling)
  nodes that weren't in the transitive fanins of the roots in the call to
  OrdNetworkOrderTFIOfRoots. nodeToHandle is a hash table mapping each node in
  nodeOrderList to its handle in the list; dangling nodes are inserted into
  this table.]

  SideEffects [nodeOrderList and nodeToHandle will be modified if dangling
  nodes exist.]

  SeeAlso     [OrdNetworkOrderTFIOfRoots]

******************************************************************************/
static void
NetworkAddDanglingNodesToOrderList(
  Ntk_Network_t * network,
  lsList  nodeOrderList /* of Ntk_Node_t*  */,
  st_table *nodeToHandle /* Ntk_Node_t* to lsHandle */)
{
  lsGen       gen;
  Ntk_Node_t *node;

  /*
   * For each network node, if it's not in nodeOrderList, then add it to the
   * end of the list. 
   * (NOTE: may be sensitive to ordering in memory.)
   */
  Ntk_NetworkForEachNode(network, gen, node) {
    if (!st_is_member(nodeToHandle, (char *) node)) {
      lsHandle handle;
      
      (void) lsNewEnd(nodeOrderList, (lsGeneric) node, &handle);
      st_insert(nodeToHandle, (char *) node, (char *) handle);
    }
  }
}


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

  Synopsis    [Adds to nodeOrderList all next state variables.]

  Description [Adds to nodeOrderList all next state variables. If
  nsAfterSupport is TRUE, then for a given latch, its NS variable is added in
  nodeOrderList just after the latch's corresponding dataInput node. If
  nsAfterSupport is FALSE, then for a given latch, its NS variable is added in
  nodeOrderList just after the latch (i.e. its present state variable). (If the
  latch itself is not present yet in the nodeOrderList, then first adds latch
  to the end of the ordering.)<p>

  nodeToHandle is a hash table mapping each node in nodeOrderList to its
  handle in the list; next state nodes are inserted into this table.]

  SideEffects [nodeOrderList and nodeToHandle will be modified if latches
  exist.]

  SeeAlso     [OrdNetworkOrderTFIOfRoots]

******************************************************************************/
static void
NetworkAddNSVarsToOrderList(
  Ntk_Network_t * network,
  lsList  nodeOrderList /* of Ntk_Node_t  */,
  st_table *nodeToHandle /* Ntk_Node_t* to lsHandle */,
  boolean nsAfterSupport)
{
  lsGen       gen1;
  Ntk_Node_t *latch;

  /*
   * For each latch, add the latch's corresponding NS node to the ordering.
   * (NOTE: may be sensitive to ordering in memory.)
   */
  Ntk_NetworkForEachLatch(network, gen1, latch) {
    lsHandle    handle;
    lsGen       gen2;
    lsGeneric   dummyData;
    Ntk_Node_t *latchNS   = Ntk_NodeReadShadow(latch);

    if (nsAfterSupport) {
      /* Add just after the latch's dataInput. */
      lsHandle    dataInputHandle;
      Ntk_Node_t *dataInput = Ntk_LatchReadDataInput(latch);
      int         status UNUSED = st_lookup(nodeToHandle, dataInput,
                                            &dataInputHandle);

      assert(status);
      gen2 = lsGenHandle(dataInputHandle, &dummyData, LS_AFTER);
    }
    else {
      /* Add just after the latch. */
      lsHandle latchHandle;
      int      status = st_lookup(nodeToHandle, latch, &latchHandle);

      if (!status) {
        /*
         * Latch itself is not yet in the ordering.  This can happen if the
         * latch is not in the TFI of any other latch.  So add the latch first
         * (at the end of the ordering). 
         */
        (void) lsNewEnd(nodeOrderList, (lsGeneric) latch, &latchHandle);
        st_insert(nodeToHandle, (char *) latch, (char *) latchHandle);
      }
    
      gen2 = lsGenHandle(latchHandle, &dummyData, LS_AFTER);
    }

    /* Actually add to list here. */
    (void) lsInAfter(gen2, (lsGeneric) latchNS, &handle);  
    st_insert(nodeToHandle, (char *) latchNS, (char *) handle);
    (void) lsFinish(gen2);
      
  }
}


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

  Synopsis    [Converts a list of latch next state nodes to the corresponding
  list of latch data input nodes.]

  SideEffects []

******************************************************************************/
static lsList
LatchNSListConvertToLatchDataInputList(
  lsList latchNSList)
{
  lsGen       gen;
  Ntk_Node_t *node;
  Ntk_Node_t *latch;
  lsList      latchDataInputList = lsCreate();

  lsForEachItem(latchNSList, gen, node) {
    assert(Ntk_NodeTestIsNextStateNode(node));
    latch = Ntk_ShadowReadOrigin(node);
    (void) lsNewEnd(latchDataInputList, (lsGeneric)
                    Ntk_LatchReadDataInput(latch), LS_NH); 
  }

  return latchDataInputList;
}


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

  Synopsis    [Sets the depth of a node.]

  SideEffects []

  SeeAlso     [OrdNodeReadDepth]

******************************************************************************/
static void
NodeSetDepth(
  Ntk_Node_t * node,
  long depth)
{
  Ntk_NodeSetUndef(node, (void *) depth);
}

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

  Synopsis    [Group all bdd vars corresponding to mdd vars initMddId to
  initMddId + (blockSize-1) in a block which will not be split in reordering.]

  Description [Group all bdd vars corresponding to mdd vars initMddId to
  initMddId + blockSize in a block which will not be reordered internally.
  Ths bdd's corresponding to these mdd's should be contiguous; if not the
  function will fail.]

  SideEffects []

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

static void
MddGroupVariables(
  mdd_manager *mddMgr,
  int initMddId,
  int blockSize )
{
  int i, j;
  int length;
  int aIndex;
  int startingBddIndex;
  int sanityCheck;
  mvar_type initMv, anMv;
  bvar_type initBvar, aBvar;
  array_t *mvar_list, *bvar_list;
  bdd_t *bdd;
  
  mvar_list = mdd_ret_mvar_list(mddMgr);
  bvar_list = mdd_ret_bvar_list(mddMgr);

  /*
   * mvar for initMddId 
   */
  initMv = array_fetch(mvar_type, mvar_list, initMddId);

  /*
   * bvar for first bdd for initMddId 
   */
  initBvar = mdd_ret_bvar(&initMv, 0, bvar_list);

  /*
   * number of bdd variables to group 
   */
  length = 0;

  /*
   * startingBddIndex is the level of the first bdd variable 
   */
  startingBddIndex = bdd_top_var_level( mddMgr, initBvar.node );
  sanityCheck = startingBddIndex;

  /*
   * in this loop we are simply ensuring that the bdd variables
   * corresponding to the mdd vars are infact contiguous. If this
   * is not the case we fail. length is the total number of bdd variables
   * to be grouped.
   */
  for( i = 0; i < blockSize; i++) {
    anMv = array_fetch(mvar_type, mvar_list, ( initMddId + i ) );
    for ( j = 0 ; j < anMv.encode_length; j++ ) {

      aBvar = mdd_ret_bvar( & anMv, j, bvar_list );
      aIndex = bdd_top_var_level( mddMgr,  aBvar.node );

      if ( sanityCheck != aIndex ) {
        /* bdd vars are not contiguous!! */
        fprintf(vis_stderr, "Badly formed block - bdd vars for %s (mvar_id = %d) are not contiguous!!\n",
                             anMv.name, anMv.mvar_id );
        fail("Wont go on\n");
      }
      else {
        /* number of variables to group increased by one */
        sanityCheck++;
        length++;
      }
    }
  }

  bdd = bdd_var_with_index(mddMgr, startingBddIndex);
  (void) bdd_new_var_block(bdd, length);
  bdd_free(bdd);
}