cuddapi.c

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

******************************************************************************/
DdNode *
Cudd_ReadOne(
  DdManager * dd)
{
    return(dd->one);

} /* end of Cudd_ReadOne */


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

  Synopsis    [Returns the ZDD for the constant 1 function.]

  Description [Returns the ZDD for the constant 1 function.
  The representation of the constant 1 function as a ZDD depends on
  how many variables it (nominally) depends on. The index of the
  topmost variable in the support is given as argument <code>i</code>.]

  SideEffects [None]

  SeeAlso [Cudd_ReadOne]

******************************************************************************/
DdNode *
Cudd_ReadZddOne(
  DdManager * dd,
  int  i)
{
    if (i < 0)
	return(NULL);
    return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));

} /* end of Cudd_ReadZddOne */



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

  Synopsis    [Returns the zero constant of the manager.]

  Description [Returns the zero constant of the manager. The zero
  constant is the arithmetic zero, rather than the logic zero. The
  latter is the complement of the one constant.]

  SideEffects [None]

  SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]

******************************************************************************/
DdNode *
Cudd_ReadZero(
  DdManager * dd)
{
    return(DD_ZERO(dd));

} /* end of Cudd_ReadZero */


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

  Synopsis    [Returns the logic zero constant of the manager.]

  Description [Returns the zero constant of the manager. The logic zero
  constant is the complement of the one constant, and is distinct from
  the arithmetic zero.]

  SideEffects [None]

  SeeAlso [Cudd_ReadOne Cudd_ReadZero]

******************************************************************************/
DdNode *
Cudd_ReadLogicZero(
  DdManager * dd)
{
    return(Cudd_Not(DD_ONE(dd)));

} /* end of Cudd_ReadLogicZero */


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

  Synopsis    [Reads the plus-infinity constant from the manager.]

  Description []

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_ReadPlusInfinity(
  DdManager * dd)
{
    return(dd->plusinfinity);

} /* end of Cudd_ReadPlusInfinity */


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

  Synopsis    [Reads the minus-infinity constant from the manager.]

  Description []

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_ReadMinusInfinity(
  DdManager * dd)
{
    return(dd->minusinfinity);

} /* end of Cudd_ReadMinusInfinity */


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

  Synopsis    [Reads the background constant of the manager.]

  Description []

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_ReadBackground(
  DdManager * dd)
{
    return(dd->background);

} /* end of Cudd_ReadBackground */


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

  Synopsis    [Sets the background constant of the manager.]

  Description [Sets the background constant of the manager. It assumes
  that the DdNode pointer bck is already referenced.]

  SideEffects [None]

******************************************************************************/
void
Cudd_SetBackground(
  DdManager * dd,
  DdNode * bck)
{
    dd->background = bck;

} /* end of Cudd_SetBackground */


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

  Synopsis    [Reads the number of slots in the cache.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheUsedSlots]

******************************************************************************/
unsigned int
Cudd_ReadCacheSlots(
  DdManager * dd)
{
    return(dd->cacheSlots);

} /* end of Cudd_ReadCacheSlots */


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

  Synopsis    [Reads the fraction of used slots in the cache.]

  Description [Reads the fraction of used slots in the cache. The unused
  slots are those in which no valid data is stored. Garbage collection,
  variable reordering, and cache resizing may cause used slots to become
  unused.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheSlots]

******************************************************************************/
double
Cudd_ReadCacheUsedSlots(
  DdManager * dd)
{
    unsigned long used = 0;
    int slots = dd->cacheSlots;
    DdCache *cache = dd->cache;
    int i;

    for (i = 0; i < slots; i++) {
	used += cache[i].h != 0;
    }

    return((double)used / (double) dd->cacheSlots);

} /* end of Cudd_ReadCacheUsedSlots */


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

  Synopsis    [Returns the number of cache look-ups.]

  Description [Returns the number of cache look-ups.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheHits]

******************************************************************************/
double
Cudd_ReadCacheLookUps(
  DdManager * dd)
{
    return(dd->cacheHits + dd->cacheMisses +
	   dd->totCachehits + dd->totCacheMisses);

} /* end of Cudd_ReadCacheLookUps */


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

  Synopsis    [Returns the number of cache hits.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheLookUps]

