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

  FileName    [ ioWriteBlifIo.c ]

  PackageName [ io ]

  Synopsis    [ This file contains blifmv -> blif write routines that handle
                the functionality of files IO.]

  Description [ Routines for writing determinized, encoded tables to a file
                as requested by the write_blif command. All file IO routines
                are contained in this file. ]

  SeeAlso     [ ioReadBlifmv.c, ioWriteBlif.c, ioWriteBlifUtil.c]

  Author      [ Sunil P. Khatri ]

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

static char rcsid[] UNUSED = "$Id: ioWriteBlifIo.c,v 1.13 2005/05/14 02:15:22 fabio Exp $";

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



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

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

static void _IoEncodeWriteVariable(Var_Variable_t *var, FILE *encFp, int varIsOutput, st_table *encOutputsStTable, st_table *encInputsStTable);
static void _IoEncodeWriteVariableSpecial(Var_Variable_t *var, FILE *encFp, int varIsOutput, st_table *encOutputsStTable, st_table *encInputsStTable);

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


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


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

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

  Synopsis	[ Writes out mv->binary encoding tables  for relevant variables]

  Description	[ ]

  SideEffects	[ ]

  SeeAlso	[  ]
************************************************************************/
void
IoEncWriteMvToBinTables(
  Hrc_Node_t *hnode, 
  FILE *encFp, 
  st_table *encOutputsStTable, 
  st_table *encInputsStTable,
  int combinationalOnly
  )
{
  int i;
  Var_Variable_t *var;
  st_generator *gen;
  char *childname;
  Hrc_Node_t *childnode;
  
  /* latch IOs encoding tables not handled here */
  /* if a PI or SO drives a latch, then in the combinational case, this
     PI is not encoded (since the (mv) latch will be reinstated after
     sis optimization. In the non-comvinational case ("wl" or "wl -l")
     every PI and SO is encoded. 
  */
  if(combinationalOnly){
    Hrc_NodeForEachFormalInput(hnode, i, var){
      if(!((Var_VariableReadNumFanoutTables(var) == 0))){
	_IoEncodeWriteVariable(var, encFp, 0, encOutputsStTable, encInputsStTable);
      }
    }
    Hrc_NodeForEachChild(hnode, gen, childname, childnode){
      Hrc_NodeForEachActualOutput(childnode, i, var){
	if(!((Var_VariableReadNumFanoutTables(var) == 0))){
	  _IoEncodeWriteVariable(var, encFp, 0, encOutputsStTable, encInputsStTable);
	}
      }
    }
  }
  else{
    Hrc_NodeForEachFormalInput(hnode, i, var){
      _IoEncodeWriteVariable(var, encFp, 0, encOutputsStTable, encInputsStTable);
    }
    Hrc_NodeForEachChild(hnode, gen, childname, childnode){
      Hrc_NodeForEachActualOutput(childnode, i, var){
	_IoEncodeWriteVariable(var, encFp, 0, encOutputsStTable, encInputsStTable);
      }
    }
  }
}

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

  Synopsis	[ Writes out binary->mv  decoding tables  for relevant variables]

  Description	[ ]

  SideEffects	[ ]

  SeeAlso	[  ]
************************************************************************/
void
IoEncWriteBinToMvTables(
  Hrc_Node_t *hnode, 
  FILE *encFp, 
  st_table *encOutputsStTable, 
  st_table *encInputsStTable,
  int combinationalOnly,
  int makeLatchIOsPOs
  )
{
  int i;
  Var_Variable_t *var;
  st_generator *gen;
  char *childname;
  Hrc_Node_t *childnode;

  /* latch IOs encoding tables not handled here */
  /* if a PO or SI is driven by a latch, then in the combinational case, this
     var is not encoded (since the (mv) latch will be reinstated after
     sis optimization. In case of "wl -l" the same applies, since we are sure
     to be able to reinstate teh mv latch after sis optimization. However, in "wl" 
     every PI and SO is encoded since we are not sure  that mv latches can be 
     reinstated after sis optimization. Similarly, if teh PO or SI is a PI/SO  
     then no encoding is needed in all cases (comb or non-comb)
  */
  /*  if(combinationalOnly || makeLatchIOsPOs){ */
  /* The above line was changed since "wl -l" now writes out latches such that
     they drive a buffer node. As a result, even if a PO or SI is driven by the 
     latch, the PO/SI needs bin-mv tables 
  */
  if(combinationalOnly){ 
    Hrc_NodeForEachFormalOutput(hnode, i, var){
      if(!((Var_VariableTestIsSO(var) || Var_VariableTestIsPI(var) ||
	    Var_VariableTestIsPS(var)))){
	_IoEncodeWriteVariable(var, encFp, 1, encOutputsStTable, encInputsStTable);
      }
    }
    Hrc_NodeForEachChild(hnode, gen, childname, childnode){
      Hrc_NodeForEachActualInput(childnode, i, var){
	if(!((Var_VariableTestIsSO(var) || Var_VariableTestIsPI(var) ||
	      Var_VariableTestIsPS(var)))){
	  _IoEncodeWriteVariable(var, encFp, 1, encOutputsStTable, encInputsStTable);
	}
      }
    }
  }
  else{
    Hrc_NodeForEachFormalOutput(hnode, i, var){
      if(!((Var_VariableTestIsSO(var) || Var_VariableTestIsPI(var)))){
        _IoEncodeWriteVariable(var, encFp, 1, encOutputsStTable, encInputsStTable);
      }
    }
    Hrc_NodeForEachChild(hnode, gen, childname, childnode){
      Hrc_NodeForEachActualInput(childnode, i, var){
        if(!((Var_VariableTestIsSO(var) || Var_VariableTestIsPI(var)))){
          _IoEncodeWriteVariable(var, encFp, 1, encOutputsStTable, encInputsStTable);
        }
      }
    }
  }
}

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

  Synopsis	[ Writes out .input line for blif file]

  Description	[ ]

  SideEffects	[ ]

  SeeAlso	[  ]
