distr/cudd/cuddLCache.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddLCache.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for local caches.]
   8
   9   Description [Internal procedures included in this module:
  10                 <ul>
  11                 <li> cuddLocalCacheInit()
  12                 <li> cuddLocalCacheQuit()
  13                 <li> cuddLocalCacheInsert()
  14                 <li> cuddLocalCacheLookup()
  15                 <li> cuddLocalCacheClearDead()
  16                 <li> cuddLocalCacheClearAll()
  17                 <li> cuddLocalCacheProfile()
  18                 <li> cuddHashTableInit()
  19                 <li> cuddHashTableQuit()
  20                 <li> cuddHashTableInsert()
  21                 <li> cuddHashTableLookup()
  22                 <li> cuddHashTableInsert2()
  23                 <li> cuddHashTableLookup2()
  24                 <li> cuddHashTableInsert3()
  25                 <li> cuddHashTableLookup3()
  26                 </ul>
  27             Static procedures included in this module:
  28                 <ul>
  29                 <li> cuddLocalCacheResize()
  30                 <li> ddLCHash()
  31                 <li> cuddLocalCacheAddToList()
  32                 <li> cuddLocalCacheRemoveFromList()
  33                 <li> cuddHashTableResize()
  34                 <li> cuddHashTableAlloc()
  35                 </ul> ]
  36
  37   SeeAlso     []
  38
  39   Author      [Fabio Somenzi]
  40
  41   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  42
  43   All rights reserved.
  44
  45   Redistribution and use in source and binary forms, with or without
  46   modification, are permitted provided that the following conditions
  47   are met:
  48
  49   Redistributions of source code must retain the above copyright
  50   notice, this list of conditions and the following disclaimer.
  51
  52   Redistributions in binary form must reproduce the above copyright
  53   notice, this list of conditions and the following disclaimer in the
  54   documentation and/or other materials provided with the distribution.
  55
  56   Neither the name of the University of Colorado nor the names of its
  57   contributors may be used to endorse or promote products derived from
  58   this software without specific prior written permission.
  59
  60   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  61   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  62   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  63   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  64   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  65   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  66   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  67   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  68   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  69   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  70   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  71   POSSIBILITY OF SUCH DAMAGE.]
  72
  73 ******************************************************************************/
  74
  75 #include "util.h"
  76 #include "cuddInt.h"
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Constant declarations                                                     */
  80 /*---------------------------------------------------------------------------*/
  81
  82 #define DD_MAX_HASHTABLE_DENSITY 2      /* tells when to resize a table */
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Stucture declarations                                                     */
  86 /*---------------------------------------------------------------------------*/
  87
  88
  89 /*---------------------------------------------------------------------------*/
  90 /* Type declarations                                                         */
  91 /*---------------------------------------------------------------------------*/
  92
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Variable declarations                                                     */
  96 /*---------------------------------------------------------------------------*/
  97
  98 #ifndef lint
  99 static char rcsid[] DD_UNUSED = "$Id: cuddLCache.c,v 1.24 2009/03/08 02:49:02 fabio Exp $";
 100 #endif
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Macro declarations                                                        */
 104 /*---------------------------------------------------------------------------*/
 105
 106 /**Macro***********************************************************************
 107
 108   Synopsis    [Computes hash function for keys of two operands.]
 109
 110   Description []
 111
 112   SideEffects [None]
 113
 114   SeeAlso     [ddLCHash3 ddLCHash]
 115
 116 ******************************************************************************/
 117 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
 118 #define ddLCHash2(f,g,shift) \
 119 ((((unsigned)(ptruint)(f) * DD_P1 + \
 120    (unsigned)(ptruint)(g)) * DD_P2) >> (shift))
 121 #else
 122 #define ddLCHash2(f,g,shift) \
 123 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift))
 124 #endif
 125
 126
 127 /**Macro***********************************************************************
 128
 129   Synopsis    [Computes hash function for keys of three operands.]
 130
 131   Description []
 132
 133   SideEffects [None]
 134
 135   SeeAlso     [ddLCHash2 ddLCHash]
 136
 137 ******************************************************************************/
 138 #define ddLCHash3(f,g,h,shift) ddCHash2(f,g,h,shift)
 139
 140
 141 /**AutomaticStart*************************************************************/
 142
 143 /*---------------------------------------------------------------------------*/
 144 /* Static function prototypes                                                */
 145 /*---------------------------------------------------------------------------*/
 146
 147 static void cuddLocalCacheResize (DdLocalCache *cache);
 148 DD_INLINE static unsigned int ddLCHash (DdNodePtr *key, unsigned int keysize, int shift);
 149 static void cuddLocalCacheAddToList (DdLocalCache *cache);
 150 static void cuddLocalCacheRemoveFromList (DdLocalCache *cache);
 151 static int cuddHashTableResize (DdHashTable *hash);
 152 DD_INLINE static DdHashItem * cuddHashTableAlloc (DdHashTable *hash);
 153
 154 /**AutomaticEnd***************************************************************/
 155
 156
 157 /*---------------------------------------------------------------------------*/
 158 /* Definition of exported functions                                          */
 159 /*---------------------------------------------------------------------------*/
 160
 161 /*---------------------------------------------------------------------------*/
 162 /* Definition of internal functions                                          */
 163 /*---------------------------------------------------------------------------*/
 164
 165
 166 /**Function********************************************************************
 167
 168   Synopsis    [Initializes a local computed table.]
 169
 170   Description [Initializes a computed table.  Returns a pointer the
 171   the new local cache in case of success; NULL otherwise.]
 172
 173   SideEffects [None]
 174
 175   SeeAlso     [cuddInitCache]
 176
 177 ******************************************************************************/
 178 DdLocalCache *
 179 cuddLocalCacheInit(
 180   DdManager * manager /* manager */,
 181   unsigned int  keySize /* size of the key (number of operands) */,
 182   unsigned int  cacheSize /* Initial size of the cache */,
 183   unsigned int  maxCacheSize /* Size of the cache beyond which no resizing occurs */)
 184 {
 185     DdLocalCache *cache;
 186     int logSize;
 187
 188     cache = ALLOC(DdLocalCache,1);
 189     if (cache == NULL) {
 190         manager->errorCode = CUDD_MEMORY_OUT;
 191         return(NULL);
 192     }
 193     cache->manager = manager;
 194     cache->keysize = keySize;
 195     cache->itemsize = (keySize + 1) * sizeof(DdNode *);
 196 #ifdef DD_CACHE_PROFILE
 197     cache->itemsize += sizeof(ptrint);
 198 #endif
 199     logSize = cuddComputeFloorLog2(ddMax(cacheSize,manager->slots/2));
 200     cacheSize = 1 << logSize;
 201     cache->item = (DdLocalCacheItem *)
 202         ALLOC(char, cacheSize * cache->itemsize);
 203     if (cache->item == NULL) {
 204         manager->errorCode = CUDD_MEMORY_OUT;
 205         FREE(cache);
 206         return(NULL);
 207     }
 208     cache->slots = cacheSize;
 209     cache->shift = sizeof(int) * 8 - logSize;
 210     cache->maxslots = ddMin(maxCacheSize,manager->slots);
 211     cache->minHit = manager->minHit;
 212     /* Initialize to avoid division by 0 and immediate resizing. */
 213     cache->lookUps = (double) (int) (cacheSize * cache->minHit + 1);
 214     cache->hits = 0;
 215     manager->memused += cacheSize * cache->itemsize + sizeof(DdLocalCache);
 216
 217     /* Initialize the cache. */
 218     memset(cache->item, 0, cacheSize * cache->itemsize);
 219
 220     /* Add to manager's list of local caches for GC. */
 221     cuddLocalCacheAddToList(cache);
 222
 223     return(cache);
 224
 225 } /* end of cuddLocalCacheInit */
 226
 227
 228 /**Function********************************************************************
 229
 230   Synopsis    [Shuts down a local computed table.]
 231
 232   Description [Initializes the computed table. It is called by
 233   Cudd_Init. Returns a pointer the the new local cache in case of
 234   success; NULL otherwise.]
 235
 236   SideEffects [None]
 237
 238   SeeAlso     [cuddLocalCacheInit]
 239
 240 ******************************************************************************/
 241 void
 242 cuddLocalCacheQuit(
 243   DdLocalCache * cache /* cache to be shut down */)
 244 {
 245     cache->manager->memused -=
 246         cache->slots * cache->itemsize + sizeof(DdLocalCache);
 247     cuddLocalCacheRemoveFromList(cache);
 248     FREE(cache->item);
 249     FREE(cache);
 250
 251     return;
 252
 253 } /* end of cuddLocalCacheQuit */
 254
 255
 256 /**Function********************************************************************
 257
 258   Synopsis    [Inserts a result in a local cache.]
 259
 260   Description []
 261
 262   SideEffects [None]
 263
 264   SeeAlso     []
 265
 266 ******************************************************************************/
 267 void
 268 cuddLocalCacheInsert(
 269   DdLocalCache * cache,
 270   DdNodePtr * key,
 271   DdNode * value)
 272 {
 273     unsigned int posn;
 274     DdLocalCacheItem *entry;
 275
 276     posn = ddLCHash(key,cache->keysize,cache->shift);
 277     entry = (DdLocalCacheItem *) ((char *) cache->item +
 278                                   posn * cache->itemsize);
 279     memcpy(entry->key,key,cache->keysize * sizeof(DdNode *));
 280     entry->value = value;
 281 #ifdef DD_CACHE_PROFILE
 282     entry->count++;
 283 #endif
 284
 285 } /* end of cuddLocalCacheInsert */
 286
 287
 288 /**Function********************************************************************
 289
 290   Synopsis [Looks up in a local cache.]
 291
 292   Description [Looks up in a local cache. Returns the result if found;
 293   it returns NULL if no result is found.]
 294
 295   SideEffects [None]
 296
 297   SeeAlso     []
 298
 299 ******************************************************************************/
 300 DdNode *
 301 cuddLocalCacheLookup(
 302   DdLocalCache * cache,
 303   DdNodePtr * key)
 304 {
 305     unsigned int posn;
 306     DdLocalCacheItem *entry;
 307     DdNode *value;
 308
 309     cache->lookUps++;
 310     posn = ddLCHash(key,cache->keysize,cache->shift);
 311     entry = (DdLocalCacheItem *) ((char *) cache->item +
 312                                   posn * cache->itemsize);
 313     if (entry->value != NULL &&
 314         memcmp(key,entry->key,cache->keysize*sizeof(DdNode *)) == 0) {
 315         cache->hits++;
 316         value = Cudd_Regular(entry->value);
 317         if (value->ref == 0) {
 318             cuddReclaim(cache->manager,value);
 319         }
 320         return(entry->value);
 321     }
 322
 323     /* Cache miss: decide whether to resize */
 324
 325     if (cache->slots < cache->maxslots &&
 326         cache->hits > cache->lookUps * cache->minHit) {
 327         cuddLocalCacheResize(cache);
 328     }
 329
 330     return(NULL);
 331
 332 } /* end of cuddLocalCacheLookup */
 333
 334
 335 /**Function********************************************************************
 336
 337   Synopsis [Clears the dead entries of the local caches of a manager.]
 338
 339   Description [Clears the dead entries of the local caches of a manager.
 340   Used during garbage collection.]
 341
 342   SideEffects [None]
 343
 344   SeeAlso     []
 345
 346 ******************************************************************************/
 347 void
 348 cuddLocalCacheClearDead(
 349   DdManager * manager)
 350 {
 351     DdLocalCache *cache = manager->localCaches;
 352     unsigned int keysize;
 353     unsigned int itemsize;
 354     unsigned int slots;
 355     DdLocalCacheItem *item;
 356     DdNodePtr *key;
 357     unsigned int i, j;
 358
 359     while (cache != NULL) {
 360         keysize = cache->keysize;
 361         itemsize = cache->itemsize;
 362         slots = cache->slots;
 363         item = cache->item;
 364         for (i = 0; i < slots; i++) {
 365             if (item->value != NULL) {
 366                 if (Cudd_Regular(item->value)->ref == 0) {
 367                     item->value = NULL;
 368                 } else {
 369                     key = item->key;
 370                     for (j = 0; j < keysize; j++) {
 371                         if (Cudd_Regular(key[j])->ref == 0) {
 372                             item->value = NULL;
 373                             break;
 374                         }
 375                     }
 376                 }
 377             }
 378             item = (DdLocalCacheItem *) ((char *) item + itemsize);
 379         }
 380         cache = cache->next;
 381     }
 382     return;
 383
 384 } /* end of cuddLocalCacheClearDead */
 385
 386
 387 /**Function********************************************************************
 388
 389   Synopsis [Clears the local caches of a manager.]
 390
 391   Description [Clears the local caches of a manager.
 392   Used before reordering.]
 393
 394   SideEffects [None]
 395
 396   SeeAlso     []
 397
 398 ******************************************************************************/
 399 void
 400 cuddLocalCacheClearAll(
 401   DdManager * manager)
 402 {
 403     DdLocalCache *cache = manager->localCaches;
 404
 405     while (cache != NULL) {
 406         memset(cache->item, 0, cache->slots * cache->itemsize);
 407         cache = cache->next;
 408     }
 409     return;
 410
 411 } /* end of cuddLocalCacheClearAll */
 412
 413
 414 #ifdef DD_CACHE_PROFILE
 415
 416 #define DD_HYSTO_BINS 8
 417
 418 /**Function********************************************************************
 419
 420   Synopsis    [Computes and prints a profile of a local cache usage.]
 421
 422   Description [Computes and prints a profile of a local cache usage.
 423   Returns 1 if successful; 0 otherwise.]
 424
 425   SideEffects [None]
 426
 427   SeeAlso     []
 428
 429 ******************************************************************************/
 430 int
 431 cuddLocalCacheProfile(
 432   DdLocalCache * cache)
 433 {
 434     double count, mean, meansq, stddev, expected;
 435     long max, min;
 436     int imax, imin;
 437     int i, retval, slots;
 438     long *hystogram;
 439     int nbins = DD_HYSTO_BINS;
 440     int bin;
 441     long thiscount;
 442     double totalcount;
 443     int nzeroes;
 444     DdLocalCacheItem *entry;
 445     FILE *fp = cache->manager->out;
 446
 447     slots = cache->slots;
 448
 449     meansq = mean = expected = 0.0;
 450     max = min = (long) cache->item[0].count;
 451     imax = imin = nzeroes = 0;
 452     totalcount = 0.0;
 453
 454     hystogram = ALLOC(long, nbins);
 455     if (hystogram == NULL) {
 456         return(0);
 457     }
 458     for (i = 0; i < nbins; i++) {
 459         hystogram[i] = 0;
 460     }
 461
 462     for (i = 0; i < slots; i++) {
 463         entry = (DdLocalCacheItem *) ((char *) cache->item +
 464                                       i * cache->itemsize);
 465         thiscount = (long) entry->count;
 466         if (thiscount > max) {
 467             max = thiscount;
 468             imax = i;
 469         }
 470         if (thiscount < min) {
 471             min = thiscount;
 472             imin = i;
 473         }
 474         if (thiscount == 0) {
 475             nzeroes++;
 476         }
 477         count = (double) thiscount;
 478         mean += count;
 479         meansq += count * count;
 480         totalcount += count;
 481         expected += count * (double) i;
 482         bin = (i * nbins) / slots;
 483         hystogram[bin] += thiscount;
 484     }
 485     mean /= (double) slots;
 486     meansq /= (double) slots;
 487     stddev = sqrt(meansq - mean*mean);
 488
 489     retval = fprintf(fp,"Cache stats: slots = %d average = %g ", slots, mean);
 490     if (retval == EOF) return(0);
 491     retval = fprintf(fp,"standard deviation = %g\n", stddev);
 492     if (retval == EOF) return(0);
 493     retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
 494     if (retval == EOF) return(0);
 495     retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
 496     if (retval == EOF) return(0);
 497     retval = fprintf(fp,"Cache unused slots = %d\n", nzeroes);
 498     if (retval == EOF) return(0);
 499
 500     if (totalcount) {
 501         expected /= totalcount;
 502         retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
 503         if (retval == EOF) return(0);
 504         retval = fprintf(fp," (expected bin value = %g)\n# ", expected);
 505         if (retval == EOF) return(0);
 506         for (i = nbins - 1; i>=0; i--) {
 507             retval = fprintf(fp,"%ld ", hystogram[i]);
 508             if (retval == EOF) return(0);
 509         }
 510         retval = fprintf(fp,"\n");
 511         if (retval == EOF) return(0);
 512     }
 513
 514     FREE(hystogram);
 515     return(1);
 516
 517 } /* end of cuddLocalCacheProfile */
 518 #endif
 519
 520
 521 /**Function********************************************************************
 522
 523   Synopsis    [Initializes a hash table.]
 524
 525   Description [Initializes a hash table. Returns a pointer to the new
 526   table if successful; NULL otherwise.]
 527
 528   SideEffects [None]
 529
 530   SeeAlso     [cuddHashTableQuit]
 531
 532 ******************************************************************************/
 533 DdHashTable *
 534 cuddHashTableInit(
 535   DdManager * manager,
 536   unsigned int  keySize,
 537   unsigned int  initSize)
 538 {
 539     DdHashTable *hash;
 540     int logSize;
 541
 542 #ifdef __osf__
 543 #pragma pointer_size save
 544 #pragma pointer_size short
 545 #endif
 546     hash = ALLOC(DdHashTable, 1);
 547     if (hash == NULL) {
 548         manager->errorCode = CUDD_MEMORY_OUT;
 549         return(NULL);
 550     }
 551     hash->keysize = keySize;
 552     hash->manager = manager;
 553     hash->memoryList = NULL;
 554     hash->nextFree = NULL;
 555     hash->itemsize = (keySize + 1) * sizeof(DdNode *) +
 556         sizeof(ptrint) + sizeof(DdHashItem *);
 557     /* We have to guarantee that the shift be < 32. */
 558     if (initSize < 2) initSize = 2;
 559     logSize = cuddComputeFloorLog2(initSize);
 560     hash->numBuckets = 1 << logSize;
 561     hash->shift = sizeof(int) * 8 - logSize;
 562     hash->bucket = ALLOC(DdHashItem *, hash->numBuckets);
 563     if (hash->bucket == NULL) {
 564         manager->errorCode = CUDD_MEMORY_OUT;
 565         FREE(hash);
 566         return(NULL);
 567     }
 568     memset(hash->bucket, 0, hash->numBuckets * sizeof(DdHashItem *));
 569     hash->size = 0;
 570     hash->maxsize = hash->numBuckets * DD_MAX_HASHTABLE_DENSITY;
 571 #ifdef __osf__
 572 #pragma pointer_size restore
 573 #endif
 574     return(hash);
 575
 576 } /* end of cuddHashTableInit */
 577
 578
 579 /**Function********************************************************************
 580
 581   Synopsis    [Shuts down a hash table.]
 582
 583   Description [Shuts down a hash table, dereferencing all the values.]
 584
 585   SideEffects [None]
 586
 587   SeeAlso     [cuddHashTableInit]
 588
 589 ******************************************************************************/
 590 void
 591 cuddHashTableQuit(
 592   DdHashTable * hash)
 593 {
 594 #ifdef __osf__
 595 #pragma pointer_size save
 596 #pragma pointer_size short
 597 #endif
 598     unsigned int i;
 599     DdManager *dd = hash->manager;
 600     DdHashItem *bucket;
 601     DdHashItem **memlist, **nextmem;
 602     unsigned int numBuckets = hash->numBuckets;
 603
 604     for (i = 0; i < numBuckets; i++) {
 605         bucket = hash->bucket[i];
 606         while (bucket != NULL) {
 607             Cudd_RecursiveDeref(dd, bucket->value);
 608             bucket = bucket->next;
 609         }
 610     }
 611
 612     memlist = hash->memoryList;
 613     while (memlist != NULL) {
 614         nextmem = (DdHashItem **) memlist[0];
 615         FREE(memlist);
 616         memlist = nextmem;
 617     }
 618
 619     FREE(hash->bucket);
 620     FREE(hash);
 621 #ifdef __osf__
 622 #pragma pointer_size restore
 623 #endif
 624
 625     return;
 626
 627 } /* end of cuddHashTableQuit */
 628
 629
 630 /**Function********************************************************************
 631
 632   Synopsis    [Inserts an item in a hash table.]
 633
 634   Description [Inserts an item in a hash table when the key has more than
 635   three pointers.  Returns 1 if successful; 0 otherwise.]
 636
 637   SideEffects [None]
 638
 639   SeeAlso     [[cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableInsert3
 640   cuddHashTableLookup]
 641
 642 ******************************************************************************/
 643 int
 644 cuddHashTableInsert(
 645   DdHashTable * hash,
 646   DdNodePtr * key,
 647   DdNode * value,
 648   ptrint count)
 649 {
 650     int result;
 651     unsigned int posn;
 652     DdHashItem *item;
 653     unsigned int i;
 654
 655 #ifdef DD_DEBUG
 656     assert(hash->keysize > 3);
 657 #endif
 658
 659     if (hash->size > hash->maxsize) {
 660         result = cuddHashTableResize(hash);
 661         if (result == 0) return(0);
 662     }
 663     item = cuddHashTableAlloc(hash);
 664     if (item == NULL) return(0);
 665     hash->size++;
 666     item->value = value;
 667     cuddRef(value);
 668     item->count = count;
 669     for (i = 0; i < hash->keysize; i++) {
 670         item->key[i] = key[i];
 671     }
 672     posn = ddLCHash(key,hash->keysize,hash->shift);
 673     item->next = hash->bucket[posn];
 674     hash->bucket[posn] = item;
 675
 676     return(1);
 677
 678 } /* end of cuddHashTableInsert */
 679
 680
 681 /**Function********************************************************************
 682
 683   Synopsis    [Looks up a key in a hash table.]
 684
 685   Description [Looks up a key consisting of more than three pointers
 686   in a hash table.  Returns the value associated to the key if there
 687   is an entry for the given key in the table; NULL otherwise. If the
 688   entry is present, its reference counter is decremented if not
 689   saturated. If the counter reaches 0, the value of the entry is
 690   dereferenced, and the entry is returned to the free list.]
 691
 692   SideEffects [None]
 693
 694   SeeAlso     [cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableLookup3
 695   cuddHashTableInsert]
 696
 697 ******************************************************************************/
 698 DdNode *
 699 cuddHashTableLookup(
 700   DdHashTable * hash,
 701   DdNodePtr * key)
 702 {
 703     unsigned int posn;
 704     DdHashItem *item, *prev;
 705     unsigned int i, keysize;
 706
 707 #ifdef DD_DEBUG
 708     assert(hash->keysize > 3);
 709 #endif
 710
 711     posn = ddLCHash(key,hash->keysize,hash->shift);
 712     item = hash->bucket[posn];
 713     prev = NULL;
 714
 715     keysize = hash->keysize;
 716     while (item != NULL) {
 717         DdNodePtr *key2 = item->key;
 718         int equal = 1;
 719         for (i = 0; i < keysize; i++) {
 720             if (key[i] != key2[i]) {
 721                 equal = 0;
 722                 break;
 723             }
 724         }
 725         if (equal) {
 726             DdNode *value = item->value;
 727             cuddSatDec(item->count);
 728             if (item->count == 0) {
 729                 cuddDeref(value);
 730                 if (prev == NULL) {
 731                     hash->bucket[posn] = item->next;
 732                 } else {
 733                     prev->next = item->next;
 734                 }
 735                 item->next = hash->nextFree;
 736                 hash->nextFree = item;
 737                 hash->size--;
 738             }
 739             return(value);
 740         }
 741         prev = item;
 742         item = item->next;
 743     }
 744     return(NULL);
 745
 746 } /* end of cuddHashTableLookup */
 747
 748
 749 /**Function********************************************************************
 750
 751   Synopsis    [Inserts an item in a hash table.]
 752
 753   Description [Inserts an item in a hash table when the key is one pointer.
 754   Returns 1 if successful; 0 otherwise.]
 755
 756   SideEffects [None]
 757
 758   SeeAlso     [cuddHashTableInsert cuddHashTableInsert2 cuddHashTableInsert3
 759   cuddHashTableLookup1]
 760
 761 ******************************************************************************/
 762 int
 763 cuddHashTableInsert1(
 764   DdHashTable * hash,
 765   DdNode * f,
 766   DdNode * value,
 767   ptrint count)
 768 {
 769     int result;
 770     unsigned int posn;
 771     DdHashItem *item;
 772
 773 #ifdef DD_DEBUG
 774     assert(hash->keysize == 1);
 775 #endif
 776
 777     if (hash->size > hash->maxsize) {
 778         result = cuddHashTableResize(hash);
 779         if (result == 0) return(0);
 780     }
 781     item = cuddHashTableAlloc(hash);
 782     if (item == NULL) return(0);
 783     hash->size++;
 784     item->value = value;
 785     cuddRef(value);
 786     item->count = count;
 787     item->key[0] = f;
 788     posn = ddLCHash2(f,f,hash->shift);
 789     item->next = hash->bucket[posn];
 790     hash->bucket[posn] = item;
 791
 792     return(1);
 793
 794 } /* end of cuddHashTableInsert1 */
 795
 796
 797 /**Function********************************************************************
 798
 799   Synopsis    [Looks up a key consisting of one pointer in a hash table.]
 800
 801   Description [Looks up a key consisting of one pointer in a hash table.
 802   Returns the value associated to the key if there is an entry for the given
 803   key in the table; NULL otherwise. If the entry is present, its reference
 804   counter is decremented if not saturated. If the counter reaches 0, the
 805   value of the entry is dereferenced, and the entry is returned to the free
 806   list.]
 807
 808   SideEffects [None]
 809
 810   SeeAlso     [cuddHashTableLookup cuddHashTableLookup2 cuddHashTableLookup3
 811   cuddHashTableInsert1]
 812
 813 ******************************************************************************/
 814 DdNode *
 815 cuddHashTableLookup1(
 816   DdHashTable * hash,
 817   DdNode * f)
 818 {
 819     unsigned int posn;
 820     DdHashItem *item, *prev;
 821
 822 #ifdef DD_DEBUG
 823     assert(hash->keysize == 1);
 824 #endif
 825
 826     posn = ddLCHash2(f,f,hash->shift);
 827     item = hash->bucket[posn];
 828     prev = NULL;
 829
 830     while (item != NULL) {
 831         DdNodePtr *key = item->key;
 832         if (f == key[0]) {
 833             DdNode *value = item->value;
 834             cuddSatDec(item->count);
 835             if (item->count == 0) {
 836                 cuddDeref(value);
 837                 if (prev == NULL) {
 838                     hash->bucket[posn] = item->next;
 839                 } else {
 840                     prev->next = item->next;
 841                 }
 842                 item->next = hash->nextFree;
 843                 hash->nextFree = item;
 844                 hash->size--;
 845             }
 846             return(value);
 847         }
 848         prev = item;
 849         item = item->next;
 850     }
 851     return(NULL);
 852
 853 } /* end of cuddHashTableLookup1 */
 854
 855
 856 /**Function********************************************************************
 857
 858   Synopsis    [Inserts an item in a hash table.]
 859
 860   Description [Inserts an item in a hash table when the key is
 861   composed of two pointers. Returns 1 if successful; 0 otherwise.]
 862
 863   SideEffects [None]
 864
 865   SeeAlso     [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert3
 866   cuddHashTableLookup2]
 867
 868 ******************************************************************************/
 869 int
 870 cuddHashTableInsert2(
 871   DdHashTable * hash,
 872   DdNode * f,
 873   DdNode * g,
 874   DdNode * value,
 875   ptrint count)
 876 {
 877     int result;
 878     unsigned int posn;
 879     DdHashItem *item;
 880
 881 #ifdef DD_DEBUG
 882     assert(hash->keysize == 2);
 883 #endif
 884
 885     if (hash->size > hash->maxsize) {
 886         result = cuddHashTableResize(hash);
 887         if (result == 0) return(0);
 888     }
 889     item = cuddHashTableAlloc(hash);
 890     if (item == NULL) return(0);
 891     hash->size++;
 892     item->value = value;
 893     cuddRef(value);
 894     item->count = count;
 895     item->key[0] = f;
 896     item->key[1] = g;
 897     posn = ddLCHash2(f,g,hash->shift);
 898     item->next = hash->bucket[posn];
 899     hash->bucket[posn] = item;
 900
 901     return(1);
 902
 903 } /* end of cuddHashTableInsert2 */
 904
 905
 906 /**Function********************************************************************
 907
 908   Synopsis    [Looks up a key consisting of two pointers in a hash table.]
 909
 910   Description [Looks up a key consisting of two pointer in a hash table.
 911   Returns the value associated to the key if there is an entry for the given
 912   key in the table; NULL otherwise. If the entry is present, its reference
 913   counter is decremented if not saturated. If the counter reaches 0, the
 914   value of the entry is dereferenced, and the entry is returned to the free
 915   list.]
 916
 917   SideEffects [None]
 918
 919   SeeAlso     [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup3
 920   cuddHashTableInsert2]
 921
 922 ******************************************************************************/
 923 DdNode *
 924 cuddHashTableLookup2(
 925   DdHashTable * hash,
 926   DdNode * f,
 927   DdNode * g)
 928 {
 929     unsigned int posn;
 930     DdHashItem *item, *prev;
 931
 932 #ifdef DD_DEBUG
 933     assert(hash->keysize == 2);
 934 #endif
 935
 936     posn = ddLCHash2(f,g,hash->shift);
 937     item = hash->bucket[posn];
 938     prev = NULL;
 939
 940     while (item != NULL) {
 941         DdNodePtr *key = item->key;
 942         if ((f == key[0]) && (g == key[1])) {
 943             DdNode *value = item->value;
 944             cuddSatDec(item->count);
 945             if (item->count == 0) {
 946                 cuddDeref(value);
 947                 if (prev == NULL) {
 948                     hash->bucket[posn] = item->next;
 949                 } else {
 950                     prev->next = item->next;
 951                 }
 952                 item->next = hash->nextFree;
 953                 hash->nextFree = item;
 954                 hash->size--;
 955             }
 956             return(value);
 957         }
 958         prev = item;
 959         item = item->next;
 960     }
 961     return(NULL);
 962
 963 } /* end of cuddHashTableLookup2 */
 964
 965
 966 /**Function********************************************************************
 967
 968   Synopsis    [Inserts an item in a hash table.]
 969
 970   Description [Inserts an item in a hash table when the key is
 971   composed of three pointers. Returns 1 if successful; 0 otherwise.]
 972
 973   SideEffects [None]
 974
 975   SeeAlso     [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert2
 976   cuddHashTableLookup3]
 977
 978 ******************************************************************************/
 979 int
 980 cuddHashTableInsert3(
 981   DdHashTable * hash,
 982   DdNode * f,
 983   DdNode * g,
 984   DdNode * h,
 985   DdNode * value,
 986   ptrint count)
 987 {
 988     int result;
 989     unsigned int posn;
 990     DdHashItem *item;
 991
 992 #ifdef DD_DEBUG
 993     assert(hash->keysize == 3);
 994 #endif
 995
 996     if (hash->size > hash->maxsize) {
 997         result = cuddHashTableResize(hash);
 998         if (result == 0) return(0);
 999     }
1000     item = cuddHashTableAlloc(hash);
1001     if (item == NULL) return(0);
1002     hash->size++;
1003     item->value = value;
1004     cuddRef(value);
1005     item->count = count;
1006     item->key[0] = f;
1007     item->key[1] = g;
1008     item->key[2] = h;
1009     posn = ddLCHash3(f,g,h,hash->shift);
1010     item->next = hash->bucket[posn];
1011     hash->bucket[posn] = item;
1012
1013     return(1);
1014
1015 } /* end of cuddHashTableInsert3 */
1016
1017
1018 /**Function********************************************************************
1019
1020   Synopsis    [Looks up a key consisting of three pointers in a hash table.]
1021
1022   Description [Looks up a key consisting of three pointers in a hash table.
1023   Returns the value associated to the key if there is an entry for the given
1024   key in the table; NULL otherwise. If the entry is present, its reference
1025   counter is decremented if not saturated. If the counter reaches 0, the
1026   value of the entry is dereferenced, and the entry is returned to the free
1027   list.]
1028
1029   SideEffects [None]
1030
1031   SeeAlso     [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup2
1032   cuddHashTableInsert3]
1033
1034 ******************************************************************************/
1035 DdNode *
1036 cuddHashTableLookup3(
1037   DdHashTable * hash,
1038   DdNode * f,
1039   DdNode * g,
1040   DdNode * h)
1041 {
1042     unsigned int posn;
1043     DdHashItem *item, *prev;
1044
1045 #ifdef DD_DEBUG
1046     assert(hash->keysize == 3);
1047 #endif
1048
1049     posn = ddLCHash3(f,g,h,hash->shift);
1050     item = hash->bucket[posn];
1051     prev = NULL;
1052
1053     while (item != NULL) {
1054         DdNodePtr *key = item->key;
1055         if ((f == key[0]) && (g == key[1]) && (h == key[2])) {
1056             DdNode *value = item->value;
1057             cuddSatDec(item->count);
1058             if (item->count == 0) {
1059                 cuddDeref(value);
1060                 if (prev == NULL) {
1061                     hash->bucket[posn] = item->next;
1062                 } else {
1063                     prev->next = item->next;
1064                 }
1065                 item->next = hash->nextFree;
1066                 hash->nextFree = item;
1067                 hash->size--;
1068             }
1069             return(value);
1070         }
1071         prev = item;
1072         item = item->next;
1073     }
1074     return(NULL);
1075
1076 } /* end of cuddHashTableLookup3 */
1077
1078
1079 /*---------------------------------------------------------------------------*/
1080 /* Definition of static functions                                            */
1081 /*---------------------------------------------------------------------------*/
1082
1083
1084 /**Function********************************************************************
1085
1086   Synopsis    [Resizes a local cache.]
1087
1088   Description []
1089
1090   SideEffects [None]
1091
1092   SeeAlso     []
1093
1094 ******************************************************************************/
1095 static void
1096 cuddLocalCacheResize(
1097   DdLocalCache * cache)
1098 {
1099     DdLocalCacheItem *item, *olditem, *entry, *old;
1100     int i, shift;
1101     unsigned int posn;
1102     unsigned int slots, oldslots;
1103     extern DD_OOMFP MMoutOfMemory;
1104     DD_OOMFP saveHandler;
1105
1106     olditem = cache->item;
1107     oldslots = cache->slots;
1108     slots = cache->slots = oldslots << 1;
1109
1110 #ifdef DD_VERBOSE
1111     (void) fprintf(cache->manager->err,
1112                    "Resizing local cache from %d to %d entries\n",
1113                    oldslots, slots);
1114     (void) fprintf(cache->manager->err,
1115                    "\thits = %.0f\tlookups = %.0f\thit ratio = %5.3f\n",
1116                    cache->hits, cache->lookUps, cache->hits / cache->lookUps);
1117 #endif
1118
1119     saveHandler = MMoutOfMemory;
1120     MMoutOfMemory = Cudd_OutOfMem;
1121     cache->item = item =
1122         (DdLocalCacheItem *) ALLOC(char, slots * cache->itemsize);
1123     MMoutOfMemory = saveHandler;
1124     /* If we fail to allocate the new table we just give up. */
1125     if (item == NULL) {
1126 #ifdef DD_VERBOSE
1127         (void) fprintf(cache->manager->err,"Resizing failed. Giving up.\n");
1128 #endif
1129         cache->slots = oldslots;
1130         cache->item = olditem;
1131         /* Do not try to resize again. */
1132         cache->maxslots = oldslots - 1;
1133         return;
1134     }
1135     shift = --(cache->shift);
1136     cache->manager->memused += (slots - oldslots) * cache->itemsize;
1137
1138     /* Clear new cache. */
1139     memset(item, 0, slots * cache->itemsize);
1140
1141     /* Copy from old cache to new one. */
1142     for (i = 0; (unsigned) i < oldslots; i++) {
1143         old = (DdLocalCacheItem *) ((char *) olditem + i * cache->itemsize);
1144         if (old->value != NULL) {
1145             posn = ddLCHash(old->key,cache->keysize,shift);
1146             entry = (DdLocalCacheItem *) ((char *) item +
1147                                           posn * cache->itemsize);
1148             memcpy(entry->key,old->key,cache->keysize*sizeof(DdNode *));
1149             entry->value = old->value;
1150         }
1151     }
1152
1153     FREE(olditem);
1154
1155     /* Reinitialize measurements so as to avoid division by 0 and
1156     ** immediate resizing.
1157     */
1158     cache->lookUps = (double) (int) (slots * cache->minHit + 1);
1159     cache->hits = 0;
1160
1161 } /* end of cuddLocalCacheResize */
1162
1163
1164 /**Function********************************************************************
1165
1166   Synopsis    [Computes the hash value for a local cache.]
1167
1168   Description [Computes the hash value for a local cache. Returns the
1169   bucket index.]
1170
1171   SideEffects [None]
1172
1173   SeeAlso     []
1174
1175 ******************************************************************************/
1176 DD_INLINE
1177 static unsigned int
1178 ddLCHash(
1179   DdNodePtr * key,
1180   unsigned int keysize,
1181   int shift)
1182 {
1183     unsigned int val = (unsigned int) (ptrint) key[0] * DD_P2;
1184     unsigned int i;
1185
1186     for (i = 1; i < keysize; i++) {
1187         val = val * DD_P1 + (int) (ptrint) key[i];
1188     }
1189
1190     return(val >> shift);
1191
1192 } /* end of ddLCHash */
1193
1194
1195 /**Function********************************************************************
1196
1197   Synopsis    [Inserts a local cache in the manager list.]
1198
1199   Description []
1200
1201   SideEffects [None]
1202
1203   SeeAlso     []
1204
1205 ******************************************************************************/
1206 static void
1207 cuddLocalCacheAddToList(
1208   DdLocalCache * cache)
1209 {
1210     DdManager *manager = cache->manager;
1211
1212     cache->next = manager->localCaches;
1213     manager->localCaches = cache;
1214     return;
1215
1216 } /* end of cuddLocalCacheAddToList */
1217
1218
1219 /**Function********************************************************************
1220
1221   Synopsis    [Removes a local cache from the manager list.]
1222
1223   Description []
1224
1225   SideEffects [None]
1226
1227   SeeAlso     []
1228
1229 ******************************************************************************/
1230 static void
1231 cuddLocalCacheRemoveFromList(
1232   DdLocalCache * cache)
1233 {
1234     DdManager *manager = cache->manager;
1235 #ifdef __osf__
1236 #pragma pointer_size save
1237 #pragma pointer_size short
1238 #endif
1239     DdLocalCache **prevCache, *nextCache;
1240 #ifdef __osf__
1241 #pragma pointer_size restore
1242 #endif
1243
1244     prevCache = &(manager->localCaches);
1245     nextCache = manager->localCaches;
1246
1247     while (nextCache != NULL) {
1248         if (nextCache == cache) {
1249             *prevCache = nextCache->next;
1250             return;
1251         }
1252         prevCache = &(nextCache->next);
1253         nextCache = nextCache->next;
1254     }
1255     return;                     /* should never get here */
1256
1257 } /* end of cuddLocalCacheRemoveFromList */
1258
1259
1260 /**Function********************************************************************
1261
1262   Synopsis    [Resizes a hash table.]
1263
1264   Description [Resizes a hash table. Returns 1 if successful; 0
1265   otherwise.]
1266
1267   SideEffects [None]
1268
1269   SeeAlso     [cuddHashTableInsert]
1270
1271 ******************************************************************************/
1272 static int
1273 cuddHashTableResize(
1274   DdHashTable * hash)
1275 {
1276     int j;
1277     unsigned int posn;
1278     DdHashItem *item;
1279     DdHashItem *next;
1280 #ifdef __osf__
1281 #pragma pointer_size save
1282 #pragma pointer_size short
1283 #endif
1284     DdNode **key;
1285     int numBuckets;
1286     DdHashItem **buckets;
1287     DdHashItem **oldBuckets = hash->bucket;
1288 #ifdef __osf__
1289 #pragma pointer_size restore
1290 #endif
1291     int shift;
1292     int oldNumBuckets = hash->numBuckets;
1293     extern DD_OOMFP MMoutOfMemory;
1294     DD_OOMFP saveHandler;
1295
1296     /* Compute the new size of the table. */
1297     numBuckets = oldNumBuckets << 1;
1298     saveHandler = MMoutOfMemory;
1299     MMoutOfMemory = Cudd_OutOfMem;
1300 #ifdef __osf__
1301 #pragma pointer_size save
1302 #pragma pointer_size short
1303 #endif
1304     buckets = ALLOC(DdHashItem *, numBuckets);
1305     MMoutOfMemory = saveHandler;
1306     if (buckets == NULL) {
1307         hash->maxsize <<= 1;
1308         return(1);
1309     }
1310
1311     hash->bucket = buckets;
1312     hash->numBuckets = numBuckets;
1313     shift = --(hash->shift);
1314     hash->maxsize <<= 1;
1315     memset(buckets, 0, numBuckets * sizeof(DdHashItem *));
1316 #ifdef __osf__
1317 #pragma pointer_size restore
1318 #endif
1319     if (hash->keysize == 1) {
1320         for (j = 0; j < oldNumBuckets; j++) {
1321             item = oldBuckets[j];
1322             while (item != NULL) {
1323                 next = item->next;
1324                 key = item->key;
1325                 posn = ddLCHash2(key[0], key[0], shift);
1326                 item->next = buckets[posn];
1327                 buckets[posn] = item;
1328                 item = next;
1329             }
1330         }
1331     } else if (hash->keysize == 2) {
1332         for (j = 0; j < oldNumBuckets; j++) {
1333             item = oldBuckets[j];
1334             while (item != NULL) {
1335                 next = item->next;
1336                 key = item->key;
1337                 posn = ddLCHash2(key[0], key[1], shift);
1338                 item->next = buckets[posn];
1339                 buckets[posn] = item;
1340                 item = next;
1341             }
1342         }
1343     } else if (hash->keysize == 3) {
1344         for (j = 0; j < oldNumBuckets; j++) {
1345             item = oldBuckets[j];
1346             while (item != NULL) {
1347                 next = item->next;
1348                 key = item->key;
1349                 posn = ddLCHash3(key[0], key[1], key[2], shift);
1350                 item->next = buckets[posn];
1351                 buckets[posn] = item;
1352                 item = next;
1353             }
1354         }
1355     } else {
1356         for (j = 0; j < oldNumBuckets; j++) {
1357             item = oldBuckets[j];
1358             while (item != NULL) {
1359                 next = item->next;
1360                 posn = ddLCHash(item->key, hash->keysize, shift);
1361                 item->next = buckets[posn];
1362                 buckets[posn] = item;
1363                 item = next;
1364             }
1365         }
1366     }
1367     FREE(oldBuckets);
1368     return(1);
1369
1370 } /* end of cuddHashTableResize */
1371
1372
1373 /**Function********************************************************************
1374
1375   Synopsis    [Fast storage allocation for items in a hash table.]
1376
1377   Description [Fast storage allocation for items in a hash table. The
1378   first 4 bytes of a chunk contain a pointer to the next block; the
1379   rest contains DD_MEM_CHUNK spaces for hash items.  Returns a pointer to
1380   a new item if successful; NULL is memory is full.]
1381
1382   SideEffects [None]
1383
1384   SeeAlso     [cuddAllocNode cuddDynamicAllocNode]
1385
1386 ******************************************************************************/
1387 DD_INLINE
1388 static DdHashItem *
1389 cuddHashTableAlloc(
1390   DdHashTable * hash)
1391 {
1392     int i;
1393     unsigned int itemsize = hash->itemsize;
1394     extern DD_OOMFP MMoutOfMemory;
1395     DD_OOMFP saveHandler;
1396 #ifdef __osf__
1397 #pragma pointer_size save
1398 #pragma pointer_size short
1399 #endif
1400     DdHashItem **mem, *thisOne, *next, *item;
1401
1402     if (hash->nextFree == NULL) {
1403         saveHandler = MMoutOfMemory;
1404         MMoutOfMemory = Cudd_OutOfMem;
1405         mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
1406         MMoutOfMemory = saveHandler;
1407 #ifdef __osf__
1408 #pragma pointer_size restore
1409 #endif
1410         if (mem == NULL) {
1411             if (hash->manager->stash != NULL) {
1412                 FREE(hash->manager->stash);
1413                 hash->manager->stash = NULL;
1414                 /* Inhibit resizing of tables. */
1415                 hash->manager->maxCacheHard = hash->manager->cacheSlots - 1;
1416                 hash->manager->cacheSlack = - (int) (hash->manager->cacheSlots + 1);
1417                 for (i = 0; i < hash->manager->size; i++) {
1418                     hash->manager->subtables[i].maxKeys <<= 2;
1419                 }
1420                 hash->manager->gcFrac = 0.2;
1421                 hash->manager->minDead =
1422                     (unsigned) (0.2 * (double) hash->manager->slots);
1423 #ifdef __osf__
1424 #pragma pointer_size save
1425 #pragma pointer_size short
1426 #endif
1427                 mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
1428 #ifdef __osf__
1429 #pragma pointer_size restore
1430 #endif
1431             }
1432             if (mem == NULL) {
1433                 (*MMoutOfMemory)((long)((DD_MEM_CHUNK + 1) * itemsize));
1434                 hash->manager->errorCode = CUDD_MEMORY_OUT;
1435                 return(NULL);
1436             }
1437         }
1438
1439         mem[0] = (DdHashItem *) hash->memoryList;
1440         hash->memoryList = mem;
1441
1442         thisOne = (DdHashItem *) ((char *) mem + itemsize);
1443         hash->nextFree = thisOne;
1444         for (i = 1; i < DD_MEM_CHUNK; i++) {
1445             next = (DdHashItem *) ((char *) thisOne + itemsize);
1446             thisOne->next = next;
1447             thisOne = next;
1448         }
1449
1450         thisOne->next = NULL;
1451
1452     }
1453     item = hash->nextFree;
1454     hash->nextFree = item->next;
1455     return(item);
1456
1457 } /* end of cuddHashTableAlloc */