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

  FileName    [synthDiv.c]

  PackageName [synth]

  Synopsis    [Divisor 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: synthDiv.c,v 1.25 2002/09/10 05:50:52 fabio Exp $";

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

#define	MAX_COUNT	100000000 /* just chosen for a very large number */

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


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

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

  Synopsis    [Structure of one BFS item to count variable occurrences.]

  Description [Structure of one BFS item to count variable occurrences.]

  SeeAlso     []

******************************************************************************/
typedef	struct	bfs_item {
  int			reach; /* number of path from top node */
  int			count; /* number of path to constant 1 */
  bdd_node		*node; /* ZDD node */
  struct bfs_item	*next;
} BfsItem;

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

  Synopsis    [Structure for BFS operation to count variable occurrences.]

  Description [Structure for BFS operation to count variable occurrences.]

  SeeAlso     []

******************************************************************************/
typedef	struct	bfs_list {
  struct bfs_item	*item;
  int			child; /* 1 : T, 0 : E */
  struct bfs_list	*next;
} BfsList;


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


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

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

static int FindQuickDivisor(bdd_node *f, bdd_node *one, int *v);

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


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


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

  Synopsis [Finds a divisor that occurs in more than one cube of the ZDD
  graph.]

  Description [Finds a divisor that occurs in more than one cube of the ZDD
  graph. This is done in a greedy manner. It returns a ZDD node.]

  SideEffects []

  SeeAlso     [Synth_ZddLeastDivisor Synth_ZddMostDivisor
  Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]

******************************************************************************/
bdd_node *
Synth_ZddQuickDivisor(bdd_manager *dd,
		      bdd_node *f)
{
  bdd_node	*res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddQuickDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


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

  Synopsis [Finds a divisor that occurs the least frequently (but more
  than once) in the cubes of a cover.]

  Description [Finds a divisor that occurs the least frequently (but more
  than once) in the cubes of a cover. It returns a ZDD node.]

  SideEffects []

  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddMostDivisor
  Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]

******************************************************************************/
bdd_node *
Synth_ZddLeastDivisor(bdd_manager *dd,
		      bdd_node *f)
{
  bdd_node	*res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddLeastDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


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

  Synopsis [Finds a divisor that occurs the most frequently in the cubes
  of a cover.]

  Description [Finds a divisor that occurs the most frequently in the cubes
  of a cover. It returns a ZDD node.]

  SideEffects []

  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddLeastDivisor
  Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]

******************************************************************************/
bdd_node *
Synth_ZddMostDivisor(bdd_manager *dd,
		     bdd_node *f)
{
  bdd_node	*res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddMostDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


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

  Synopsis    [Finds a divisor that is a level-0 cokernel.]

  Description [Finds a divisor that is a level-0 cokernel. It returns a
  ZDD node.]

  SideEffects []

  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddLeastDivisor
  Synth_ZddMostDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]

******************************************************************************/
bdd_node *
Synth_ZddLevelZeroDivisor(bdd_manager *dd,
			  bdd_node *f)
{
  bdd_node	*res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddLevelZeroDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


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

  Synopsis    [Find a divisor whose literals occur in all cubes.]

  Description [Find a divisor whose literals occur in all cubes. It
  returns a ZDD node.]

  SideEffects []

  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddMostDivisor
  Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddLpDivisor]

******************************************************************************/
bdd_node *
Synth_ZddCommonDivisor(bdd_manager *dd,
		       bdd_node *f)
{
  bdd_node	*res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddCommonDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


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

  Synopsis    [Find a good divisor for low power.]

  Description [Find a good divisor for low power. It returns a ZDD
  node.]

  SideEffects []

  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddMostDivisor
  Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor]
******************************************************************************/
bdd_node *
Synth_ZddLpDivisor(bdd_manager *dd,
		   bdd_node *f)
{
  bdd_node	*res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddLpDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


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


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

  Synopsis    [Performs the recursive steps of Synth_ZddQuickDivisor.]

  Description [Performs the recursive steps of Synth_ZddQuickDivisor.
  When FindQuickDivisor fails to find a literal, the function uses as
  backup strategy finding the literal that occurs the least. The reason
  is the following. If a node has more than one parent, then it is
  guaranteed to appear in more than one cube. However, the converse is not
  true.]

  SideEffects []

  SeeAlso     [SynthZddLeastDivisor SynthZddMostDivisor
  SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]

******************************************************************************/
bdd_node *
SynthZddQuickDivisor(bdd_manager *dd,
		     bdd_node *f)
{
  int		i, v;
  int		nvars;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node;
  bdd_node	*tmp;
  int		min_count;

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

  /* Search for a literal appearing in at least two cubes. */
  v = -1;
  FindQuickDivisor(f, one, &v);
  SynthZddClearFlag(f);

  if (v == -1) {
    /* Quick divisor not found by looking at the ZDD graph.
     * Find the literal that occurs the least among those occuring
     * at least twice.
     */
    min_count = MAX_COUNT;
    nvars = bdd_num_zdd_vars(dd);
    count = ALLOC(int, nvars);
    (void)memset((void *)count, 0, sizeof(int) * nvars);
    SynthCountLiteralOccurrence(dd, f, count);
    for (i = 0; i < nvars; i++) {
      if (count[i] > 1 && count[i] < min_count) {
	v = i;
	min_count = count[i];
      }
    }
    FREE(count);
    if (v == -1) {
      /* All literal appear exactly once. We are done. */
      return(f);
    }
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp) {
    bdd_recursive_deref_zdd(dd,node);
    return(NULL);
  }
  bdd_ref(tmp);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddQuickDivisor(dd, tmp);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd,tmp);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp);

  bdd_deref(divisor);
  return(divisor);
}


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

  Synopsis    [Performs the recursive steps of Synth_ZddLeastDivisor.]

  Description [Performs the recursive steps of Synth_ZddLeastDivisor.]

  SideEffects []

  SeeAlso     [SynthZddQuickDivisor SynthZddMostDivisor
  SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]