************************************************************************/
 int
IoBlifWriteInputs(
  Hrc_Node_t *hnode, 
  FILE *fp, 
  st_table *blifInputsStTable,
  int combinationalOnly,
  int makeLatchIOsPOs
  )
{
  int i, j, k, numVal, numEncBits, numInputsWritten;
  Tbl_Table_t *table;
  st_generator *gen;
  Var_Variable_t *var;
  char *name, *dupName, *varName;
  boolean test;
  
  numInputsWritten = 0;
  fprintf(fp,".inputs ");     
  Hrc_NodeForEachNameTable(hnode, i, table){
    Tbl_TableForEachInputVar(table, k, var){
      if(combinationalOnly){
	test = Var_VariableTestIsPS(var) || Var_VariableTestIsSO(var) || Var_VariableTestIsPI(var);
      }
      else{
	test = Var_VariableTestIsSO(var) || Var_VariableTestIsPI(var);
      }
      if(test){
	name = Var_VariableReadName(var);
	numVal = Var_VariableReadNumValues(var);
	numEncBits = IoNumEncBits(numVal);
	for(j=0; j<numEncBits; j++){
	  dupName = ALLOC(char, strlen(name) + IoNumDigits(numEncBits) + 2);
	  sprintf(dupName, "%s%d", name, j);
	  if(!st_is_member(blifInputsStTable, (char *)dupName)){
	    fprintf(fp,"%s ",dupName);
	    numInputsWritten++;
	    st_insert(blifInputsStTable, (char *)dupName, (char *)1);
	  }
	  else{
	    FREE(dupName);
	  }
	}
      }
    }
  }
  if(!combinationalOnly){
    Hrc_NodeForEachVariable(hnode, gen, varName, var){
      if(Var_VariableTestIsPI(var)){
	name = Var_VariableReadName(var);
	numVal = Var_VariableReadNumValues(var);
	numEncBits = IoNumEncBits(numVal);
	for(j=0; j<numEncBits; j++){
	  dupName = ALLOC(char, strlen(name) + IoNumDigits(numEncBits) + 2);
	  sprintf(dupName, "%s%d", name, j);
	  if(!st_is_member(blifInputsStTable, (char *)dupName)){
	    fprintf(fp,"%s ",dupName);
	    numInputsWritten++;
	    st_insert(blifInputsStTable, (char *)dupName, (char *)1);
	  }
	  else{
	    FREE(dupName);
	  }
	}
      }
    }
  }
  return numInputsWritten;
}


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

  Synopsis	[ Writes out .output line for blif file]

  Description	[ ]

  SideEffects	[ ]

  SeeAlso	[  ]
************************************************************************/
 int
