src/bdd/cudd/cuddCache.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddCache.c:

Go to the source code of this file.

Functions

int cuddInitCache (DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize)
void cuddCacheInsert (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data)
void cuddCacheInsert2 (DdManager *table, DdNode *(*op)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data)
void cuddCacheInsert1 (DdManager *table, DdNode *(*op)(DdManager *, DdNode *), DdNode *f, DdNode *data)
DdNodecuddCacheLookup (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
DdNodecuddCacheLookupZdd (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
DdNodecuddCacheLookup2 (DdManager *table, DdNode *(*op)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)
DdNodecuddCacheLookup1 (DdManager *table, DdNode *(*op)(DdManager *, DdNode *), DdNode *f)
DdNodecuddCacheLookup2Zdd (DdManager *table, DdNode *(*op)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)
DdNodecuddCacheLookup1Zdd (DdManager *table, DdNode *(*op)(DdManager *, DdNode *), DdNode *f)
DdNodecuddConstantLookup (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
int cuddCacheProfile (DdManager *table, FILE *fp)
void cuddCacheResize (DdManager *table)
void cuddCacheFlush (DdManager *table)
int cuddComputeFloorLog2 (unsigned int value)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddCache.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"

Function Documentation

void cuddCacheFlush ( DdManager table  ) 

Function********************************************************************

Synopsis [Flushes the cache.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 974 of file cuddCache.c.

00976 {
00977     int i, slots;
00978     DdCache *cache;
00979 
00980     slots = table->cacheSlots;
00981     cache = table->cache;
00982     for (i = 0; i < slots; i++) {
00983         table->cachedeletions += cache[i].data != NULL;
00984         cache[i].data = NULL;
00985     }
00986     table->cacheLastInserts = table->cacheinserts;
00987 
00988     return;
00989 
00990 } /* end of cuddCacheFlush */

void cuddCacheInsert ( DdManager table,
ptruint  op,
DdNode f,
DdNode g,
DdNode h,
DdNode data 
)

Function********************************************************************

Synopsis [Inserts a result in the cache.]

Description []

SideEffects [None]

SeeAlso [cuddCacheInsert2 cuddCacheInsert1]

Definition at line 187 of file cuddCache.c.

00194 {
00195     int posn;
00196     register DdCache *entry;
00197     ptruint uf, ug, uh;
00198 
00199     uf = (ptruint) f | (op & 0xe);
00200     ug = (ptruint) g | (op >> 4);
00201     uh = (ptruint) h;
00202 
00203     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00204     entry = &table->cache[posn];
00205 
00206     table->cachecollisions += entry->data != NULL;
00207     table->cacheinserts++;
00208 
00209     entry->f    = (DdNode *) uf;
00210     entry->g    = (DdNode *) ug;
00211     entry->h    = uh;
00212     entry->data = data;
00213 #ifdef DD_CACHE_PROFILE
00214     entry->count++;
00215 #endif
00216 
00217 } /* end of cuddCacheInsert */

void cuddCacheInsert1 ( DdManager table,
DdNode *(*)(DdManager *, DdNode *)  op,
DdNode f,
DdNode data 
)

Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso [cuddCacheInsert cuddCacheInsert2]

Definition at line 275 of file cuddCache.c.

00280 {
00281     int posn;
00282     register DdCache *entry;
00283 
00284     posn = ddCHash2(op,f,f,table->cacheShift);
00285     entry = &table->cache[posn];
00286 
00287     if (entry->data != NULL) {
00288         table->cachecollisions++;
00289     }
00290     table->cacheinserts++;
00291 
00292     entry->f = f;
00293     entry->g = f;
00294     entry->h = (ptruint) op;
00295     entry->data = data;
00296 #ifdef DD_CACHE_PROFILE
00297     entry->count++;
00298 #endif
00299 
00300 } /* end of cuddCacheInsert1 */

void cuddCacheInsert2 ( DdManager table,
DdNode *(*)(DdManager *, DdNode *, DdNode *)  op,
DdNode f,
DdNode g,
DdNode data 
)

Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso [cuddCacheInsert cuddCacheInsert1]

Definition at line 233 of file cuddCache.c.

00239 {
00240     int posn;
00241     register DdCache *entry;
00242 
00243     posn = ddCHash2(op,f,g,table->cacheShift);
00244     entry = &table->cache[posn];
00245 
00246     if (entry->data != NULL) {
00247         table->cachecollisions++;
00248     }
00249     table->cacheinserts++;
00250 
00251     entry->f = f;
00252     entry->g = g;
00253     entry->h = (ptruint) op;
00254     entry->data = data;
00255 #ifdef DD_CACHE_PROFILE
00256     entry->count++;
00257 #endif
00258 
00259 } /* end of cuddCacheInsert2 */

DdNode* cuddCacheLookup ( DdManager table,
ptruint  op,
DdNode f,
DdNode g,
DdNode h 
)

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]

Definition at line 317 of file cuddCache.c.

00323 {
00324     int posn;
00325     DdCache *en,*cache;
00326     DdNode *data;
00327     ptruint uf, ug, uh;
00328 
00329     uf = (ptruint) f | (op & 0xe);
00330     ug = (ptruint) g | (op >> 4);
00331     uh = (ptruint) h;
00332 
00333     cache = table->cache;
00334 #ifdef DD_DEBUG
00335     if (cache == NULL) {
00336         return(NULL);
00337     }
00338 #endif
00339 
00340     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00341     en = &cache[posn];
00342     if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
00343         en->h==uh) {
00344         data = Cudd_Regular(en->data);
00345         table->cacheHits++;
00346         if (data->ref == 0) {
00347             cuddReclaim(table,data);
00348         }
00349         return(en->data);
00350     }
00351 
00352     /* Cache miss: decide whether to resize. */
00353     table->cacheMisses++;
00354 
00355     if (table->cacheSlack >= 0 &&
00356         table->cacheHits > table->cacheMisses * table->minHit) {
00357         cuddCacheResize(table);
00358     }
00359 
00360     return(NULL);
00361 
00362 } /* end of cuddCacheLookup */

DdNode* cuddCacheLookup1 ( DdManager table,
DdNode *(*)(DdManager *, DdNode *)  op,
DdNode f 
)

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]

Definition at line 495 of file cuddCache.c.

00499 {
00500     int posn;
00501     DdCache *en,*cache;
00502     DdNode *data;
00503 
00504     cache = table->cache;
00505 #ifdef DD_DEBUG
00506     if (cache == NULL) {
00507         return(NULL);
00508     }
00509 #endif
00510 
00511     posn = ddCHash2(op,f,f,table->cacheShift);
00512     en = &cache[posn];
00513     if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
00514         data = Cudd_Regular(en->data);
00515         table->cacheHits++;
00516         if (data->ref == 0) {
00517             cuddReclaim(table,data);
00518         }
00519         return(en->data);
00520     }
00521 
00522     /* Cache miss: decide whether to resize. */
00523     table->cacheMisses++;
00524 
00525     if (table->cacheSlack >= 0 &&
00526         table->cacheHits > table->cacheMisses * table->minHit) {
00527         cuddCacheResize(table);
00528     }
00529 
00530     return(NULL);
00531 
00532 } /* end of cuddCacheLookup1 */

