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

  FileName    [synthOpt.c]

  PackageName [synth]

  Synopsis    [Multilevel optimization functions.]

  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: synthOpt.c,v 1.53 2005/05/11 20:18:25 hhhan Exp $";

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


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


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


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

int	OutputOrdering = 1; /*
			    ** 0 : just use VIS's order
			    ** 1 : smaller first in terms of support
			    ** 2 : smaller first in terms of bdd size
			    */

static	int	UseFuncDivisor = 1;
static	float	SuppFactor = 10.0;
static	float	ProbFactor = 10.0;
static	int	*SupportCount;
static	float	*Probability;
static	char	**outputNames;

extern	int	TryNodeSharing;
extern	int	noMemoryFlag;
extern	int	VerifyTreeMode;

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

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

static void GetOutputOrder(bdd_manager *dd, bdd_node **ofuncs, int no, int *order, int verbosity);
static int IsSubsetOfSupportForOneWord(unsigned int mask1, unsigned int mask2);
static int IsNullSupport(int size, unsigned int *mask);
static void PrintSupportMask(int n, int size, unsigned int *mask);
static int GetNumberOfSupport(int n, int size, unsigned int *mask);
static int factorizeNetwork(Ntk_Network_t *net, bdd_manager *dd, bdd_node **ofuncs, MlTree **tree, int no, int *out_order, st_table *table, char **combOutNames, int divisor, MlTree *(* factoring_func)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int), int verbosity);

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


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


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

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

  Synopsis [Optimizes a network by factorizing.]

  Description [Optimizes a network by factorizing.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthMultiLevelOptimize(Ntk_Network_t *network,
			bdd_node **combOutBdds,
			bdd_node **combUpperBdds,
			char **combOutNames,
			int *initStates,
			Synth_InfoData_t *synthInfo,
			int verbosity)
{
  bdd_manager		*dd = (bdd_manager *)Ntk_NetworkReadMddManager(network);
  bdd_node		*top;
  bdd_node		**ofuncs;
  int			i, no;
  int			factoring, divisor;
  char			*filename;
  char			*filehead;
  MlTree		**tree;
  bdd_node		*zdd_I;
  st_table		*table;
  int			nml, tml;
  int			*out_order;
  FILE			*feqn;
  MlTree		*(* factoring_func)(bdd_manager *, st_table *,
					    bdd_node *, int, int *, MlTree *,
					    int, MlTree *, int);
  int			autoDyn, autoDynZ;
  bdd_reorder_type_t	method, methodZ;
  int			error;

  factoring = synthInfo->factoring;
  divisor = synthInfo->divisor;
  filehead = synthInfo->filehead;
  TryNodeSharing = synthInfo->trySharing;
  SynthSetInternalNodePrefix(synthInfo->prefix);

  /* Save reordering status and set reordering mode specific to
   * synthesis.
   */
  autoDyn = bdd_reordering_status(dd, &method);
  autoDynZ = bdd_reordering_zdd_status(dd, &methodZ);

  switch (synthInfo->reordering) {
  case 0 :
    bdd_dynamic_reordering_disable(dd);
    bdd_dynamic_reordering_zdd_disable(dd);
    break;
  case 1 :
    bdd_dynamic_reordering(dd, method, BDD_REORDER_VERBOSITY_DEFAULT);
    bdd_dynamic_reordering_zdd_disable(dd);
    break;
  case 2 :
    bdd_dynamic_reordering_disable(dd);
    bdd_dynamic_reordering_zdd(dd, methodZ, BDD_REORDER_VERBOSITY_DEFAULT);
    break;
  case 3 :
    bdd_dynamic_reordering(dd, method, BDD_REORDER_VERBOSITY_DEFAULT);
    bdd_dynamic_reordering_zdd(dd, methodZ, BDD_REORDER_VERBOSITY_DEFAULT);
    break;
  default :
    bdd_dynamic_reordering_disable(dd);
    bdd_dynamic_reordering_zdd_disable(dd);
    break;
  }

  if (factoring == 0)
    factoring_func = SynthSimpleFactorTree;
  else
    factoring_func = SynthGenericFactorTree;

  /* outputNames is a static global variable for this file. */
  outputNames = combOutNames;

  /* Initialize the node-tree table and other factoring-related variables.
   * The table contains pairs of a ZDD node and the corresponding multi-level
   * tree.
   */
  table = st_init_table(st_ptrcmp, st_ptrhash);
  SynthInitMlTable();

  /* Create ZDD variables for the positive and negative literals. */
  bdd_zdd_vars_from_bdd_vars(dd, 2);

  /* Since we currently support only blif files, the number of
   * functions to synthesize should not include the initial
   * inputs of latches in case of sequential ckts.
   */
  no = Ntk_NetworkReadNumCombOutputs(network) -
    Ntk_NetworkReadNumLatches(network);

  /* Compute two-level covers for all the functions to be synthesized. */
  ofuncs = ALLOC(bdd_node *, no);
  for (i = 0; i < no; i++) {
    if (verbosity) {
      (void)fprintf(vis_stdout, "** synth info: Synthesizing output [%d(%s)]\n",
		    i, combOutNames[i]);
    }
    bdd_ref(top = bdd_zdd_isop(dd, combOutBdds[i], combUpperBdds[i],
			       &zdd_I));
    bdd_ref(zdd_I);
    bdd_recursive_deref(dd, top);
    ofuncs[i] = zdd_I;
  }

  if (VerifyTreeMode == 2)
    SynthDumpBlif(network, dd, no, ofuncs, combOutNames, initStates, filehead);

  /* Initialize array of factoring trees and determine the order in
   * which the functions will be processed. Then proceed to factor.
   */
  tree = ALLOC(MlTree *, no);
  (void)memset((void *)tree, 0, no * sizeof(MlTree *));
  out_order = ALLOC(int, no);
  GetOutputOrder(dd, ofuncs, no, out_order, verbosity);
  error = factorizeNetwork(network, dd, ofuncs, tree, no, out_order,
		   table, combOutNames, divisor, factoring_func, verbosity);
  FREE(out_order);

  if (error) {
    (void)fprintf(vis_stderr,
		  "** synth error: synthesize_network has finished abnormally");
    if (noMemoryFlag)
      (void)fprintf(vis_stderr, " due to lack of memory\n");
    else
      (void)fprintf(vis_stderr, " for some reason\n");
    goto cleanup;
  }

  /* Count total number of literals in multi-level network. */
  tml = 0;
  for (i = 0; i < no; i++) {
    if (tree[i]) {
      nml = SynthCountMlLiteral(dd, tree[i], 1);
      tml += nml;
    }
  }
  (void)fprintf(vis_stdout,
		"** synth info: Total number of literals = %d\n", tml);

  /* Write network in eqn and blif formats. */
  SynthSetupNodeNameTable(network);
  filename = ALLOC(char, strlen(filehead) + 9);
  if (synthInfo->eqn) {
    sprintf(filename, "%s.eqn", filehead);
    feqn = Cmd_FileOpen(filename, "w", NIL(char *), 0);
    if (feqn) {
      fprintf(feqn, "** synth info: Total number of literals = %d\n", tml);
      SynthWriteEqnHeader(feqn, network, dd);
      for (i = 0; i < no; i++) {
	if (tree[i])
	  SynthWriteEqn(feqn, network, dd, tree[i], ofuncs, combOutNames[i], 1);
      }
      fclose(feqn);
    } else {
      (void)fprintf(vis_stdout,
		    "** synth error: Error in opening file [%s]\n", filename);
    }
  }
  sprintf(filename, "%s.ml.blif", filehead);
  SynthWriteBlifFile(network, dd, tree, filename, no, ofuncs, initStates,
		     0, verbosity);
  FREE(filename);
  SynthFreeNodeNameTable();

 cleanup:
  /* Clean up. */
  for (i = 0; i < no; i++) {
    if (!tree[i])
      continue;
    bdd_recursive_deref_zdd(dd, tree[i]->node);
    /* frees some trees not in node-tree table */
    if (tree[i]->ref)
      SynthFreeMlTree(tree[i], 0);
  }

  SynthClearMlTable(dd, table);
  st_free_table(table);
  FREE(tree);

  for (i = 0; i < no; i++) {
    if (!ofuncs[i])
      continue;
    bdd_recursive_deref_zdd(dd, ofuncs[i]);
  }

  FREE(ofuncs);

  /* Restore reordering status. */
  if (autoDyn)
    bdd_dynamic_reordering(dd, method, BDD_REORDER_VERBOSITY_DEFAULT);
  else
    bdd_dynamic_reordering_disable(dd);
  if (autoDynZ)
    bdd_dynamic_reordering_zdd(dd, methodZ, BDD_REORDER_VERBOSITY_DEFAULT);
  else
    bdd_dynamic_reordering_zdd_disable(dd);
}


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

  Synopsis [Sets the optional variable UseFuncDivisor.]

  Description [Sets the optional variable UseFuncDivisor. Currently
  UseFuncDivisor has always the initial value of 1, this is because it
  seems does better almost always than 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthSetUseFuncDivisor(int mode)
{
  UseFuncDivisor = mode;
}


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

  Synopsis [Sets the optional variable OutputOrdering.]

  Description [Sets the optional variable OutputOrdering.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthSetOutputOrdering(int mode)
{
  OutputOrdering = mode;
}


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

  Synopsis [Sets the cost factors to get a divisor for low power.]

  Description [Sets the cost factors to get a divisor for low power.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthSetCostFactors(float supp,
		    float prob)
{
  SuppFactor = supp;
  ProbFactor = prob;
}


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

  Synopsis [Sets the variable SupportCount.]

  Description [Sets the variable SupportCount.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthSetSupportCount(int *count)
{
  SupportCount = count;
}


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

  Synopsis [Sets the variable Probability.]

  Description [Sets the variable Probability.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthSetProbability(float *prob)
{
  Probability = prob;
}


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

  Synopsis [Finds a good divisor for low power.]

  Description [Finds a good divisor for low power.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
SynthFindDivisorForLowPower(int	*count,
			    int	nvars,
			    int	min_count,
			    int	min_pos)
{
  int	i, v;
  float	cost, best;

  if ((!SupportCount) || (!Probability))
    return(-1);

  v = min_pos;
  if (SuppFactor == 0.0 && ProbFactor == 0.0)
    best = (float)SupportCount[min_pos] * Probability[min_pos];
  else {
    best = (float)SupportCount[min_pos] * SuppFactor +
      Probability[min_pos] * ProbFactor;
  }

  for (i = min_pos + 1; i < nvars; i++) {
    if (count[i] == min_count) {
      if (SuppFactor == 0.0 && ProbFactor == 0.0)
	cost = (float)SupportCount[i] * Probability[i];
      else {
	cost = (float)SupportCount[i] * SuppFactor +
	  Probability[i] * ProbFactor;
      }
      if (cost > best) {
	best = cost;
	v = i;
      }
    }
  }

  return(v);
}


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

  Synopsis [Returns the i-th output name.]

  Description [Returns the i-th output name.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
SynthGetIthOutputName(int i)
{
  return outputNames[i];
}


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

  Synopsis    [Checks whether one support set is a subset of the other
  support set.]

  Description [Checks whether one support set is a subset of the other
  support set. A support set is represented by a bit-vector. If the
  index 0 variable of a unique table is in the support of a function,
  then the MSB bit is set to 1. In general, for the variable of index
  i, the i-th bit from the MSB is set to 1. The argument size means
  the number of words (word = sizeof(int)). If the sets are the same,
  SynthIsSubsetOfSupport returns 2. If the first set is a subset of
  the second, it returns 1, otherwise it returns 0.]

  SideEffects []

  SeeAlso     [IsSubsetOfSupportForOneWord IsNullSupport]

******************************************************************************/
int
SynthIsSubsetOfSupport(int size,
		       unsigned int *mask1,
		       unsigned int *mask2)
{
  int	i, tmp, flag = 0;

  if (!mask2)
    return(1);

  if (IsNullSupport(size, mask1) && IsNullSupport(size, mask2))
    return(0);
  else if (IsNullSupport(size, mask1))
    return(0);
  else if (IsNullSupport(size, mask2))
    return(1);

  for (i = 0; i < size; i++) {
    tmp = IsSubsetOfSupportForOneWord(mask1[i], mask2[i]);
    if (tmp == 0)
      return(0);
    flag |= tmp;
  }

  return(flag);
}


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

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

  Synopsis [This function orders the output functions. With this
  output ordering, the lowest indexed output function is factorized
  first.]

  Description [This function orders the output functions. With this
  output ordering, the lowest indexed output function is factorized
  first. If OutputOrder is 0, the output order is just the same as the
  order VIS has. If OutputOrder is 1, the smallest function (in terms
  of the number of support variables) will be placed first in the
  order. In case of tie, the function with the smaller BDD is placed
  before the other in the order. If OutputOrder is 2, the smallest
  function in terms of BDD size is first.]

  SideEffects []

  SeeAlso     [SynthMultiLevelOptimize]

******************************************************************************/
static void
GetOutputOrder(bdd_manager *dd,
	       bdd_node **ofuncs,
	       int no,
	       int *order,
	       int verbosity)
{
  int		i, j, k, flag;
  int		*support, *bddsize;
  int		size;
  unsigned int	**mask;
  int		word, sizeZ;
  int		pos, bit, bit_mask;
  int		insert_flag, s1, s2;

  if (no == 1) {
    order[0] = 0;
    return;
  }

  if (OutputOrdering == 0) {
    for (i = 0; i < no; i++)
      order[i] = i;
    return;
  }

  bddsize = ALLOC(int, no);
  if (OutputOrdering == 2) {
    for (i = 0; i < no; i++) {
      if (!ofuncs[i]) {
	order[i] = i;
	bddsize[i] = 0;
	continue;
      }

      bddsize[i] = bdd_node_size(ofuncs[i]);

      /* Insert i-th output at the right place in the order. */
      for (j = 0; j < i; j++) {
	if (bddsize[i] < bddsize[order[j]]) {
	  for (k = i; k > j; k--)
	    order[k] = order[k - 1];
	  order[j] = i;
	  break;
	}
      }

      if (j == i)
	order[i] = i;
    }

    if (verbosity) {
      fprintf(vis_stdout, "output order :");
      for (i = 0; i < no; i++)
	fprintf(vis_stdout, " %d", order[i]);
      fprintf(vis_stdout, "\n");
      if (verbosity > 1) {
	for (i = 0; i < no; i++)
	  fprintf(vis_stdout, "%d - %d", i, bddsize[i]);
      }
    }

    FREE(bddsize);
    return;
  }

  /* Here OutputOrdering should be 1. */
  mask = ALLOC(unsigned int *, no);
  sizeZ = bdd_num_zdd_vars(dd);
  support = ALLOC(int, sizeZ);
  word = sizeof(int) * 8;
  size = sizeZ / word + 1;

  for (i = 0; i < no; i++) {
    if (!ofuncs[i]) {
      mask[i] = (unsigned int *)NULL;
      order[i] = i;
      bddsize[i] = 0;
      continue;
    }

    mask[i] = ALLOC(unsigned int, size);
    (void)memset((void *)mask[i], 0, size * sizeof(int));
    (void)memset((void *)support, 0, sizeof(int) * sizeZ);
    SynthZddSupportStep(bdd_regular(ofuncs[i]), support);
    SynthZddClearFlag(bdd_regular(ofuncs[i]));
    /* Pack the support array into a bit vector. */
    for (j = 0; j < sizeZ; j++) {
      if (support[j]) {
	pos = j / word;
	bit = j % word;
	bit_mask = 01 << bit;
	mask[i][pos] |= bit_mask;
      }
    }
    bddsize[i] = bdd_node_size(ofuncs[i]);

    for (j = 0; j < i; j++) {
      insert_flag = 0;
      flag = SynthIsSubsetOfSupport(size, mask[i], mask[order[j]]);
      if (flag == 1)
	insert_flag = 1;
      else if (flag == 2) {
	s1 = GetNumberOfSupport(sizeZ, size, mask[i]);
	s2 = GetNumberOfSupport(sizeZ, size, mask[order[j]]);
	if (s1 < s2 || (s1 == s2 && bddsize[i] < bddsize[order[j]]))
	  insert_flag = 1;
      }
      if (insert_flag) {
	for (k = i; k > j; k--)
	  order[k] = order[k - 1];
	order[j] = i;
	break;
      }
    }

    if (j == i)
      order[i] = i;
  }
  FREE(support);
  FREE(bddsize);

  if (verbosity) {
    fprintf(vis_stdout, "output order :");
    for (i = 0; i < no; i++)
      fprintf(vis_stdout, " %d", order[i]);
    fprintf(vis_stdout, "\n");
    if (verbosity > 1) {
      for (i = 0; i < no; i++) {
	if (mask[i])
	  PrintSupportMask(sizeZ, size, mask[i]);
      }
    }
  }

  for (i = 0; i < no; i++) {
    if (mask[i])
      FREE(mask[i]);
  }
  FREE(mask);
}


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

  Synopsis [Checks whether a set of support for one word is subset of the
  other set of support for one word.]

  Description [Checks whether a set of support for one word is subset of
  the other set of support for one word. SynthIsSubsetOfSupport() calls
  this function for each word.]

  SideEffects []

  SeeAlso     [SynthIsSubsetOfSupport]

******************************************************************************/
static int
IsSubsetOfSupportForOneWord(unsigned int mask1,
			    unsigned int mask2)
{
  unsigned int	tmp;

  if (mask1 == mask2)
    return(2);

  tmp = mask1 | mask2;
  if (tmp != mask2)
    return(0);
  return(1);
}


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

  Synopsis [Checks if a support set is empty.]

  Description [Checks if a support set is empty.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
IsNullSupport(int size,
	      unsigned int *mask)
{
  int	i;

  for (i = 0; i < size; i++) {
    if (mask[i] != 0)
      return(0);
  }
  return(1);
}


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

  Synopsis [Prints the support of a function.]

  Description [Prints the support of a function. The argument n is the
  number of variables and size is the number of word and mask is the
  array of support mask. The first line shows column index by modulo 10
  and the next line shows which variables are support by printing 1.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
PrintSupportMask(int n,
		 int size,
		 unsigned int *mask)
{
  int	i, j, pos, last;
  char	*support;
  char	*mark;
  int	bit;

  support = ALLOC(char,n);
  mark = ALLOC(char,n);

  pos = 0;
  for (i = 0; i < size; i++) {
    if (i == (size - 1))
      last = n % 32;
    else
      last = 32;
    bit = 01;
    for (j = 0; j < last; j++) {
      sprintf(&mark[pos], "%d", pos % 10);
      if (mask[i] & bit)
	support[pos] = '1';
      else
	support[pos] = '0';
      pos++;
      bit = bit << 1;
    }
  }
  mark[pos] = support[pos] = '\0';

  fprintf(vis_stdout, "%s\n", mark);
  fprintf(vis_stdout, "%s\n", support);

  FREE(support);
  FREE(mark);
}


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

  Synopsis [Returns the number of support variables of a function.]

  Description [Returns the number of support variables of a function.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
GetNumberOfSupport(int n,
		   int size,
		   unsigned int *mask)
{
  int	i, j, last;
  int	bit;
  int	count;

  count = 0;
  for (i = 0; i < size; i++) {
    if (i == (size - 1))
      last = n % 32;
    else
      last = 32;
    bit = 01;
    for (j = 0; j < last; j++) {
      if (mask[i] & bit)
	count++;
      bit = bit << 1;
    }
  }
  return(count);
}


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

  Synopsis [Factorizes a network.]

  Description [Factorizes a network. If successful, it returns 0,
  otherwise it returns 1 due to lack of memory.] 

  SideEffects []

  SeeAlso     [SynthMultiLevelOptimize]

******************************************************************************/
static int
factorizeNetwork(Ntk_Network_t *net,
		 bdd_manager *dd,
		 bdd_node **ofuncs,
		 MlTree **tree,
		 int no,
		 int *out_order,
		 st_table *table,
		 char **combOutNames,
		 int divisor,
		 MlTree *(* factoring_func)(bdd_manager *, st_table *,
					    bdd_node *, int, int *, MlTree *,
					    int, MlTree *, int),
		 int verbosity)
{
  int		i, j, k;
  int		ref;
  int		nml;
  MlTree	*tmp_tree;
  int		flag;
  int		comp_flag;

  SynthSetZddDivisorFunc(divisor); /* set static variable in synthFactor.c */

  for (k = 0; k < no; k++) {
    i = out_order[k];
    if (!ofuncs[i]) {
      tree[i] = NULL;
      continue;
    }
    if (verbosity)
      SynthPrintZddCoverWithName(net, dd, ofuncs[i]);

    tree[i] = (MlTree *)NULL;
    ref = 0;
    if (ofuncs[i] == bdd_read_one(dd) || ofuncs[i] == bdd_read_zero(dd)) {
      tree[i] = SynthFindOrCreateMlTree(table, dd, ofuncs[i], 1, 0,
					&ref, verbosity);
      if (!tree[i])
	return(1);
    } else {
      tree[i] = SynthLookupMlTable(table, dd, ofuncs[i], 1, verbosity);
      if (tree[i]) {
	if (MlTree_IsComplement(tree[i]) || tree[i]->top)
	  ref = 1;
	else
	  SynthUpdateRefOfParent(tree[i]);
      }
      else if (UseFuncDivisor) {
	/* Try to divide by existing functions. The smaller
	 * functions are factored first to increase the probability
	 * of success of this step. Both phases of the divisor are
	 * tried.
	 */
	for (j = k - 1; j >= 0; j--) {
	  tree[i] = (* factoring_func)(dd, table, ofuncs[i], 0, &ref,
				       tree[out_order[j]], 0, NULL, verbosity);
	  if (tree[i]) {
	    SynthSetSharedFlag(dd, tree[out_order[j]]);
	    break;
	  } else if (noMemoryFlag == 1)
	    return(1);
	  else {
	    tree[i] = (* factoring_func)(dd, table, ofuncs[i], 0,
				 &ref, tree[out_order[j]], 1, NULL, verbosity);
	    if (tree[i]) {
	      SynthSetSharedFlag(dd, tree[out_order[j]]);
	      break;
	    } else if (noMemoryFlag == 1)
	      return(1);
	  }
	}
      }
    }
    /* Division by other functions did not work. Find a brand-new
     * factorization.
     */
    if (!tree[i]) {
      tree[i] = (* factoring_func)(dd, table, ofuncs[i], 0,
				   &ref, NULL, 0, NULL, verbosity);
      if (!tree[i])
	return(1);
    }
    /* Compute the complement ZDD node of ofuncs[i], if not exist.
     * This is to increase sharing.
     */
    tmp_tree = tree[i];
    tree[i] = SynthCheckAndMakeComplement(dd, table, tree[i], &comp_flag,
					  verbosity);
    if (!tree[i])
      return(1);
    else if (tree[i] != tmp_tree) {
      ref = 1;
      if (comp_flag)
	tree[i] = MlTree_Not(tree[i]);
    }

    /* When the tree already exists, create a new tree and copy all
     * contents, and set the field 'ref' to 1. This is for the
     * purpose of avoiding duplicate literal counting.
     */
    if (ref) {
      int	comp_flag;

      comp_flag = 0;
      if (MlTree_IsComplement(tree[i])) {
	tree[i] = MlTree_Not(tree[i]);
	comp_flag = 1;
      }
      tmp_tree = ALLOC(MlTree, sizeof(MlTree));
      memcpy((void *)tmp_tree, (void *)tree[i], sizeof(MlTree));
      tree[i] = tmp_tree;
      tree[i]->ref = 1;
      tree[i]->comp = comp_flag;
    }
    tree[i]->top = 1;
    bdd_ref(tree[i]->node);

    nml = SynthCountMlLiteral(dd, tree[i], 1);

    if (verbosity) {
      SynthPrintMlTreeWithName(net, dd, tree[i], "result : ");
      fprintf(vis_stdout, "**** %d (#literal = %d) ****\n", i, nml);
      if (verbosity > 1)
	SynthWriteEqn(stdout, net, dd, tree[i], ofuncs, combOutNames[i], 1);
    }

    if (VerifyTreeMode) {
      SynthVerifyTree(dd, tree[i], 1);
      SynthVerifyMlTable(dd, table);
    }
  }

  flag = SynthPostFactoring(dd, table, factoring_func, verbosity);

  if (VerifyTreeMode) {
    bdd_node *tmp;

    for (i = 0; i < no; i++) {
      if (tree[i]->comp)
	tmp = tree[i]->complement;
      else
	tmp = tree[i]->node;
      if (tmp != ofuncs[i]) {
	(void) fprintf(vis_stdout,
		       "** synth error: Different zdds in [%s].\n",
		       combOutNames[i]);
      }
      SynthVerifyTree(dd, tree[i], 1);
    }
  }

  return(flag);
}