source: vis_dev/vis-2.3/src/ord/ordCmd.c @ 57

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

  FileName    [ordCmd.c]

  PackageName [ord]

  Synopsis    [Command interface to the ordering package.]

  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: ordCmd.c,v 1.37 2005/05/19 03:22:55 awedh Exp $";

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;


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

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

static int CommandStaticOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandReadOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandWriteOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandDynamicVarOrdering(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintBddStats(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static Ord_OrderType StringConvertToOrderType(char *string);
static bdd_reorder_type_t StringConvertToDynOrderType(char *string);
static char * DynOrderTypeConvertToString(bdd_reorder_type_t method);
static boolean NetworkCheckSuppliedNodeList(Ntk_Network_t * network, lsList suppliedNodeList, Ord_OrderType orderType);
static void TimeOutHandle(void);

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


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

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

  Synopsis    [Initializes the order package.]

  SideEffects []

  SeeAlso     [Ord_End]

******************************************************************************/
void
Ord_Init(void)
{
  Cmd_CommandAdd("static_order", CommandStaticOrder, 0);
  Cmd_CommandAdd("read_order", CommandReadOrder, 0);
  Cmd_CommandAdd("write_order", CommandWriteOrder, 0);
  Cmd_CommandAdd("dynamic_var_ordering", CommandDynamicVarOrdering, 0);
  Cmd_CommandAdd("print_bdd_stats", CommandPrintBddStats, 0);
}


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

  Synopsis    [Ends the order package.]

  SideEffects []

  SeeAlso     [Ord_Init]

******************************************************************************/
void
Ord_End(void)
{
}


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

  Synopsis    [Checks that all nodes corresponding to orderType have MDD ids.]

  Description [For each node of network that falls in the class given by
  orderType, checks that the node has an MDD id.  If all such nodes have MDD
  ids, return 1, else returns 0.  orderType can have one of 3 values:
  Ord_All_c, checks all nodes of network; Ord_InputAndLatch_c, checks all
  combinational inputs and latch next states; Ord_NextStateNode_c, checks all
  next state nodes.  Returns 0 on the first such node not having an MDD id,
  and writes an error message in error_string.  Also returns 0 if the network
  doesn't have an MDD manager.]

  SideEffects []

******************************************************************************/
boolean
Ord_NetworkTestAreVariablesOrdered(
  Ntk_Network_t * network,
  Ord_OrderType  orderType)
{
  lsGen          gen;
  Ntk_Node_t    *node;
  mdd_manager   *mddManager = Ntk_NetworkReadMddManager(network);
  
  assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c)
         || (orderType == Ord_NextStateNode_c));

  if (mddManager == NIL(mdd_manager)) {
    error_append("network doesn't have an MDD manager\n");
  return 0;
  }

  /*
   * Next state nodes are included by all 3 order types.
   */
  Ntk_NetworkForEachNode(network, gen, node) {
    if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) {
      if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) {
        error_append("node ");
        error_append(Ntk_NodeReadName(node));
        error_append(" not ordered\n");
        (void) lsFinish(gen);
        return 0;
      }
    }
    else if ((orderType == Ord_InputAndLatch_c)
             && Ntk_NodeTestIsCombInput(node)) {
      if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) {
        error_append("node ");
        error_append(Ntk_NodeReadName(node));
        error_append(" not ordered\n");
        (void) lsFinish(gen);
        return 0;
      }
    }
    /* else, this node is not included by orderType */
  }

  return 1;
}


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


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

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

  Synopsis    [Implements the static_order command.]

  SideEffects []

  CommandName [static_order]

  CommandSynopsis [order the MDD variables of the flattened network]

  CommandArguments [\[-a\] \[-h\] \[-n <method>\] \[-o <type>\] 
  \[-r <method>\] -s <type> \[-t <timeOut>\] \[-v #\]
  <file>] 

  CommandDescription [Order the MDD variables of the flattened network.  MDD
  variables must be created before MDDs can be built.  Networks with
  combinational cycles cannot be ordered.  If the MDD variables have already
  been ordered, then this command does nothing.  To undo the current ordering,
  reinvoke the command <tt>flatten_hierarchy</tt>. 
  <p>
  

  Command options:<p>

  <dl>

  <dt> -a
  <dd> Order each next state variable immediately following the variables in
  the support of the corresponding next state function.  By default, each next
  state variable is placed immeadiately following the corresponding present
  state variable.  It has been observed experimentally that ordering the NS
  variable after the PS variable is almost always better; however, as a last
b  resort, you might want to try this option.<p>

  Unless the -a flag is set, the PS and NS variables corresponding to latches
  are grouped together and cannot be separated by dynamic reordering. (This is
  done even when the ordering is read from a file - adjacent PS/NS vars in the
  file are grouped).<p>
  
  <dt> -h
  <dd> Print the command usage.<p>
  
  <dt> -n &lt;method&gt;

  <dd> Specify which node ordering method to use.  Node ordering is the
  process of computing a total ordering on all the network nodes.  This
  ordering is then projected onto the set of nodes specified by <tt>-o
  type</tt>. In the complexity measures below, n is the number of network
  nodes, E is the number of network edges, and k is the number of
  latches. "Method" must be one of the following:<p>

  <b>interleave:</b> (default) Uses Algorithm 2 of Fujii et al.,
  "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993.
  The complexity is O(E+nlog(n)).<p>

  <b>append:</b> Uses the algorithm of Malik, et al. "Logic Verification using
  Binary Decision Diagrams in a Logic Synthesis Environment," ICCAD,
  1988. Nodes are visited in DFS order, and appended to a global order list in
  the order they are visited.  The fanins of a node are visited in order of
  decreasing depth. The roots of the DFS are visited in the order determined
  by the <tt>-r method</tt>.  The complexity is O(E+nlog(n)).<p>
  
  <b>merge_left:</b> Uses an algorithm alluded to in Fujii et al.,
  "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993. Nodes
  are visited in DFS order.  At a given node g, its fanins are visited in
  order of decreasing depth.  For each fanin fi, a total order is computed for
  all the nodes in the transitive fanin (TFI) of fi, including fi itself.
  This ordering is merged into the combined ordering from fanins of higher
  priority.  After processing all of the fanins, the result is a total
  ordering on all TFI nodes of g.  Finally, g is appended to the end of this
  ordering, yielding a topological ordering. For example if the ordering for
  f1 is list1 = (a,b,d,f1) and for f2 is list2=(c,d,e,f2), and f1 has greater
  depth than f2, then the ordering for g is (c,a,b,d,e,f2,f1,g). The merge is
  done by inserting into list1 those nodes in list2 not already in list1, in
  such a way that the inserted nodes remain as close as possible to their left
  neighbors in list2 ("insert as far left as possible"). The roots of the DFS
  are merged in the order determined by <tt>-r method</tt>.  The complexity is
  O(n^2) (currently, there is a bug which causes more memory to be consumed
  than necessary).<p>

  <b>merge_right:</b> Same as <tt>merge_left</tt>, except that the merge is
  done in such a way that the inserted nodes remain as close as possible to
  their right neighbors in list2 ("insert as far right as possible"). For the
  example above, the ordering for g is (a,b,c,d,f1,e,f2,g).  It has been
  observed experimentally that neither <tt>merge_left</tt> nor
  <tt>merge_right</tt> is superior to the other; there are cases where
  verification times out with <tt>merge_left</tt> but not
  <tt>merge_right</tt>, and vice versa.<p>


  <dt> -o &lt;type&gt; <dd> Specify the network nodes for which MDD variables
  should be created.  Type can be one of the following:<p>

  <b>all:</b> Order all the nodes of the network.  This is normally not used.<p>

  <b>input_and_latch:</b> (default) Order the primary inputs, pseudo
  inputs, latches, and next state variables.  This is the minimum set of nodes
  that need to be ordered to perform operations on FSMs (e.g. model checking,
  reachability).  For purely combinational circuits, just the primary and
  pseudo inputs are ordered.<p>

  
  <dt> -r &lt;method&gt;

  <dd> Specify which root ordering method to use.  The "roots" of a network
  refer to the roots of the cones of logic driving the combinational outputs
  (data latch inputs, initial state latch inputs, and primary outputs) of a
  network. Root ordering is used to determine in which order to visit the
  roots of the network for the DFS carried out in node ordering (see
  <tt>-n</tt>). "Method" must be one of the following:<p>

  <b>depth:</b> (default for 30 or more latches) Roots are ordered based on
  logic depth (i.e. longest path to a combinational input).  Greater depth
  roots appear earlier in the ordering. All data latch inputs appear before
  all other combinational outputs. The complexity is O(E+nlog(n)). It has been
  observed experimentally that <tt>mincomm</tt> produces superior orderings to
  <tt>depth</tt>.  However, the complexity of the <tt>mincomm</tt> algorithm
  is such that it cannot produce orderings for designs with more than a
  hundred or so latches.  Hence, for big designs, use <tt>depth</tt>, followed
  optionally by <tt>dynamic_var_ordering</tt>.<p>

  <b>mincomm:</b> (default for less than 30 latches) Uses the algorithm of
  Aziz, et al. "BDD Variable Ordering for Interacting Finite State Machines,"
  DAC, 1994. First, the latches are ordered to decrease a communication
  complexity bound (where backward edges are more expensive than forward
  edges) on the latch communication graph. This directly gives an ordering for
  the data latch inputs.  The remaining combinational outputs are ordered
  after the data latch inputs, in decreasing order of their depth. The total
  complexity is O(nlog(n)+E+k^3).<p>


  <dt> -s &lt;type&gt;

  <dd> Used in conjunction with <tt>&lt;file&gt;</tt> to specify which
  nodes are supplied in the ordering file. Type can be one of the following
  (there is no default):<p>

  <b>all:</b> The ordering file supplies all the nodes of the network.
  The ordering generated is the supplied order, projected onto the set of nodes
  specified by <tt>-o</tt>.<p>

  <b>input_and_latch:</b> The ordering file supplies the primary inputs,
  pseudo inputs, latches, and next state variables. The ordering generated is
  exactly what is supplied (in the case of <tt>-o input_and_latch</tt>). <tt>-o
  all</tt> is incompatible with <tt>-s input_and_latch</tt>.<p>

  <b>next_state_node:</b> The ordering file supplies next state
  variables. During the ordering algorithm, the next state functions are
  visited in the order in which their corresponding next state variables
  appear in the file. The order of the next state variables in the ordering
  generated is not necessarily maintained.<p>

  <b>partial:</b> The ordering file supplies an arbitrary subset of nodes
  of the network. The ordering algorithm works by finding a total ordering on
  all the nodes (independent of the ordering supplied), then merging the
  computed order into the supplied order (maintaining the relative order of
  the supplied order), and then projecting the resulting ordering onto the set
  of nodes specified by <tt>-o</tt>.<p>
  

  <dt> -t &lt;timeOut&gt;
  <dd> Time in seconds allowed to perform static ordering.  If the flattened
  network has more than a couple hundred latches and you are using option
  <tt>-r mincomm</tt>, then you might want to set a timeOut to limit the
  allowed time.  The default is no limit.<p>

  <dt> -v #
  <dd> Print debug information.
  <dd>

  0 Nothing is printed out.  This is the default.<p>
  
  >= 1 Prints the nodes read from the input file (satisfying the supplied
  order type); prints the root order used for exploring the network.<p>
  
  >= 2 Prints the depth of nodes.<p>
  
  >= 3 Prints the ordering computed at each node.<p>

  
  <dt> &lt;file&gt;

  <dd> A file containing names of network nodes, used to specify a variable
  ordering. The name of a node is the full hierarchical path name, starting
  from the current hierarchical node.  A node should appear at most once in
  the file.  Each node name should appear at the beginning of a new line, with
  no white space preceeding it.  The end of a node name is marked by white
  space, and any other text on the rest of the line is ignored.  Any line
  starting with "#" or white space is ignored. See <tt>write_order</tt>
  for a sample file. Note that the variable ordering cannot be specified at
  the bit-level; it can only be specified at the multi-valued variable level.

  </dl>
  ]

  
  SeeAlso     [CommandWriteOrder]

******************************************************************************/
static int
CommandStaticOrder(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int                   c;
  FILE                 *fp;
  static int            timeOutPeriod;
  static int            verbose;
  static Ord_NodeMethod nodeMethod;
  static Ord_RootMethod rootMethod;
  static Ord_OrderType  suppliedOrderType;
  static Ord_OrderType  generatedOrderType;
  static boolean        nsAfterSupport;
  lsList                suppliedNodeList = (lsList) NULL;
                                /* list of Ntk_Node_t * */
  Ntk_Network_t        *network;

  /*
   * These are the default values.  These variables must be declared static
   * to avoid lint warnings.  Since they are static, we must reinitialize
   * them outside of the variable declarations.
   */
  timeOutPeriod      = 0;  
  verbose            = 0;
  nodeMethod         = Ord_NodesByDefault_c;
  rootMethod         = Ord_RootsByDefault_c;
  suppliedOrderType  = Ord_Unassigned_c;   /* default */
  generatedOrderType = Ord_InputAndLatch_c;/* default */
  nsAfterSupport     = FALSE;              /* default */
  
  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "av:o:s:t:n:r:h")) != EOF) {
    switch (c) {
      case 'a':
        nsAfterSupport = TRUE;
        break;
      case 'h':
        goto usage;
      case 'v':
        verbose = atoi(util_optarg);
        break;
      case 't':
        timeOutPeriod = atoi(util_optarg);
        break;
      case 'o':
        generatedOrderType = StringConvertToOrderType(util_optarg);
        if ((generatedOrderType == Ord_NextStateNode_c)
            || (generatedOrderType == Ord_Partial_c)) { 
          (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg);
          goto usage;
        }
        else if (generatedOrderType == Ord_Unassigned_c) {
          (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg);
          goto usage;
        }
        break;
      case 's':
        suppliedOrderType = StringConvertToOrderType(util_optarg);
        if (suppliedOrderType == Ord_Unassigned_c) {
          (void) fprintf(vis_stderr, "unknown input order type: %s\n", util_optarg);
          goto usage;
        }
        break;
      case 'n':
        if (strcmp("interleave", util_optarg) == 0) { 
          nodeMethod = Ord_NodesByInterleaving_c;
        }
        else if (strcmp("merge_left", util_optarg) == 0) { 
          nodeMethod = Ord_NodesByMergingLeft_c;
        }
        else if (strcmp("merge_right", util_optarg) == 0) { 
          nodeMethod = Ord_NodesByMergingRight_c;
        }
        else if (strcmp("append", util_optarg) == 0) { 
          nodeMethod = Ord_NodesByAppending_c;
        }
        else {
          (void) fprintf(vis_stderr, "unknown node order method: %s\n", util_optarg);
          goto usage;
        }
        break;
      case 'r':
        if (strcmp("depth", util_optarg) == 0) { 
          rootMethod = Ord_RootsByDepth_c;
        }
        else if (strcmp("mincomm", util_optarg) == 0) { 
          rootMethod = Ord_RootsByPerm_c;
        }
        else {
          (void) fprintf(vis_stderr, "unknown root order method: %s\n", util_optarg);
          goto usage;
        }
        break;
      default:
        goto usage;
    }
  }

  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  if ((suppliedOrderType == Ord_InputAndLatch_c) && (generatedOrderType == Ord_All_c)) {
    (void) fprintf(vis_stderr, "-o all -s input_and_latch not currently supported\n");
    return 1;
  }

  /*
   * The minimum set of variables that can be ordered are those specified by
   * Ord_InputAndLatch_c.  If these have already been ordered, then just return.
   */
  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) {
    (void) fprintf(vis_stderr, "Variables already ordered. ");
    (void) fprintf(vis_stderr, "Reinvoke flatten_hierarchy to undo variable ordering.\n");
    return 1;
  }
  
    
  /*
   * Process the input ordering file.
   */
  if (suppliedOrderType == Ord_Unassigned_c) {
    if (argc - util_optind > 0) {
      (void) fprintf(vis_stderr, "must specify -s if supplying order file\n");
      goto usage;
    }
  }
  else {
    if (argc - util_optind == 0) {
      (void) fprintf(vis_stderr, "order file not provided\n");
      goto usage;
    }
    else if (argc - util_optind > 1) {
      (void) fprintf(vis_stderr, "too many arguments\n");
      goto usage;
    }

    fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
    if (fp == NIL(FILE)) {
      (void) fprintf(vis_stderr, "File %s is not readable, please check if it exists\n", argv[util_optind]);
      return 1;
    }
    else {
      boolean status;
      
      error_init();
      status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose);
      if (status == FALSE) {
        (void) fprintf(vis_stderr, "Error reading ordering file:\n");
        (void) fprintf(vis_stderr, "%s", error_string());
        (void) fprintf(vis_stderr, "Cannot perform static ordering.\n");
        (void) fclose(fp);
        return 1;
      }
      else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList,
                                            suppliedOrderType) == FALSE) { 
        (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n");
        (void) fprintf(vis_stderr, "%s", error_string());
        (void) fprintf(vis_stderr, "Cannot perform static ordering.\n");
        (void) fclose(fp);
        (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
        return 1;
      }
      else {
        (void) fclose(fp);
        if (verbose > 0) {
          (void) fprintf(vis_stdout, "\nNodes supplied in ordering file, ");
          (void) fprintf(vis_stdout, "according to -s option: \n");
          OrdNodeListWrite(vis_stdout, suppliedNodeList);
        }
      }
    }
  }
  
  
  /*
   * In order for static ordering to proceed, network must not have any
   * combinational cycles.
   */
  error_init();
  if(Ntk_NetworkTestIsAcyclic(network) == 0) {
    (void) fprintf(vis_stderr, "Combinational cycle found: ");
    (void) fprintf(vis_stderr, "%s\n", error_string());
    (void) fprintf(vis_stderr, "cannot perform static ordering\n");
    if (suppliedOrderType != Ord_Unassigned_c) {
      (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
    }
    return 1;
  }

  /* Start the timer before calling the variable ordering routine. */
  if (timeOutPeriod > 0){
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod);
      alarm(0);
      return 1;
    }
  }

  /*
   * Order the variables.
   */
  Ord_NetworkOrderVariables(network, rootMethod, nodeMethod, nsAfterSupport, 
                            generatedOrderType, suppliedOrderType,
                            suppliedNodeList, verbose);

  if (suppliedOrderType != Ord_Unassigned_c) {
    (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
  }

  /*
   * As a sanity check, make sure that all the variables in generatedOrderType
   * have an MDD id. 
   */
  assert(Ord_NetworkTestAreVariablesOrdered(network, generatedOrderType));
  
  alarm(0);
  return 0;  /* Everything okay */

  usage:
  (void) fprintf(vis_stderr, "usage: static_order [-a] [-h] [-n method] [-o type] [-r method] -s type [-t time] [-v #] file\n");
  (void) fprintf(vis_stderr, "   -a        order NS variables after support\n");
  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
  (void) fprintf(vis_stderr, "   -n method node ordering method\n");
  (void) fprintf(vis_stderr, "             (interleave (default), append, merge_left, merge_right)\n");
  (void) fprintf(vis_stderr, "   -o type   nodes to order (all, input_and_latch (default))\n");
  (void) fprintf(vis_stderr, "   -r method root ordering method (depth, mincomm (default for < 30 latches))\n");
  (void) fprintf(vis_stderr, "   -s type   nodes in file (all, input_and_latch, next_state_node, partial)\n");
  (void) fprintf(vis_stderr, "   -t time   time out period (in seconds)\n");
  (void) fprintf(vis_stderr, "   -v #      verbosity level\n");
  (void) fprintf(vis_stderr, "   file      supplied ordering of nodes\n");

  return 1;
}


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

  Synopsis    [Implements the read_order command.]

  SideEffects []

  CommandName [read_order]

  CommandSynopsis [Read and reorder variable order from a file.]

  CommandArguments [\[-h\] \[-v\] \[&lt;file&gt;\]] 

  CommandDescription [This command reads variable order from a file and
  reorder variable order according to the order. This command can be used
  any time after static_order command. However, the users should notice that
  there is a possibility to get BDD blowups during this command.
  <p>
  

  Command options:<p>

  <dl>

  <dt> -h
  <dd> Print the command usage.<p>

  <dt> -g &lt;group&gt;

  <dd> Specify whether to group present and next state variables or not.<p>

  <b>0:</b> Do not group.<p>

  <b>1:</b> Do group (default).<p>

  <dt> -v
  <dd> Print debug information.
  <dd>
  
  <dt> &lt;file&gt;

  <dd> A file containing names of network nodes, used to specify a variable
  ordering. The name of a node is the full hierarchical path name, starting
  from the current hierarchical node.  A node should appear at most once in
  the file.  Each node name should appear at the beginning of a new line, with
  no white space preceeding it.  The end of a node name is marked by white
  space, and any other text on the rest of the line is ignored.  Any line
  starting with "#" or white space is ignored. See <tt>write_order</tt>
  for a sample file. Note that the variable ordering cannot be specified at
  the bit-level; it can only be specified at the multi-valued variable level.

  </dl>
  ]

  
  SeeAlso     [CommandStaticOrder CommandWriteOrder]

