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

  FileName    [ ioWriteBlif.c ] 

  PackageName [ io ]

  Synopsis    [ This file contains blifmv -> blif write routines ]

  Description [ Routines for (determinizing, encoding and) writing a blifmv table
                into a blif description are provided. The encoding of multivalued 
                vars is written to separate files. ]

  SeeAlso     [ ioReadBlifmv.c, ioWriteBlifIo.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: ioWriteBlif.c,v 1.14 2005/04/29 14:23:29 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define MAX_NUMBER_BDD_VARS 500

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



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

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

static int _IoTableWriteBlif(Io_Encoding_Type_t encodingType, Hrc_Node_t *hnode, Tbl_Table_t *origBlifmvTable, st_table *blifInputsStTable, FILE *fp, FILE *encFp, int verbosity);
static int _IoMakeInitialEncodings(IoBlifInfo_t *blifInfo, Hrc_Node_t *hnode);
static void _IoDeterminizeEncodeOutputPart(IoBlifInfo_t *blifInfo, st_table *blifInputsStTable);
static void _IoDeterminizeEncodeRows(IoBlifInfo_t *blifInfo, st_table *blifInputsStTable);
static void _IoMakeDcTables(IoBlifInfo_t *blifInfo);
static void _IoMakeBinTable(IoBlifInfo_t *blifInfo);
static int _IoCheckHnodeTreeIsBooleanAndDeterministic(mdd_manager **mddMgr, Hrc_Node_t *hnode, st_table *modelTable, boolean *pSymVarsPresent, int verbosity);
static int _IoCheckHnodeVarsAreBoolean(Hrc_Node_t *hnode, boolean *pSymVarsPresent);
static int _IoCheckHnodeLatchResetIsConstant(Hrc_Node_t *hnode);
static int _IoCheckHnodeTablesAreDeterministic(mdd_manager **mddMgr, Hrc_Node_t *hnode);
static void _MddManagerResetIfNecessary(mdd_manager **mddMgr);
static void _IoHnodeWriteBlifRecursively(Io_Encoding_Type_t encodingType, Hrc_Node_t *hnode, st_table *modelTable, FILE *fp, FILE *encFp, int verbosity);
static int _IoHnodeWriteBlifRecursivelyStep(Io_Encoding_Type_t encodingType, Hrc_Node_t *hnode, FILE *fp, FILE *encFp, int verbosity);
static int _IoCheckHnodeIsBooleanAndDeterministic(mdd_manager **mddMgr, Hrc_Node_t *hnode, boolean *pSymVarsPresent);
static int _IoCheckPseudoinputIsPO(Tbl_Table_t *table);

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


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

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


  Synopsis	[ Recursively write out the entire hierarchy below the current 
                  hnode to a blif file. ]

  Description	[ This routine recursively writes out the entire hierarchy below
                  the given hnode to a named blif file. This sub-hierarchy must 
                  comply with the following restrictions. First all tables in it
                  should be deterministic. Secondly, all variables should be 
                  binary. The function returns a 0 upon success, 1 in case of 
                  failure. Upon failure, appropriate error messages are printed 
                  to stderr. The function is passed an enumerated type called 
                  encodingType, only SIMPLE is supported. Refer to the description 
                  of Io_HnodeWriteBlif for more information on this. The hnode 
                  is passed, along with the file pointer fp, for the file into which 
                  the resulting blif network is to be written. A verbosity flag 
                  (valid values are between 0 and 2) causes intermediate information 
		  to be printed to stderr.
		  ]

  SideEffects	[ ]

  SeeAlso	[  ]
**********************************************************************/
int
Io_HnodeWriteBlifTotal(
    Io_Encoding_Type_t encodingType,
    Hrc_Node_t *hnode, 
    FILE *fp, 
    int verbosity)
{
  st_table *modelTable;
  Hrc_Manager_t *manager;
  mdd_manager *mddMgr;
  FILE *encFp;
  boolean symVarsPresent;
  
  manager = Hrc_NodeReadManager(hnode);
  modelTable = st_init_table(st_ptrcmp, st_ptrhash);
  mddMgr = mdd_init_empty();
  bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
  symVarsPresent = FALSE;

  /* check that the node and all its children are boolean and deterministic. */
  if(_IoCheckHnodeTreeIsBooleanAndDeterministic(&mddMgr, hnode, modelTable, &symVarsPresent, verbosity)){
    mdd_quit(mddMgr);
    st_free_table(modelTable);
    return 1;
  }
  if(verbosity > 0){
    fprintf(vis_stderr, "Done with hierarcy checks\n");
  }
  
  if(symVarsPresent == TRUE){
    fprintf(vis_stderr, "Warning - some variables in the hierarchy are symbolic\n");
  }
  
  st_free_table(modelTable);
  modelTable = st_init_table(st_ptrcmp, st_ptrhash);  
  encFp = Cmd_FileOpen("/dev/null", "w", NIL(char *), 1);

  _IoHnodeWriteBlifRecursively(encodingType, hnode, modelTable, fp, encFp, verbosity);
  Hrc_ManagerSetCurrentNode(manager, hnode);

  st_free_table(modelTable);
  mdd_quit(mddMgr);
  return 0;
}
    

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


  Synopsis	[ Determinize, encode and write all blifmv tables in a hnode 
                  to a blif file. Also writes all encoding information to a 
		  encoding file. This encoding file can later be read in, along 
		  with the blif file (potentially after optimization in SIS), 
		  into that hnode (see "read_blif -i" for details).  Currently, only the 
		  combinational part of the hnode is written to the blif file.]

  Description	[ This routine determinizes, encodes and writes all blifmv tables
                  in a hnode to a named blif file.
		  It also writes encoding information to another named file.
		  This encoding file must be used while reading back the (optimized) 
		  blif file into blifmv. 
		  The function returns a 0 upon success, 1 in case of failure. It 
		  should be supplied a Io_Encoding_Type_t. Currently only SIMPLE is 
		  supported. Under this scheme, binary encoding is done on the 
		  multi-valued variables, and the binary variable with smallest length
		  is chosen at any step of the  determinization process. Other parameters 
		  to this function  include a Hrc_Node_t *, and file pointers for the 
		  blif output file and the encoding file. The default blif file is 
		  stdout, and the default encoding file is <model>.enc. A verbosity flag 
		  (valid values are between 0 and 2) print intermediate information to 
		  stdout.
		  ]

  SideEffects	[ ]

  SeeAlso	[  ]
  **********************************************************************/
int
Io_HnodeWriteBlif(
    Io_Encoding_Type_t encodingType,
    Hrc_Node_t *hnode,
    FILE *fp,
    FILE *encFp,
    int verbosity,
    int combinationalOnly,
    int makeLatchIOsPOs)
{
    Tbl_Table_t *table, *singleOutputTable;
    Tbl_Entry_t *entry;
    int i, j, k, numVal, numInputs, numOutputs;
    Var_Variable_t *var, *actualVar, *outputVar;
    char *name, *instanceName, *modelName, *newModelName;
    st_generator *gen;
    st_table *blifInputsStTable, *blifOutputsStTable, *printedMvsStTable;
    st_table *encOutputsStTable, *encInputsStTable;
    Hrc_Node_t *subcktHnode;
    Hrc_Model_t *model, *subcktModel;
    Hrc_Subckt_t *subckt;
    Hrc_Manager_t *manager;
    array_t *subcktActualInputVars, *subcktActualOutputVars;
   

    Hrc_NodeForEachNameTable(hnode, i, table){
      if(_IoCheckPseudoinputIsPO(table)){
	fprintf(stdout, "Hnode contains a pseudoinput which is also a primary output - quitting\n");
	return 1;
      }
      for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
	entry = Tbl_TableDefaultReadEntry(table, j);
	if(entry != NIL(Tbl_Entry_t)){
	  if(Tbl_EntryReadType(entry) == Tbl_EntryNormal_c){
	    if(Tbl_EntryReadNumValues(entry) > 1){
	      outputVar = Tbl_TableReadIndexVar(table, j, 1);
	      (void)fprintf(stdout, "The table with %s as an output has non-singleton default values - quitting\n", Var_VariableReadName(outputVar));
	      return 1;
	    }
	  }
	  else{
	    var = Tbl_EntryReadVar(table, entry);
	    k = Tbl_TableReadVarIndex(table, var, 1);
	    if(k<0){
	      outputVar = Tbl_TableReadIndexVar(table, j, 1);	      
	      (void)fprintf(stdout, "Output %s has a default value that refers to an input variable - quitting\n", Var_VariableReadName(outputVar));
	      return 1;
	    }
	  }
	}
      }
    }

    printedMvsStTable = st_init_table(strcmp, st_strhash);

    if(!(combinationalOnly || makeLatchIOsPOs)){
      fprintf(encFp,"# This encoding file and the blif file that was written out with it cannot\n");           
      fprintf(encFp,"# currently be read back into VIS. If you would like to read the blif and\n");           
      fprintf(encFp,"# encoding files back into VIS, then use the 'write_blif -l' or\n");
      fprintf(encFp,"#'write_blif -c' options.\n");
    }

  /* .model */
    modelName = Hrc_NodeReadModelName(hnode);
    manager = Hrc_NodeReadManager(hnode);
    model = Hrc_ManagerFindModelByName(manager, modelName);
    newModelName = ALLOC(char, strlen(modelName) + 256);
    i = 0;
    sprintf(newModelName, "%s[%d]", modelName, i);

    while(Hrc_ManagerFindModelByName(manager, newModelName) != NIL(Hrc_Model_t)){
	i++;
	sprintf(newModelName, "%s[%d]", modelName, i);
    }
    (void)fprintf(encFp,".model %s\n",newModelName);
    FREE(newModelName);
    /* .inputs line of enc file*/
    if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
	(void)fprintf(encFp,".inputs ");
	Hrc_NodeForEachFormalInput(hnode,i,var){
	    (void)fprintf(encFp,"%s ",Var_VariableReadName(var));
	}
	(void)fprintf(encFp,"\n");
    }
    
    /* .outputs line of enc file*/
    if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
	(void)fprintf(encFp,".outputs ");
	Hrc_NodeForEachFormalOutput(hnode,i,var){
	    (void)fprintf(encFp,"%s ",Var_VariableReadName(var));
	}
	(void)fprintf(encFp,"\n");
    }
    
    /* .mv for primary inputs, printed to enc file*/
    Hrc_NodeForEachFormalInput(hnode,i,var){
	IoMvCheckPrint(encFp,var,printedMvsStTable);
    }
    /* .mv for primary outputs, printed to enc file*/
    Hrc_NodeForEachFormalOutput(hnode,i,var){
	IoMvCheckPrint(encFp,var,printedMvsStTable);
    }
    
    /* .subckt stuff */
    Hrc_ModelForEachSubckt(model,gen,instanceName,subckt){
	subcktModel = Hrc_SubcktReadModel(subckt);
	subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
	subcktActualInputVars = Hrc_SubcktReadActualInputVars(subckt);
	subcktActualOutputVars = Hrc_SubcktReadActualOutputVars(subckt);
	
	/* .mv for subckt inputs */
	for (i=0; i < array_n(subcktActualInputVars); i++){
	    var = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
	    IoMvCheckPrint(encFp,var,printedMvsStTable);
	}

	/* .mv for subckt outputs */
	for (i=0; i < array_n(subcktActualOutputVars); i++){
	    var = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
	    IoMvCheckPrint(encFp,var,printedMvsStTable);
	}

	/* .subckt declarations */
	(void)fprintf(encFp,".subckt %s %s ",
		      Hrc_ModelReadName(subcktModel), Hrc_SubcktReadInstanceName(subckt));
	Hrc_NodeForEachFormalInput(subcktHnode,i,var){
	    actualVar = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
	    (void)fprintf(encFp,"%s = %s ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
	}   
	Hrc_NodeForEachFormalOutput(subcktHnode,i,var){
	    actualVar = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
	    (void)fprintf(encFp,"%s = %s ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
	}   
	(void)fprintf(encFp,"\n");
    }

    encOutputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
    encInputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
    blifInputsStTable = st_init_table(strcmp, st_strhash);
    blifOutputsStTable = st_init_table(strcmp, st_strhash);

    /* encoding tables to .enc file */
    IoEncWriteMvToBinTables(hnode, encFp, encOutputsStTable, encInputsStTable, combinationalOnly);

    /* decoding tables to .enc file */
    IoEncWriteBinToMvTables(hnode, encFp, encOutputsStTable, encInputsStTable, combinationalOnly, makeLatchIOsPOs);

    /* if write_blif called without -c or -l options, then print a warning saying
       that the files cant be read back into vis..
    */
    if(!(combinationalOnly || makeLatchIOsPOs)){
      fprintf(fp,"# This blif file and the encoding file that was written out with it cannot\n");           
      fprintf(fp,"# currently be read back into VIS. If you would like to read the blif and\n");           
      fprintf(fp,"# encoding files back into VIS, then use the 'write_blif -l' or\n");
      fprintf(fp,"#'write_blif -c' options.\n");
    }
    
    /* .inputs declarations for blif file */
    fprintf(fp,".model %s\n",modelName );     
    numInputs = IoBlifWriteInputs(hnode, fp, blifInputsStTable, combinationalOnly, makeLatchIOsPOs);

    /* .outputs declarations for blif file */
    numOutputs = IoBlifWriteOutputs(hnode, fp, blifOutputsStTable, combinationalOnly, makeLatchIOsPOs);

    if((numInputs == 0) && (numOutputs != 0)){
      fprintf(vis_stderr, "Warning: Blif file has zero inputs\n");
    }
    if((numOutputs == 0) && (numInputs != 0)){
      fprintf(vis_stderr, "Warning: Blif file has zero outputs\n");
    }
    if((numInputs == 0) && (numOutputs == 0)){
      fprintf(vis_stderr, "Warning: Blif file has zero inputs and zero outputs\n");
    }

    /* .latch declarations for blif file */
    IoWriteLatches(hnode, fp, encFp, printedMvsStTable, blifOutputsStTable, blifInputsStTable, encOutputsStTable, encInputsStTable, combinationalOnly, makeLatchIOsPOs, verbosity);
    Hrc_NodeForEachNameTable(hnode, i, table){
	if((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1)){
	    (void)fprintf(stdout, "Warning: ");
	    Tbl_TableForEachOutputVar(table, j, var){
		(void)fprintf(stdout, "%s, ", Var_VariableReadName(var));
	    }
	    (void)fprintf(stdout, "assumed to be pseudoinputs\n");
	    Tbl_TableForEachOutputVar(table, j, var){
		singleOutputTable = Tbl_TableAlloc();
		Tbl_TableAddColumn(singleOutputTable, var, 1);
	        (void) Tbl_TableAddRow(singleOutputTable);
		entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		numVal = Var_VariableReadNumValues(var);
		Tbl_EntrySetValue(entry, 0, numVal - 1);
		Tbl_TableSetEntry(singleOutputTable, entry, 0, 0, 1);
		_IoTableWriteBlif(encodingType, hnode, singleOutputTable, blifInputsStTable, fp, encFp,
				  verbosity);
		Tbl_TableFree(singleOutputTable);
	    }
	}
	else{
	  if(IoOutputExpansionRequired(table)){
	    if(verbosity > 0){
	      (void)fprintf(stdout, "Splitting into Single Output Table before Processing\n");
	    }
	    for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
	      singleOutputTable = IoMakeSingleOutputTable(table, j);
	      _IoTableWriteBlif(encodingType, hnode, singleOutputTable, blifInputsStTable, fp, encFp,
				verbosity);
	      Tbl_TableFree(singleOutputTable);
	    }
	  }
	  else{
	    if(!((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1))){
	      _IoTableWriteBlif(encodingType, hnode, table, blifInputsStTable, fp, encFp,
				verbosity);
	    }
	  }
	}
    }
    st_foreach_item_int(blifInputsStTable, gen, &name, &i){
	FREE(name);
    }
    st_free_table(blifInputsStTable);
    st_foreach_item_int(blifOutputsStTable, gen, &name, &i){
	FREE(name);
    }
    st_free_table(blifOutputsStTable);
    st_free_table(encInputsStTable);
    st_free_table(encOutputsStTable);
    st_foreach_item_int(printedMvsStTable, gen, &name, &i){
	FREE(name);
    }
    st_free_table(printedMvsStTable);
    /* printing an empty .exdc network keeps sis from sweeping away the
       dummy buffers that latch outputs are made to drive as a result of the 
       "write_blif -l" cmd. The dummy buffers were added because if they were 
       not present, sis would introduce buffers whenever latch outputs drive POs
       directly (in the "xdc" command), ruining the name correspondence required 
       for read_blif to work and reinstate mv latches.
    */
    fprintf(fp,".exdc\n");
    fprintf(fp,".end\n");
    if(encFp != stdout){
      (void) fclose(encFp);
    }
    return 0;
}


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

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


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


  Synopsis	[ Determinize, encode and write a blifmv table to blif file ]

  Description	[ Note that this routine cannot handle the "=" construct of 
                  blifmv. It is my opinion that a front-end routine should be
                  used to remove the "="'s. ]

  SideEffects	[ ]

  SeeAlso	[  ]
  **********************************************************************/
static int
_IoTableWriteBlif(
    Io_Encoding_Type_t encodingType,
    Hrc_Node_t *hnode,		 
    Tbl_Table_t *origBlifmvTable,
    st_table *blifInputsStTable,
    FILE *fp,
    FILE *encFp,
    int verbosity )
{
    IoBlifInfo_t *blifInfo;

    blifInfo = ALLOC(IoBlifInfo_t, 1);
    if(verbosity > 1){
	(void)fprintf(stdout, "Original Blifmv Table :\n");
	Tbl_TableWriteBlifMvToFile(origBlifmvTable, 0, stdout);
    }
    IoInitBlifInfo(blifInfo, origBlifmvTable, fp, encFp, verbosity);
    if(encodingType == SIMPLE){
	if(_IoMakeInitialEncodings(blifInfo, hnode)){
	    blifInfo->binTblArray = array_alloc(Tbl_Table_t *, 0);
	    IoFreeBlifInfo(blifInfo);
	    return 0;
	}
	_IoDeterminizeEncodeOutputPart(blifInfo, blifInputsStTable);
	_IoMakeBinTable(blifInfo);
	if(blifInfo->verbosity > 0){
	    (void)fprintf(stdout, "Done with Output Singletonization\n");
	}
	if(blifInfo->verbosity > 1){
	    (void)fprintf(stdout, "Final Blifmv Table After Output Singletonization:\n");
	    Tbl_TableWriteBlifMvToFile(blifInfo->blifmvTable, 0, stdout);    
	    (void)fprintf(stdout, "Bin Table After Output Singletonization:\n");
	    Tbl_TableWriteBlifMvToFile(blifInfo->binTable, 0, stdout);    
	}
	_IoDeterminizeEncodeRows(blifInfo, blifInputsStTable);     
	if(blifInfo->verbosity > 0){
	    (void)fprintf(stdout, "Done with Row Intersection and Determinization\n");
	}
	if(blifInfo->verbosity > 1){
	    (void)fprintf(stdout, "Final Bin Table After Determinization \n");
	    Tbl_TableWriteBlifMvToFile(blifInfo->binTable, 0, stdout);    
	}
	_IoMakeDcTables(blifInfo);
	blifInfo->binTblArray = Tbl_TableSplit(blifInfo->binTable);
	IoWriteBinTablesToFile(blifInfo);
	IoFreeBlifInfo(blifInfo);
	return 0;
    }
    else{
	(void)fprintf(vis_stderr, "This encoding strategy has not been implemented yet\n");
	return 1;
    }
}
  

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

  Synopsis    [Encodes variables based on their ranges]

  Description [Returns encodings in the form of an array of tables for each
               multivalued variable. ] 

  SideEffects [Populates the array of tables describing the encoding]

  SeeAlso     []

******************************************************************************/
static int
_IoMakeInitialEncodings(
   IoBlifInfo_t *blifInfo,
   Hrc_Node_t *hnode		       
   )
{
    Var_Variable_t *var, *origVar;
    int i, colnum, numRows, numValues, varRange, value, numEncBits;
    char *name, *varname, *dupName;
    Tbl_Entry_t *entry, *newEntry, *defEntry, *newDefEntry;
    lsGen gen;
    Tbl_Range_t *range;
    Tbl_Table_t *table, *origTable;

    if(Tbl_TableReadNumInputs(blifInfo->blifmvTable) == 0){
	value = -1;
	if(Tbl_TableReadNumRows(blifInfo->blifmvTable) != 0){
	  entry = Tbl_TableReadEntry(blifInfo->blifmvTable, 0, 0, 1);
	  numValues = Tbl_EntryReadNumValues(entry);
	}
	else{
	  entry = Tbl_TableDefaultReadEntry(blifInfo->blifmvTable, 0);
	  numValues = Tbl_EntryReadNumValues(entry);
	}
	origTable = Tbl_TableHardDup(blifInfo->blifmvTable);

	if(Tbl_TableReadNumRows(blifInfo->blifmvTable) <= 1){
	    if(numValues == 1){
	    /* not a pseudoinput */
		Tbl_EntryForEachValue(entry, value, gen, range);
		assert(value != -1);
		var = Tbl_TableReadIndexVar(blifInfo->blifmvTable, 0, 1);
		varRange = Var_VariableReadNumValues(var);
		numEncBits = IoNumEncBits(varRange);
		varname = Var_VariableReadName(var);
		for(i = numEncBits - 1; i >= 0; i--){
		    dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
		    sprintf(dupName, "%s%d", varname, i);
		    (void)fprintf(blifInfo->BlifFp, ".names %s\n", dupName);
		    FREE(dupName);
		    if(value > (int) pow((double) 2, (double) i)){
			(void)fprintf(blifInfo->BlifFp, "1\n");
			value -= (int) pow((double) 2, (double) i);
		    }
		    else{
			(void)fprintf(blifInfo->BlifFp, "0\n");
		    }
		}
		Tbl_TableFree(origTable);
		return 1;
	    }
	    else{
		/* is a pseudoinput! */
		/* make it look like a table with many rows, and singleton output entries per row */
		table = Tbl_TableAlloc();

		Tbl_TableForEachOutputVar(blifInfo->blifmvTable, i, var){
		    Tbl_TableAddColumn(table, var, 1);
		}
		Tbl_TableForEachDefaultEntry(blifInfo->blifmvTable, defEntry, i) {
		    if (defEntry != NIL(Tbl_Entry_t)) {
			newDefEntry = Tbl_EntryDup(defEntry);
		    }
		    else {
			newDefEntry = NIL(Tbl_Entry_t);
		    }
		    (void) Tbl_TableDefaultSetEntry(table, newDefEntry, i);
		}
		Tbl_EntryForEachValue(entry, value, gen, range){
		    i = Tbl_TableAddRow(table);
		    newEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(newEntry, value, value);
		    Tbl_TableSetEntry(table, newEntry, i, 0, 1);
		}
		Tbl_TableFree(blifInfo->blifmvTable);
		blifInfo->blifmvTable = table;
	    }
	}
	/* it is a pseudoinput, and has been singletonized wrt outputs */
	if(Tbl_TableReadNumRows(blifInfo->blifmvTable) > 1){
	    name = ALLOC(char, 256);
	    i = 0;
	    sprintf(name, "[%d]", i);
	    while(!(Hrc_NodeFindVariableByName(hnode, name) == NULL)){	
		i++;
		sprintf(name, "[%d]", i);
	    }
	    
	    blifInfo->pseudoinputFlag = TRUE;
	    var = Var_VariableAlloc(hnode, name);
	    Tbl_TableAddColumn(blifInfo->blifmvTable, var, 0);
	    (void)fprintf(blifInfo->BlifFp, ".inputs %s0\n", name);
	    origVar = Tbl_TableReadIndexVar(origTable, 0, 1);
	    IoMvPrint(blifInfo->EncFp, origVar);
	    Tbl_TableWriteBlifMvToFile(origTable, 0, blifInfo->EncFp);    
	    Tbl_TableFree(origTable);
	    numRows = Tbl_TableReadNumRows(blifInfo->blifmvTable);
	    for(i = 0; i < numRows; i++){
		if(i % 2 == 1){
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 1, 1);
		    Tbl_TableSetEntry(blifInfo->blifmvTable, entry, i, 0, 0);
		}
		else{
		    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
		    Tbl_EntrySetValue(entry, 0, 0);
		    Tbl_TableSetEntry(blifInfo->blifmvTable, entry, i, 0, 0);
		}
	    }
	    FREE(name);
	}
    }

    Tbl_TableForEachInputVar(blifInfo->blifmvTable, colnum, var){
	IoEncodeVariable(blifInfo, var, colnum, 0);
    }

    Tbl_TableForEachOutputVar(blifInfo->blifmvTable, colnum, var){
	IoEncodeVariable(blifInfo, var, colnum, 1);
    }
    return 0;
}


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

  Synopsis    [Encodes variables to make singleton output values in every row]

  Description [Returns modified table along with a modified array of tables for 
               encoding the multivalued variables. If the original table
               has singleton output values then it is returned unmodified, 
	       with the unmodified variable encoding tables.]

  SideEffects [Potentially modifies the array of tables describing the encoding]

  SeeAlso     []

