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

  FileName    [restrCmd.c]

  PackageName [restr]

  Synopsis    [Command interface for the restr package.]

  Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]

  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

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

#include "restrInt.h"

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


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


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


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

static jmp_buf timeOutEnv;
int restrCreatedPart;
int restrCreatedFsm;
boolean restrVerbose;

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

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

static int CommandRestructureFsm(Hrc_Manager_t **hmgr, int argc, char **argv);
static void TimeOutHandle(void);
static st_table * readInputProbabilities(Ntk_Network_t *network, FILE *fp);
static void CleanUp(Ntk_Network_t *network1, st_table *inputProb, char *outOrderFileName, char *dumpFileName, char *prefix, int varOrdered, int restrCreatedPart, int restrCreatedFsm, char *probFile);
static enum st_retval stCountFree(char *key, char *value, char *arg);
static int IsPartitionValid(Ntk_Network_t *network, graph_t *partition);
static int TestIsNetworkMultipleValued(Ntk_Network_t *network);

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


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

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

  Synopsis    [This function initializes the restr package.]

  SideEffects [None]

  SeeAlso     [Restr_End]

******************************************************************************/
void
Restr_Init(void)
{
  Cmd_CommandAdd("restruct_fsm", CommandRestructureFsm, 0);
}

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

  Synopsis    [This function ends the restr package.]

  SideEffects [None]

  SeeAlso     [Restr_Init]

