diff options
Diffstat (limited to 'src/bdd/cudd/cuddCheck.c')
-rw-r--r-- | src/bdd/cudd/cuddCheck.c | 881 |
1 files changed, 456 insertions, 425 deletions
diff --git a/src/bdd/cudd/cuddCheck.c b/src/bdd/cudd/cuddCheck.c index 92c0f5e1..5526aaf2 100644 --- a/src/bdd/cudd/cuddCheck.c +++ b/src/bdd/cudd/cuddCheck.c @@ -7,30 +7,57 @@ 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> - ] + <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.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ @@ -40,6 +67,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -60,7 +88,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.35 2009/03/08 02:49:01 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -74,9 +102,9 @@ static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.1.1.1 2003/02/24 22:23:51 /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static void debugFindParent ARGS((DdManager *table, DdNode *node)); +static void debugFindParent (DdManager *table, DdNode *node); #if 0 -static void debugCheckParent ARGS((DdManager *table, DdNode *node)); +static void debugCheckParent (DdManager *table, DdNode *node); #endif /**AutomaticEnd***************************************************************/ @@ -115,232 +143,233 @@ 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);; + 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) { + index = table->invperm[i]; + if (i != (unsigned) table->perm[index]) { (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++; + "Permutation corrupted: invperm[%u] = %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_int(edgeTable,(char *)cuddT(f),&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_int(edgeTable,(char *)Cudd_Regular(cuddE(f)), + &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); + debugCheckParent(table,f); #endif - } else { - fprintf(table->err, - "Error: node has illegal Then or Else pointers\n"); - cuddPrintNode(f,table->err); + } 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; } - - 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 */ + 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)) { + index = table->invpermZ[i]; + if (i != (unsigned) table->permZ[index]) { (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++; + "Permutation corrupted: invpermZ[%u] = %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_int(edgeTable,(char *)cuddT(f),&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_int(edgeTable,(char *)cuddE(f),&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); + debugCheckParent(table,f); #endif - } else { + } 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: ZDD node has illegal Then or Else pointers\n"); - cuddPrintNode(f,table->err); + "Error: wrong number of total nodes in ZDD\n"); 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 */ + 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; @@ -349,50 +378,50 @@ Cudd_DebugCheck( 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"); + 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)); + fprintf(table->err, + " node 0x%lx, id = %u, ref = %u, value = %g\n", + (ptruint)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)); + fprintf(table->err, + " node 0x%x, id = %hu, ref = %hu, value = %g\n", + (ptruint)f,f->index,f->ref,cuddV(f)); #endif - flag = 1; - } - } else { - deadNode++; + flag = 1; + } + } else { + deadNode++; + } + f = f->next; } - f = f->next; - } } if ((unsigned) totalNode != table->constants.keys) { - (void) fprintf(table->err, - "Error: wrong number of total nodes in constants\n"); - flag = 1; + (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; + (void) fprintf(table->err, + "Error: wrong number of dead nodes in constants\n"); + flag = 1; } gen = st_init_gen(edgeTable); - while (st_gen(gen,(const char **)&f,(char **)&count)) { - if (count > (int)(f->ref) && f->ref != DD_MAXREF) { + while (st_gen(gen, (const 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)); + 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)); #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)); + 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)); #endif - debugFindParent(table,f); - flag = 1; - } + debugFindParent(table,f); + flag = 1; + } } st_free_gen(gen); st_free_table(edgeTable); @@ -449,80 +478,80 @@ Cudd_CheckKeys( 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--; + 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); } - node = node->next; + 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 \ + 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 \ + 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 */ + } + } /* 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; + 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 \ + 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 \ + 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 */ + } + } /* for each ZDD subtable */ /* Check the constant table. */ subtable = &(table->constants); @@ -533,43 +562,43 @@ in ZDD unique table no. %d (difference=%d)\n", i, dead); 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 = nodelist[j]; + if (node != NULL) { + nonEmpty++; + } + while (node != NULL) { + keys--; + if (node->ref == 0) { + dead--; + } + node = node->next; } - node = node->next; - } } if (keys != 0) { - (void) fprintf(table->err, "Wrong number of keys found \ + (void) fprintf(table->err, "Wrong number of keys found \ in the constant table (difference=%d)\n", keys); - count++; + count++; } if (dead != 0) { - (void) fprintf(table->err, "Wrong number of dead found \ + (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); + (void) fprintf(table->err, "Wrong number of total keys found \ +(difference=%d)\n", (int) (totalKeys-table->keys)); } if ((unsigned) totalSlots != table->slots) { - (void) fprintf(table->err, "Wrong number of total slots found \ -(difference=%d)\n", totalSlots-table->slots); + (void) fprintf(table->err, "Wrong number of total slots found \ +(difference=%d)\n", (int) (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)); + (void) fprintf(table->err, "Wrong number of minimum dead found \ +(%u vs. %u)\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) fprintf(table->err, "Wrong number of total dead found \ +(difference=%d)\n", (int) (totalDead-table->dead)); } (void)printf("Average length of non-empty lists = %g\n", (double) table->keys / (double) nonEmpty); @@ -612,51 +641,51 @@ cuddHeapProfile( { 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 */ + 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); + (ptruint) dd); #else retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n", - (unsigned) dd); + (ptruint) 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 = 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; - } + 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); + ntables+1, nonempty, largest); if (retval == EOF) return 0; retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes); if (retval == EOF) return 0; @@ -684,9 +713,9 @@ cuddPrintNode( { 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)); + (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)); #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)); + (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)); #endif } /* end of cuddPrintNode */ @@ -728,32 +757,32 @@ cuddPrintVarGroups( assert(root->younger == NULL || root->younger->elder == root); assert(root->elder == NULL || root->elder->younger == root); if (zdd) { - level = dd->permZ[root->index]; + level = dd->permZ[root->index]; } else { - level = dd->perm[root->index]; + level = dd->perm[root->index]; } if (!silent) (void) printf("(%d",level); if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) { - if (!silent) (void) printf(","); + 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; - } + 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"); + (void) printf("%d", (int) (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; @@ -783,29 +812,29 @@ debugFindParent( DdNode * node) { int i,j; - int slots; - DdNodePtr *nodelist; - DdNode *f; - + 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; + 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) { + 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)); + (void) fprintf(table->out,"parent is at 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)); #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)); + (void) fprintf(table->out,"parent is at 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)); #endif + } + f = f->next; + } } - f = f->next; - } - } } } /* end of debugFindParent */ @@ -830,27 +859,29 @@ debugCheckParent( 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; + int slots; + DdNode **nodelist,*f; - 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; + 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 = %u, ref = %u, 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 = %u, ref = %u, then = 0x%x, else = 0x%x\n",node,node->index,node->ref,cuddT(node),cuddE(node)); + } + f = f->next; + } } } - } } #endif + + ABC_NAMESPACE_IMPL_END |