******************************************************************************/
static void
_IoDeterminizeEncodeOutputPart( 
   IoBlifInfo_t *blifInfo,
   st_table *blifInputsStTable
   )
{
    Tbl_Entry_t *entry;
    int numValues, i, j, numRows, numOutputs;
    IoVarEncEntry_t *varEnc;
    array_t *MvOutputArray;

    numRows = Tbl_TableReadNumRows(blifInfo->blifmvTable);
    numOutputs = Tbl_TableReadNumOutputs(blifInfo->blifmvTable);
    for(i = 0; i < numRows; i++){
	MvOutputArray = array_alloc(int, 0);
    	numValues = 1;
	for(j = 0; j < numOutputs; j++){
	    entry = Tbl_TableReadEntry(blifInfo->blifmvTable, i, j, 1);
	    numValues *= Tbl_EntryReadNumValues(entry);
	    array_insert_last(int, MvOutputArray, Tbl_EntryReadNumValues(entry));
	}
	if(numValues > 1){
	    varEnc = IoFindSmallestCode(blifInfo);
	    if(blifInfo->verbosity > 2){
		(void)fprintf(stdout, "Singletonizing Outputs in Row %d\n", i);
		(void)fprintf(stdout, "Best Variable is %s\n", Var_VariableReadName(varEnc->variable));
	    }
	    IoIncreaseCodeSize(varEnc, numValues, blifInfo->verbosity);
	    IoChangeBlifmvTableEntries(blifInfo, i, numValues, varEnc, MvOutputArray);
	    IoChangeEncTableEntries(blifInfo, blifInputsStTable, varEnc, numValues);
	    i = -1;
	    array_free(MvOutputArray);
	    
	    if(blifInfo->verbosity > 2){
		(void)fprintf(stdout, "Blifmv Table After Output Singletonization\n");
		Tbl_TableWriteBlifMvToFile(blifInfo->blifmvTable, 0, stdout);    
	    }
	}
	else{
	    array_free(MvOutputArray);
	}
    }
}


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

  Synopsis    [Encodes variables to make table deterministic]

  Description [Returns modified table along with a modified array of tables for 
               encoding the multivalued variables. If the original table
               is deterministic, then it is returned unmodified, 
	       with the unmodified variable encoding tables.]

  SideEffects [Potentially modifies the array of tables describing the encoding]

  SeeAlso     []