IoBlifWriteOutputs(
  Hrc_Node_t *hnode, 
  FILE *fp,
  st_table *blifOutputsStTable,
  int combinationalOnly,
  int makeLatchIOsPOs
  )
{
  int i, j, k, numVal, numEncBits, numOutputsWritten;
  Tbl_Table_t *table;
  st_generator *gen;
  Var_Variable_t *var;
  char *name, *dupName, *varName;
  boolean test;

  numOutputsWritten = 0;
  fprintf(fp,"\n.outputs "); 
  Hrc_NodeForEachNameTable(hnode, i, table){
    Tbl_TableForEachOutputVar(table, k, var){
      if(combinationalOnly){
	test = Var_VariableTestIsNS(var) || Var_VariableTestIsSI(var) || Var_VariableTestIsPO(var);
      }
      else{
	test = Var_VariableTestIsSI(var) || Var_VariableTestIsPO(var);
      }
      if(test){
	name = Var_VariableReadName(var);
	numVal = Var_VariableReadNumValues(var);
	numEncBits = IoNumEncBits(numVal);
	for(j=0; j<numEncBits; j++){
	  dupName = ALLOC(char, strlen(name) + IoNumDigits(numEncBits) + 2);
	  sprintf(dupName, "%s%d", name, j);
	  if(!st_is_member(blifOutputsStTable, (char *)dupName)){
	    fprintf(fp,"%s ",dupName);
	    numOutputsWritten++;
	    st_insert(blifOutputsStTable, (char *)dupName, (char *)1);
	  }
          else{
	    FREE(dupName);
	  }
	}
      }
    }
  }
  if(!combinationalOnly){
    Hrc_NodeForEachVariable(hnode, gen, varName, var){
      if(Var_VariableTestIsPO(var) && Var_VariableTestIsPS(var)){
	name = Var_VariableReadName(var);
	numVal = Var_VariableReadNumValues(var);
	numEncBits = IoNumEncBits(numVal);
	for(j=0; j<numEncBits; j++){
	  dupName = ALLOC(char, strlen(name) + IoNumDigits(numEncBits) + 2);
	  sprintf(dupName, "%s%d", name, j);
	  if(!st_is_member(blifOutputsStTable, (char *)dupName)){
	    fprintf(fp,"%s ",dupName);
	    numOutputsWritten++;
	    st_insert(blifOutputsStTable, (char *)dupName, (char *)1);
	  }
	  else{
	    FREE(dupName);
	  }
	}
      }
    }
  }
  fprintf(fp,"\n");
  return numOutputsWritten;
}

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

  Synopsis    [Writes out latches to the blif file]

  Description [ ] 

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
IoWriteLatches(
   Hrc_Node_t *hnode,
   FILE *fp,	      
   FILE *encFp,
   st_table *printedMvsStTable,	       
   st_table *blifOutputsStTable,	       
   st_table *blifInputsStTable,
   st_table *encOutputsStTable,	       
   st_table *encInputsStTable,
   int combinationalOnly,
   int makeLatchIOsPOs,
   int verbosity
   )
{
  Hrc_Latch_t *latch;
  st_generator *gen;
  char *varName, *latchName, *inputVarName, *outputVarName;
  char *latchInName, *latchOutName, *dupName;
  Var_Variable_t *outputVar, *inputVar, *var;
  Tbl_Table_t *resetTable;
  boolean test;
  int i, j, index, tempResetValue, resetValue, numEncBits, numVal;
  st_table *encodedResetVarsStTable;

    mdd_manager *mddMgr;
    Ntk_Node_t *ntkLatch, *ntkCombInput, *latchResetNtkNode;
    Ntk_Network_t *network;
    st_table *tableOfLeaves;
    array_t *singletonArrayOfRoots, *singletonMvfArray;
    Mvf_Function_t *mvf;
    lsGen listGen;
    Hrc_Manager_t *HrcMgr;

  /* stuff for doing reset table constantness check. Needs to do a "flt -b", "ord"
     and create a leaves table for mvf computation later.
  */
  mddMgr = mdd_init_empty();
  bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT,BDD_REORDER_VERBOSITY_DEFAULT);

  HrcMgr = Hrc_NodeReadManager(hnode);
  Hrc_ManagerSetCurrentNode(HrcMgr, hnode);
  
  network = Ntk_HrcNodeConvertToNetwork(hnode, TRUE, (lsList) NULL);
  Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, Ord_NodesByDefault_c, 0, Ord_InputAndLatch_c, Ord_Unassigned_c, (lsList) NULL, 0);
  tableOfLeaves = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachCombInput(network, listGen, ntkCombInput) {
    st_insert(tableOfLeaves, (char *)ntkCombInput, (char *) (long) (-1) );
  }

  encodedResetVarsStTable = st_init_table(strcmp, st_strhash);
  Hrc_NodeForEachLatch(hnode, gen, latchName, latch){
    inputVar = Hrc_LatchReadInput(latch);
    outputVar = Hrc_LatchReadOutput(latch);
    inputVarName = Var_VariableReadName(inputVar);
    outputVarName = Var_VariableReadName(outputVar);
    resetTable = Hrc_LatchReadResetTable(latch);
    
    IoMvCheckPrint(encFp,inputVar,printedMvsStTable);
    /* if makeLatchIOsPOs, then the .mv statement should have "_bufin" appended to the 
       variable names */
    if(makeLatchIOsPOs){
      IoMvCheckPrintSpecial(encFp,outputVar,printedMvsStTable);
    }
    else{
      IoMvCheckPrint(encFp,outputVar,printedMvsStTable);
    }
	  
    
    /* Write bin2mv table for input var if needed */
    /* if makeLatchIOsPOs, then the test for writing the bin2mv table should not include 
       a check to see if the var is a PS. This was previously required, since in hte case
       where a latchOutput drove a latchInput, we wanted to reinstate both mv latches after
       read_blif, and so didnt need any enc/dec tables. However, if makeLatchIOsPOs, then we
       will insert a buffer after latches, so enc/dec tables _will_ be needed. 
    */
    if(makeLatchIOsPOs){
      if(!IoVarIsHnodePIO(hnode, inputVar)){
	if(!st_is_member(encodedResetVarsStTable, (char *)Var_VariableReadName(inputVar))){
	  _IoEncodeWriteVariable(inputVar, encFp, 1, encOutputsStTable, encInputsStTable);
	  st_insert(encodedResetVarsStTable, (char *)Var_VariableReadName(inputVar), (char *)1);
	}
      }
    }
    else{      
      if(!IoVarIsHnodePIO(hnode, inputVar) && !Var_VariableTestIsPS(inputVar)){
	if(!st_is_member(encodedResetVarsStTable, (char *)Var_VariableReadName(inputVar))){
	  _IoEncodeWriteVariable(inputVar, encFp, 1, encOutputsStTable, encInputsStTable);
	  st_insert(encodedResetVarsStTable, (char *)Var_VariableReadName(inputVar), (char *)1);
	}
      }
    }
    
    /* Write mv2bin table for output var if needed */
    /* if makeLatchIOsPOs, then the enc tables should have "_bufin" appended to the 
       names. This is a hack, and I dont insert this name in the table since it does
       not correspond to a real name in the hrc node.
    */
    if(makeLatchIOsPOs){
      _IoEncodeWriteVariableSpecial(outputVar, encFp, 0, encOutputsStTable, encInputsStTable);  
    }
    else{      
      if(!(Var_VariableReadNumFanoutTables(outputVar) == 0)){
	if(!st_is_member(encodedResetVarsStTable, (char *)Var_VariableReadName(outputVar))){
	  _IoEncodeWriteVariable(outputVar, encFp, 0, encOutputsStTable, encInputsStTable);    
	  st_insert(encodedResetVarsStTable, (char *)Var_VariableReadName(outputVar), (char *)1);
	}
      }
    }
    /* Write latch IOs as POs if the "-l" option was used */
    if(makeLatchIOsPOs){
      /* 
	 first deal with inputVar - check if it has been printed to 
	 blif file in binary form, by looking up blifInputsStTable
      */
      numVal = Var_VariableReadNumValues(inputVar);
      numEncBits = IoNumEncBits(numVal);
      for(j=0; j<numEncBits; j++){
	dupName = ALLOC(char, strlen(inputVarName) + IoNumDigits(numEncBits) + 2);
	sprintf(dupName, "%s%d", inputVarName, j);
	if(!st_is_member(blifInputsStTable, (char *)dupName)){
	  fprintf(fp,".outputs %s\n",dupName);
	  st_insert(blifInputsStTable, (char *)dupName, (char *)1);
	}
	else{
	  FREE(dupName);
	}
      }
      /* 
	 next deal with outputVar - check if it has been printed to 
	 blif file in binary form, by looking up blifOutputsStTable
      */
      numVal = Var_VariableReadNumValues(outputVar);
      numEncBits = IoNumEncBits(numVal);
      for(j=0; j<numEncBits; j++){
	dupName = ALLOC(char, strlen(outputVarName) + IoNumDigits(numEncBits) + 2);
	sprintf(dupName, "%s%d", outputVarName, j);
	if(!st_is_member(blifOutputsStTable, (char *)dupName)){
	  fprintf(fp,".outputs %s\n",dupName);
	  st_insert(blifOutputsStTable, (char *)dupName, (char *)1);
	}
	else{
	  FREE(dupName);
	}
      }
    }

    /* handle reset tables (all cases "wl -c", "wl -l", and "wl")*/
    Tbl_TableForEachInputVar(resetTable, index, var){
      if(!IoVarIsHnodePIO(hnode, var)){
	IoMvCheckPrint(encFp, var,printedMvsStTable);
      }
      /* dont encode if (comb&ps) or (makeLatchIOsPOs&ps) */
      /*      if(!((combinationalOnly || makeLatchIOsPOs) && Var_VariableTestIsPS(var))){ */
      /* since we insert a buffer after each latch whenever makeLatchIOsPOs, there will
	 be a need for a bin2mv table for the latch output var. Previously, it was assumed
	 that when the mv latch will replace the bin latches, there will be no need for a
	 bin2mv table since the mv latch was directly driving the reset table.
      */
      if(!(combinationalOnly && Var_VariableTestIsPS(var))){ 
	/* if var is a PI or SO, then mv->bin tables exist for it, so dont 
	   make bin->mv tables since the mv variable will exist anyway 
        */
	if(!Var_VariableTestIsPI(var) && !Var_VariableTestIsSO(var)){
	  if(!st_is_member(encodedResetVarsStTable, (char *)Var_VariableReadName(var))){
	    _IoEncodeWriteVariable(var, encFp, 1, encOutputsStTable, encInputsStTable);
	    st_insert(encodedResetVarsStTable, (char *)Var_VariableReadName(var), (char *)1);
	  }
	}
      }
      /*
         if we are doing "wl -c" and there is a resetTable input var
	 which is also a PS which does not have fanout tbls, then this 
	 variable will not be encoded and listed in the blif file.
	 Hence such a variable should not be encoded and listed in teh 
         blif file as a PO, since it will have no driving tables.
      */
      if(!(combinationalOnly && Var_VariableTestIsPS(var) && 
	 (Var_VariableReadNumFanoutTables(var) == 0))){
	/* 
	   write encoded vars as outputs after checking that they havent 
	   already been written as outputs or inputs to the blif file
        */
	varName = Var_VariableReadName(var);
	numVal = Var_VariableReadNumValues(var);
	numEncBits = IoNumEncBits(numVal);
	for(j=0; j<numEncBits; j++){
	  dupName = ALLOC(char, strlen(varName) + IoNumDigits(numEncBits) + 2);
	  sprintf(dupName, "%s%d", varName, j);
	  if(!st_is_member(blifInputsStTable, (char *)dupName) && !st_is_member(blifOutputsStTable, (char *)dupName)){
	    fprintf(fp,".outputs %s\n",dupName);
	    st_insert(blifOutputsStTable, (char *)dupName, (char *)1);
	  }
	  else{
	    FREE(dupName);
	  }
	}
      }
    }
  }

  /* write latch stmts to blif file */
  Hrc_NodeForEachLatch(hnode, gen, latchName, latch){
    inputVar = Hrc_LatchReadInput(latch);
    outputVar = Hrc_LatchReadOutput(latch);
    inputVarName = Var_VariableReadName(inputVar);
    outputVarName = Var_VariableReadName(outputVar);
    resetTable = Hrc_LatchReadResetTable(latch);
    /* write out mv latches to enc file, they are needed even if we are 
       writing only combinational part of the network */
    /* if makeLatchIOsPOs, then append "_bufin" to the output name, since latch 
       outputs are buffered. Also, reset table should reflect this new name.
    */
    if(makeLatchIOsPOs){
      (void)fprintf(encFp, ".latch %s %s_bufin \n", inputVarName, outputVarName);	    
      Tbl_TableWriteBlifMvToFileSpecial(resetTable, 1, encFp);
    }
    else{
      (void)fprintf(encFp, ".latch %s %s \n", inputVarName, outputVarName);	    
      Tbl_TableWriteBlifMvToFile(resetTable, 1, encFp);
    }      
    
    /* determine value of reset table - whether const, or not */
    if(!combinationalOnly){      
      ntkLatch = Ntk_NetworkFindNodeByName(network, latchName);
      assert(Ntk_NodeTestIsLatch(ntkLatch));
      latchResetNtkNode = Ntk_LatchReadInitialInput(ntkLatch);
      singletonArrayOfRoots = array_alloc(Ntk_Node_t *, 0);
      array_insert_last(Ntk_Node_t *, singletonArrayOfRoots, latchResetNtkNode);
      singletonMvfArray = Ntm_NetworkBuildMvfs(network, singletonArrayOfRoots, tableOfLeaves, NIL(mdd_t));
      mvf = array_fetch(Mvf_Function_t *, singletonMvfArray, 0);
      array_free(singletonMvfArray);
      array_free(singletonArrayOfRoots);
      test = Mvf_FunctionTestIsConstant(mvf, &resetValue);
      Mvf_FunctionFree(mvf);
      if(verbosity > 1){
	(void)fprintf(stdout, "Reset table is: \n");                
	Tbl_TableWriteBlifMvToFile(resetTable, 0, stdout);
      }
      if(verbosity > 0){
	(void)fprintf(stdout, "Reset table constantness test result was %d\n", test);          
      }
      if(test == FALSE){
	resetValue = VIS_INFINITY;
      }
      if(verbosity > 0){
	fprintf(stdout, "Reset value %d\n", resetValue);
      }
      
      /* write latches to blif file */
      numEncBits = IoNumEncBits(Var_VariableReadNumValues(inputVar));
      if(resetValue == VIS_INFINITY){
	for(i = 0; i < numEncBits; i++){
	  resetValue = 2;
	  latchInName = ALLOC(char, strlen(inputVarName) + IoNumDigits(numEncBits) + 2);
	  latchOutName = ALLOC(char, strlen(outputVarName) + IoNumDigits(numEncBits) + 10); 
	  sprintf(latchInName, "%s%d", inputVarName, i);
	  /* if makelatchIOsPOs, then latch drives buffer input, and buffer needs to be 
             be written to the blif file too
          */
	  if(makeLatchIOsPOs){
	    sprintf(latchOutName, "%s_bufin%d", outputVarName, i);
	  }
	  else{
	    sprintf(latchOutName, "%s%d", outputVarName, i);
	  }
	  (void)fprintf(fp, ".latch %s %s %d\n", latchInName, latchOutName, resetValue);
	  if(makeLatchIOsPOs){
	    (void)fprintf(fp, ".names %s %s%d\n", latchOutName, outputVarName, i);
	    (void)fprintf(fp, "1 1\n");
	  }
	  FREE(latchInName);
	  FREE(latchOutName);
	}
      }
      else{
	tempResetValue = resetValue;
	for(i = numEncBits - 1; i >= 0; i--){
	  if(((int)(tempResetValue / pow((double) 2, (double) i))) == 1){
	    resetValue = 1;
	    tempResetValue = tempResetValue - (int)pow((double)2,(double)i);	    
	  }
	  else{
	    resetValue = 0;
	  }
	  latchInName = ALLOC(char, strlen(inputVarName) + IoNumDigits(numEncBits) + 2);
	  latchOutName = ALLOC(char, strlen(outputVarName) + IoNumDigits(numEncBits) + 10); 
	  sprintf(latchInName, "%s%d", inputVarName, i);
	  /* if makelatchIOsPOs, then latch drives buffer input, and buffer needs to be 
             be written to the blif file too.
          */
	  if(makeLatchIOsPOs){
	    sprintf(latchOutName, "%s_bufin%d", outputVarName, i);
	  }
	  else{
	    sprintf(latchOutName, "%s%d", outputVarName, i);
	  }	    
	  (void)fprintf(fp, ".latch %s %s %d\n", latchInName, latchOutName, resetValue);
	  if(makeLatchIOsPOs){
	    (void)fprintf(fp, ".names %s %s%d\n", latchOutName, outputVarName, i);
	    (void)fprintf(fp, "1 1\n");
	  }
	  FREE(latchInName);
	  FREE(latchOutName);
	}
      }
    }
  }
  st_free_table(encodedResetVarsStTable);
  st_free_table(tableOfLeaves);
  Ntk_NetworkFree(network);
  mdd_quit(mddMgr);
}


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

  Synopsis    [Prints the .mv declaration of a variable, to file, if it is not in the 
               st_table variables already printed]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