DdNode* cuddCacheLookup1Zdd ( DdManager table,
DdNode *(*)(DdManager *, DdNode *)  op,
DdNode f 
)

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]

Definition at line 603 of file cuddCache.c.

00607 {
00608     int posn;
00609     DdCache *en,*cache;
00610     DdNode *data;
00611 
00612     cache = table->cache;
00613 #ifdef DD_DEBUG
00614     if (cache == NULL) {
00615         return(NULL);
00616     }
00617 #endif
00618 
00619     posn = ddCHash2(op,f,f,table->cacheShift);
00620     en = &cache[posn];
00621     if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
00622         data = Cudd_Regular(en->data);
00623         table->cacheHits++;
00624         if (data->ref == 0) {
00625             cuddReclaimZdd(table,data);
00626         }
00627         return(en->data);
00628     }
00629 
00630     /* Cache miss: decide whether to resize. */
00631     table->cacheMisses++;
00632 
00633     if (table->cacheSlack >= 0  &&
00634         table->cacheHits > table->cacheMisses * table->minHit) {
00635         cuddCacheResize(table);
00636     }
00637 
00638     return(NULL);
00639 
00640 } /* end of cuddCacheLookup1Zdd */

DdNode* cuddCacheLookup2 ( DdManager table,
DdNode *(*)(DdManager *, DdNode *, DdNode *)  op,
DdNode f,
DdNode g 
)

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]

Definition at line 441 of file cuddCache.c.

