src/cuBdd/cuddCheck.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddCheck.c:

Go to the source code of this file.

Functions

static void debugFindParent (DdManager *table, DdNode *node)
int Cudd_DebugCheck (DdManager *table)
int Cudd_CheckKeys (DdManager *table)
int cuddHeapProfile (DdManager *dd)
void cuddPrintNode (DdNode *f, FILE *fp)
void cuddPrintVarGroups (DdManager *dd, MtrNode *root, int zdd, int silent)

Variables

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

Function Documentation

int Cudd_CheckKeys ( DdManager *  table  ) 

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.]

SideEffects [None]

SeeAlso [Cudd_DebugCheck]

Definition at line 454 of file cuddCheck.c.

00456 {
00457     int size;
00458     int i,j;
00459     DdNodePtr *nodelist;
00460     DdNode *node;
00461     DdNode *sentinel = &(table->sentinel);
00462     DdSubtable *subtable;
00463     int keys;
00464     int dead;
00465     int count = 0;
00466     int totalKeys = 0;
00467     int totalSlots = 0;
00468     int totalDead = 0;
00469     int nonEmpty = 0;
00470     unsigned int slots;
00471     int logSlots;
00472     int shift;
00473 
00474     size = table->size;
00475 
00476     for (i = 0; i < size; i++) {
00477         subtable = &(table->subtables[i]);
00478         nodelist = subtable->nodelist;
00479         keys = subtable->keys;
00480         dead = subtable->dead;
00481         totalKeys += keys;
00482         slots = subtable->slots;
00483         shift = subtable->shift;
00484         logSlots = sizeof(int) * 8 - shift;
00485         if (((slots >> logSlots) << logSlots) != slots) {
00486             (void) fprintf(table->err,
00487                            "Unique table %d is not the right power of 2\n", i);
00488             (void) fprintf(table->err,
00489                            "    slots = %u shift = %d\n", slots, shift);
00490         }
00491         totalSlots += slots;
00492         totalDead += dead;
00493         for (j = 0; (unsigned) j < slots; j++) {
00494             node = nodelist[j];
00495             if (node != sentinel) {
00496                 nonEmpty++;
00497             }
00498             while (node != sentinel) {
00499                 keys--;
00500                 if (node->ref == 0) {
00501                     dead--;
00502                 }
00503                 node = node->next;
00504             }
00505         }
00506         if (keys != 0) {
00507             (void) fprintf(table->err, "Wrong number of keys found \
00508 in unique table %d (difference=%d)\n", i, keys);
00509             count++;
00510         }
00511         if (dead != 0) {
00512             (void) fprintf(table->err, "Wrong number of dead found \
00513 in unique table no. %d (difference=%d)\n", i, dead);
00514         }
00515     }   /* for each BDD/ADD subtable */
00516 
00517     /* Check the ZDD subtables. */
00518     size = table->sizeZ;
00519 
00520     for (i = 0; i < size; i++) {
00521         subtable = &(table->subtableZ[i]);
00522         nodelist = subtable->nodelist;
00523         keys = subtable->keys;
00524         dead = subtable->dead;
00525         totalKeys += keys;
00526         totalSlots += subtable->slots;
00527         totalDead += dead;
00528         for (j = 0; (unsigned) j < subtable->slots; j++) {
00529             node = nodelist[j];
00530             if (node != NULL) {
00531                 nonEmpty++;
00532             }
00533             while (node != NULL) {
00534                 keys--;
00535                 if (node->ref == 0) {
00536                     dead--;
00537                 }
00538                 node = node->next;
00539             }
00540         }
00541         if (keys != 0) {
00542             (void) fprintf(table->err, "Wrong number of keys found \
00543 in ZDD unique table no. %d (difference=%d)\n", i, keys);
00544             count++;
00545         }
00546         if (dead != 0) {
00547             (void) fprintf(table->err, "Wrong number of dead found \
00548 in ZDD unique table no. %d (difference=%d)\n", i, dead);
00549         }
00550     }   /* for each ZDD subtable */
00551 
00552     /* Check the constant table. */
00553     subtable = &(table->constants);
00554     nodelist = subtable->nodelist;
00555     keys = subtable->keys;
00556     dead = subtable->dead;
00557     totalKeys += keys;
00558     totalSlots += subtable->slots;
00559     totalDead += dead;
00560     for (j = 0; (unsigned) j < subtable->slots; j++) {
00561         node = nodelist[j];
00562         if (node != NULL) {
00563             nonEmpty++;
00564         }
00565         while (node != NULL) {
00566             keys--;
00567             if (node->ref == 0) {
00568                 dead--;
00569             }
00570             node = node->next;
00571         }
00572     }
00573     if (keys != 0) {
00574         (void) fprintf(table->err, "Wrong number of keys found \
00575 in the constant table (difference=%d)\n", keys);
00576         count++;
00577     }
00578     if (dead != 0) {
00579         (void) fprintf(table->err, "Wrong number of dead found \
00580 in the constant table (difference=%d)\n", dead);
00581     }
00582     if ((unsigned) totalKeys != table->keys + table->keysZ) {
00583         (void) fprintf(table->err, "Wrong number of total keys found \
00584 (difference=%d)\n", (int) (totalKeys-table->keys));
00585     }
00586     if ((unsigned) totalSlots != table->slots) {
00587         (void) fprintf(table->err, "Wrong number of total slots found \
00588 (difference=%d)\n", (int) (totalSlots-table->slots));
00589     }
00590     if (table->minDead != (unsigned) (table->gcFrac * table->slots)) {
00591         (void) fprintf(table->err, "Wrong number of minimum dead found \
00592 (%u vs. %u)\n", table->minDead,
00593         (unsigned) (table->gcFrac * (double) table->slots));
00594     }
00595     if ((unsigned) totalDead != table->dead + table->deadZ) {
00596         (void) fprintf(table->err, "Wrong number of total dead found \
00597 (difference=%d)\n", (int) (totalDead-table->dead));
00598     }
00599     (void)printf("Average length of non-empty lists = %g\n",
00600     (double) table->keys / (double) nonEmpty);
00601 
00602     return(count);
00603 
00604 } /* end of Cudd_CheckKeys */