******************************************************************************/
static int
CommandReadOrder(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int           c, status;
  FILE          *fp;
  int           verbose = 0;
  int           group = 0;
  lsList        suppliedNodeList = (lsList)NULL; /* list of Ntk_Node_t * */
  Ntk_Network_t *network;
  mdd_manager   *mddMgr;

  if (bdd_get_package_name() != CUDD) {
    fprintf(vis_stderr,
           "** ord error: read_order can be used only with the CUDD package\n");
  }

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hg:v")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      case 'g':
        group = atoi(util_optarg);
        break;
      case 'v':
        verbose = 1;
        break;
      default:
        goto usage;
    }
  }

  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  if (!Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) {
    (void) fprintf(vis_stderr,
                   "** ord error: static_order was not called yet.\n");
    return 1;
  }

  /*
   * Process the input ordering file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "order file not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "too many arguments\n");
    goto usage;
  }

  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
  if (fp == NIL(FILE)) {
    return 1;
  } else {
    boolean status;
    
    error_init();
    status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose);
    if (status == FALSE) {
      (void) fprintf(vis_stderr, "Error reading ordering file:\n");
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot perform static ordering.\n");
      (void) fclose(fp);
      return 1;
    } else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList,
                                            Ord_InputAndLatch_c) == FALSE) { 
      (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n");
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot perform read_order.\n");
      (void) fclose(fp);
      (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
      return 1;
    } else {
      (void) fclose(fp);
      if (verbose > 0) {
        (void) fprintf(vis_stdout, "\nNew variable order from file %s:\n",
                        argv[util_optind]);
        OrdNodeListWrite(vis_stdout, suppliedNodeList);
      }
    }
  }
  
  /*
   * Reorder the variables.
   */
  mddMgr = Ntk_NetworkReadMddManager(network);
  status = OrdMakeNewVariableOrder(mddMgr, suppliedNodeList, group, verbose);

  (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
  if (status)
    return 1;

  alarm(0);
  return 0;  /* Everything okay */

  usage:
  (void) fprintf(vis_stderr, "usage: read_order [-g #] [-h] [-v] file\n");
  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
  (void) fprintf(vis_stderr, "   -g #      ps/ns variables grouping\n");
  (void) fprintf(vis_stderr, "             0 : do not group ps/ns\n");
  (void) fprintf(vis_stderr, "             1 : group ps/ns (default)\n");
  (void) fprintf(vis_stderr, "   -v        verbosity on\n");
  (void) fprintf(vis_stderr, "   file      variable order file\n");

  return 1;
}


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

  Synopsis    [Implements the write_order command.]

  SideEffects [none]

  CommandName [write_order]

  CommandSynopsis [write the current order of the MDD variables of the
  flattened network] 

  CommandArguments [\[-h\] \[-o &lt;type&gt;\] \[&lt;file&gt;\]]

  CommandDescription [Write the current order of the MDD variables of the
  flattened network.  If no file name is specified, the output is written to
  stdout. A sample output is shown here.

  <pre>
  # name                 type            mddId vals levs
  system.choosing0      primary-input       31    2 (61)
  system.p0.pc          latch               32   11 (62, 63, 64, 65)
  </pre>

  The first column gives the full hierarchical path name of the node, starting
  from the current hierarchical node. The second column gives the type of the
  node in the flattened network (see the command <tt>print_network</tt>).  The third
  column gives the MDD id of the node; this can be thought of as just another
  name for the node.  The fourth column gives the number of values that the
  multi-valued variable at the output of the node can assume.  The last column
  gives the levels of the BDD variables that encode the multi-valued variable
  (0 is the topmost level of the BDD). <p>

  The bits of a multi-valued variable need not appear consecutively (due to
  dynamic variable ordering).  Each node appears at most once in the output
  file. The nodes in the file appear in ascending order of the lowest level
  bit in the encoding of the node's multi-valued variable (e.g. a node with
  levels (12, 73) will appear before a node with levels (17, 21, 25)).<p>
  
  To specify a variable ordering for static_order, a convenient tactic is to
  write out the current ordering, edit the file to rearrange the ordering (or
  comment out some nodes, using "#"), and then read the file back in using
  <tt>static_order</tt>. Note that everything after the first column is
  ignored when the file is read in.<p>

  Command options:<p>  
  
  <dl>

  <dt> -h
  <dd> Print the command usage.<p>

  <dt> -o &lt;type&gt;
  <dd> Specify the network nodes to write out.  Type can be one of the following:<p>

  <b>all:</b> Write out all the nodes of the network.  This option is
  allowed only if all variables have been ordered.<p>

  <b>input_and_latch:</b> (default) Write out the primary inputs, pseudo
  inputs, latches, and next state variables.  <p>

  <b>next_state_node:</b> Write out the next state variables (node type is
  "shadow").  This file can be modified and read back in using the
  <tt>static_order -s next_state_node</tt> command.<p>
  
  <dt> &lt;file&gt;

  <dd> File to which to write the ordering.  By default, the ordering is
  written to stdout.<p>
  
  </dl>]

