abc/src/bdd/cudd/cuddCheck.c
/**Function********************************************************************

  Synopsis    [Checks for several conditions that should not occur.]

  Description [Checks for the following conditions:
  <ul>
  <li>Wrong sizes of subtables.
  <li>Wrong number of keys found in unique subtable.
  <li>Wrong number of dead found in unique subtable.
  <li>Wrong number of keys found in the constant table
  <li>Wrong number of dead found in the constant table
  <li>Wrong number of total slots found
  <li>Wrong number of maximum keys found
  <li>Wrong number of total dead found
  </ul>
  Reports the average length of non-empty lists. Returns the number of
  subtables for which the number of keys is wrong.]

  SideEffects [None]

  SeeAlso     [Cudd_DebugCheck]

******************************************************************************/
Function
Synopsis    [Checks for several conditions that should not occur.]

Description [Checks for the following conditions:

Wrong sizes of subtables.
Wrong number of keys found in unique subtable.
Wrong number of dead found in unique subtable.
Wrong number of keys found in the constant table
Wrong number of dead found in the constant table
Wrong number of total slots found
Wrong number of maximum keys found
Wrong number of total dead found

Reports the average length of non-empty lists. Returns the number of
subtables for which the number of keys is wrong.]




Function Synopsis [ Checks for several conditions that should not occur . ] Description [ Checks for the following conditions : Wrong sizes of subtables . Wrong number of keys found in unique subtable . Wrong number of dead found in unique subtable . Wrong number of keys found in the constant table Wrong number of dead found in the constant table Wrong number of total slots found Wrong number of maximum keys found Wrong number of total dead found Reports the average length of non - empty lists . Returns the number of subtables for which the number of keys is wrong . ]
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);
        }
    }   
    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);
        }
    }   
    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);
}
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 , " \n " , i ) ; ( void ) fprintf ( table -> err , " \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 , " \
 \n " , i , keys ) ; count ++ ; } if ( dead != 0 ) { ( void ) fprintf ( table -> err , " \
 \n " , i , dead ) ; } } 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 , " \
 \n " , i , keys ) ; count ++ ; } if ( dead != 0 ) { ( void ) fprintf ( table -> err , " \
 \n " , i , dead ) ; } } 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 , " \
 \n " , keys ) ; count ++ ; } if ( dead != 0 ) { ( void ) fprintf ( table -> err , " \
 \n " , dead ) ; } if ( ( unsigned ) totalKeys != table -> keys + table -> keysZ ) { ( void ) fprintf ( table -> err , " \
 \n " , ( int ) ( totalKeys - table -> keys ) ) ; } if ( ( unsigned ) totalSlots != table -> slots ) { ( void ) fprintf ( table -> err , " \
 \n " , ( int ) ( totalSlots - table -> slots ) ) ; } if ( table -> minDead != ( unsigned ) ( table -> gcFrac * table -> slots ) ) { ( void ) fprintf ( table -> err , " \
 \n " , table -> minDead , ( unsigned ) ( table -> gcFrac * ( double ) table -> slots ) ) ; } if ( ( unsigned ) totalDead != table -> dead + table -> deadZ ) { ( void ) fprintf ( table -> err , " \
 \n " , ( int ) ( totalDead - table -> dead ) ) ; } ( void ) printf ( " \n " , ( double ) table -> keys / ( double ) nonEmpty ) ; return ( count ) ; }
Function
Synopsis    [Checks for several conditions that should not occur.]
Function Synopsis [ Checks for several conditions that should not occur . ]
/* for each BDD/ADD subtable */ /* Check the ZDD subtables. */ /* for each ZDD subtable */ /* Check the constant table. */