int Cudd_DebugCheck ( DdManager *  table  ) 

AutomaticEnd Function********************************************************************

Synopsis [Checks for inconsistencies in the DD heap.]

Description [Checks for inconsistencies in the DD heap:

  • node has illegal index
  • live node has dead children
  • node has illegal Then or Else pointers
  • BDD/ADD node has identical children
  • ZDD node has zero then child
  • wrong number of total nodes
  • wrong number of dead nodes
  • ref count error at node

Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is not enough memory; 1 otherwise.]

SideEffects [None]

SeeAlso [Cudd_CheckKeys]

Definition at line 138 of file cuddCheck.c.

00140 {
00141     unsigned int i;
00142     int         j,count;
00143     int         slots;
00144     DdNodePtr   *nodelist;
00145     DdNode      *f;
00146     DdNode      *sentinel = &(table->sentinel);
00147     st_table    *edgeTable;     /* stores internal ref count for each node */
00148     st_generator        *gen;
00149     int         flag = 0;
00150     int         totalNode;
00151     int         deadNode;
00152     int         index;
00153 
00154 
00155     edgeTable = st_init_table(st_ptrcmp,st_ptrhash);
00156     if (edgeTable == NULL) return(CUDD_OUT_OF_MEM);
00157 
00158     /* Check the BDD/ADD subtables. */
00159     for (i = 0; i < (unsigned) table->size; i++) {
00160         index = table->invperm[i];
00161         if (i != (unsigned) table->perm[index]) {
00162             (void) fprintf(table->err,
00163                            "Permutation corrupted: invperm[%u] = %d\t perm[%d] = %d\n",
00164                            i, index, index, table->perm[index]);
00165         }
00166         nodelist = table->subtables[i].nodelist;
00167         slots = table->subtables[i].slots;
00168 
00169         totalNode = 0;
00170         deadNode = 0;
00171         for (j = 0; j < slots; j++) {   /* for each subtable slot */
00172             f = nodelist[j];
00173             while (f != sentinel) {
00174                 totalNode++;
00175                 if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
00176                     if ((int) f->index != index) {
00177                         (void) fprintf(table->err,
00178                                        "Error: node has illegal index\n");
00179                         cuddPrintNode(f,table->err);
00180                         flag = 1;
00181                     }
00182                     if ((unsigned) cuddI(table,cuddT(f)->index) <= i ||
00183                         (unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index)
00184                         <= i) {
00185                         (void) fprintf(table->err,
00186                                        "Error: node has illegal children\n");
00187                         cuddPrintNode(f,table->err);
00188                         flag = 1;
00189                     }
00190                     if (Cudd_Regular(cuddT(f)) != cuddT(f)) {
00191                         (void) fprintf(table->err,
00192                                        "Error: node has illegal form\n");
00193                         cuddPrintNode(f,table->err);
00194                         flag = 1;
00195                     }
00196                     if (cuddT(f) == cuddE(f)) {
00197                         (void) fprintf(table->err,
00198                                        "Error: node has identical children\n");
00199                         cuddPrintNode(f,table->err);
00200                         flag = 1;
00201                     }
00202                     if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) {
00203                         (void) fprintf(table->err,
00204                                        "Error: live node has dead children\n");
00205                         cuddPrintNode(f,table->err);
00206                         flag =1;
00207                     }
00208                     /* Increment the internal reference count for the
00209                     ** then child of the current node.
00210                     */
00211                     if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
00212                         count++;
00213                     } else {
00214                         count = 1;
00215                     }
00216                     if (st_insert(edgeTable,(char *)cuddT(f),
00217                     (char *)(long)count) == ST_OUT_OF_MEM) {
00218                         st_free_table(edgeTable);
00219                         return(CUDD_OUT_OF_MEM);
00220                     }
00221 
00222                     /* Increment the internal reference count for the
00223                     ** else child of the current node.
00224                     */
00225                     if (st_lookup_int(edgeTable,(char *)Cudd_Regular(cuddE(f)),
00226                                       &count)) {
00227                         count++;
00228                     } else {
00229                         count = 1;
00230                     }
00231                     if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
00232                     (char *)(long)count) == ST_OUT_OF_MEM) {
00233                         st_free_table(edgeTable);
00234                         return(CUDD_OUT_OF_MEM);
00235                     }
00236                 } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
00237                     deadNode++;
00238 #if 0
00239                     debugCheckParent(table,f);
00240 #endif
00241                 } else {
00242                     fprintf(table->err,
00243                             "Error: node has illegal Then or Else pointers\n");
00244                     cuddPrintNode(f,table->err);
00245                     flag = 1;
00246                 }
00247 
00248                 f = f->next;
00249             }   /* for each element of the collision list */
00250         }       /* for each subtable slot */
00251 
00252         if ((unsigned) totalNode != table->subtables[i].keys) {
00253             fprintf(table->err,"Error: wrong number of total nodes\n");
00254             flag = 1;
00255         }
00256         if ((unsigned) deadNode != table->subtables[i].dead) {
00257             fprintf(table->err,"Error: wrong number of dead nodes\n");
00258             flag = 1;
00259         }
00260     }   /* for each BDD/ADD subtable */
00261 
00262     /* Check the ZDD subtables. */
00263     for (i = 0; i < (unsigned) table->sizeZ; i++) {
00264         index = table->invpermZ[i];
00265         if (i != (unsigned) table->permZ[index]) {
00266             (void) fprintf(table->err,
00267                            "Permutation corrupted: invpermZ[%u] = %d\t permZ[%d] = %d in ZDD\n",
00268                            i, index, index, table->permZ[index]);
00269         }
00270         nodelist = table->subtableZ[i].nodelist;
00271         slots = table->subtableZ[i].slots;
00272 
00273         totalNode = 0;
00274         deadNode = 0;
00275         for (j = 0; j < slots; j++) {   /* for each subtable slot */
00276             f = nodelist[j];
00277             while (f != NULL) {
00278                 totalNode++;
00279                 if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
00280                     if ((int) f->index != index) {
00281                         (void) fprintf(table->err,
00282                                        "Error: ZDD node has illegal index\n");
00283                         cuddPrintNode(f,table->err);
00284                         flag = 1;
00285                     }
00286                     if (Cudd_IsComplement(cuddT(f)) ||
00287                         Cudd_IsComplement(cuddE(f))) {
00288                         (void) fprintf(table->err,
00289                                        "Error: ZDD node has complemented children\n");
00290                         cuddPrintNode(f,table->err);
00291                         flag = 1;
00292                     }
00293                     if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i ||
00294                     (unsigned) cuddIZ(table,cuddE(f)->index) <= i) {
00295                         (void) fprintf(table->err,
00296                                        "Error: ZDD node has illegal children\n");
00297                         cuddPrintNode(f,table->err);
00298                         cuddPrintNode(cuddT(f),table->err);
00299                         cuddPrintNode(cuddE(f),table->err);
00300                         flag = 1;
00301                     }
00302                     if (cuddT(f) == DD_ZERO(table)) {
00303                         (void) fprintf(table->err,
00304                                        "Error: ZDD node has zero then child\n");
00305                         cuddPrintNode(f,table->err);
00306                         flag = 1;
00307                     }
00308                     if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) {
00309                         (void) fprintf(table->err,
00310                                        "Error: ZDD live node has dead children\n");
00311                         cuddPrintNode(f,table->err);
00312                         flag =1;
00313                     }
00314                     /* Increment the internal reference count for the
00315                     ** then child of the current node.
00316                     */
00317                     if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
00318                         count++;
00319                     } else {
00320                         count = 1;
00321                     }
00322                     if (st_insert(edgeTable,(char *)cuddT(f),
00323                     (char *)(long)count) == ST_OUT_OF_MEM) {
00324                         st_free_table(edgeTable);
00325                         return(CUDD_OUT_OF_MEM);
00326                     }
00327 
00328                     /* Increment the internal reference count for the
00329                     ** else child of the current node.
00330                     */
00331                     if (st_lookup_int(edgeTable,(char *)cuddE(f),&count)) {
00332                         count++;
00333                     } else {
00334                         count = 1;
00335                     }
00336                     if (st_insert(edgeTable,(char *)cuddE(f),
00337                     (char *)(long)count) == ST_OUT_OF_MEM) {
00338                         st_free_table(edgeTable);
00339                         table->errorCode = CUDD_MEMORY_OUT;
00340                         return(CUDD_OUT_OF_MEM);
00341                     }
00342                 } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
00343                     deadNode++;
00344 #if 0
00345                     debugCheckParent(table,f);
00346 #endif
00347                 } else {
00348                     fprintf(table->err,
00349                             "Error: ZDD node has illegal Then or Else pointers\n");
00350                     cuddPrintNode(f,table->err);
00351                     flag = 1;
00352                 }
00353 
00354                 f = f->next;
00355             }   /* for each element of the collision list */
00356         }       /* for each subtable slot */
00357 
00358         if ((unsigned) totalNode != table->subtableZ[i].keys) {
00359             fprintf(table->err,
00360                     "Error: wrong number of total nodes in ZDD\n");
00361             flag = 1;
00362         }
00363         if ((unsigned) deadNode != table->subtableZ[i].dead) {
00364             fprintf(table->err,
00365                     "Error: wrong number of dead nodes in ZDD\n");
00366             flag = 1;
00367         }
00368     }   /* for each ZDD subtable */
00369 
00370     /* Check the constant table. */
00371     nodelist = table->constants.nodelist;
00372     slots = table->constants.slots;
00373 
00374     totalNode = 0;
00375     deadNode = 0;
00376     for (j = 0; j < slots; j++) {
00377         f = nodelist[j];
00378         while (f != NULL) {
00379             totalNode++;
00380             if (f->ref != 0) {
00381                 if (f->index != CUDD_CONST_INDEX) {
00382                     fprintf(table->err,"Error: node has illegal index\n");
00383 #if SIZEOF_VOID_P == 8
00384                     fprintf(table->err,
00385                             "       node 0x%lx, id = %u, ref = %u, value = %g\n",
00386                             (ptruint)f,f->index,f->ref,cuddV(f));
00387 #else
00388                     fprintf(table->err,
00389                             "       node 0x%x, id = %hu, ref = %hu, value = %g\n",
00390                             (ptruint)f,f->index,f->ref,cuddV(f));
00391 #endif
00392                     flag = 1;
00393                 }
00394             } else {
00395                 deadNode++;
00396             }
00397             f = f->next;
00398         }
00399     }
00400     if ((unsigned) totalNode != table->constants.keys) {
00401         (void) fprintf(table->err,
00402                        "Error: wrong number of total nodes in constants\n");
00403         flag = 1;
00404     }
00405     if ((unsigned) deadNode != table->constants.dead) {
00406         (void) fprintf(table->err,
00407                        "Error: wrong number of dead nodes in constants\n");
00408         flag = 1;
00409     }
00410     gen = st_init_gen(edgeTable);
00411     while (st_gen(gen, &f, &count)) {
00412         if (count > (int)(f->ref) && f->ref != DD_MAXREF) {
00413 #if SIZEOF_VOID_P == 8
00414             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));
00415 #else
00416             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));
00417 #endif
00418             debugFindParent(table,f);
00419             flag = 1;
00420         }
00421     }
00422     st_free_gen(gen);
00423     st_free_table(edgeTable);
00424 
00425     return (flag);
00426 
00427 } /* end of Cudd_DebugCheck */