******************************************************************************/
static int
CommandWriteOrder(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  FILE          *fp;
  int            status;
  Ord_OrderType  orderType = Ord_InputAndLatch_c; /* default */
  Ntk_Network_t *network;
  
  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "ho:")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      case 'o':
        orderType = StringConvertToOrderType(util_optarg);
        if (orderType == Ord_Partial_c) { 
          (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg);
          goto usage;
        }
        else if (orderType == Ord_Unassigned_c) {
          (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg);
          goto usage;
        }
        break;
      default:
        goto usage;
    }
  }

  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  /*
   * Open the destination file.
   */
  if (argc - util_optind == 0) {
    fp = Cmd_FileOpen("-", "w", NIL(char *), /* silent */0);
  }
  else if (argc - util_optind == 1) {
    fp = Cmd_FileOpen(argv[util_optind], "w", NIL(char *), /* silent */0);
  }
  else {
    goto usage;
  }
  if (fp == NIL(FILE)) {
    return 1;
  }

  error_init();
  if (Ord_NetworkPrintVariableOrder(fp, network, orderType) == 0) {
    (void) fprintf(vis_stderr, "Not all nodes are ordered: ");
    (void) fprintf(vis_stderr, "%s", error_string());
    status = 1;
  }
  else {
    status = 0;  /* success */
  }

  if (fp != stdout) {
    (void) fclose(fp);
  }
  return (status);
  
