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

  FileName    [synthCount.c]

  PackageName [synth]

  Synopsis    [Literal counting 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: synthCount.c,v 1.14 1998/08/31 19:22:12 mooni Exp $";

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


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


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


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

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

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

static int CountMultiLevelFactor(bdd_manager *dd, MlTree *top, MlTree *tree, int ref);
static int GetLiteralCount(bdd_manager *dd, bdd_node *node, int nLiterals);

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


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


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

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

  Synopsis [Counts the number of literals of a MlTree.]

  Description [Counts the number of literals of a MlTree. The argument
  ref controls whether to count shared literals or non-shared. If ref is
  1, it counts shared literals.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
SynthCountMlLiteral(bdd_manager *dd,
		    MlTree *tree,
		    int ref)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		count = 0;

  if (tree->top || tree->shared) {
    if (ref && tree->ref) {
      if (tree->node != zero && tree->node != one)
	count = 1;
      return(count);
    }
    count += CountMultiLevelFactor(dd, tree, tree, ref);
  }

  if (tree->leaf)
    return(count);

  if (tree->q_ref == 0)
    count += SynthCountMlLiteral(dd, tree->q, ref);
  if (tree->d_ref == 0)
    count += SynthCountMlLiteral(dd, tree->d, ref);
  if (tree->r_ref == 0)
    count += SynthCountMlLiteral(dd, tree->r, ref);

  return(count);
}


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

  Synopsis [Makes a bit string for representing the support of a node.]

  Description [Makes a bit string for representing the support of a node.
  It returns the number of support variables of the ZDD node. The
  argument mask is given by caller, which is array of unsigned integer.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
SynthGetSupportMask(bdd_manager *dd,
		    bdd_node *node,
		    unsigned int *mask)
{
  int		i, pos, count;
  int		word, size;
  int		bit, bit_mask;
  int		*support;
  int		zddSize = bdd_num_zdd_vars(dd);

  count = 0;
  word = sizeof(int) * 8;
  size = zddSize / word + 1;

  support = ALLOC(int, zddSize);
  (void)memset((void *)support, 0, sizeof(int) * zddSize);
  (void)memset((void *)mask, 0, size * sizeof(int));
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < zddSize; i++) {
    if (support[i]) {
      pos = i / word;
      bit = i % word;
      bit_mask = 01 << bit;
      mask[pos] |= bit_mask;
      count++;
    }
  }
  FREE(support);
  return(count);
}


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

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

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

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
SynthGetSupportCount(bdd_manager *dd,
		     bdd_node *node)
{
  int		i, count;
  int		*support;
  int		zddSize = bdd_num_zdd_vars(dd);

  count = 0;
  support = ALLOC(int, zddSize);
  (void)memset((void *)support, 0, sizeof(int) * zddSize);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < zddSize; i++) {
    if (support[i])
      count++;
  }
  FREE(support);
  return(count);
}


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

  Synopsis [Finds the support of f.]

  Description [Finds the support of f. Performs a DFS from f. Whenever a node
  is visited, the variable of the node is accumulated in support, and the
  the node is marked not to be visited again. Uses the LSB of the next pointer
  as visited flag.]

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

  SeeAlso     [SynthZddClearFlag]

******************************************************************************/
void
SynthZddSupportStep(bdd_node *f, int *support)
{
  if (bdd_is_constant(f) || bdd_is_complement(bdd_read_next(f))) {
    return;
  }

  support[bdd_node_read_index(f)] = 1;
  SynthZddSupportStep(bdd_bdd_T(f),support);
  SynthZddSupportStep(bdd_regular(bdd_bdd_E(f)),support);
  /* Mark as visited. */
  bdd_set_next(f, bdd_not_bdd_node(bdd_read_next(f)));
  return;
}


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

  Synopsis [Performs a DFS from f, clearing the LSB of the next pointers.]

  Description [Performs a DFS from f, clearing the LSB of the next pointers.]

  SideEffects []

  SeeAlso     [SynthZddSupportStep]

******************************************************************************/
void
SynthZddClearFlag(bdd_node *f)
{
  bdd_node *temp;

  temp = bdd_read_next(f);

  if (!bdd_is_complement(temp)) {
    return;
  }
  /* Clear visited flag. */
  bdd_set_next(f, bdd_regular(temp));
  if (bdd_is_constant(f)) {
    return;
  }
  SynthZddClearFlag(bdd_bdd_T(f));
  SynthZddClearFlag(bdd_regular(bdd_bdd_E(f)));
  return;
}


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

  Synopsis [Counts the number of literals in a ZDD cover.]

  Description [Counts the number of literals in a ZDD cover.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
SynthGetLiteralCount(bdd_manager *dd,
		     bdd_node *node)
{
  return(GetLiteralCount(dd, node, 0));
}


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

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

  Synopsis [Counts the number of literals of a MlTree.]

  Description [Counts the number of literals of a MlTree.]

  SideEffects []

  SeeAlso     [SynthCountMlLiteral]

******************************************************************************/
static int
CountMultiLevelFactor(bdd_manager *dd,
		      MlTree *top,
		      MlTree *tree,
		      int ref)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*f;
  int		i, *support;
  int		count = 0;
  int		sizeZ = bdd_num_zdd_vars(dd);

  if (ref && tree != top && tree->shared)
    return(1);

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

  if (tree->leaf) {
    support = ALLOC(int, sizeZ);
    if (!support)
      return(0);
    (void)memset((void *)support, 0, sizeof(int) * sizeZ);
    SynthZddSupportStep(bdd_regular(tree->node), support);
    SynthZddClearFlag(bdd_regular(tree->node));
    for (i = 0; i < sizeZ; i++) {
      if (support[i])
	count++;
    }
    FREE(support);
    return(count);
  }

  count += CountMultiLevelFactor(dd, top, tree->q, ref);
  count += CountMultiLevelFactor(dd, top, tree->d, ref);
  count += CountMultiLevelFactor(dd, top, tree->r, ref);

  return(count);
}


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

  Synopsis [Recursive procedure of SynthGetLiteralCount.]

  Description [Recursive procedure of SynthGetLiteralCount. Counts the
  number of literals in a ZDD cover. The argument nLiterals is the
  number of literals currently counted.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetLiteralCount(bdd_manager *dd,
		bdd_node *node,
		int nLiterals)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		count = 0;

  if (node == zero)
    return(0);
  if (node == one)
    return(nLiterals);

  count = GetLiteralCount(dd, bdd_bdd_T(node), nLiterals + 1);
  count += GetLiteralCount(dd, bdd_bdd_E(node), nLiterals);

  return(count);
}