int cuddHeapProfile ( DdManager *  dd  ) 

Function********************************************************************

Synopsis [Prints information about the heap.]

Description [Prints to the manager's stdout the number of live nodes for each level of the DD heap that contains at least one live node. It also prints a summary containing:

  • total number of tables;
  • number of tables with live nodes;
  • table with the largest number of live nodes;
  • number of nodes in that table.

If more than one table contains the maximum number of live nodes, only the one of lowest index is reported. Returns 1 in case of success and 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 635 of file cuddCheck.c.

00637 {
00638     int ntables = dd->size;
00639     DdSubtable *subtables = dd->subtables;
00640     int i,              /* loop index */
00641         nodes,          /* live nodes in i-th layer */
00642         retval,         /* return value of fprintf */
00643         largest = -1,   /* index of the table with most live nodes */
00644         maxnodes = -1,  /* maximum number of live nodes in a table */
00645         nonempty = 0;   /* number of tables with live nodes */
00646 
00647     /* Print header. */
00648 #if SIZEOF_VOID_P == 8
00649     retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n",
00650                      (ptruint) dd);
00651 #else
00652     retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n",
00653                      (ptruint) dd);
00654 #endif
00655     if (retval == EOF) return 0;
00656 
00657     /* Print number of live nodes for each nonempty table. */
00658     for (i=0; i<ntables; i++) {
00659         nodes = subtables[i].keys - subtables[i].dead;
00660         if (nodes) {
00661             nonempty++;
00662             retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes);
00663             if (retval == EOF) return 0;
00664             if (nodes > maxnodes) {
00665                 maxnodes = nodes;
00666                 largest = i;
00667             }
00668         }
00669     }
00670 
00671     nodes = dd->constants.keys - dd->constants.dead;
00672     if (nodes) {
00673         nonempty++;
00674         retval = fprintf(dd->out,"const: %5d nodes\n", nodes);
00675         if (retval == EOF) return 0;
00676         if (nodes > maxnodes) {
00677             maxnodes = nodes;
00678             largest = CUDD_CONST_INDEX;
00679         }
00680     }
00681 
00682     /* Print summary. */
00683     retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ",
00684           ntables+1, nonempty, largest);
00685     if (retval == EOF) return 0;
00686     retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes);
00687     if (retval == EOF) return 0;
00688 
00689     return(1);
00690 
00691 } /* end of cuddHeapProfile */