******************************************************************************/
static void
_IoDeterminizeEncodeRows( 
   IoBlifInfo_t *blifInfo,
   st_table *blifInputsStTable
   )
{
    int i, j, k, numRows, numOutputs, numInputs, mvValue;
    boolean rowsIntersect;
    IoVarEncEntry_t *varEnc;
    char *pseudoInputName, *realPseudoInputName;
    Var_Variable_t *outvar, *var, *origVar;
    Tbl_Entry_t *entry;
    
    
    numRows = Tbl_TableReadNumRows(blifInfo->binTable);
    for(i = 0; i < numRows; i++){
	for(j = i + 1; j < numRows; j++){	
	    if(blifInfo->verbosity > 2){
		(void)fprintf(stdout, "Intersecting Rows %d and %d \n", i, j);
	    }
	    rowsIntersect = Tbl_RowInputIntersect(blifInfo->binTable, i, j); 
	    if(rowsIntersect == 1){  
		if(blifInfo->verbosity > 2){
		    (void)fprintf(stdout, "Input Intersection non-null\n");
		}
		if(!Tbl_RowOutputIntersect(blifInfo->binTable, i, j)){
		    varEnc = IoFindSmallestCode(blifInfo);
		    if(blifInfo->verbosity > 2){
			(void)fprintf(stdout, "Output Intersection null\n");
			(void)fprintf(stdout, "Best Variable is %s\n", Var_VariableReadName(varEnc->variable));

		    }
		    IoIncreaseCodeSize(varEnc, 2, blifInfo->verbosity); 
		    IoChangeBlifmvTableRows(blifInfo, varEnc, i, j);
		    IoChangeEncTableEntries(blifInfo, blifInputsStTable, varEnc, 2); 
		    
		    if(blifInfo->verbosity > 2){
			(void)fprintf(stdout, "Bin Table After Row Overlap elimination \n");
			Tbl_TableWriteBlifMvToFile(blifInfo->binTable, 0, stdout);    
		    }
		}
	    }
	}
    }
    if(blifInfo->pseudoinputFlag == TRUE){
	/* pseudoinput cant have .def construct */
	outvar = Tbl_TableReadIndexVar(blifInfo->binTable, 0, 1);
	pseudoInputName = Var_VariableReadName(outvar);
	realPseudoInputName = ALLOC(char, strlen(pseudoInputName) + 2);
	sprintf(realPseudoInputName, "%s", pseudoInputName);
	realPseudoInputName[strlen(pseudoInputName) - 1] = '\0';
	numOutputs = Tbl_TableReadNumOutputs(blifInfo->binTable);
	numInputs = Tbl_TableReadNumInputs(blifInfo->binTable);
	for(i = 0; i < numInputs; i++){
	    (void)fprintf(blifInfo->EncFp, ".table %s ->", realPseudoInputName);
	    var = Tbl_TableReadIndexVar(blifInfo->binTable, i, 0);
	    (void)fprintf(blifInfo->EncFp, "%s\n", Var_VariableReadName(var));		
	    (void)fprintf(blifInfo->EncFp, ".default 0\n");
	    for(j = 0; j < numRows; j++){
		mvValue = 0;
		for(k = 0; k < numOutputs; k++){
		    entry = Tbl_TableReadEntry(blifInfo->binTable, j, k, 1);
		    if(Tbl_EntryCheckRange(entry, 1, 1)){
			mvValue += (int) pow((double)2, (double) k);
		    }
		}
		origVar = Tbl_TableReadIndexVar(blifInfo->blifmvTable, 0, 1);
		if(Var_VariableTestIsSymbolic(origVar)){
		    (void)fprintf(blifInfo->EncFp, "%s ",
				  Var_VariableReadSymbolicValueFromIndex(origVar, mvValue));		    
		}
		else{
		    (void)fprintf(blifInfo->EncFp, "%d ", mvValue);
		}

		entry = Tbl_TableReadEntry(blifInfo->binTable, j, i, 0);
		if(Tbl_EntryCheckRange(entry, 1, 1)){
		    (void)fprintf(blifInfo->EncFp, "%d\n", 1);
		}
		else{ 
		    if(Tbl_EntryCheckRange(entry, 0, 0)){
			(void)fprintf(blifInfo->EncFp, "%d\n", 0);
		    }
		    else{
			(void)fprintf(blifInfo->EncFp, "-\n");
		    }
		}
	    }
	}
	FREE(realPseudoInputName);
    }
}


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

  Synopsis    [Creates Dont-Care Tables for Variable Encodings]

  Description [For each table in the blifInfo->inputEncTblArray, this
               function creates dont-care tables]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