00446 {
00447     int posn;
00448     DdCache *en,*cache;
00449     DdNode *data;
00450 
00451     cache = table->cache;
00452 #ifdef DD_DEBUG
00453     if (cache == NULL) {
00454         return(NULL);
00455     }
00456 #endif
00457 
00458     posn = ddCHash2(op,f,g,table->cacheShift);
00459     en = &cache[posn];
00460     if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
00461         data = Cudd_Regular(en->data);
00462         table->cacheHits++;
00463         if (data->ref == 0) {
00464             cuddReclaim(table,data);
00465         }
00466         return(en->data);
00467     }
00468 
00469     /* Cache miss: decide whether to resize. */
00470     table->cacheMisses++;
00471 
00472     if (table->cacheSlack >= 0 &&
00473         table->cacheHits > table->cacheMisses * table->minHit) {
00474         cuddCacheResize(table);
00475     }
00476 
00477     return(NULL);
00478 
00479 } /* end of cuddCacheLookup2 */

DdNode* cuddCacheLookup2Zdd ( DdManager table,
DdNode *(*)(DdManager *, DdNode *, DdNode *)  op,
DdNode f,
DdNode g 
)

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]

Definition at line 549 of file cuddCache.c.

00554 {
00555     int posn;
00556     DdCache *en,*cache;
00557     DdNode *data;
00558 
00559     cache = table->cache;
00560 #ifdef DD_DEBUG
00561     if (cache == NULL) {
00562         return(NULL);
00563     }
00564 #endif
00565 
00566     posn = ddCHash2(op,f,g,table->cacheShift);
00567     en = &cache[posn];
00568     if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
00569         data = Cudd_Regular(en->data);
00570         table->cacheHits++;
00571         if (data->ref == 0) {
00572             cuddReclaimZdd(table,data);
00573         }
00574         return(en->data);
00575     }
00576 
00577     /* Cache miss: decide whether to resize. */
00578     table->cacheMisses++;
00579 
00580     if (table->cacheSlack >= 0 &&
00581         table->cacheHits > table->cacheMisses * table->minHit) {
00582         cuddCacheResize(table);
00583     }
00584 
00585     return(NULL);
00586 
00587 } /* end of cuddCacheLookup2Zdd */

DdNode* cuddCacheLookupZdd ( DdManager table,
ptruint  op,
DdNode f,
DdNode g,
DdNode h 
)

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]

Definition at line 379 of file cuddCache.c.

00385 {
00386     int posn;
00387     DdCache *en,*cache;
00388     DdNode *data;
00389     ptruint uf, ug, uh;
00390 
00391     uf = (ptruint) f | (op & 0xe);
00392     ug = (ptruint) g | (op >> 4);
00393     uh = (ptruint) h;
00394 
00395     cache = table->cache;
00396 #ifdef DD_DEBUG
00397     if (cache == NULL) {
00398         return(NULL);
00399     }
00400 #endif
00401 
00402     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00403     en = &cache[posn];
00404     if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
00405         en->h==uh) {
00406         data = Cudd_Regular(en->data);
00407         table->cacheHits++;
00408         if (data->ref == 0) {
00409             cuddReclaimZdd(table,data);
00410         }
00411         return(en->data);
00412     }
00413 
00414     /* Cache miss: decide whether to resize. */
00415     table->cacheMisses++;
00416 
00417     if (table->cacheSlack >= 0 &&
00418         table->cacheHits > table->cacheMisses * table->minHit) {
00419         cuddCacheResize(table);
00420     }
00421 
00422     return(NULL);
00423 
00424 } /* end of cuddCacheLookupZdd */

int cuddCacheProfile ( DdManager table,
FILE *  fp 
)

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 []

Definition at line 719 of file cuddCache.c.

