src/synth/synthCount.c

Go to the documentation of this file.

#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                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* 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);

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


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

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);
}


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);
}


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);
}


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;
}


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;
}


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


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

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);
}


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);
}