Upgrade to the latest CUDD 2.4.2.

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