IoMvCheckPrint(
   FILE *fp, 
   Var_Variable_t *var,
   st_table *printedMvsStTable
  )
{
    char *varname, *tmpName;

    tmpName = Var_VariableReadName(var);
    varname = ALLOC(char, strlen(tmpName) + 2);
    sprintf(varname, "%s", tmpName);
    if(!st_is_member(printedMvsStTable, (char *)varname)){
	st_insert(printedMvsStTable, (char *)varname, (char *)1);
	IoMvPrint(fp, var);
    }
    else{
        FREE(varname);
    }
}

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

  Synopsis    [Prints the .mv declaration of a variable, to file, if it is not in the 
               st_table variables already printed. Appends a special string "_bufin"
	       at the end of the name.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
IoMvCheckPrintSpecial(
   FILE *fp, 
   Var_Variable_t *var,
   st_table *printedMvsStTable
  )
{
    char *varname, *tmpName;

    tmpName = Var_VariableReadName(var);
    varname = ALLOC(char, strlen(tmpName) + 10);
    sprintf(varname, "%s_bufin", tmpName);
    if(!st_is_member(printedMvsStTable, (char *)varname)){
	st_insert(printedMvsStTable, (char *)varname, (char *)1);
	IoMvPrintSpecial(fp, var);
    }
    else{
        FREE(varname);
    }
}

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

  Synopsis    [Writes a blifmv value, in expanded form, into binTable]

  Description [Writes the binary value corresponding to "value" in the binTable
               starting from the rootRow, rootCol entry. The values are repeated
	       "entryRepetitionCount" times]

  SideEffects []

  SeeAlso     []

******************************************************************************/
 int
IoWriteExpandedValueToBinTable( 
   Tbl_Table_t *binTable,
   int rootRow,
   int rootCol,
   IoBinRangeEntry_t *binRangeEntry,
   int entryRepetitionCount,
   int numBits,
   int output
   )
{
    int i, j, row, value, numDash, end;
    Tbl_Entry_t *entry;

    numDash = IoLog(binRangeEntry->runLength);
    end = IoLog(binRangeEntry->skipLength);
    value = binRangeEntry->startValue;
    for(j = numBits - 1; j >= 0; j--){
      row = rootRow;
	if((j < end) || (j >= numDash + end)){
	    if(((int)(value / pow((double) 2, (double) j))) == 1){
		for(i = 0; i < entryRepetitionCount; i++){
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 1, 1);
		    Tbl_TableSetEntry(binTable, entry, row++, rootCol+j, output);
		}
		value -= (int)pow((double)2,(double)j);
	    }
	    else{
		for(i = 0; i < entryRepetitionCount; i++){
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 0, 0);
		    Tbl_TableSetEntry(binTable, entry, row++, rootCol+j, output);
		}
	    }
	}
	else{
	    for(i = 0; i < entryRepetitionCount; i++){
		entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		Tbl_EntrySetValue(entry, 0, 1);
		Tbl_TableSetEntry(binTable, entry, row++, rootCol+j, output);
	    }
	}
    }
    return 0;
}


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

  Synopsis    [Writes out tables in binTblArray to a named blif file]

  Description [Writes out binary tables in the binTblArray to 
               blif file pointed to by fp]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