00722 {
00723     DdCache *cache = table->cache;
00724     int slots = table->cacheSlots;
00725     int nzeroes = 0;
00726     int i, retval;
00727     double exUsed;
00728 
00729 #ifdef DD_CACHE_PROFILE
00730     double count, mean, meansq, stddev, expected;
00731     long max, min;
00732     int imax, imin;
00733     double *hystogramQ, *hystogramR; /* histograms by quotient and remainder */
00734     int nbins = DD_HYSTO_BINS;
00735     int bin;
00736     long thiscount;
00737     double totalcount, exStddev;
00738 
00739     meansq = mean = expected = 0.0;
00740     max = min = (long) cache[0].count;
00741     imax = imin = 0;
00742     totalcount = 0.0;
00743 
00744     hystogramQ = ALLOC(double, nbins);
00745     if (hystogramQ == NULL) {
00746         table->errorCode = CUDD_MEMORY_OUT;
00747         return(0);
00748     }
00749     hystogramR = ALLOC(double, nbins);
00750     if (hystogramR == NULL) {
00751         FREE(hystogramQ);
00752         table->errorCode = CUDD_MEMORY_OUT;
00753         return(0);
00754     }
00755     for (i = 0; i < nbins; i++) {
00756         hystogramQ[i] = 0;
00757         hystogramR[i] = 0;
00758     }
00759 
00760     for (i = 0; i < slots; i++) {
00761         thiscount = (long) cache[i].count;
00762         if (thiscount > max) {
00763             max = thiscount;
00764             imax = i;
00765         }
00766         if (thiscount < min) {
00767             min = thiscount;
00768             imin = i;
00769         }
00770         if (thiscount == 0) {
00771             nzeroes++;
00772         }
00773         count = (double) thiscount;
00774         mean += count;
00775         meansq += count * count;
00776         totalcount += count;
00777         expected += count * (double) i;
00778         bin = (i * nbins) / slots;
00779         hystogramQ[bin] += (double) thiscount;
00780         bin = i % nbins;
00781         hystogramR[bin] += (double) thiscount;
00782     }
00783     mean /= (double) slots;
00784     meansq /= (double) slots;
00785     
00786     /* Compute the standard deviation from both the data and the
00787     ** theoretical model for a random distribution. */
00788     stddev = sqrt(meansq - mean*mean);
00789     exStddev = sqrt((1 - 1/(double) slots) * totalcount / (double) slots);
00790 
00791     retval = fprintf(fp,"Cache average accesses = %g\n",  mean);
00792     if (retval == EOF) return(0);
00793     retval = fprintf(fp,"Cache access standard deviation = %g ", stddev);
00794     if (retval == EOF) return(0);
00795     retval = fprintf(fp,"(expected = %g)\n", exStddev);
00796     if (retval == EOF) return(0);
00797     retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
00798     if (retval == EOF) return(0);
00799     retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
00800     if (retval == EOF) return(0);
00801     exUsed = 100.0 * (1.0 - exp(-totalcount / (double) slots));
00802     retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
00803                      100.0 - (double) nzeroes * 100.0 / (double) slots,
00804                      exUsed);
00805     if (retval == EOF) return(0);
00806 
00807     if (totalcount > 0) {
00808         expected /= totalcount;
00809         retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
00810         if (retval == EOF) return(0);
00811         retval = fprintf(fp," (expected bin value = %g)\nBy quotient:",
00812                          expected);
00813         if (retval == EOF) return(0);
00814         for (i = nbins - 1; i>=0; i--) {
00815             retval = fprintf(fp," %.0f", hystogramQ[i]);
00816             if (retval == EOF) return(0);
00817         }
00818         retval = fprintf(fp,"\nBy residue: ");
00819         if (retval == EOF) return(0);
00820         for (i = nbins - 1; i>=0; i--) {
00821             retval = fprintf(fp," %.0f", hystogramR[i]);
00822             if (retval == EOF) return(0);
00823         }
00824         retval = fprintf(fp,"\n");
00825         if (retval == EOF) return(0);
00826     }
00827 
00828     FREE(hystogramQ);
00829     FREE(hystogramR);
00830 #else
00831     for (i = 0; i < slots; i++) {
00832         nzeroes += cache[i].h == 0;
00833     }
00834     exUsed = 100.0 *
00835         (1.0 - exp(-(table->cacheinserts - table->cacheLastInserts) /
00836                    (double) slots));
00837     retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
00838                      100.0 - (double) nzeroes * 100.0 / (double) slots,
00839                      exUsed);
00840     if (retval == EOF) return(0);
00841 #endif
00842     return(1);
00843 
00844 } /* end of cuddCacheProfile */

void cuddCacheResize ( DdManager table  ) 

Function********************************************************************