usage:
  (void) fprintf(vis_stderr, "usage: write_order [-h] [-o type] [file]\n");
  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
  (void) fprintf(vis_stderr, "   -o type   nodes to write (all, input_and_latch (default), next_state_node)\n");
  (void) fprintf(vis_stderr, "   file      output file name\n");

  return 1;
}


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

  Synopsis    [Implements the dynamic_var_ordering command.]

  SideEffects []

  CommandName [dynamic_var_ordering]

  CommandSynopsis [control the application of dynamic variable ordering]

  CommandArguments [ \[-d\] \[-e &lt;method&gt;\] \[-f &lt;method&gt;\]
  \[-h\]]

  CommandDescription [Control the application of dynamic variable ordering to the
  flattened network. Dynamic ordering is a technique to reorder the MDD
  variables to reduce the size of the existing MDDs.  When no options are
  specified, the current status of dynamic ordering is displayed.  At most one
  of the options -e, -f, and -d should be specified.  The commands
  <tt>flatten_hierarchy</tt> and <tt>static_order</tt> must be invoked before
  this command.<p>

  Dynamic ordering may be time consuming, but can often reduce the size of the
  MDDs dramatically.  The good points to invoke dynamic ordering explicitly
  (using the -f option) are after the commands <tt>build_partition_mdds</tt>
  and <tt>print_img_info</tt>.  If dynamic ordering finds a good ordering,
  then you may wish to save this ordering (using <tt>write_order</tt>) and
  reuse it (using <tt>static_order -s</tt>) in the future. A common sequence
  used to get a good ordering is the following:<p>

  <pre>
  init_verify
  print_img_info
  dynamic_var_ordering -f sift
  write_order <file>
  flatten_hierarchy
  static_order -s input_and_latch -f <file>
  build_partition_mdds
  print_img_info
  dynamic_var_ordering -f sift
  </pre>  
  
  <p>For many large examples, there is no single best variable order,
  or that order is hard to find.  For example, the best ordering
  during partitioning of the network may be different from the best
  ordering during a model check. In that case you can use automatic
  reordering, using the <tt>-e</tt> option. This will trigger
  reordering whenever the total size of the MDD increases by a certain
  factor. Often, the <tt>init</tt> command is replaced by the
  following sequence:
  
  <pre>
  flatten_hierarchy 
  static_order
  dynamic_var_ordering -e sift
  build_partition_mdds
  </pre>
  
  Command options:<p>  

  <dl>

  <dt> -d
  <dd> Disable dynamic ordering from triggering automatically.<p>
  
  <dt> -e &lt;method&gt;
  <dd> Enable dynamic ordering to trigger automatically whenever a certain
  threshold on the overall MDD size is reached. "Method" must be one of the following:<p>

  <b>window:</b> Permutes the variables within windows of three adjacent
  variables so as to minimize the overall MDD size.  This process is repeated
  until no more reduction in size occurs.<p>

  <b>sift:</b> Moves each variable throughout the order to find an optimal
  position for that variable (assuming all other variables are fixed).  This
  generally achieves greater size reductions than the window method, but is
  slower.<p>
  
  The following methods are only available if VIS has been linked with the Bdd
  package from the University of Colorado (cuBdd).</b><p>

  <b>random:</b> Pairs of variables are randomly chosen, and swapped in the
  order. The swap is performed by a series of swaps of adjacent variables. The
  best order among those obtained by the series of swaps is retained. The
  number of pairs chosen for swapping equals the number of variables in the
  diagram.<p>

  <b>random_pivot:</b> Same as <b>random</b>, but the two variables are chosen
  so that the first is above the variable with the largest number of nodes, and
  the second is below that variable.  In case there are several variables tied
  for the maximum number of nodes, the one closest to the root is used.<p>

  <b>sift_converge:</b> The <b>sift</b> method is iterated until no further
  improvement is obtained.<p>

  <b>symmetry_sift:</b> This method is an implementation of symmetric
  sifting. It is similar to sifting, with one addition: Variables that become
  adjacent during sifting are tested for symmetry. If they are symmetric, they
  are linked in a group. Sifting then continues with a group being moved,
  instead of a single variable.<p>

  <b>symmetry_sift_converge:</b> The <b>symmetry_sift</b> method is iterated
  until no further improvement is obtained.<p>

  <b>window{2,3,4}:</b> Permutes the variables within windows of n adjacent
  variables, where "n" can be either 2, 3 or 4, so as to minimize the overall
  MDD size.<p>

  <b>window{2,3,4}_converge:</b> The <b>window{2,3,4}</b> method is iterated
  until no further improvement is obtained.<p>

  <b>group_sift:</b> This method is similar to <b>symmetry_sift</b>,
  but uses more general criteria to create groups.<p>

  <b>group_sift_converge:</b> The <b>group_sift</b> method is iterated until no
  further improvement is obtained.<p>

  <b>lazy_sift:</b> This method is similar to <b>group_sift</b>, but the
  creation of groups takes into account the pairing of present and next state
  variables.<p>

  <b>annealing:</b> This method is an implementation of simulated annealing for
  variable ordering. This method is potentially very slow.<p>

  <b>genetic:</b> This method is an implementation of a genetic algorithm for
  variable ordering. This method is potentially very slow.<p>

  <dt> -f &lt;method&gt;
  <dd> Force dynamic ordering to be invoked immediately.  The values for
  method are the same as in option -e.<p>

  <dt> -h
  <dd> Print the command usage.

  <dt> -v &lt;#&gt;
  <dd> Verbosity level. Default is 0. For values greater than 0,
  statistics pertaining to reordering will be printed whenever
  reordering occurs.
  
  </dl>
  ]
  