IoWriteBinTablesToFile( 
   IoBlifInfo_t *blifInfo	       		      
   )
{
    int i, colnum, rownum, value, hasZeroRows;
    Tbl_Table_t *table;
    Var_Variable_t *outputVar, *dupOutputVar;
    char *outputVarName;
    Tbl_Entry_t *entry;
    Tbl_Range_t *range;
    lsGen gen;

    for(i = 0; i < array_n(blifInfo->binTblArray); i++){
	table = array_fetch(Tbl_Table_t *, blifInfo->binTblArray, i);
   /* if table has zero rows, print it as ".names <var>" */
	hasZeroRows = 1;
	Tbl_TableForEachOutputEntry(table, colnum, rownum, entry){
	    Tbl_EntryForEachValue(entry, value, gen, range){
		if(value == 1){
		    hasZeroRows = 0;
		}
	    }
	}
	if(hasZeroRows){
	    outputVar = Tbl_TableReadIndexVar(table, 0, 1);
	    table = Tbl_TableAlloc();
	    outputVarName = Var_VariableReadName(outputVar);
	    dupOutputVar = Var_VariableAlloc(NIL(Hrc_Node_t), outputVarName);
	    (void)Tbl_TableAddColumn(table, dupOutputVar, 1);
	    Tbl_TableWriteBlifToFile(table, blifInfo->BlifFp); 
	    Tbl_TableFree(table);
	    Var_VariableFree(dupOutputVar);
	}
	else{
	    Tbl_TableWriteBlifToFile(table, blifInfo->BlifFp); 
	}
    }
}


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


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

  Synopsis    [Encodes individual variable based on its ranges, and writes to the file called
               "encoding"]

  Description []

  SideEffects [Program state is not changed]

  SeeAlso     []

