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

  FileName    [cuddCache.c]

  PackageName [cudd]

  Synopsis    [Functions for cache insertion and lookup.]

  Description [Internal procedures included in this module:
		<ul>
		<li> cuddInitCache()
		<li> cuddCacheInsert()
		<li> cuddCacheInsert2()
		<li> cuddCacheLookup()
		<li> cuddCacheLookupZdd()
		<li> cuddCacheLookup2()
		<li> cuddCacheLookup2Zdd()
		<li> cuddConstantLookup()
		<li> cuddCacheProfile()
		<li> cuddCacheResize()
		<li> cuddCacheFlush()
		<li> cuddComputeFloorLog2()
		</ul>
	    Static procedures included in this module:
		<ul>
		</ul> ]

  SeeAlso     []

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

#ifdef DD_CACHE_PROFILE
#define DD_HYSTO_BINS 8
#endif

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


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


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

#ifndef lint
static char rcsid[] DD_UNUSED =
	"$Id: cuddCache.c,v 1.31 2001/03/20 18:42:26 fabio Exp $";
#endif

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


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

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


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


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

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


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

  Synopsis    [Initializes the computed table.]

  Description [Initializes the computed table. It is called by
  Cudd_Init. Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Init]

******************************************************************************/
int
cuddInitCache( DdManager * unique /* unique table */ ,
			   unsigned int cacheSize /* initial size of the cache */ ,
			   unsigned int maxCacheSize
			   /* cache size beyond which no resizing occurs */  )
{
	int i;
	unsigned int logSize;
#ifndef DD_CACHE_PROFILE
	DdNodePtr *mem;
	ptruint offset;
#endif

	/* Round cacheSize to largest power of 2 not greater than the requested
	   ** initial cache size. */
	logSize = cuddComputeFloorLog2( ddMax( cacheSize, unique->slots / 2 ) );
	cacheSize = 1 << logSize;
	unique->acache = ALLOC( DdCache, cacheSize + 1 );
	if ( unique->acache == NULL )
	{
		unique->errorCode = CUDD_MEMORY_OUT;
		return ( 0 );
	}
	/* If the size of the cache entry is a power of 2, we want to
	   ** enforce alignment to that power of two. This happens when
	   ** DD_CACHE_PROFILE is not defined. */
#ifdef DD_CACHE_PROFILE
	unique->cache = unique->acache;
	unique->memused += ( cacheSize ) * sizeof( DdCache );
#else
	mem = ( DdNodePtr * ) unique->acache;
	offset = ( ptruint ) mem & ( sizeof( DdCache ) - 1 );
	mem += ( sizeof( DdCache ) - offset ) / sizeof( DdNodePtr );
	unique->cache = ( DdCache * ) mem;
	assert( ( ( ptruint ) unique->cache & ( sizeof( DdCache ) - 1 ) ) == 0 );
	unique->memused += ( cacheSize + 1 ) * sizeof( DdCache );
#endif
	unique->cacheSlots = cacheSize;
	unique->cacheShift = sizeof( int ) * 8 - logSize;
	unique->maxCacheHard = maxCacheSize;
	/* If cacheSlack is non-negative, we can resize. */
	unique->cacheSlack = ( int ) ddMin( maxCacheSize,
										DD_MAX_CACHE_TO_SLOTS_RATIO *
										unique->slots ) -
		2 * ( int ) cacheSize;
	Cudd_SetMinHit( unique, DD_MIN_HIT );
	/* Initialize to avoid division by 0 and immediate resizing. */
	unique->cacheMisses =
		( double ) ( int ) ( cacheSize * unique->minHit + 1 );
	unique->cacheHits = 0;
	unique->totCachehits = 0;
	/* The sum of cacheMisses and totCacheMisses is always correct,
	   ** even though cacheMisses is larger than it should for the reasons
	   ** explained above. */
	unique->totCacheMisses = -unique->cacheMisses;
	unique->cachecollisions = 0;
	unique->cacheinserts = 0;
	unique->cacheLastInserts = 0;
	unique->cachedeletions = 0;

	/* Initialize the cache */
	for ( i = 0; ( unsigned ) i < cacheSize; i++ )
	{
		unique->cache[i].h = 0;	/* unused slots */
		unique->cache[i].data = NULL;	/* invalid entry */
#ifdef DD_CACHE_PROFILE
		unique->cache[i].count = 0;
#endif
	}

	return ( 1 );

}								/* end of cuddInitCache */


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

  Synopsis    [Inserts a result in the cache.]

  Description []

  SideEffects [None]

  SeeAlso     [cuddCacheInsert2 cuddCacheInsert1]

