src/cuBdd/cuddCheck.c

Go to the documentation of this file.

#include "util.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.35 2009/03/08 02:49:01 fabio Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void debugFindParent (DdManager *table, DdNode *node);
#if 0
static void debugCheckParent (DdManager *table, DdNode *node);
#endif

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


int
Cudd_DebugCheck(
  DdManager * table)
{
    unsigned int i;
    int         j,count;
    int         slots;
    DdNodePtr   *nodelist;
    DdNode      *f;
    DdNode      *sentinel = &(table->sentinel);
    st_table    *edgeTable;     /* stores internal ref count for each node */
    st_generator        *gen;
    int         flag = 0;
    int         totalNode;
    int         deadNode;
    int         index;


    edgeTable = st_init_table(st_ptrcmp,st_ptrhash);
    if (edgeTable == NULL) return(CUDD_OUT_OF_MEM);

    /* Check the BDD/ADD subtables. */
    for (i = 0; i < (unsigned) table->size; i++) {
        index = table->invperm[i];
        if (i != (unsigned) table->perm[index]) {
            (void) fprintf(table->err,
                           "Permutation corrupted: invperm[%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);
#endif
                } else {
                    fprintf(table->err,
                            "Error: node has illegal Then or Else pointers\n");
                    cuddPrintNode(f,table->err);
                    flag = 1;
                }

                f = f->next;
            }   /* for each element of the collision list */
        }       /* for each subtable slot */

        if ((unsigned) totalNode != table->subtables[i].keys) {
            fprintf(table->err,"Error: wrong number of total nodes\n");
            flag = 1;
        }
        if ((unsigned) deadNode != table->subtables[i].dead) {
            fprintf(table->err,"Error: wrong number of dead nodes\n");
            flag = 1;
        }
    }   /* for each BDD/ADD subtable */

    /* Check the ZDD subtables. */
    for (i = 0; i < (unsigned) table->sizeZ; i++) {
        index = table->invpermZ[i];
        if (i != (unsigned) table->permZ[index]) {
            (void) fprintf(table->err,
                           "Permutation corrupted: invpermZ[%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);
#endif
                } else {
                    fprintf(table->err,
                            "Error: ZDD node has illegal Then or Else pointers\n");
                    cuddPrintNode(f,table->err);
                    flag = 1;
                }

                f = f->next;
            }   /* for each element of the collision list */
        }       /* for each subtable slot */

        if ((unsigned) totalNode != table->subtableZ[i].keys) {
            fprintf(table->err,
                    "Error: wrong number of total nodes in ZDD\n");
            flag = 1;
        }
        if ((unsigned) deadNode != table->subtableZ[i].dead) {
            fprintf(table->err,
                    "Error: wrong number of dead nodes in ZDD\n");
            flag = 1;
        }
    }   /* for each ZDD subtable */

    /* Check the constant table. */
    nodelist = table->constants.nodelist;
    slots = table->constants.slots;

    totalNode = 0;
    deadNode = 0;
    for (j = 0; j < slots; j++) {
        f = nodelist[j];
        while (f != NULL) {
            totalNode++;
            if (f->ref != 0) {
                if (f->index != CUDD_CONST_INDEX) {
                    fprintf(table->err,"Error: node has illegal index\n");
#if SIZEOF_VOID_P == 8
                    fprintf(table->err,
                            "       node 0x%lx, id = %u, ref = %u, value = %g\n",
                            (ptruint)f,f->index,f->ref,cuddV(f));
#else
                    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++;
            }
            f = f->next;
        }
    }
    if ((unsigned) totalNode != table->constants.keys) {
        (void) fprintf(table->err,
                       "Error: wrong number of total nodes in constants\n");
        flag = 1;
    }
    if ((unsigned) deadNode != table->constants.dead) {
        (void) fprintf(table->err,
                       "Error: wrong number of dead nodes in constants\n");
        flag = 1;
    }
    gen = st_init_gen(edgeTable);
    while (st_gen(gen, &f, &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 = %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 = %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;
        }
    }
    st_free_gen(gen);
    st_free_table(edgeTable);

    return (flag);

} /* end of Cudd_DebugCheck */


