diff options
Diffstat (limited to 'src/bdd/cudd/cuddCheck.c')
| -rw-r--r-- | src/bdd/cudd/cuddCheck.c | 851 |
1 files changed, 0 insertions, 851 deletions
diff --git a/src/bdd/cudd/cuddCheck.c b/src/bdd/cudd/cuddCheck.c deleted file mode 100644 index aec8246d..00000000 --- a/src/bdd/cudd/cuddCheck.c +++ /dev/null @@ -1,851 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddCheck.c] - - PackageName [cudd] - - Synopsis [Functions to check consistency of data structures.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_DebugCheck() - <li> Cudd_CheckKeys() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddHeapProfile() - <li> cuddPrintNode() - <li> cuddPrintVarGroups() - </ul> - Static procedures included in this module: - <ul> - <li> debugFindParent() - </ul> - ] - - 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.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static void debugFindParent ARGS((DdManager *table, DdNode *node)); -#if 0 -static void debugCheckParent ARGS((DdManager *table, DdNode *node)); -#endif - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Checks for inconsistencies in the DD heap.] - - Description [Checks for inconsistencies in the DD heap: - <ul> - <li> node has illegal index - <li> live node has dead children - <li> node has illegal Then or Else pointers - <li> BDD/ADD node has identical children - <li> ZDD node has zero then child - <li> wrong number of total nodes - <li> wrong number of dead nodes - <li> ref count error at node - </ul> - Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is - not enough memory; 1 otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_CheckKeys] - -******************************************************************************/ -int -Cudd_DebugCheck( - DdManager * table) -{ - unsigned int i; - int j,count; - int slots; - DdNodePtr *nodelist; - DdNode *f; - DdNode *sentinel = &(table->sentinel); - st_table *edgeTable; /* stores internal ref count for each node */ - st_generator *gen; - int flag = 0; - int totalNode; - int deadNode; - int index; - - - edgeTable = st_init_table(st_ptrcmp,st_ptrhash); - if (edgeTable == NULL) return(CUDD_OUT_OF_MEM); - - /* Check the BDD/ADD subtables. */ - for (i = 0; i < (unsigned) table->size; i++) { - index = table->invperm[i]; - if (i != (unsigned) table->perm[index]) { - (void) fprintf(table->err, - "Permutation corrupted: invperm[%d] = %d\t perm[%d] = %d\n", - i, index, index, table->perm[index]); - } - nodelist = table->subtables[i].nodelist; - slots = table->subtables[i].slots; - - totalNode = 0; - deadNode = 0; - for (j = 0; j < slots; j++) { /* for each subtable slot */ - f = nodelist[j]; - while (f != sentinel) { - totalNode++; - if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) { - if ((int) f->index != index) { - (void) fprintf(table->err, - "Error: node has illegal index\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if ((unsigned) cuddI(table,cuddT(f)->index) <= i || - (unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index) - <= i) { - (void) fprintf(table->err, - "Error: node has illegal children\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if (Cudd_Regular(cuddT(f)) != cuddT(f)) { - (void) fprintf(table->err, - "Error: node has illegal form\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if (cuddT(f) == cuddE(f)) { - (void) fprintf(table->err, - "Error: node has identical children\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) { - (void) fprintf(table->err, - "Error: live node has dead children\n"); - cuddPrintNode(f,table->err); - flag =1; - } - /* Increment the internal reference count for the - ** then child of the current node. - */ - if (st_lookup(edgeTable,(char *)cuddT(f),(char **)&count)) { - count++; - } else { - count = 1; - } - if (st_insert(edgeTable,(char *)cuddT(f), - (char *)(long)count) == ST_OUT_OF_MEM) { - st_free_table(edgeTable); - return(CUDD_OUT_OF_MEM); - } - - /* Increment the internal reference count for the - ** else child of the current node. - */ - if (st_lookup(edgeTable,(char *)Cudd_Regular(cuddE(f)),(char **)&count)) { - count++; - } else { - count = 1; - } - if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)), - (char *)(long)count) == ST_OUT_OF_MEM) { - st_free_table(edgeTable); - return(CUDD_OUT_OF_MEM); - } - } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) { - deadNode++; -#if 0 - debugCheckParent(table,f); -#endif - } else { - fprintf(table->err, - "Error: node has illegal Then or Else pointers\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - - f = f->next; - } /* for each element of the collision list */ - } /* for each subtable slot */ - - if ((unsigned) totalNode != table->subtables[i].keys) { - fprintf(table->err,"Error: wrong number of total nodes\n"); - flag = 1; - } - if ((unsigned) deadNode != table->subtables[i].dead) { - fprintf(table->err,"Error: wrong number of dead nodes\n"); - flag = 1; - } - } /* for each BDD/ADD subtable */ - - /* Check the ZDD subtables. */ - for (i = 0; i < (unsigned) table->sizeZ; i++) { - index = table->invpermZ[i]; - if (i != (unsigned) table->permZ[index]) { - (void) fprintf(table->err, - "Permutation corrupted: invpermZ[%d] = %d\t permZ[%d] = %d in ZDD\n", - i, index, index, table->permZ[index]); - } - nodelist = table->subtableZ[i].nodelist; - slots = table->subtableZ[i].slots; - - totalNode = 0; - deadNode = 0; - for (j = 0; j < slots; j++) { /* for each subtable slot */ - f = nodelist[j]; - while (f != NULL) { - totalNode++; - if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) { - if ((int) f->index != index) { - (void) fprintf(table->err, - "Error: ZDD node has illegal index\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if (Cudd_IsComplement(cuddT(f)) || - Cudd_IsComplement(cuddE(f))) { - (void) fprintf(table->err, - "Error: ZDD node has complemented children\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i || - (unsigned) cuddIZ(table,cuddE(f)->index) <= i) { - (void) fprintf(table->err, - "Error: ZDD node has illegal children\n"); - cuddPrintNode(f,table->err); - cuddPrintNode(cuddT(f),table->err); - cuddPrintNode(cuddE(f),table->err); - flag = 1; - } - if (cuddT(f) == DD_ZERO(table)) { - (void) fprintf(table->err, - "Error: ZDD node has zero then child\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) { - (void) fprintf(table->err, - "Error: ZDD live node has dead children\n"); - cuddPrintNode(f,table->err); - flag =1; - } - /* Increment the internal reference count for the - ** then child of the current node. - */ - if (st_lookup(edgeTable,(char *)cuddT(f),(char **)&count)) { - count++; - } else { - count = 1; - } - if (st_insert(edgeTable,(char *)cuddT(f), - (char *)(long)count) == ST_OUT_OF_MEM) { - st_free_table(edgeTable); - return(CUDD_OUT_OF_MEM); - } - - /* Increment the internal reference count for the - ** else child of the current node. - */ - if (st_lookup(edgeTable,(char *)cuddE(f),(char **)&count)) { - count++; - } else { - count = 1; - } - if (st_insert(edgeTable,(char *)cuddE(f), - (char *)(long)count) == ST_OUT_OF_MEM) { - st_free_table(edgeTable); - table->errorCode = CUDD_MEMORY_OUT; - return(CUDD_OUT_OF_MEM); - } - } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) { - deadNode++; -#if 0 - debugCheckParent(table,f); -#endif - } else { - fprintf(table->err, - "Error: ZDD node has illegal Then or Else pointers\n"); - cuddPrintNode(f,table->err); - flag = 1; - } - - f = f->next; - } /* for each element of the collision list */ - } /* for each subtable slot */ - - if ((unsigned) totalNode != table->subtableZ[i].keys) { - fprintf(table->err, - "Error: wrong number of total nodes in ZDD\n"); - flag = 1; - } - if ((unsigned) deadNode != table->subtableZ[i].dead) { - fprintf(table->err, - "Error: wrong number of dead nodes in ZDD\n"); - flag = 1; - } - } /* for each ZDD subtable */ - - /* Check the constant table. */ - nodelist = table->constants.nodelist; - slots = table->constants.slots; - - totalNode = 0; - deadNode = 0; - for (j = 0; j < slots; j++) { - f = nodelist[j]; - while (f != NULL) { - totalNode++; - if (f->ref != 0) { - if (f->index != CUDD_CONST_INDEX) { - fprintf(table->err,"Error: node has illegal index\n"); -#if SIZEOF_VOID_P == 8 - fprintf(table->err, - " node 0x%lx, id = %d, ref = %d, value = %g\n", - (unsigned long)f,f->index,f->ref,cuddV(f)); -#else - fprintf(table->err, - " node 0x%x, id = %d, ref = %d, value = %g\n", - (unsigned)f,f->index,f->ref,cuddV(f)); -#endif - flag = 1; - } - } else { - deadNode++; - } - f = f->next; - } - } - if ((unsigned) totalNode != table->constants.keys) { - (void) fprintf(table->err, - "Error: wrong number of total nodes in constants\n"); - flag = 1; - } - if ((unsigned) deadNode != table->constants.dead) { - (void) fprintf(table->err, - "Error: wrong number of dead nodes in constants\n"); - flag = 1; - } - gen = st_init_gen(edgeTable); - while (st_gen(gen,(char **)&f,(char **)&count)) { - if (count > (int)(f->ref) && f->ref != DD_MAXREF) { -#if SIZEOF_VOID_P == 8 - 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)); -#else - 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)); -#endif - debugFindParent(table,f); - flag = 1; - } - } - st_free_gen(gen); - st_free_table(edgeTable); - - return (flag); - -} /* end of Cudd_DebugCheck */ - - -/**Function******************************************************************** - - Synopsis [Checks for several conditions that should not occur.] - - Description [Checks for the following conditions: - <ul> - <li>Wrong sizes of subtables. - <li>Wrong number of keys found in unique subtable. - <li>Wrong number of dead found in unique subtable. - <li>Wrong number of keys found in the constant table - <li>Wrong number of dead found in the constant table - <li>Wrong number of total slots found - <li>Wrong number of maximum keys found - <li>Wrong number of total dead found - </ul> - 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] - -******************************************************************************/ -int -Cudd_CheckKeys( - DdManager * table) -{ - int size; - int i,j; - DdNodePtr *nodelist; - DdNode *node; - DdNode *sentinel = &(table->sentinel); - DdSubtable *subtable; - int keys; - int dead; - int count = 0; - int totalKeys = 0; - int totalSlots = 0; - int totalDead = 0; - int nonEmpty = 0; - unsigned int slots; - int logSlots; - int shift; - - size = table->size; - - for (i = 0; i < size; i++) { - subtable = &(table->subtables[i]); - nodelist = subtable->nodelist; - keys = subtable->keys; - dead = subtable->dead; - totalKeys += keys; - slots = subtable->slots; - shift = subtable->shift; - logSlots = sizeof(int) * 8 - shift; - if (((slots >> logSlots) << logSlots) != slots) { - (void) fprintf(table->err, - "Unique table %d is not the right power of 2\n", i); - (void) fprintf(table->err, - " slots = %u shift = %d\n", slots, shift); - } - totalSlots += slots; - totalDead += dead; - for (j = 0; (unsigned) j < slots; j++) { - node = nodelist[j]; - if (node != sentinel) { - nonEmpty++; - } - while (node != sentinel) { - keys--; - if (node->ref == 0) { - dead--; - } - node = node->next; - } - } - if (keys != 0) { - (void) fprintf(table->err, "Wrong number of keys found \ -in unique table %d (difference=%d)\n", i, keys); - count++; - } - if (dead != 0) { - (void) fprintf(table->err, "Wrong number of dead found \ -in unique table no. %d (difference=%d)\n", i, dead); - } - } /* for each BDD/ADD subtable */ - - /* Check the ZDD subtables. */ - size = table->sizeZ; - - for (i = 0; i < size; i++) { - subtable = &(table->subtableZ[i]); - nodelist = subtable->nodelist; - keys = subtable->keys; - dead = subtable->dead; - totalKeys += keys; - totalSlots += subtable->slots; - totalDead += dead; - for (j = 0; (unsigned) j < subtable->slots; j++) { - node = nodelist[j]; - if (node != NULL) { - nonEmpty++; - } - while (node != NULL) { - keys--; - if (node->ref == 0) { - dead--; - } - node = node->next; - } - } - if (keys != 0) { - (void) fprintf(table->err, "Wrong number of keys found \ -in ZDD unique table no. %d (difference=%d)\n", i, keys); - count++; - } - if (dead != 0) { - (void) fprintf(table->err, "Wrong number of dead found \ -in ZDD unique table no. %d (difference=%d)\n", i, dead); - } - } /* for each ZDD subtable */ - - /* Check the constant table. */ - subtable = &(table->constants); - nodelist = subtable->nodelist; - keys = subtable->keys; - dead = subtable->dead; - totalKeys += keys; - totalSlots += subtable->slots; - totalDead += dead; - for (j = 0; (unsigned) j < subtable->slots; j++) { - node = nodelist[j]; - if (node != NULL) { - nonEmpty++; - } - while (node != NULL) { - keys--; - if (node->ref == 0) { - dead--; - } - node = node->next; - } - } - if (keys != 0) { - (void) fprintf(table->err, "Wrong number of keys found \ -in the constant table (difference=%d)\n", keys); - count++; - } - if (dead != 0) { - (void) fprintf(table->err, "Wrong number of dead found \ -in the constant table (difference=%d)\n", dead); - } - if ((unsigned) totalKeys != table->keys + table->keysZ) { - (void) fprintf(table->err, "Wrong number of total keys found \ -(difference=%d)\n", totalKeys-table->keys); - } - if ((unsigned) totalSlots != table->slots) { - (void) fprintf(table->err, "Wrong number of total slots found \ -(difference=%d)\n", totalSlots-table->slots); - } - if (table->minDead != (unsigned) (table->gcFrac * table->slots)) { - (void) fprintf(table->err, "Wrong number of minimum dead found \ -(%d vs. %d)\n", table->minDead, - (unsigned) (table->gcFrac * (double) table->slots)); - } - if ((unsigned) totalDead != table->dead + table->deadZ) { - (void) fprintf(table->err, "Wrong number of total dead found \ -(difference=%d)\n", totalDead-table->dead); - } - (void)printf("Average length of non-empty lists = %g\n", - (double) table->keys / (double) nonEmpty); - - return(count); - -} /* end of Cudd_CheckKeys */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**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: - <ul> - <li> total number of tables; - <li> number of tables with live nodes; - <li> table with the largest number of live nodes; - <li> number of nodes in that table. - </ul> - 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 [] - -******************************************************************************/ -int -cuddHeapProfile( - DdManager * dd) -{ - int ntables = dd->size; - DdSubtable *subtables = dd->subtables; - int i, /* loop index */ - nodes, /* live nodes in i-th layer */ - retval, /* return value of fprintf */ - largest = -1, /* index of the table with most live nodes */ - maxnodes = -1, /* maximum number of live nodes in a table */ - nonempty = 0; /* number of tables with live nodes */ - - /* Print header. */ -#if SIZEOF_VOID_P == 8 - retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n", - (unsigned long) dd); -#else - retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n", - (unsigned) dd); -#endif - if (retval == EOF) return 0; - - /* Print number of live nodes for each nonempty table. */ - for (i=0; i<ntables; i++) { - nodes = subtables[i].keys - subtables[i].dead; - if (nodes) { - nonempty++; - retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes); - if (retval == EOF) return 0; - if (nodes > maxnodes) { - maxnodes = nodes; - largest = i; - } - } - } - - nodes = dd->constants.keys - dd->constants.dead; - if (nodes) { - nonempty++; - retval = fprintf(dd->out,"const: %5d nodes\n", nodes); - if (retval == EOF) return 0; - if (nodes > maxnodes) { - maxnodes = nodes; - largest = CUDD_CONST_INDEX; - } - } - - /* Print summary. */ - retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ", - ntables+1, nonempty, largest); - if (retval == EOF) return 0; - retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes); - if (retval == EOF) return 0; - - return(1); - -} /* end of cuddHeapProfile */ - - -/**Function******************************************************************** - - Synopsis [Prints out information on a node.] - - Description [Prints out information on a node.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void -cuddPrintNode( - DdNode * f, - FILE *fp) -{ - f = Cudd_Regular(f); -#if SIZEOF_VOID_P == 8 - (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)); -#else - (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)); -#endif - -} /* 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. - <ul> - <li>F: MTR_FIXED - <li>N: MTR_NEWNODE - <li>S: MTR_SOFT - </ul> - The second argument, silent, if different from 0, causes - Cudd_PrintVarGroups to only check the syntax of the group tree.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void -cuddPrintVarGroups( - DdManager * dd /* manager */, - MtrNode * root /* root of the group tree */, - int zdd /* 0: BDD; 1: ZDD */, - int silent /* flag to check tree syntax only */) -{ - MtrNode *node; - int level; - - assert(root != NULL); - assert(root->younger == NULL || root->younger->elder == root); - assert(root->elder == NULL || root->elder->younger == root); - if (zdd) { - level = dd->permZ[root->index]; - } else { - level = dd->perm[root->index]; - } - if (!silent) (void) printf("(%d",level); - if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) { - if (!silent) (void) printf(","); - } else { - node = root->child; - while (node != NULL) { - assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size)); - assert(node->parent == root); - cuddPrintVarGroups(dd,node,zdd,silent); - node = node->younger; - } - } - if (!silent) { - (void) printf("%d", level + root->size - 1); - if (root->flags != MTR_DEFAULT) { - (void) printf("|"); - if (MTR_TEST(root,MTR_FIXED)) (void) printf("F"); - if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N"); - if (MTR_TEST(root,MTR_SOFT)) (void) printf("S"); - } - (void) printf(")"); - if (root->parent == NULL) (void) printf("\n"); - } - assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0); - return; - -} /* end of cuddPrintVarGroups */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Searches the subtables above node for its parents.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static void -debugFindParent( - DdManager * table, - DdNode * node) -{ - int i,j; - int slots; - DdNodePtr *nodelist; - DdNode *f; - - for (i = 0; i < cuddI(table,node->index); i++) { - nodelist = table->subtables[i].nodelist; - slots = table->subtables[i].slots; - - for (j=0;j<slots;j++) { - f = nodelist[j]; - while (f != NULL) { - if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) { -#if SIZEOF_VOID_P == 8 - (void) fprintf(table->out,"parent is at 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)); -#else - (void) fprintf(table->out,"parent is at 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)); -#endif - } - f = f->next; - } - } - } - -} /* end of debugFindParent */ - - -#if 0 -/**Function******************************************************************** - - Synopsis [Reports an error if a (dead) node has a non-dead parent.] - - Description [Searches all the subtables above node. Very expensive. - The same check is now implemented more efficiently in ddDebugCheck.] - - SideEffects [None] - - SeeAlso [debugFindParent] - -******************************************************************************/ -static void -debugCheckParent( - DdManager * table, - DdNode * node) -{ - int i,j; - int slots; - DdNode **nodelist,*f; - - for (i = 0; i < cuddI(table,node->index); i++) { - nodelist = table->subtables[i].nodelist; - slots = table->subtables[i].slots; - - for (j=0;j<slots;j++) { - f = nodelist[j]; - while (f != NULL) { - if ((Cudd_Regular(cuddE(f)) == node || cuddT(f) == node) && f->ref != 0) { - (void) fprintf(table->err, - "error with zero ref count\n"); - (void) fprintf(table->err,"parent is 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",f,f->index,f->ref,cuddT(f),cuddE(f)); - (void) fprintf(table->err,"child is 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",node,node->index,node->ref,cuddT(node),cuddE(node)); - } - f = f->next; - } - } - } -} -#endif |