******************************************************************************/
void
Restr_End(void)
{

} /* End of Restr_End */


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

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


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

  Synopsis [Implements the <tt>restruct_fsm</tt> command.]

  Description [This command implements an State Transition Graph (STG)
  restructuring algorithm that exploits the existence of equivalent
  states to decrease power dissipation, not necessarily by collapsing
  the equivalence states, but by redirecting transitions in the
  graph. This algorithm is based on the monolithic transition relation. The
  complexity of the algorithm in general increases with an increase in
  the size of the state transition graph, which depends on the number
  of state variables and primary inputs. For more details see, "A
  Symbolic Algorithm for Low-Power Sequential Synthesis", ISLPED 97.]

  SideEffects [None]

  SeeAlso []

  CommandName [restruct_fsm]

  CommandSynopsis [Restructre the STG of a finite state machine to
  reduce power dissipation.]

  CommandArguments [\[-D &lt;fileHead&gt;\] \[-d &lt;divMethod&gt;\] \[-E\]
  \[-F &lt;factMethod&gt;\] \[-f &lt;probFile&gt;\] \[-h\] \[-N\] \[-o
  &lt;orderFile&gt;\] \[-p &lt;string&gt;\] \[-s &lt;restrMethod&gt;\] \[-t
  &lt;seconds&gt;\] \[-v\]]

  CommandDescription [This command implements an STG restructuring
  algorithm that exploits the existence of equivalent states to
  decrease power dissipation, not necessarily by collapsing the
  equivalence states, but by redirecting transitions in the state
  transition graph (STG). This algorithm is based on monolithic
  transition relation. The complexity of the algorithm in general
  increases with an increase in the size of the STG. The number of
  states and edges in the STG are exponential in the number of state
  variables and primary inputs. The memory utilization is not
  necessarily exponential due to symbolic representation of the
  STG. For more details see, "A Symbolic Algorithm for Low-Power
  Sequential Synthesis", ISLPED 97.

  This command works only if VIS is compiled with CUDD package. The
  algorithm can handle circuits described in both BLIF and BLIF-MV
  format. However, multi-valued variables are not supported. Also, the
  final synthesized circuit (network implementation of the restructured
  STG) is available only in BLIF format. The sequential circuit should
  have a single initial state.

  A network should have been created for the circuit and its primary
  inputs and state variables assigned BDD ids prior to the invocation
  of this command. A network can be created by the command
  <tt>flatten_hierarchy</tt> and command <tt>static_order</tt> assigns
  BDD ids to the input and state variables. The command proceeds by
  creating BDDs for the outputs and next state functions. An FSM data
  structure is then created on which subsequent operations are
  performed. After the STG is restructured a new circuit is
  synthesized by symbolic factorization based on Zero-Suppressed
  Decision Diagrams (ZDDs). The final synthesized circuit is a file in
  BLIF format with ".ml.blif" as the extension.

  <p>
  The typical command flow in vis is the following: <br><br>
  <code>
  vis> read_blif foo.blif <br>
  vis> flatten_hierarchy <br>
  vis> static_order <br>
  vis> dynamic_var_ordering -e sift <br>
  vis> restruct_fsm
  </code>

  <p>

  In the above case example, the final synthesized circuit is
  MODEL.ml.blif if the name of the design in foo.blif is MODEL.
  <br><br>
  <b> Command options: </b> <br>

  <dl>

  <dt> -A 
  <dd> Allow realignment (during symbolic factorization) of ZDDs
  after BDD reordering and vice versa.  This option is effective
  when only one of the BDD or ZDD variable reordering is enabled. <p>

  <dt> -D &lt;fileHead&gt;
  <dd> Specify the output file name for synthesized circuit. File extension
  is not necessary. By default, the model name of the circuit is used. For 
  example, -D foobar, will result in foobar.ml.blif <p>

  <dt> -d &lt;divMethod&gt; 
  <dd> Choose a divisor. See <tt>synthesize_network</tt> for more details.<p>

  <dt> -E
  <dd> Print the number of equivalence classes in the FSM. <p>

  <dt> -F &lt;probFile&gt;
  <dd> File with primary input probabilities, one per line. 
  <tt>input_name</tt> &lt;probability&gt; <p>

  <dt> -f &lt;factMethod&gt; 
  <dd> Choose a method for factorization. See <tt>synthesize_network</tt> for
  more details.<p>

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

  <dt> -i &lt;string&gt;
  <dd> Specify the prefix to be used to generate names for internal 
  nodes during synthesis. By default, the prefix is "_n". <p>

  <dt> -N
  <dd> Expand the reachable set R to include those states which are equivalent 
  to R but not reachable. The default is not to include such states. <p>

  <dt> -o &lt;orderFile&gt;
  <dd> File to output BDD variable ordering after the restructured 
  circuit is synthesized. <p>

  <dt> -R &lt;value&gt;
  <dd> Allow reordering in BDD and/or ZDD variables during symbolic 
  factorization stage. <p>
  0 : (default) No reordering neither in BDD nor in ZDD. <p>
  1 : Allows reordering only in BDD, not in ZDD. <p>
  2 : Allows reordering only in ZDD, not in BDD. <p>
  3 : Allows reordering both in BDD and in ZDD. <p>

  <dt> -s &lt;heuristic&gt; 
  
  <dd> Heuristic to perform restructuring. Consider a fragment of an
  STG containing states A,B and C and an edge from A to B. Let B and C
  be equivalent. Since B and C are equivalent, it is possible to
  change the transition between A and B to A and C. In the more
  general case, the choice can be driven by different cost
  constraints. The following are the heuristics: <br>

  <dd> ham : Hamming distance based heuristic. An edge is chosen that reduces
  the Hamming distance (or state bit transitions) between the states.<br>

  <dd> fanin : Fanin oriented heuristic. A representative from the equivalence
  class is chosen that reduces the total average state bit switching on the
  incoming edges. <br> 

  <dd> faninout : Fanin-Fanout oriented heuristic. A representative from the
  equivalence class is chosen that reduces the total average state bit
  switching on the incoming as well as outgoing edges. <br>

  <dd> cproj : A simple C-Projection. A representative from the
  equivalence class is chosen which is closest to the initial
  state. The distance d(x,y) is defined as:
  <br><br>
  \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}).<p>

  <dt> -T
  <dd> Try to share more nodes during symbolic factorization. Existing
  divisors are checked for potential reuse before extracting divisors from the
  current boolean function.<p>

  <dt> -t &lt;seconds&gt;
  <dd> Time in seconds allowed to complete the command. If the computation time
  goes above that limit, the process is aborted.  The default is no limit.<p>

  <dt> -v
  <dd> Turn on verbosity. <p>

  <dt> See also command : synthesize_network <p>

  </dl>
  ]

  SideEffects [Package specific information is stored in the network and
  cleared at the end.]

  SeeAlso []

