src/cuBdd/cuddCache.c File Reference

#include "util.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, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
void cuddCacheInsert1 (DdManager *table, DD_CTFP1 op, 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, DD_CTFP op, DdNode *f, DdNode *g)
DdNodecuddCacheLookup1 (DdManager *table, DD_CTFP1 op, DdNode *f)
DdNodecuddCacheLookup2Zdd (DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
DdNodecuddCacheLookup1Zdd (DdManager *table, DD_CTFP1 op, 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.34 2009/02/19 16:17:50 fabio Exp $"

Function Documentation

void cuddCacheFlush ( DdManager table  ) 

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

Synopsis [Flushes the cache.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1001 of file cuddCache.c.

01003 {
01004     int i, slots;
01005     DdCache *cache;
01006 
01007     slots = table->cacheSlots;
01008     cache = table->cache;
01009     for (i = 0; i < slots; i++) {
01010         table->cachedeletions += cache[i].data != NULL;
01011         cache[i].data = NULL;
01012     }
01013     table->cacheLastInserts = table->cacheinserts;
01014 
01015     return;
01016 
01017 } /* 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 214 of file cuddCache.c.

00221 {
00222     int posn;
00223     register DdCache *entry;
00224     ptruint uf, ug, uh;
00225 
00226     uf = (ptruint) f | (op & 0xe);
00227     ug = (ptruint) g | (op >> 4);
00228     uh = (ptruint) h;
00229 
00230     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00231     entry = &table->cache[posn];
00232 
00233     table->cachecollisions += entry->data != NULL;
00234     table->cacheinserts++;
00235 
00236     entry->f    = (DdNode *) uf;
00237     entry->g    = (DdNode *) ug;
00238     entry->h    = uh;
00239     entry->data = data;
00240 #ifdef DD_CACHE_PROFILE
00241     entry->count++;
00242 #endif
00243 
00244 } /* end of cuddCacheInsert */

void cuddCacheInsert1 ( DdManager table,
DD_CTFP1  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 302 of file cuddCache.c.

00307 {
00308     int posn;
00309     register DdCache *entry;
00310 
00311     posn = ddCHash2(op,f,f,table->cacheShift);
00312     entry = &table->cache[posn];
00313 
00314     if (entry->data != NULL) {
00315         table->cachecollisions++;
00316     }
00317     table->cacheinserts++;
00318 
00319     entry->f = f;
00320     entry->g = f;
00321     entry->h = (ptruint) op;
00322     entry->data = data;
00323 #ifdef DD_CACHE_PROFILE
00324     entry->count++;
00325 #endif
00326 
00327 } /* end of cuddCacheInsert1 */

void cuddCacheInsert2 ( DdManager table,
DD_CTFP  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 260 of file cuddCache.c.

00266 {
00267     int posn;
00268     register DdCache *entry;
00269 
00270     posn = ddCHash2(op,f,g,table->cacheShift);
00271     entry = &table->cache[posn];
00272 
00273     if (entry->data != NULL) {
00274         table->cachecollisions++;
00275     }
00276     table->cacheinserts++;
00277 
00278     entry->f = f;
00279     entry->g = g;
00280     entry->h = (ptruint) op;
00281     entry->data = data;
00282 #ifdef DD_CACHE_PROFILE
00283     entry->count++;
00284 #endif
00285 
00286 } /* 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 344 of file cuddCache.c.

00350 {
00351     int posn;
00352     DdCache *en,*cache;
00353     DdNode *data;
00354     ptruint uf, ug, uh;
00355 
00356     uf = (ptruint) f | (op & 0xe);
00357     ug = (ptruint) g | (op >> 4);
00358     uh = (ptruint) h;
00359 
00360     cache = table->cache;
00361 #ifdef DD_DEBUG
00362     if (cache == NULL) {
00363         return(NULL);
00364     }
00365 #endif
00366 
00367     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00368     en = &cache[posn];
00369     if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
00370         en->h==uh) {
00371         data = Cudd_Regular(en->data);
00372         table->cacheHits++;
00373         if (data->ref == 0) {
00374             cuddReclaim(table,data);
00375         }
00376         return(en->data);
00377     }
00378 
00379     /* Cache miss: decide whether to resize. */
00380     table->cacheMisses++;
00381 
00382     if (table->cacheSlack >= 0 &&
00383         table->cacheHits > table->cacheMisses * table->minHit) {
00384         cuddCacheResize(table);
00385     }
00386 
00387     return(NULL);
00388 
00389 } /* end of cuddCacheLookup */

DdNode* cuddCacheLookup1 ( DdManager table,
DD_CTFP1  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 522 of file cuddCache.c.

00526 {
00527     int posn;
00528     DdCache *en,*cache;
00529     DdNode *data;
00530 
00531     cache = table->cache;
00532 #ifdef DD_DEBUG
00533     if (cache == NULL) {
00534         return(NULL);
00535     }
00536 #endif
00537 
00538     posn = ddCHash2(op,f,f,table->cacheShift);
00539     en = &cache[posn];
00540     if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
00541         data = Cudd_Regular(en->data);
00542         table->cacheHits++;
00543         if (data->ref == 0) {
00544             cuddReclaim(table,data);
00545         }
00546         return(en->data);
00547     }
00548 
00549     /* Cache miss: decide whether to resize. */
00550     table->cacheMisses++;
00551 
00552     if (table->cacheSlack >= 0 &&
00553         table->cacheHits > table->cacheMisses * table->minHit) {
00554         cuddCacheResize(table);
00555     }
00556 
00557     return(NULL);
00558 
00559 } /* end of cuddCacheLookup1 */

DdNode* cuddCacheLookup1Zdd ( DdManager table,
DD_CTFP1  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 630 of file cuddCache.c.

00634 {
00635     int posn;
00636     DdCache *en,*cache;
00637     DdNode *data;
00638 
00639     cache = table->cache;
00640 #ifdef DD_DEBUG
00641     if (cache == NULL) {
00642         return(NULL);
00643     }
00644 #endif
00645 
00646     posn = ddCHash2(op,f,f,table->cacheShift);
00647     en = &cache[posn];
00648     if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
00649         data = Cudd_Regular(en->data);
00650         table->cacheHits++;
00651         if (data->ref == 0) {
00652             cuddReclaimZdd(table,data);
00653         }
00654         return(en->data);
00655     }
00656 
00657     /* Cache miss: decide whether to resize. */
00658     table->cacheMisses++;
00659 
00660     if (table->cacheSlack >= 0  &&
00661         table->cacheHits > table->cacheMisses * table->minHit) {
00662         cuddCacheResize(table);
00663     }
00664 
00665     return(NULL);
00666 
00667 } /* end of cuddCacheLookup1Zdd */

DdNode* cuddCacheLookup2 ( DdManager table,
DD_CTFP  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 468 of file cuddCache.c.

00473 {
00474     int posn;
00475     DdCache *en,*cache;
00476     DdNode *data;
00477 
00478     cache = table->cache;
00479 #ifdef DD_DEBUG
00480     if (cache == NULL) {
00481         return(NULL);
00482     }
00483 #endif
00484 
00485     posn = ddCHash2(op,f,g,table->cacheShift);
00486     en = &cache[posn];
00487     if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
00488         data = Cudd_Regular(en->data);
00489         table->cacheHits++;
00490         if (data->ref == 0) {
00491             cuddReclaim(table,data);
00492         }
00493         return(en->data);
00494     }
00495 
00496     /* Cache miss: decide whether to resize. */
00497     table->cacheMisses++;
00498 
00499     if (table->cacheSlack >= 0 &&
00500         table->cacheHits > table->cacheMisses * table->minHit) {
00501         cuddCacheResize(table);
00502     }
00503 
00504     return(NULL);
00505 
00506 } /* end of cuddCacheLookup2 */

DdNode* cuddCacheLookup2Zdd ( DdManager table,
DD_CTFP  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 576 of file cuddCache.c.

00581 {
00582     int posn;
00583     DdCache *en,*cache;
00584     DdNode *data;
00585 
00586     cache = table->cache;
00587 #ifdef DD_DEBUG
00588     if (cache == NULL) {
00589         return(NULL);
00590     }
00591 #endif
00592 
00593     posn = ddCHash2(op,f,g,table->cacheShift);
00594     en = &cache[posn];
00595     if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
00596         data = Cudd_Regular(en->data);
00597         table->cacheHits++;
00598         if (data->ref == 0) {
00599             cuddReclaimZdd(table,data);
00600         }
00601         return(en->data);
00602     }
00603 
00604     /* Cache miss: decide whether to resize. */
00605     table->cacheMisses++;
00606 
00607     if (table->cacheSlack >= 0 &&
00608         table->cacheHits > table->cacheMisses * table->minHit) {
00609         cuddCacheResize(table);
00610     }
00611 
00612     return(NULL);
00613 
00614 } /* 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 406 of file cuddCache.c.

00412 {
00413     int posn;
00414     DdCache *en,*cache;
00415     DdNode *data;
00416     ptruint uf, ug, uh;
00417 
00418     uf = (ptruint) f | (op & 0xe);
00419     ug = (ptruint) g | (op >> 4);
00420     uh = (ptruint) h;
00421 
00422     cache = table->cache;
00423 #ifdef DD_DEBUG
00424     if (cache == NULL) {
00425         return(NULL);
00426     }
00427 #endif
00428 
00429     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00430     en = &cache[posn];
00431     if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
00432         en->h==uh) {
00433         data = Cudd_Regular(en->data);
00434         table->cacheHits++;
00435         if (data->ref == 0) {
00436             cuddReclaimZdd(table,data);
00437         }
00438         return(en->data);
00439     }
00440 
00441     /* Cache miss: decide whether to resize. */
00442     table->cacheMisses++;
00443 
00444     if (table->cacheSlack >= 0 &&
00445         table->cacheHits > table->cacheMisses * table->minHit) {
00446         cuddCacheResize(table);
00447     }
00448 
00449     return(NULL);
00450 
00451 } /* 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 746 of file cuddCache.c.

00749 {
00750     DdCache *cache = table->cache;
00751     int slots = table->cacheSlots;
00752     int nzeroes = 0;
00753     int i, retval;
00754     double exUsed;
00755 
00756 #ifdef DD_CACHE_PROFILE
00757     double count, mean, meansq, stddev, expected;
00758     long max, min;
00759     int imax, imin;
00760     double *hystogramQ, *hystogramR; /* histograms by quotient and remainder */
00761     int nbins = DD_HYSTO_BINS;
00762     int bin;
00763     long thiscount;
00764     double totalcount, exStddev;
00765 
00766     meansq = mean = expected = 0.0;
00767     max = min = (long) cache[0].count;
00768     imax = imin = 0;
00769     totalcount = 0.0;
00770 
00771     hystogramQ = ALLOC(double, nbins);
00772     if (hystogramQ == NULL) {
00773         table->errorCode = CUDD_MEMORY_OUT;
00774         return(0);
00775     }
00776     hystogramR = ALLOC(double, nbins);
00777     if (hystogramR == NULL) {
00778         FREE(hystogramQ);
00779         table->errorCode = CUDD_MEMORY_OUT;
00780         return(0);
00781     }
00782     for (i = 0; i < nbins; i++) {
00783         hystogramQ[i] = 0;
00784         hystogramR[i] = 0;
00785     }
00786 
00787     for (i = 0; i < slots; i++) {
00788         thiscount = (long) cache[i].count;
00789         if (thiscount > max) {
00790             max = thiscount;
00791             imax = i;
00792         }
00793         if (thiscount < min) {
00794             min = thiscount;
00795             imin = i;
00796         }
00797         if (thiscount == 0) {
00798             nzeroes++;
00799         }
00800         count = (double) thiscount;
00801         mean += count;
00802         meansq += count * count;
00803         totalcount += count;
00804         expected += count * (double) i;
00805         bin = (i * nbins) / slots;
00806         hystogramQ[bin] += (double) thiscount;
00807         bin = i % nbins;
00808         hystogramR[bin] += (double) thiscount;
00809     }
00810     mean /= (double) slots;
00811     meansq /= (double) slots;
00812 
00813     /* Compute the standard deviation from both the data and the
00814     ** theoretical model for a random distribution. */
00815     stddev = sqrt(meansq - mean*mean);
00816     exStddev = sqrt((1 - 1/(double) slots) * totalcount / (double) slots);
00817 
00818     retval = fprintf(fp,"Cache average accesses = %g\n",  mean);
00819     if (retval == EOF) return(0);
00820     retval = fprintf(fp,"Cache access standard deviation = %g ", stddev);
00821     if (retval == EOF) return(0);
00822     retval = fprintf(fp,"(expected = %g)\n", exStddev);
00823     if (retval == EOF) return(0);
00824     retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
00825     if (retval == EOF) return(0);
00826     retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
00827     if (retval == EOF) return(0);
00828     exUsed = 100.0 * (1.0 - exp(-totalcount / (double) slots));
00829     retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
00830                      100.0 - (double) nzeroes * 100.0 / (double) slots,
00831                      exUsed);
00832     if (retval == EOF) return(0);
00833 
00834     if (totalcount > 0) {
00835         expected /= totalcount;
00836         retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
00837         if (retval == EOF) return(0);
00838         retval = fprintf(fp," (expected bin value = %g)\nBy quotient:",
00839                          expected);
00840         if (retval == EOF) return(0);
00841         for (i = nbins - 1; i>=0; i--) {
00842             retval = fprintf(fp," %.0f", hystogramQ[i]);
00843             if (retval == EOF) return(0);
00844         }
00845         retval = fprintf(fp,"\nBy residue: ");
00846         if (retval == EOF) return(0);
00847         for (i = nbins - 1; i>=0; i--) {
00848             retval = fprintf(fp," %.0f", hystogramR[i]);
00849             if (retval == EOF) return(0);
00850         }
00851         retval = fprintf(fp,"\n");
00852         if (retval == EOF) return(0);
00853     }
00854 
00855     FREE(hystogramQ);
00856     FREE(hystogramR);
00857 #else
00858     for (i = 0; i < slots; i++) {
00859         nzeroes += cache[i].h == 0;
00860     }
00861     exUsed = 100.0 *
00862         (1.0 - exp(-(table->cacheinserts - table->cacheLastInserts) /
00863                    (double) slots));
00864     retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
00865                      100.0 - (double) nzeroes * 100.0 / (double) slots,
00866                      exUsed);
00867     if (retval == EOF) return(0);
00868 #endif
00869     return(1);
00870 
00871 } /* end of cuddCacheProfile */