******************************************************************************/
static void
_IoEncodeWriteVariable(
   Var_Variable_t *var,
   FILE *encFp,		      
   int varIsOutput,
   st_table *encOutputsStTable, 
   st_table *encInputsStTable
   )
{
    int j, i, tempI, range, numEncBits, rownum, varIsInput;
    Tbl_Table_t *encTable;
    char *varname, *dupName;
    Var_Variable_t *encVar;
    Tbl_Entry_t *entry;
    array_t *varArray;

    if(varIsOutput == 1){
	varIsInput = 0;
    }
    else{
	varIsInput = 1;
    }

    if(varIsOutput){
	if(st_is_member(encOutputsStTable, (char *)var)){
	    return;
	}
	else{
	    st_insert(encOutputsStTable, (char *) var, (char *) 1);
	}
    }
    else{
	if(st_is_member(encInputsStTable, (char *)var)){
	    return;
	}
	else{
	    st_insert(encInputsStTable, (char *) var, (char *) 1);
	}
    }
	    

        /* declare encoding input vars based on range. These are associated
           with their encoding table. These have names <var>0, <var>1, ...  */

    varArray = array_alloc(Var_Variable_t *, 0);
    range = Var_VariableReadNumValues(var);
    numEncBits = IoNumEncBits(range);
    /* create encoding table */
    encTable = Tbl_TableAlloc();
    varname = Var_VariableReadName(var);
    for(i=0; i<numEncBits; i++){
	dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
	sprintf(dupName, "%s%d", varname, i);
	encVar = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
	FREE(dupName);
	array_insert_last(Var_Variable_t *, varArray, encVar);
	(void) Tbl_TableAddColumn(encTable, encVar, varIsInput);
    }

        /* declare output var for the encoding table. It is called <var>     */

    (void) Tbl_TableAddColumn(encTable, var, varIsOutput);
    
        /* fill in entries of the variable encoding table. Assign codes based on 
           the variable's index. Nothing fancy here...                        */

    for(i=0; i<range; i++){    
	tempI = i;
 	rownum = Tbl_TableAddRow(encTable);
	for(j = numEncBits - 1; j >= 0; j--){
	    if(((int)(tempI / pow((double) 2, (double) j))) == 1){
		entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		Tbl_EntrySetValue(entry, 1, 1);
		Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
		tempI = tempI - (int)pow((double)2,(double)j);
	    }
	    else{
		entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		Tbl_EntrySetValue(entry, 0, 0);
		Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
	    }
	}
	entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
	Tbl_EntrySetValue(entry, i, i);
	Tbl_TableSetEntry(encTable, entry, rownum, 0, varIsOutput);
    }
    /* make sure not inc specced if var is output */
    if(varIsOutput){
	for(i = range; i < ((int) pow((double)2, (double)numEncBits)); i++){
	    tempI = i;
	    rownum = Tbl_TableAddRow(encTable);
	    for(j = numEncBits - 1; j >= 0; j--){
		if(((int)(tempI / pow((double) 2, (double) j))) == 1){
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 1, 1);
		    Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
		    tempI = tempI - (int)pow((double)2,(double)j);
		}
		else{
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 0, 0);
		    Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
		}
	    }
	    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
	    Tbl_EntrySetValue(entry, 0, 0);
	    Tbl_TableSetEntry(encTable, entry, rownum, 0, varIsOutput);
	}
    }
    
    
    /* store the var, var number, and its table in the encTblArray. */
    
    Tbl_TableWriteBlifMvToFile(encTable, 0, encFp);
    Tbl_TableFree(encTable);

    for(i=0; i < array_n(varArray); i++){
	Var_VariableFree(array_fetch(Var_Variable_t *, varArray, i));
    }
    array_free(varArray);

}



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

  Synopsis    [Encodes individual variable based on its ranges. Variable name has
               the string "_bufin" appended to it.]

  Description []

  SideEffects [Program state is not changed]

  SeeAlso     []