******************************************************************************/
bdd_node *
SynthZddLeastDivisor(bdd_manager *dd,
		     bdd_node *f)
{
  int		i, v;
  int		nvars, min_count;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node;
  bdd_node	*tmp1;

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

  /* Find the literal that occurs the least among those occuring at
   * least twice.
   */
  v = -1;
  min_count = MAX_COUNT;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > 1 && count[i] < min_count) {
      v = i;
      min_count = count[i];
    }
  }
  FREE(count);

  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node) {
    return(NULL);
  }
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddLeastDivisor(dd, tmp1);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp1);

  bdd_deref(divisor);
  return(divisor);
}


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

  Synopsis    [Performs the recursive steps of Synth_ZddMostDivisor.]

  Description [Performs the recursive steps of Synth_ZddMostDivisor.]

  SideEffects []

  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
  SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]

******************************************************************************/
bdd_node *
SynthZddMostDivisor(bdd_manager *dd,
		    bdd_node *f)
{
  int		i, v;
  int		nvars, max_count;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node;
  bdd_node	*tmp1;

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

  /* Find the literal that occurs the most. */
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
    }
  }

  FREE(count);

  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddMostDivisor(dd, tmp1);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp1);

  bdd_deref(divisor);
  return(divisor);
}


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

  Synopsis    [Performs the recursive steps of Synth_ZddLevelZeroDivisor.]

  Description [Performs the recursive steps of Synth_ZddLevelZeroDivisor.]

  SideEffects []

  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
  SynthZddMostDivisor SynthZddCommonDivisor SynthZddLpDivisor]

