cuddutil.c

主要进行大规模的电路综合

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

  FileName    [cuddUtil.c]

  PackageName [cudd]

  Synopsis    [Utility functions.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_PrintMinterm()
		<li> Cudd_PrintDebug()
		<li> Cudd_DagSize()
		<li> Cudd_EstimateCofactor()
		<li> Cudd_EstimateCofactorSimple()
		<li> Cudd_SharingSize()
		<li> Cudd_CountMinterm()
		<li> Cudd_EpdCountMinterm()
		<li> Cudd_CountPath()
		<li> Cudd_CountPathsToNonZero()
		<li> Cudd_Support()
		<li> Cudd_SupportIndex()
		<li> Cudd_SupportSize()
		<li> Cudd_VectorSupport()
		<li> Cudd_VectorSupportIndex()
		<li> Cudd_VectorSupportSize()
		<li> Cudd_ClassifySupport()
		<li> Cudd_CountLeaves()
		<li> Cudd_bddPickOneCube()
		<li> Cudd_bddPickOneMinterm()
		<li> Cudd_bddPickArbitraryMinterms()
		<li> Cudd_SubsetWithMaskVars()
		<li> Cudd_FirstCube()
		<li> Cudd_NextCube()
		<li> Cudd_bddComputeCube()
		<li> Cudd_addComputeCube()
		<li> Cudd_FirstNode()
		<li> Cudd_NextNode()
		<li> Cudd_GenFree()
		<li> Cudd_IsGenEmpty()
		<li> Cudd_IndicesToCube()
		<li> Cudd_PrintVersion()
		<li> Cudd_AverageDistance()
		<li> Cudd_Random()
		<li> Cudd_Srandom()
		<li> Cudd_Density()
		</ul>
	Internal procedures included in this module:
		<ul>
		<li> cuddP()
		<li> cuddStCountfree()
		<li> cuddCollectNodes()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> dp2()
		<li> ddPrintMintermAux()
		<li> ddDagInt()
		<li> ddCountMintermAux()
		<li> ddEpdCountMintermAux()
		<li> ddCountPathAux()
		<li> ddSupportStep()
		<li> ddClearFlag()
		<li> ddLeavesInt()
		<li> ddPickArbitraryMinterms()
		<li> ddPickRepresentativeCube()
		<li> ddEpdFree()
		</ul>]

  Author      [Fabio Somenzi]

  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 "util.h"
#include "cuddInt.h"

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

/* Random generator constants. */
#define MODULUS1 2147483563
#define LEQA1 40014
#define LEQQ1 53668
#define LEQR1 12211
#define MODULUS2 2147483399
#define LEQA2 40692
#define LEQQ2 52774
#define LEQR2 3791
#define STAB_SIZE 64
#define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

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


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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
#endif

static	DdNode	*background, *zero;

static	long cuddRand = 0;
static	long cuddRand2;
static	long shuffleSelect;
static 	long shuffleTable[STAB_SIZE];

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define bang(f)	((Cudd_IsComplement(f)) ? '!' : ' ')

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

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

static int dp2 ARGS((DdManager *dd, DdNode *f, st_table *t));
static void ddPrintMintermAux ARGS((DdManager *dd, DdNode *node, int *list));
static int ddDagInt ARGS((DdNode *n));
static int cuddEstimateCofactor ARGS((DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr));
static DdNode * cuddUniqueLookup ARGS((DdManager * unique, int  index, DdNode * T, DdNode * E));
static int cuddEstimateCofactorSimple ARGS((DdNode * node, int i));
static double ddCountMintermAux ARGS((DdNode *node, double max, DdHashTable *table));
static int ddEpdCountMintermAux ARGS((DdNode *node, EpDouble *max, EpDouble *epd, st_table *table));
static double ddCountPathAux ARGS((DdNode *node, st_table *table));
static double ddCountPathsToNonZero ARGS((DdNode * N, st_table * table));
static void ddSupportStep ARGS((DdNode *f, int *support));
static void ddClearFlag ARGS((DdNode *f));
static int ddLeavesInt ARGS((DdNode *n));
static int ddPickArbitraryMinterms ARGS((DdManager *dd, DdNode *node, int nvars, int nminterms, char **string));
static int ddPickRepresentativeCube ARGS((DdManager *dd, DdNode *node, int nvars, double *weight, char *string));
static enum st_retval ddEpdFree ARGS((char * key, char * value, char * arg));

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


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


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

  Synopsis    [Prints a disjoint sum of products.]

  Description [Prints a disjoint sum of product cover for the function
  rooted at node. Each product corresponds to a path from node to a
  leaf node different from the logical zero, and different from the
  background value. Uses the package default output file.  Returns 1
  if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_PrintDebug Cudd_bddPrintCover]

