source: vis_dev/glu-2.3/src/cuBdd/cuddLCache.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 37.8 KB
RevLine 
[13]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
99static 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
147static void cuddLocalCacheResize (DdLocalCache *cache);
148DD_INLINE static unsigned int ddLCHash (DdNodePtr *key, unsigned int keysize, int shift);
149static void cuddLocalCacheAddToList (DdLocalCache *cache);
150static void cuddLocalCacheRemoveFromList (DdLocalCache *cache);
151static int cuddHashTableResize (DdHashTable *hash);
152DD_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******************************************************************************/
178DdLocalCache *
179cuddLocalCacheInit(
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******************************************************************************/
241void
242cuddLocalCacheQuit(
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******************************************************************************/
267void
268cuddLocalCacheInsert(
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******************************************************************************/
300DdNode *
301cuddLocalCacheLookup(
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******************************************************************************/
347void
348cuddLocalCacheClearDead(
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******************************************************************************/
399void
400cuddLocalCacheClearAll(
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******************************************************************************/
430int
431cuddLocalCacheProfile(
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******************************************************************************/
533DdHashTable *
534cuddHashTableInit(
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******************************************************************************/
590void
591cuddHashTableQuit(
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******************************************************************************/
643int
644cuddHashTableInsert(
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******************************************************************************/
698DdNode *
699cuddHashTableLookup(
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******************************************************************************/
762int
763cuddHashTableInsert1(
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******************************************************************************/
814DdNode *
815cuddHashTableLookup1(
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******************************************************************************/
869int
870cuddHashTableInsert2(
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******************************************************************************/
923DdNode *
924cuddHashTableLookup2(
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******************************************************************************/
979int
980cuddHashTableInsert3(
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******************************************************************************/
1035DdNode *
1036cuddHashTableLookup3(
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******************************************************************************/
1095static void
1096cuddLocalCacheResize(
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******************************************************************************/
1176DD_INLINE
1177static unsigned int
1178ddLCHash(
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******************************************************************************/
1206static void
1207cuddLocalCacheAddToList(
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******************************************************************************/
1230static void
1231cuddLocalCacheRemoveFromList(
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******************************************************************************/
1272static int
1273cuddHashTableResize(
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******************************************************************************/
1387DD_INLINE
1388static DdHashItem *
1389cuddHashTableAlloc(
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 */
Note: See TracBrowser for help on using the repository browser.