void cuddCacheResize ( DdManager table  ) 

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

Synopsis [Resizes the cache.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 886 of file cuddCache.c.

00888 {
00889     DdCache *cache, *oldcache, *oldacache, *entry, *old;
00890     int i;
00891     int posn, shift;
00892     unsigned int slots, oldslots;
00893     double offset;
00894     int moved = 0;
00895     extern DD_OOMFP MMoutOfMemory;
00896     DD_OOMFP saveHandler;
00897 #ifndef DD_CACHE_PROFILE
00898     ptruint misalignment;
00899     DdNodePtr *mem;
00900 #endif
00901 
00902     oldcache = table->cache;
00903     oldacache = table->acache;
00904     oldslots = table->cacheSlots;
00905     slots = table->cacheSlots = oldslots << 1;
00906 
00907 #ifdef DD_VERBOSE
00908     (void) fprintf(table->err,"Resizing the cache from %d to %d entries\n",
00909                    oldslots, slots);
00910     (void) fprintf(table->err,
00911                    "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
00912                    table->cacheHits, table->cacheMisses,
00913                    table->cacheHits / (table->cacheHits + table->cacheMisses));
00914 #endif
00915 
00916     saveHandler = MMoutOfMemory;
00917     MMoutOfMemory = Cudd_OutOfMem;
00918     table->acache = cache = ALLOC(DdCache,slots+1);
00919     MMoutOfMemory = saveHandler;
00920     /* If we fail to allocate the new table we just give up. */
00921     if (cache == NULL) {
00922 #ifdef DD_VERBOSE
00923         (void) fprintf(table->err,"Resizing failed. Giving up.\n");
00924 #endif
00925         table->cacheSlots = oldslots;
00926         table->acache = oldacache;
00927         /* Do not try to resize again. */
00928         table->maxCacheHard = oldslots - 1;
00929         table->cacheSlack = - (int) (oldslots + 1);
00930         return;
00931     }
00932     /* If the size of the cache entry is a power of 2, we want to
00933     ** enforce alignment to that power of two. This happens when
00934     ** DD_CACHE_PROFILE is not defined. */
00935 #ifdef DD_CACHE_PROFILE
00936     table->cache = cache;
00937 #else
00938     mem = (DdNodePtr *) cache;
00939     misalignment = (ptruint) mem & (sizeof(DdCache) - 1);
00940     mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr);
00941     table->cache = cache = (DdCache *) mem;
00942     assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0);
00943 #endif
00944     shift = --(table->cacheShift);
00945     table->memused += (slots - oldslots) * sizeof(DdCache);
00946     table->cacheSlack -= slots; /* need these many slots to double again */
00947 
00948     /* Clear new cache. */
00949     for (i = 0; (unsigned) i < slots; i++) {
00950         cache[i].data = NULL;
00951         cache[i].h = 0;
00952 #ifdef DD_CACHE_PROFILE
00953         cache[i].count = 0;
00954 #endif
00955     }
00956 
00957     /* Copy from old cache to new one. */
00958     for (i = 0; (unsigned) i < oldslots; i++) {
00959         old = &oldcache[i];
00960         if (old->data != NULL) {
00961             posn = ddCHash2(old->h,old->f,old->g,shift);
00962             entry = &cache[posn];
00963             entry->f = old->f;
00964             entry->g = old->g;
00965             entry->h = old->h;
00966             entry->data = old->data;
00967 #ifdef DD_CACHE_PROFILE
00968             entry->count = 1;
00969 #endif
00970             moved++;
00971         }
00972     }
00973 
00974     FREE(oldacache);
00975 
00976     /* Reinitialize measurements so as to avoid division by 0 and
00977     ** immediate resizing.
00978     */
00979     offset = (double) (int) (slots * table->minHit + 1);
00980     table->totCacheMisses += table->cacheMisses - offset;
00981     table->cacheMisses = offset;
00982     table->totCachehits += table->cacheHits;
00983     table->cacheHits = 0;
00984     table->cacheLastInserts = table->cacheinserts - (double) moved;
00985 
00986 } /* 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 1033 of file cuddCache.c.

01035 {
01036     int floorLog = 0;
01037 #ifdef DD_DEBUG
01038     assert(value > 0);
01039 #endif
01040     while (value > 1) {
01041         floorLog++;
01042         value >>= 1;
01043     }
01044     return(floorLog);
01045 
01046 } /* 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 687 of file cuddCache.c.

00693 {
00694     int posn;
00695     DdCache *en,*cache;
00696     ptruint uf, ug, uh;
00697 
00698     uf = (ptruint) f | (op & 0xe);
00699     ug = (ptruint) g | (op >> 4);
00700     uh = (ptruint) h;
00701 
00702     cache = table->cache;
00703 #ifdef DD_DEBUG
00704     if (cache == NULL) {
00705         return(NULL);
00706     }
00707 #endif
00708     posn = ddCHash2(uh,uf,ug,table->cacheShift);
00709     en = &cache[posn];
00710 
00711     /* We do not reclaim here because the result should not be
00712      * referenced, but only tested for being a constant.
00713      */
00714     if (en->data != NULL &&
00715         en->f == (DdNodePtr)uf && en->g == (DdNodePtr)ug && en->h == uh) {
00716         table->cacheHits++;
00717         return(en->data);
00718     }
00719 
00720     /* Cache miss: decide whether to resize. */
00721     table->cacheMisses++;
00722 
00723     if (table->cacheSlack >= 0 &&
00724         table->cacheHits > table->cacheMisses * table->minHit) {
00725         cuddCacheResize(table);
00726     }
00727 
00728     return(NULL);
00729 
00730 } /* 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 132 of file cuddCache.c.

00136 {
00137     int i;
00138     unsigned int logSize;
00139 #ifndef DD_CACHE_PROFILE
00140     DdNodePtr *mem;
00141     ptruint offset;
00142 #endif
00143 
00144     /* Round cacheSize to largest power of 2 not greater than the requested
00145     ** initial cache size. */
00146     logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
00147     cacheSize = 1 << logSize;
00148     unique->acache = ALLOC(DdCache,cacheSize+1);
00149     if (unique->acache == NULL) {
00150         unique->errorCode = CUDD_MEMORY_OUT;
00151         return(0);
00152     }
00153     /* If the size of the cache entry is a power of 2, we want to
00154     ** enforce alignment to that power of two. This happens when
00155     ** DD_CACHE_PROFILE is not defined. */
00156 #ifdef DD_CACHE_PROFILE
00157     unique->cache = unique->acache;
00158     unique->memused += (cacheSize) * sizeof(DdCache);
00159 #else
00160     mem = (DdNodePtr *) unique->acache;
00161     offset = (ptruint) mem & (sizeof(DdCache) - 1);
00162     mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr);
00163     unique->cache = (DdCache *) mem;
00164     assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0);
00165     unique->memused += (cacheSize+1) * sizeof(DdCache);
00166 #endif
00167     unique->cacheSlots = cacheSize;
00168     unique->cacheShift = sizeof(int) * 8 - logSize;
00169     unique->maxCacheHard = maxCacheSize;
00170     /* If cacheSlack is non-negative, we can resize. */
00171     unique->cacheSlack = (int) ddMin(maxCacheSize,
00172         DD_MAX_CACHE_TO_SLOTS_RATIO*unique->slots) -
00173         2 * (int) cacheSize;
00174     Cudd_SetMinHit(unique,DD_MIN_HIT);
00175     /* Initialize to avoid division by 0 and immediate resizing. */
00176     unique->cacheMisses = (double) (int) (cacheSize * unique->minHit + 1);
00177     unique->cacheHits = 0;
00178     unique->totCachehits = 0;
00179     /* The sum of cacheMisses and totCacheMisses is always correct,
00180     ** even though cacheMisses is larger than it should for the reasons
00181     ** explained above. */
00182     unique->totCacheMisses = -unique->cacheMisses;
00183     unique->cachecollisions = 0;
00184     unique->cacheinserts = 0;
00185     unique->cacheLastInserts = 0;
00186     unique->cachedeletions = 0;
00187 
00188     /* Initialize the cache */
00189     for (i = 0; (unsigned) i < cacheSize; i++) {
00190         unique->cache[i].h = 0; /* unused slots */
00191         unique->cache[i].data = NULL; /* invalid entry */
00192 #ifdef DD_CACHE_PROFILE
00193         unique->cache[i].count = 0;
00194 #endif
00195     }
00196 
00197     return(1);
00198 
00199 } /* end of cuddInitCache */


Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddCache.c,v 1.34 2009/02/19 16:17:50 fabio 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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 92 of file cuddCache.c.


Generated on Tue Jan 12 13:57:18 2010 for glu-2.2 by  doxygen 1.6.1