summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddCheck.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddCheck.c')
-rw-r--r--src/bdd/cudd/cuddCheck.c881
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-12 12:20:44 +0000