int
Cudd_CheckKeys(
  DdManager * table)
{
    int size;
    int i,j;
    DdNodePtr *nodelist;
    DdNode *node;
    DdNode *sentinel = &(table->sentinel);
    DdSubtable *subtable;
    int keys;
    int dead;
    int count = 0;
    int totalKeys = 0;
    int totalSlots = 0;
    int totalDead = 0;
    int nonEmpty = 0;
    unsigned int slots;
    int logSlots;
    int shift;

    size = table->size;

    for (i = 0; i < size; i++) {
        subtable = &(table->subtables[i]);
        nodelist = subtable->nodelist;
        keys = subtable->keys;
        dead = subtable->dead;
        totalKeys += keys;
        slots = subtable->slots;
        shift = subtable->shift;
        logSlots = sizeof(int) * 8 - shift;
        if (((slots >> logSlots) << logSlots) != slots) {
            (void) fprintf(table->err,
                           "Unique table %d is not the right power of 2\n", i);
            (void) fprintf(table->err,
                           "    slots = %u shift = %d\n", slots, shift);
        }
        totalSlots += slots;
        totalDead += dead;
        for (j = 0; (unsigned) j < slots; j++) {
            node = nodelist[j];
            if (node != sentinel) {
                nonEmpty++;
            }
            while (node != sentinel) {
                keys--;
                if (node->ref == 0) {
                    dead--;
                }
                node = node->next;
            }
        }
        if (keys != 0) {
            (void) fprintf(table->err, "Wrong number of keys found \
in unique table %d (difference=%d)\n", i, keys);
            count++;
        }
        if (dead != 0) {
            (void) fprintf(table->err, "Wrong number of dead found \
in unique table no. %d (difference=%d)\n", i, dead);
        }
    }   /* for each BDD/ADD subtable */

    /* Check the ZDD subtables. */
    size = table->sizeZ;

    for (i = 0; i < size; i++) {
        subtable = &(table->subtableZ[i]);
        nodelist = subtable->nodelist;
        keys = subtable->keys;
        dead = subtable->dead;
        totalKeys += keys;
        totalSlots += subtable->slots;
        totalDead += dead;
        for (j = 0; (unsigned) j < subtable->slots; j++) {
            node = nodelist[j];
            if (node != NULL) {
                nonEmpty++;
            }
            while (node != NULL) {
                keys--;
                if (node->ref == 0) {
                    dead--;
                }
                node = node->next;
            }
        }
        if (keys != 0) {
            (void) fprintf(table->err, "Wrong number of keys found \
in ZDD unique table no. %d (difference=%d)\n", i, keys);
            count++;
        }
        if (dead != 0) {
            (void) fprintf(table->err, "Wrong number of dead found \
in ZDD unique table no. %d (difference=%d)\n", i, dead);
        }
    }   /* for each ZDD subtable */

    /* Check the constant table. */
    subtable = &(table->constants);
    nodelist = subtable->nodelist;
    keys = subtable->keys;
    dead = subtable->dead;
    totalKeys += keys;
    totalSlots += subtable->slots;
    totalDead += dead;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
        node = nodelist[j];
        if (node != NULL) {
            nonEmpty++;
        }
        while (node != NULL) {
            keys--;
            if (node->ref == 0) {
                dead--;
            }
            node = node->next;
        }
    }
    if (keys != 0) {
        (void) fprintf(table->err, "Wrong number of keys found \
in the constant table (difference=%d)\n", keys);
        count++;
    }
    if (dead != 0) {
        (void) fprintf(table->err, "Wrong number of dead found \
in the constant table (difference=%d)\n", dead);
    }
    if ((unsigned) totalKeys != table->keys + table->keysZ) {
        (void) fprintf(table->err, "Wrong number of total keys found \
(difference=%d)\n", (int) (totalKeys-table->keys));
    }
    if ((unsigned) 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 \
(%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", (int) (totalDead-table->dead));
    }
    (void)printf("Average length of non-empty lists = %g\n",
    (double) table->keys / (double) nonEmpty);

    return(count);

} /* end of Cudd_CheckKeys */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


