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

Last change on this file since 104 was 13, checked in by cecile, 15 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.