******************************************************************************/
static int
CommandDynamicVarOrdering(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int                 c;
  bdd_reorder_type_t  currentMethod;
  bdd_reorder_type_t  dynOrderingMethod = BDD_REORDER_NONE; /* for lint */
  boolean             disableFlag       = FALSE;
  boolean             enableFlag        = FALSE;
  boolean             forceFlag         = FALSE;
  Ntk_Network_t      *network;
  int verbosityFlag = -1;
  bdd_reorder_verbosity_t reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT;

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "df:e:hv:")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      case 'f':
        forceFlag = TRUE;
        dynOrderingMethod = StringConvertToDynOrderType(util_optarg);
        if (dynOrderingMethod == BDD_REORDER_NONE) {
          (void) fprintf(vis_stderr, "unknown method: %s\n", util_optarg);
          goto usage;
        }
        break;
      case 'e':
        enableFlag = TRUE;
        dynOrderingMethod = StringConvertToDynOrderType(util_optarg);
        if (dynOrderingMethod == BDD_REORDER_NONE) {
          (void) fprintf(vis_stderr, "unknown method: %s\n", util_optarg);
          goto usage;
        }
        break;
      case 'd':
        disableFlag = TRUE;
        break;
      case 'v':
        verbosityFlag = atoi(util_optarg);
        break;
    default:
        goto usage;
    }
  }
  if (c == EOF && argc != util_optind)
    goto usage;

  switch (verbosityFlag) {
  case 0: reorderVerbosity = BDD_REORDER_NO_VERBOSITY; break;
  case 1: reorderVerbosity = BDD_REORDER_VERBOSITY; break;
  default: reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT; break;
  }
  
  /* flatten_hierarchy and static_order must have been invoked already. */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }
  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) {
    (void) fprintf(vis_stderr, "The MDD variables have not been ordered. ");
    (void) fprintf(vis_stderr, "Use static_order.\n");
    return 1;
  }

  /* At most one option is allowed. */
  if ((disableFlag && enableFlag) || (disableFlag && forceFlag)
      || (enableFlag && forceFlag)) {
    (void) fprintf(vis_stderr, "Only one of -d, -f, -e is allowed.\n");
    return 1;
  }

  /*
   * Get the current method for reading and to save in case temporarily
   * overwritten.
   */
  currentMethod = Ntk_NetworkReadDynamicVarOrderingMethod(network);
  
  /* If no options are given, then just display current status. */
  if (!(disableFlag || enableFlag || forceFlag)) {
    if (currentMethod == BDD_REORDER_NONE) {
      (void) fprintf(vis_stdout, "Dynamic variable ordering is disabled.\n");
    }
    else {
      (void) fprintf(vis_stdout, "Dynamic variable ordering is enabled ");
      (void) fprintf(vis_stdout, "with method %s.\n",
                     DynOrderTypeConvertToString(currentMethod));
    }
  }

  if (disableFlag) {
    if (currentMethod == BDD_REORDER_NONE) {
      (void) fprintf(vis_stdout, "Dynamic variable ordering is already disabled.\n");
    }
    else {
      (void) fprintf(vis_stdout, "Dynamic variable ordering is disabled.\n");
      Ntk_NetworkSetDynamicVarOrderingMethod(network, BDD_REORDER_NONE, reorderVerbosity);
    }
  }

  /*
   * Set the dynamic ordering method of the network.  Note that
   * Ntk_NetworkSetDynamicVarOrderingMethod makes the necessary call to
   * bdd_dynamic_reordering.
   */
  if (enableFlag) {
    Ntk_NetworkSetDynamicVarOrderingMethod(network, dynOrderingMethod,
                                           reorderVerbosity);
    if (bdd_get_package_name() != CUDD)
      dynOrderingMethod = Ntk_NetworkReadDynamicVarOrderingMethod(network);
    (void) fprintf(vis_stdout,
                   "Dynamic variable ordering is enabled with method %s.\n",
                   DynOrderTypeConvertToString(dynOrderingMethod));
  }

  /*
   * Force a reordering.  Note that the mddManager has to have the method set
   * before calling bdd_reorder.  This is done via a call to
   * Ntk_NetworkSetDynamicVarOrderingMethod with dynOrderingMethod.  The value
   * of the ordering method is restored afterwards.
   */
  if (forceFlag) {
    mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
    bdd_reorder_verbosity_t prevReorderVerbosity;
    prevReorderVerbosity = bdd_reordering_reporting(mddManager);

    (void) fprintf(vis_stdout, "Dynamic variable ordering forced ");
    (void) fprintf(vis_stdout, "with method %s....\n",
                   DynOrderTypeConvertToString(dynOrderingMethod));
    Ntk_NetworkSetDynamicVarOrderingMethod(network, dynOrderingMethod, reorderVerbosity);
    bdd_reorder(Ntk_NetworkReadMddManager(network));
    Ntk_NetworkSetDynamicVarOrderingMethod(network, currentMethod, prevReorderVerbosity);
  }

  return 0;  /* Everything okay */

