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