Synopsis [Resizes the cache.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 859 of file cuddCache.c.

00861 {
00862     DdCache *cache, *oldcache, *oldacache, *entry, *old;
00863     int i;
00864     int posn, shift;
00865     unsigned int slots, oldslots;
00866     double offset;
00867     int moved = 0;
00868     extern void (*MMoutOfMemory)(long);
00869     void (*saveHandler)(long);
00870 #ifndef DD_CACHE_PROFILE
00871     ptruint misalignment;
00872     DdNodePtr *mem;
00873 #endif
00874 
00875     oldcache = table->cache;
00876     oldacache = table->acache;
00877     oldslots = table->cacheSlots;
00878     slots = table->cacheSlots = oldslots << 1;
00879 
00880 #ifdef DD_VERBOSE
00881     (void) fprintf(table->err,"Resizing the cache from %d to %d entries\n",
00882                    oldslots, slots);
00883     (void) fprintf(table->err,
00884                    "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
00885                    table->cacheHits, table->cacheMisses,
00886                    table->cacheHits / (table->cacheHits + table->cacheMisses));
00887 #endif
00888 
00889     saveHandler = MMoutOfMemory;
00890     MMoutOfMemory = Cudd_OutOfMem;
00891     table->acache = cache = ALLOC(DdCache,slots+1);
00892     MMoutOfMemory = saveHandler;
00893     /* If we fail to allocate the new table we just give up. */
00894     if (cache == NULL) {
00895 #ifdef DD_VERBOSE
00896         (void) fprintf(table->err,"Resizing failed. Giving up.\n");
00897 #endif
00898         table->cacheSlots = oldslots;
00899         table->acache = oldacache;
00900         /* Do not try to resize again. */
00901         table->maxCacheHard = oldslots - 1;
00902         table->cacheSlack = - (oldslots + 1);
00903         return;
00904     }
00905     /* If the size of the cache entry is a power of 2, we want to
00906     ** enforce alignment to that power of two. This happens when
00907     ** DD_CACHE_PROFILE is not defined. */
00908 #ifdef DD_CACHE_PROFILE
00909     table->cache = cache;
00910 #else
00911     mem = (DdNodePtr *) cache;
00912     misalignment = (ptruint) mem & (sizeof(DdCache) - 1);
00913     mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr);
00914     table->cache = cache = (DdCache *) mem;
00915     assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0);
00916 #endif
00917     shift = --(table->cacheShift);
00918     table->memused += (slots - oldslots) * sizeof(DdCache);
00919     table->cacheSlack -= slots; /* need these many slots to double again */
00920 
00921     /* Clear new cache. */
00922     for (i = 0; (unsigned) i < slots; i++) {
00923         cache[i].data = NULL;
00924         cache[i].h = 0;
00925 #ifdef DD_CACHE_PROFILE
00926         cache[i].count = 0;
00927 #endif
00928     }
00929 
00930     /* Copy from old cache to new one. */
00931     for (i = 0; (unsigned) i < oldslots; i++) {
00932         old = &oldcache[i];
00933         if (old->data != NULL) {
00934             posn = ddCHash2(old->h,old->f,old->g,shift);
00935             entry = &cache[posn];
00936             entry->f = old->f;
00937             entry->g = old->g;
00938             entry->h = old->h;
00939             entry->data = old->data;    
00940 #ifdef DD_CACHE_PROFILE
00941             entry->count = 1;
00942 #endif
00943             moved++;
00944         }
00945     }
00946 
00947     FREE(oldacache);
00948 
00949     /* Reinitialize measurements so as to avoid division by 0 and
00950     ** immediate resizing.
00951     */
00952     offset = (double) (int) (slots * table->minHit + 1);
00953     table->totCacheMisses += table->cacheMisses - offset;
00954     table->cacheMisses = offset;
00955     table->totCachehits += table->cacheHits;
00956     table->cacheHits = 0;
00957     table->cacheLastInserts = table->cacheinserts - (double) moved;
00958 
00959 } /* end of cuddCacheResize */

int cuddComputeFloorLog2 ( unsigned int  value  ) 

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 []

Definition at line 1006 of file cuddCache.c.

01008 {
01009     int floorLog = 0;
01010 #ifdef DD_DEBUG
01011     assert(value > 0);
01012 #endif
01013     while (value > 1) {
01014         floorLog++;
01015         value >>= 1;
01016     }
01017     return(floorLog);
01018 
01019 } /* end of cuddComputeFloorLog2 */

DdNode* cuddConstantLookup ( DdManager table,
ptruint  op,
DdNode f,
DdNode g,
DdNode h 
)

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]

Definition at line 660 of file cuddCache.c.