int
cuddHeapProfile(
  DdManager * dd)
{
    int ntables = dd->size;
    DdSubtable *subtables = dd->subtables;
    int i,              /* loop index */
        nodes,          /* live nodes in i-th layer */
        retval,         /* return value of fprintf */
        largest = -1,   /* index of the table with most live nodes */
        maxnodes = -1,  /* maximum number of live nodes in a table */
        nonempty = 0;   /* number of tables with live nodes */

    /* Print header. */
#if SIZEOF_VOID_P == 8
    retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n",
                     (ptruint) dd);
#else
    retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n",
                     (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 = dd->constants.keys - dd->constants.dead;
    if (nodes) {
        nonempty++;
        retval = fprintf(dd->out,"const: %5d nodes\n", nodes);
        if (retval == EOF) return 0;
        if (nodes > maxnodes) {
            maxnodes = nodes;
            largest = CUDD_CONST_INDEX;
        }
    }

    /* Print summary. */
    retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ",
          ntables+1, nonempty, largest);
    if (retval == EOF) return 0;
    retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes);
    if (retval == EOF) return 0;

    return(1);

} /* end of cuddHeapProfile */


void
cuddPrintNode(
  DdNode * f,
  FILE *fp)
{
    f = Cudd_Regular(f);
#if SIZEOF_VOID_P == 8
    (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 = %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 */



void
cuddPrintVarGroups(
  DdManager * dd /* manager */,
  MtrNode * root /* root of the group tree */,
  int zdd /* 0: BDD; 1: ZDD */,
  int silent /* flag to check tree syntax only */)
{
    MtrNode *node;
    int level;

    assert(root != NULL);
    assert(root->younger == NULL || root->younger->elder == root);
    assert(root->elder == NULL || root->elder->younger == root);
    if (zdd) {
        level = dd->permZ[root->index];
    } else {
        level = dd->perm[root->index];
    }
    if (!silent) (void) printf("(%d",level);
    if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
        if (!silent) (void) printf(",");
    } else {
        node = root->child;
        while (node != NULL) {
            assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
            assert(node->parent == root);
            cuddPrintVarGroups(dd,node,zdd,silent);
            node = node->younger;
        }
    }
    if (!silent) {
        (void) printf("%d", (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;

} /* end of cuddPrintVarGroups */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static void
debugFindParent(
  DdManager * table,
  DdNode * node)
{
    int         i,j;
    int         slots;
    DdNodePtr   *nodelist;
    DdNode      *f;

    for (i = 0; i < cuddI(table,node->index); i++) {
        nodelist = table->subtables[i].nodelist;
        slots = table->subtables[i].slots;

        for (j=0;j<slots;j++) {
            f = nodelist[j];
            while (f != NULL) {
                if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) {
#if SIZEOF_VOID_P == 8
                    (void) fprintf(table->out,"parent is at 0x%lx, id = %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 = %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;
            }
        }
    }

} /* end of debugFindParent */


#if 0

static void
debugCheckParent(
  DdManager * table,
  DdNode * node)
{
    int         i,j;
    int         slots;
    DdNode      **nodelist,*f;

    for (i = 0; i < cuddI(table,node->index); i++) {
        nodelist = table->subtables[i].nodelist;
        slots = table->subtables[i].slots;

        for (j=0;j<slots;j++) {
            f = nodelist[j];
            while (f != NULL) {
                if ((Cudd_Regular(cuddE(f)) == node || cuddT(f) == node) && f->ref != 0) {
                    (void) fprintf(table->err,
                                   "error with zero ref count\n");
                    (void) fprintf(table->err,"parent is 0x%x, id = %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

---