******************************************************************************/
static void
_IoEncodeWriteVariableSpecial(
   Var_Variable_t *var,
   FILE *encFp,		      
   int varIsOutput,
   st_table *encOutputsStTable, 
   st_table *encInputsStTable
   )
{
    int j, i, tempI, range, numEncBits, rownum, varIsInput;
    Tbl_Table_t *encTable;
    char *varname, *dupName;
    Var_Variable_t *encVar, *outVar;
    Tbl_Entry_t *entry;
    array_t *varArray, *symValArray;

    if(varIsOutput == 1){
	varIsInput = 0;
    }
    else{
	varIsInput = 1;
    }

    if(varIsOutput){
	if(st_is_member(encOutputsStTable, (char *)var)){
	    return;
	}
	else{
	    st_insert(encOutputsStTable, (char *) var, (char *) 1);
	}
    }
    else{
	if(st_is_member(encInputsStTable, (char *)var)){
	    return;
	}
	else{
	    st_insert(encInputsStTable, (char *) var, (char *) 1);
	}
    }
	    

        /* declare encoding input vars based on range. These are associated
           with their encoding table. These have names <var>0, <var>1, ...  */

    varArray = array_alloc(Var_Variable_t *, 0);
    range = Var_VariableReadNumValues(var);
    numEncBits = IoNumEncBits(range);
    /* create encoding table */
    encTable = Tbl_TableAlloc();
    varname = Var_VariableReadName(var);
    for(i=0; i<numEncBits; i++){
	dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 10);
	sprintf(dupName, "%s_bufin%d", varname, i);
	encVar = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
	FREE(dupName);
	array_insert_last(Var_Variable_t *, varArray, encVar);
	(void) Tbl_TableAddColumn(encTable, encVar, varIsInput);
    }

        /* declare output var for the encoding table. It is called <var>_bufin     */

    varname = Var_VariableReadName(var);
    dupName = ALLOC(char, strlen(varname) + 10);    
    sprintf(dupName, "%s_bufin", varname);
    outVar = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
    array_insert_last(Var_Variable_t *, varArray, outVar);
    FREE(dupName);
    if(Var_VariableTestIsSymbolic(var)){
      symValArray = array_alloc(char *, 0);
      for(i = 0; i < range; i++){
	array_insert_last(char *, symValArray, Var_VariableReadSymbolicValueFromIndex(var, i));
      }
      Var_VariableAddRangeInfo(outVar, range, symValArray);
      array_free(symValArray);
    }
    else{
      if(range > 2){
	Var_VariableExpandRange(outVar, range);
      }
    }
    (void) Tbl_TableAddColumn(encTable, outVar, varIsOutput);


        /* fill in entries of the variable encoding table. Assign codes based on 
           the variable's index. Nothing fancy here...                        */

    for(i=0; i<range; i++){    
	tempI = i;
 	rownum = Tbl_TableAddRow(encTable);
	for(j = numEncBits - 1; j >= 0; j--){
	    if(((int)(tempI / pow((double) 2, (double) j))) == 1){
		entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		Tbl_EntrySetValue(entry, 1, 1);
		Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
		tempI = tempI - (int)pow((double)2,(double)j);
	    }
	    else{
		entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		Tbl_EntrySetValue(entry, 0, 0);
		Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
	    }
	}
	entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
	Tbl_EntrySetValue(entry, i, i);
	Tbl_TableSetEntry(encTable, entry, rownum, 0, varIsOutput);
    }
    /* make sure not inc specced if var is output */
    if(varIsOutput){
	for(i = range; i < ((int) pow((double)2, (double)numEncBits)); i++){
	    tempI = i;
	    rownum = Tbl_TableAddRow(encTable);
	    for(j = numEncBits - 1; j >= 0; j--){
		if(((int)(tempI / pow((double) 2, (double) j))) == 1){
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 1, 1);
		    Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
		    tempI = tempI - (int)pow((double)2,(double)j);
		}
		else{
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 0, 0);
		    Tbl_TableSetEntry(encTable, entry, rownum, j, varIsInput);
		}
	    }
	    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
	    Tbl_EntrySetValue(entry, 0, 0);
	    Tbl_TableSetEntry(encTable, entry, rownum, 0, varIsOutput);
	}
    }
    
    
    /* store the var, var number, and its table in the encTblArray. */
    
    Tbl_TableWriteBlifMvToFile(encTable, 0, encFp);
    Tbl_TableFree(encTable);

    for(i=0; i < array_n(varArray); i++){
	Var_VariableFree(array_fetch(Var_Variable_t *, varArray, i));
    }
    array_free(varArray);

}