******************************************************************************/
bdd_node *
SynthZddLevelZeroDivisor(bdd_manager *dd,
			 bdd_node *f)
{
  int		i, v;
  int		nvars, max_count;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node;
  bdd_node	*tmp1, *tmp2;

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

  /* Find the literal that occurs the most. */
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
    }
  }

  FREE(count);

  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Factor out all literals appearing in all cubes. */
  tmp2 = SynthMakeCubeFree(dd, tmp1);
  if (!tmp2) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(tmp2);
  bdd_recursive_deref_zdd(dd, tmp1);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddLevelZeroDivisor(dd, tmp2);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp2);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp2);

  bdd_deref(divisor);
  return(divisor);
}

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

  Synopsis    [The internal function of Synth_ZddCommonDivisor.]

  Description [The internal function of Synth_ZddCommonDivisor.]

  SideEffects []

  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
  SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddLpDivisor]

******************************************************************************/
bdd_node *
SynthZddCommonDivisor(bdd_manager *dd,
		      bdd_node *f)
{
  int		i;
  int		nvars;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node, *tmp;
  int		nCubes;

  divisor = (bdd_node *)NULL;	/* NULL means no such divisor exists */
  if (f == one || f == zero)
    return(divisor);

  nCubes = bdd_zdd_count(dd, f);
  if (nCubes == 1)
    return(divisor);

  /* Find the literals that appear exactly as many times as there
   * are cubes. These literals appear in all cubes, hence in the
   * common divisor. Their product is accumulated in divisor. */
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] == nCubes) {
      node = bdd_zdd_get_node(dd, i, one, zero);
      if (!node) {
	FREE(count);
	return(NULL);
      }
      bdd_ref(node);
      if (!divisor) {
	divisor = node;
	continue;
      }
      tmp = divisor;
      divisor = (* SynthGetZddProductRecurFunc())(dd, divisor, node);
      if (!divisor) {
	bdd_recursive_deref_zdd(dd, tmp);
	bdd_recursive_deref_zdd(dd, node);
	FREE(count);
	return(NULL);
      }
      bdd_ref(divisor);
      bdd_recursive_deref_zdd(dd, tmp);
      bdd_recursive_deref_zdd(dd, node);
    }
  }
  FREE(count);

  if (divisor)
    bdd_deref(divisor);
  return(divisor);
}


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

  Synopsis    [Performs the recursive steps of Synth_ZddLpDivisor.]

  Description [Performs the recursive steps of Synth_ZddLpDivisor.]

  SideEffects []

  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
  SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddCommonDivisor]

