src/bdd/cudd/cuddCheck.c File Reference
#include "util_hack.h"#include "cuddInt.h"
Include dependency graph for cuddCheck.c:
Go to the source code of this file.
Functions | |
| static void debugFindParent | ARGS ((DdManager *table, DdNode *node)) |
| int | Cudd_DebugCheck (DdManager *table) |
| int | Cudd_CheckKeys (DdManager *table) |
| int | cuddHeapProfile (DdManager *dd) |
| void | cuddPrintNode (DdNode *f, FILE *fp) |
| void | cuddPrintVarGroups (DdManager *dd, MtrNode *root, int zdd, int silent) |
| static void | debugFindParent (DdManager *table, DdNode *node) |
Variables | |
| static char rcsid[] | DD_UNUSED = "$Id: cuddCheck.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" |
Function Documentation
| int Cudd_CheckKeys | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Checks for several conditions that should not occur.]
Description [Checks for the following conditions:
- Wrong sizes of subtables.
- Wrong number of keys found in unique subtable.
- Wrong number of dead found in unique subtable.
- Wrong number of keys found in the constant table
- Wrong number of dead found in the constant table
- Wrong number of total slots found
- Wrong number of maximum keys found
- Wrong number of total dead found
Reports the average length of non-empty lists. Returns the number of subtables for which the number of keys is wrong.]
SideEffects [None]
SeeAlso [Cudd_DebugCheck]
Definition at line 426 of file cuddCheck.c.
00428 { 00429 int size; 00430 int i,j; 00431 DdNodePtr *nodelist; 00432 DdNode *node; 00433 DdNode *sentinel = &(table->sentinel); 00434 DdSubtable *subtable; 00435 int keys; 00436 int dead; 00437 int count = 0; 00438 int totalKeys = 0; 00439 int totalSlots = 0; 00440 int totalDead = 0; 00441 int nonEmpty = 0; 00442 unsigned int slots; 00443 int logSlots; 00444 int shift; 00445 00446 size = table->size; 00447 00448 for (i = 0; i < size; i++) { 00449 subtable = &(table->subtables[i]); 00450 nodelist = subtable->nodelist; 00451 keys = subtable->keys; 00452 dead = subtable->dead; 00453 totalKeys += keys; 00454 slots = subtable->slots; 00455 shift = subtable->shift; 00456 logSlots = sizeof(int) * 8 - shift; 00457 if (((slots >> logSlots) << logSlots) != slots) { 00458 (void) fprintf(table->err, 00459 "Unique table %d is not the right power of 2\n", i); 00460 (void) fprintf(table->err, 00461 " slots = %u shift = %d\n", slots, shift); 00462 } 00463 totalSlots += slots; 00464 totalDead += dead; 00465 for (j = 0; (unsigned) j < slots; j++) { 00466 node = nodelist[j]; 00467 if (node != sentinel) { 00468 nonEmpty++; 00469 } 00470 while (node != sentinel) { 00471 keys--; 00472 if (node->ref == 0) { 00473 dead--; 00474 } 00475 node = node->next; 00476 } 00477 } 00478 if (keys != 0) { 00479 (void) fprintf(table->err, "Wrong number of keys found \ 00480 in unique table %d (difference=%d)\n", i, keys); 00481 count++; 00482 } 00483 if (dead != 0) { 00484 (void) fprintf(table->err, "Wrong number of dead found \ 00485 in unique table no. %d (difference=%d)\n", i, dead); 00486 } 00487 } /* for each BDD/ADD subtable */ 00488 00489 /* Check the ZDD subtables. */ 00490 size = table->sizeZ; 00491 00492 for (i = 0; i < size; i++) { 00493 subtable = &(table->subtableZ[i]); 00494 nodelist = subtable->nodelist; 00495 keys = subtable->keys; 00496 dead = subtable->dead; 00497 totalKeys += keys; 00498 totalSlots += subtable->slots; 00499 totalDead += dead; 00500 for (j = 0; (unsigned) j < subtable->slots; j++) { 00501 node = nodelist[j]; 00502 if (node != NULL) { 00503 nonEmpty++; 00504 } 00505 while (node != NULL) { 00506 keys--; 00507 if (node->ref == 0) { 00508 dead--; 00509 } 00510 node = node->next; 00511 } 00512 } 00513 if (keys != 0) { 00514 (void) fprintf(table->err, "Wrong number of keys found \ 00515 in ZDD unique table no. %d (difference=%d)\n", i, keys); 00516 count++; 00517 } 00518 if (dead != 0) { 00519 (void) fprintf(table->err, "Wrong number of dead found \ 00520 in ZDD unique table no. %d (difference=%d)\n", i, dead); 00521 } 00522 } /* for each ZDD subtable */ 00523 00524 /* Check the constant table. */ 00525 subtable = &(table->constants); 00526 nodelist = subtable->nodelist; 00527 keys = subtable->keys; 00528 dead = subtable->dead; 00529 totalKeys += keys; 00530 totalSlots += subtable->slots; 00531 totalDead += dead; 00532 for (j = 0; (unsigned) j < subtable->slots; j++) { 00533 node = nodelist[j]; 00534 if (node != NULL) { 00535 nonEmpty++; 00536 } 00537 while (node != NULL) { 00538 keys--; 00539 if (node->ref == 0) { 00540 dead--; 00541 } 00542 node = node->next; 00543 } 00544 } 00545 if (keys != 0) { 00546 (void) fprintf(table->err, "Wrong number of keys found \ 00547 in the constant table (difference=%d)\n", keys); 00548 count++; 00549 } 00550 if (dead != 0) { 00551 (void) fprintf(table->err, "Wrong number of dead found \ 00552 in the constant table (difference=%d)\n", dead); 00553 } 00554 if ((unsigned) totalKeys != table->keys + table->keysZ) { 00555 (void) fprintf(table->err, "Wrong number of total keys found \ 00556 (difference=%d)\n", totalKeys-table->keys); 00557 } 00558 if ((unsigned) totalSlots != table->slots) { 00559 (void) fprintf(table->err, "Wrong number of total slots found \ 00560 (difference=%d)\n", totalSlots-table->slots); 00561 } 00562 if (table->minDead != (unsigned) (table->gcFrac * table->slots)) { 00563 (void) fprintf(table->err, "Wrong number of minimum dead found \ 00564 (%d vs. %d)\n", table->minDead, 00565 (unsigned) (table->gcFrac * (double) table->slots)); 00566 } 00567 if ((unsigned) totalDead != table->dead + table->deadZ) { 00568 (void) fprintf(table->err, "Wrong number of total dead found \ 00569 (difference=%d)\n", totalDead-table->dead); 00570 } 00571 (void)printf("Average length of non-empty lists = %g\n", 00572 (double) table->keys / (double) nonEmpty); 00573 00574 return(count); 00575 00576 } /* end of Cudd_CheckKeys */
| int Cudd_DebugCheck | ( | DdManager * | table | ) |
AutomaticEnd Function********************************************************************
Synopsis [Checks for inconsistencies in the DD heap.]
Description [Checks for inconsistencies in the DD heap:
- node has illegal index
- live node has dead children
- node has illegal Then or Else pointers
- BDD/ADD node has identical children
- ZDD node has zero then child
- wrong number of total nodes
- wrong number of dead nodes
- ref count error at node
Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is not enough memory; 1 otherwise.]
SideEffects [None]
SeeAlso [Cudd_CheckKeys]
Definition at line 111 of file cuddCheck.c.
00113 { 00114 unsigned int i; 00115 int j,count; 00116 int slots; 00117 DdNodePtr *nodelist; 00118 DdNode *f; 00119 DdNode *sentinel = &(table->sentinel); 00120 st_table *edgeTable; /* stores internal ref count for each node */ 00121 st_generator *gen; 00122 int flag = 0; 00123 int totalNode; 00124 int deadNode; 00125 int index; 00126 00127 00128 edgeTable = st_init_table(st_ptrcmp,st_ptrhash); 00129 if (edgeTable == NULL) return(CUDD_OUT_OF_MEM); 00130 00131 /* Check the BDD/ADD subtables. */ 00132 for (i = 0; i < (unsigned) table->size; i++) { 00133 index = table->invperm[i]; 00134 if (i != (unsigned) table->perm[index]) { 00135 (void) fprintf(table->err, 00136 "Permutation corrupted: invperm[%d] = %d\t perm[%d] = %d\n", 00137 i, index, index, table->perm[index]); 00138 } 00139 nodelist = table->subtables[i].nodelist; 00140 slots = table->subtables[i].slots; 00141 00142 totalNode = 0; 00143 deadNode = 0; 00144 for (j = 0; j < slots; j++) { /* for each subtable slot */ 00145 f = nodelist[j]; 00146 while (f != sentinel) { 00147 totalNode++; 00148 if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) { 00149 if ((int) f->index != index) { 00150 (void) fprintf(table->err, 00151 "Error: node has illegal index\n"); 00152 cuddPrintNode(f,table->err); 00153 flag = 1; 00154 } 00155 if ((unsigned) cuddI(table,cuddT(f)->index) <= i || 00156 (unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index) 00157 <= i) { 00158 (void) fprintf(table->err, 00159 "Error: node has illegal children\n"); 00160 cuddPrintNode(f,table->err); 00161 flag = 1; 00162 } 00163 if (Cudd_Regular(cuddT(f)) != cuddT(f)) { 00164 (void) fprintf(table->err, 00165 "Error: node has illegal form\n"); 00166 cuddPrintNode(f,table->err); 00167 flag = 1; 00168 } 00169 if (cuddT(f) == cuddE(f)) { 00170 (void) fprintf(table->err, 00171 "Error: node has identical children\n"); 00172 cuddPrintNode(f,table->err); 00173 flag = 1; 00174 } 00175 if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) { 00176 (void) fprintf(table->err, 00177 "Error: live node has dead children\n"); 00178 cuddPrintNode(f,table->err); 00179 flag =1; 00180 } 00181 /* Increment the internal reference count for the 00182 ** then child of the current node. 00183 */ 00184 if (st_lookup(edgeTable,(char *)cuddT(f),(char **)&count)) { 00185 count++; 00186 } else { 00187 count = 1; 00188 } 00189 if (st_insert(edgeTable,(char *)cuddT(f), 00190 (char *)(long)count) == ST_OUT_OF_MEM) { 00191 st_free_table(edgeTable); 00192 return(CUDD_OUT_OF_MEM); 00193 } 00194 00195 /* Increment the internal reference count for the 00196 ** else child of the current node. 00197 */ 00198 if (st_lookup(edgeTable,(char *)Cudd_Regular(cuddE(f)),(char **)&count)) { 00199 count++; 00200 } else { 00201 count = 1; 00202 } 00203 if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)), 00204 (char *)(long)count) == ST_OUT_OF_MEM) { 00205 st_free_table(edgeTable); 00206 return(CUDD_OUT_OF_MEM); 00207 } 00208 } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) { 00209 deadNode++; 00210 #if 0 00211 debugCheckParent(table,f); 00212 #endif 00213 } else { 00214 fprintf(table->err, 00215 "Error: node has illegal Then or Else pointers\n"); 00216 cuddPrintNode(f,table->err); 00217 flag = 1; 00218 } 00219 00220 f = f->next; 00221 } /* for each element of the collision list */ 00222 } /* for each subtable slot */ 00223 00224 if ((unsigned) totalNode != table->subtables[i].keys) { 00225 fprintf(table->err,"Error: wrong number of total nodes\n"); 00226 flag = 1; 00227 } 00228 if ((unsigned) deadNode != table->subtables[i].dead) { 00229 fprintf(table->err,"Error: wrong number of dead nodes\n"); 00230 flag = 1; 00231 } 00232 } /* for each BDD/ADD subtable */ 00233 00234 /* Check the ZDD subtables. */ 00235 for (i = 0; i < (unsigned) table->sizeZ; i++) { 00236 index = table->invpermZ[i]; 00237 if (i != (unsigned) table->permZ[index]) { 00238 (void) fprintf(table->err, 00239 "Permutation corrupted: invpermZ[%d] = %d\t permZ[%d] = %d in ZDD\n", 00240 i, index, index, table->permZ[index]); 00241 } 00242 nodelist = table->subtableZ[i].nodelist; 00243 slots = table->subtableZ[i].slots; 00244 00245 totalNode = 0; 00246 deadNode = 0; 00247 for (j = 0; j < slots; j++) { /* for each subtable slot */ 00248 f = nodelist[j]; 00249 while (f != NULL) { 00250 totalNode++; 00251 if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) { 00252 if ((int) f->index != index) { 00253 (void) fprintf(table->err, 00254 "Error: ZDD node has illegal index\n"); 00255 cuddPrintNode(f,table->err); 00256 flag = 1; 00257 } 00258 if (Cudd_IsComplement(cuddT(f)) || 00259 Cudd_IsComplement(cuddE(f))) { 00260 (void) fprintf(table->err, 00261 "Error: ZDD node has complemented children\n"); 00262 cuddPrintNode(f,table->err); 00263 flag = 1; 00264 } 00265 if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i || 00266 (unsigned) cuddIZ(table,cuddE(f)->index) <= i) { 00267 (void) fprintf(table->err, 00268 "Error: ZDD node has illegal children\n"); 00269 cuddPrintNode(f,table->err); 00270 cuddPrintNode(cuddT(f),table->err); 00271 cuddPrintNode(cuddE(f),table->err); 00272 flag = 1; 00273 } 00274 if (cuddT(f) == DD_ZERO(table)) { 00275 (void) fprintf(table->err, 00276 "Error: ZDD node has zero then child\n"); 00277 cuddPrintNode(f,table->err); 00278 flag = 1; 00279 } 00280 if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) { 00281 (void) fprintf(table->err, 00282 "Error: ZDD live node has dead children\n"); 00283 cuddPrintNode(f,table->err); 00284 flag =1; 00285 } 00286 /* Increment the internal reference count for the 00287 ** then child of the current node. 00288 */ 00289 if (st_lookup(edgeTable,(char *)cuddT(f),(char **)&count)) { 00290 count++; 00291 } else { 00292 count = 1; 00293 } 00294 if (st_insert(edgeTable,(char *)cuddT(f), 00295 (char *)(long)count) == ST_OUT_OF_MEM) { 00296 st_free_table(edgeTable); 00297 return(CUDD_OUT_OF_MEM); 00298 } 00299 00300 /* Increment the internal reference count for the 00301 ** else child of the current node. 00302 */ 00303 if (st_lookup(edgeTable,(char *)cuddE(f),(char **)&count)) { 00304 count++; 00305 } else { 00306 count = 1; 00307 } 00308 if (st_insert(edgeTable,(char *)cuddE(f), 00309 (char *)(long)count) == ST_OUT_OF_MEM) { 00310 st_free_table(edgeTable); 00311 table->errorCode = CUDD_MEMORY_OUT; 00312 return(CUDD_OUT_OF_MEM); 00313 } 00314 } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) { 00315 deadNode++; 00316 #if 0 00317 debugCheckParent(table,f); 00318 #endif 00319 } else { 00320 fprintf(table->err, 00321 "Error: ZDD node has illegal Then or Else pointers\n"); 00322 cuddPrintNode(f,table->err); 00323 flag = 1; 00324 } 00325 00326 f = f->next; 00327 } /* for each element of the collision list */ 00328 } /* for each subtable slot */ 00329 00330 if ((unsigned) totalNode != table->subtableZ[i].keys) { 00331 fprintf(table->err, 00332 "Error: wrong number of total nodes in ZDD\n"); 00333 flag = 1; 00334 } 00335 if ((unsigned) deadNode != table->subtableZ[i].dead) { 00336 fprintf(table->err, 00337 "Error: wrong number of dead nodes in ZDD\n"); 00338 flag = 1; 00339 } 00340 } /* for each ZDD subtable */ 00341 00342 /* Check the constant table. */ 00343 nodelist = table->constants.nodelist; 00344 slots = table->constants.slots; 00345 00346 totalNode = 0; 00347 deadNode = 0; 00348 for (j = 0; j < slots; j++) { 00349 f = nodelist[j]; 00350 while (f != NULL) { 00351 totalNode++; 00352 if (f->ref != 0) { 00353 if (f->index != CUDD_CONST_INDEX) { 00354 fprintf(table->err,"Error: node has illegal index\n"); 00355 #if SIZEOF_VOID_P == 8 00356 fprintf(table->err, 00357 " node 0x%lx, id = %d, ref = %d, value = %g\n", 00358 (unsigned long)f,f->index,f->ref,cuddV(f)); 00359 #else 00360 fprintf(table->err, 00361 " node 0x%x, id = %d, ref = %d, value = %g\n", 00362 (unsigned)f,f->index,f->ref,cuddV(f)); 00363 #endif 00364 flag = 1; 00365 } 00366 } else { 00367 deadNode++; 00368 } 00369 f = f->next; 00370 } 00371 } 00372 if ((unsigned) totalNode != table->constants.keys) { 00373 (void) fprintf(table->err, 00374 "Error: wrong number of total nodes in constants\n"); 00375 flag = 1; 00376 } 00377 if ((unsigned) deadNode != table->constants.dead) { 00378 (void) fprintf(table->err, 00379 "Error: wrong number of dead nodes in constants\n"); 00380 flag = 1; 00381 } 00382 gen = st_init_gen(edgeTable); 00383 while (st_gen(gen,(char **)&f,(char **)&count)) { 00384 if (count > (int)(f->ref) && f->ref != DD_MAXREF) { 00385 #if SIZEOF_VOID_P == 8 00386 fprintf(table->err,"ref count error at node 0x%lx, count = %d, id = %d, ref = %d, then = 0x%lx, else = 0x%lx\n",(unsigned long)f,count,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f)); 00387 #else 00388 fprintf(table->err,"ref count error at node 0x%x, count = %d, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",(unsigned)f,count,f->index,f->ref,(unsigned)cuddT(f),(unsigned)cuddE(f)); 00389 #endif 00390 debugFindParent(table,f); 00391 flag = 1; 00392 } 00393 } 00394 st_free_gen(gen); 00395 st_free_table(edgeTable); 00396 00397 return (flag); 00398 00399 } /* end of Cudd_DebugCheck */
| int cuddHeapProfile | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Prints information about the heap.]
Description [Prints to the manager's stdout the number of live nodes for each level of the DD heap that contains at least one live node. It also prints a summary containing:
- total number of tables;
- number of tables with live nodes;
- table with the largest number of live nodes;
- number of nodes in that table.
If more than one table contains the maximum number of live nodes, only the one of lowest index is reported. Returns 1 in case of success and 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 607 of file cuddCheck.c.
00609 { 00610 int ntables = dd->size; 00611 DdSubtable *subtables = dd->subtables; 00612 int i, /* loop index */ 00613 nodes, /* live nodes in i-th layer */ 00614 retval, /* return value of fprintf */ 00615 largest = -1, /* index of the table with most live nodes */ 00616 maxnodes = -1, /* maximum number of live nodes in a table */ 00617 nonempty = 0; /* number of tables with live nodes */ 00618 00619 /* Print header. */ 00620 #if SIZEOF_VOID_P == 8 00621 retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n", 00622 (unsigned long) dd); 00623 #else 00624 retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n", 00625 (unsigned) dd); 00626 #endif 00627 if (retval == EOF) return 0; 00628 00629 /* Print number of live nodes for each nonempty table. */ 00630 for (i=0; i<ntables; i++) { 00631 nodes = subtables[i].keys - subtables[i].dead; 00632 if (nodes) { 00633 nonempty++; 00634 retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes); 00635 if (retval == EOF) return 0; 00636 if (nodes > maxnodes) { 00637 maxnodes = nodes; 00638 largest = i; 00639 } 00640 } 00641 } 00642 00643 nodes = dd->constants.keys - dd->constants.dead; 00644 if (nodes) { 00645 nonempty++; 00646 retval = fprintf(dd->out,"const: %5d nodes\n", nodes); 00647 if (retval == EOF) return 0; 00648 if (nodes > maxnodes) { 00649 maxnodes = nodes; 00650 largest = CUDD_CONST_INDEX; 00651 } 00652 } 00653 00654 /* Print summary. */ 00655 retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ", 00656 ntables+1, nonempty, largest); 00657 if (retval == EOF) return 0; 00658 retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes); 00659 if (retval == EOF) return 0; 00660 00661 return(1); 00662 00663 } /* end of cuddHeapProfile */
| void cuddPrintNode | ( | DdNode * | f, | |
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Prints out information on a node.]
Description [Prints out information on a node.]
SideEffects [None]
SeeAlso []
Definition at line 678 of file cuddCheck.c.
00681 { 00682 f = Cudd_Regular(f); 00683 #if SIZEOF_VOID_P == 8 00684 (void) fprintf(fp," node 0x%lx, id = %d, ref = %d, then = 0x%lx, else = 0x%lx\n",(unsigned long)f,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f)); 00685 #else 00686 (void) fprintf(fp," node 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",(unsigned)f,f->index,f->ref,(unsigned)cuddT(f),(unsigned)cuddE(f)); 00687 #endif 00688 00689 } /* end of cuddPrintNode */
Function********************************************************************
Synopsis [Prints the variable groups as a parenthesized list.]
Description [Prints the variable groups as a parenthesized list. For each group the level range that it represents is printed. After each group, the group's flags are printed, preceded by a `|'. For each flag (except MTR_TERMINAL) a character is printed.
- F: MTR_FIXED
- N: MTR_NEWNODE
- S: MTR_SOFT
The second argument, silent, if different from 0, causes Cudd_PrintVarGroups to only check the syntax of the group tree.]
SideEffects [None]
SeeAlso []
Definition at line 715 of file cuddCheck.c.
00718 : BDD; 1: ZDD */, 00719 int silent /* flag to check tree syntax only */) 00720 { 00721 MtrNode *node; 00722 int level; 00723 00724 assert(root != NULL); 00725 assert(root->younger == NULL || root->younger->elder == root); 00726 assert(root->elder == NULL || root->elder->younger == root); 00727 if (zdd) { 00728 level = dd->permZ[root->index]; 00729 } else { 00730 level = dd->perm[root->index]; 00731 } 00732 if (!silent) (void) printf("(%d",level); 00733 if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) { 00734 if (!silent) (void) printf(","); 00735 } else { 00736 node = root->child; 00737 while (node != NULL) { 00738 assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size)); 00739 assert(node->parent == root); 00740 cuddPrintVarGroups(dd,node,zdd,silent); 00741 node = node->younger; 00742 } 00743 } 00744 if (!silent) { 00745 (void) printf("%d", level + root->size - 1); 00746 if (root->flags != MTR_DEFAULT) { 00747 (void) printf("|"); 00748 if (MTR_TEST(root,MTR_FIXED)) (void) printf("F"); 00749 if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N"); 00750 if (MTR_TEST(root,MTR_SOFT)) (void) printf("S"); 00751 } 00752 (void) printf(")"); 00753 if (root->parent == NULL) (void) printf("\n"); 00754 } 00755 assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0); 00756 return; 00757 00758 } /* end of cuddPrintVarGroups */
Function********************************************************************
Synopsis [Searches the subtables above node for its parents.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 778 of file cuddCheck.c.
00781 { 00782 int i,j; 00783 int slots; 00784 DdNodePtr *nodelist; 00785 DdNode *f; 00786 00787 for (i = 0; i < cuddI(table,node->index); i++) { 00788 nodelist = table->subtables[i].nodelist; 00789 slots = table->subtables[i].slots; 00790 00791 for (j=0;j<slots;j++) { 00792 f = nodelist[j]; 00793 while (f != NULL) { 00794 if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) { 00795 #if SIZEOF_VOID_P == 8 00796 (void) fprintf(table->out,"parent is at 0x%lx, id = %d, ref = %d, then = 0x%lx, else = 0x%lx\n", 00797 (unsigned long)f,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f)); 00798 #else 00799 (void) fprintf(table->out,"parent is at 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n", 00800 (unsigned)f,f->index,f->ref,(unsigned)cuddT(f),(unsigned)cuddE(f)); 00801 #endif 00802 } 00803 f = f->next; 00804 } 00805 } 00806 } 00807 00808 } /* end of debugFindParent */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddCheck.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddCheck.c]
PackageName [cudd]
Synopsis [Functions to check consistency of data structures.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 60 of file cuddCheck.c.