_IoMakeDcTables( 
   IoBlifInfo_t *blifInfo
   )
{
}



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

  Synopsis    [Writes out blifmvTable to binTable in encoded form]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
_IoMakeBinTable( 
  IoBlifInfo_t *blifInfo
  )
{
    int i, j, k, m, n, colnum, numRowsAfterExpansion, numEncBits;
    int rootCol, rootRow, entryRepetitionCount, numCycles, value, numBits, currRow;
    int numOutputs, numRows, numInputs, defValue, varRange;
    Tbl_Entry_t *entry, *workingEntry;
    array_t *binRangesArray, *mvEntryBinRanges;
    IoVarEncEntry_t *varEnc;
    char *varname, *dupName;
    Var_Variable_t *var;
    lsGen gen, gen2;
    Tbl_Range_t *range, *range2;
    IoBinRangeEntry_t *binRangeEntry;
    
    
    /* initialize the binTable, defining input vars etc   */
    
    numRows = Tbl_TableReadNumRows(blifInfo->blifmvTable);
    numInputs = Tbl_TableReadNumInputs(blifInfo->blifmvTable);
    numOutputs = Tbl_TableReadNumOutputs(blifInfo->blifmvTable);
    for(j = 0; j < Tbl_TableReadNumInputs(blifInfo->blifmvTable); j++){
	varEnc = array_fetch(IoVarEncEntry_t *, blifInfo->inputEncTblArray, j);
	numEncBits = varEnc->numEncBits;
	for(k = 0; k < numEncBits ; k++){
	    varname = Var_VariableReadName(varEnc->variable);
	    dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
	    sprintf(dupName, "%s%d", varname, k);
	    var = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
	    FREE(dupName);
	    array_insert_last(Var_Variable_t *, blifInfo->varArray, var);
	    colnum = Tbl_TableAddColumn(blifInfo->binTable, var, 0);
	}
    }
    
    for(j = 0; j < Tbl_TableReadNumOutputs(blifInfo->blifmvTable); j++){
	varEnc = array_fetch(IoVarEncEntry_t *, blifInfo->outputEncTblArray, j);
	numEncBits = varEnc->numEncBits;
	for(k = 0; k < numEncBits ; k++){
	    varname = Var_VariableReadName(varEnc->variable);
	    dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
	    sprintf(dupName, "%s%d", varname, k);
	    var = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
	    FREE(dupName);
	    array_insert_last(Var_Variable_t *, blifInfo->varArray, var);
	    colnum = Tbl_TableAddColumn(blifInfo->binTable, var, 1);
	}
    }
    
    
/*
    fprintf(stdout, "\n");    
*/
    for(i = 0; i < numRows; i++){
	
	/* make temp array of number of values for each input var  */
	numRowsAfterExpansion = 1;
	binRangesArray = array_alloc(array_t *, 0);
	
	for(colnum = 0; colnum < numInputs; colnum++){
	    entry = Tbl_TableReadEntry(blifInfo->blifmvTable, i, colnum, 0);
	    workingEntry = Tbl_EntryDup(entry);
	    mvEntryBinRanges = IoMakeBinaryRangesArray(workingEntry, colnum, blifInfo);
	    numRowsAfterExpansion *= array_n(mvEntryBinRanges);
	    array_insert_last(array_t *, binRangesArray, mvEntryBinRanges); 
	}

/*
	for(j = 0; j < array_n(binRangesArray); j++){
	    mvEntryBinRanges = array_fetch(array_t *, binRangesArray, j);
	    for(k = 0; k < array_n(mvEntryBinRanges); k++){
		binRangeEntry = array_fetch(IoBinRangeEntry_t *, mvEntryBinRanges, k);
		fprintf(stdout, "start %d\t runlen%d\t skip %d\n", binRangeEntry->startValue, binRangeEntry->runLength, binRangeEntry->skipLength);
	    }
	    (void)fprintf(stdout, "\n");
	}
	fprintf(stdout, "numRowsAfterExpansion %d\n", numRowsAfterExpansion);

*/
	/* add numRowsAfterExpansion rows to binTable */
	
	rootCol = 0;
	rootRow = Tbl_TableReadNumRows(blifInfo->binTable);
	for(j = 0; j < numRowsAfterExpansion; j++){
	    Tbl_TableAddRow(blifInfo->binTable);
	}

	/* write out binary encoded variable values for the determinized, encoded blifmvTable
	   (input parts) */

	entryRepetitionCount = numRowsAfterExpansion;
	m = 0;
	numCycles = 1;

	for(colnum = 0; colnum < numInputs; colnum++){
	    mvEntryBinRanges = array_fetch(array_t *, binRangesArray, colnum);
	    currRow = rootRow;
	    rootCol += IoNumBinVars(colnum, blifInfo->inputEncTblArray);
	    entryRepetitionCount = entryRepetitionCount / array_n(array_fetch(array_t *, binRangesArray, m));
	    numCycles *= IoNumValuesFromBinRangesArray(colnum, binRangesArray);
	    numBits = IoNumBinVars(colnum + 1, blifInfo->inputEncTblArray);
	    for(k=0; k<numCycles; k++){
		for(n = 0; n < array_n(mvEntryBinRanges); n++){
		    binRangeEntry = array_fetch(IoBinRangeEntry_t *, mvEntryBinRanges, n);
		    IoWriteExpandedValueToBinTable(blifInfo->binTable, currRow, rootCol, binRangeEntry, entryRepetitionCount, numBits, 0);
		    currRow = currRow + entryRepetitionCount;
		}
	    }
	    m++;
	}

	/* write out binary encoded variable values for the determinized, encoded blifmvTable
	   (output parts) */

	rootCol = 0;

	for(colnum = 0; colnum < numOutputs; colnum++){
	    entry = Tbl_TableReadEntry(blifInfo->blifmvTable, i, colnum, 1);
	    rootCol += IoNumBinVars(colnum, blifInfo->outputEncTblArray);
	    numBits = IoNumBinVars(colnum + 1, blifInfo->outputEncTblArray);
	    Tbl_EntryForEachValue(entry, value, gen, range){
		binRangeEntry = ALLOC(IoBinRangeEntry_t, 1);
		binRangeEntry->startValue = value;
		binRangeEntry->runLength = 1;
		binRangeEntry->skipLength = 1;
		IoWriteExpandedValueToBinTable(blifInfo->binTable, rootRow, rootCol, binRangeEntry, numRowsAfterExpansion, numBits, 1);
		FREE(binRangeEntry);
	    }
	}
	for(j = 0; j < array_n(binRangesArray); j++){
	    mvEntryBinRanges = array_fetch(array_t *, binRangesArray, j);
	    for(n = 0; n < array_n(mvEntryBinRanges); n++){
		binRangeEntry = array_fetch(IoBinRangeEntry_t *, mvEntryBinRanges, n);
		FREE(binRangeEntry);
	    }
	    array_free(mvEntryBinRanges);
	}
	array_free(binRangesArray);
    }
    
    rootCol = 0;
    Tbl_TableForEachOutputVar(blifInfo->blifmvTable, colnum, var){
	entry = Tbl_TableDefaultReadEntry(blifInfo->blifmvTable, colnum);
	if(entry != NIL(Tbl_Entry_t)){
	    varRange = Var_VariableReadNumValues(var);
	    numEncBits = IoNumEncBits(varRange);
	    defValue = -1;
	    Tbl_EntryForEachValue(entry, value, gen2, range2){
		defValue = value;
		assert(defValue != -1);
	    }
	    for(j = numEncBits - 1; j >= 0; j--){
		if(((int)(defValue / pow((double) 2, (double) j))) == 1){
		    IoInvertBinTableOutput(blifInfo, rootCol + j);
		    defValue = defValue - (int)pow((double)2,(double)j);
		}
	    }
	    rootCol += numEncBits;
	}
    }
}


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

  Synopsis    [Checks that all hnodes rooted at the give hnode are boolean and 
               deterministic]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_IoCheckHnodeTreeIsBooleanAndDeterministic(
  mdd_manager **mddMgr,				       
  Hrc_Node_t *hnode, 
  st_table *modelTable,
  boolean *pSymVarsPresent,
  int verbosity
  )
{
  char *modelName, *childName;
  Hrc_Model_t *model;
  st_generator *stGen;
  Hrc_Manager_t *manager;  
  Hrc_Node_t *childNode;

  manager = Hrc_NodeReadManager(hnode);
  /* enter current model in modelTable */
  modelName = Hrc_NodeReadModelName(hnode);
  model = Hrc_ManagerFindModelByName(manager, modelName);
  if(st_is_member(modelTable, (char *) model)){
    return 0;
  }
  else{
    st_insert(modelTable, (char *)model, (char *) (long) (-1));
  }
  
  if(_IoCheckHnodeIsBooleanAndDeterministic(mddMgr, hnode, pSymVarsPresent)){
    if(verbosity > 1){
      fprintf(vis_stderr, "Model %s is NOT boolean and deterministic\n", modelName);
    }
    return 1;
  }
  if(verbosity > 1){
    fprintf(vis_stderr, "Model %s is boolean and deterministic\n", modelName);
  }
  Hrc_NodeForEachChild(hnode, stGen, childName, childNode){
    if(_IoCheckHnodeTreeIsBooleanAndDeterministic(mddMgr, childNode, modelTable, pSymVarsPresent, verbosity)){
      st_free_gen(stGen);
      return 1;
    }
  }
  return 0;
}


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

  Synopsis    [Checks that the given hnode is boolean and deterministic]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_IoCheckHnodeIsBooleanAndDeterministic(
  mdd_manager **mddMgr,				       
  Hrc_Node_t *hnode,
  boolean *pSymVarsPresent
  )
{
  
  /* check that variables of all models are boolean */
  if(_IoCheckHnodeVarsAreBoolean(hnode, pSymVarsPresent)){
    return 1;
  }

  /* check that latch resets of all models are either 0/1/2 */
  if(_IoCheckHnodeLatchResetIsConstant(hnode)){
    return 1;
  }

  /* check that tables of all models are deterministic */
  if(_IoCheckHnodeTablesAreDeterministic(mddMgr, hnode)){
    return 1;
  }

  return 0;
}

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

  Synopsis    [Checks that the variables of a model are boolean]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_IoCheckHnodeVarsAreBoolean(
  Hrc_Node_t *hnode,
  boolean *pSymVarsPresent
  )
{
  st_generator *stGen;
  char *varName;
  Var_Variable_t *var;
  
  Hrc_NodeForEachVariable(hnode, stGen, varName, var){
    if(Var_VariableReadNumValues(var) > 2){
      fprintf(vis_stderr, "Variable %s is not boolean - quitting.\n", varName);      
      st_free_gen(stGen);
      return 1;
    }
    if(Var_VariableTestIsSymbolic(var)){
      *pSymVarsPresent = TRUE;
    }
  }
  return 0;
}


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

  Synopsis    [Checks that the latches of a model have constant reset tables]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_IoCheckHnodeLatchResetIsConstant(
  Hrc_Node_t *hnode 
  )
{
  st_generator *stGen;
  char *latchName;
  Hrc_Latch_t *latch;
  boolean test;
  Tbl_Table_t *table, *resetTable;
  Tbl_Entry_t *entry;
  Var_Variable_t *var, *parentVar;
  int i, j;

  Hrc_NodeForEachLatch(hnode, stGen, latchName, latch){
    resetTable = Hrc_LatchReadResetTable(latch);
    test = Tbl_TableTestIsConstant(resetTable, 0);
    /*
      Tbl_TableTestIsConstant gives 0 result for reset tables of
      the type .reset a ->b; - =a; where a is a constant defined 
      in another table. So check for this case as well. 
      */
    if(test == FALSE){
      if(Tbl_TableReadNumRows(resetTable) == 1){
	entry = Tbl_TableReadEntry(resetTable, 0, 0, 1);
	if(Tbl_EntryReadType(entry) == Tbl_EntryEqual_c){
	  parentVar = Tbl_EntryReadVar(resetTable, entry);
	  Hrc_NodeForEachNameTable(hnode, i, table){
	    Tbl_TableForEachOutputVar(table, j, var){
	      if(var == parentVar){
		test = Tbl_TableTestIsConstant(table, j);
	      }
	    }
	  }
	}
      }
    }
    if (test == FALSE){
      fprintf(vis_stderr, "Latch %s has a non-constant reset value - quitting.\n", latchName);
      st_free_gen(stGen);
      return 1;
    }
  }
  return 0;
}

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

  Synopsis    [Checks that all tables in a model are deterministic]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_IoCheckHnodeTablesAreDeterministic(
  mdd_manager **mddMgr,				    
  Hrc_Node_t *hnode 
  )
{
  int i, j, k, index, colNum, offset, numInputs;
  Tbl_Table_t *table;
  Var_Variable_t *inputVar, *outputVar, *var;
  Mvf_Function_t *faninMvf, *outMvf;
  array_t *faninMvfArray;
  array_t *mvarValues;
  Tbl_Entry_t *entry;


  /* note that reset tables are not handled here */
  Hrc_NodeForEachNameTable(hnode, i, table){
    Tbl_TableForEachOutputVar(table, index, outputVar){

      faninMvfArray = array_alloc(Mvf_Function_t *, 0);
      mvarValues = array_alloc(int, 0);
      
      /* Create MDD variables for the table inputs. */
      Tbl_TableForEachInputVar(table, colNum, inputVar) {
	array_insert_last(int, mvarValues, Var_VariableReadNumValues(inputVar));
      }
      offset = array_n(mdd_ret_mvar_list(*mddMgr));  /* number of existing mvars */
      mdd_create_variables(*mddMgr, mvarValues, NIL(array_t), NIL(array_t));
      array_free(mvarValues);
      
      /*
       * Construct an MVF for each table input. The MVF for column j is the MVF
       * for MDD variable j.
       */
      
      numInputs = Tbl_TableReadNumInputs(table );
      for (j = 0; j < numInputs; j++) {
	faninMvf = Mvf_FunctionCreateFromVariable(*mddMgr, (j + offset));
	array_insert_last(Mvf_Function_t *, faninMvfArray, faninMvf);
      }
      
      /* Compute the MVF of the output indexed by index. */
      outMvf = Tbl_TableBuildMvfFromFanins(table, index, faninMvfArray, *mddMgr);
      Mvf_FunctionArrayFree(faninMvfArray);
      
      /*
       * If the function is a non-deterministic constant, or it has some
       * inputs, and is non-deterministic, then fail
       */
      if((numInputs > 0) && !Mvf_FunctionTestIsDeterministic(outMvf)){
	(void) fprintf(vis_stderr, "Table %s is non-deterministic - quitting\n", Var_VariableReadName(outputVar));
	Mvf_FunctionFree(outMvf);
	return 1;
      }
      if(Mvf_FunctionTestIsNonDeterministicConstant(outMvf)){
	(void) fprintf(vis_stderr, "Table %s is a non-deterministic constant - quitting\n", Var_VariableReadName(outputVar));
	Mvf_FunctionFree(outMvf);
	return 1;
      }
      if (!Mvf_FunctionTestIsCompletelySpecified(outMvf)) {
	(void) fprintf(vis_stderr, "Table %s is not completely specified - quitting\n", Var_VariableReadName(outputVar));
	Mvf_FunctionFree(outMvf);
	return 1; 
      } 
      Mvf_FunctionFree(outMvf);
      _MddManagerResetIfNecessary(mddMgr);

    }
  }

  Hrc_NodeForEachNameTable(hnode, i, table){
    for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
      entry = Tbl_TableDefaultReadEntry(table, j);
      if(entry != NIL(Tbl_Entry_t)){
	if(Tbl_EntryReadType(entry) == Tbl_EntryNormal_c){
	  if(Tbl_EntryReadNumValues(entry) > 1){
	    outputVar = Tbl_TableReadIndexVar(table, j, 1);
	    (void)fprintf(stdout, "The table with %s as an output has non-singleton default values - quitting\n", Var_VariableReadName(outputVar));
	    return 1;
	  }
	}
	else{
	  var = Tbl_EntryReadVar(table, entry);
	  k = Tbl_TableReadVarIndex(table, var, 1);
	  if(k<0){
	    outputVar = Tbl_TableReadIndexVar(table, j, 1);
	    (void)fprintf(stdout, "Output %s has a default value that refers to an input variable - quitting\n", Var_VariableReadName(outputVar));
	    return 1;
	  }
	}
      }
    }
  }
  return 0;
}


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

  Synopsis    [Potentially quits mddMgr and starts a new one.]

  Description [Quits mddMgr if the number of binary variables exceeds
  MAX_NUMBER_BDD_VARS, and starts a new manager with no variables.
  Initializing an empty MDD manager is costly in some BDD packages, so we want
  to avoid doing it often (say, once per table).  On the other hand, we don't
  want the manager to have too many variables, because then reordering becomes
  expensive.]

  SideEffects []