void cuddPrintNode ( DdNode *  f,
FILE *  fp 
)

Function********************************************************************

Synopsis [Prints out information on a node.]

Description [Prints out information on a node.]

SideEffects [None]

SeeAlso []

Definition at line 706 of file cuddCheck.c.

00709 {
00710     f = Cudd_Regular(f);
00711 #if SIZEOF_VOID_P == 8
00712     (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));
00713 #else
00714     (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));
00715 #endif
00716 
00717 } /* end of cuddPrintNode */

void cuddPrintVarGroups ( DdManager *  dd,
MtrNode *  root,
int  zdd,
int  silent 
)

Function********************************************************************

Synopsis [Prints the variable groups as a parenthesized list.]

Description [Prints the variable groups as a parenthesized list. For each group the level range that it represents is printed. After each group, the group's flags are printed, preceded by a `|'. For each flag (except MTR_TERMINAL) a character is printed.

  • F: MTR_FIXED
  • N: MTR_NEWNODE
  • S: MTR_SOFT

The second argument, silent, if different from 0, causes Cudd_PrintVarGroups to only check the syntax of the group tree.]

SideEffects [None]

SeeAlso []

Definition at line 743 of file cuddCheck.c.

00746               : BDD; 1: ZDD */,
00747   int silent /* flag to check tree syntax only */)
00748 {
00749     MtrNode *node;
00750     int level;
00751 
00752     assert(root != NULL);
00753     assert(root->younger == NULL || root->younger->elder == root);
00754     assert(root->elder == NULL || root->elder->younger == root);
00755     if (zdd) {
00756         level = dd->permZ[root->index];
00757     } else {
00758         level = dd->perm[root->index];
00759     }
00760     if (!silent) (void) printf("(%d",level);
00761     if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
00762         if (!silent) (void) printf(",");
00763     } else {
00764         node = root->child;
00765         while (node != NULL) {
00766             assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
00767             assert(node->parent == root);
00768             cuddPrintVarGroups(dd,node,zdd,silent);
00769             node = node->younger;
00770         }
00771     }
00772     if (!silent) {
00773         (void) printf("%d", (int) (level + root->size - 1));
00774         if (root->flags != MTR_DEFAULT) {
00775             (void) printf("|");
00776             if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
00777             if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
00778             if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
00779         }
00780         (void) printf(")");
00781         if (root->parent == NULL) (void) printf("\n");
00782     }
00783     assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
00784     return;
00785 
00786 } /* end of cuddPrintVarGroups */

