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

  FileName    [synthWrite.c]

  PackageName [synth]

  Synopsis    [Functions to write blif file and equation file.]

  Description []

  Author      [In-Ho Moon, Balakrishna Kumthekar]

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

static char rcsid[] UNUSED = "$Id: synthWrite.c,v 1.43 2005/05/11 20:18:39 hhhan Exp $";

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


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


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

/**Struct**********************************************************************

  Synopsis    [Type to store a line of the truth table of a node.
  The entire truth table is implemented as a linked list of
  objects of this type.]

  Description []

  SeeAlso     []

******************************************************************************/
typedef struct TruthTableLine {
  char *values;    /* string of 1, 0, and - */
  struct TruthTableLine *next; /* pointer to next table line */
} TruthTableLine;


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

static	char		*DefaultPrefix = "_n";
static	char		*InternalNodePrefix;
static	st_table	*NodeNameTable; /* to keep all node names for
					 * primary input, primary output 
					 * latch input and output
					 */

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

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

static void WriteMlBlif(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, FILE *fout, int no, bdd_node **ofuncs, int *oflags, int top_flag, int verbosity);
static void WriteLeafMlBlif(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, FILE *fout, int no, bdd_node **ofuncs, int *oflags, int top_flag, int verbosity);
static void WriteBlifBinary(bdd_manager *dd, bdd_node *node, char *name, FILE *fout, int *support);
static void WriteEqnOfTree(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs);
static int GetEqnOfTree(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, char *eq, bdd_node **ofuncs);
static void WriteMlTreeBlif(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, char *func_name, int ref);
static void WriteMultiLevelBlif(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no);
static TruthTableLine * GetMultiLevelBlifRecur(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static int GetMultiLevelNodes(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static int GetLeafNodes(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static TruthTableLine * GetTautologyLine(int ni);
static TruthTableLine * GetLeafLines(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
static TruthTableLine * GetBlifBinary(TruthTableLine *line, bdd_manager *dd, bdd_node *node, char *values, int *support, int ni);
static TruthTableLine * GetComplementOneLine(TruthTableLine *line, int ni, int flag);
static TruthTableLine * GetComplementLines(TruthTableLine *lines, int ni, int flag);
static TruthTableLine * GetAndLines(TruthTableLine *line1, TruthTableLine *line2, int ni, int flag);
static bdd_node	* GetDdNodeOfMlTree(MlTree *tree, int comp);
static int GetMlTreeName(Ntk_Network_t *net, bdd_node **ofuncs, MlTree *tree, char *name);
static char ** GetAllVarNameArray(bdd_manager *dd);

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


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


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


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

  Synopsis    [Compares two strings to see which one is first in
  alphabetic order.]

  Description [Compares two strings to see which one is first in
  alphabetic order.]

  SideEffects []

  SeeAlso     [qsort]

******************************************************************************/
int
SynthStringCompare(char **a,
		   char **b)
{
  char	*pa, *pb;

  pa = *a;
  pb = *b;

  if (*pa == '\0') {
    if (*pb == '\0')
      return(0);
    else
      return(-1);
  } else if (*pb == '\0')
    return(1);
  while (*pa != '\0' && *pb != '\0') {
    if (*pa > *pb)
      return(1);
    if (*pa < *pb)
      return(-1);
    pa++;
    pb++;
    if (*pa == '\0') {
      if (*pb == '\0')
	return(0);
      else
	return(-1);
    } else if (*pb == '\0')
      return(1);
  }
  return(0);
}


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

  Synopsis    [Write a blif file of the factorized network.]

  Description [Write a blif file of the factorized network. There are 2
  ways of writing a blif file depending on argument ml_mode. If
  ml_mode is 0, then the resulting blif file will be based on the
  factorized multi level tree that has 3 children; quotient, divisor,
  and remainder. If ml_mode is 1, then the resulting blif file will be
  generated as follows. All top nodes and all nodes that are shared will
  be output nodes of .names in blif file. By default, ml_mode is 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthWriteBlifFile(Ntk_Network_t *net,
		   bdd_manager *dd,
		   MlTree **tree,
		   char *filename,
		   int no,
		   bdd_node **ofuncs,
		   int *initStates,
		   int ml_mode,
		   int verbosity)
{
  FILE		*fout;
  int		i, j;
  int		*oflags;
  char		out_name[MAX_NAME_LEN], name[MAX_NAME_LEN];
  lsGen		gen;
  Ntk_Node_t	*node;
  char		**sorted_name;
  int		ni, po;
  int		polarity;

  fout = Cmd_FileOpen(filename, "w", NIL(char *), 0);
  if (!fout) {
    (void)fprintf(vis_stdout,
		  "** synth error: Error in opening file [%s]\n", filename);
    return;
  }

  fprintf(fout, ".model %s\n", Ntk_NetworkReadName(net));
  fprintf(fout, ".inputs");

  /* Write list of primary inputs sorted lexicographically. */
  ni = Ntk_NetworkReadNumPrimaryInputs(net);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, ni, sizeof(char *),
	(int (*)(const void *, const void *)) SynthStringCompare);
  for (i = 0; i < ni; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);

  fprintf(fout, "\n");
  fprintf(fout, ".outputs");

  /* Write list of primary outputs sorted lexicographically. */
  po = Ntk_NetworkReadNumPrimaryOutputs(net);
  sorted_name = ALLOC(char *, po * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, po, sizeof(char *),
	(int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < po; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);
  fprintf(fout, "\n");

  /* Print list of latches. */
  i = 0;
  Ntk_NetworkForEachLatch(net, gen, node) {
    fprintf(fout,".latch %s", Ntk_NodeReadName(Ntk_LatchReadDataInput(node)));
    fprintf(fout, " %s", Ntk_NodeReadName(node));
    fprintf(fout, " %d\n", initStates[i]);
    i++;
  }

  oflags = ALLOC(int, no);
  (void)memset((void *)oflags, 0, no * sizeof(int));
  for (i = 0; i < no; i++) {
    if (!tree[i])
      continue;
    if (bdd_is_constant(tree[i]->node)) {
      if (tree[i]->comp) {
	for (j = 0; j < no; j++) {
	  if (tree[i]->complement == ofuncs[j] && oflags[j] == 0) {
	    sprintf(out_name, "%s", SynthGetIthOutputName(j));
	    break;
	  }
	}
      } else {
	for (j = 0; j < no; j++) {
	  if (tree[i]->node == ofuncs[j] && oflags[j] == 0) {
	    sprintf(out_name, "%s", SynthGetIthOutputName(j));
	    break;
	  }
	}
      }
      if (j == no)
	SynthGetInternalNodeName(out_name, tree[i]->id);
      else {
	if (oflags[j])
	  continue;
	else
	  oflags[j] = 1;
      }
      fprintf(fout, "\n.names %s\n", out_name);
      if (tree[i]->node == bdd_read_one(dd)) {
	if (tree[i]->comp)
	  fprintf(fout, "0\n");
	else
	  fprintf(fout, "1\n");
      } else {
	if (tree[i]->comp)
	  fprintf(fout, "1\n");
	else
	  fprintf(fout, "0\n");
      }
      continue;
    } else if (tree[i]->ref) {
      for (j = 0; j < no; j++) {
	if ((((tree[i]->comp == 0 && tree[i]->node == ofuncs[j]) ||
	      (tree[i]->comp && tree[i]->complement == ofuncs[j]))) &&
	    oflags[j] == 0) {
	  sprintf(out_name, "%s", SynthGetIthOutputName(j));
	  break;
	}
      }
      if (j == no)
	SynthGetInternalNodeName(out_name, tree[i]->id);
      else {
	if (oflags[j])
	  continue;
	else
	  oflags[j] = 1;
      }
      polarity = GetMlTreeName(net, ofuncs, tree[i], name);
      if (strcmp(out_name, name) == 0)
	SynthGetPrimaryNodeName(net, tree[i]->node, name);
      fprintf(fout, "\n.names %s %s\n", name, out_name);
      if (polarity == 0) {
	if (tree[i]->comp)
	  fprintf(fout, "0 1\n");
	else
	  fprintf(fout, "1 1\n");
      } else {
	if (tree[i]->comp)
	  fprintf(fout, "1 1\n");
	else
	  fprintf(fout, "0 1\n");
      }
      continue;
    }
    if (ml_mode == 0) {
      if (tree[i]->pi) {
	tree[i]->pi = 0;
	WriteMlBlif(net, dd, tree[i], fout, no, ofuncs, oflags, 1, verbosity);
	tree[i]->pi = 1;
      } else {
	WriteMlBlif(net, dd, tree[i], fout, no, ofuncs, oflags, 1, verbosity);
      }
    } else {
      for (j = 0; j < no; j++) {
	if (tree[i]->node == ofuncs[j]) {
	  if (oflags[j])
	    continue;
	  else
	    oflags[j] = 1;
	  sprintf(out_name, "%s", SynthGetIthOutputName(j));
	  break;
	}
      }
      if (j == no)
	SynthGetInternalNodeName(out_name, tree[i]->id);
      if (tree[i]->pi) {
	tree[i]->pi = 0;
	WriteMlTreeBlif(fout, net, dd, tree[i], ofuncs, no, out_name, 1);
	tree[i]->pi = 1;
      } else {
	WriteMlTreeBlif(fout, net, dd, tree[i], ofuncs, no, out_name, 1);
      }
    }
  }
  FREE(oflags);

  fprintf(fout, "\n.end\n");
  fclose(fout);
}


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

  Synopsis    [Writes header of equation format for a network.]

  Description [Writes header of equation format for a network.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthWriteEqnHeader(FILE *fout,
		  Ntk_Network_t *net,
		  bdd_manager *dd)
{
  int		i;
  lsGen		gen;
  Ntk_Node_t	*node;
  char		**sorted_name;
  int		ni, po;

  /* Write list of primary inputs sorted lexicographically. */
  ni = Ntk_NetworkReadNumPrimaryInputs(net);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, ni, sizeof(char *),
	(int (*)(const void *, const void *))SynthStringCompare);
  fprintf(fout, "INORDER");
  for (i = 0; i < ni; i++)
    fprintf(fout," %s", sorted_name[i]);
  fprintf(fout, "\n");
  FREE(sorted_name);

  /* Write list of primary outputs sorted lexicographically. */
  po = Ntk_NetworkReadNumPrimaryOutputs(net);
  sorted_name = ALLOC(char *, po * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, po, sizeof(char *),
	(int (*)(const void *, const void *))SynthStringCompare);
  fprintf(fout, "OUTORDER");
  for (i = 0; i < po; i++)
    fprintf(fout," %s", sorted_name[i]);
  fprintf(fout, "\n");
  FREE(sorted_name);
}


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

  Synopsis    [Writes an equation of a factorized tree.]

  Description [Writes an equation of a factorized tree.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthWriteEqn(FILE *fout,
	      Ntk_Network_t *net,
	      bdd_manager *dd,
	      MlTree *tree,
	      bdd_node **ofuncs,
	      char *func_name,
	      int ref)
{
  char	name[MAX_NAME_LEN];
  int	polarity = 0;

  if (tree->top || tree->shared) {
    if (ref) {
      /* If tree is shared we print the name of the original function
       * unless it is a constant.
       */
      if (tree->ref) {
	if (tree->node == bdd_read_zero(dd))
	  sprintf(name, "zero");
	else if (tree->node == bdd_read_one(dd))
	  sprintf(name, "one");
	else
	  polarity = GetMlTreeName(net, ofuncs, tree, name);
	if (polarity == 0) {
	  if (tree->comp)
	    SynthMakeComplementString(name);
	} else {
	  if (!tree->comp)
	    SynthMakeComplementString(name);
	}
	fprintf(fout, "%s = %s\n", func_name, name);
	return;
      }
    }
    WriteEqnOfTree(fout, net, dd, tree, ofuncs);
  }

  if (tree->leaf) {
    return;
  }

  if (tree->q_ref == 0)
    SynthWriteEqn(fout, net, dd, tree->q, ofuncs, NULL, ref);
  if (tree->d_ref == 0)
    SynthWriteEqn(fout, net, dd, tree->d, ofuncs, NULL, ref);
  if (tree->r_ref == 0)
    SynthWriteEqn(fout, net, dd, tree->r, ofuncs, NULL, ref);
}


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

  Synopsis    [Set the prefix of internal node name.]

  Description [Set the prefix of internal node name.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthSetInternalNodePrefix(char *prefix)
{
  if (prefix)
    InternalNodePrefix = prefix;
  else
    InternalNodePrefix = DefaultPrefix;
}


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

  Synopsis    [Creates a st_table to keep all node names for primary
  input, primary output, latch input and output nodes.]

  Description [Creates a st_table to keep all node names for primary
  input, primary output, latch input and output nodes. This table is used
  when we make internal node names, to see if there is a same name.]

  SideEffects []

  SeeAlso     [SynthFreeNodeNameTable SynthGetInternalNodeName]

******************************************************************************/
void
SynthSetupNodeNameTable(Ntk_Network_t *net)
{
  lsGen		gen;
  Ntk_Node_t	*node;

  if (NodeNameTable) {
    (void)fprintf(vis_stdout,
	"** synth warning: table already exists in SynthSetupNodeNameTable.\n");
    st_free_table(NodeNameTable);
  }

  NodeNameTable = st_init_table(strcmp, st_strhash);

  /* Register all primary input node names. */
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
  }

  /* Register all primary output node names. */
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
  }

  /* Register all latch input and output node names. */
  Ntk_NetworkForEachLatch(net, gen, node) {
    st_insert(NodeNameTable, Ntk_NodeReadName(Ntk_LatchReadDataInput(node)),
    	      (char *)NULL);
    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
  }
}


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

  Synopsis    [Frees the st_table named NodeNameTable.]

  Description [Frees the st_table named NodeNameTable.]

  SideEffects []

  SeeAlso     [SynthSetupNodeNameTable SynthGetInternalNodeName]

******************************************************************************/
void
SynthFreeNodeNameTable(void)
{
  st_free_table(NodeNameTable);
  NodeNameTable = NIL(st_table);
}


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

  Synopsis    [Returns a proper internal node name.]

  Description [Returns a proper internal node name. Internal node name
  is made by "prefix+id". If NodeNameTable exists, fist lookup the table
  to see if the name already exists. If it exists, another prefix
  "_synth_" is used. Then, whenever a same name exists, extra prefix "_"
  is used.]

  SideEffects []

  SeeAlso     [SynthSetupNodeNameTable SynthFreeNodeNameTable]

******************************************************************************/
void
SynthGetInternalNodeName(char *name, int id)
{
  sprintf(name, "%s%d", InternalNodePrefix, id);
  if (NodeNameTable) {
    if (st_lookup(NodeNameTable, name, NIL(char *))) {
      int	pos;

      sprintf(name, "_synth_%s%d", InternalNodePrefix, id);
      pos = 7; /* _synth_ */
      while (st_lookup(NodeNameTable, name, NIL(char *))) {
	sprintf(&name[pos], "_%s%d", InternalNodePrefix, id);
	pos++;
      }
    }
  } else {
    (void)fprintf(vis_stdout,
    		  "** synth warning: skipping internal node name checking.\n");
  }
}


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

  Synopsis    [Dumps Bdds of all output nodes.]

  Description [Dumps Bdds of all output nodes. just for debug]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthDumpBlif(Ntk_Network_t *net,
	      bdd_manager *dd,
	      int no,
	      bdd_node **ofuncs,
	      char **onames,
	      int *initStates,
	      char *model)
{
  int		size;
  bdd_node	**bdds;
  FILE		*fout;
  char		**inames;
  char		filename[MAX_NAME_LEN];
  int		i;
  lsGen		gen;
  Ntk_Node_t	*node;
  char		**sorted_name;
  int		ni, po;

  sprintf(filename, "%s.debug.blif", model);
  fout = fopen(filename, "w");
  if (!fout) {
    (void)fprintf(vis_stderr,
		  "** synth error: Can't open the file %s.\n", filename);
    return;
  }

  fprintf(fout, ".model %s\n", model);
  fprintf(fout, ".inputs");

  /* Write list of primary inputs sorted lexicographically. */
  ni = Ntk_NetworkReadNumPrimaryInputs(net);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, ni, sizeof(char *),
	(int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < ni; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);

  fprintf(fout, "\n");
  fprintf(fout, ".outputs");

  /* Write list of primary outputs sorted lexicographically. */
  po = Ntk_NetworkReadNumPrimaryOutputs(net);
  sorted_name = ALLOC(char *, po * sizeof(char *));
  i = 0;
  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
    sorted_name[i++] = Ntk_NodeReadName(node);
  }
  qsort(sorted_name, po, sizeof(char *),
	(int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < po; i++)
    fprintf(fout," %s", sorted_name[i]);
  FREE(sorted_name);
  fprintf(fout, "\n");

  /* Print list of latches. */
  i = 0;
  Ntk_NetworkForEachLatch(net, gen, node) {
    fprintf(fout,".latch %s", Ntk_NodeReadName(Ntk_LatchReadDataInput(node)));
    fprintf(fout, " %s", Ntk_NodeReadName(node));
    fprintf(fout, " %d\n", initStates[i]);
    i++;
  }

  bdds = ALLOC(bdd_node *, no);

  for (i = 0; i < no; i++) {
    bdds[i] = bdd_make_bdd_from_zdd_cover(dd, ofuncs[i]);
    bdd_ref(bdds[i]);
  }

  inames = GetAllVarNameArray(dd);
  if (!inames) {
    for (i = 0; i < no; i++)
      bdd_recursive_deref(dd, bdds[i]);
    FREE(bdds);
    fclose(fout);
    (void)fprintf(vis_stderr, "** synth error: Out of memory.\n");
    return;
  }

  bdd_dump_blif_body(dd, no, bdds, inames, onames, fout);
  fprintf(fout, ".end\n");

  size = bdd_num_vars(dd);
  for (i = 0; i < size; i++)
    FREE(inames[i]);
  FREE(inames);

  for (i = 0; i < no; i++)
    bdd_recursive_deref(dd, bdds[i]);

  FREE(bdds);
  fclose(fout);
}


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

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

  Synopsis    [Writes a part of a blif file for each output function.]

  Description [Writes a part of a blif file for each output function.
  The resulting blif file will be based on the factorized multi level tree
  that has 3 children: quotient, divisor, and remainder.]

  SideEffects []

  SeeAlso     [WriteMlTreeBlif]

******************************************************************************/
static void
WriteMlBlif(Ntk_Network_t *net,
	    bdd_manager *dd,
	    MlTree *tree,
	    FILE *fout,
	    int no,
	    bdd_node **ofuncs,
	    int *oflags,
	    int top_flag,
	    int verbosity)
{
  int		i;
  char		name[MAX_NAME_LEN], q_name[MAX_NAME_LEN];
  char		d_name[MAX_NAME_LEN], r_name[MAX_NAME_LEN];
  char		eq[MAX_EQ_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  char		q, d, r;
  int		comp;

  if (tree->leaf) {
    WriteLeafMlBlif(net, dd, tree, fout, no, ofuncs, oflags, top_flag,
		    verbosity);
    return;
  }

  if (!tree->ref) {
    if (!tree->q_ref)
      WriteMlBlif(net, dd, tree->q, fout, no, ofuncs, oflags, 0, verbosity);
    if (!tree->d_ref)
      WriteMlBlif(net, dd, tree->d, fout, no, ofuncs, oflags, 0, verbosity);
    if (!tree->r_ref)
      WriteMlBlif(net, dd, tree->r, fout, no, ofuncs, oflags, 0, verbosity);
  }

  for (i = 0; i < no; i++) {
    if (tree->node == ofuncs[i]) {
      if (top_flag == 0)
	return;

      if (oflags[i])
	continue;
      else
	oflags[i] = 1;
      sprintf(name, "%s",  SynthGetIthOutputName(i));
      break;
    }
  }
  if (i == no)
    SynthGetInternalNodeName(name, tree->id);

  fprintf(fout, "\n");
  if (verbosity > 2) {
    SynthGetChildMlTreeWithName(net, dd, tree, eq);
    (void)fprintf(fout, "# %s\n", eq);
  }

  if (tree->q->pi) {
    comp = SynthGetPrimaryNodeName(net, tree->q->node, q_name);

    if (comp)
      q = '0';
    else
      q = '1';
    if (tree->q_comp) {
      if (q == '0')
	q = '1';
      else
	q = '0';
    }
  } else {
    for (i = 0; i < no; i++) {
      if (tree->q->node == ofuncs[i]) {
	sprintf(q_name, "%s",  SynthGetIthOutputName(i));
	break;
      }
    }
    if (i == no)
      SynthGetInternalNodeName(q_name, tree->q->id);
    if (tree->q_comp)
      q = '0';
    else
      q = '1';
  }
  if (tree->d->pi) {
    comp = SynthGetPrimaryNodeName(net, tree->d->node, d_name);

    if (comp)
      d = '0';
    else
      d = '1';
    if (tree->d_comp) {
      if (d == '0')
	d = '1';
      else
	d = '0';
    }
  } else {
    for (i = 0; i < no; i++) {
      if (tree->d->node == ofuncs[i]) {
	sprintf(d_name, "%s", SynthGetIthOutputName(i));
	break;
      }
    }
    if (i == no)
      SynthGetInternalNodeName(d_name, tree->d->id);
    if (tree->d_comp)
      d = '0';
    else
      d = '1';
  }
  if (tree->r->pi) {
    comp = SynthGetPrimaryNodeName(net, tree->r->node, r_name);

    if (comp)
      r = '0';
    else
      r = '1';
    if (tree->r_comp) {
      if (r == '0')
	r = '1';
      else
	r = '0';
    }
  } else {
    for (i = 0; i < no; i++) {
      if (tree->r->node == ofuncs[i]) {
	sprintf(r_name, "%s", SynthGetIthOutputName(i));
	break;
      }
    }
    if (i == no)
      SynthGetInternalNodeName(r_name, tree->r->id);
    if (tree->r_comp)
      r = '0';
    else
      r = '1';
  }

  if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == zero ||
      GetDdNodeOfMlTree(tree->d, tree->d_comp) == zero) {
    if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "0\n");
    } else {
      fprintf(fout, ".names %s %s\n", r_name, name);
      fprintf(fout, "%c 1\n", r);
    }
  } else if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == one) {
    if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == zero) {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
	fprintf(fout, ".names %s\n", name);
	fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
	fprintf(fout, ".names %s\n", name);
	fprintf(fout, "0\n");
      } else {
	fprintf(fout, ".names %s %s\n", r_name, name);
	fprintf(fout, "%c 1\n", r);
      }
    } else {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
	fprintf(fout, ".names %s\n", name);
	fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
	fprintf(fout, ".names %s %s\n", d_name, name);
	fprintf(fout, "%c 1\n", d);
      } else {
	fprintf(fout, ".names %s %s %s\n", d_name, r_name,
		name);
	fprintf(fout, "%c- 1\n", d);
	fprintf(fout, "-%c 1\n", r);
      }
    }
  } else if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one) {
    if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == zero) {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
	fprintf(fout, ".names %s\n", name);
	fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
	fprintf(fout, ".names %s\n", name);
	fprintf(fout, "0\n");
      } else {
	fprintf(fout, ".names %s %s\n", r_name, name);
	fprintf(fout, "%c 1\n", r);
      }
    } else {
      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
	fprintf(fout, ".names %s\n", name);
	fprintf(fout, "1\n");
      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
	fprintf(fout, ".names %s %s\n", q_name, name);
	fprintf(fout, "%c 1\n", q);
      } else {
	fprintf(fout, ".names %s %s %s\n", q_name, r_name, name);
	fprintf(fout, "%c- 1\n", q);
	fprintf(fout, "-%c 1\n", r);
      }
    }
  } else {
    if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
      fprintf(fout, ".names %s\n", name);
      fprintf(fout, "1\n");
    } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
      fprintf(fout, ".names %s %s %s\n", q_name, d_name, name);
      fprintf(fout, "%c%c 1\n", q, d);
    } else {
      fprintf(fout, ".names %s %s %s %s\n", q_name, d_name, r_name, name);
      fprintf(fout, "%c%c- 1\n", q, d);
      fprintf(fout, "--%c 1\n", r);
    }
  }
}

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

  Synopsis    [Writes a .names block in blif file for each tree that is a leaf
  node.]

  Description [Writes a .names block in blif file for each tree that is a leaf
  node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
WriteLeafMlBlif(Ntk_Network_t *net,
		bdd_manager *dd,
		MlTree *tree,
		FILE *fout,
		int no,
		bdd_node **ofuncs,
		int *oflags,
		int top_flag,
		int verbosity)
{
  int		i, count, *support;
  char		name[MAX_EQ_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  char		out_name[MAX_NAME_LEN];
  bdd_node	*node;
  Ntk_Node_t	*ntk_node;
  int		sizeZ;

  sizeZ = bdd_num_zdd_vars(dd);

  if (tree->node == one || tree->node == zero || tree->pi)
    return;

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;
  for (i = 0; i < no; i++) {
    if (node == ofuncs[i]) {
      if (top_flag == 0)
	return;

      if (oflags[i])
	continue;
      else
	oflags[i] = 1;
      sprintf(out_name, "%s", SynthGetIthOutputName(i));
      break;
    }
  }
  if (i == no)
    SynthGetInternalNodeName(out_name, tree->id);
  else {
    ntk_node = Ntk_NetworkFindNodeByName(net, out_name);
    if (Ntk_NodeTestIsLatch(ntk_node))
      return;
  }

  fprintf(fout, "\n");
  if (verbosity > 2) {
    SynthGetChildMlTreeWithName(net, dd, tree, name);
    fprintf(fout, "# %s\n", name);
  }
  fprintf(fout, ".names ");

  support = ALLOC(int, sizeZ);
  if (!support)
    return;
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  count = 0;
  for (i = 0; i < sizeZ; i++) {
    if (support[i]) {
      SynthGetPrimaryIndexName(net, i, name);
      fprintf(fout, "%s ", name);
      if (i % 2 == 0) {
	support[i] = count;
	i++;
	if (support[i])
	  support[i] = count;
      } else {
	support[i] = count;
      }
      count++;
    }
  }
  fprintf(fout, "%s\n", out_name);

  for (i = 0; i < count; i++)
    name[i] = '-';
  name[count] = '\0';
  WriteBlifBinary(dd, node, name, fout, support);
  FREE(support);
}


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

  Synopsis    [Writes all cubes of the node in .name block.]

  Description [Writes all cubes of the node in .name block. This can be done
  by finding all paths to the constant 1 node from the node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
WriteBlifBinary(bdd_manager *dd,
		bdd_node *node,
		char *name,
		FILE *fout,
		int *support)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		id = bdd_node_read_index(node);

  if (node == zero)
    return;

  if (node == one) {
    fprintf(fout, "%s 1\n", name);
    return;
  }

  if (id % 2 == 0)
    name[support[id]] = '1';
  else
    name[support[id]] = '0';
  WriteBlifBinary(dd, bdd_bdd_T(node), name, fout, support);
  name[support[id]] = '-';
  WriteBlifBinary(dd, bdd_bdd_E(node), name, fout, support);
  name[support[id]] = '-';
}


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

  Synopsis    [Writes multi level equations of a tree.]

  Description [Writes multi level equations of a tree.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
WriteEqnOfTree(FILE *fout,
	       Ntk_Network_t *net,
	       bdd_manager *dd,
	       MlTree *tree,
	       bdd_node **ofuncs)
{
  char	eq[MAX_EQ_LEN];
  char	name[MAX_NAME_LEN];
  int	polarity = 0;

  polarity = GetMlTreeName(net, ofuncs, tree, name);
  eq[0] = '\0';
  GetEqnOfTree(net, dd, tree, tree, eq, ofuncs);
  if (polarity)
    SynthMakeComplementString(eq);
  fprintf(fout, "%s = %s\n", name, eq);
}


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

  Synopsis    [Gets multi level equations of a tree.]

  Description [Gets multi level equations of a tree.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetEqnOfTree(Ntk_Network_t *net,
	     bdd_manager *dd,
	     MlTree *top,
	     MlTree *tree,
	     char *eq,
	     bdd_node **ofuncs)
{
  char		q_eq[MAX_EQ_LEN];
  char		d_eq[MAX_EQ_LEN];
  char		r_eq[MAX_EQ_LEN];
  char		qd_eq[MAX_EQ_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*f;
  int		flag;
  int		polarity = 0;

  if (tree != top && tree->shared) {
    polarity = GetMlTreeName(net, ofuncs, tree, eq);
    if (polarity)
      SynthMakeComplementString(eq);
    return(0);
  }

  f = tree->node;
  if (tree->leaf) {
    flag = SynthGetChildTreeWithName(net, dd, f, eq);
    return(flag);
  }

  if (f == one) {
    sprintf(eq, "one");
    return(0);
  } else if (f == zero) {
    sprintf(eq, "zero");
    return(0);
  }

  q_eq[0] = d_eq[0] = r_eq[0] = '\0';
  flag = GetEqnOfTree(net, dd, top, tree->q, q_eq, ofuncs);
  if (tree->q_comp)
    SynthMakeComplementString(q_eq);
  if (flag)
    return(1);
  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one)
    d_eq[0] = '\0';
  else {
    flag = GetEqnOfTree(net, dd, top, tree->d, d_eq, ofuncs);
    if (tree->d_comp)
      SynthMakeComplementString(d_eq);
    if (flag)
      return(1);
  }
  flag = GetEqnOfTree(net, dd, top, tree->r, r_eq, ofuncs);
  if (tree->r_comp)
    SynthMakeComplementString(r_eq);
  if (flag)
    return(1);

  if (strcmp(q_eq, "one") == 0)
    sprintf(qd_eq, "%s", d_eq);
  else if (strcmp(q_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else if (strcmp(d_eq, "one") == 0)
    sprintf(qd_eq, "%s", q_eq);
  else if (strcmp(d_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else {
    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", q_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
	eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	eq[MAX_EQ_LEN - 1] = '\0';
      } else {
	eq[strlen(eq)] = '#'; /* truncated */
	eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(qd_eq, "%s %s", q_eq, d_eq);
  }

  if (strcmp(r_eq, "zero") == 0)
    sprintf(eq, "%s", qd_eq);
  else {
    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", qd_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
	eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	eq[MAX_EQ_LEN - 1] = '\0';
      } else {
	eq[strlen(eq)] = '#'; /* truncated */
	eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
  }
  return(0);
}


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

  Synopsis    [Writes a part of a blif file for each output function.]

  Description [Writes a part of a blif file for each output function.
  All top nodes and all nodes that are shared will be output nodes of
  .names in blif file.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
WriteMlTreeBlif(FILE *fout,
		Ntk_Network_t *net,
		bdd_manager *dd,
		MlTree *tree,
		bdd_node **ofuncs,
		int no,
		char *func_name,
		int ref)
{
  char	name[MAX_NAME_LEN];
  int	polarity = 0;

  if (tree->top || tree->shared) {
    if (ref) {
      if (tree->ref) {
	polarity = GetMlTreeName(net, ofuncs, tree, name);
	fprintf(fout, "\n.names %s %s\n", name, func_name);
	if (polarity == 0) {
	  if (tree->comp)
	    fprintf(fout, "0 1\n");
	  else
	    fprintf(fout, "1 1\n");
	} else {
	  if (tree->comp)
	    fprintf(fout, "1 1\n");
	  else
	    fprintf(fout, "0 1\n");
	}
	return;
      }
    }
    WriteMultiLevelBlif(fout, net, dd, tree, ofuncs, no);
  }

  if (tree->leaf)
    return;

  if (tree->q_ref == 0)
    WriteMlTreeBlif(fout, net, dd, tree->q, ofuncs, no, NULL, ref);
  if (tree->d_ref == 0)
    WriteMlTreeBlif(fout, net, dd, tree->d, ofuncs, no, NULL, ref);
  if (tree->r_ref == 0)
    WriteMlTreeBlif(fout, net, dd, tree->r, ofuncs, no, NULL, ref);
}


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

  Synopsis    [Writes a .names block in blif file for each tree that is a
  top node or a shared node.]

  Description [Writes a .names block in blif file for each tree that is a
  top node or a shared node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
WriteMultiLevelBlif(FILE *fout,
		    Ntk_Network_t *net,
		    bdd_manager *dd,
		    MlTree *tree,
		    bdd_node **ofuncs,
		    int no)
{
  int			i, ni;
  char			name[MAX_NAME_LEN];
  TruthTableLine	*lines, *cur, *next;
  st_table		*table;
  char			**sorted_name, *key;
  st_generator		*gen;
  int			pos;
  Ntk_Node_t		*ntk_node;
  int			polarity = 0;

  polarity = GetMlTreeName(net, ofuncs, tree, name);
  for (i = 0; i < no; i++) {
    if (tree->node == ofuncs[i]) {
      ntk_node = Ntk_NetworkFindNodeByName(net, name);
      if (Ntk_NodeTestIsLatch(ntk_node))
	return;
    }
  }

  table = st_init_table(strcmp, st_strhash);
  ni = 0;
  ni = GetMultiLevelNodes(net, dd, tree, tree, ofuncs, no, table, ni);
  sorted_name = ALLOC(char *, ni * sizeof(char *));
  i = 0;
  st_foreach_item_int(table, gen, (char **)&key, &pos) {
    sorted_name[i] = key;
    i++;
  }
  qsort(sorted_name, ni, sizeof(char *),
	(int (*)(const void *, const void *))SynthStringCompare);
  for (i = 0; i < ni; i++) {
    st_insert(table, (char *)sorted_name[i], (char *)(long)i);
  }
  lines = GetMultiLevelBlifRecur(net, dd, tree, tree, ofuncs, no, table, ni);
  fprintf(fout, "\n.names");
  for (i = 0; i < ni; i++)
    fprintf(fout, " %s", sorted_name[i]);
  fprintf(fout, " %s\n", name);
  cur = lines;
  while (cur) {
    next = cur->next;
    if (polarity == 0)
      fprintf(fout, "%s 1\n", cur->values);
    else
      fprintf(fout, "%s 0\n", cur->values);
    FREE(cur->values);
    FREE(cur);
    cur = next;
  }
  st_free_table(table);
  for (i = 0; i < ni; i++)
    FREE(sorted_name[i]);
  FREE(sorted_name);
}


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

  Synopsis    [Gets all cube list of a .name block.]

  Description [Gets all cube list of a .name block.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static TruthTableLine *
GetMultiLevelBlifRecur(Ntk_Network_t *net,
		       bdd_manager *dd,
		       MlTree *top,
		       MlTree *tree,
		       bdd_node **ofuncs,
		       int no,
		       st_table *table,
		       int ni)
{
  bdd_node		*one = bdd_read_one(dd);
  bdd_node		*zero = bdd_read_zero(dd);
  bdd_node		*f;
  TruthTableLine	*line;
  TruthTableLine	*cur, *q_line, *d_line, *r_line;
  int			pos;
  char			name[MAX_NAME_LEN];
  int			polarity = 0;

  line = (TruthTableLine *)NULL;

  if (tree != top && tree->shared) {
    polarity = GetMlTreeName(net, ofuncs, tree, name);
    line = GetTautologyLine(ni);
    if (st_lookup_int(table, (char *)name, (int *)(&pos))) {
      if (polarity == 0)
	line->values[pos] = '1';
      else
	line->values[pos] = '0';
    }
    return(line);
  }

  f = tree->node;
  if (tree->leaf) {
    line = GetLeafLines(net, dd, tree, ofuncs, no, table, ni);
    return(line);
  }

  if (f == one || f == zero)
    return(line);

  q_line = GetMultiLevelBlifRecur(net, dd, top, tree->q, ofuncs,
				  no, table, ni);
  if (q_line && tree->q_comp)
    q_line = GetComplementLines(q_line, ni, 1);
  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one)
    d_line = (TruthTableLine *)NULL;
  else {
    d_line = GetMultiLevelBlifRecur(net, dd, top, tree->d, ofuncs, no,
				    table, ni);
    if (d_line && tree->d_comp)
      d_line = GetComplementLines(d_line, ni, 1);
  }
  if (q_line && d_line)
    line = GetAndLines(q_line, d_line, ni, 1);
  else if (q_line)
    line = q_line;
  else if (d_line)
    line = d_line;
  r_line = GetMultiLevelBlifRecur(net, dd, top, tree->r, ofuncs, no, table, ni);
  if (r_line && tree->r_comp)
    r_line = GetComplementLines(r_line, ni, 1);
  if (r_line) {
    cur = line;
    while (cur) {
      if (!cur->next) {
	cur->next = r_line;
	break;
      }
      cur = cur->next;
    }
  }

  return(line);
}


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

  Synopsis    [Get the names of all input nodes of .name block for an output
  tree.]

  Description [Get the names of all input nodes of .name block for an output
  tree.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetMultiLevelNodes(Ntk_Network_t *net,
		   bdd_manager *dd,
		   MlTree *top,
		   MlTree *tree,
		   bdd_node **ofuncs,
		   int no,
		   st_table *table,
		   int ni)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*f;
  char		name[MAX_NAME_LEN], *st_name;
  int		pos;

  if (tree != top && tree->shared) {
    (void) GetMlTreeName(net, ofuncs, tree, name);
    if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
      st_name = ALLOC(char, strlen(name) + 1);
      strcpy(st_name, name);
      st_insert(table, (char *)st_name, (char *)(long)ni);
      ni++;
    }
    return(ni);
  }

  f = tree->node;
  if (tree->leaf) {
    ni = GetLeafNodes(net, dd, tree, ofuncs, no, table, ni);
    return(ni);
  }

  if (f == one || f == zero)
    return(ni);

  ni = GetMultiLevelNodes(net, dd, top, tree->q, ofuncs, no, table, ni);
  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) != one)
    ni = GetMultiLevelNodes(net, dd, top, tree->d, ofuncs, no, table, ni);
  ni = GetMultiLevelNodes(net, dd, top, tree->r, ofuncs, no, table, ni);

  return(ni);
}


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

  Synopsis    [Get the names of all input nodes of a tree which is a leaf
  node.]

  Description [Get the names of all input nodes of a tree which is a leaf
  node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetLeafNodes(Ntk_Network_t *net,
	     bdd_manager *dd,
	     MlTree *tree,
	     bdd_node **ofuncs,
	     int no,
	     st_table *table,
	     int ni)
{
  int		i, *support;
  char		name[MAX_NAME_LEN], *st_name;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*node;
  int		pos, sizeZ = bdd_num_zdd_vars(dd);

  if (tree->node == one || tree->node == zero)
    return(ni);

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;

  support = ALLOC(int, sizeZ);
  if (!support)
    return(ni);
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < sizeZ; i++) {
    if (support[i]) {
      SynthGetPrimaryIndexName(net, i, name);
      if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
	st_name = ALLOC(char, strlen(name) + 1);
	strcpy(st_name, name);
	st_insert(table, (char *)st_name, (char *)(long)ni);
	ni++;
      }
    }
  }
  FREE(support);
  return(ni);
}


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

  Synopsis    [Gets a tautologous TruthTableLine.]

  Description [Gets a tautologous TruthTableLine.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static TruthTableLine *
GetTautologyLine(int ni)
{
  int			i;
  TruthTableLine	*line;

  line = ALLOC(TruthTableLine, 1);
  (void)memset((void *)line, 0, sizeof(TruthTableLine));
  line->values = (char *)malloc(ni + 1);
  for (i = 0; i < ni; i++)
    line->values[i] = '-';
  line->values[ni] = '\0';
  return(line);
}


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

  Synopsis    [Gets a list of TruthTableLine for a tree which is a leaf node.]

  Description [Gets a list of TruthTableLine for a tree which is a leaf node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static TruthTableLine *
GetLeafLines(Ntk_Network_t *net,
	     bdd_manager *dd,
	     MlTree *tree,
	     bdd_node **ofuncs,
	     int no,
	     st_table *table,
	     int ni)
{
  int			i, *support;
  char			values[MAX_EQ_LEN];
  bdd_node		*one = bdd_read_one(dd);
  bdd_node		*zero = bdd_read_zero(dd);
  bdd_node		*node;
  TruthTableLine	*line;
  int			pos, sizeZ = bdd_num_zdd_vars(dd);
  char			name[MAX_NAME_LEN];

  line = (TruthTableLine *)NULL;

  if (tree->node == one || tree->node == zero)
    return(line);

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;

  support = ALLOC(int, sizeZ);
  if (!support)
    return(line);
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < sizeZ; i++) {
    if (support[i]) {
      SynthGetPrimaryIndexName(net, i, name);
      if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
	fprintf(vis_stdout,
		"** synth error: Failed to find %s in hash.\n", name);
      }
      support[i] = pos;
    }
  }

  for (i = 0; i < ni; i++)
    values[i] = '-';
  values[ni] = '\0';
  line = GetBlifBinary(line, dd, node, values, support, ni);
  FREE(support);
  return(line);
}


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

  Synopsis    [Gets a list of TruthTableLine for a tree which is a leaf node.]

  Description [Gets a list of TruthTableLine for a tree which is a leaf node.]

  SideEffects []

  SeeAlso     [GetLeafLines]

******************************************************************************/
static TruthTableLine *
GetBlifBinary(TruthTableLine *line,
	      bdd_manager *dd,
	      bdd_node *node,
	      char *values,
	      int *support,
	      int ni)
{
  bdd_node		*one = bdd_read_one(dd);
  bdd_node		*zero = bdd_read_zero(dd);
  TruthTableLine	*new_, *cur;
  int			id = bdd_node_read_index(node);

  if (node == zero)
    return(line);

  if (node == one) {
    new_ = ALLOC(TruthTableLine, 1);
    (void)memset((void *)new_, 0, sizeof(TruthTableLine));
    new_->values = ALLOC(char,ni+1);
    strcpy(new_->values, values);
    if (line) {
      cur = line;
      while (cur->next)
	cur = cur->next;
      cur->next = new_;
    } else
      line = new_;
    return(line);
  }

  if (id % 2 == 0)
    values[support[id]] = '1';
  else
    values[support[id]] = '0';
  line = GetBlifBinary(line, dd, bdd_bdd_T(node), values, support, ni);
  values[support[id]] = '-';
  line = GetBlifBinary(line, dd, bdd_bdd_E(node), values, support, ni);
  values[support[id]] = '-';
  return(line);
}


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

  Synopsis    [Returns the complemented TruthTableLine only for the first one.]

  Description [Returns the complemented TruthTableLine only for the first one.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static TruthTableLine *
GetComplementOneLine(TruthTableLine *line,
		     int ni,
		     int flag)
{
  int			i;
  TruthTableLine	*new_line, *start, *last;

  start = last = (TruthTableLine *)NULL;

  for (i = 0; i < ni; i++) {
    if (line->values[i] != '-') {
      new_line = GetTautologyLine(ni);
      if (line->values[i] == '1')
	new_line->values[i] = '0';
      else
	new_line->values[i] = '1';
      if (last) {
	last->next = new_line;
	last = new_line;
      } else
	start = last = new_line;
    }
  }

  if (flag) {
    FREE(line->values);
    FREE(line);
  }

  return(start);
}


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

  Synopsis    [Returns the complemented TruthTableLine.]

  Description [Returns the complemented TruthTableLine.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static TruthTableLine *
GetComplementLines(TruthTableLine *lines,
		   int ni,
		   int flag)
{
  TruthTableLine	*first, *cur, *next;

  if (!lines)
    return(lines);

  first = lines;
  cur = first->next;
  first = GetComplementOneLine(first, ni, flag);
  while (cur) {
    next = cur->next;
    cur = GetComplementOneLine(cur, ni, flag);
    first = GetAndLines(first, cur, ni, flag);
    cur = next;
  }
  return(first);
}


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

  Synopsis    [Returns the result of Boolean AND for two TruthTableLine.]

  Description [Returns the result of Boolean AND for two TruthTableLine.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static TruthTableLine *
GetAndLines(TruthTableLine *line1,
	    TruthTableLine *line2,
	    int ni,
	    int flag)
{
  int			i;
  TruthTableLine	*cur1, *cur2, *next1, *next2;
  TruthTableLine	*start, *last;
  TruthTableLine	*new_line;

  start = last = (TruthTableLine *)NULL;

  cur1 = line1;
  while (cur1) {
    next1 = cur1->next;
    cur2 = line2;
    while (cur2) {
      new_line = GetTautologyLine(ni);
      strcpy(new_line->values, cur1->values);
      for (i = 0; i < ni; i++) {
	if (cur2->values[i] != '-')
	  new_line->values[i] = cur2->values[i];
      }
      if (last) {
	last->next = new_line;
	last = new_line;
      } else {
	start = last = new_line;
      }
      cur2 = cur2->next;
    }
    if (flag) {
      FREE(cur1->values);
      FREE(cur1);
    }
    cur1 = next1;
  }

  if (flag) {
    cur2 = line2;
    while (cur2) {
      next2 = cur2->next;
      FREE(cur2->values);
      FREE(cur2);
      cur2 = next2;
    }
  }

  return(start);
}


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

  Synopsis    [Returns the node or the complement node of a tree.]

  Description [Returns the node or the complement node of a tree.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static bdd_node	*
GetDdNodeOfMlTree(MlTree *tree,
		  int comp)
{
  if (comp)
    return(tree->complement);
  return(tree->node);
}

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

  Synopsis    [Gets the node name of a tree.]

  Description [Gets the node name of a tree. Return value shows polarity;
  0 means positive node and 1 means negative.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetMlTreeName(Ntk_Network_t *net,
	      bdd_node **ofuncs,
	      MlTree *tree,
	      char *name)
{
  int	i, no;
  int	polarity = 0; /* positive */

  no = Ntk_NetworkReadNumCombOutputs(net) - Ntk_NetworkReadNumLatches(net);
  for (i = 0; i < no; i++) {
    if (tree->node == ofuncs[i]) {
      sprintf(name, "%s", SynthGetIthOutputName(i));
      break;
    }
  }
  if (i == no) {
    if (tree->pi)
      polarity = SynthGetPrimaryNodeName(net, tree->node, name);
    else
      SynthGetInternalNodeName(name, tree->id);
  }

  return(polarity);
}

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

  Synopsis    [Gets the original name of a tree.]

  Description [Gets the original name of a tree.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static char **
GetAllVarNameArray(bdd_manager *dd)
{
  int		size, i, j;
  mvar_type	var;
  char		**nameArray, *name;

  size = bdd_num_vars(dd);
  nameArray = ALLOC(char *, size);
  if (!nameArray)
    return(NIL(char *));

  for (i = 0; i < size; i++) {
    var = mdd_get_var_by_id(dd, i);
    name = ALLOC(char, strlen(var.name) + 1);
    if (!name) {
      for (j = 0; j < i; j++)
	FREE(nameArray[j]);
      FREE(nameArray);
      return(NIL(char *));
    }
    strcpy(name, var.name);
    nameArray[i] = name;
  }
  
  return(nameArray);
}