00666 {
00667     int posn;
00668     DdCache *en,*cache;
00669     ptruint uf, ug, uh;
00670 
00671     uf = (ptruint) f | (op & 0xe);
00672     ug = (ptruint) g | (op >> 4);
00673     uh = (ptruint) h;
00674 
00675     cache = table->cache;
00676 #ifdef DD_DEBUG
00677     if (cache == NULL) {
00678         return(NULL);
00679     }
00680 #endif
00681     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00682     en = &cache[posn];
00683 
00684     /* We do not reclaim here because the result should not be
00685      * referenced, but only tested for being a constant.
00686      */
00687     if (en->data != NULL &&
00688         en->f == (DdNodePtr)uf && en->g == (DdNodePtr)ug && en->h == uh) {
00689         table->cacheHits++;
00690         return(en->data);
00691     }
00692 
00693     /* Cache miss: decide whether to resize. */
00694     table->cacheMisses++;
00695 
00696     if (table->cacheSlack >= 0 &&
00697         table->cacheHits > table->cacheMisses * table->minHit) {
00698         cuddCacheResize(table);
00699     }
00700 
00701     return(NULL);
00702 
00703 } /* end of cuddConstantLookup */

int cuddInitCache ( DdManager unique,
unsigned int  cacheSize,
unsigned int  maxCacheSize 
)

AutomaticStart AutomaticEnd 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]

Definition at line 105 of file cuddCache.c.

00109 {
00110     int i;
00111     unsigned int logSize;
00112 #ifndef DD_CACHE_PROFILE
00113     DdNodePtr *mem;
00114     ptruint offset;
00115 #endif
00116 
00117     /* Round cacheSize to largest power of 2 not greater than the requested
00118     ** initial cache size. */
00119     logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
00120     cacheSize = 1 << logSize;
00121     unique->acache = ALLOC(DdCache,cacheSize+1);
00122     if (unique->acache == NULL) {
00123         unique->errorCode = CUDD_MEMORY_OUT;
00124         return(0);
00125     }
00126     /* If the size of the cache entry is a power of 2, we want to
00127     ** enforce alignment to that power of two. This happens when
00128     ** DD_CACHE_PROFILE is not defined. */
00129 #ifdef DD_CACHE_PROFILE
00130     unique->cache = unique->acache;
00131     unique->memused += (cacheSize) * sizeof(DdCache);
00132 #else
00133     mem = (DdNodePtr *) unique->acache;
00134     offset = (ptruint) mem & (sizeof(DdCache) - 1);
00135     mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr);
00136     unique->cache = (DdCache *) mem;
00137     assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0);
00138     unique->memused += (cacheSize+1) * sizeof(DdCache);
00139 #endif
00140     unique->cacheSlots = cacheSize;
00141     unique->cacheShift = sizeof(int) * 8 - logSize;
00142     unique->maxCacheHard = maxCacheSize;
00143     /* If cacheSlack is non-negative, we can resize. */
00144     unique->cacheSlack = (int) ddMin(maxCacheSize,
00145         DD_MAX_CACHE_TO_SLOTS_RATIO*unique->slots) -
00146         2 * (int) cacheSize;
00147     Cudd_SetMinHit(unique,DD_MIN_HIT);
00148     /* Initialize to avoid division by 0 and immediate resizing. */
00149     unique->cacheMisses = (double) (int) (cacheSize * unique->minHit + 1);
00150     unique->cacheHits = 0;
00151     unique->totCachehits = 0;
00152     /* The sum of cacheMisses and totCacheMisses is always correct,
00153     ** even though cacheMisses is larger than it should for the reasons
00154     ** explained above. */
00155     unique->totCacheMisses = -unique->cacheMisses;
00156     unique->cachecollisions = 0;
00157     unique->cacheinserts = 0;
00158     unique->cacheLastInserts = 0;
00159     unique->cachedeletions = 0;
00160 
00161     /* Initialize the cache */
00162     for (i = 0; (unsigned) i < cacheSize; i++) {
00163         unique->cache[i].h = 0; /* unused slots */
00164         unique->cache[i].data = NULL; /* invalid entry */
00165 #ifdef DD_CACHE_PROFILE
00166         unique->cache[i].count = 0;
00167 #endif
00168     }
00169 
00170     return(1);
00171 
00172 } /* end of cuddInitCache */


Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddCache.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddCache.c]

PackageName [cudd]

Synopsis [Functions for cache insertion and lookup.]

Description [Internal procedures included in this module:

Static procedures included in this module:

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.]

Definition at line 65 of file cuddCache.c.


Generated on Tue Jan 5 12:18:53 2010 for abc70930 by  doxygen 1.6.1