******************************************************************************/
void
cuddCacheInsert( DdManager * table,
				 ptruint op,
				 DdNode * f, DdNode * g, DdNode * h, DdNode * data )
{
	int posn;
	register DdCache *entry;
	ptruint uf, ug, uh;

	uf = ( ptruint ) f | ( op & 0xe );
	ug = ( ptruint ) g | ( op >> 4 );
	uh = ( ptruint ) h;

	posn = ddCHash2( uh, uf, ug, table->cacheShift );
	entry = &table->cache[posn];

	table->cachecollisions += entry->data != NULL;
	table->cacheinserts++;

	entry->f = ( DdNode * ) uf;
	entry->g = ( DdNode * ) ug;
	entry->h = uh;
	entry->data = data;
#ifdef DD_CACHE_PROFILE
	entry->count++;
#endif

}								/* end of cuddCacheInsert */


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

  Synopsis    [Inserts a result in the cache for a function with two
  operands.]

  Description []

  SideEffects [None]

  SeeAlso     [cuddCacheInsert cuddCacheInsert1]

******************************************************************************/
void
cuddCacheInsert2( DdManager * table,
				  DdNode * ( *op ) ( DdManager *, DdNode *, DdNode * ),
				  DdNode * f, DdNode * g, DdNode * data )
{
	int posn;
	register DdCache *entry;

	posn = ddCHash2( op, f, g, table->cacheShift );
	entry = &table->cache[posn];

	if ( entry->data != NULL )
	{
		table->cachecollisions++;
	}
	table->cacheinserts++;

	entry->f = f;
	entry->g = g;
	entry->h = ( ptruint ) op;
	entry->data = data;
#ifdef DD_CACHE_PROFILE
	entry->count++;
#endif

}								/* end of cuddCacheInsert2 */


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

  Synopsis    [Inserts a result in the cache for a function with two
  operands.]

  Description []

  SideEffects [None]

  SeeAlso     [cuddCacheInsert cuddCacheInsert2]

******************************************************************************/
void
cuddCacheInsert1( DdManager * table,
				  DdNode * ( *op ) ( DdManager *, DdNode * ),
				  DdNode * f, DdNode * data )
{
	int posn;
	register DdCache *entry;

	posn = ddCHash2( op, f, f, table->cacheShift );
	entry = &table->cache[posn];

	if ( entry->data != NULL )
	{
		table->cachecollisions++;
	}
	table->cacheinserts++;

	entry->f = f;
	entry->g = f;
	entry->h = ( ptruint ) op;
	entry->data = data;
#ifdef DD_CACHE_PROFILE
	entry->count++;
#endif

}								/* end of cuddCacheInsert1 */


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

  Synopsis    [Looks up in the cache for the result of op applied to f,
  g, and h.]

  Description [Returns the result if found; it returns NULL if no
  result is found.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookup2 cuddCacheLookup1]

