1 /**CFile***********************************************************************
2
3 FileName [cuddRef.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions that manipulate the reference counts.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_Ref()
12 <li> Cudd_RecursiveDeref()
13 <li> Cudd_IterDerefBdd()
14 <li> Cudd_DelayedDerefBdd()
15 <li> Cudd_RecursiveDerefZdd()
16 <li> Cudd_Deref()
17 <li> Cudd_CheckZeroRef()
18 </ul>
19 Internal procedures included in this module:
20 <ul>
21 <li> cuddReclaim()
22 <li> cuddReclaimZdd()
23 <li> cuddClearDeathRow()
24 <li> cuddShrinkDeathRow()
25 <li> cuddIsInDeathRow()
26 <li> cuddTimesInDeathRow()
27 </ul>
28 ]
29
30 SeeAlso []
31
32 Author [Fabio Somenzi]
33
34 Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
35
36 All rights reserved.
37
38 Redistribution and use in source and binary forms, with or without
39 modification, are permitted provided that the following conditions
40 are met:
41
42 Redistributions of source code must retain the above copyright
43 notice, this list of conditions and the following disclaimer.
44
45 Redistributions in binary form must reproduce the above copyright
46 notice, this list of conditions and the following disclaimer in the
47 documentation and/or other materials provided with the distribution.
48
49 Neither the name of the University of Colorado nor the names of its
50 contributors may be used to endorse or promote products derived from
51 this software without specific prior written permission.
52
53 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
54 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
55 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
56 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
57 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
58 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
59 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
60 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
61 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
62 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
63 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
64 POSSIBILITY OF SUCH DAMAGE.]
65
66 ******************************************************************************/
67
68 #include "util.h"
69 #include "cuddInt.h"
70
71 #ifndef PBORI_FORCE_ORIGINAL_CUDD
72 #include <polybori/cudd/prefix_internal.h>
73 #endif
74
75 /*---------------------------------------------------------------------------*/
76 /* Constant declarations */
77 /*---------------------------------------------------------------------------*/
78
79
80 /*---------------------------------------------------------------------------*/
81 /* Stucture declarations */
82 /*---------------------------------------------------------------------------*/
83
84
85 /*---------------------------------------------------------------------------*/
86 /* Type declarations */
87 /*---------------------------------------------------------------------------*/
88
89
90 /*---------------------------------------------------------------------------*/
91 /* Variable declarations */
92 /*---------------------------------------------------------------------------*/
93
94 #ifndef lint
95 static char rcsid[] DD_UNUSED = "$Id: cuddRef.c,v 1.29 2012/02/05 01:07:19 fabio Exp $";
96 #endif
97
98 /*---------------------------------------------------------------------------*/
99 /* Macro declarations */
100 /*---------------------------------------------------------------------------*/
101
102
103 /**AutomaticStart*************************************************************/
104
105 /*---------------------------------------------------------------------------*/
106 /* Static function prototypes */
107 /*---------------------------------------------------------------------------*/
108
109 /**AutomaticEnd***************************************************************/
110
111
112 /*---------------------------------------------------------------------------*/
113 /* Definition of exported functions */
114 /*---------------------------------------------------------------------------*/
115
116 /**Function********************************************************************
117
118 Synopsis [Increases the reference count of a node, if it is not
119 saturated.]
120
121 Description []
122
123 SideEffects [None]
124
125 SeeAlso [Cudd_RecursiveDeref Cudd_Deref]
126
127 ******************************************************************************/
128 void
Cudd_Ref(DdNode * n)129 Cudd_Ref(
130 DdNode * n)
131 {
132
133 n = Cudd_Regular(n);
134
135 cuddSatInc(n->ref);
136
137 } /* end of Cudd_Ref */
138
139
140 /**Function********************************************************************
141
142 Synopsis [Decreases the reference count of node n.]
143
144 Description [Decreases the reference count of node n. If n dies,
145 recursively decreases the reference counts of its children. It is
146 used to dispose of a DD that is no longer needed.]
147
148 SideEffects [None]
149
150 SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]
151
152 ******************************************************************************/
153 void
Cudd_RecursiveDeref(DdManager * table,DdNode * n)154 Cudd_RecursiveDeref(
155 DdManager * table,
156 DdNode * n)
157 {
158 DdNode *N;
159 int ord;
160 DdNodePtr *stack = table->stack;
161 int SP = 1;
162
163 unsigned int live = table->keys - table->dead;
164 if (live > table->peakLiveNodes) {
165 table->peakLiveNodes = live;
166 }
167
168 N = Cudd_Regular(n);
169
170 do {
171 #ifdef DD_DEBUG
172 CUDD_ASSERT(N->ref != 0);
173 #endif
174
175 if (N->ref == 1) {
176 N->ref = 0;
177 table->dead++;
178 #ifdef DD_STATS
179 table->nodesDropped++;
180 #endif
181 if (cuddIsConstant(N)) {
182 table->constants.dead++;
183 N = stack[--SP];
184 } else {
185 ord = table->perm[N->index];
186 stack[SP++] = Cudd_Regular(cuddE(N));
187 table->subtables[ord].dead++;
188 N = cuddT(N);
189 }
190 } else {
191 cuddSatDec(N->ref);
192 N = stack[--SP];
193 }
194 } while (SP != 0);
195
196 } /* end of Cudd_RecursiveDeref */
197
198
199 /**Function********************************************************************
200
201 Synopsis [Decreases the reference count of BDD node n.]
202
203 Description [Decreases the reference count of node n. If n dies,
204 recursively decreases the reference counts of its children. It is
205 used to dispose of a BDD that is no longer needed. It is more
206 efficient than Cudd_RecursiveDeref, but it cannot be used on
207 ADDs. The greater efficiency comes from being able to assume that no
208 constant node will ever die as a result of a call to this
209 procedure.]
210
211 SideEffects [None]
212
213 SeeAlso [Cudd_RecursiveDeref Cudd_DelayedDerefBdd]
214
215 ******************************************************************************/
216 void
Cudd_IterDerefBdd(DdManager * table,DdNode * n)217 Cudd_IterDerefBdd(
218 DdManager * table,
219 DdNode * n)
220 {
221 DdNode *N;
222 int ord;
223 DdNodePtr *stack = table->stack;
224 int SP = 1;
225
226 unsigned int live = table->keys - table->dead;
227 if (live > table->peakLiveNodes) {
228 table->peakLiveNodes = live;
229 }
230
231 N = Cudd_Regular(n);
232
233 do {
234 #ifdef DD_DEBUG
235 CUDD_ASSERT(N->ref != 0);
236 #endif
237
238 if (N->ref == 1) {
239 N->ref = 0;
240 table->dead++;
241 #ifdef DD_STATS
242 table->nodesDropped++;
243 #endif
244 ord = table->perm[N->index];
245 stack[SP++] = Cudd_Regular(cuddE(N));
246 table->subtables[ord].dead++;
247 N = cuddT(N);
248 } else {
249 cuddSatDec(N->ref);
250 N = stack[--SP];
251 }
252 } while (SP != 0);
253
254 } /* end of Cudd_IterDerefBdd */
255
256
257 /**Function********************************************************************
258
259 Synopsis [Decreases the reference count of BDD node n.]
260
261 Description [Enqueues node n for later dereferencing. If the queue
262 is full decreases the reference count of the oldest node N to make
263 room for n. If N dies, recursively decreases the reference counts of
264 its children. It is used to dispose of a BDD that is currently not
265 needed, but may be useful again in the near future. The dereferencing
266 proper is done as in Cudd_IterDerefBdd.]
267
268 SideEffects [None]
269
270 SeeAlso [Cudd_RecursiveDeref Cudd_IterDerefBdd]
271
272 ******************************************************************************/
273 void
Cudd_DelayedDerefBdd(DdManager * table,DdNode * n)274 Cudd_DelayedDerefBdd(
275 DdManager * table,
276 DdNode * n)
277 {
278 DdNode *N;
279 int ord;
280 DdNodePtr *stack;
281 int SP;
282
283 unsigned int live = table->keys - table->dead;
284 if (live > table->peakLiveNodes) {
285 table->peakLiveNodes = live;
286 }
287
288 n = Cudd_Regular(n);
289 #ifdef DD_DEBUG
290 CUDD_ASSERT(n->ref != 0);
291 #endif
292
293 #ifdef DD_NO_DEATH_ROW
294 N = n;
295 #else
296 if (cuddIsConstant(n) || n->ref > 1) {
297 #ifdef DD_DEBUG
298 CUDD_ASSERT(n->ref != 1 && (!cuddIsConstant(n) || n == DD_ONE(table)));
299 #endif
300 cuddSatDec(n->ref);
301 return;
302 }
303
304 N = table->deathRow[table->nextDead];
305
306 if (N != NULL) {
307 #endif
308 #ifdef DD_DEBUG
309 CUDD_ASSERT(!Cudd_IsComplement(N));
310 #endif
311 stack = table->stack;
312 SP = 1;
313 do {
314 #ifdef DD_DEBUG
315 CUDD_ASSERT(N->ref != 0);
316 #endif
317 if (N->ref == 1) {
318 N->ref = 0;
319 table->dead++;
320 #ifdef DD_STATS
321 table->nodesDropped++;
322 #endif
323 ord = table->perm[N->index];
324 stack[SP++] = Cudd_Regular(cuddE(N));
325 table->subtables[ord].dead++;
326 N = cuddT(N);
327 } else {
328 cuddSatDec(N->ref);
329 N = stack[--SP];
330 }
331 } while (SP != 0);
332 #ifndef DD_NO_DEATH_ROW
333 }
334 table->deathRow[table->nextDead] = n;
335
336 /* Udate insertion point. */
337 table->nextDead++;
338 table->nextDead &= table->deadMask;
339 #if 0
340 if (table->nextDead == table->deathRowDepth) {
341 if (table->deathRowDepth < table->looseUpTo / 2) {
342 extern void (*MMoutOfMemory)(long);
343 void (*saveHandler)(long) = MMoutOfMemory;
344 DdNodePtr *newRow;
345 MMoutOfMemory = Cudd_OutOfMem;
346 newRow = REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
347 MMoutOfMemory = saveHandler;
348 if (newRow == NULL) {
349 table->nextDead = 0;
350 } else {
351 int i;
352 table->memused += table->deathRowDepth;
353 i = table->deathRowDepth;
354 table->deathRowDepth <<= 1;
355 for (; i < table->deathRowDepth; i++) {
356 newRow[i] = NULL;
357 }
358 table->deadMask = table->deathRowDepth - 1;
359 table->deathRow = newRow;
360 }
361 } else {
362 table->nextDead = 0;
363 }
364 }
365 #endif
366 #endif
367
368 } /* end of Cudd_DelayedDerefBdd */
369
370
371 /**Function********************************************************************
372
373 Synopsis [Decreases the reference count of ZDD node n.]
374
375 Description [Decreases the reference count of ZDD node n. If n dies,
376 recursively decreases the reference counts of its children. It is
377 used to dispose of a ZDD that is no longer needed.]
378
379 SideEffects [None]
380
381 SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDeref]
382
383 ******************************************************************************/
384 void
Cudd_RecursiveDerefZdd(DdManager * table,DdNode * n)385 Cudd_RecursiveDerefZdd(
386 DdManager * table,
387 DdNode * n)
388 {
389 DdNode *N;
390 int ord;
391 DdNodePtr *stack = table->stack;
392 int SP = 1;
393
394 N = n;
395
396 do {
397 #ifdef DD_DEBUG
398 CUDD_ASSERT(N->ref != 0);
399 #endif
400
401 cuddSatDec(N->ref);
402
403 if (N->ref == 0) {
404 table->deadZ++;
405 #ifdef DD_STATS
406 table->nodesDropped++;
407 #endif
408 #ifdef DD_DEBUG
409 CUDD_ASSERT(!cuddIsConstant(N));
410 #endif
411 ord = table->permZ[N->index];
412 stack[SP++] = cuddE(N);
413 table->subtableZ[ord].dead++;
414 N = cuddT(N);
415 } else {
416 N = stack[--SP];
417 }
418 } while (SP != 0);
419
420 } /* end of Cudd_RecursiveDerefZdd */
421
422
423 /**Function********************************************************************
424
425 Synopsis [Decreases the reference count of node.]
426
427 Description [Decreases the reference count of node. It is primarily
428 used in recursive procedures to decrease the ref count of a result
429 node before returning it. This accomplishes the goal of removing the
430 protection applied by a previous Cudd_Ref.]
431
432 SideEffects [None]
433
434 SeeAlso [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]
435
436 ******************************************************************************/
437 void
Cudd_Deref(DdNode * node)438 Cudd_Deref(
439 DdNode * node)
440 {
441 node = Cudd_Regular(node);
442 cuddSatDec(node->ref);
443
444 } /* end of Cudd_Deref */
445
446
447 /**Function********************************************************************
448
449 Synopsis [Checks the unique table for nodes with non-zero reference
450 counts.]
451
452 Description [Checks the unique table for nodes with non-zero
453 reference counts. It is normally called before Cudd_Quit to make sure
454 that there are no memory leaks due to missing Cudd_RecursiveDeref's.
455 Takes into account that reference counts may saturate and that the
456 basic constants and the projection functions are referenced by the
457 manager. Returns the number of nodes with non-zero reference count.
458 (Except for the cases mentioned above.)]
459
460 SideEffects [None]
461
462 SeeAlso []
463
464 ******************************************************************************/
465 int
Cudd_CheckZeroRef(DdManager * manager)466 Cudd_CheckZeroRef(
467 DdManager * manager)
468 {
469 int size;
470 int i, j;
471 int remain; /* the expected number of remaining references to one */
472 DdNodePtr *nodelist;
473 DdNode *node;
474 DdNode *sentinel = &(manager->sentinel);
475 DdSubtable *subtable;
476 int count = 0;
477 int index;
478
479 #ifndef DD_NO_DEATH_ROW
480 cuddClearDeathRow(manager);
481 #endif
482
483 /* First look at the BDD/ADD subtables. */
484 remain = 1; /* reference from the manager */
485 size = manager->size;
486 remain += 2 * size; /* reference from the BDD projection functions */
487
488 for (i = 0; i < size; i++) {
489 subtable = &(manager->subtables[i]);
490 nodelist = subtable->nodelist;
491 for (j = 0; (unsigned) j < subtable->slots; j++) {
492 node = nodelist[j];
493 while (node != sentinel) {
494 if (node->ref != 0 && node->ref != DD_MAXREF) {
495 index = (int) node->index;
496 if (node != manager->vars[index]) {
497 count++;
498 } else {
499 if (node->ref != 1) {
500 count++;
501 }
502 }
503 }
504 node = node->next;
505 }
506 }
507 }
508
509 /* Then look at the ZDD subtables. */
510 size = manager->sizeZ;
511 if (size) /* references from ZDD universe */
512 remain += 2;
513
514 for (i = 0; i < size; i++) {
515 subtable = &(manager->subtableZ[i]);
516 nodelist = subtable->nodelist;
517 for (j = 0; (unsigned) j < subtable->slots; j++) {
518 node = nodelist[j];
519 while (node != NULL) {
520 if (node->ref != 0 && node->ref != DD_MAXREF) {
521 index = (int) node->index;
522 if (node == manager->univ[manager->permZ[index]]) {
523 if (node->ref > 2) {
524 count++;
525 }
526 } else {
527 count++;
528 }
529 }
530 node = node->next;
531 }
532 }
533 }
534
535 /* Now examine the constant table. Plusinfinity, minusinfinity, and
536 ** zero are referenced by the manager. One is referenced by the
537 ** manager, by the ZDD universe, and by all projection functions.
538 ** All other nodes should have no references.
539 */
540 nodelist = manager->constants.nodelist;
541 for (j = 0; (unsigned) j < manager->constants.slots; j++) {
542 node = nodelist[j];
543 while (node != NULL) {
544 if (node->ref != 0 && node->ref != DD_MAXREF) {
545 if (node == manager->one) {
546 if ((int) node->ref != remain) {
547 count++;
548 }
549 } else if (node == manager->zero ||
550 node == manager->plusinfinity ||
551 node == manager->minusinfinity) {
552 if (node->ref != 1) {
553 count++;
554 }
555 } else {
556 count++;
557 }
558 }
559 node = node->next;
560 }
561 }
562 return(count);
563
564 } /* end of Cudd_CheckZeroRef */
565
566
567 /*---------------------------------------------------------------------------*/
568 /* Definition of internal functions */
569 /*---------------------------------------------------------------------------*/
570
571
572 /**Function********************************************************************
573
574 Synopsis [Brings children of a dead node back.]
575
576 Description []
577
578 SideEffects [None]
579
580 SeeAlso [cuddReclaimZdd]
581
582 ******************************************************************************/
583 void
cuddReclaim(DdManager * table,DdNode * n)584 cuddReclaim(
585 DdManager * table,
586 DdNode * n)
587 {
588 DdNode *N;
589 int ord;
590 DdNodePtr *stack = table->stack;
591 int SP = 1;
592 double initialDead = table->dead;
593
594 N = Cudd_Regular(n);
595
596 #ifdef DD_DEBUG
597 CUDD_ASSERT(N->ref == 0);
598 #endif
599
600 do {
601 if (N->ref == 0) {
602 N->ref = 1;
603 table->dead--;
604 if (cuddIsConstant(N)) {
605 table->constants.dead--;
606 N = stack[--SP];
607 } else {
608 ord = table->perm[N->index];
609 stack[SP++] = Cudd_Regular(cuddE(N));
610 table->subtables[ord].dead--;
611 N = cuddT(N);
612 }
613 } else {
614 cuddSatInc(N->ref);
615 N = stack[--SP];
616 }
617 } while (SP != 0);
618
619 N = Cudd_Regular(n);
620 cuddSatDec(N->ref);
621 table->reclaimed += initialDead - table->dead;
622
623 } /* end of cuddReclaim */
624
625
626 /**Function********************************************************************
627
628 Synopsis [Brings children of a dead ZDD node back.]
629
630 Description []
631
632 SideEffects [None]
633
634 SeeAlso [cuddReclaim]
635
636 ******************************************************************************/
637 void
cuddReclaimZdd(DdManager * table,DdNode * n)638 cuddReclaimZdd(
639 DdManager * table,
640 DdNode * n)
641 {
642 DdNode *N;
643 int ord;
644 DdNodePtr *stack = table->stack;
645 int SP = 1;
646
647 N = n;
648
649 #ifdef DD_DEBUG
650 CUDD_ASSERT(N->ref == 0);
651 #endif
652
653 do {
654 cuddSatInc(N->ref);
655
656 if (N->ref == 1) {
657 table->deadZ--;
658 table->reclaimed++;
659 #ifdef DD_DEBUG
660 CUDD_ASSERT(!cuddIsConstant(N));
661 #endif
662 ord = table->permZ[N->index];
663 stack[SP++] = cuddE(N);
664 table->subtableZ[ord].dead--;
665 N = cuddT(N);
666 } else {
667 N = stack[--SP];
668 }
669 } while (SP != 0);
670
671 cuddSatDec(n->ref);
672
673 } /* end of cuddReclaimZdd */
674
675
676 /**Function********************************************************************
677
678 Synopsis [Shrinks the death row.]
679
680 Description [Shrinks the death row by a factor of four.]
681
682 SideEffects [None]
683
684 SeeAlso [cuddClearDeathRow]
685
686 ******************************************************************************/
687 void
cuddShrinkDeathRow(DdManager * table)688 cuddShrinkDeathRow(
689 DdManager *table)
690 {
691 #ifndef DD_NO_DEATH_ROW
692 int i;
693
694 if (table->deathRowDepth > 3) {
695 for (i = table->deathRowDepth/4; i < table->deathRowDepth; i++) {
696 if (table->deathRow[i] == NULL) break;
697 Cudd_IterDerefBdd(table,table->deathRow[i]);
698 table->deathRow[i] = NULL;
699 }
700 table->deathRowDepth /= 4;
701 table->deadMask = table->deathRowDepth - 1;
702 if ((unsigned) table->nextDead > table->deadMask) {
703 table->nextDead = 0;
704 }
705 table->deathRow = REALLOC(DdNodePtr, table->deathRow,
706 table->deathRowDepth);
707 }
708 #endif
709
710 } /* end of cuddShrinkDeathRow */
711
712
713 /**Function********************************************************************
714
715 Synopsis [Clears the death row.]
716
717 Description []
718
719 SideEffects [None]
720
721 SeeAlso [Cudd_DelayedDerefBdd Cudd_IterDerefBdd Cudd_CheckZeroRef
722 cuddGarbageCollect]
723
724 ******************************************************************************/
725 void
cuddClearDeathRow(DdManager * table)726 cuddClearDeathRow(
727 DdManager *table)
728 {
729 #ifndef DD_NO_DEATH_ROW
730 int i;
731
732 for (i = 0; i < table->deathRowDepth; i++) {
733 if (table->deathRow[i] == NULL) break;
734 Cudd_IterDerefBdd(table,table->deathRow[i]);
735 table->deathRow[i] = NULL;
736 }
737 #ifdef DD_DEBUG
738 for (; i < table->deathRowDepth; i++) {
739 CUDD_ASSERT(table->deathRow[i] == NULL);
740 }
741 #endif
742 table->nextDead = 0;
743 #endif
744
745 } /* end of cuddClearDeathRow */
746
747
748 /**Function********************************************************************
749
750 Synopsis [Checks whether a node is in the death row.]
751
752 Description [Checks whether a node is in the death row. Returns the
753 position of the first occurrence if the node is present; -1
754 otherwise.]
755
756 SideEffects [None]
757
758 SeeAlso [Cudd_DelayedDerefBdd cuddClearDeathRow]
759
760 ******************************************************************************/
761 int
cuddIsInDeathRow(DdManager * dd,DdNode * f)762 cuddIsInDeathRow(
763 DdManager *dd,
764 DdNode *f)
765 {
766 #ifndef DD_NO_DEATH_ROW
767 int i;
768
769 for (i = 0; i < dd->deathRowDepth; i++) {
770 if (f == dd->deathRow[i]) {
771 return(i);
772 }
773 }
774 #endif
775
776 return(-1);
777
778 } /* end of cuddIsInDeathRow */
779
780
781 /**Function********************************************************************
782
783 Synopsis [Counts how many times a node is in the death row.]
784
785 Description []
786
787 SideEffects [None]
788
789 SeeAlso [Cudd_DelayedDerefBdd cuddClearDeathRow cuddIsInDeathRow]
790
791 ******************************************************************************/
792 int
cuddTimesInDeathRow(DdManager * dd,DdNode * f)793 cuddTimesInDeathRow(
794 DdManager *dd,
795 DdNode *f)
796 {
797 int count = 0;
798 #ifndef DD_NO_DEATH_ROW
799 int i;
800
801 for (i = 0; i < dd->deathRowDepth; i++) {
802 count += f == dd->deathRow[i];
803 }
804 #endif
805
806 return(count);
807
808 } /* end of cuddTimesInDeathRow */
809
810 /*---------------------------------------------------------------------------*/
811 /* Definition of static functions */
812 /*---------------------------------------------------------------------------*/
813