usage:
  (void) fprintf(vis_stderr, "usage: dynamic_var_ordering [-d] [-e method] [-f method] [-h]\n");
  (void) fprintf(vis_stderr, "   -d        disable dynamic ordering\n");
  (void) fprintf(vis_stderr, "   -e method enable dynamic ordering with method (window, sift)\n");
  (void) fprintf(vis_stderr, "   -f method force dynamic ordering with method (window, sift)\n");
  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
  (void) fprintf(vis_stderr, "   -v #      verbosity level \n");
  
  return 1;
}


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

  Synopsis    [Implements the print_bdd_stats command.]

  SideEffects []

  CommandName [print_bdd_stats]

  CommandSynopsis [print the BDD statistics for the flattened network]

  CommandArguments [\[-h\]]

  CommandDescription [Print the BDD statistics for the flattened network.  The
  MDDs representing the functions of the network are themselves represented by
  BDDs via an encoding of the multi-valued variables into binary valued
  variables.  The statistics given by this command depend on the underlying
  BDD package with which VIS was linked.  To get more information about the
  statistics, consult the documentation for the given BDD package.  The
  commands <tt>flatten_hierarchy</tt> and <tt>static_order</tt> must be
  invoked before this command.<p>

  Command options:<p>  

  <dl>

  <dt> -h
  <dd> Print the command usage.

  </dl>
  ]
  
