1 /**CFile***********************************************************************
7 Synopsis [Functions that manipulate the reference counts.]
9 Description [External procedures included in this module:
12 <li> Cudd_RecursiveDeref()
13 <li> Cudd_IterDerefBdd()
14 <li> Cudd_DelayedDerefBdd()
15 <li> Cudd_RecursiveDerefZdd()
17 <li> Cudd_CheckZeroRef()
19 Internal procedures included in this module:
23 <li> cuddClearDeathRow()
24 <li> cuddShrinkDeathRow()
25 <li> cuddIsInDeathRow()
26 <li> cuddTimesInDeathRow()
32 Author [Fabio Somenzi]
34 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
38 Redistribution and use in source and binary forms, with or without
39 modification, are permitted provided that the following conditions
42 Redistributions of source code must retain the above copyright
43 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
66 ******************************************************************************/
71 /*---------------------------------------------------------------------------*/
72 /* Constant declarations */
73 /*---------------------------------------------------------------------------*/
76 /*---------------------------------------------------------------------------*/
77 /* Stucture declarations */
78 /*---------------------------------------------------------------------------*/
81 /*---------------------------------------------------------------------------*/
82 /* Type declarations */
83 /*---------------------------------------------------------------------------*/
86 /*---------------------------------------------------------------------------*/
87 /* Variable declarations */
88 /*---------------------------------------------------------------------------*/
91 static char rcsid
[] DD_UNUSED
= "$Id: cuddRef.c,v 1.28 2004/08/13 18:04:50 fabio Exp $";
94 /*---------------------------------------------------------------------------*/
95 /* Macro declarations */
96 /*---------------------------------------------------------------------------*/
99 /**AutomaticStart*************************************************************/
101 /*---------------------------------------------------------------------------*/
102 /* Static function prototypes */
103 /*---------------------------------------------------------------------------*/
105 /**AutomaticEnd***************************************************************/
108 /*---------------------------------------------------------------------------*/
109 /* Definition of exported functions */
110 /*---------------------------------------------------------------------------*/
112 /**Function********************************************************************
114 Synopsis [Increases the reference count of a node, if it is not
121 SeeAlso [Cudd_RecursiveDeref Cudd_Deref]
123 ******************************************************************************/
133 } /* end of Cudd_Ref */
136 /**Function********************************************************************
138 Synopsis [Decreases the reference count of node n.]
140 Description [Decreases the reference count of node n. If n dies,
141 recursively decreases the reference counts of its children. It is
142 used to dispose of a DD that is no longer needed.]
146 SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]
148 ******************************************************************************/
156 DdNodePtr
*stack
= table
->stack
;
159 unsigned int live
= table
->keys
- table
->dead
;
160 if (live
> table
->peakLiveNodes
) {
161 table
->peakLiveNodes
= live
;
175 table
->nodesDropped
++;
177 if (cuddIsConstant(N
)) {
178 table
->constants
.dead
++;
181 ord
= table
->perm
[N
->index
];
182 stack
[SP
++] = Cudd_Regular(cuddE(N
));
183 table
->subtables
[ord
].dead
++;
192 } /* end of Cudd_RecursiveDeref */
195 /**Function********************************************************************
197 Synopsis [Decreases the reference count of BDD node n.]
199 Description [Decreases the reference count of node n. If n dies,
200 recursively decreases the reference counts of its children. It is
201 used to dispose of a BDD that is no longer needed. It is more
202 efficient than Cudd_RecursiveDeref, but it cannot be used on
203 ADDs. The greater efficiency comes from being able to assume that no
204 constant node will ever die as a result of a call to this
209 SeeAlso [Cudd_RecursiveDeref Cudd_DelayedDerefBdd]
211 ******************************************************************************/
219 DdNodePtr
*stack
= table
->stack
;
222 unsigned int live
= table
->keys
- table
->dead
;
223 if (live
> table
->peakLiveNodes
) {
224 table
->peakLiveNodes
= live
;
238 table
->nodesDropped
++;
240 ord
= table
->perm
[N
->index
];
241 stack
[SP
++] = Cudd_Regular(cuddE(N
));
242 table
->subtables
[ord
].dead
++;
250 } /* end of Cudd_IterDerefBdd */
253 /**Function********************************************************************
255 Synopsis [Decreases the reference count of BDD node n.]
257 Description [Enqueues node n for later dereferencing. If the queue
258 is full decreases the reference count of the oldest node N to make
259 room for n. If N dies, recursively decreases the reference counts of
260 its children. It is used to dispose of a BDD that is currently not
261 needed, but may be useful again in the near future. The dereferencing
262 proper is done as in Cudd_IterDerefBdd.]
266 SeeAlso [Cudd_RecursiveDeref Cudd_IterDerefBdd]
268 ******************************************************************************/
270 Cudd_DelayedDerefBdd(
279 unsigned int live
= table
->keys
- table
->dead
;
280 if (live
> table
->peakLiveNodes
) {
281 table
->peakLiveNodes
= live
;
289 #ifdef DD_NO_DEATH_ROW
292 if (cuddIsConstant(n
) || n
->ref
> 1) {
294 assert(n
->ref
!= 1 && (!cuddIsConstant(n
) || n
== DD_ONE(table
)));
300 N
= table
->deathRow
[table
->nextDead
];
305 assert(!Cudd_IsComplement(N
));
307 stack
= table
->stack
;
317 table
->nodesDropped
++;
319 ord
= table
->perm
[N
->index
];
320 stack
[SP
++] = Cudd_Regular(cuddE(N
));
321 table
->subtables
[ord
].dead
++;
328 #ifndef DD_NO_DEATH_ROW
330 table
->deathRow
[table
->nextDead
] = n
;
332 /* Udate insertion point. */
334 table
->nextDead
&= table
->deadMask
;
336 if (table
->nextDead
== table
->deathRowDepth
) {
337 if (table
->deathRowDepth
< table
->looseUpTo
/ 2) {
338 extern void (*MMoutOfMemory
)(long);
339 void (*saveHandler
)(long) = MMoutOfMemory
;
341 MMoutOfMemory
= Cudd_OutOfMem
;
342 newRow
= REALLOC(DdNodePtr
,table
->deathRow
,2*table
->deathRowDepth
);
343 MMoutOfMemory
= saveHandler
;
344 if (newRow
== NULL
) {
348 table
->memused
+= table
->deathRowDepth
;
349 i
= table
->deathRowDepth
;
350 table
->deathRowDepth
<<= 1;
351 for (; i
< table
->deathRowDepth
; i
++) {
354 table
->deadMask
= table
->deathRowDepth
- 1;
355 table
->deathRow
= newRow
;
364 } /* end of Cudd_DelayedDerefBdd */
367 /**Function********************************************************************
369 Synopsis [Decreases the reference count of ZDD node n.]
371 Description [Decreases the reference count of ZDD node n. If n dies,
372 recursively decreases the reference counts of its children. It is
373 used to dispose of a ZDD that is no longer needed.]
377 SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDeref]
379 ******************************************************************************/
381 Cudd_RecursiveDerefZdd(
387 DdNodePtr
*stack
= table
->stack
;
402 table
->nodesDropped
++;
405 assert(!cuddIsConstant(N
));
407 ord
= table
->permZ
[N
->index
];
408 stack
[SP
++] = cuddE(N
);
409 table
->subtableZ
[ord
].dead
++;
416 } /* end of Cudd_RecursiveDerefZdd */
419 /**Function********************************************************************
421 Synopsis [Decreases the reference count of node.]
423 Description [Decreases the reference count of node. It is primarily
424 used in recursive procedures to decrease the ref count of a result
425 node before returning it. This accomplishes the goal of removing the
426 protection applied by a previous Cudd_Ref.]
430 SeeAlso [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]
432 ******************************************************************************/
437 node
= Cudd_Regular(node
);
438 cuddSatDec(node
->ref
);
440 } /* end of Cudd_Deref */
443 /**Function********************************************************************
445 Synopsis [Checks the unique table for nodes with non-zero reference
448 Description [Checks the unique table for nodes with non-zero
449 reference counts. It is normally called before Cudd_Quit to make sure
450 that there are no memory leaks due to missing Cudd_RecursiveDeref's.
451 Takes into account that reference counts may saturate and that the
452 basic constants and the projection functions are referenced by the
453 manager. Returns the number of nodes with non-zero reference count.
454 (Except for the cases mentioned above.)]
460 ******************************************************************************/
467 int remain
; /* the expected number of remaining references to one */
470 DdNode
*sentinel
= &(manager
->sentinel
);
471 DdSubtable
*subtable
;
475 #ifndef DD_NO_DEATH_ROW
476 cuddClearDeathRow(manager
);
479 /* First look at the BDD/ADD subtables. */
480 remain
= 1; /* reference from the manager */
481 size
= manager
->size
;
482 remain
+= 2 * size
; /* reference from the BDD projection functions */
484 for (i
= 0; i
< size
; i
++) {
485 subtable
= &(manager
->subtables
[i
]);
486 nodelist
= subtable
->nodelist
;
487 for (j
= 0; (unsigned) j
< subtable
->slots
; j
++) {
489 while (node
!= sentinel
) {
490 if (node
->ref
!= 0 && node
->ref
!= DD_MAXREF
) {
491 index
= (int) node
->index
;
492 if (node
!= manager
->vars
[index
]) {
495 if (node
->ref
!= 1) {
505 /* Then look at the ZDD subtables. */
506 size
= manager
->sizeZ
;
507 if (size
) /* references from ZDD universe */
510 for (i
= 0; i
< size
; i
++) {
511 subtable
= &(manager
->subtableZ
[i
]);
512 nodelist
= subtable
->nodelist
;
513 for (j
= 0; (unsigned) j
< subtable
->slots
; j
++) {
515 while (node
!= NULL
) {
516 if (node
->ref
!= 0 && node
->ref
!= DD_MAXREF
) {
517 index
= (int) node
->index
;
518 if (node
== manager
->univ
[manager
->permZ
[index
]]) {
531 /* Now examine the constant table. Plusinfinity, minusinfinity, and
532 ** zero are referenced by the manager. One is referenced by the
533 ** manager, by the ZDD universe, and by all projection functions.
534 ** All other nodes should have no references.
536 nodelist
= manager
->constants
.nodelist
;
537 for (j
= 0; (unsigned) j
< manager
->constants
.slots
; j
++) {
539 while (node
!= NULL
) {
540 if (node
->ref
!= 0 && node
->ref
!= DD_MAXREF
) {
541 if (node
== manager
->one
) {
542 if ((int) node
->ref
!= remain
) {
545 } else if (node
== manager
->zero
||
546 node
== manager
->plusinfinity
||
547 node
== manager
->minusinfinity
) {
548 if (node
->ref
!= 1) {
560 } /* end of Cudd_CheckZeroRef */
563 /*---------------------------------------------------------------------------*/
564 /* Definition of internal functions */
565 /*---------------------------------------------------------------------------*/
568 /**Function********************************************************************
570 Synopsis [Brings children of a dead node back.]
576 SeeAlso [cuddReclaimZdd]
578 ******************************************************************************/
586 DdNodePtr
*stack
= table
->stack
;
588 double initialDead
= table
->dead
;
600 if (cuddIsConstant(N
)) {
601 table
->constants
.dead
--;
604 ord
= table
->perm
[N
->index
];
605 stack
[SP
++] = Cudd_Regular(cuddE(N
));
606 table
->subtables
[ord
].dead
--;
617 table
->reclaimed
+= initialDead
- table
->dead
;
619 } /* end of cuddReclaim */
622 /**Function********************************************************************
624 Synopsis [Brings children of a dead ZDD node back.]
630 SeeAlso [cuddReclaim]
632 ******************************************************************************/
640 DdNodePtr
*stack
= table
->stack
;
656 assert(!cuddIsConstant(N
));
658 ord
= table
->permZ
[N
->index
];
659 stack
[SP
++] = cuddE(N
);
660 table
->subtableZ
[ord
].dead
--;
669 } /* end of cuddReclaimZdd */
672 /**Function********************************************************************
674 Synopsis [Shrinks the death row.]
676 Description [Shrinks the death row by a factor of four.]
680 SeeAlso [cuddClearDeathRow]
682 ******************************************************************************/
687 #ifndef DD_NO_DEATH_ROW
690 if (table
->deathRowDepth
> 3) {
691 for (i
= table
->deathRowDepth
/4; i
< table
->deathRowDepth
; i
++) {
692 if (table
->deathRow
[i
] == NULL
) break;
693 Cudd_IterDerefBdd(table
,table
->deathRow
[i
]);
694 table
->deathRow
[i
] = NULL
;
696 table
->deathRowDepth
/= 4;
697 table
->deadMask
= table
->deathRowDepth
- 1;
698 if ((unsigned) table
->nextDead
> table
->deadMask
) {
701 table
->deathRow
= REALLOC(DdNodePtr
, table
->deathRow
,
702 table
->deathRowDepth
);
706 } /* end of cuddShrinkDeathRow */
709 /**Function********************************************************************
711 Synopsis [Clears the death row.]
717 SeeAlso [Cudd_DelayedDerefBdd Cudd_IterDerefBdd Cudd_CheckZeroRef
720 ******************************************************************************/
725 #ifndef DD_NO_DEATH_ROW
728 for (i
= 0; i
< table
->deathRowDepth
; i
++) {
729 if (table
->deathRow
[i
] == NULL
) break;
730 Cudd_IterDerefBdd(table
,table
->deathRow
[i
]);
731 table
->deathRow
[i
] = NULL
;
734 for (; i
< table
->deathRowDepth
; i
++) {
735 assert(table
->deathRow
[i
] == NULL
);
741 } /* end of cuddClearDeathRow */
744 /**Function********************************************************************
746 Synopsis [Checks whether a node is in the death row.]
748 Description [Checks whether a node is in the death row. Returns the
749 position of the first occurrence if the node is present; -1
754 SeeAlso [Cudd_DelayedDerefBdd cuddClearDeathRow]
756 ******************************************************************************/
762 #ifndef DD_NO_DEATH_ROW
765 for (i
= 0; i
< dd
->deathRowDepth
; i
++) {
766 if (f
== dd
->deathRow
[i
]) {
774 } /* end of cuddIsInDeathRow */
777 /**Function********************************************************************
779 Synopsis [Counts how many times a node is in the death row.]
785 SeeAlso [Cudd_DelayedDerefBdd cuddClearDeathRow cuddIsInDeathRow]
787 ******************************************************************************/
794 #ifndef DD_NO_DEATH_ROW
797 for (i
= 0; i
< dd
->deathRowDepth
; i
++) {
798 count
+= f
== dd
->deathRow
[i
];
804 } /* end of cuddTimesInDeathRow */
806 /*---------------------------------------------------------------------------*/
807 /* Definition of static functions */
808 /*---------------------------------------------------------------------------*/