#include "util.h"
#include "cuddInt.h"
Go to the source code of this file.
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 */
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 */
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 */
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 */
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 */
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 */
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 */
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 */
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 */
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 */
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.