00001
00048 #include "util_hack.h"
00049 #include "cuddInt.h"
00050
00051
00052
00053
00054
00055 #define DD_MAX_HASHTABLE_DENSITY 2
00056
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066
00067
00068
00069
00070
00071 #ifndef lint
00072 static char rcsid[] DD_UNUSED = "$Id: cuddLCache.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
00073 #endif
00074
00075
00076
00077
00078
00090 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00091 #define ddLCHash2(f,g,shift) \
00092 ((((unsigned)(unsigned long)(f) * DD_P1 + \
00093 (unsigned)(unsigned long)(g)) * DD_P2) >> (shift))
00094 #else
00095 #define ddLCHash2(f,g,shift) \
00096 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift))
00097 #endif
00098
00099
00111 #define ddLCHash3(f,g,h,shift) ddCHash2(f,g,h,shift)
00112
00113
00116
00117
00118
00119
00120 static void cuddLocalCacheResize ARGS((DdLocalCache *cache));
00121 DD_INLINE static unsigned int ddLCHash ARGS((DdNodePtr *key, unsigned int keysize, int shift));
00122 static void cuddLocalCacheAddToList ARGS((DdLocalCache *cache));
00123 static void cuddLocalCacheRemoveFromList ARGS((DdLocalCache *cache));
00124 static int cuddHashTableResize ARGS((DdHashTable *hash));
00125 DD_INLINE static DdHashItem * cuddHashTableAlloc ARGS((DdHashTable *hash));
00126
00130
00131
00132
00133
00134
00135
00136
00137
00138
00151 DdLocalCache *
00152 cuddLocalCacheInit(
00153 DdManager * manager ,
00154 unsigned int keySize ,
00155 unsigned int cacheSize ,
00156 unsigned int maxCacheSize )
00157 {
00158 DdLocalCache *cache;
00159 int logSize;
00160
00161 cache = ALLOC(DdLocalCache,1);
00162 if (cache == NULL) {
00163 manager->errorCode = CUDD_MEMORY_OUT;
00164 return(NULL);
00165 }
00166 cache->manager = manager;
00167 cache->keysize = keySize;
00168 cache->itemsize = (keySize + 1) * sizeof(DdNode *);
00169 #ifdef DD_CACHE_PROFILE
00170 cache->itemsize += sizeof(ptrint);
00171 #endif
00172 logSize = cuddComputeFloorLog2(ddMax(cacheSize,manager->slots/2));
00173 cacheSize = 1 << logSize;
00174 cache->item = (DdLocalCacheItem *)
00175 ALLOC(char, cacheSize * cache->itemsize);
00176 if (cache->item == NULL) {
00177 manager->errorCode = CUDD_MEMORY_OUT;
00178 FREE(cache);
00179 return(NULL);
00180 }
00181 cache->slots = cacheSize;
00182 cache->shift = sizeof(int) * 8 - logSize;
00183 cache->maxslots = ddMin(maxCacheSize,manager->slots);
00184 cache->minHit = manager->minHit;
00185
00186 cache->lookUps = (double) (int) (cacheSize * cache->minHit + 1);
00187 cache->hits = 0;
00188 manager->memused += cacheSize * cache->itemsize + sizeof(DdLocalCache);
00189
00190
00191 memset(cache->item, 0, cacheSize * cache->itemsize);
00192
00193
00194 cuddLocalCacheAddToList(cache);
00195
00196 return(cache);
00197
00198 }
00199
00200
00214 void
00215 cuddLocalCacheQuit(
00216 DdLocalCache * cache )
00217 {
00218 cache->manager->memused -=
00219 cache->slots * cache->itemsize + sizeof(DdLocalCache);
00220 cuddLocalCacheRemoveFromList(cache);
00221 FREE(cache->item);
00222 FREE(cache);
00223
00224 return;
00225
00226 }
00227
00228
00240 void
00241 cuddLocalCacheInsert(
00242 DdLocalCache * cache,
00243 DdNodePtr * key,
00244 DdNode * value)
00245 {
00246 unsigned int posn;
00247 DdLocalCacheItem *entry;
00248
00249 posn = ddLCHash(key,cache->keysize,cache->shift);
00250 entry = (DdLocalCacheItem *) ((char *) cache->item +
00251 posn * cache->itemsize);
00252 memcpy(entry->key,key,cache->keysize * sizeof(DdNode *));
00253 entry->value = value;
00254 #ifdef DD_CACHE_PROFILE
00255 entry->count++;
00256 #endif
00257
00258 }
00259
00260
00273 DdNode *
00274 cuddLocalCacheLookup(
00275 DdLocalCache * cache,
00276 DdNodePtr * key)
00277 {
00278 unsigned int posn;
00279 DdLocalCacheItem *entry;
00280 DdNode *value;
00281
00282 cache->lookUps++;
00283 posn = ddLCHash(key,cache->keysize,cache->shift);
00284 entry = (DdLocalCacheItem *) ((char *) cache->item +
00285 posn * cache->itemsize);
00286 if (entry->value != NULL &&
00287 memcmp(key,entry->key,cache->keysize*sizeof(DdNode *)) == 0) {
00288 cache->hits++;
00289 value = Cudd_Regular(entry->value);
00290 if (value->ref == 0) {
00291 cuddReclaim(cache->manager,value);
00292 }
00293 return(entry->value);
00294 }
00295
00296
00297
00298 if (cache->slots < cache->maxslots &&
00299 cache->hits > cache->lookUps * cache->minHit) {
00300 cuddLocalCacheResize(cache);
00301 }
00302
00303 return(NULL);
00304
00305 }
00306
00307
00320 void
00321 cuddLocalCacheClearDead(
00322 DdManager * manager)
00323 {
00324 DdLocalCache *cache = manager->localCaches;
00325 unsigned int keysize;
00326 unsigned int itemsize;
00327 unsigned int slots;
00328 DdLocalCacheItem *item;
00329 DdNodePtr *key;
00330 unsigned int i, j;
00331
00332 while (cache != NULL) {
00333 keysize = cache->keysize;
00334 itemsize = cache->itemsize;
00335 slots = cache->slots;
00336 item = cache->item;
00337 for (i = 0; i < slots; i++) {
00338 if (item->value != NULL && Cudd_Regular(item->value)->ref == 0) {
00339 item->value = NULL;
00340 } else {
00341 key = item->key;
00342 for (j = 0; j < keysize; j++) {
00343 if (Cudd_Regular(key[j])->ref == 0) {
00344 item->value = NULL;
00345 break;
00346 }
00347 }
00348 }
00349 item = (DdLocalCacheItem *) ((char *) item + itemsize);
00350 }
00351 cache = cache->next;
00352 }
00353 return;
00354
00355 }
00356
00357
00370 void
00371 cuddLocalCacheClearAll(
00372 DdManager * manager)
00373 {
00374 DdLocalCache *cache = manager->localCaches;
00375
00376 while (cache != NULL) {
00377 memset(cache->item, 0, cache->slots * cache->itemsize);
00378 cache = cache->next;
00379 }
00380 return;
00381
00382 }
00383
00384
00385 #ifdef DD_CACHE_PROFILE
00386
00387 #define DD_HYSTO_BINS 8
00388
00401 int
00402 cuddLocalCacheProfile(
00403 DdLocalCache * cache)
00404 {
00405 double count, mean, meansq, stddev, expected;
00406 long max, min;
00407 int imax, imin;
00408 int i, retval, slots;
00409 long *hystogram;
00410 int nbins = DD_HYSTO_BINS;
00411 int bin;
00412 long thiscount;
00413 double totalcount;
00414 int nzeroes;
00415 DdLocalCacheItem *entry;
00416 FILE *fp = cache->manager->out;
00417
00418 slots = cache->slots;
00419
00420 meansq = mean = expected = 0.0;
00421 max = min = (long) cache->item[0].count;
00422 imax = imin = nzeroes = 0;
00423 totalcount = 0.0;
00424
00425 hystogram = ALLOC(long, nbins);
00426 if (hystogram == NULL) {
00427 return(0);
00428 }
00429 for (i = 0; i < nbins; i++) {
00430 hystogram[i] = 0;
00431 }
00432
00433 for (i = 0; i < slots; i++) {
00434 entry = (DdLocalCacheItem *) ((char *) cache->item +
00435 i * cache->itemsize);
00436 thiscount = (long) entry->count;
00437 if (thiscount > max) {
00438 max = thiscount;
00439 imax = i;
00440 }
00441 if (thiscount < min) {
00442 min = thiscount;
00443 imin = i;
00444 }
00445 if (thiscount == 0) {
00446 nzeroes++;
00447 }
00448 count = (double) thiscount;
00449 mean += count;
00450 meansq += count * count;
00451 totalcount += count;
00452 expected += count * (double) i;
00453 bin = (i * nbins) / slots;
00454 hystogram[bin] += thiscount;
00455 }
00456 mean /= (double) slots;
00457 meansq /= (double) slots;
00458 stddev = sqrt(meansq - mean*mean);
00459
00460 retval = fprintf(fp,"Cache stats: slots = %d average = %g ", slots, mean);
00461 if (retval == EOF) return(0);
00462 retval = fprintf(fp,"standard deviation = %g\n", stddev);
00463 if (retval == EOF) return(0);
00464 retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
00465 if (retval == EOF) return(0);
00466 retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
00467 if (retval == EOF) return(0);
00468 retval = fprintf(fp,"Cache unused slots = %d\n", nzeroes);
00469 if (retval == EOF) return(0);
00470
00471 if (totalcount) {
00472 expected /= totalcount;
00473 retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
00474 if (retval == EOF) return(0);
00475 retval = fprintf(fp," (expected bin value = %g)\n# ", expected);
00476 if (retval == EOF) return(0);
00477 for (i = nbins - 1; i>=0; i--) {
00478 retval = fprintf(fp,"%ld ", hystogram[i]);
00479 if (retval == EOF) return(0);
00480 }
00481 retval = fprintf(fp,"\n");
00482 if (retval == EOF) return(0);
00483 }
00484
00485 FREE(hystogram);
00486 return(1);
00487
00488 }
00489 #endif
00490
00491
00504 DdHashTable *
00505 cuddHashTableInit(
00506 DdManager * manager,
00507 unsigned int keySize,
00508 unsigned int initSize)
00509 {
00510 DdHashTable *hash;
00511 int logSize;
00512
00513 #ifdef __osf__
00514 #pragma pointer_size save
00515 #pragma pointer_size short
00516 #endif
00517 hash = ALLOC(DdHashTable, 1);
00518 if (hash == NULL) {
00519 manager->errorCode = CUDD_MEMORY_OUT;
00520 return(NULL);
00521 }
00522 hash->keysize = keySize;
00523 hash->manager = manager;
00524 hash->memoryList = NULL;
00525 hash->nextFree = NULL;
00526 hash->itemsize = (keySize + 1) * sizeof(DdNode *) +
00527 sizeof(ptrint) + sizeof(DdHashItem *);
00528
00529 if (initSize < 2) initSize = 2;
00530 logSize = cuddComputeFloorLog2(initSize);
00531 hash->numBuckets = 1 << logSize;
00532 hash->shift = sizeof(int) * 8 - logSize;
00533 hash->bucket = ALLOC(DdHashItem *, hash->numBuckets);
00534 if (hash->bucket == NULL) {
00535 manager->errorCode = CUDD_MEMORY_OUT;
00536 FREE(hash);
00537 return(NULL);
00538 }
00539 memset(hash->bucket, 0, hash->numBuckets * sizeof(DdHashItem *));
00540 hash->size = 0;
00541 hash->maxsize = hash->numBuckets * DD_MAX_HASHTABLE_DENSITY;
00542 #ifdef __osf__
00543 #pragma pointer_size restore
00544 #endif
00545 return(hash);
00546
00547 }
00548
00549
00561 void
00562 cuddHashTableQuit(
00563 DdHashTable * hash)
00564 {
00565 #ifdef __osf__
00566 #pragma pointer_size save
00567 #pragma pointer_size short
00568 #endif
00569 unsigned int i;
00570 DdManager *dd = hash->manager;
00571 DdHashItem *bucket;
00572 DdHashItem **memlist, **nextmem;
00573 unsigned int numBuckets = hash->numBuckets;
00574
00575 for (i = 0; i < numBuckets; i++) {
00576 bucket = hash->bucket[i];
00577 while (bucket != NULL) {
00578 Cudd_RecursiveDeref(dd, bucket->value);
00579 bucket = bucket->next;
00580 }
00581 }
00582
00583 memlist = hash->memoryList;
00584 while (memlist != NULL) {
00585 nextmem = (DdHashItem **) memlist[0];
00586 FREE(memlist);
00587 memlist = nextmem;
00588 }
00589
00590 FREE(hash->bucket);
00591 FREE(hash);
00592 #ifdef __osf__
00593 #pragma pointer_size restore
00594 #endif
00595
00596 return;
00597
00598 }
00599
00600
00614 int
00615 cuddHashTableInsert(
00616 DdHashTable * hash,
00617 DdNodePtr * key,
00618 DdNode * value,
00619 ptrint count)
00620 {
00621 int result;
00622 unsigned int posn;
00623 DdHashItem *item;
00624 unsigned int i;
00625
00626 #ifdef DD_DEBUG
00627 assert(hash->keysize > 3);
00628 #endif
00629
00630 if (hash->size > hash->maxsize) {
00631 result = cuddHashTableResize(hash);
00632 if (result == 0) return(0);
00633 }
00634 item = cuddHashTableAlloc(hash);
00635 if (item == NULL) return(0);
00636 hash->size++;
00637 item->value = value;
00638 cuddRef(value);
00639 item->count = count;
00640 for (i = 0; i < hash->keysize; i++) {
00641 item->key[i] = key[i];
00642 }
00643 posn = ddLCHash(key,hash->keysize,hash->shift);
00644 item->next = hash->bucket[posn];
00645 hash->bucket[posn] = item;
00646
00647 return(1);
00648
00649 }
00650
00651
00669 DdNode *
00670 cuddHashTableLookup(
00671 DdHashTable * hash,
00672 DdNodePtr * key)
00673 {
00674 unsigned int posn;
00675 DdHashItem *item, *prev;
00676 unsigned int i, keysize;
00677
00678 #ifdef DD_DEBUG
00679 assert(hash->keysize > 3);
00680 #endif
00681
00682 posn = ddLCHash(key,hash->keysize,hash->shift);
00683 item = hash->bucket[posn];
00684 prev = NULL;
00685
00686 keysize = hash->keysize;
00687 while (item != NULL) {
00688 DdNodePtr *key2 = item->key;
00689 int equal = 1;
00690 for (i = 0; i < keysize; i++) {
00691 if (key[i] != key2[i]) {
00692 equal = 0;
00693 break;
00694 }
00695 }
00696 if (equal) {
00697 DdNode *value = item->value;
00698 cuddSatDec(item->count);
00699 if (item->count == 0) {
00700 cuddDeref(value);
00701 if (prev == NULL) {
00702 hash->bucket[posn] = item->next;
00703 } else {
00704 prev->next = item->next;
00705 }
00706 item->next = hash->nextFree;
00707 hash->nextFree = item;
00708 hash->size--;
00709 }
00710 return(value);
00711 }
00712 prev = item;
00713 item = item->next;
00714 }
00715 return(NULL);
00716
00717 }
00718
00719
00733 int
00734 cuddHashTableInsert1(
00735 DdHashTable * hash,
00736 DdNode * f,
00737 DdNode * value,
00738 ptrint count)
00739 {
00740 int result;
00741 unsigned int posn;
00742 DdHashItem *item;
00743
00744 #ifdef DD_DEBUG
00745 assert(hash->keysize == 1);
00746 #endif
00747
00748 if (hash->size > hash->maxsize) {
00749 result = cuddHashTableResize(hash);
00750 if (result == 0) return(0);
00751 }
00752 item = cuddHashTableAlloc(hash);
00753 if (item == NULL) return(0);
00754 hash->size++;
00755 item->value = value;
00756 cuddRef(value);
00757 item->count = count;
00758 item->key[0] = f;
00759 posn = ddLCHash2(f,f,hash->shift);
00760 item->next = hash->bucket[posn];
00761 hash->bucket[posn] = item;
00762
00763 return(1);
00764
00765 }
00766
00767
00785 DdNode *
00786 cuddHashTableLookup1(
00787 DdHashTable * hash,
00788 DdNode * f)
00789 {
00790 unsigned int posn;
00791 DdHashItem *item, *prev;
00792
00793 #ifdef DD_DEBUG
00794 assert(hash->keysize == 1);
00795 #endif
00796
00797 posn = ddLCHash2(f,f,hash->shift);
00798 item = hash->bucket[posn];
00799 prev = NULL;
00800
00801 while (item != NULL) {
00802 DdNodePtr *key = item->key;
00803 if (f == key[0]) {
00804 DdNode *value = item->value;
00805 cuddSatDec(item->count);
00806 if (item->count == 0) {
00807 cuddDeref(value);
00808 if (prev == NULL) {
00809 hash->bucket[posn] = item->next;
00810 } else {
00811 prev->next = item->next;
00812 }
00813 item->next = hash->nextFree;
00814 hash->nextFree = item;
00815 hash->size--;
00816 }
00817 return(value);
00818 }
00819 prev = item;
00820 item = item->next;
00821 }
00822 return(NULL);
00823
00824 }
00825
00826
00840 int
00841 cuddHashTableInsert2(
00842 DdHashTable * hash,
00843 DdNode * f,
00844 DdNode * g,
00845 DdNode * value,
00846 ptrint count)
00847 {
00848 int result;
00849 unsigned int posn;
00850 DdHashItem *item;
00851
00852 #ifdef DD_DEBUG
00853 assert(hash->keysize == 2);
00854 #endif
00855
00856 if (hash->size > hash->maxsize) {
00857 result = cuddHashTableResize(hash);
00858 if (result == 0) return(0);
00859 }
00860 item = cuddHashTableAlloc(hash);
00861 if (item == NULL) return(0);
00862 hash->size++;
00863 item->value = value;
00864 cuddRef(value);
00865 item->count = count;
00866 item->key[0] = f;
00867 item->key[1] = g;
00868 posn = ddLCHash2(f,g,hash->shift);
00869 item->next = hash->bucket[posn];
00870 hash->bucket[posn] = item;
00871
00872 return(1);
00873
00874 }
00875
00876
00894 DdNode *
00895 cuddHashTableLookup2(
00896 DdHashTable * hash,
00897 DdNode * f,
00898 DdNode * g)
00899 {
00900 unsigned int posn;
00901 DdHashItem *item, *prev;
00902
00903 #ifdef DD_DEBUG
00904 assert(hash->keysize == 2);
00905 #endif
00906
00907 posn = ddLCHash2(f,g,hash->shift);
00908 item = hash->bucket[posn];
00909 prev = NULL;
00910
00911 while (item != NULL) {
00912 DdNodePtr *key = item->key;
00913 if ((f == key[0]) && (g == key[1])) {
00914 DdNode *value = item->value;
00915 cuddSatDec(item->count);
00916 if (item->count == 0) {
00917 cuddDeref(value);
00918 if (prev == NULL) {
00919 hash->bucket[posn] = item->next;
00920 } else {
00921 prev->next = item->next;
00922 }
00923 item->next = hash->nextFree;
00924 hash->nextFree = item;
00925 hash->size--;
00926 }
00927 return(value);
00928 }
00929 prev = item;
00930 item = item->next;
00931 }
00932 return(NULL);
00933
00934 }
00935
00936
00950 int
00951 cuddHashTableInsert3(
00952 DdHashTable * hash,
00953 DdNode * f,
00954 DdNode * g,
00955 DdNode * h,
00956 DdNode * value,
00957 ptrint count)
00958 {
00959 int result;
00960 unsigned int posn;
00961 DdHashItem *item;
00962
00963 #ifdef DD_DEBUG
00964 assert(hash->keysize == 3);
00965 #endif
00966
00967 if (hash->size > hash->maxsize) {
00968 result = cuddHashTableResize(hash);
00969 if (result == 0) return(0);
00970 }
00971 item = cuddHashTableAlloc(hash);
00972 if (item == NULL) return(0);
00973 hash->size++;
00974 item->value = value;
00975 cuddRef(value);
00976 item->count = count;
00977 item->key[0] = f;
00978 item->key[1] = g;
00979 item->key[2] = h;
00980 posn = ddLCHash3(f,g,h,hash->shift);
00981 item->next = hash->bucket[posn];
00982 hash->bucket[posn] = item;
00983
00984 return(1);
00985
00986 }
00987
00988
01006 DdNode *
01007 cuddHashTableLookup3(
01008 DdHashTable * hash,
01009 DdNode * f,
01010 DdNode * g,
01011 DdNode * h)
01012 {
01013 unsigned int posn;
01014 DdHashItem *item, *prev;
01015
01016 #ifdef DD_DEBUG
01017 assert(hash->keysize == 3);
01018 #endif
01019
01020 posn = ddLCHash3(f,g,h,hash->shift);
01021 item = hash->bucket[posn];
01022 prev = NULL;
01023
01024 while (item != NULL) {
01025 DdNodePtr *key = item->key;
01026 if ((f == key[0]) && (g == key[1]) && (h == key[2])) {
01027 DdNode *value = item->value;
01028 cuddSatDec(item->count);
01029 if (item->count == 0) {
01030 cuddDeref(value);
01031 if (prev == NULL) {
01032 hash->bucket[posn] = item->next;
01033 } else {
01034 prev->next = item->next;
01035 }
01036 item->next = hash->nextFree;
01037 hash->nextFree = item;
01038 hash->size--;
01039 }
01040 return(value);
01041 }
01042 prev = item;
01043 item = item->next;
01044 }
01045 return(NULL);
01046
01047 }
01048
01049
01050
01051
01052
01053
01054
01066 static void
01067 cuddLocalCacheResize(
01068 DdLocalCache * cache)
01069 {
01070 DdLocalCacheItem *item, *olditem, *entry, *old;
01071 int i, shift;
01072 unsigned int posn;
01073 unsigned int slots, oldslots;
01074 extern void (*MMoutOfMemory)(long);
01075 void (*saveHandler)(long);
01076
01077 olditem = cache->item;
01078 oldslots = cache->slots;
01079 slots = cache->slots = oldslots << 1;
01080
01081 #ifdef DD_VERBOSE
01082 (void) fprintf(cache->manager->err,
01083 "Resizing local cache from %d to %d entries\n",
01084 oldslots, slots);
01085 (void) fprintf(cache->manager->err,
01086 "\thits = %.0f\tlookups = %.0f\thit ratio = %5.3f\n",
01087 cache->hits, cache->lookUps, cache->hits / cache->lookUps);
01088 #endif
01089
01090 saveHandler = MMoutOfMemory;
01091 MMoutOfMemory = Cudd_OutOfMem;
01092 cache->item = item =
01093 (DdLocalCacheItem *) ALLOC(char, slots * cache->itemsize);
01094 MMoutOfMemory = saveHandler;
01095
01096 if (item == NULL) {
01097 #ifdef DD_VERBOSE
01098 (void) fprintf(cache->manager->err,"Resizing failed. Giving up.\n");
01099 #endif
01100 cache->slots = oldslots;
01101 cache->item = olditem;
01102
01103 cache->maxslots = oldslots - 1;
01104 return;
01105 }
01106 shift = --(cache->shift);
01107 cache->manager->memused += (slots - oldslots) * cache->itemsize;
01108
01109
01110 memset(item, 0, slots * cache->itemsize);
01111
01112
01113 for (i = 0; (unsigned) i < oldslots; i++) {
01114 old = (DdLocalCacheItem *) ((char *) olditem + i * cache->itemsize);
01115 if (old->value != NULL) {
01116 posn = ddLCHash(old->key,cache->keysize,slots);
01117 entry = (DdLocalCacheItem *) ((char *) item +
01118 posn * cache->itemsize);
01119 memcpy(entry->key,old->key,cache->keysize*sizeof(DdNode *));
01120 entry->value = old->value;
01121 }
01122 }
01123
01124 FREE(olditem);
01125
01126
01127
01128
01129 cache->lookUps = (double) (int) (slots * cache->minHit + 1);
01130 cache->hits = 0;
01131
01132 }
01133
01134
01147 DD_INLINE
01148 static unsigned int
01149 ddLCHash(
01150 DdNodePtr * key,
01151 unsigned int keysize,
01152 int shift)
01153 {
01154 unsigned int val = (unsigned int) (ptrint) key[0];
01155 unsigned int i;
01156
01157 for (i = 1; i < keysize; i++) {
01158 val = val * DD_P1 + (int) (ptrint) key[i];
01159 }
01160
01161 return(val >> shift);
01162
01163 }
01164
01165
01177 static void
01178 cuddLocalCacheAddToList(
01179 DdLocalCache * cache)
01180 {
01181 DdManager *manager = cache->manager;
01182
01183 cache->next = manager->localCaches;
01184 manager->localCaches = cache;
01185 return;
01186
01187 }
01188
01189
01201 static void
01202 cuddLocalCacheRemoveFromList(
01203 DdLocalCache * cache)
01204 {
01205 DdManager *manager = cache->manager;
01206 #ifdef __osf__
01207 #pragma pointer_size save
01208 #pragma pointer_size short
01209 #endif
01210 DdLocalCache **prevCache, *nextCache;
01211 #ifdef __osf__
01212 #pragma pointer_size restore
01213 #endif
01214
01215 prevCache = &(manager->localCaches);
01216 nextCache = manager->localCaches;
01217
01218 while (nextCache != NULL) {
01219 if (nextCache == cache) {
01220 *prevCache = nextCache->next;
01221 return;
01222 }
01223 prevCache = &(nextCache->next);
01224 nextCache = nextCache->next;
01225 }
01226 return;
01227
01228 }
01229
01230
01243 static int
01244 cuddHashTableResize(
01245 DdHashTable * hash)
01246 {
01247 int j;
01248 unsigned int posn;
01249 DdHashItem *item;
01250 DdHashItem *next;
01251 #ifdef __osf__
01252 #pragma pointer_size save
01253 #pragma pointer_size short
01254 #endif
01255 DdNode **key;
01256 int numBuckets;
01257 DdHashItem **buckets;
01258 DdHashItem **oldBuckets = hash->bucket;
01259 #ifdef __osf__
01260 #pragma pointer_size restore
01261 #endif
01262 int shift;
01263 int oldNumBuckets = hash->numBuckets;
01264 extern void (*MMoutOfMemory)(long);
01265 void (*saveHandler)(long);
01266
01267
01268 numBuckets = oldNumBuckets << 1;
01269 saveHandler = MMoutOfMemory;
01270 MMoutOfMemory = Cudd_OutOfMem;
01271 #ifdef __osf__
01272 #pragma pointer_size save
01273 #pragma pointer_size short
01274 #endif
01275 buckets = ALLOC(DdHashItem *, numBuckets);
01276 MMoutOfMemory = saveHandler;
01277 if (buckets == NULL) {
01278 hash->maxsize <<= 1;
01279 return(1);
01280 }
01281
01282 hash->bucket = buckets;
01283 hash->numBuckets = numBuckets;
01284 shift = --(hash->shift);
01285 hash->maxsize <<= 1;
01286 memset(buckets, 0, numBuckets * sizeof(DdHashItem *));
01287 #ifdef __osf__
01288 #pragma pointer_size restore
01289 #endif
01290 if (hash->keysize == 1) {
01291 for (j = 0; j < oldNumBuckets; j++) {
01292 item = oldBuckets[j];
01293 while (item != NULL) {
01294 next = item->next;
01295 key = item->key;
01296 posn = ddLCHash2(key[0], key[0], shift);
01297 item->next = buckets[posn];
01298 buckets[posn] = item;
01299 item = next;
01300 }
01301 }
01302 } else if (hash->keysize == 2) {
01303 for (j = 0; j < oldNumBuckets; j++) {
01304 item = oldBuckets[j];
01305 while (item != NULL) {
01306 next = item->next;
01307 key = item->key;
01308 posn = ddLCHash2(key[0], key[1], shift);
01309 item->next = buckets[posn];
01310 buckets[posn] = item;
01311 item = next;
01312 }
01313 }
01314 } else if (hash->keysize == 3) {
01315 for (j = 0; j < oldNumBuckets; j++) {
01316 item = oldBuckets[j];
01317 while (item != NULL) {
01318 next = item->next;
01319 key = item->key;
01320 posn = ddLCHash3(key[0], key[1], key[2], shift);
01321 item->next = buckets[posn];
01322 buckets[posn] = item;
01323 item = next;
01324 }
01325 }
01326 } else {
01327 for (j = 0; j < oldNumBuckets; j++) {
01328 item = oldBuckets[j];
01329 while (item != NULL) {
01330 next = item->next;
01331 posn = ddLCHash(item->key, hash->keysize, shift);
01332 item->next = buckets[posn];
01333 buckets[posn] = item;
01334 item = next;
01335 }
01336 }
01337 }
01338 FREE(oldBuckets);
01339 return(1);
01340
01341 }
01342
01343
01358 DD_INLINE
01359 static DdHashItem *
01360 cuddHashTableAlloc(
01361 DdHashTable * hash)
01362 {
01363 int i;
01364 unsigned int itemsize = hash->itemsize;
01365 extern void (*MMoutOfMemory)(long);
01366 void (*saveHandler)(long);
01367 #ifdef __osf__
01368 #pragma pointer_size save
01369 #pragma pointer_size short
01370 #endif
01371 DdHashItem **mem, *thisOne, *next, *item;
01372
01373 if (hash->nextFree == NULL) {
01374 saveHandler = MMoutOfMemory;
01375 MMoutOfMemory = Cudd_OutOfMem;
01376 mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
01377 MMoutOfMemory = saveHandler;
01378 #ifdef __osf__
01379 #pragma pointer_size restore
01380 #endif
01381 if (mem == NULL) {
01382 if (hash->manager->stash != NULL) {
01383 FREE(hash->manager->stash);
01384 hash->manager->stash = NULL;
01385
01386 hash->manager->maxCacheHard = hash->manager->cacheSlots - 1;
01387 hash->manager->cacheSlack = -(hash->manager->cacheSlots + 1);
01388 for (i = 0; i < hash->manager->size; i++) {
01389 hash->manager->subtables[i].maxKeys <<= 2;
01390 }
01391 hash->manager->gcFrac = 0.2;
01392 hash->manager->minDead =
01393 (unsigned) (0.2 * (double) hash->manager->slots);
01394 #ifdef __osf__
01395 #pragma pointer_size save
01396 #pragma pointer_size short
01397 #endif
01398 mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
01399 #ifdef __osf__
01400 #pragma pointer_size restore
01401 #endif
01402 }
01403 if (mem == NULL) {
01404 (*MMoutOfMemory)((DD_MEM_CHUNK + 1) * itemsize);
01405 hash->manager->errorCode = CUDD_MEMORY_OUT;
01406 return(NULL);
01407 }
01408 }
01409
01410 mem[0] = (DdHashItem *) hash->memoryList;
01411 hash->memoryList = mem;
01412
01413 thisOne = (DdHashItem *) ((char *) mem + itemsize);
01414 hash->nextFree = thisOne;
01415 for (i = 1; i < DD_MEM_CHUNK; i++) {
01416 next = (DdHashItem *) ((char *) thisOne + itemsize);
01417 thisOne->next = next;
01418 thisOne = next;
01419 }
01420
01421 thisOne->next = NULL;
01422
01423 }
01424 item = hash->nextFree;
01425 hash->nextFree = item->next;
01426 return(item);
01427
01428 }