******************************************************************************/
static int
CommandPrintBddStats(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  Ntk_Network_t *network;

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  /* flatten_hierarchy and static_order must have been invoked already. */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }
  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) {
    (void) fprintf(vis_stderr, "The MDD variables have not been ordered. ");
    (void) fprintf(vis_stderr, "Use static_order.\n");
    return 1;
  }

  bdd_print_stats(Ntk_NetworkReadMddManager(network), vis_stdout);

  return 0;  /* Everything okay */

usage:
  (void) fprintf(vis_stderr, "usage: print_bdd_stats [-h]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");

  return 1;
}


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

  Synopsis    [Converts a string to an order type.]

  Description [Converts a string to an order type. If string does not refer to 
  one of the allowed order types, then returns Ord_Unassigned_c.]

  SideEffects []

******************************************************************************/
static Ord_OrderType
StringConvertToOrderType(
  char *string)
{
  if (strcmp("all", string) == 0) { 
    return Ord_All_c; 
  }
  else if (strcmp("input_and_latch", string) == 0) { 
    return Ord_InputAndLatch_c;
  }
  else if (strcmp("next_state_node", string) == 0) {
    return Ord_NextStateNode_c;
  }
  else if (strcmp("partial", string) == 0) {
    return Ord_Partial_c;
  }
  else {
    return Ord_Unassigned_c;
  }
}


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

  Synopsis    [Converts a string to a dynamic ordering method type.]

  Description [Converts a string to a dynamic ordering method type. If string
  is not "sift" or "window", then returns BDD_REORDER_NONE.]

  SideEffects []

******************************************************************************/
static bdd_reorder_type_t
StringConvertToDynOrderType(
  char *string)
{
  if (strcmp("sift", string) == 0) { 
    return BDD_REORDER_SIFT;
  }
  else if (strcmp("window", string) == 0) { 
    return BDD_REORDER_WINDOW;
  }
  else if (strcmp("random", string) == 0) { 
    return BDD_REORDER_RANDOM;
  }
  else if (strcmp("random_pivot", string) == 0) { 
    return  BDD_REORDER_RANDOM_PIVOT;
  }
  else if (strcmp("sift_converge", string) == 0) { 
    return  BDD_REORDER_SIFT_CONVERGE;
  }
  else if (strcmp("symmetry_sift", string) == 0) { 
    return  BDD_REORDER_SYMM_SIFT;
  }
  else if (strcmp("symmetry_sift_converge", string) == 0) { 
    return  BDD_REORDER_SYMM_SIFT_CONV;
  }
  else if (strcmp("window2", string) == 0) { 
    return  BDD_REORDER_WINDOW2;
  }
  else if (strcmp("window3", string) == 0) { 
    return  BDD_REORDER_WINDOW3;
  }
  else if (strcmp("window4", string) == 0) { 
    return  BDD_REORDER_WINDOW4;
  }
  else if (strcmp("window2_converge", string) == 0) { 
    return  BDD_REORDER_WINDOW2_CONV;
  }
  else if (strcmp("window3_converge", string) == 0) { 
    return  BDD_REORDER_WINDOW3_CONV;
  }
  else if (strcmp("window4_converge", string) == 0) { 
    return  BDD_REORDER_WINDOW4_CONV;
  }
  else if (strcmp("group_sift", string) == 0) { 
    return  BDD_REORDER_GROUP_SIFT;
  }
  else if (strcmp("group_sift_converge", string) == 0) { 
    return  BDD_REORDER_GROUP_SIFT_CONV;
  }
  else if (strcmp("annealing", string) == 0) { 
    return  BDD_REORDER_ANNEALING;
  }
  else if (strcmp("genetic", string) == 0) { 
    return  BDD_REORDER_GENETIC;
  }
  else if (strcmp("exact", string) == 0) { 
    return  BDD_REORDER_EXACT;
  }
  else if (strcmp("lazy_sift", string) == 0) {
    return BDD_REORDER_LAZY_SIFT;
  }
  else {
    return BDD_REORDER_NONE;
  }
}


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

  Synopsis    [Converts a dynamic ordering method type to a string.]

  Description [Converts a dynamic ordering method type to a string.  This
  string must NOT be freed by the caller.]

  SideEffects []