******************************************************************************/
DdNode *
cuddCacheLookup( DdManager * table,
				 ptruint op, DdNode * f, DdNode * g, DdNode * h )
{
	int posn;
	DdCache *en, *cache;
	DdNode *data;
	ptruint uf, ug, uh;

	uf = ( ptruint ) f | ( op & 0xe );
	ug = ( ptruint ) g | ( op >> 4 );
	uh = ( ptruint ) h;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif

	posn = ddCHash2( uh, uf, ug, table->cacheShift );
	en = &cache[posn];
	if ( en->data != NULL && en->f == ( DdNodePtr ) uf
		 && en->g == ( DdNodePtr ) ug && en->h == uh )
	{
		data = Cudd_Regular( en->data );
		table->cacheHits++;
		if ( data->ref == 0 )
		{
			cuddReclaim( table, data );
		}
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddCacheLookup */


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

  Synopsis    [Looks up in the cache for the result of op applied to f,
  g, and h.]

  Description [Returns the result if found; it returns NULL if no
  result is found.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookup2Zdd cuddCacheLookup1Zdd]

******************************************************************************/
DdNode *
cuddCacheLookupZdd( DdManager * table,
					ptruint op, DdNode * f, DdNode * g, DdNode * h )
{
	int posn;
	DdCache *en, *cache;
	DdNode *data;
	ptruint uf, ug, uh;

	uf = ( ptruint ) f | ( op & 0xe );
	ug = ( ptruint ) g | ( op >> 4 );
	uh = ( ptruint ) h;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif

	posn = ddCHash2( uh, uf, ug, table->cacheShift );
	en = &cache[posn];
	if ( en->data != NULL && en->f == ( DdNodePtr ) uf
		 && en->g == ( DdNodePtr ) ug && en->h == uh )
	{
		data = Cudd_Regular( en->data );
		table->cacheHits++;
		if ( data->ref == 0 )
		{
			cuddReclaimZdd( table, data );
		}
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddCacheLookupZdd */


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

  Synopsis    [Looks up in the cache for the result of op applied to f
  and g.]

  Description [Returns the result if found; it returns NULL if no
  result is found.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookup cuddCacheLookup1]

******************************************************************************/
DdNode *
cuddCacheLookup2( DdManager * table,
				  DdNode * ( *op ) ( DdManager *, DdNode *, DdNode * ),
				  DdNode * f, DdNode * g )
{
	int posn;
	DdCache *en, *cache;
	DdNode *data;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif

	posn = ddCHash2( op, f, g, table->cacheShift );
	en = &cache[posn];
	if ( en->data != NULL && en->f == f && en->g == g
		 && en->h == ( ptruint ) op )
	{
		data = Cudd_Regular( en->data );
		table->cacheHits++;
		if ( data->ref == 0 )
		{
			cuddReclaim( table, data );
		}
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddCacheLookup2 */


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

  Synopsis [Looks up in the cache for the result of op applied to f.]

  Description [Returns the result if found; it returns NULL if no
  result is found.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookup cuddCacheLookup2]

******************************************************************************/
DdNode *
cuddCacheLookup1( DdManager * table,
				  DdNode * ( *op ) ( DdManager *, DdNode * ), DdNode * f )
{
	int posn;
	DdCache *en, *cache;
	DdNode *data;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif

	posn = ddCHash2( op, f, f, table->cacheShift );
	en = &cache[posn];
	if ( en->data != NULL && en->f == f && en->h == ( ptruint ) op )
	{
		data = Cudd_Regular( en->data );
		table->cacheHits++;
		if ( data->ref == 0 )
		{
			cuddReclaim( table, data );
		}
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddCacheLookup1 */


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

  Synopsis [Looks up in the cache for the result of op applied to f
  and g.]

  Description [Returns the result if found; it returns NULL if no
  result is found.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookupZdd cuddCacheLookup1Zdd]

******************************************************************************/
DdNode *
cuddCacheLookup2Zdd( DdManager * table,
					 DdNode * ( *op ) ( DdManager *, DdNode *, DdNode * ),
					 DdNode * f, DdNode * g )
{
	int posn;
	DdCache *en, *cache;
	DdNode *data;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif

	posn = ddCHash2( op, f, g, table->cacheShift );
	en = &cache[posn];
	if ( en->data != NULL && en->f == f && en->g == g
		 && en->h == ( ptruint ) op )
	{
		data = Cudd_Regular( en->data );
		table->cacheHits++;
		if ( data->ref == 0 )
		{
			cuddReclaimZdd( table, data );
		}
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddCacheLookup2Zdd */


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

  Synopsis [Looks up in the cache for the result of op applied to f.]

  Description [Returns the result if found; it returns NULL if no
  result is found.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookupZdd cuddCacheLookup2Zdd]

******************************************************************************/
DdNode *
cuddCacheLookup1Zdd( DdManager * table,
					 DdNode * ( *op ) ( DdManager *, DdNode * ), DdNode * f )
{
	int posn;
	DdCache *en, *cache;
	DdNode *data;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif

	posn = ddCHash2( op, f, f, table->cacheShift );
	en = &cache[posn];
	if ( en->data != NULL && en->f == f && en->h == ( ptruint ) op )
	{
		data = Cudd_Regular( en->data );
		table->cacheHits++;
		if ( data->ref == 0 )
		{
			cuddReclaimZdd( table, data );
		}
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddCacheLookup1Zdd */


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

  Synopsis [Looks up in the cache for the result of op applied to f,
  g, and h.]

  Description [Looks up in the cache for the result of op applied to f,
  g, and h. Assumes that the calling procedure (e.g.,
  Cudd_bddIteConstant) is only interested in whether the result is
  constant or not. Returns the result if found (possibly
  DD_NON_CONSTANT); otherwise it returns NULL.]

  SideEffects [None]

  SeeAlso     [cuddCacheLookup]

******************************************************************************/
DdNode *
cuddConstantLookup( DdManager * table,
					ptruint op, DdNode * f, DdNode * g, DdNode * h )
{
	int posn;
	DdCache *en, *cache;
	ptruint uf, ug, uh;

	uf = ( ptruint ) f | ( op & 0xe );
	ug = ( ptruint ) g | ( op >> 4 );
	uh = ( ptruint ) h;

	cache = table->cache;
#ifdef DD_DEBUG
	if ( cache == NULL )
	{
		return ( NULL );
	}
#endif
	posn = ddCHash2( uh, uf, ug, table->cacheShift );
	en = &cache[posn];

	/* We do not reclaim here because the result should not be
	 * referenced, but only tested for being a constant.
	 */
	if ( en->data != NULL &&
		 en->f == ( DdNodePtr ) uf && en->g == ( DdNodePtr ) ug
		 && en->h == uh )
	{
		table->cacheHits++;
		return ( en->data );
	}

	/* Cache miss: decide whether to resize. */
	table->cacheMisses++;

	if ( table->cacheSlack >= 0 &&
		 table->cacheHits > table->cacheMisses * table->minHit )
	{
		cuddCacheResize( table );
	}

	return ( NULL );

}								/* end of cuddConstantLookup */


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

  Synopsis    [Computes and prints a profile of the cache usage.]

  Description [Computes and prints a profile of the cache usage.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddCacheProfile( DdManager * table, FILE * fp )
{
	DdCache *cache = table->cache;
	int slots = table->cacheSlots;
	int nzeroes = 0;
	int i, retval;
	double exUsed;

#ifdef DD_CACHE_PROFILE
	double count, mean, meansq, stddev, expected;
	long max, min;
	int imax, imin;
	double *hystogramQ, *hystogramR;	/* histograms by quotient and remainder */
	int nbins = DD_HYSTO_BINS;
	int bin;
	long thiscount;
	double totalcount, exStddev;

	meansq = mean = expected = 0.0;
	max = min = ( long ) cache[0].count;
	imax = imin = 0;
	totalcount = 0.0;

	hystogramQ = ALLOC( double, nbins );
	if ( hystogramQ == NULL )
	{
		table->errorCode = CUDD_MEMORY_OUT;
		return ( 0 );
	}
	hystogramR = ALLOC( double, nbins );
	if ( hystogramR == NULL )
	{
		FREE( hystogramQ );
		table->errorCode = CUDD_MEMORY_OUT;
		return ( 0 );
	}
	for ( i = 0; i < nbins; i++ )
	{
		hystogramQ[i] = 0;
		hystogramR[i] = 0;
	}

	for ( i = 0; i < slots; i++ )
	{
		thiscount = ( long ) cache[i].count;
		if ( thiscount > max )
		{
			max = thiscount;
			imax = i;
		}
		if ( thiscount < min )
		{
			min = thiscount;
			imin = i;
		}
		if ( thiscount == 0 )
		{
			nzeroes++;
		}
		count = ( double ) thiscount;
		mean += count;
		meansq += count * count;
		totalcount += count;
		expected += count * ( double ) i;
		bin = ( i * nbins ) / slots;
		hystogramQ[bin] += ( double ) thiscount;
		bin = i % nbins;
		hystogramR[bin] += ( double ) thiscount;
	}
	mean /= ( double ) slots;
	meansq /= ( double ) slots;

	/* Compute the standard deviation from both the data and the
	   ** theoretical model for a random distribution. */
	stddev = sqrt( meansq - mean * mean );
	exStddev =
		sqrt( ( 1 - 1 / ( double ) slots ) * totalcount / ( double ) slots );

	retval = fprintf( fp, "Cache average accesses = %g\n", mean );
	if ( retval == EOF )
		return ( 0 );
	retval = fprintf( fp, "Cache access standard deviation = %g ", stddev );
	if ( retval == EOF )
		return ( 0 );
	retval = fprintf( fp, "(expected = %g)\n", exStddev );
	if ( retval == EOF )
		return ( 0 );
	retval =
		fprintf( fp, "Cache max accesses = %ld for slot %d\n", max, imax );
	if ( retval == EOF )
		return ( 0 );
	retval =
		fprintf( fp, "Cache min accesses = %ld for slot %d\n", min, imin );
	if ( retval == EOF )
		return ( 0 );
	exUsed = 100.0 * ( 1.0 - exp( -totalcount / ( double ) slots ) );
	retval = fprintf( fp, "Cache used slots = %.2f%% (expected %.2f%%)\n",
					  100.0 - ( double ) nzeroes * 100.0 / ( double ) slots,
					  exUsed );
	if ( retval == EOF )
		return ( 0 );

	if ( totalcount > 0 )
	{
		expected /= totalcount;
		retval = fprintf( fp, "Cache access hystogram for %d bins", nbins );
		if ( retval == EOF )
			return ( 0 );
		retval = fprintf( fp, " (expected bin value = %g)\nBy quotient:",
						  expected );
		if ( retval == EOF )
			return ( 0 );
		for ( i = nbins - 1; i >= 0; i-- )
		{
			retval = fprintf( fp, " %.0f", hystogramQ[i] );
			if ( retval == EOF )
				return ( 0 );
		}
		retval = fprintf( fp, "\nBy residue: " );
		if ( retval == EOF )
			return ( 0 );
		for ( i = nbins - 1; i >= 0; i-- )
		{
			retval = fprintf( fp, " %.0f", hystogramR[i] );
			if ( retval == EOF )
				return ( 0 );
		}
		retval = fprintf( fp, "\n" );
		if ( retval == EOF )
			return ( 0 );
	}

	FREE( hystogramQ );
	FREE( hystogramR );
#else
	for ( i = 0; i < slots; i++ )
	{
		nzeroes += cache[i].h == 0;
	}
	exUsed = 100.0 *
		( 1.0 - exp( -( table->cacheinserts - table->cacheLastInserts ) /
					 ( double ) slots ) );
	retval = fprintf( fp, "Cache used slots = %.2f%% (expected %.2f%%)\n",
					  100.0 - ( double ) nzeroes * 100.0 / ( double ) slots,
					  exUsed );
	if ( retval == EOF )
		return ( 0 );
#endif
	return ( 1 );

}								/* end of cuddCacheProfile */


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

  Synopsis    [Resizes the cache.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddCacheResize( DdManager * table )
{
	DdCache *cache, *oldcache, *oldacache, *entry, *old;
	int i;
	int posn, shift;
	unsigned int slots, oldslots;
	double offset;
	int moved = 0;
	extern void ( *MMoutOfMemory ) ( long );
	void ( *saveHandler ) ( long );
#ifndef DD_CACHE_PROFILE
	ptruint misalignment;
	DdNodePtr *mem;
#endif

	oldcache = table->cache;
	oldacache = table->acache;
	oldslots = table->cacheSlots;
	slots = table->cacheSlots = oldslots << 1;

#ifdef DD_VERBOSE
	( void ) fprintf( table->err,
					  "Resizing the cache from %d to %d entries\n", oldslots,
					  slots );
	( void ) fprintf( table->err,
					  "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
					  table->cacheHits, table->cacheMisses,
					  table->cacheHits / ( table->cacheHits +
										   table->cacheMisses ) );
#endif

	saveHandler = MMoutOfMemory;
	MMoutOfMemory = Cudd_OutOfMem;
	table->acache = cache = ALLOC( DdCache, slots + 1 );
	MMoutOfMemory = saveHandler;
	/* If we fail to allocate the new table we just give up. */
	if ( cache == NULL )
	{
#ifdef DD_VERBOSE
		( void ) fprintf( table->err, "Resizing failed. Giving up.\n" );
#endif
		table->cacheSlots = oldslots;
		table->acache = oldacache;
		/* Do not try to resize again. */
		table->maxCacheHard = oldslots - 1;
		table->cacheSlack = -( oldslots + 1 );
		return;
	}
	/* If the size of the cache entry is a power of 2, we want to
	   ** enforce alignment to that power of two. This happens when
	   ** DD_CACHE_PROFILE is not defined. */
#ifdef DD_CACHE_PROFILE
	table->cache = cache;
#else
	mem = ( DdNodePtr * ) cache;
	misalignment = ( ptruint ) mem & ( sizeof( DdCache ) - 1 );
	mem += ( sizeof( DdCache ) - misalignment ) / sizeof( DdNodePtr );
	table->cache = cache = ( DdCache * ) mem;
	assert( ( ( ptruint ) table->cache & ( sizeof( DdCache ) - 1 ) ) == 0 );
#endif
	shift = --( table->cacheShift );
	table->memused += ( slots - oldslots ) * sizeof( DdCache );
	table->cacheSlack -= slots;	/* need these many slots to double again */

	/* Clear new cache. */
	for ( i = 0; ( unsigned ) i < slots; i++ )
	{
		cache[i].data = NULL;
		cache[i].h = 0;
#ifdef DD_CACHE_PROFILE
		cache[i].count = 0;
#endif
	}

	/* Copy from old cache to new one. */
	for ( i = 0; ( unsigned ) i < oldslots; i++ )
	{
		old = &oldcache[i];
		if ( old->data != NULL )
		{
			posn = ddCHash2( old->h, old->f, old->g, shift );
			entry = &cache[posn];
			entry->f = old->f;
			entry->g = old->g;
			entry->h = old->h;
			entry->data = old->data;
#ifdef DD_CACHE_PROFILE
			entry->count = 1;
#endif
			moved++;
		}
	}

	FREE( oldacache );

	/* Reinitialize measurements so as to avoid division by 0 and
	   ** immediate resizing.
	 */
	offset = ( double ) ( int ) ( slots * table->minHit + 1 );
	table->totCacheMisses += table->cacheMisses - offset;
	table->cacheMisses = offset;
	table->totCachehits += table->cacheHits;
	table->cacheHits = 0;
	table->cacheLastInserts = table->cacheinserts - ( double ) moved;

}								/* end of cuddCacheResize */


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

  Synopsis    [Flushes the cache.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddCacheFlush( DdManager * table )
{
	int i, slots;
	DdCache *cache;

	slots = table->cacheSlots;
	cache = table->cache;
	for ( i = 0; i < slots; i++ )
	{
		table->cachedeletions += cache[i].data != NULL;
		cache[i].data = NULL;
	}
	table->cacheLastInserts = table->cacheinserts;

	return;

}								/* end of cuddCacheFlush */


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

  Synopsis    [Returns the floor of the logarithm to the base 2.]

  Description [Returns the floor of the logarithm to the base 2.
  The input value is assumed to be greater than 0.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddComputeFloorLog2( unsigned int value )
{
	int floorLog = 0;
#ifdef DD_DEBUG
	assert( value > 0 );
#endif
	while ( value > 1 )
	{
		floorLog++;
		value >>= 1;
	}
	return ( floorLog );

}								/* end of cuddComputeFloorLog2 */

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