******************************************************************************/
double
Cudd_ReadCacheHits(
  DdManager * dd)
{
    return(dd->cacheHits + dd->totCachehits);

} /* end of Cudd_ReadCacheHits */


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

  Synopsis    [Returns the number of recursive calls.]

  Description [Returns the number of recursive calls if the package is
  compiled with DD_COUNT defined.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
double
Cudd_ReadRecursiveCalls(
  DdManager * dd)
{
#ifdef DD_COUNT
    return(dd->recursiveCalls);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadRecursiveCalls */



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

  Synopsis    [Reads the hit rate that causes resizinig of the computed
  table.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetMinHit]

******************************************************************************/
unsigned int
Cudd_ReadMinHit(
  DdManager * dd)
{
    /* Internally, the package manipulates the ratio of hits to
    ** misses instead of the ratio of hits to accesses. */
    return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));

} /* end of Cudd_ReadMinHit */


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

  Synopsis    [Sets the hit rate that causes resizinig of the computed
  table.]

  Description [Sets the minHit parameter of the manager. This
  parameter controls the resizing of the computed table. If the hit
  rate is larger than the specified value, and the cache is not
  already too large, then its size is doubled.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMinHit]

******************************************************************************/
void
Cudd_SetMinHit(
  DdManager * dd,
  unsigned int hr)
{
    /* Internally, the package manipulates the ratio of hits to
    ** misses instead of the ratio of hits to accesses. */
    dd->minHit = (double) hr / (100.0 - (double) hr);

} /* end of Cudd_SetMinHit */


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

  Synopsis    [Reads the looseUpTo parameter of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead]

******************************************************************************/
unsigned int
Cudd_ReadLooseUpTo(
  DdManager * dd)
{
    return(dd->looseUpTo);

} /* end of Cudd_ReadLooseUpTo */


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

  Synopsis    [Sets the looseUpTo parameter of the manager.]

  Description [Sets the looseUpTo parameter of the manager. This
  parameter of the manager controls the threshold beyond which no fast
  growth of the unique table is allowed. The threshold is given as a
  number of slots. If the value passed to this function is 0, the
  function determines a suitable value based on the available memory.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadLooseUpTo Cudd_SetMinHit]

******************************************************************************/
void
Cudd_SetLooseUpTo(
  DdManager * dd,
  unsigned int lut)
{
    if (lut == 0) {
	long datalimit = getSoftDataLimit();
	lut = (unsigned int) (datalimit / (sizeof(DdNode) *
					   DD_MAX_LOOSE_FRACTION));
    }
    dd->looseUpTo = lut;

} /* end of Cudd_SetLooseUpTo */


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

  Synopsis    [Returns the soft limit for the cache size.]

  Description [Returns the soft limit for the cache size. The soft limit]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxCache]

******************************************************************************/
unsigned int
Cudd_ReadMaxCache(
  DdManager * dd)
{
    return(2 * dd->cacheSlots + dd->cacheSlack);

} /* end of Cudd_ReadMaxCache */


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

  Synopsis    [Reads the maxCacheHard parameter of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetMaxCacheHard Cudd_ReadMaxCache]

******************************************************************************/
unsigned int
Cudd_ReadMaxCacheHard(
  DdManager * dd)
{
    return(dd->maxCacheHard);

} /* end of Cudd_ReadMaxCache */


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

  Synopsis    [Sets the maxCacheHard parameter of the manager.]

  Description [Sets the maxCacheHard parameter of the manager. The
  cache cannot grow larger than maxCacheHard entries. This parameter
  allows an application to control the trade-off of memory versus
  speed. If the value passed to this function is 0, the function
  determines a suitable maximum cache size based on the available memory.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]

******************************************************************************/
void
Cudd_SetMaxCacheHard(
  DdManager * dd,
  unsigned int mc)
{
    if (mc == 0) {
	long datalimit = getSoftDataLimit();
	mc = (unsigned int) (datalimit / (sizeof(DdCache) *
					  DD_MAX_CACHE_FRACTION));
    }
    dd->maxCacheHard = mc;

} /* end of Cudd_SetMaxCacheHard */


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

  Synopsis    [Returns the number of BDD variables in existance.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadZddSize]

******************************************************************************/
int
Cudd_ReadSize(
  DdManager * dd)
{
    return(dd->size);

} /* end of Cudd_ReadSize */


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

  Synopsis    [Returns the number of ZDD variables in existance.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadSize]

******************************************************************************/