******************************************************************************/
bdd_node *
SynthZddLpDivisor(bdd_manager *dd,
		  bdd_node *f)
{
  int		i, v;
  int		nvars, min_count, min_pos = 0;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node;
  bdd_node	*tmp1;

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

  /* Find the literal that occurs the least among those occuring at
   * least twice.
   */
  v = -1;
  min_count = MAX_COUNT;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);

  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > 1 && count[i] < min_count) {
      v = i;
      min_count = count[i];
      min_pos = i;
    }
  }
  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    FREE(count);
    return(f);
  }

  /* Among the literals with minimum count, find a good one. */
  v = SynthFindDivisorForLowPower(count, nvars, min_count, min_pos);

  FREE(count);

  if (v == -1) {
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddLpDivisor(dd, tmp1);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp1);

  bdd_deref(divisor);
  return(divisor);
}


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

  Synopsis    [Counts the number of occurrences of each variable.]

  Description [Counts the number of occurrences of each variable.
  First, we count the number of paths to the top node for each node from
  top to bottom. Let this number be C_t. Initially, C_t of the top node
  is 1, and C_t of a node is the sum of C_t's of all predecessors of the
  node. Second, we count the number of paths to the constant one node from
  bottom to top. Let this number be C_1. Initially, C_1 of the constant one
  node is 1 and C_1 of the constant zero node is 0, and C_1 of a node is the
  sum of C_1's of two successors of the node. Third, we count the number of
  occurrences of variables using the C_t's and C_1's of each node. Here, let
  C_m of a node be C_t of the node times C_1 of then child of the node.
  The number of occurrences of a variable is determined by summing C_m of all
  nodes that belongs to the variable in the ZDD. The argument count is
  passed by caller, and it is an array of integer to store the number of
  occurrence for each variable, and the size of the array is the number
  of ZDD variables.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthCountLiteralOccurrence(bdd_manager *dd,
			    bdd_node *f,
			    int *count)
{
  BfsItem	**level, *item, *cur_item, *next_item, *last_item;
  BfsList	*list, *pre_list, *cur_list, *next_list, *last_list;
  BfsList	*new_list, *save_last_list;
  int		cur_level, next_level, start_level, last_level;
  int		exist;
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*one = bdd_read_one(dd);
  int		i, ct, ce;
  bdd_node	*node;
  int		lv, *index, id;
  int		sizeZ = bdd_num_zdd_vars(dd);

  if (bdd_is_constant(f))
    return;

  level = ALLOC(BfsItem *, sizeZ);
  (void)memset((void *)level, 0, sizeof(BfsItem *) * sizeZ);
  index = ALLOC(int, sizeZ);
  (void)memset((void *)index, 0, sizeof(int) * sizeZ);

  /* Initialize BFS by entering f in the queue. */
  item = ALLOC(BfsItem, 1);
  (void)memset((void *)item, 0, sizeof(BfsItem));
  item->node = f;
  item->reach = 1;
  lv = bdd_read_zdd_level(dd,bdd_node_read_index(f));
  level[lv] = item;
  index[lv] = bdd_node_read_index(f);
  start_level = last_level = lv;

  if (!bdd_is_constant(bdd_bdd_T(f))) {
    list = ALLOC(BfsList, 1);
    (void)memset((void *)list, 0, sizeof(BfsList));
    list->item = item;
    list->child = 1;
    last_list = list;
  } else
    list = last_list = (BfsList *)NULL;
  if (!bdd_is_constant(bdd_bdd_E(f))) {
    last_list = ALLOC(BfsList, 1);
    (void)memset((void *)last_list, 0, sizeof(BfsList));
    last_list->item = item;
    last_list->child = 0;
    if (list)
      list->next = last_list;
    else
      list = last_list;
  }

  /* Perform the BFS. */
  while (list) {
    cur_level = sizeZ;
    cur_list = list;
    while (cur_list) {
      if (cur_list->child)
	id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
      else
	id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
      next_level = bdd_read_zdd_level(dd,id);
      cur_level = (cur_level < next_level) ? cur_level : next_level;
      cur_list = cur_list->next;
    }
    last_level = cur_level;
    save_last_list = last_list;

    pre_list = (BfsList *)NULL;
    cur_list = list;
    while (cur_list) {
      if (cur_list->child)
	id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
      else
	id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
      next_level = bdd_read_zdd_level(dd,id);

      if (next_level != cur_level) {
	pre_list = cur_list;
	cur_list = cur_list->next;
	continue;
      }

      if (cur_list->child)
	node = bdd_bdd_T(cur_list->item->node);
      else
	node = bdd_bdd_E(cur_list->item->node);

      exist = 0;
      last_item = level[cur_level];
      while (last_item) {
	if (node == last_item->node) {
	  last_item->reach += cur_list->item->reach;
	  exist = 1;
	  break;
	}
	if (last_item->next)
	  last_item = last_item->next;
	else
	  break;
      }

      if (exist == 0) {
	item = ALLOC(BfsItem, 1);
	(void)memset((void *)item, 0, sizeof(BfsItem));
	item->node = node;
	item->reach = cur_list->item->reach;
	if (last_item)
	  last_item->next = item;
	else {
	  level[cur_level] = item;
	  index[cur_level] = id;
	}

	if (!bdd_is_constant(bdd_bdd_T(node))) {
	  new_list = ALLOC(BfsList, 1);
	  (void)memset((void *)new_list, 0, sizeof(BfsList));
	  new_list->item = item;
	  new_list->child = 1;
	  last_list->next = new_list;
	  last_list = new_list;
	}
	if (!bdd_is_constant(bdd_bdd_E(node))) {
	  new_list = ALLOC(BfsList, 1);
	  (void)memset((void *)new_list, 0, sizeof(BfsList));
	  new_list->item = item;
	  new_list->child = 0;
	  last_list->next = new_list;
	  last_list = new_list;
	}
      }

      next_list = cur_list->next;
      if (cur_list == list && cur_list == last_list) {
	FREE(cur_list);
	list = next_list;
      } else if (cur_list == list) {
	FREE(cur_list);
	pre_list = (BfsList *)NULL;
	if (list == save_last_list) {
	  list = next_list;
	  next_list = (BfsList *)NULL;
	} else
	  list = next_list;
      } else if (cur_list == last_list) {
	if (pre_list)
	  pre_list->next = cur_list->next;
	FREE(cur_list);
	last_list = pre_list;
      } else {
	if (pre_list)
	  pre_list->next = cur_list->next;
	if (cur_list == save_last_list) {
	  FREE(cur_list);
	  next_list = (BfsList *)NULL;
	} else
	  FREE(cur_list);
      }

      cur_list = next_list;
    }
  }

  /* Compute the number of paths to the constant 1 for each node in
   * bottom up fashion. Update the occurrence count of the variables.
   */
  for (i = last_level; i >= start_level; i--) {
    item = level[i];
    while (item) {
      ct = ce = 0;
      if (bdd_bdd_T(item->node) == one)
	ct = 1;
      else {
	node = bdd_bdd_T(item->node);
	next_level = bdd_read_zdd_level(dd, bdd_node_read_index(node));
	cur_item = level[next_level];
	while (cur_item) {
	  if (cur_item->node == node) {
	    ct = cur_item->count;
	    break;
	  }
	  cur_item = cur_item->next;
	}
      }
      if (bdd_bdd_E(item->node) != zero) {
	node = bdd_bdd_E(item->node);
	next_level = bdd_read_zdd_level(dd,
					bdd_node_read_index(node));
	cur_item = level[next_level];
	while (cur_item) {
	  if (cur_item->node == node) {
	    ce = cur_item->count;
	    break;
	  }
	  cur_item = cur_item->next;
	}
      }
      item->count = ct + ce;
      count[index[i]] += ct * item->reach;
      item = item->next;
    }
  }

  /* Clean up. */
  for (i = last_level; i >= start_level; i--) {
    item = level[i];
    while (item) {
      next_item = item->next;
      FREE(item);
      item = next_item;
    }
  }

  FREE(level);
  FREE(index);
}


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


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

  Synopsis [Finds a ZDD node that is referred by more than one parent
  node in a function.]

  Description [Finds a ZDD node that is referred by more than one parent
  node in a function. Performs a DFS from f. Whenever a node is visited,
  the node is marked. When a node is visited, if the node is already marked,
  it returns the index of the node. Uses the LSB of the next pointer as
  visited flag. This function returns the number of path to constant 1 from
  the node, and return value -1 means already found.]

  SideEffects [Once this function is called, SynthZddClearFlag() should
  be called right after.];

  SeeAlso     [SynthZddClearFlag]

******************************************************************************/
static int
FindQuickDivisor(bdd_node *f,
		 bdd_node *one,
		 int *v)
{
  int		c, ct, ce;
  bdd_node	*temp = bdd_read_next(f);

  if (bdd_is_constant(f)) {
    if (f == one)
      return(1);
    else
      return(0);
  }

  if (bdd_is_complement(temp)) { /* already visited */
    *v = bdd_node_read_index(f);
    return(-1);
  }
  /* mark as visited */
  bdd_set_next(f, bdd_not_bdd_node(temp));

  ct = FindQuickDivisor(bdd_bdd_T(f), one, v);
  if (ct == -1) /* already found */
    return(-1);
  else if (ct > 1) {
    *v = bdd_node_read_index(f);
    return(-1);
  }

  ce = FindQuickDivisor(bdd_bdd_E(f), one, v);
  if (ce == -1) /* already found */
    return(-1);

  /* Add the number of path to constant 1 from two children nodes. */
  c = ct + ce;
  return(c);
}