static void debugFindParent ( DdManager *  table,
DdNode *  node 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [Searches the subtables above node for its parents.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 806 of file cuddCheck.c.

00809 {
00810     int         i,j;
00811     int         slots;
00812     DdNodePtr   *nodelist;
00813     DdNode      *f;
00814 
00815     for (i = 0; i < cuddI(table,node->index); i++) {
00816         nodelist = table->subtables[i].nodelist;
00817         slots = table->subtables[i].slots;
00818 
00819         for (j=0;j<slots;j++) {
00820             f = nodelist[j];
00821             while (f != NULL) {
00822                 if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) {
00823 #if SIZEOF_VOID_P == 8
00824                     (void) fprintf(table->out,"parent is at 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",
00825                         (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
00826 #else
00827                     (void) fprintf(table->out,"parent is at 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",
00828                         (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
00829 #endif
00830                 }
00831                 f = f->next;
00832             }
00833         }
00834     }
00835 
00836 } /* end of debugFindParent */

Variable Documentation

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

CFile***********************************************************************

FileName [cuddCheck.c]

PackageName [cudd]

Synopsis [Functions to check consistency of data structures.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso []

Author [Fabio Somenzi]

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.]

Definition at line 87 of file cuddCheck.c.

Generated on Tue Jan 12 13:57:18 2010 for glu-2.2 by  doxygen 1.6.1