******************************************************************************/
static int
CommandRestructureFsm(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
  graph_t *partition = NIL(graph_t);
  Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t);
  Ntk_Network_t *network1 = NIL(Ntk_Network_t);
  Hrc_Node_t *currentNode = NIL(Hrc_Node_t);
  lsList dummy = (lsList) 0;
  char *modelName,*str;
  int timeOutPeriod;
  boolean status;
  int c;
  long initialTime, finalTime;
  RestructureHeuristic heuristic;
  boolean equivClasses, nonReachEquiv;
  boolean eqvMethod;
  int varOrdered;
  char *outOrderFileName,*blifName;
  char *dumpFileName,*probFile;
  int reorder,trySharing,realign;
  FILE *fp;
  st_table *inputProb = NULL;

    /* Synthesis related options */
  Synth_InfoData_t *synthInfo;
  int factoring, divisor;
  char *prefix;
  
  if (bdd_get_package_name() != CUDD) {
    (void) fprintf(vis_stderr,
		   "** restr error: The restr package can be used only with CUDD package\n");
    (void) fprintf(vis_stderr,"** restr error: Please link with CUDD package\n");
    return 0;
  }
	
  /* These are the default values. */
  timeOutPeriod   = 0;  
  status          = FALSE;
  restrVerbose	  = 0;
  equivClasses    = 0;
  nonReachEquiv   = 0;
  eqvMethod       = 0;
  heuristic	  = RestrHammingD_c;
  fp 		  = NIL(FILE);
  outOrderFileName = NIL(char);
  dumpFileName = NIL(char);
  probFile = NIL(char);
  restrCreatedPart = 0;
  restrCreatedFsm = 0;
  varOrdered = 0;

  /* Synthesis related default values */
  factoring = 0;
  divisor = 1;
  prefix = NIL(char);
  reorder = 0;
  trySharing = 0;
  realign = 0;

  util_getopt_reset();

  while((c = util_getopt(argc, argv, "f:d:i:EeNvD:o:t:s:F:R:TAh")) != EOF) {
    switch(c) {
    case 'f':
      factoring = atoi(util_optarg);
      break;
    case 'd':
      divisor = atoi(util_optarg);
      break;
    case 'i':
      prefix = util_strsav(util_optarg);
      break;
    case 'E':
      equivClasses = 1;
      break;
    case 'e':
      eqvMethod = 1;
      break;
    case 'N':
      nonReachEquiv = 1;
      break;
    case 'v':
      restrVerbose = 1;
      break;
    case 'D':
      dumpFileName = util_strsav(util_optarg);
      break;
    case 'o':
      outOrderFileName = util_strsav(util_optarg);
      /* Check if the file specified to dump variable order already exists */
      fp = Cmd_FileOpen(outOrderFileName,"r",NIL(char *),1);
      if (fp) {
	(void) fprintf(vis_stderr,"** restr error: Output order file %s already exists.\n",
		       outOrderFileName);
	(void) fprintf(vis_stderr,"** restr error: Please specify another name.\n");
	fclose(fp);
	FREE(outOrderFileName);
	goto endgame;
      }
      break;
    case 't':
      timeOutPeriod = atoi(util_optarg);
      break;
    case 's':
      str = util_strsav(util_optarg);
      if (strcmp(str,"ham") == 0) {
	heuristic = RestrHammingD_c;
      } else if (strcmp(str,"fanin") == 0) {
	heuristic = RestrFanin_c;
      } else if (strcmp(str,"faninout") == 0) {
	heuristic = RestrFaninFanout_c;
      } else if (strcmp(str,"cproj") == 0) {
	heuristic = RestrCProjection_c;
      } else {
	(void) fprintf(vis_stderr,"** restr warning: Invalid option %s\n",str);
	(void) fprintf(vis_stderr,"** restr warning: Using Hamming distance heuristic\n\n");
	heuristic = RestrHammingD_c;
      }
      FREE(str);
      break;
    case 'F':
      probFile = util_strsav(util_optarg);
      fp = Cmd_FileOpen(probFile,"r",NIL(char *),1);
      if (!fp) {
	fprintf(vis_stderr,"** restr warning: Cannot open %s \n",probFile);
	fprintf(vis_stderr,"** restr warning: Assuming equi probable primary inputs\n");
	FREE(probFile);
	probFile = NIL(char);
      } else {
	fclose(fp);
      }
      break;
    case 'R':
      /* Option to enable/disable reordering during synthesis
         (factorization) stage */
      reorder = atoi(util_optarg);
      break;
    case 'T':
      /* During factorization maximize sharing of nodes */
      trySharing = 1;
      break;
    case 'A':
      /* Realign ZDD variables after BDD variable reordering and vice
         versa */
      realign = 1;
      break;
    case 'h':
      goto usage;
    default:
      goto usage;
    }
  }

  if(Hrc_ManagerReadCurrentNode(*hmgr) == NIL(Hrc_Node_t)) {
    (void) fprintf(vis_stderr,"** restr error: The hierarchy manager is empty.");
    (void) fprintf(vis_stderr," Read in design.\n");
    goto endgame;
  }

  network1 = (Ntk_Network_t *) 
    Hrc_NodeReadApplInfo(Hrc_ManagerReadCurrentNode(*hmgr), 
			 NTK_HRC_NODE_APPL_KEY);

  if(network1 == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stderr,"** restr error: There is no network. ");
    (void) fprintf(vis_stderr,"Use flatten_hierarchy.\n");
    goto endgame;
  }

  if(!Ntk_NetworkReadNumLatches(network1)) {
    (void) fprintf(vis_stderr,"**restr error: No latches present in the ");
    (void) fprintf(vis_stderr,"current network.\n");
    (void) fprintf(vis_stderr,"** restr error: This algorithm does not apply.\n");
    goto endgame;
  }

  /* Check if the current network has signals with multiple values. */
  if (TestIsNetworkMultipleValued(network1)) {
    (void) fprintf(vis_stderr,"** restr error: Circuit has multiple valued variables.\n");
    (void) fprintf(vis_stderr,"** restr error: This algorithm applies to boolean signals only.\n");
    goto endgame;
  }

  if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
     Ntk_NetworkReadNumInputs(network1)) {
    (void) fprintf(vis_stderr,"** restr error: Pseudo inputs present in the network.\n");
    (void) fprintf(vis_stderr,"** restr error: This algorithm does not apply.\n");
    goto endgame;
  }

  if (!dumpFileName)
    dumpFileName = util_strsav(Ntk_NetworkReadName(network1));
  /* Check if the output blif file already exists */
  blifName = util_strcat3(dumpFileName,".ml.blif","");
  fp = Cmd_FileOpen(blifName,"r",NIL(char *),1);
  if (fp) {
    (void) fprintf(vis_stderr,"** restr error: Output blif file %s already exists.\n",
		   blifName);
    (void) fprintf(vis_stderr,"** restr error: Please specify another name.\n");
    fclose(fp);
    FREE(blifName);
    goto endgame;
  }
  FREE(blifName);


  /* Check if the network has the variables ordered */
  if (Ord_NetworkTestAreVariablesOrdered(network1, Ord_InputAndLatch_c) == 
      FALSE) {
    Ord_NetworkOrderVariables(network1,Ord_RootsByDefault_c,
			      Ord_NodesByDefault_c, FALSE,
			      Ord_InputAndLatch_c,Ord_Unassigned_c,
			      dummy,0);
    varOrdered = 1;
  }

  /* If primary input probabilities are specified, read them */
  if (probFile) {
    fp = Cmd_FileOpen(probFile,"r",NIL(char *),1);
    inputProb = readInputProbabilities(network1,fp);
    fclose(fp);
    FREE(probFile);
    fp = NIL(FILE);
  }

  /* Check if there is an FSM already attached to the network */
  fsm = (Fsm_Fsm_t *) Ntk_NetworkReadApplInfo(network1, 
					      FSM_NETWORK_APPL_KEY);
  if (fsm == NIL(Fsm_Fsm_t)) {
    partition = (graph_t *) Ntk_NetworkReadApplInfo(network1,
						    PART_NETWORK_APPL_KEY);
    /* If there is none then create one. */
    if (partition == NIL(graph_t) ||
	(!IsPartitionValid(network1,partition))) {
      currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
      modelName = Hrc_NodeReadModelName(currentNode);
      partition = Part_NetworkCreatePartition(network1, currentNode,
					      modelName, (lsList) 0, 
					      (lsList) 0, NIL(mdd_t), 
					      Part_InOut_c, (lsList) 0, 
					      FALSE, FALSE, TRUE);
 
      Ntk_NetworkAddApplInfo(network1, RESTR_PART_NETWORK_APPL_KEY,
			     (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
			     (void *) partition);
      restrCreatedPart = 1;
    }
    fsm = Fsm_FsmCreateFromNetworkWithPartition(network1, 
						Part_PartitionDuplicate(partition));
    if (fsm == NIL(Fsm_Fsm_t)) {
      (void) fprintf(vis_stderr,"** restr error: Could not create ");
      (void) fprintf(vis_stderr,"an Fsm\n");
      goto endgame;
    }
    Ntk_NetworkAddApplInfo(network1, RESTR_FSM_NETWORK_APPL_KEY,
			   (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
			   (void *) fsm);
    restrCreatedFsm = 1;
  } else {
    partition = (graph_t *) Fsm_FsmReadPartition(fsm);

    if (partition == NIL(graph_t) || 
	(!IsPartitionValid(network1,partition))) {
      currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
      modelName = Hrc_NodeReadModelName(currentNode);
      partition = Part_NetworkCreatePartition(network1, currentNode,
					      modelName, (lsList) 0, 
					      (lsList) 0, NIL(mdd_t), 
					      Part_InOut_c, (lsList) 0, 
					      FALSE, FALSE, TRUE);
      Ntk_NetworkAddApplInfo(network1, RESTR_PART_NETWORK_APPL_KEY,
			     (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
			     (void *) partition);
      restrCreatedPart = 1;

      fsm = Fsm_FsmCreateFromNetworkWithPartition(network1, 
						  Part_PartitionDuplicate(partition));
      if (fsm == NIL(Fsm_Fsm_t)) {
	(void) fprintf(vis_stderr,"** restr error: Could not create ");
	(void) fprintf(vis_stderr,"an Fsm\n");
	goto endgame;
      }
      Ntk_NetworkAddApplInfo(network1, RESTR_FSM_NETWORK_APPL_KEY,
			     (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
			     (void *) fsm);
      restrCreatedFsm = 1;
    }
  }

  /* Start the timer before calling restruct. */
  if (timeOutPeriod > 0){
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stderr, "** restr warning: Timeout occurred after ");
      (void) fprintf(vis_stderr, "%d seconds.\n", timeOutPeriod);
      alarm(0);
      goto endgame;
    }
  }

  /* Prepare the data structure for the synthesis package */
  synthInfo = Synth_InitializeInfo(factoring,divisor,0,
				   reorder,trySharing,realign,
				   dumpFileName,prefix,0);

  initialTime = util_cpu_time();
  status = RestrCommandRestructureFsm(fsm, heuristic,outOrderFileName,
				      equivClasses,nonReachEquiv,
				      eqvMethod,inputProb,synthInfo);
  finalTime = util_cpu_time();
  if(status) {
    (void) fprintf(vis_stdout, "%-20s%10ld\n", "RESTR: analysis time =",
		   (finalTime-initialTime)/1000);

  }
  else {
    (void) fprintf(vis_stdout, "** restr error: Could not restructure successfully.\n");
  }
    
  if (synthInfo)
    Synth_FreeInfo(synthInfo);

    /* Clean up */
  CleanUp(network1,inputProb,outOrderFileName,dumpFileName,prefix,
	  varOrdered,restrCreatedPart,restrCreatedFsm,probFile);

  alarm(0);
  return 0;  /* normal exit */

endgame:
  /* Clean up */
  CleanUp(network1,inputProb,outOrderFileName,dumpFileName,prefix,
	  varOrdered,restrCreatedPart,restrCreatedFsm,probFile);
    
  return 1; /* Error exit */

usage:
  if (outOrderFileName)
    FREE(outOrderFileName);
  if (dumpFileName)
    FREE(dumpFileName);
  if (prefix)
    FREE(prefix);
  if (probFile)
    FREE(probFile);

  (void) fprintf(vis_stderr, "\nusage: Also see help restruct_fsm for more details.\n\n");
  (void) fprintf(vis_stderr, "    -A      \t\tAllow realignment--during symbolic factorization--of BDD\n");
  (void) fprintf(vis_stderr, "            \t\tand ZDD variables after reordering.\n\n");
  (void) fprintf(vis_stderr, "    -D <fileHead>\tOutput file name for synthesized circuit.\n");
  (void) fprintf(vis_stderr, "            \t\tDefault: model_name.ml.blif\n\n");
  (void) fprintf(vis_stderr, "    -d <divMethod>\tChoose a divisor during synthesis. See\n");
  (void) fprintf(vis_stderr, "            \t\tsynthesize_network command for more details.\n");
  (void) fprintf(vis_stderr, "            \t\t0 : Fast divisor\n");
  (void) fprintf(vis_stderr, "            \t\t1 : Least occuring literal divisor (default)\n");
  (void) fprintf(vis_stderr, "            \t\t2 : Most occuring literal divisor\n");
  (void) fprintf(vis_stderr, "            \t\t3 : Level-0 kernel divisor\n\n");
  (void) fprintf(vis_stderr, "    -E      \t\tPrint the number of equivalence classes in the STG.\n\n");
  (void) fprintf(vis_stderr, "    -F <probFile>\tInput file with PI probabilities, one per line.\n\n");
  (void) fprintf(vis_stderr, "    -f <factMethod>\tChoose a factorization method. See synthesize_network\n");
  (void) fprintf(vis_stderr, "            \t\tfor more details.\n");
  (void) fprintf(vis_stderr, "            \t\t0 : Simple factoring (default)\n");
  (void) fprintf(vis_stderr, "            \t\t1 : Generic factoring\n\n");
  (void) fprintf(vis_stderr, "    -h      \t\tPrint command usage.\n\n");
  (void) fprintf(vis_stderr, "    -i <name>\t\tPrefix to be used to generate names for internal\n");
  (void) fprintf(vis_stderr, "            \t\tnodes during synthesis. Default: \"_n\"\n\n");
  (void) fprintf(vis_stderr, "    -N      \t\tExpand the reachable set R to include those states\n");
  (void) fprintf(vis_stderr, "            \t\twhich are equivalent to R but unreachable.\n");
  (void) fprintf(vis_stderr, "            \t\tThe default is not to include.\n\n");
  (void) fprintf(vis_stderr, "    -o <orderFile>\tFile to output BDD variable order at the end.\n\n");
  (void) fprintf(vis_stderr, "    -R <value>\t\tSet reordering (0-3)\n");
  (void) fprintf(vis_stderr, "            \t\t0 : no reordering (default)\n");
  (void) fprintf(vis_stderr, "            \t\t1 : reordering in only BDD\n");
  (void) fprintf(vis_stderr, "            \t\t2 : reordering on only ZDD\n");
  (void) fprintf(vis_stderr, "            \t\t3 : reordering on both\n\n");
  (void) fprintf(vis_stderr, "    -s <heuristic>\tHeuristic to perform restructuring.\n");
  (void) fprintf(vis_stderr, "            \t\tType help restruct_fsm for more details on each option.\n");
  (void) fprintf(vis_stderr, "            \t\tham : Hamming distance based heuristic. (Default)\n");
  (void) fprintf(vis_stderr, "            \t\tfanin : Fanin oriented heuristic.\n");
  (void) fprintf(vis_stderr, "            \t\tfaninout : Fanin-Fanout oriented heuristic.\n");
  (void) fprintf(vis_stderr, "            \t\tcproj : C-Projection based heuristic.\n\n");
  (void) fprintf(vis_stderr, "    -T      \t\tTry to share mode nodes during symbolic factorization.\n\n");
  (void) fprintf(vis_stderr, "    -t <seconds>\tTime in seconds to complete the command. The command\n");
  (void) fprintf(vis_stderr, "            \t\tis aborted if computation time goes above this limit.\n\n");
  (void) fprintf(vis_stderr, "    -v      \t\tTurn on verbosity.\n");


  return 1;    /* error exit */
}

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

  Synopsis    [Handle function for timeout.]

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

  SideEffects []

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


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

  Synopsis    [Reads the input probabilities of primary inputs.]

  Description [Reads the input probabilities of primary inputs.]

  SideEffects [None]
  
  SeeAlso []

******************************************************************************/
static st_table *
readInputProbabilities(
  Ntk_Network_t *network,
  FILE *fp)

{
  Ntk_Node_t *node;
  char name[MAX_NAME_LEN];
  double value;
  double *valuePtr;
  st_table *inputProb;

  inputProb = st_init_table(st_numcmp,st_numhash);

  while (fscanf(fp, "%s %lf\n", name, &value) != EOF) {
    node = Ntk_NetworkFindNodeByName(network,name);
    if (node == NIL(Ntk_Node_t)) {
      (void) fprintf(vis_stderr,"** restr error: No node by name %s in the network\n",name);
      (void) fprintf(vis_stderr,"** restr error: Aborting.\n");
      st_foreach(inputProb,stCountFree,NIL(char));
      st_free_table(inputProb);
      return NULL;
    }
    if (!Ntk_NodeTestIsPrimaryInput(node)) {
      fprintf(vis_stderr,"** restr warning: <%s> is not a primary input.\n",name);
      fprintf(vis_stderr,"** restr warning: Assuming equiprobable primary inputs\n");
      st_foreach(inputProb,stCountFree,NIL(char));
      st_free_table(inputProb);
      return NULL;
    }
    valuePtr = ALLOC(double,1);
    if (value > 1.0) {
      (void) fprintf(vis_stderr,"** restr warning: %s has prob. value greater than 1: %g\n",
		     name,value);
      (void) fprintf(vis_stderr,"** restr warning: Assuming a prob. value of 0.5\n");
      *valuePtr = 0.5;
    } else {
      *valuePtr = value;
    }
    st_insert(inputProb,(char *)(long)Ntk_NodeReadMddId(node),(char *)valuePtr);
  }

  return inputProb;
}

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

  Synopsis    [Free memory at the end of the task.]

  Description [Free memory at the end of the task.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static void
CleanUp(
  Ntk_Network_t *network1,
  st_table *inputProb,
  char *outOrderFileName,
  char *dumpFileName,
  char *prefix,
  int varOrdered,
  int restrCreatedPart,
  int restrCreatedFsm,
  char *probFile)
{
  Ntk_Node_t *node;
  lsGen gen;

  if (inputProb) {
    st_foreach(inputProb,stCountFree,NIL(char));
    st_free_table(inputProb);
  }
    
  if (outOrderFileName)
    FREE(outOrderFileName);
  if (dumpFileName)
    FREE(dumpFileName);
  if (prefix)
    FREE(prefix);
  if (probFile)
    FREE(probFile);

  /* Set the mdd id's for all the primary inputs, latches and next
   * state nodes to UNASSIGNED if it was specifically set in this
   * routine.
   */
  if (varOrdered) {
    Ntk_NetworkForEachPrimaryInput(network1,gen,node) {
      Ntk_NodeSetMddId(node,NTK_UNASSIGNED_MDD_ID);
    }
    Ntk_NetworkForEachLatch(network1,gen,node) {
      Ntk_Node_t *shadow;
      shadow = Ntk_NodeReadShadow(node);
      Ntk_NodeSetMddId(node,NTK_UNASSIGNED_MDD_ID);    
      Ntk_NodeSetMddId(shadow,NTK_UNASSIGNED_MDD_ID);    
    }
  }
  /* Delete the partition hooked to the network if it was created in
   * this routine.
   */
  if (restrCreatedPart) {
    Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY);
  }
  /* Delete the FSM hooked to the network if it was created in
   * this routine.
   */
  if (restrCreatedFsm) {
    Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY);
  }
}

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

  Synopsis    [Procedure to delete values stored in an st_table.]

  Description [Procedure to delete values stored in an st_table.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static enum st_retval
stCountFree(
  char *key,
  char *value,
  char *arg)
{
  double	*d;
  
  d = (double *)value;
  FREE(d);
  return(ST_CONTINUE);
  
} /* end of stCountfree */


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

  Synopsis    [Checks whether partition is valid.]

  Description [Checks whether partition is valid. The condition is that the
  given partition should have a vertex for each combinational output (PO and
  NS) and combinational input (PI and PS) of the network.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
IsPartitionValid(Ntk_Network_t *network,
		 graph_t *partition)
{
  Ntk_Node_t *node;
  lsGen gen;
  char *name;

  Ntk_NetworkForEachCombOutput(network, gen, node) {
    name = Ntk_NodeReadName(node);
    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
      return(0);
    }
  }
  Ntk_NetworkForEachCombInput(network, gen, node) {
    name = Ntk_NodeReadName(node);
    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
      return(0);
    }
  }

  return 1;
}

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

  Synopsis    [Checks whether the network has multiple valued signals.]

  Description [Checks whether the network has multiple valued
  signals. Returns 1 if true, else 0.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
TestIsNetworkMultipleValued(Ntk_Network_t *network)
{
  Ntk_Node_t *node;
  lsGen gen;
  Var_Variable_t *var;
  int numValues;

  Ntk_NetworkForEachNode(network,gen,node) {
    var = Ntk_NodeReadVariable(node);
    numValues = Var_VariableReadNumValues(var);
    if (numValues > 2)
      return 1;
  }
  return 0;
}