******************************************************************************/
int
Cudd_PrintMinterm(
  DdManager * manager,
  DdNode * node)
{
    int		i, *list;

    background = manager->background;
    zero = Cudd_Not(manager->one);
    list = ALLOC(int,manager->size);
    if (list == NULL) {
	manager->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    for (i = 0; i < manager->size; i++) list[i] = 2;
    ddPrintMintermAux(manager,node,list);
    FREE(list);
    return(1);

} /* end of Cudd_PrintMinterm */


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

  Synopsis    [Prints a sum of prime implicants of a BDD.]

  Description [Prints a sum of product cover for an incompletely
  specified function given by a lower bound and an upper bound.  Each
  product is a prime implicant obtained by expanding the product
  corresponding to a path from node to the constant one.  Uses the
  package default output file.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_PrintMinterm]

******************************************************************************/
int
Cudd_bddPrintCover(
  DdManager *dd,
  DdNode *l,
  DdNode *u)
{
    int *array;
    int q, result;
    DdNode *lb;
#ifdef DD_DEBUG
    DdNode *cover;
#endif

    array = ALLOC(int, Cudd_ReadSize(dd));
    if (array == NULL) return(0);
    lb = l;
    cuddRef(lb);
#ifdef DD_DEBUG
    cover = Cudd_ReadLogicZero(dd);
    cuddRef(cover);
#endif
    while (lb != Cudd_ReadLogicZero(dd)) {
	DdNode *implicant, *prime, *tmp;
	int length;
	implicant = Cudd_LargestCube(dd,lb,&length);
	if (implicant == NULL) {
	    Cudd_RecursiveDeref(dd,lb);
	    FREE(array);
	    return(0);
	}
	cuddRef(implicant);
	prime = Cudd_bddMakePrime(dd,implicant,u);
	if (prime == NULL) {
	    Cudd_RecursiveDeref(dd,lb);
	    Cudd_RecursiveDeref(dd,implicant);
	    FREE(array);
	    return(0);
	}
	cuddRef(prime);
	Cudd_RecursiveDeref(dd,implicant);
	tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
	if (tmp == NULL) {
	    Cudd_RecursiveDeref(dd,lb);
	    Cudd_RecursiveDeref(dd,prime);
	    FREE(array);
	    return(0);
	}
	cuddRef(tmp);
	Cudd_RecursiveDeref(dd,lb);
	lb = tmp;
	result = Cudd_BddToCubeArray(dd,prime,array);
	if (result == 0) {
	    Cudd_RecursiveDeref(dd,lb);
	    Cudd_RecursiveDeref(dd,prime);
	    FREE(array);
	    return(0);
	}
	for (q = 0; q < dd->size; q++) {
	    switch (array[q]) {
	    case 0:
		(void) fprintf(dd->out, "0");
		break;
	    case 1:
		(void) fprintf(dd->out, "1");
		break;
	    case 2:
		(void) fprintf(dd->out, "-");
		break;
	    default:
		(void) fprintf(dd->out, "?");
	    }
	}
	(void) fprintf(dd->out, " 1\n");
#ifdef DD_DEBUG
	tmp = Cudd_bddOr(dd,prime,cover);
	if (tmp == NULL) {
	    Cudd_RecursiveDeref(dd,cover);
	    Cudd_RecursiveDeref(dd,lb);
	    Cudd_RecursiveDeref(dd,prime);
	    FREE(array);
	    return(0);
	}
	cuddRef(tmp);
	Cudd_RecursiveDeref(dd,cover);
	cover = tmp;
#endif
	Cudd_RecursiveDeref(dd,prime);
    }
    (void) fprintf(dd->out, "\n");
    Cudd_RecursiveDeref(dd,lb);
    FREE(array);
#ifdef DD_DEBUG
    if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
        Cudd_RecursiveDeref(dd,cover);
        return(0);
    }
    Cudd_RecursiveDeref(dd,cover);
#endif
    return(1);

} /* end of Cudd_bddPrintCover */


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

  Synopsis    [Prints to the standard output a DD and its statistics.]

  Description [Prints to the standard output a DD and its statistics.
  The statistics include the number of nodes, the number of leaves, and
  the number of minterms. (The number of minterms is the number of
  assignments to the variables that cause the function to be different
  from the logical zero (for BDDs) and from the background value (for
  ADDs.) The statistics are printed if pr &gt; 0. Specifically:
  <ul>
  <li> pr = 0 : prints nothing
  <li> pr = 1 : prints counts of nodes and minterms
  <li> pr = 2 : prints counts + disjoint sum of product
  <li> pr = 3 : prints counts + list of nodes
  <li> pr &gt; 3 : prints counts + disjoint sum of product + list of nodes
  </ul>
  For the purpose of counting the number of minterms, the function is
  supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm
  Cudd_PrintMinterm]

******************************************************************************/
int
Cudd_PrintDebug(
  DdManager * dd,
  DdNode * f,
  int  n,
  int  pr)
{
    DdNode *azero, *bzero;
    int	   nodes;
    int	   leaves;
    double minterms;
    int    retval = 1;

    if (f == NULL) {
	(void) fprintf(dd->out,": is the NULL DD\n");
	(void) fflush(dd->out);
	return(0);
    }
    azero = DD_ZERO(dd);
    bzero = Cudd_Not(DD_ONE(dd));
    if ((f == azero || f == bzero) && pr > 0){
       (void) fprintf(dd->out,": is the zero DD\n");
       (void) fflush(dd->out);
       return(1);
    }
    if (pr > 0) {
	nodes = Cudd_DagSize(f);
	if (nodes == CUDD_OUT_OF_MEM) retval = 0;
	leaves = Cudd_CountLeaves(f);
	if (leaves == CUDD_OUT_OF_MEM) retval = 0;
	minterms = Cudd_CountMinterm(dd, f, n);
	if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
	(void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
		       nodes, leaves, minterms);
        if (pr > 2) {
	    if (!cuddP(dd, f)) retval = 0;
	}
	if (pr == 2 || pr > 3) {
	    if (!Cudd_PrintMinterm(dd,f)) retval = 0;
	    (void) fprintf(dd->out,"\n");
	}
        (void) fflush(dd->out);
    }
    return(retval);

} /* end of Cudd_PrintDebug */


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

  Synopsis    [Counts the number of nodes in a DD.]

  Description [Counts the number of nodes in a DD. Returns the number
  of nodes in the graph rooted at node.]

  SideEffects [None]

  SeeAlso     [Cudd_SharingSize Cudd_PrintDebug]

******************************************************************************/
int
Cudd_DagSize(
  DdNode * node)
{
    int	i;	

    i = ddDagInt(Cudd_Regular(node));
    ddClearFlag(Cudd_Regular(node));

    return(i);

} /* end of Cudd_DagSize */


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

  Synopsis    [Estimates the number of nodes in a cofactor of a DD.]

  Description [Estimates the number of nodes in a cofactor of a DD.
  Returns an estimate of the number of nodes in a cofactor of
  the graph rooted at node with respect to the variable whose index is i.
  In case of failure, returns CUDD_OUT_OF_MEM.
  This function uses a refinement of the algorithm of Cabodi et al.
  (ICCAD96). The refinement allows the procedure to account for part
  of the recombination that may occur in the part of the cofactor above
  the cofactoring variable. This procedure does no create any new node.
  It does keep a small table of results; therefore itmay run out of memory.
  If this is a concern, one should use Cudd_EstimateCofactorSimple, which
  is faster, does not allocate any memory, but is less accurate.]

  SideEffects [None]

  SeeAlso     [Cudd_DagSize Cudd_EstimateCofactorSimple]

******************************************************************************/
int
Cudd_EstimateCofactor(
  DdManager *dd /* manager */,
  DdNode * f	/* function */,
  int i		/* index of variable */,
  int phase	/* 1: positive; 0: negative */
  )
{
    int	val;
    DdNode *ptr;
    st_table *table;

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) return(CUDD_OUT_OF_MEM);
    val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
    ddClearFlag(Cudd_Regular(f));
    st_free_table(table);

    return(val);

} /* end of Cudd_EstimateCofactor */


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

  Synopsis    [Estimates the number of nodes in a cofactor of a DD.]

  Description [Estimates the number of nodes in a cofactor of a DD.
  Returns an estimate of the number of nodes in the positive cofactor of
  the graph rooted at node with respect to the variable whose index is i.
  This procedure implements with minor changes the algorithm of Cabodi et al.
  (ICCAD96). It does not allocate any memory, it does not change the
  state of the manager, and it is fast. However, it has been observed to
  overestimate the size of the cofactor by as much as a factor of 2.]

  SideEffects [None]

  SeeAlso     [Cudd_DagSize]

******************************************************************************/
int
Cudd_EstimateCofactorSimple(
  DdNode * node,
  int i)
{
    int	val;	

    val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
    ddClearFlag(Cudd_Regular(node));

    return(val);