#include "util_hack.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 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 */
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 */
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 */
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.
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 */
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.