source: vis_dev/glu-2.3/src/cuBdd/cuddCache.c @ 100

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

library glu 2.3

File size: 27.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddCache.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for cache insertion and lookup.]
8
9  Description [Internal procedures included in this module:
10                <ul>
11                <li> cuddInitCache()
12                <li> cuddCacheInsert()
13                <li> cuddCacheInsert2()
14                <li> cuddCacheLookup()
15                <li> cuddCacheLookupZdd()
16                <li> cuddCacheLookup2()
17                <li> cuddCacheLookup2Zdd()
18                <li> cuddConstantLookup()
19                <li> cuddCacheProfile()
20                <li> cuddCacheResize()
21                <li> cuddCacheFlush()
22                <li> cuddComputeFloorLog2()
23                </ul>
24            Static procedures included in this module:
25                <ul>
26                </ul> ]
27
28  SeeAlso     []
29
30  Author      [Fabio Somenzi]
31
32  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
33
34  All rights reserved.
35
36  Redistribution and use in source and binary forms, with or without
37  modification, are permitted provided that the following conditions
38  are met:
39
40  Redistributions of source code must retain the above copyright
41  notice, this list of conditions and the following disclaimer.
42
43  Redistributions in binary form must reproduce the above copyright
44  notice, this list of conditions and the following disclaimer in the
45  documentation and/or other materials provided with the distribution.
46
47  Neither the name of the University of Colorado nor the names of its
48  contributors may be used to endorse or promote products derived from
49  this software without specific prior written permission.
50
51  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
52  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
53  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
54  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
55  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
56  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
57  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
58  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
59  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
60  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
61  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
62  POSSIBILITY OF SUCH DAMAGE.]
63
64******************************************************************************/
65
66#include "util.h"
67#include "cuddInt.h"
68
69/*---------------------------------------------------------------------------*/
70/* Constant declarations                                                     */
71/*---------------------------------------------------------------------------*/
72
73#ifdef DD_CACHE_PROFILE
74#define DD_HYSTO_BINS 8
75#endif
76
77/*---------------------------------------------------------------------------*/
78/* Stucture declarations                                                     */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Type declarations                                                         */
84/*---------------------------------------------------------------------------*/
85
86
87/*---------------------------------------------------------------------------*/
88/* Variable declarations                                                     */
89/*---------------------------------------------------------------------------*/
90
91#ifndef lint
92static char rcsid[] DD_UNUSED = "$Id: cuddCache.c,v 1.34 2009/02/19 16:17:50 fabio Exp $";
93#endif
94
95/*---------------------------------------------------------------------------*/
96/* Macro declarations                                                        */
97/*---------------------------------------------------------------------------*/
98
99
100/**AutomaticStart*************************************************************/
101
102/*---------------------------------------------------------------------------*/
103/* Static function prototypes                                                */
104/*---------------------------------------------------------------------------*/
105
106
107/**AutomaticEnd***************************************************************/
108
109
110/*---------------------------------------------------------------------------*/
111/* Definition of exported functions                                          */
112/*---------------------------------------------------------------------------*/
113
114/*---------------------------------------------------------------------------*/
115/* Definition of internal functions                                          */
116/*---------------------------------------------------------------------------*/
117
118
119/**Function********************************************************************
120
121  Synopsis    [Initializes the computed table.]
122
123  Description [Initializes the computed table. It is called by
124  Cudd_Init. Returns 1 in case of success; 0 otherwise.]
125
126  SideEffects [None]
127
128  SeeAlso     [Cudd_Init]
129
130******************************************************************************/
131int
132cuddInitCache(
133  DdManager * unique /* unique table */,
134  unsigned int cacheSize /* initial size of the cache */,
135  unsigned int maxCacheSize /* cache size beyond which no resizing occurs */)
136{
137    int i;
138    unsigned int logSize;
139#ifndef DD_CACHE_PROFILE
140    DdNodePtr *mem;
141    ptruint offset;
142#endif
143
144    /* Round cacheSize to largest power of 2 not greater than the requested
145    ** initial cache size. */
146    logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
147    cacheSize = 1 << logSize;
148    unique->acache = ALLOC(DdCache,cacheSize+1);
149    if (unique->acache == NULL) {
150        unique->errorCode = CUDD_MEMORY_OUT;
151        return(0);
152    }
153    /* If the size of the cache entry is a power of 2, we want to
154    ** enforce alignment to that power of two. This happens when
155    ** DD_CACHE_PROFILE is not defined. */
156#ifdef DD_CACHE_PROFILE
157    unique->cache = unique->acache;
158    unique->memused += (cacheSize) * sizeof(DdCache);
159#else
160    mem = (DdNodePtr *) unique->acache;
161    offset = (ptruint) mem & (sizeof(DdCache) - 1);
162    mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr);
163    unique->cache = (DdCache *) mem;
164    assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0);
165    unique->memused += (cacheSize+1) * sizeof(DdCache);
166#endif
167    unique->cacheSlots = cacheSize;
168    unique->cacheShift = sizeof(int) * 8 - logSize;
169    unique->maxCacheHard = maxCacheSize;
170    /* If cacheSlack is non-negative, we can resize. */
171    unique->cacheSlack = (int) ddMin(maxCacheSize,
172        DD_MAX_CACHE_TO_SLOTS_RATIO*unique->slots) -
173        2 * (int) cacheSize;
174    Cudd_SetMinHit(unique,DD_MIN_HIT);
175    /* Initialize to avoid division by 0 and immediate resizing. */
176    unique->cacheMisses = (double) (int) (cacheSize * unique->minHit + 1);
177    unique->cacheHits = 0;
178    unique->totCachehits = 0;
179    /* The sum of cacheMisses and totCacheMisses is always correct,
180    ** even though cacheMisses is larger than it should for the reasons
181    ** explained above. */
182    unique->totCacheMisses = -unique->cacheMisses;
183    unique->cachecollisions = 0;
184    unique->cacheinserts = 0;
185    unique->cacheLastInserts = 0;
186    unique->cachedeletions = 0;
187
188    /* Initialize the cache */
189    for (i = 0; (unsigned) i < cacheSize; i++) {
190        unique->cache[i].h = 0; /* unused slots */
191        unique->cache[i].data = NULL; /* invalid entry */
192#ifdef DD_CACHE_PROFILE
193        unique->cache[i].count = 0;
194#endif
195    }
196
197    return(1);
198
199} /* end of cuddInitCache */
200
201
202/**Function********************************************************************
203
204  Synopsis    [Inserts a result in the cache.]
205
206  Description []
207
208  SideEffects [None]
209
210  SeeAlso     [cuddCacheInsert2 cuddCacheInsert1]
211
212******************************************************************************/
213void
214cuddCacheInsert(
215  DdManager * table,
216  ptruint op,
217  DdNode * f,
218  DdNode * g,
219  DdNode * h,
220  DdNode * data)
221{
222    int posn;
223    register DdCache *entry;
224    ptruint uf, ug, uh;
225
226    uf = (ptruint) f | (op & 0xe);
227    ug = (ptruint) g | (op >> 4);
228    uh = (ptruint) h;
229
230    posn = ddCHash2(uh,uf,ug,table->cacheShift);
231    entry = &table->cache[posn];
232
233    table->cachecollisions += entry->data != NULL;
234    table->cacheinserts++;
235
236    entry->f    = (DdNode *) uf;
237    entry->g    = (DdNode *) ug;
238    entry->h    = uh;
239    entry->data = data;
240#ifdef DD_CACHE_PROFILE
241    entry->count++;
242#endif
243
244} /* end of cuddCacheInsert */
245
246
247/**Function********************************************************************
248
249  Synopsis    [Inserts a result in the cache for a function with two
250  operands.]
251
252  Description []
253
254  SideEffects [None]
255
256  SeeAlso     [cuddCacheInsert cuddCacheInsert1]
257
258******************************************************************************/
259void
260cuddCacheInsert2(
261  DdManager * table,
262  DD_CTFP op,
263  DdNode * f,
264  DdNode * g,
265  DdNode * data)
266{
267    int posn;
268    register DdCache *entry;
269
270    posn = ddCHash2(op,f,g,table->cacheShift);
271    entry = &table->cache[posn];
272
273    if (entry->data != NULL) {
274        table->cachecollisions++;
275    }
276    table->cacheinserts++;
277
278    entry->f = f;
279    entry->g = g;
280    entry->h = (ptruint) op;
281    entry->data = data;
282#ifdef DD_CACHE_PROFILE
283    entry->count++;
284#endif
285
286} /* end of cuddCacheInsert2 */
287
288
289/**Function********************************************************************
290
291  Synopsis    [Inserts a result in the cache for a function with two
292  operands.]
293
294  Description []
295
296  SideEffects [None]
297
298  SeeAlso     [cuddCacheInsert cuddCacheInsert2]
299
300******************************************************************************/
301void
302cuddCacheInsert1(
303  DdManager * table,
304  DD_CTFP1 op,
305  DdNode * f,
306  DdNode * data)
307{
308    int posn;
309    register DdCache *entry;
310
311    posn = ddCHash2(op,f,f,table->cacheShift);
312    entry = &table->cache[posn];
313
314    if (entry->data != NULL) {
315        table->cachecollisions++;
316    }
317    table->cacheinserts++;
318
319    entry->f = f;
320    entry->g = f;
321    entry->h = (ptruint) op;
322    entry->data = data;
323#ifdef DD_CACHE_PROFILE
324    entry->count++;
325#endif
326
327} /* end of cuddCacheInsert1 */
328
329
330/**Function********************************************************************
331
332  Synopsis    [Looks up in the cache for the result of op applied to f,
333  g, and h.]
334
335  Description [Returns the result if found; it returns NULL if no
336  result is found.]
337
338  SideEffects [None]
339
340  SeeAlso     [cuddCacheLookup2 cuddCacheLookup1]
341
342******************************************************************************/
343DdNode *
344cuddCacheLookup(
345  DdManager * table,
346  ptruint op,
347  DdNode * f,
348  DdNode * g,
349  DdNode * h)
350{
351    int posn;
352    DdCache *en,*cache;
353    DdNode *data;
354    ptruint uf, ug, uh;
355
356    uf = (ptruint) f | (op & 0xe);
357    ug = (ptruint) g | (op >> 4);
358    uh = (ptruint) h;
359
360    cache = table->cache;
361#ifdef DD_DEBUG
362    if (cache == NULL) {
363        return(NULL);
364    }
365#endif
366
367    posn = ddCHash2(uh,uf,ug,table->cacheShift);
368    en = &cache[posn];
369    if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
370        en->h==uh) {
371        data = Cudd_Regular(en->data);
372        table->cacheHits++;
373        if (data->ref == 0) {
374            cuddReclaim(table,data);
375        }
376        return(en->data);
377    }
378
379    /* Cache miss: decide whether to resize. */
380    table->cacheMisses++;
381
382    if (table->cacheSlack >= 0 &&
383        table->cacheHits > table->cacheMisses * table->minHit) {
384        cuddCacheResize(table);
385    }
386
387    return(NULL);
388
389} /* end of cuddCacheLookup */
390
391
392/**Function********************************************************************
393
394  Synopsis    [Looks up in the cache for the result of op applied to f,
395  g, and h.]
396
397  Description [Returns the result if found; it returns NULL if no
398  result is found.]
399
400  SideEffects [None]
401
402  SeeAlso     [cuddCacheLookup2Zdd cuddCacheLookup1Zdd]
403
404******************************************************************************/
405DdNode *
406cuddCacheLookupZdd(
407  DdManager * table,
408  ptruint op,
409  DdNode * f,
410  DdNode * g,
411  DdNode * h)
412{
413    int posn;
414    DdCache *en,*cache;
415    DdNode *data;
416    ptruint uf, ug, uh;
417
418    uf = (ptruint) f | (op & 0xe);
419    ug = (ptruint) g | (op >> 4);
420    uh = (ptruint) h;
421
422    cache = table->cache;
423#ifdef DD_DEBUG
424    if (cache == NULL) {
425        return(NULL);
426    }
427#endif
428
429    posn = ddCHash2(uh,uf,ug,table->cacheShift);
430    en = &cache[posn];
431    if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
432        en->h==uh) {
433        data = Cudd_Regular(en->data);
434        table->cacheHits++;
435        if (data->ref == 0) {
436            cuddReclaimZdd(table,data);
437        }
438        return(en->data);
439    }
440
441    /* Cache miss: decide whether to resize. */
442    table->cacheMisses++;
443
444    if (table->cacheSlack >= 0 &&
445        table->cacheHits > table->cacheMisses * table->minHit) {
446        cuddCacheResize(table);
447    }
448
449    return(NULL);
450
451} /* end of cuddCacheLookupZdd */
452
453
454/**Function********************************************************************
455
456  Synopsis    [Looks up in the cache for the result of op applied to f
457  and g.]
458
459  Description [Returns the result if found; it returns NULL if no
460  result is found.]
461
462  SideEffects [None]
463
464  SeeAlso     [cuddCacheLookup cuddCacheLookup1]
465
466******************************************************************************/
467DdNode *
468cuddCacheLookup2(
469  DdManager * table,
470  DD_CTFP op,
471  DdNode * f,
472  DdNode * g)
473{
474    int posn;
475    DdCache *en,*cache;
476    DdNode *data;
477
478    cache = table->cache;
479#ifdef DD_DEBUG
480    if (cache == NULL) {
481        return(NULL);
482    }
483#endif
484
485    posn = ddCHash2(op,f,g,table->cacheShift);
486    en = &cache[posn];
487    if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
488        data = Cudd_Regular(en->data);
489        table->cacheHits++;
490        if (data->ref == 0) {
491            cuddReclaim(table,data);
492        }
493        return(en->data);
494    }
495
496    /* Cache miss: decide whether to resize. */
497    table->cacheMisses++;
498
499    if (table->cacheSlack >= 0 &&
500        table->cacheHits > table->cacheMisses * table->minHit) {
501        cuddCacheResize(table);
502    }
503
504    return(NULL);
505
506} /* end of cuddCacheLookup2 */
507
508
509/**Function********************************************************************
510
511  Synopsis [Looks up in the cache for the result of op applied to f.]
512
513  Description [Returns the result if found; it returns NULL if no
514  result is found.]
515
516  SideEffects [None]
517
518  SeeAlso     [cuddCacheLookup cuddCacheLookup2]
519
520******************************************************************************/
521DdNode *
522cuddCacheLookup1(
523  DdManager * table,
524  DD_CTFP1 op,
525  DdNode * f)
526{
527    int posn;
528    DdCache *en,*cache;
529    DdNode *data;
530
531    cache = table->cache;
532#ifdef DD_DEBUG
533    if (cache == NULL) {
534        return(NULL);
535    }
536#endif
537
538    posn = ddCHash2(op,f,f,table->cacheShift);
539    en = &cache[posn];
540    if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
541        data = Cudd_Regular(en->data);
542        table->cacheHits++;
543        if (data->ref == 0) {
544            cuddReclaim(table,data);
545        }
546        return(en->data);
547    }
548
549    /* Cache miss: decide whether to resize. */
550    table->cacheMisses++;
551
552    if (table->cacheSlack >= 0 &&
553        table->cacheHits > table->cacheMisses * table->minHit) {
554        cuddCacheResize(table);
555    }
556
557    return(NULL);
558
559} /* end of cuddCacheLookup1 */
560
561
562/**Function********************************************************************
563
564  Synopsis [Looks up in the cache for the result of op applied to f
565  and g.]
566
567  Description [Returns the result if found; it returns NULL if no
568  result is found.]
569
570  SideEffects [None]
571
572  SeeAlso     [cuddCacheLookupZdd cuddCacheLookup1Zdd]
573
574******************************************************************************/
575DdNode *
576cuddCacheLookup2Zdd(
577  DdManager * table,
578  DD_CTFP op,
579  DdNode * f,
580  DdNode * g)
581{
582    int posn;
583    DdCache *en,*cache;
584    DdNode *data;
585
586    cache = table->cache;
587#ifdef DD_DEBUG
588    if (cache == NULL) {
589        return(NULL);
590    }
591#endif
592
593    posn = ddCHash2(op,f,g,table->cacheShift);
594    en = &cache[posn];
595    if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
596        data = Cudd_Regular(en->data);
597        table->cacheHits++;
598        if (data->ref == 0) {
599            cuddReclaimZdd(table,data);
600        }
601        return(en->data);
602    }
603
604    /* Cache miss: decide whether to resize. */
605    table->cacheMisses++;
606
607    if (table->cacheSlack >= 0 &&
608        table->cacheHits > table->cacheMisses * table->minHit) {
609        cuddCacheResize(table);
610    }
611
612    return(NULL);
613
614} /* end of cuddCacheLookup2Zdd */
615
616
617/**Function********************************************************************
618
619  Synopsis [Looks up in the cache for the result of op applied to f.]
620
621  Description [Returns the result if found; it returns NULL if no
622  result is found.]
623
624  SideEffects [None]
625
626  SeeAlso     [cuddCacheLookupZdd cuddCacheLookup2Zdd]
627
628******************************************************************************/
629DdNode *
630cuddCacheLookup1Zdd(
631  DdManager * table,
632  DD_CTFP1 op,
633  DdNode * f)
634{
635    int posn;
636    DdCache *en,*cache;
637    DdNode *data;
638
639    cache = table->cache;
640#ifdef DD_DEBUG
641    if (cache == NULL) {
642        return(NULL);
643    }
644#endif
645
646    posn = ddCHash2(op,f,f,table->cacheShift);
647    en = &cache[posn];
648    if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
649        data = Cudd_Regular(en->data);
650        table->cacheHits++;
651        if (data->ref == 0) {
652            cuddReclaimZdd(table,data);
653        }
654        return(en->data);
655    }
656
657    /* Cache miss: decide whether to resize. */
658    table->cacheMisses++;
659
660    if (table->cacheSlack >= 0  &&
661        table->cacheHits > table->cacheMisses * table->minHit) {
662        cuddCacheResize(table);
663    }
664
665    return(NULL);
666
667} /* end of cuddCacheLookup1Zdd */
668
669
670/**Function********************************************************************
671
672  Synopsis [Looks up in the cache for the result of op applied to f,
673  g, and h.]
674
675  Description [Looks up in the cache for the result of op applied to f,
676  g, and h. Assumes that the calling procedure (e.g.,
677  Cudd_bddIteConstant) is only interested in whether the result is
678  constant or not. Returns the result if found (possibly
679  DD_NON_CONSTANT); otherwise it returns NULL.]
680
681  SideEffects [None]
682
683  SeeAlso     [cuddCacheLookup]
684
685******************************************************************************/
686DdNode *
687cuddConstantLookup(
688  DdManager * table,
689  ptruint op,
690  DdNode * f,
691  DdNode * g,
692  DdNode * h)
693{
694    int posn;
695    DdCache *en,*cache;
696    ptruint uf, ug, uh;
697
698    uf = (ptruint) f | (op & 0xe);
699    ug = (ptruint) g | (op >> 4);
700    uh = (ptruint) h;
701
702    cache = table->cache;
703#ifdef DD_DEBUG
704    if (cache == NULL) {
705        return(NULL);
706    }
707#endif
708    posn = ddCHash2(uh,uf,ug,table->cacheShift);
709    en = &cache[posn];
710
711    /* We do not reclaim here because the result should not be
712     * referenced, but only tested for being a constant.
713     */
714    if (en->data != NULL &&
715        en->f == (DdNodePtr)uf && en->g == (DdNodePtr)ug && en->h == uh) {
716        table->cacheHits++;
717        return(en->data);
718    }
719
720    /* Cache miss: decide whether to resize. */
721    table->cacheMisses++;
722
723    if (table->cacheSlack >= 0 &&
724        table->cacheHits > table->cacheMisses * table->minHit) {
725        cuddCacheResize(table);
726    }
727
728    return(NULL);
729
730} /* end of cuddConstantLookup */
731
732
733/**Function********************************************************************
734
735  Synopsis    [Computes and prints a profile of the cache usage.]
736
737  Description [Computes and prints a profile of the cache usage.
738  Returns 1 if successful; 0 otherwise.]
739
740  SideEffects [None]
741
742  SeeAlso     []
743
744******************************************************************************/
745int
746cuddCacheProfile(
747  DdManager * table,
748  FILE * fp)
749{
750    DdCache *cache = table->cache;
751    int slots = table->cacheSlots;
752    int nzeroes = 0;
753    int i, retval;
754    double exUsed;
755
756#ifdef DD_CACHE_PROFILE
757    double count, mean, meansq, stddev, expected;
758    long max, min;
759    int imax, imin;
760    double *hystogramQ, *hystogramR; /* histograms by quotient and remainder */
761    int nbins = DD_HYSTO_BINS;
762    int bin;
763    long thiscount;
764    double totalcount, exStddev;
765
766    meansq = mean = expected = 0.0;
767    max = min = (long) cache[0].count;
768    imax = imin = 0;
769    totalcount = 0.0;
770
771    hystogramQ = ALLOC(double, nbins);
772    if (hystogramQ == NULL) {
773        table->errorCode = CUDD_MEMORY_OUT;
774        return(0);
775    }
776    hystogramR = ALLOC(double, nbins);
777    if (hystogramR == NULL) {
778        FREE(hystogramQ);
779        table->errorCode = CUDD_MEMORY_OUT;
780        return(0);
781    }
782    for (i = 0; i < nbins; i++) {
783        hystogramQ[i] = 0;
784        hystogramR[i] = 0;
785    }
786
787    for (i = 0; i < slots; i++) {
788        thiscount = (long) cache[i].count;
789        if (thiscount > max) {
790            max = thiscount;
791            imax = i;
792        }
793        if (thiscount < min) {
794            min = thiscount;
795            imin = i;
796        }
797        if (thiscount == 0) {
798            nzeroes++;
799        }
800        count = (double) thiscount;
801        mean += count;
802        meansq += count * count;
803        totalcount += count;
804        expected += count * (double) i;
805        bin = (i * nbins) / slots;
806        hystogramQ[bin] += (double) thiscount;
807        bin = i % nbins;
808        hystogramR[bin] += (double) thiscount;
809    }
810    mean /= (double) slots;
811    meansq /= (double) slots;
812
813    /* Compute the standard deviation from both the data and the
814    ** theoretical model for a random distribution. */
815    stddev = sqrt(meansq - mean*mean);
816    exStddev = sqrt((1 - 1/(double) slots) * totalcount / (double) slots);
817
818    retval = fprintf(fp,"Cache average accesses = %g\n",  mean);
819    if (retval == EOF) return(0);
820    retval = fprintf(fp,"Cache access standard deviation = %g ", stddev);
821    if (retval == EOF) return(0);
822    retval = fprintf(fp,"(expected = %g)\n", exStddev);
823    if (retval == EOF) return(0);
824    retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
825    if (retval == EOF) return(0);
826    retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
827    if (retval == EOF) return(0);
828    exUsed = 100.0 * (1.0 - exp(-totalcount / (double) slots));
829    retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
830                     100.0 - (double) nzeroes * 100.0 / (double) slots,
831                     exUsed);
832    if (retval == EOF) return(0);
833
834    if (totalcount > 0) {
835        expected /= totalcount;
836        retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
837        if (retval == EOF) return(0);
838        retval = fprintf(fp," (expected bin value = %g)\nBy quotient:",
839                         expected);
840        if (retval == EOF) return(0);
841        for (i = nbins - 1; i>=0; i--) {
842            retval = fprintf(fp," %.0f", hystogramQ[i]);
843            if (retval == EOF) return(0);
844        }
845        retval = fprintf(fp,"\nBy residue: ");
846        if (retval == EOF) return(0);
847        for (i = nbins - 1; i>=0; i--) {
848            retval = fprintf(fp," %.0f", hystogramR[i]);
849            if (retval == EOF) return(0);
850        }
851        retval = fprintf(fp,"\n");
852        if (retval == EOF) return(0);
853    }
854
855    FREE(hystogramQ);
856    FREE(hystogramR);
857#else
858    for (i = 0; i < slots; i++) {
859        nzeroes += cache[i].h == 0;
860    }
861    exUsed = 100.0 *
862        (1.0 - exp(-(table->cacheinserts - table->cacheLastInserts) /
863                   (double) slots));
864    retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
865                     100.0 - (double) nzeroes * 100.0 / (double) slots,
866                     exUsed);
867    if (retval == EOF) return(0);
868#endif
869    return(1);
870
871} /* end of cuddCacheProfile */
872
873
874/**Function********************************************************************
875
876  Synopsis    [Resizes the cache.]
877
878  Description []
879
880  SideEffects [None]
881
882  SeeAlso     []
883
884******************************************************************************/
885void
886cuddCacheResize(
887  DdManager * table)
888{
889    DdCache *cache, *oldcache, *oldacache, *entry, *old;
890    int i;
891    int posn, shift;
892    unsigned int slots, oldslots;
893    double offset;
894    int moved = 0;
895    extern DD_OOMFP MMoutOfMemory;
896    DD_OOMFP saveHandler;
897#ifndef DD_CACHE_PROFILE
898    ptruint misalignment;
899    DdNodePtr *mem;
900#endif
901
902    oldcache = table->cache;
903    oldacache = table->acache;
904    oldslots = table->cacheSlots;
905    slots = table->cacheSlots = oldslots << 1;
906
907#ifdef DD_VERBOSE
908    (void) fprintf(table->err,"Resizing the cache from %d to %d entries\n",
909                   oldslots, slots);
910    (void) fprintf(table->err,
911                   "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
912                   table->cacheHits, table->cacheMisses,
913                   table->cacheHits / (table->cacheHits + table->cacheMisses));
914#endif
915
916    saveHandler = MMoutOfMemory;
917    MMoutOfMemory = Cudd_OutOfMem;
918    table->acache = cache = ALLOC(DdCache,slots+1);
919    MMoutOfMemory = saveHandler;
920    /* If we fail to allocate the new table we just give up. */
921    if (cache == NULL) {
922#ifdef DD_VERBOSE
923        (void) fprintf(table->err,"Resizing failed. Giving up.\n");
924#endif
925        table->cacheSlots = oldslots;
926        table->acache = oldacache;
927        /* Do not try to resize again. */
928        table->maxCacheHard = oldslots - 1;
929        table->cacheSlack = - (int) (oldslots + 1);
930        return;
931    }
932    /* If the size of the cache entry is a power of 2, we want to
933    ** enforce alignment to that power of two. This happens when
934    ** DD_CACHE_PROFILE is not defined. */
935#ifdef DD_CACHE_PROFILE
936    table->cache = cache;
937#else
938    mem = (DdNodePtr *) cache;
939    misalignment = (ptruint) mem & (sizeof(DdCache) - 1);
940    mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr);
941    table->cache = cache = (DdCache *) mem;
942    assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0);
943#endif
944    shift = --(table->cacheShift);
945    table->memused += (slots - oldslots) * sizeof(DdCache);
946    table->cacheSlack -= slots; /* need these many slots to double again */
947
948    /* Clear new cache. */
949    for (i = 0; (unsigned) i < slots; i++) {
950        cache[i].data = NULL;
951        cache[i].h = 0;
952#ifdef DD_CACHE_PROFILE
953        cache[i].count = 0;
954#endif
955    }
956
957    /* Copy from old cache to new one. */
958    for (i = 0; (unsigned) i < oldslots; i++) {
959        old = &oldcache[i];
960        if (old->data != NULL) {
961            posn = ddCHash2(old->h,old->f,old->g,shift);
962            entry = &cache[posn];
963            entry->f = old->f;
964            entry->g = old->g;
965            entry->h = old->h;
966            entry->data = old->data;
967#ifdef DD_CACHE_PROFILE
968            entry->count = 1;
969#endif
970            moved++;
971        }
972    }
973
974    FREE(oldacache);
975
976    /* Reinitialize measurements so as to avoid division by 0 and
977    ** immediate resizing.
978    */
979    offset = (double) (int) (slots * table->minHit + 1);
980    table->totCacheMisses += table->cacheMisses - offset;
981    table->cacheMisses = offset;
982    table->totCachehits += table->cacheHits;
983    table->cacheHits = 0;
984    table->cacheLastInserts = table->cacheinserts - (double) moved;
985
986} /* end of cuddCacheResize */
987
988
989/**Function********************************************************************
990
991  Synopsis    [Flushes the cache.]
992
993  Description []
994
995  SideEffects [None]
996
997  SeeAlso     []
998
999******************************************************************************/
1000void
1001cuddCacheFlush(
1002  DdManager * table)
1003{
1004    int i, slots;
1005    DdCache *cache;
1006
1007    slots = table->cacheSlots;
1008    cache = table->cache;
1009    for (i = 0; i < slots; i++) {
1010        table->cachedeletions += cache[i].data != NULL;
1011        cache[i].data = NULL;
1012    }
1013    table->cacheLastInserts = table->cacheinserts;
1014
1015    return;
1016
1017} /* end of cuddCacheFlush */
1018
1019
1020/**Function********************************************************************
1021
1022  Synopsis    [Returns the floor of the logarithm to the base 2.]
1023
1024  Description [Returns the floor of the logarithm to the base 2.
1025  The input value is assumed to be greater than 0.]
1026
1027  SideEffects [None]
1028
1029  SeeAlso     []
1030
1031******************************************************************************/
1032int
1033cuddComputeFloorLog2(
1034  unsigned int value)
1035{
1036    int floorLog = 0;
1037#ifdef DD_DEBUG
1038    assert(value > 0);
1039#endif
1040    while (value > 1) {
1041        floorLog++;
1042        value >>= 1;
1043    }
1044    return(floorLog);
1045
1046} /* end of cuddComputeFloorLog2 */
1047
1048/*---------------------------------------------------------------------------*/
1049/* Definition of static functions                                            */
1050/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.