source: vis_dev/glu-2.1/src/cuBdd/cuddLCache.c @ 6

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

Ajout de glus pour dev VIS mod
File size: 37.8 KB
Line 
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.21 2004/08/13 18:04:49 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)(unsigned long)(f) * DD_P1 + \
120   (unsigned)(unsigned long)(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 && Cudd_Regular(item->value)->ref == 0) {
366                item->value = NULL;
367            } else {
368                key = item->key;
369                for (j = 0; j < keysize; j++) {
370                    if (Cudd_Regular(key[j])->ref == 0) {
371                        item->value = NULL;
372                        break;
373                    }
374                }
375            }
376            item = (DdLocalCacheItem *) ((char *) item + itemsize);
377        }
378        cache = cache->next;
379    }
380    return;
381
382} /* end of cuddLocalCacheClearDead */
383
384
385/**Function********************************************************************
386
387  Synopsis [Clears the local caches of a manager.]
388
389  Description [Clears the local caches of a manager.
390  Used before reordering.]
391
392  SideEffects [None]
393
394  SeeAlso     []
395
396******************************************************************************/
397void
398cuddLocalCacheClearAll(
399  DdManager * manager)
400{
401    DdLocalCache *cache = manager->localCaches;
402
403    while (cache != NULL) {
404        memset(cache->item, 0, cache->slots * cache->itemsize);
405        cache = cache->next;
406    }
407    return;
408
409} /* end of cuddLocalCacheClearAll */
410
411
412#ifdef DD_CACHE_PROFILE
413
414#define DD_HYSTO_BINS 8
415
416/**Function********************************************************************
417
418  Synopsis    [Computes and prints a profile of a local cache usage.]
419
420  Description [Computes and prints a profile of a local cache usage.
421  Returns 1 if successful; 0 otherwise.]
422
423  SideEffects [None]
424
425  SeeAlso     []
426
427******************************************************************************/
428int
429cuddLocalCacheProfile(
430  DdLocalCache * cache)
431{
432    double count, mean, meansq, stddev, expected;
433    long max, min;
434    int imax, imin;
435    int i, retval, slots;
436    long *hystogram;
437    int nbins = DD_HYSTO_BINS;
438    int bin;
439    long thiscount;
440    double totalcount;
441    int nzeroes;
442    DdLocalCacheItem *entry;
443    FILE *fp = cache->manager->out;
444
445    slots = cache->slots;
446
447    meansq = mean = expected = 0.0;
448    max = min = (long) cache->item[0].count;
449    imax = imin = nzeroes = 0;
450    totalcount = 0.0;
451
452    hystogram = ALLOC(long, nbins);
453    if (hystogram == NULL) {
454        return(0);
455    }
456    for (i = 0; i < nbins; i++) {
457        hystogram[i] = 0;
458    }
459
460    for (i = 0; i < slots; i++) {
461        entry = (DdLocalCacheItem *) ((char *) cache->item +
462                                      i * cache->itemsize);
463        thiscount = (long) entry->count;
464        if (thiscount > max) {
465            max = thiscount;
466            imax = i;
467        }
468        if (thiscount < min) {
469            min = thiscount;
470            imin = i;
471        }
472        if (thiscount == 0) {
473            nzeroes++;
474        }
475        count = (double) thiscount;
476        mean += count;
477        meansq += count * count;
478        totalcount += count;
479        expected += count * (double) i;
480        bin = (i * nbins) / slots;
481        hystogram[bin] += thiscount;
482    }
483    mean /= (double) slots;
484    meansq /= (double) slots;
485    stddev = sqrt(meansq - mean*mean);
486
487    retval = fprintf(fp,"Cache stats: slots = %d average = %g ", slots, mean);
488    if (retval == EOF) return(0);
489    retval = fprintf(fp,"standard deviation = %g\n", stddev);
490    if (retval == EOF) return(0);
491    retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
492    if (retval == EOF) return(0);
493    retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
494    if (retval == EOF) return(0);
495    retval = fprintf(fp,"Cache unused slots = %d\n", nzeroes);
496    if (retval == EOF) return(0);
497
498    if (totalcount) {
499        expected /= totalcount;
500        retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
501        if (retval == EOF) return(0);
502        retval = fprintf(fp," (expected bin value = %g)\n# ", expected);
503        if (retval == EOF) return(0);
504        for (i = nbins - 1; i>=0; i--) {
505            retval = fprintf(fp,"%ld ", hystogram[i]);
506            if (retval == EOF) return(0);
507        }
508        retval = fprintf(fp,"\n");
509        if (retval == EOF) return(0);
510    }
511
512    FREE(hystogram);
513    return(1);
514
515} /* end of cuddLocalCacheProfile */
516#endif
517
518
519/**Function********************************************************************
520
521  Synopsis    [Initializes a hash table.]
522
523  Description [Initializes a hash table. Returns a pointer to the new
524  table if successful; NULL otherwise.]
525
526  SideEffects [None]
527
528  SeeAlso     [cuddHashTableQuit]
529
530******************************************************************************/
531DdHashTable *
532cuddHashTableInit(
533  DdManager * manager,
534  unsigned int  keySize,
535  unsigned int  initSize)
536{
537    DdHashTable *hash;
538    int logSize;
539
540#ifdef __osf__
541#pragma pointer_size save
542#pragma pointer_size short
543#endif
544    hash = ALLOC(DdHashTable, 1);
545    if (hash == NULL) {
546        manager->errorCode = CUDD_MEMORY_OUT;
547        return(NULL);
548    }
549    hash->keysize = keySize;
550    hash->manager = manager;
551    hash->memoryList = NULL;
552    hash->nextFree = NULL;
553    hash->itemsize = (keySize + 1) * sizeof(DdNode *) +
554        sizeof(ptrint) + sizeof(DdHashItem *);
555    /* We have to guarantee that the shift be < 32. */
556    if (initSize < 2) initSize = 2;
557    logSize = cuddComputeFloorLog2(initSize);
558    hash->numBuckets = 1 << logSize;
559    hash->shift = sizeof(int) * 8 - logSize;
560    hash->bucket = ALLOC(DdHashItem *, hash->numBuckets);
561    if (hash->bucket == NULL) {
562        manager->errorCode = CUDD_MEMORY_OUT;
563        FREE(hash);
564        return(NULL);
565    }
566    memset(hash->bucket, 0, hash->numBuckets * sizeof(DdHashItem *));
567    hash->size = 0;
568    hash->maxsize = hash->numBuckets * DD_MAX_HASHTABLE_DENSITY;
569#ifdef __osf__
570#pragma pointer_size restore
571#endif
572    return(hash);
573
574} /* end of cuddHashTableInit */
575
576
577/**Function********************************************************************
578
579  Synopsis    [Shuts down a hash table.]
580
581  Description [Shuts down a hash table, dereferencing all the values.]
582
583  SideEffects [None]
584
585  SeeAlso     [cuddHashTableInit]
586
587******************************************************************************/
588void
589cuddHashTableQuit(
590  DdHashTable * hash)
591{
592#ifdef __osf__
593#pragma pointer_size save
594#pragma pointer_size short
595#endif
596    unsigned int i;
597    DdManager *dd = hash->manager;
598    DdHashItem *bucket;
599    DdHashItem **memlist, **nextmem;
600    unsigned int numBuckets = hash->numBuckets;
601
602    for (i = 0; i < numBuckets; i++) {
603        bucket = hash->bucket[i];
604        while (bucket != NULL) {
605            Cudd_RecursiveDeref(dd, bucket->value);
606            bucket = bucket->next;
607        }
608    }
609
610    memlist = hash->memoryList;
611    while (memlist != NULL) {
612        nextmem = (DdHashItem **) memlist[0];
613        FREE(memlist);
614        memlist = nextmem;
615    }
616
617    FREE(hash->bucket);
618    FREE(hash);
619#ifdef __osf__
620#pragma pointer_size restore
621#endif
622
623    return;
624
625} /* end of cuddHashTableQuit */
626
627
628/**Function********************************************************************
629
630  Synopsis    [Inserts an item in a hash table.]
631
632  Description [Inserts an item in a hash table when the key has more than
633  three pointers.  Returns 1 if successful; 0 otherwise.]
634
635  SideEffects [None]
636
637  SeeAlso     [[cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableInsert3
638  cuddHashTableLookup]
639
640******************************************************************************/
641int
642cuddHashTableInsert(
643  DdHashTable * hash,
644  DdNodePtr * key,
645  DdNode * value,
646  ptrint count)
647{
648    int result;
649    unsigned int posn;
650    DdHashItem *item;
651    unsigned int i;
652
653#ifdef DD_DEBUG
654    assert(hash->keysize > 3);
655#endif
656
657    if (hash->size > hash->maxsize) {
658        result = cuddHashTableResize(hash);
659        if (result == 0) return(0);
660    }
661    item = cuddHashTableAlloc(hash);
662    if (item == NULL) return(0);
663    hash->size++;
664    item->value = value;
665    cuddRef(value);
666    item->count = count;
667    for (i = 0; i < hash->keysize; i++) {
668        item->key[i] = key[i];
669    }
670    posn = ddLCHash(key,hash->keysize,hash->shift);
671    item->next = hash->bucket[posn];
672    hash->bucket[posn] = item;
673
674    return(1);
675
676} /* end of cuddHashTableInsert */
677
678
679/**Function********************************************************************
680
681  Synopsis    [Looks up a key in a hash table.]
682
683  Description [Looks up a key consisting of more than three pointers
684  in a hash table.  Returns the value associated to the key if there
685  is an entry for the given key in the table; NULL otherwise. If the
686  entry is present, its reference counter is decremented if not
687  saturated. If the counter reaches 0, the value of the entry is
688  dereferenced, and the entry is returned to the free list.]
689
690  SideEffects [None]
691
692  SeeAlso     [cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableLookup3
693  cuddHashTableInsert]
694
695******************************************************************************/
696DdNode *
697cuddHashTableLookup(
698  DdHashTable * hash,
699  DdNodePtr * key)
700{
701    unsigned int posn;
702    DdHashItem *item, *prev;
703    unsigned int i, keysize;
704
705#ifdef DD_DEBUG
706    assert(hash->keysize > 3);
707#endif
708
709    posn = ddLCHash(key,hash->keysize,hash->shift);
710    item = hash->bucket[posn];
711    prev = NULL;
712
713    keysize = hash->keysize;
714    while (item != NULL) {
715        DdNodePtr *key2 = item->key;
716        int equal = 1;
717        for (i = 0; i < keysize; i++) {
718            if (key[i] != key2[i]) {
719                equal = 0;
720                break;
721            }
722        }
723        if (equal) {
724            DdNode *value = item->value;
725            cuddSatDec(item->count);
726            if (item->count == 0) {
727                cuddDeref(value);
728                if (prev == NULL) {
729                    hash->bucket[posn] = item->next;
730                } else {
731                    prev->next = item->next;
732                }
733                item->next = hash->nextFree;
734                hash->nextFree = item;
735                hash->size--;
736            }
737            return(value);
738        }
739        prev = item;
740        item = item->next;
741    }
742    return(NULL);
743
744} /* end of cuddHashTableLookup */
745
746
747/**Function********************************************************************
748
749  Synopsis    [Inserts an item in a hash table.]
750
751  Description [Inserts an item in a hash table when the key is one pointer.
752  Returns 1 if successful; 0 otherwise.]
753
754  SideEffects [None]
755
756  SeeAlso     [cuddHashTableInsert cuddHashTableInsert2 cuddHashTableInsert3
757  cuddHashTableLookup1]
758
759******************************************************************************/
760int
761cuddHashTableInsert1(
762  DdHashTable * hash,
763  DdNode * f,
764  DdNode * value,
765  ptrint count)
766{
767    int result;
768    unsigned int posn;
769    DdHashItem *item;
770
771#ifdef DD_DEBUG
772    assert(hash->keysize == 1);
773#endif
774
775    if (hash->size > hash->maxsize) {
776        result = cuddHashTableResize(hash);
777        if (result == 0) return(0);
778    }
779    item = cuddHashTableAlloc(hash);
780    if (item == NULL) return(0);
781    hash->size++;
782    item->value = value;
783    cuddRef(value);
784    item->count = count;
785    item->key[0] = f;
786    posn = ddLCHash2(f,f,hash->shift);
787    item->next = hash->bucket[posn];
788    hash->bucket[posn] = item;
789
790    return(1);
791
792} /* end of cuddHashTableInsert1 */
793
794
795/**Function********************************************************************
796
797  Synopsis    [Looks up a key consisting of one pointer in a hash table.]
798
799  Description [Looks up a key consisting of one pointer in a hash table.
800  Returns the value associated to the key if there is an entry for the given
801  key in the table; NULL otherwise. If the entry is present, its reference
802  counter is decremented if not saturated. If the counter reaches 0, the
803  value of the entry is dereferenced, and the entry is returned to the free
804  list.]
805
806  SideEffects [None]
807
808  SeeAlso     [cuddHashTableLookup cuddHashTableLookup2 cuddHashTableLookup3
809  cuddHashTableInsert1]
810
811******************************************************************************/
812DdNode *
813cuddHashTableLookup1(
814  DdHashTable * hash,
815  DdNode * f)
816{
817    unsigned int posn;
818    DdHashItem *item, *prev;
819
820#ifdef DD_DEBUG
821    assert(hash->keysize == 1);
822#endif
823
824    posn = ddLCHash2(f,f,hash->shift);
825    item = hash->bucket[posn];
826    prev = NULL;
827
828    while (item != NULL) {
829        DdNodePtr *key = item->key;
830        if (f == key[0]) {
831            DdNode *value = item->value;
832            cuddSatDec(item->count);
833            if (item->count == 0) {
834                cuddDeref(value);
835                if (prev == NULL) {
836                    hash->bucket[posn] = item->next;
837                } else {
838                    prev->next = item->next;
839                }
840                item->next = hash->nextFree;
841                hash->nextFree = item;
842                hash->size--;
843            }
844            return(value);
845        }
846        prev = item;
847        item = item->next;
848    }
849    return(NULL);
850
851} /* end of cuddHashTableLookup1 */
852
853
854/**Function********************************************************************
855
856  Synopsis    [Inserts an item in a hash table.]
857
858  Description [Inserts an item in a hash table when the key is
859  composed of two pointers. Returns 1 if successful; 0 otherwise.]
860
861  SideEffects [None]
862
863  SeeAlso     [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert3
864  cuddHashTableLookup2]
865
866******************************************************************************/
867int
868cuddHashTableInsert2(
869  DdHashTable * hash,
870  DdNode * f,
871  DdNode * g,
872  DdNode * value,
873  ptrint count)
874{
875    int result;
876    unsigned int posn;
877    DdHashItem *item;
878
879#ifdef DD_DEBUG
880    assert(hash->keysize == 2);
881#endif
882
883    if (hash->size > hash->maxsize) {
884        result = cuddHashTableResize(hash);
885        if (result == 0) return(0);
886    }
887    item = cuddHashTableAlloc(hash);
888    if (item == NULL) return(0);
889    hash->size++;
890    item->value = value;
891    cuddRef(value);
892    item->count = count;
893    item->key[0] = f;
894    item->key[1] = g;
895    posn = ddLCHash2(f,g,hash->shift);
896    item->next = hash->bucket[posn];
897    hash->bucket[posn] = item;
898
899    return(1);
900
901} /* end of cuddHashTableInsert2 */
902
903
904/**Function********************************************************************
905
906  Synopsis    [Looks up a key consisting of two pointers in a hash table.]
907
908  Description [Looks up a key consisting of two pointer in a hash table.
909  Returns the value associated to the key if there is an entry for the given
910  key in the table; NULL otherwise. If the entry is present, its reference
911  counter is decremented if not saturated. If the counter reaches 0, the
912  value of the entry is dereferenced, and the entry is returned to the free
913  list.]
914
915  SideEffects [None]
916
917  SeeAlso     [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup3
918  cuddHashTableInsert2]
919
920******************************************************************************/
921DdNode *
922cuddHashTableLookup2(
923  DdHashTable * hash,
924  DdNode * f,
925  DdNode * g)
926{
927    unsigned int posn;
928    DdHashItem *item, *prev;
929
930#ifdef DD_DEBUG
931    assert(hash->keysize == 2);
932#endif
933
934    posn = ddLCHash2(f,g,hash->shift);
935    item = hash->bucket[posn];
936    prev = NULL;
937
938    while (item != NULL) {
939        DdNodePtr *key = item->key;
940        if ((f == key[0]) && (g == key[1])) {
941            DdNode *value = item->value;
942            cuddSatDec(item->count);
943            if (item->count == 0) {
944                cuddDeref(value);
945                if (prev == NULL) {
946                    hash->bucket[posn] = item->next;
947                } else {
948                    prev->next = item->next;
949                }
950                item->next = hash->nextFree;
951                hash->nextFree = item;
952                hash->size--;
953            }
954            return(value);
955        }
956        prev = item;
957        item = item->next;
958    }
959    return(NULL);
960
961} /* end of cuddHashTableLookup2 */
962
963
964/**Function********************************************************************
965
966  Synopsis    [Inserts an item in a hash table.]
967
968  Description [Inserts an item in a hash table when the key is
969  composed of three pointers. Returns 1 if successful; 0 otherwise.]
970
971  SideEffects [None]
972
973  SeeAlso     [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert2
974  cuddHashTableLookup3]
975
976******************************************************************************/
977int
978cuddHashTableInsert3(
979  DdHashTable * hash,
980  DdNode * f,
981  DdNode * g,
982  DdNode * h,
983  DdNode * value,
984  ptrint count)
985{
986    int result;
987    unsigned int posn;
988    DdHashItem *item;
989
990#ifdef DD_DEBUG
991    assert(hash->keysize == 3);
992#endif
993
994    if (hash->size > hash->maxsize) {
995        result = cuddHashTableResize(hash);
996        if (result == 0) return(0);
997    }
998    item = cuddHashTableAlloc(hash);
999    if (item == NULL) return(0);
1000    hash->size++;
1001    item->value = value;
1002    cuddRef(value);
1003    item->count = count;
1004    item->key[0] = f;
1005    item->key[1] = g;
1006    item->key[2] = h;
1007    posn = ddLCHash3(f,g,h,hash->shift);
1008    item->next = hash->bucket[posn];
1009    hash->bucket[posn] = item;
1010
1011    return(1);
1012
1013} /* end of cuddHashTableInsert3 */
1014
1015
1016/**Function********************************************************************
1017
1018  Synopsis    [Looks up a key consisting of three pointers in a hash table.]
1019
1020  Description [Looks up a key consisting of three pointers in a hash table.
1021  Returns the value associated to the key if there is an entry for the given
1022  key in the table; NULL otherwise. If the entry is present, its reference
1023  counter is decremented if not saturated. If the counter reaches 0, the
1024  value of the entry is dereferenced, and the entry is returned to the free
1025  list.]
1026
1027  SideEffects [None]
1028
1029  SeeAlso     [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup2
1030  cuddHashTableInsert3]
1031
1032******************************************************************************/
1033DdNode *
1034cuddHashTableLookup3(
1035  DdHashTable * hash,
1036  DdNode * f,
1037  DdNode * g,
1038  DdNode * h)
1039{
1040    unsigned int posn;
1041    DdHashItem *item, *prev;
1042
1043#ifdef DD_DEBUG
1044    assert(hash->keysize == 3);
1045#endif
1046
1047    posn = ddLCHash3(f,g,h,hash->shift);
1048    item = hash->bucket[posn];
1049    prev = NULL;
1050
1051    while (item != NULL) {
1052        DdNodePtr *key = item->key;
1053        if ((f == key[0]) && (g == key[1]) && (h == key[2])) {
1054            DdNode *value = item->value;
1055            cuddSatDec(item->count);
1056            if (item->count == 0) {
1057                cuddDeref(value);
1058                if (prev == NULL) {
1059                    hash->bucket[posn] = item->next;
1060                } else {
1061                    prev->next = item->next;
1062                }
1063                item->next = hash->nextFree;
1064                hash->nextFree = item;
1065                hash->size--;
1066            }
1067            return(value);
1068        }
1069        prev = item;
1070        item = item->next;
1071    }
1072    return(NULL);
1073
1074} /* end of cuddHashTableLookup3 */
1075
1076
1077/*---------------------------------------------------------------------------*/
1078/* Definition of static functions                                            */
1079/*---------------------------------------------------------------------------*/
1080
1081
1082/**Function********************************************************************
1083
1084  Synopsis    [Resizes a local cache.]
1085
1086  Description []
1087
1088  SideEffects [None]
1089
1090  SeeAlso     []
1091
1092******************************************************************************/
1093static void
1094cuddLocalCacheResize(
1095  DdLocalCache * cache)
1096{
1097    DdLocalCacheItem *item, *olditem, *entry, *old;
1098    int i, shift;
1099    unsigned int posn;
1100    unsigned int slots, oldslots;
1101    extern DD_OOMFP MMoutOfMemory;
1102    DD_OOMFP saveHandler;
1103
1104    olditem = cache->item;
1105    oldslots = cache->slots;
1106    slots = cache->slots = oldslots << 1;
1107
1108#ifdef DD_VERBOSE
1109    (void) fprintf(cache->manager->err,
1110                   "Resizing local cache from %d to %d entries\n",
1111                   oldslots, slots);
1112    (void) fprintf(cache->manager->err,
1113                   "\thits = %.0f\tlookups = %.0f\thit ratio = %5.3f\n",
1114                   cache->hits, cache->lookUps, cache->hits / cache->lookUps);
1115#endif
1116
1117    saveHandler = MMoutOfMemory;
1118    MMoutOfMemory = Cudd_OutOfMem;
1119    cache->item = item =
1120        (DdLocalCacheItem *) ALLOC(char, slots * cache->itemsize);
1121    MMoutOfMemory = saveHandler;
1122    /* If we fail to allocate the new table we just give up. */
1123    if (item == NULL) {
1124#ifdef DD_VERBOSE
1125        (void) fprintf(cache->manager->err,"Resizing failed. Giving up.\n");
1126#endif
1127        cache->slots = oldslots;
1128        cache->item = olditem;
1129        /* Do not try to resize again. */
1130        cache->maxslots = oldslots - 1;
1131        return;
1132    }
1133    shift = --(cache->shift);
1134    cache->manager->memused += (slots - oldslots) * cache->itemsize;
1135
1136    /* Clear new cache. */
1137    memset(item, 0, slots * cache->itemsize);
1138
1139    /* Copy from old cache to new one. */
1140    for (i = 0; (unsigned) i < oldslots; i++) {
1141        old = (DdLocalCacheItem *) ((char *) olditem + i * cache->itemsize);
1142        if (old->value != NULL) {
1143            posn = ddLCHash(old->key,cache->keysize,shift);
1144            entry = (DdLocalCacheItem *) ((char *) item +
1145                                          posn * cache->itemsize);
1146            memcpy(entry->key,old->key,cache->keysize*sizeof(DdNode *));
1147            entry->value = old->value; 
1148        }
1149    }
1150
1151    FREE(olditem);
1152
1153    /* Reinitialize measurements so as to avoid division by 0 and
1154    ** immediate resizing.
1155    */
1156    cache->lookUps = (double) (int) (slots * cache->minHit + 1);
1157    cache->hits = 0;
1158
1159} /* end of cuddLocalCacheResize */
1160
1161
1162/**Function********************************************************************
1163
1164  Synopsis    [Computes the hash value for a local cache.]
1165
1166  Description [Computes the hash value for a local cache. Returns the
1167  bucket index.]
1168
1169  SideEffects [None]
1170
1171  SeeAlso     []
1172
1173******************************************************************************/
1174DD_INLINE
1175static unsigned int
1176ddLCHash(
1177  DdNodePtr * key,
1178  unsigned int keysize,
1179  int shift)
1180{
1181    unsigned int val = (unsigned int) (ptrint) key[0] * DD_P2;
1182    unsigned int i;
1183
1184    for (i = 1; i < keysize; i++) {
1185        val = val * DD_P1 + (int) (ptrint) key[i];
1186    }
1187
1188    return(val >> shift);
1189
1190} /* end of ddLCHash */
1191
1192
1193/**Function********************************************************************
1194
1195  Synopsis    [Inserts a local cache in the manager list.]
1196
1197  Description []
1198
1199  SideEffects [None]
1200
1201  SeeAlso     []
1202
1203******************************************************************************/
1204static void
1205cuddLocalCacheAddToList(
1206  DdLocalCache * cache)
1207{
1208    DdManager *manager = cache->manager;
1209
1210    cache->next = manager->localCaches;
1211    manager->localCaches = cache;
1212    return;
1213
1214} /* end of cuddLocalCacheAddToList */
1215
1216
1217/**Function********************************************************************
1218
1219  Synopsis    [Removes a local cache from the manager list.]
1220
1221  Description []
1222
1223  SideEffects [None]
1224
1225  SeeAlso     []
1226
1227******************************************************************************/
1228static void
1229cuddLocalCacheRemoveFromList(
1230  DdLocalCache * cache)
1231{
1232    DdManager *manager = cache->manager;
1233#ifdef __osf__
1234#pragma pointer_size save
1235#pragma pointer_size short
1236#endif
1237    DdLocalCache **prevCache, *nextCache;
1238#ifdef __osf__
1239#pragma pointer_size restore
1240#endif
1241
1242    prevCache = &(manager->localCaches);
1243    nextCache = manager->localCaches;
1244
1245    while (nextCache != NULL) {
1246        if (nextCache == cache) {
1247            *prevCache = nextCache->next;
1248            return;
1249        }
1250        prevCache = &(nextCache->next);
1251        nextCache = nextCache->next;
1252    }
1253    return;                     /* should never get here */
1254
1255} /* end of cuddLocalCacheRemoveFromList */
1256
1257
1258/**Function********************************************************************
1259
1260  Synopsis    [Resizes a hash table.]
1261
1262  Description [Resizes a hash table. Returns 1 if successful; 0
1263  otherwise.]
1264
1265  SideEffects [None]
1266
1267  SeeAlso     [cuddHashTableInsert]
1268
1269******************************************************************************/
1270static int
1271cuddHashTableResize(
1272  DdHashTable * hash)
1273{
1274    int j;
1275    unsigned int posn;
1276    DdHashItem *item;
1277    DdHashItem *next;
1278#ifdef __osf__
1279#pragma pointer_size save
1280#pragma pointer_size short
1281#endif
1282    DdNode **key;
1283    int numBuckets;
1284    DdHashItem **buckets;
1285    DdHashItem **oldBuckets = hash->bucket;
1286#ifdef __osf__
1287#pragma pointer_size restore
1288#endif
1289    int shift;
1290    int oldNumBuckets = hash->numBuckets;
1291    extern DD_OOMFP MMoutOfMemory;
1292    DD_OOMFP saveHandler;
1293
1294    /* Compute the new size of the table. */
1295    numBuckets = oldNumBuckets << 1;
1296    saveHandler = MMoutOfMemory;
1297    MMoutOfMemory = Cudd_OutOfMem;
1298#ifdef __osf__
1299#pragma pointer_size save
1300#pragma pointer_size short
1301#endif
1302    buckets = ALLOC(DdHashItem *, numBuckets);
1303    MMoutOfMemory = saveHandler;
1304    if (buckets == NULL) {
1305        hash->maxsize <<= 1;
1306        return(1);
1307    }
1308
1309    hash->bucket = buckets;
1310    hash->numBuckets = numBuckets;
1311    shift = --(hash->shift);
1312    hash->maxsize <<= 1;
1313    memset(buckets, 0, numBuckets * sizeof(DdHashItem *));
1314#ifdef __osf__
1315#pragma pointer_size restore
1316#endif
1317    if (hash->keysize == 1) {
1318        for (j = 0; j < oldNumBuckets; j++) {
1319            item = oldBuckets[j];
1320            while (item != NULL) {
1321                next = item->next;
1322                key = item->key;
1323                posn = ddLCHash2(key[0], key[0], shift);
1324                item->next = buckets[posn];
1325                buckets[posn] = item;
1326                item = next;
1327            }
1328        }
1329    } else if (hash->keysize == 2) {
1330        for (j = 0; j < oldNumBuckets; j++) {
1331            item = oldBuckets[j];
1332            while (item != NULL) {
1333                next = item->next;
1334                key = item->key;
1335                posn = ddLCHash2(key[0], key[1], shift);
1336                item->next = buckets[posn];
1337                buckets[posn] = item;
1338                item = next;
1339            }
1340        }
1341    } else if (hash->keysize == 3) {
1342        for (j = 0; j < oldNumBuckets; j++) {
1343            item = oldBuckets[j];
1344            while (item != NULL) {
1345                next = item->next;
1346                key = item->key;
1347                posn = ddLCHash3(key[0], key[1], key[2], shift);
1348                item->next = buckets[posn];
1349                buckets[posn] = item;
1350                item = next;
1351            }
1352        }
1353    } else {
1354        for (j = 0; j < oldNumBuckets; j++) {
1355            item = oldBuckets[j];
1356            while (item != NULL) {
1357                next = item->next;
1358                posn = ddLCHash(item->key, hash->keysize, shift);
1359                item->next = buckets[posn];
1360                buckets[posn] = item;
1361                item = next;
1362            }
1363        }
1364    }
1365    FREE(oldBuckets);
1366    return(1);
1367
1368} /* end of cuddHashTableResize */
1369
1370
1371/**Function********************************************************************
1372
1373  Synopsis    [Fast storage allocation for items in a hash table.]
1374
1375  Description [Fast storage allocation for items in a hash table. The
1376  first 4 bytes of a chunk contain a pointer to the next block; the
1377  rest contains DD_MEM_CHUNK spaces for hash items.  Returns a pointer to
1378  a new item if successful; NULL is memory is full.]
1379
1380  SideEffects [None]
1381
1382  SeeAlso     [cuddAllocNode cuddDynamicAllocNode]
1383
1384******************************************************************************/
1385DD_INLINE
1386static DdHashItem *
1387cuddHashTableAlloc(
1388  DdHashTable * hash)
1389{
1390    int i;
1391    unsigned int itemsize = hash->itemsize;
1392    extern DD_OOMFP MMoutOfMemory;
1393    DD_OOMFP saveHandler;
1394#ifdef __osf__
1395#pragma pointer_size save
1396#pragma pointer_size short
1397#endif
1398    DdHashItem **mem, *thisOne, *next, *item;
1399
1400    if (hash->nextFree == NULL) {
1401        saveHandler = MMoutOfMemory;
1402        MMoutOfMemory = Cudd_OutOfMem;
1403        mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
1404        MMoutOfMemory = saveHandler;
1405#ifdef __osf__
1406#pragma pointer_size restore
1407#endif
1408        if (mem == NULL) {
1409            if (hash->manager->stash != NULL) {
1410                FREE(hash->manager->stash);
1411                hash->manager->stash = NULL;
1412                /* Inhibit resizing of tables. */
1413                hash->manager->maxCacheHard = hash->manager->cacheSlots - 1;
1414                hash->manager->cacheSlack = -(hash->manager->cacheSlots + 1);
1415                for (i = 0; i < hash->manager->size; i++) {
1416                    hash->manager->subtables[i].maxKeys <<= 2;
1417                }
1418                hash->manager->gcFrac = 0.2;
1419                hash->manager->minDead =
1420                    (unsigned) (0.2 * (double) hash->manager->slots);
1421#ifdef __osf__
1422#pragma pointer_size save
1423#pragma pointer_size short
1424#endif
1425                mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
1426#ifdef __osf__
1427#pragma pointer_size restore
1428#endif
1429            }
1430            if (mem == NULL) {
1431                (*MMoutOfMemory)((long)((DD_MEM_CHUNK + 1) * itemsize));
1432                hash->manager->errorCode = CUDD_MEMORY_OUT;
1433                return(NULL);
1434            }
1435        }
1436
1437        mem[0] = (DdHashItem *) hash->memoryList;
1438        hash->memoryList = mem;
1439
1440        thisOne = (DdHashItem *) ((char *) mem + itemsize);
1441        hash->nextFree = thisOne;
1442        for (i = 1; i < DD_MEM_CHUNK; i++) {
1443            next = (DdHashItem *) ((char *) thisOne + itemsize);
1444            thisOne->next = next;
1445            thisOne = next;
1446        }
1447
1448        thisOne->next = NULL;
1449
1450    }
1451    item = hash->nextFree;
1452    hash->nextFree = item->next;
1453    return(item);
1454
1455} /* end of cuddHashTableAlloc */
Note: See TracBrowser for help on using the repository browser.