cuddCheck.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

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


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


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


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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.37 2012/02/05 01:07:18 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;
    int         shift;

    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;
    shift = table->subtables[i].shift;

    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;
            }
                    if (ddHash(cuddT(f),cuddE(f),shift) != j) {
                        (void) fprintf(table->err, "Error: misplaced node\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) fprintf(table->out,"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