******************************************************************************/
static char *
DynOrderTypeConvertToString(
  bdd_reorder_type_t method)
{
  if (method == BDD_REORDER_SIFT) {
    return "sift"; 
  }
  else if (method == BDD_REORDER_WINDOW) {
    return "window"; 
  }
  else if (method == BDD_REORDER_NONE) {
    return "none"; 
  }
  else if (method == BDD_REORDER_RANDOM) { 
    return "random";
  }
  else if (method == BDD_REORDER_RANDOM_PIVOT) { 
    return "random_pivot";
  }
  else if (method == BDD_REORDER_SIFT_CONVERGE) { 
    return "sift_converge";
  }
  else if (method == BDD_REORDER_SYMM_SIFT) { 
    return "symmetry_sift";
  }
  else if (method == BDD_REORDER_SYMM_SIFT_CONV) { 
    return "symmetry_sift_converge";
  }
  else if (method == BDD_REORDER_WINDOW2) { 
    return "window2";
  }
  else if (method == BDD_REORDER_WINDOW3) { 
    return "window3";
  }
  else if (method == BDD_REORDER_WINDOW4) { 
    return "window4";
  }
  else if (method == BDD_REORDER_WINDOW2_CONV) { 
    return "window2_converge";
  }
  else if (method == BDD_REORDER_WINDOW3_CONV) { 
    return "window3_converge";
  }
  else if (method == BDD_REORDER_WINDOW4_CONV) { 
    return "window4_converge";
  }
  else if (method == BDD_REORDER_GROUP_SIFT) { 
    return "group_sift";
  }
  else if (method == BDD_REORDER_GROUP_SIFT_CONV) { 
    return "group_sift_converge";
  }
  else if (method == BDD_REORDER_ANNEALING) { 
    return "annealing";
  }
  else if (method == BDD_REORDER_GENETIC) { 
    return "genetic";
  }
  else if (method ==  BDD_REORDER_EXACT) { 
    return "exact";
  }
  else if (method == BDD_REORDER_LAZY_SIFT) {
    return "lazy_sift";
  }
  else {
    fail("unrecognized method");
    return NIL(char); /* not reached */
  }
}


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

  Synopsis    [Verifies that suppliedNodeList has the correct nodes.]

  Description [Returns TRUE if the set of nodes in suppliedNodeList matches
  the set of nodes in network specified by orderType; else returns FALSE and
  writes a message to error_string. OrderType should be one of the following:
  1) Ord_All_c: should match the set of all nodes in network; 2)
  Ord_InputAndLatch_c: should match the set of inputs (primary + pseudo),
  latches, and next state nodes; 3) Ord_NextStateNode_c: should match the set
  of next state nodes; number should be the number of latches; 4)
  Ord_Partial_c: returns TRUE automatically.]

  SideEffects []

******************************************************************************/
static boolean
NetworkCheckSuppliedNodeList(
  Ntk_Network_t * network,
  lsList  suppliedNodeList,
  Ord_OrderType  orderType)
{
  lsGen         gen;
  st_generator *stGen;
  Ntk_Node_t   *node;
  st_table     *requiredNodes;
  st_table     *suppliedNodes;
  char         *dummy;
  boolean       returnFlag = TRUE;
  
  assert(orderType != Ord_Unassigned_c);

  if (orderType == Ord_Partial_c) {
    return TRUE;
  }
  
  /* At this point, orderType must be one of the these. */
  assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c)
         || (orderType == Ord_NextStateNode_c));
  

  /*
   * Build up the table of required nodes. Next state nodes are included by
   * all 3 order types. 
   */
  requiredNodes = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachNode(network, gen, node) {
    if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) {
      st_insert(requiredNodes, (char *) node, NIL(char));
    }
    else if ((orderType == Ord_InputAndLatch_c)
             && Ntk_NodeTestIsCombInput(node)) {
      st_insert(requiredNodes, (char *) node, NIL(char));
    }
    /* else, this node is not included by orderType */
  }

  /*
   * Convert suppliedNodeList to the table of supplied nodes.
   */
  suppliedNodes = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(suppliedNodeList, gen, node) {
    int status = st_insert(suppliedNodes, (char *) node, NIL(char));
    if (status) {
      error_append("node ");
      error_append(Ntk_NodeReadName(node));
      error_append(" appears more than once in ordering file\n");
      returnFlag = FALSE;
    }
  }

  /*
   * Check that suppliedNodes is contained in requiredNodes.
   */
  st_foreach_item(suppliedNodes, stGen, &node, &dummy) {
    if (!st_is_member(requiredNodes, node)) {
      error_append("node ");
      error_append(Ntk_NodeReadName(node));
      error_append(" supplied but not required\n");
      returnFlag = FALSE;
    }
  }
  
  /*
   * Check that suppliedNodes is contained in requiredNodes.
   */
  st_foreach_item(requiredNodes, stGen, &node, &dummy) {
    if (!st_is_member(suppliedNodes, node)) {
      error_append("node ");
      error_append(Ntk_NodeReadName(node));
      error_append(" required but not supplied\n");
      returnFlag = FALSE;
    }
  }
  
  st_free_table(requiredNodes);
  st_free_table(suppliedNodes);
  return returnFlag;
}


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

  Synopsis    [Handle function for timeout.]

  Description [This function is called when the time out occurs.]

  SideEffects []

******************************************************************************/
static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
}