******************************************************************************/
static void
_MddManagerResetIfNecessary(
  mdd_manager **mddMgr)
{
  if (bdd_num_vars(*mddMgr) > MAX_NUMBER_BDD_VARS) {
    mdd_quit(*mddMgr);
    *mddMgr = mdd_init_empty();
  }
}



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

  Synopsis    [Write out a Hnode and recurse on its children]

  Description [Call the function to write out the given hnode in blif, and 
  recursively call the same function on its children.]

  SideEffects []

******************************************************************************/
static void
_IoHnodeWriteBlifRecursively(
   Io_Encoding_Type_t encodingType,
   Hrc_Node_t *hnode,
   st_table *modelTable, 
   FILE *fp,
   FILE *encFp,
   int verbosity
  )
{
  char *modelName, *childName;
  Hrc_Model_t *model;
  Hrc_Manager_t *manager;  
  st_generator *stGen;
  Hrc_Node_t *childNode;

  manager = Hrc_NodeReadManager(hnode);
  /* enter current model in modelTable */
  modelName = Hrc_NodeReadModelName(hnode);
  model = Hrc_ManagerFindModelByName(manager, modelName);
  if(st_is_member(modelTable, (char *) model)){
    return;
  }
  else{
    st_insert(modelTable, (char *)model, (char *) (long) (-1));
  }

  _IoHnodeWriteBlifRecursivelyStep(encodingType, hnode, fp, encFp, verbosity);  
  Hrc_NodeForEachChild(hnode, stGen, childName, childNode){
    _IoHnodeWriteBlifRecursively(encodingType, childNode, modelTable, fp, encFp, verbosity);
  }
  return;
}


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


  Synopsis	[ Writes out an hnode to blif]

  Description	[ Writes out IO declarations, subckt declarations and tables to
                  the blif file specified.]

  SideEffects	[ ]

  SeeAlso	[  ]
