1 /**CFile***********************************************************************
7 Synopsis [Functions to check consistency of data structures.]
9 Description [External procedures included in this module:
11 <li> Cudd_DebugCheck()
14 Internal procedures included in this module:
16 <li> cuddHeapProfile()
18 <li> cuddPrintVarGroups()
20 Static procedures included in this module:
22 <li> debugFindParent()
28 Author [Fabio Somenzi]
30 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
34 Redistribution and use in source and binary forms, with or without
35 modification, are permitted provided that the following conditions
38 Redistributions of source code must retain the above copyright
39 notice, this list of conditions and the following disclaimer.
41 Redistributions in binary form must reproduce the above copyright
42 notice, this list of conditions and the following disclaimer in the
43 documentation and/or other materials provided with the distribution.
45 Neither the name of the University of Colorado nor the names of its
46 contributors may be used to endorse or promote products derived from
47 this software without specific prior written permission.
49 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60 POSSIBILITY OF SUCH DAMAGE.]
62 ******************************************************************************/
67 /*---------------------------------------------------------------------------*/
68 /* Constant declarations */
69 /*---------------------------------------------------------------------------*/
72 /*---------------------------------------------------------------------------*/
73 /* Stucture declarations */
74 /*---------------------------------------------------------------------------*/
77 /*---------------------------------------------------------------------------*/
78 /* Type declarations */
79 /*---------------------------------------------------------------------------*/
82 /*---------------------------------------------------------------------------*/
83 /* Variable declarations */
84 /*---------------------------------------------------------------------------*/
87 static char rcsid
[] DD_UNUSED
= "$Id: cuddCheck.c,v 1.35 2009/03/08 02:49:01 fabio Exp $";
90 /*---------------------------------------------------------------------------*/
91 /* Macro declarations */
92 /*---------------------------------------------------------------------------*/
95 /**AutomaticStart*************************************************************/
97 /*---------------------------------------------------------------------------*/
98 /* Static function prototypes */
99 /*---------------------------------------------------------------------------*/
101 static void debugFindParent (DdManager
*table
, DdNode
*node
);
103 static void debugCheckParent (DdManager
*table
, DdNode
*node
);
106 /**AutomaticEnd***************************************************************/
109 /*---------------------------------------------------------------------------*/
110 /* Definition of exported functions */
111 /*---------------------------------------------------------------------------*/
114 /**Function********************************************************************
116 Synopsis [Checks for inconsistencies in the DD heap.]
118 Description [Checks for inconsistencies in the DD heap:
120 <li> node has illegal index
121 <li> live node has dead children
122 <li> node has illegal Then or Else pointers
123 <li> BDD/ADD node has identical children
124 <li> ZDD node has zero then child
125 <li> wrong number of total nodes
126 <li> wrong number of dead nodes
127 <li> ref count error at node
129 Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is
130 not enough memory; 1 otherwise.]
134 SeeAlso [Cudd_CheckKeys]
136 ******************************************************************************/
146 DdNode
*sentinel
= &(table
->sentinel
);
147 st_table
*edgeTable
; /* stores internal ref count for each node */
155 edgeTable
= st_init_table(st_ptrcmp
,st_ptrhash
);
156 if (edgeTable
== NULL
) return(CUDD_OUT_OF_MEM
);
158 /* Check the BDD/ADD subtables. */
159 for (i
= 0; i
< (unsigned) table
->size
; i
++) {
160 index
= table
->invperm
[i
];
161 if (i
!= (unsigned) table
->perm
[index
]) {
162 (void) fprintf(table
->err
,
163 "Permutation corrupted: invperm[%u] = %d\t perm[%d] = %d\n",
164 i
, index
, index
, table
->perm
[index
]);
166 nodelist
= table
->subtables
[i
].nodelist
;
167 slots
= table
->subtables
[i
].slots
;
171 for (j
= 0; j
< slots
; j
++) { /* for each subtable slot */
173 while (f
!= sentinel
) {
175 if (cuddT(f
) != NULL
&& cuddE(f
) != NULL
&& f
->ref
!= 0) {
176 if ((int) f
->index
!= index
) {
177 (void) fprintf(table
->err
,
178 "Error: node has illegal index\n");
179 cuddPrintNode(f
,table
->err
);
182 if ((unsigned) cuddI(table
,cuddT(f
)->index
) <= i
||
183 (unsigned) cuddI(table
,Cudd_Regular(cuddE(f
))->index
)
185 (void) fprintf(table
->err
,
186 "Error: node has illegal children\n");
187 cuddPrintNode(f
,table
->err
);
190 if (Cudd_Regular(cuddT(f
)) != cuddT(f
)) {
191 (void) fprintf(table
->err
,
192 "Error: node has illegal form\n");
193 cuddPrintNode(f
,table
->err
);
196 if (cuddT(f
) == cuddE(f
)) {
197 (void) fprintf(table
->err
,
198 "Error: node has identical children\n");
199 cuddPrintNode(f
,table
->err
);
202 if (cuddT(f
)->ref
== 0 || Cudd_Regular(cuddE(f
))->ref
== 0) {
203 (void) fprintf(table
->err
,
204 "Error: live node has dead children\n");
205 cuddPrintNode(f
,table
->err
);
208 /* Increment the internal reference count for the
209 ** then child of the current node.
211 if (st_lookup_int(edgeTable
,(char *)cuddT(f
),&count
)) {
216 if (st_insert(edgeTable
,(char *)cuddT(f
),
217 (char *)(long)count
) == ST_OUT_OF_MEM
) {
218 st_free_table(edgeTable
);
219 return(CUDD_OUT_OF_MEM
);
222 /* Increment the internal reference count for the
223 ** else child of the current node.
225 if (st_lookup_int(edgeTable
,(char *)Cudd_Regular(cuddE(f
)),
231 if (st_insert(edgeTable
,(char *)Cudd_Regular(cuddE(f
)),
232 (char *)(long)count
) == ST_OUT_OF_MEM
) {
233 st_free_table(edgeTable
);
234 return(CUDD_OUT_OF_MEM
);
236 } else if (cuddT(f
) != NULL
&& cuddE(f
) != NULL
&& f
->ref
== 0) {
239 debugCheckParent(table
,f
);
243 "Error: node has illegal Then or Else pointers\n");
244 cuddPrintNode(f
,table
->err
);
249 } /* for each element of the collision list */
250 } /* for each subtable slot */
252 if ((unsigned) totalNode
!= table
->subtables
[i
].keys
) {
253 fprintf(table
->err
,"Error: wrong number of total nodes\n");
256 if ((unsigned) deadNode
!= table
->subtables
[i
].dead
) {
257 fprintf(table
->err
,"Error: wrong number of dead nodes\n");
260 } /* for each BDD/ADD subtable */
262 /* Check the ZDD subtables. */
263 for (i
= 0; i
< (unsigned) table
->sizeZ
; i
++) {
264 index
= table
->invpermZ
[i
];
265 if (i
!= (unsigned) table
->permZ
[index
]) {
266 (void) fprintf(table
->err
,
267 "Permutation corrupted: invpermZ[%u] = %d\t permZ[%d] = %d in ZDD\n",
268 i
, index
, index
, table
->permZ
[index
]);
270 nodelist
= table
->subtableZ
[i
].nodelist
;
271 slots
= table
->subtableZ
[i
].slots
;
275 for (j
= 0; j
< slots
; j
++) { /* for each subtable slot */
279 if (cuddT(f
) != NULL
&& cuddE(f
) != NULL
&& f
->ref
!= 0) {
280 if ((int) f
->index
!= index
) {
281 (void) fprintf(table
->err
,
282 "Error: ZDD node has illegal index\n");
283 cuddPrintNode(f
,table
->err
);
286 if (Cudd_IsComplement(cuddT(f
)) ||
287 Cudd_IsComplement(cuddE(f
))) {
288 (void) fprintf(table
->err
,
289 "Error: ZDD node has complemented children\n");
290 cuddPrintNode(f
,table
->err
);
293 if ((unsigned) cuddIZ(table
,cuddT(f
)->index
) <= i
||
294 (unsigned) cuddIZ(table
,cuddE(f
)->index
) <= i
) {
295 (void) fprintf(table
->err
,
296 "Error: ZDD node has illegal children\n");
297 cuddPrintNode(f
,table
->err
);
298 cuddPrintNode(cuddT(f
),table
->err
);
299 cuddPrintNode(cuddE(f
),table
->err
);
302 if (cuddT(f
) == DD_ZERO(table
)) {
303 (void) fprintf(table
->err
,
304 "Error: ZDD node has zero then child\n");
305 cuddPrintNode(f
,table
->err
);
308 if (cuddT(f
)->ref
== 0 || cuddE(f
)->ref
== 0) {
309 (void) fprintf(table
->err
,
310 "Error: ZDD live node has dead children\n");
311 cuddPrintNode(f
,table
->err
);
314 /* Increment the internal reference count for the
315 ** then child of the current node.
317 if (st_lookup_int(edgeTable
,(char *)cuddT(f
),&count
)) {
322 if (st_insert(edgeTable
,(char *)cuddT(f
),
323 (char *)(long)count
) == ST_OUT_OF_MEM
) {
324 st_free_table(edgeTable
);
325 return(CUDD_OUT_OF_MEM
);
328 /* Increment the internal reference count for the
329 ** else child of the current node.
331 if (st_lookup_int(edgeTable
,(char *)cuddE(f
),&count
)) {
336 if (st_insert(edgeTable
,(char *)cuddE(f
),
337 (char *)(long)count
) == ST_OUT_OF_MEM
) {
338 st_free_table(edgeTable
);
339 table
->errorCode
= CUDD_MEMORY_OUT
;
340 return(CUDD_OUT_OF_MEM
);
342 } else if (cuddT(f
) != NULL
&& cuddE(f
) != NULL
&& f
->ref
== 0) {
345 debugCheckParent(table
,f
);
349 "Error: ZDD node has illegal Then or Else pointers\n");
350 cuddPrintNode(f
,table
->err
);
355 } /* for each element of the collision list */
356 } /* for each subtable slot */
358 if ((unsigned) totalNode
!= table
->subtableZ
[i
].keys
) {
360 "Error: wrong number of total nodes in ZDD\n");
363 if ((unsigned) deadNode
!= table
->subtableZ
[i
].dead
) {
365 "Error: wrong number of dead nodes in ZDD\n");
368 } /* for each ZDD subtable */
370 /* Check the constant table. */
371 nodelist
= table
->constants
.nodelist
;
372 slots
= table
->constants
.slots
;
376 for (j
= 0; j
< slots
; j
++) {
381 if (f
->index
!= CUDD_CONST_INDEX
) {
382 fprintf(table
->err
,"Error: node has illegal index\n");
383 #if SIZEOF_VOID_P == 8
385 " node 0x%lx, id = %u, ref = %u, value = %g\n",
386 (ptruint
)f
,f
->index
,f
->ref
,cuddV(f
));
389 " node 0x%x, id = %hu, ref = %hu, value = %g\n",
390 (ptruint
)f
,f
->index
,f
->ref
,cuddV(f
));
400 if ((unsigned) totalNode
!= table
->constants
.keys
) {
401 (void) fprintf(table
->err
,
402 "Error: wrong number of total nodes in constants\n");
405 if ((unsigned) deadNode
!= table
->constants
.dead
) {
406 (void) fprintf(table
->err
,
407 "Error: wrong number of dead nodes in constants\n");
410 gen
= st_init_gen(edgeTable
);
411 while (st_gen(gen
, &f
, &count
)) {
412 if (count
> (int)(f
->ref
) && f
->ref
!= DD_MAXREF
) {
413 #if SIZEOF_VOID_P == 8
414 fprintf(table
->err
,"ref count error at node 0x%lx, count = %d, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",(ptruint
)f
,count
,f
->index
,f
->ref
,(ptruint
)cuddT(f
),(ptruint
)cuddE(f
));
416 fprintf(table
->err
,"ref count error at node 0x%x, count = %d, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",(ptruint
)f
,count
,f
->index
,f
->ref
,(ptruint
)cuddT(f
),(ptruint
)cuddE(f
));
418 debugFindParent(table
,f
);
423 st_free_table(edgeTable
);
427 } /* end of Cudd_DebugCheck */
430 /**Function********************************************************************
432 Synopsis [Checks for several conditions that should not occur.]
434 Description [Checks for the following conditions:
436 <li>Wrong sizes of subtables.
437 <li>Wrong number of keys found in unique subtable.
438 <li>Wrong number of dead found in unique subtable.
439 <li>Wrong number of keys found in the constant table
440 <li>Wrong number of dead found in the constant table
441 <li>Wrong number of total slots found
442 <li>Wrong number of maximum keys found
443 <li>Wrong number of total dead found
445 Reports the average length of non-empty lists. Returns the number of
446 subtables for which the number of keys is wrong.]
450 SeeAlso [Cudd_DebugCheck]
452 ******************************************************************************/
461 DdNode
*sentinel
= &(table
->sentinel
);
462 DdSubtable
*subtable
;
476 for (i
= 0; i
< size
; i
++) {
477 subtable
= &(table
->subtables
[i
]);
478 nodelist
= subtable
->nodelist
;
479 keys
= subtable
->keys
;
480 dead
= subtable
->dead
;
482 slots
= subtable
->slots
;
483 shift
= subtable
->shift
;
484 logSlots
= sizeof(int) * 8 - shift
;
485 if (((slots
>> logSlots
) << logSlots
) != slots
) {
486 (void) fprintf(table
->err
,
487 "Unique table %d is not the right power of 2\n", i
);
488 (void) fprintf(table
->err
,
489 " slots = %u shift = %d\n", slots
, shift
);
493 for (j
= 0; (unsigned) j
< slots
; j
++) {
495 if (node
!= sentinel
) {
498 while (node
!= sentinel
) {
500 if (node
->ref
== 0) {
507 (void) fprintf(table
->err
, "Wrong number of keys found \
508 in unique table %d (difference=%d)\n", i
, keys
);
512 (void) fprintf(table
->err
, "Wrong number of dead found \
513 in unique table no. %d (difference=%d)\n", i
, dead
);
515 } /* for each BDD/ADD subtable */
517 /* Check the ZDD subtables. */
520 for (i
= 0; i
< size
; i
++) {
521 subtable
= &(table
->subtableZ
[i
]);
522 nodelist
= subtable
->nodelist
;
523 keys
= subtable
->keys
;
524 dead
= subtable
->dead
;
526 totalSlots
+= subtable
->slots
;
528 for (j
= 0; (unsigned) j
< subtable
->slots
; j
++) {
533 while (node
!= NULL
) {
535 if (node
->ref
== 0) {
542 (void) fprintf(table
->err
, "Wrong number of keys found \
543 in ZDD unique table no. %d (difference=%d)\n", i
, keys
);
547 (void) fprintf(table
->err
, "Wrong number of dead found \
548 in ZDD unique table no. %d (difference=%d)\n", i
, dead
);
550 } /* for each ZDD subtable */
552 /* Check the constant table. */
553 subtable
= &(table
->constants
);
554 nodelist
= subtable
->nodelist
;
555 keys
= subtable
->keys
;
556 dead
= subtable
->dead
;
558 totalSlots
+= subtable
->slots
;
560 for (j
= 0; (unsigned) j
< subtable
->slots
; j
++) {
565 while (node
!= NULL
) {
567 if (node
->ref
== 0) {
574 (void) fprintf(table
->err
, "Wrong number of keys found \
575 in the constant table (difference=%d)\n", keys
);
579 (void) fprintf(table
->err
, "Wrong number of dead found \
580 in the constant table (difference=%d)\n", dead
);
582 if ((unsigned) totalKeys
!= table
->keys
+ table
->keysZ
) {
583 (void) fprintf(table
->err
, "Wrong number of total keys found \
584 (difference=%d)\n", (int) (totalKeys
-table
->keys
));
586 if ((unsigned) totalSlots
!= table
->slots
) {
587 (void) fprintf(table
->err
, "Wrong number of total slots found \
588 (difference=%d)\n", (int) (totalSlots
-table
->slots
));
590 if (table
->minDead
!= (unsigned) (table
->gcFrac
* table
->slots
)) {
591 (void) fprintf(table
->err
, "Wrong number of minimum dead found \
592 (%u vs. %u)\n", table
->minDead
,
593 (unsigned) (table
->gcFrac
* (double) table
->slots
));
595 if ((unsigned) totalDead
!= table
->dead
+ table
->deadZ
) {
596 (void) fprintf(table
->err
, "Wrong number of total dead found \
597 (difference=%d)\n", (int) (totalDead
-table
->dead
));
599 (void)printf("Average length of non-empty lists = %g\n",
600 (double) table
->keys
/ (double) nonEmpty
);
604 } /* end of Cudd_CheckKeys */
607 /*---------------------------------------------------------------------------*/
608 /* Definition of internal functions */
609 /*---------------------------------------------------------------------------*/
612 /**Function********************************************************************
614 Synopsis [Prints information about the heap.]
616 Description [Prints to the manager's stdout the number of live nodes for each
617 level of the DD heap that contains at least one live node. It also
618 prints a summary containing:
620 <li> total number of tables;
621 <li> number of tables with live nodes;
622 <li> table with the largest number of live nodes;
623 <li> number of nodes in that table.
625 If more than one table contains the maximum number of live nodes,
626 only the one of lowest index is reported. Returns 1 in case of success
633 ******************************************************************************/
638 int ntables
= dd
->size
;
639 DdSubtable
*subtables
= dd
->subtables
;
640 int i
, /* loop index */
641 nodes
, /* live nodes in i-th layer */
642 retval
, /* return value of fprintf */
643 largest
= -1, /* index of the table with most live nodes */
644 maxnodes
= -1, /* maximum number of live nodes in a table */
645 nonempty
= 0; /* number of tables with live nodes */
648 #if SIZEOF_VOID_P == 8
649 retval
= fprintf(dd
->out
,"*** DD heap profile for 0x%lx ***\n",
652 retval
= fprintf(dd
->out
,"*** DD heap profile for 0x%x ***\n",
655 if (retval
== EOF
) return 0;
657 /* Print number of live nodes for each nonempty table. */
658 for (i
=0; i
<ntables
; i
++) {
659 nodes
= subtables
[i
].keys
- subtables
[i
].dead
;
662 retval
= fprintf(dd
->out
,"%5d: %5d nodes\n", i
, nodes
);
663 if (retval
== EOF
) return 0;
664 if (nodes
> maxnodes
) {
671 nodes
= dd
->constants
.keys
- dd
->constants
.dead
;
674 retval
= fprintf(dd
->out
,"const: %5d nodes\n", nodes
);
675 if (retval
== EOF
) return 0;
676 if (nodes
> maxnodes
) {
678 largest
= CUDD_CONST_INDEX
;
683 retval
= fprintf(dd
->out
,"Summary: %d tables, %d non-empty, largest: %d ",
684 ntables
+1, nonempty
, largest
);
685 if (retval
== EOF
) return 0;
686 retval
= fprintf(dd
->out
,"(with %d nodes)\n", maxnodes
);
687 if (retval
== EOF
) return 0;
691 } /* end of cuddHeapProfile */
694 /**Function********************************************************************
696 Synopsis [Prints out information on a node.]
698 Description [Prints out information on a node.]
704 ******************************************************************************/
711 #if SIZEOF_VOID_P == 8
712 (void) fprintf(fp
," node 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",(ptruint
)f
,f
->index
,f
->ref
,(ptruint
)cuddT(f
),(ptruint
)cuddE(f
));
714 (void) fprintf(fp
," node 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",(ptruint
)f
,f
->index
,f
->ref
,(ptruint
)cuddT(f
),(ptruint
)cuddE(f
));
717 } /* end of cuddPrintNode */
721 /**Function********************************************************************
723 Synopsis [Prints the variable groups as a parenthesized list.]
725 Description [Prints the variable groups as a parenthesized list.
726 For each group the level range that it represents is printed. After
727 each group, the group's flags are printed, preceded by a `|'. For
728 each flag (except MTR_TERMINAL) a character is printed.
734 The second argument, silent, if different from 0, causes
735 Cudd_PrintVarGroups to only check the syntax of the group tree.]
741 ******************************************************************************/
744 DdManager
* dd
/* manager */,
745 MtrNode
* root
/* root of the group tree */,
746 int zdd
/* 0: BDD; 1: ZDD */,
747 int silent
/* flag to check tree syntax only */)
752 assert(root
!= NULL
);
753 assert(root
->younger
== NULL
|| root
->younger
->elder
== root
);
754 assert(root
->elder
== NULL
|| root
->elder
->younger
== root
);
756 level
= dd
->permZ
[root
->index
];
758 level
= dd
->perm
[root
->index
];
760 if (!silent
) (void) printf("(%d",level
);
761 if (MTR_TEST(root
,MTR_TERMINAL
) || root
->child
== NULL
) {
762 if (!silent
) (void) printf(",");
765 while (node
!= NULL
) {
766 assert(node
->low
>= root
->low
&& (int) (node
->low
+ node
->size
) <= (int) (root
->low
+ root
->size
));
767 assert(node
->parent
== root
);
768 cuddPrintVarGroups(dd
,node
,zdd
,silent
);
769 node
= node
->younger
;
773 (void) printf("%d", (int) (level
+ root
->size
- 1));
774 if (root
->flags
!= MTR_DEFAULT
) {
776 if (MTR_TEST(root
,MTR_FIXED
)) (void) printf("F");
777 if (MTR_TEST(root
,MTR_NEWNODE
)) (void) printf("N");
778 if (MTR_TEST(root
,MTR_SOFT
)) (void) printf("S");
781 if (root
->parent
== NULL
) (void) printf("\n");
783 assert((root
->flags
&~(MTR_TERMINAL
| MTR_SOFT
| MTR_FIXED
| MTR_NEWNODE
)) == 0);
786 } /* end of cuddPrintVarGroups */
789 /*---------------------------------------------------------------------------*/
790 /* Definition of static functions */
791 /*---------------------------------------------------------------------------*/
794 /**Function********************************************************************
796 Synopsis [Searches the subtables above node for its parents.]
804 ******************************************************************************/
815 for (i
= 0; i
< cuddI(table
,node
->index
); i
++) {
816 nodelist
= table
->subtables
[i
].nodelist
;
817 slots
= table
->subtables
[i
].slots
;
819 for (j
=0;j
<slots
;j
++) {
822 if (cuddT(f
) == node
|| Cudd_Regular(cuddE(f
)) == node
) {
823 #if SIZEOF_VOID_P == 8
824 (void) fprintf(table
->out
,"parent is at 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",
825 (ptruint
)f
,f
->index
,f
->ref
,(ptruint
)cuddT(f
),(ptruint
)cuddE(f
));
827 (void) fprintf(table
->out
,"parent is at 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",
828 (ptruint
)f
,f
->index
,f
->ref
,(ptruint
)cuddT(f
),(ptruint
)cuddE(f
));
836 } /* end of debugFindParent */
840 /**Function********************************************************************
842 Synopsis [Reports an error if a (dead) node has a non-dead parent.]
844 Description [Searches all the subtables above node. Very expensive.
845 The same check is now implemented more efficiently in ddDebugCheck.]
849 SeeAlso [debugFindParent]
851 ******************************************************************************/
859 DdNode
**nodelist
,*f
;
861 for (i
= 0; i
< cuddI(table
,node
->index
); i
++) {
862 nodelist
= table
->subtables
[i
].nodelist
;
863 slots
= table
->subtables
[i
].slots
;
865 for (j
=0;j
<slots
;j
++) {
868 if ((Cudd_Regular(cuddE(f
)) == node
|| cuddT(f
) == node
) && f
->ref
!= 0) {
869 (void) fprintf(table
->err
,
870 "error with zero ref count\n");
871 (void) fprintf(table
->err
,"parent is 0x%x, id = %u, ref = %u, then = 0x%x, else = 0x%x\n",f
,f
->index
,f
->ref
,cuddT(f
),cuddE(f
));
872 (void) fprintf(table
->err
,"child is 0x%x, id = %u, ref = %u, then = 0x%x, else = 0x%x\n",node
,node
->index
,node
->ref
,cuddT(node
),cuddE(node
));