**********************************************************************/
static int
_IoHnodeWriteBlifRecursivelyStep(
    Io_Encoding_Type_t encodingType,
    Hrc_Node_t *hnode,
    FILE *fp,
    FILE *encFp,
    int verbosity)
{
    Tbl_Table_t *table, *singleOutputTable;
    int i, j;
    Var_Variable_t *var, *actualVar;
    char *name, *instanceName, *modelName;
    st_generator *gen;
    st_table *blifInputsStTable, *blifOutputsStTable, *printedMvsStTable;
    st_table *encOutputsStTable, *encInputsStTable;
    Hrc_Node_t *subcktHnode;
    Hrc_Model_t *model, *subcktModel;
    Hrc_Subckt_t *subckt;
    Hrc_Manager_t *manager;
    array_t *subcktActualInputVars, *subcktActualOutputVars;


    printedMvsStTable = st_init_table(strcmp, st_strhash);

  /* .model */
    modelName = Hrc_NodeReadModelName(hnode);
    manager = Hrc_NodeReadManager(hnode);
    model = Hrc_ManagerFindModelByName(manager, modelName);
    (void)fprintf(fp,".model %s\n", modelName);

    /* .inputs line of blif file*/
    if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
	(void)fprintf(fp,".inputs ");
	Hrc_NodeForEachFormalInput(hnode,i,var){
	    (void)fprintf(fp,"%s0 ",Var_VariableReadName(var));
	}
	(void)fprintf(fp,"\n");
    }
    
    /* .outputs line of blif file*/
    if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
	(void)fprintf(fp,".outputs ");
	Hrc_NodeForEachFormalOutput(hnode,i,var){
	    (void)fprintf(fp,"%s0 ",Var_VariableReadName(var));
	}
	(void)fprintf(fp,"\n");
    }
    
    /* .subckt stuff */
    Hrc_ModelForEachSubckt(model,gen,instanceName,subckt){
      subcktModel = Hrc_SubcktReadModel(subckt);
      subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
      subcktActualInputVars = Hrc_SubcktReadActualInputVars(subckt);
      subcktActualOutputVars = Hrc_SubcktReadActualOutputVars(subckt);
      
      /* .subckt declarations */
      (void)fprintf(fp,".subckt %s ",
		    Hrc_ModelReadName(subcktModel));
      Hrc_NodeForEachFormalInput(subcktHnode,i,var){
	actualVar = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
	(void)fprintf(fp,"%s0=%s0 ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
      }   
      Hrc_NodeForEachFormalOutput(subcktHnode,i,var){
	actualVar = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
	(void)fprintf(fp,"%s0=%s0 ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
      }   
      (void)fprintf(fp,"\n");
    }

    encOutputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
    encInputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
    blifInputsStTable = st_init_table(strcmp, st_strhash);
    blifOutputsStTable = st_init_table(strcmp, st_strhash);

    /* .latch declarations for blif file */
    IoWriteLatches(hnode, fp, encFp, printedMvsStTable, blifOutputsStTable, blifInputsStTable, encOutputsStTable, encInputsStTable, 0, 0, verbosity);
    Hrc_NodeForEachNameTable(hnode, i, table){
	if(IoOutputExpansionRequired(table)){
	    if(verbosity > 0){
		(void)fprintf(stdout, "Splitting into Single Output Table before Processing\n");
	    }
	    for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
		singleOutputTable = IoMakeSingleOutputTable(table, j);
		_IoTableWriteBlif(encodingType, hnode, singleOutputTable, blifInputsStTable, fp, encFp,
				  verbosity);
		Tbl_TableFree(singleOutputTable);
	    }
	}
	else{
	    if(!((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1))){
		_IoTableWriteBlif(encodingType, hnode, table, blifInputsStTable, fp, encFp,
				  verbosity);
	    }
	}
    }
    st_foreach_item_int(blifInputsStTable, gen, &name, &i){
	FREE(name);
    }
    st_foreach_item_int(blifOutputsStTable, gen, &name, &i){
	FREE(name);
    }
    st_free_table(blifInputsStTable);
    st_free_table(blifOutputsStTable);
    st_free_table(encInputsStTable);
    st_free_table(encOutputsStTable);
    st_foreach_item_int(printedMvsStTable, gen, &name, &i){
	FREE(name);
    }
    st_free_table(printedMvsStTable);
    fprintf(fp,".end\n");
    return 1;
}



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


  Synopsis	[ Checks if pseudoinput is also a PO]

  Description	[ Checks if table has 0input, >1 output, or 1 output 
                  with multiple valued entry]

  SideEffects	[ ]

  SeeAlso	[  ]
**********************************************************************/
static int
_IoCheckPseudoinputIsPO(
   Tbl_Table_t *table)
{
  int j;
  Var_Variable_t *var = NIL(Var_Variable_t); /* to suppress warning */
  Tbl_Entry_t *entry;
  int numValues;
    
  if((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1)){
    /* assume all are pseudoinputs */
    Tbl_TableForEachOutputVar(table, j, var){
      if(Var_VariableTestIsPO(var)){
	return 1;
      }
    }
  }

  if(Tbl_TableReadNumInputs(table) == 0){
    if(Tbl_TableReadNumRows(table) != 0){
      entry = Tbl_TableReadEntry(table, 0, 0, 1);
      numValues = Tbl_EntryReadNumValues(entry);
    }
    else{
      entry = Tbl_TableDefaultReadEntry(table, 0);
      numValues = Tbl_EntryReadNumValues(entry);
    }

    Tbl_TableForEachOutputVar(table, j, var);
    if(Tbl_TableReadNumRows(table) <= 1){
      if(numValues > 1){
	if(Var_VariableTestIsPO(var)){
	  return 1;
	}
      }
    }
    else{
      if(Var_VariableTestIsPO(var)){      
	return 1;
      }
    }
  }

  return 0;
}