SVF
Functions | Variables
cuddCheck.c File Reference
#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

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.37 2012/02/05 01:07:18 fabio Exp $"
 

Function Documentation

◆ Cudd_CheckKeys()

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 460 of file cuddCheck.c.

462 {
463  int size;
464  int i,j;
465  DdNodePtr *nodelist;
466  DdNode *node;
467  DdNode *sentinel = &(table->sentinel);
468  DdSubtable *subtable;
469  int keys;
470  int dead;
471  int count = 0;
472  int totalKeys = 0;
473  int totalSlots = 0;
474  int totalDead = 0;
475  int nonEmpty = 0;
476  unsigned int slots;
477  int logSlots;
478  int shift;
479 
480  size = table->size;
481 
482  for (i = 0; i < size; i++) {
483  subtable = &(table->subtables[i]);
484  nodelist = subtable->nodelist;
485  keys = subtable->keys;
486  dead = subtable->dead;
487  totalKeys += keys;
488  slots = subtable->slots;
489  shift = subtable->shift;
490  logSlots = sizeof(int) * 8 - shift;
491  if (((slots >> logSlots) << logSlots) != slots) {
492  (void) fprintf(table->err,
493  "Unique table %d is not the right power of 2\n", i);
494  (void) fprintf(table->err,
495  " slots = %u shift = %d\n", slots, shift);
496  }
497  totalSlots += slots;
498  totalDead += dead;
499  for (j = 0; (unsigned) j < slots; j++) {
500  node = nodelist[j];
501  if (node != sentinel) {
502  nonEmpty++;
503  }
504  while (node != sentinel) {
505  keys--;
506  if (node->ref == 0) {
507  dead--;
508  }
509  node = node->next;
510  }
511  }
512  if (keys != 0) {
513  (void) fprintf(table->err, "Wrong number of keys found \
514 in unique table %d (difference=%d)\n", i, keys);
515  count++;
516  }
517  if (dead != 0) {
518  (void) fprintf(table->err, "Wrong number of dead found \
519 in unique table no. %d (difference=%d)\n", i, dead);
520  }
521  } /* for each BDD/ADD subtable */
522 
523  /* Check the ZDD subtables. */
524  size = table->sizeZ;
525 
526  for (i = 0; i < size; i++) {
527  subtable = &(table->subtableZ[i]);
528  nodelist = subtable->nodelist;
529  keys = subtable->keys;
530  dead = subtable->dead;
531  totalKeys += keys;
532  totalSlots += subtable->slots;
533  totalDead += dead;
534  for (j = 0; (unsigned) j < subtable->slots; j++) {
535  node = nodelist[j];
536  if (node != NULL) {
537  nonEmpty++;
538  }
539  while (node != NULL) {
540  keys--;
541  if (node->ref == 0) {
542  dead--;
543  }
544  node = node->next;
545  }
546  }
547  if (keys != 0) {
548  (void) fprintf(table->err, "Wrong number of keys found \
549 in ZDD unique table no. %d (difference=%d)\n", i, keys);
550  count++;
551  }
552  if (dead != 0) {
553  (void) fprintf(table->err, "Wrong number of dead found \
554 in ZDD unique table no. %d (difference=%d)\n", i, dead);
555  }
556  } /* for each ZDD subtable */
557 
558  /* Check the constant table. */
559  subtable = &(table->constants);
560  nodelist = subtable->nodelist;
561  keys = subtable->keys;
562  dead = subtable->dead;
563  totalKeys += keys;
564  totalSlots += subtable->slots;
565  totalDead += dead;
566  for (j = 0; (unsigned) j < subtable->slots; j++) {
567  node = nodelist[j];
568  if (node != NULL) {
569  nonEmpty++;
570  }
571  while (node != NULL) {
572  keys--;
573  if (node->ref == 0) {
574  dead--;
575  }
576  node = node->next;
577  }
578  }
579  if (keys != 0) {
580  (void) fprintf(table->err, "Wrong number of keys found \
581 in the constant table (difference=%d)\n", keys);
582  count++;
583  }
584  if (dead != 0) {
585  (void) fprintf(table->err, "Wrong number of dead found \
586 in the constant table (difference=%d)\n", dead);
587  }
588  if ((unsigned) totalKeys != table->keys + table->keysZ) {
589  (void) fprintf(table->err, "Wrong number of total keys found \
590 (difference=%d)\n", (int) (totalKeys-table->keys));
591  }
592  if ((unsigned) totalSlots != table->slots) {
593  (void) fprintf(table->err, "Wrong number of total slots found \
594 (difference=%d)\n", (int) (totalSlots-table->slots));
595  }
596  if (table->minDead != (unsigned) (table->gcFrac * table->slots)) {
597  (void) fprintf(table->err, "Wrong number of minimum dead found \
598 (%u vs. %u)\n", table->minDead,
599  (unsigned) (table->gcFrac * (double) table->slots));
600  }
601  if ((unsigned) totalDead != table->dead + table->deadZ) {
602  (void) fprintf(table->err, "Wrong number of total dead found \
603 (difference=%d)\n", (int) (totalDead-table->dead));
604  }
605  (void) fprintf(table->out,"Average length of non-empty lists = %g\n",
606  (double) table->keys / (double) nonEmpty);
607 
608  return(count);
609 
610 } /* end of Cudd_CheckKeys */
DdHalfWord ref
Definition: cudd.h:272
unsigned int keys
Definition: cuddInt.h:314
Definition: cudd.h:270
unsigned int deadZ
Definition: cuddInt.h:356
int size
Definition: cuddInt.h:345
double gcFrac
Definition: cuddInt.h:359
unsigned int slots
Definition: cuddInt.h:352
FILE * err
Definition: cuddInt.h:424
DdSubtable * subtables
Definition: cuddInt.h:349
unsigned int dead
Definition: cuddInt.h:355
DdNode sentinel
Definition: cuddInt.h:328
unsigned int keys
Definition: cuddInt.h:353
unsigned int dead
Definition: cuddInt.h:316
FILE * out
Definition: cuddInt.h:423
DdNode * next
Definition: cudd.h:273
DdNode ** nodelist
Definition: cuddInt.h:311
int sizeZ
Definition: cuddInt.h:346
unsigned int slots
Definition: cuddInt.h:313
DdSubtable constants
Definition: cuddInt.h:351
int shift
Definition: cuddInt.h:312
unsigned int keysZ
Definition: cuddInt.h:354
unsigned int minDead
Definition: cuddInt.h:358
DdSubtable * subtableZ
Definition: cuddInt.h:350

◆ Cudd_DebugCheck()

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.

140 {
141  unsigned int i;
142  int j,count;
143  int slots;
144  DdNodePtr *nodelist;
145  DdNode *f;
146  DdNode *sentinel = &(table->sentinel);
147  st_table *edgeTable; /* stores internal ref count for each node */
148  st_generator *gen;
149  int flag = 0;
150  int totalNode;
151  int deadNode;
152  int index;
153  int shift;
154 
155  edgeTable = st_init_table(st_ptrcmp,st_ptrhash);
156  if (edgeTable == NULL) return(CUDD_OUT_OF_MEM);
157 
158  /* Check the BDD/ADD subtables. */
159  for (i = 0; i < (unsigned) table->size; i++) {
160  index = table->invperm[i];
161  if (i != (unsigned) table->perm[index]) {
162  (void) fprintf(table->err,
163  "Permutation corrupted: invperm[%u] = %d\t perm[%d] = %d\n",
164  i, index, index, table->perm[index]);
165  }
166  nodelist = table->subtables[i].nodelist;
167  slots = table->subtables[i].slots;
168  shift = table->subtables[i].shift;
169 
170  totalNode = 0;
171  deadNode = 0;
172  for (j = 0; j < slots; j++) { /* for each subtable slot */
173  f = nodelist[j];
174  while (f != sentinel) {
175  totalNode++;
176  if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
177  if ((int) f->index != index) {
178  (void) fprintf(table->err,
179  "Error: node has illegal index\n");
180  cuddPrintNode(f,table->err);
181  flag = 1;
182  }
183  if ((unsigned) cuddI(table,cuddT(f)->index) <= i ||
184  (unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index)
185  <= i) {
186  (void) fprintf(table->err,
187  "Error: node has illegal children\n");
188  cuddPrintNode(f,table->err);
189  flag = 1;
190  }
191  if (Cudd_Regular(cuddT(f)) != cuddT(f)) {
192  (void) fprintf(table->err,
193  "Error: node has illegal form\n");
194  cuddPrintNode(f,table->err);
195  flag = 1;
196  }
197  if (cuddT(f) == cuddE(f)) {
198  (void) fprintf(table->err,
199  "Error: node has identical children\n");
200  cuddPrintNode(f,table->err);
201  flag = 1;
202  }
203  if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) {
204  (void) fprintf(table->err,
205  "Error: live node has dead children\n");
206  cuddPrintNode(f,table->err);
207  flag =1;
208  }
209  if (ddHash(cuddT(f),cuddE(f),shift) != j) {
210  (void) fprintf(table->err, "Error: misplaced node\n");
211  cuddPrintNode(f,table->err);
212  flag =1;
213  }
214  /* Increment the internal reference count for the
215  ** then child of the current node.
216  */
217  if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
218  count++;
219  } else {
220  count = 1;
221  }
222  if (st_insert(edgeTable,(char *)cuddT(f),
223  (char *)(long)count) == ST_OUT_OF_MEM) {
224  st_free_table(edgeTable);
225  return(CUDD_OUT_OF_MEM);
226  }
227 
228  /* Increment the internal reference count for the
229  ** else child of the current node.
230  */
231  if (st_lookup_int(edgeTable,(char *)Cudd_Regular(cuddE(f)),
232  &count)) {
233  count++;
234  } else {
235  count = 1;
236  }
237  if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
238  (char *)(long)count) == ST_OUT_OF_MEM) {
239  st_free_table(edgeTable);
240  return(CUDD_OUT_OF_MEM);
241  }
242  } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
243  deadNode++;
244 #if 0
245  debugCheckParent(table,f);
246 #endif
247  } else {
248  fprintf(table->err,
249  "Error: node has illegal Then or Else pointers\n");
250  cuddPrintNode(f,table->err);
251  flag = 1;
252  }
253 
254  f = f->next;
255  } /* for each element of the collision list */
256  } /* for each subtable slot */
257 
258  if ((unsigned) totalNode != table->subtables[i].keys) {
259  fprintf(table->err,"Error: wrong number of total nodes\n");
260  flag = 1;
261  }
262  if ((unsigned) deadNode != table->subtables[i].dead) {
263  fprintf(table->err,"Error: wrong number of dead nodes\n");
264  flag = 1;
265  }
266  } /* for each BDD/ADD subtable */
267 
268  /* Check the ZDD subtables. */
269  for (i = 0; i < (unsigned) table->sizeZ; i++) {
270  index = table->invpermZ[i];
271  if (i != (unsigned) table->permZ[index]) {
272  (void) fprintf(table->err,
273  "Permutation corrupted: invpermZ[%u] = %d\t permZ[%d] = %d in ZDD\n",
274  i, index, index, table->permZ[index]);
275  }
276  nodelist = table->subtableZ[i].nodelist;
277  slots = table->subtableZ[i].slots;
278 
279  totalNode = 0;
280  deadNode = 0;
281  for (j = 0; j < slots; j++) { /* for each subtable slot */
282  f = nodelist[j];
283  while (f != NULL) {
284  totalNode++;
285  if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
286  if ((int) f->index != index) {
287  (void) fprintf(table->err,
288  "Error: ZDD node has illegal index\n");
289  cuddPrintNode(f,table->err);
290  flag = 1;
291  }
292  if (Cudd_IsComplement(cuddT(f)) ||
293  Cudd_IsComplement(cuddE(f))) {
294  (void) fprintf(table->err,
295  "Error: ZDD node has complemented children\n");
296  cuddPrintNode(f,table->err);
297  flag = 1;
298  }
299  if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i ||
300  (unsigned) cuddIZ(table,cuddE(f)->index) <= i) {
301  (void) fprintf(table->err,
302  "Error: ZDD node has illegal children\n");
303  cuddPrintNode(f,table->err);
304  cuddPrintNode(cuddT(f),table->err);
305  cuddPrintNode(cuddE(f),table->err);
306  flag = 1;
307  }
308  if (cuddT(f) == DD_ZERO(table)) {
309  (void) fprintf(table->err,
310  "Error: ZDD node has zero then child\n");
311  cuddPrintNode(f,table->err);
312  flag = 1;
313  }
314  if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) {
315  (void) fprintf(table->err,
316  "Error: ZDD live node has dead children\n");
317  cuddPrintNode(f,table->err);
318  flag =1;
319  }
320  /* Increment the internal reference count for the
321  ** then child of the current node.
322  */
323  if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
324  count++;
325  } else {
326  count = 1;
327  }
328  if (st_insert(edgeTable,(char *)cuddT(f),
329  (char *)(long)count) == ST_OUT_OF_MEM) {
330  st_free_table(edgeTable);
331  return(CUDD_OUT_OF_MEM);
332  }
333 
334  /* Increment the internal reference count for the
335  ** else child of the current node.
336  */
337  if (st_lookup_int(edgeTable,(char *)cuddE(f),&count)) {
338  count++;
339  } else {
340  count = 1;
341  }
342  if (st_insert(edgeTable,(char *)cuddE(f),
343  (char *)(long)count) == ST_OUT_OF_MEM) {
344  st_free_table(edgeTable);
345  table->errorCode = CUDD_MEMORY_OUT;
346  return(CUDD_OUT_OF_MEM);
347  }
348  } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
349  deadNode++;
350 #if 0
351  debugCheckParent(table,f);
352 #endif
353  } else {
354  fprintf(table->err,
355  "Error: ZDD node has illegal Then or Else pointers\n");
356  cuddPrintNode(f,table->err);
357  flag = 1;
358  }
359 
360  f = f->next;
361  } /* for each element of the collision list */
362  } /* for each subtable slot */
363 
364  if ((unsigned) totalNode != table->subtableZ[i].keys) {
365  fprintf(table->err,
366  "Error: wrong number of total nodes in ZDD\n");
367  flag = 1;
368  }
369  if ((unsigned) deadNode != table->subtableZ[i].dead) {
370  fprintf(table->err,
371  "Error: wrong number of dead nodes in ZDD\n");
372  flag = 1;
373  }
374  } /* for each ZDD subtable */
375 
376  /* Check the constant table. */
377  nodelist = table->constants.nodelist;
378  slots = table->constants.slots;
379 
380  totalNode = 0;
381  deadNode = 0;
382  for (j = 0; j < slots; j++) {
383  f = nodelist[j];
384  while (f != NULL) {
385  totalNode++;
386  if (f->ref != 0) {
387  if (f->index != CUDD_CONST_INDEX) {
388  fprintf(table->err,"Error: node has illegal index\n");
389 #if SIZEOF_VOID_P == 8
390  fprintf(table->err,
391  " node 0x%lx, id = %u, ref = %u, value = %g\n",
392  (ptruint)f,f->index,f->ref,cuddV(f));
393 #else
394  fprintf(table->err,
395  " node 0x%x, id = %hu, ref = %hu, value = %g\n",
396  (ptruint)f,f->index,f->ref,cuddV(f));
397 #endif
398  flag = 1;
399  }
400  } else {
401  deadNode++;
402  }
403  f = f->next;
404  }
405  }
406  if ((unsigned) totalNode != table->constants.keys) {
407  (void) fprintf(table->err,
408  "Error: wrong number of total nodes in constants\n");
409  flag = 1;
410  }
411  if ((unsigned) deadNode != table->constants.dead) {
412  (void) fprintf(table->err,
413  "Error: wrong number of dead nodes in constants\n");
414  flag = 1;
415  }
416  gen = st_init_gen(edgeTable);
417  while (st_gen(gen, &f, &count)) {
418  if (count > (int)(f->ref) && f->ref != DD_MAXREF) {
419 #if SIZEOF_VOID_P == 8
420  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));
421 #else
422  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));
423 #endif
424  debugFindParent(table,f);
425  flag = 1;
426  }
427  }
428  st_free_gen(gen);
429  st_free_table(edgeTable);
430 
431  return (flag);
432 
433 } /* end of Cudd_DebugCheck */
DdHalfWord ref
Definition: cudd.h:272
#define DD_MAXREF
Definition: cuddInt.h:101
unsigned int keys
Definition: cuddInt.h:314
#define CUDD_OUT_OF_MEM
Definition: cudd.h:91
#define ddHash(f, g, s)
Definition: cuddInt.h:696
Definition: st.h:60
#define cuddIZ(dd, index)
Definition: cuddInt.h:677
int st_lookup_int(st_table *, void *, int *)
Definition: st.c:322
Definition: cudd.h:270
void st_free_gen(st_generator *)
Definition: st.c:994
int * invpermZ
Definition: cuddInt.h:372
static void debugFindParent(DdManager *table, DdNode *node)
Definition: cuddCheck.c:812
int size
Definition: cuddInt.h:345
void st_free_table(st_table *)
Definition: st.c:252
#define Cudd_Regular(node)
Definition: cudd.h:384
int st_gen(st_generator *, void *, void *)
Definition: st.c:908
FILE * err
Definition: cuddInt.h:424
st_generator * st_init_gen(st_table *)
Definition: st.c:870
DdSubtable * subtables
Definition: cuddInt.h:349
int * permZ
Definition: cuddInt.h:370
#define cuddV(node)
Definition: cuddInt.h:641
int st_insert(st_table *, void *, void *)
Definition: st.c:358
#define Cudd_IsComplement(node)
Definition: cudd.h:412
DdNode sentinel
Definition: cuddInt.h:328
void cuddPrintNode(DdNode *f, FILE *fp)
Definition: cuddCheck.c:712
unsigned int dead
Definition: cuddInt.h:316
DdNode * next
Definition: cudd.h:273
#define CUDD_CONST_INDEX
Definition: cudd.h:113
DdNode ** nodelist
Definition: cuddInt.h:311
int st_ptrcmp(const char *, const char *)
Definition: st.c:849
#define cuddT(node)
Definition: cuddInt.h:609
st_table * st_init_table(ST_PFICPCP, ST_PFICPI)
Definition: st.c:163
#define ST_OUT_OF_MEM
Definition: st.h:41
#define cuddI(dd, index)
Definition: cuddInt.h:659
unsigned int ptruint
Definition: cuddInt.h:250
int sizeZ
Definition: cuddInt.h:346
DdHalfWord index
Definition: cudd.h:271
unsigned int slots
Definition: cuddInt.h:313
#define cuddE(node)
Definition: cuddInt.h:625
int st_ptrhash(char *, int)
Definition: st.c:811
int * invperm
Definition: cuddInt.h:371
DdSubtable constants
Definition: cuddInt.h:351
int shift
Definition: cuddInt.h:312
int * perm
Definition: cuddInt.h:369
Cudd_ErrorType errorCode
Definition: cuddInt.h:425
DdSubtable * subtableZ
Definition: cuddInt.h:350
#define DD_ZERO(dd)
Definition: cuddInt.h:880

◆ cuddHeapProfile()

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 641 of file cuddCheck.c.

643 {
644  int ntables = dd->size;
645  DdSubtable *subtables = dd->subtables;
646  int i, /* loop index */
647  nodes, /* live nodes in i-th layer */
648  retval, /* return value of fprintf */
649  largest = -1, /* index of the table with most live nodes */
650  maxnodes = -1, /* maximum number of live nodes in a table */
651  nonempty = 0; /* number of tables with live nodes */
652 
653  /* Print header. */
654 #if SIZEOF_VOID_P == 8
655  retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n",
656  (ptruint) dd);
657 #else
658  retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n",
659  (ptruint) dd);
660 #endif
661  if (retval == EOF) return 0;
662 
663  /* Print number of live nodes for each nonempty table. */
664  for (i=0; i<ntables; i++) {
665  nodes = subtables[i].keys - subtables[i].dead;
666  if (nodes) {
667  nonempty++;
668  retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes);
669  if (retval == EOF) return 0;
670  if (nodes > maxnodes) {
671  maxnodes = nodes;
672  largest = i;
673  }
674  }
675  }
676 
677  nodes = dd->constants.keys - dd->constants.dead;
678  if (nodes) {
679  nonempty++;
680  retval = fprintf(dd->out,"const: %5d nodes\n", nodes);
681  if (retval == EOF) return 0;
682  if (nodes > maxnodes) {
683  maxnodes = nodes;
684  largest = CUDD_CONST_INDEX;
685  }
686  }
687 
688  /* Print summary. */
689  retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ",
690  ntables+1, nonempty, largest);
691  if (retval == EOF) return 0;
692  retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes);
693  if (retval == EOF) return 0;
694 
695  return(1);
696 
697 } /* end of cuddHeapProfile */
unsigned int keys
Definition: cuddInt.h:314
int size
Definition: cuddInt.h:345
DdSubtable * subtables
Definition: cuddInt.h:349
unsigned int dead
Definition: cuddInt.h:316
FILE * out
Definition: cuddInt.h:423
#define CUDD_CONST_INDEX
Definition: cudd.h:113
static int largest(void)
Definition: cuddGenetic.c:623
unsigned int ptruint
Definition: cuddInt.h:250
DdSubtable constants
Definition: cuddInt.h:351

◆ cuddPrintNode()

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 712 of file cuddCheck.c.

715 {
716  f = Cudd_Regular(f);
717 #if SIZEOF_VOID_P == 8
718  (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));
719 #else
720  (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));
721 #endif
722 
723 } /* end of cuddPrintNode */
DdHalfWord ref
Definition: cudd.h:272
#define Cudd_Regular(node)
Definition: cudd.h:384
#define cuddT(node)
Definition: cuddInt.h:609
unsigned int ptruint
Definition: cuddInt.h:250
DdHalfWord index
Definition: cudd.h:271
#define cuddE(node)
Definition: cuddInt.h:625

◆ cuddPrintVarGroups()

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 749 of file cuddCheck.c.

754 {
755  MtrNode *node;
756  int level;
757 
758  assert(root != NULL);
759  assert(root->younger == NULL || root->younger->elder == root);
760  assert(root->elder == NULL || root->elder->younger == root);
761  if (zdd) {
762  level = dd->permZ[root->index];
763  } else {
764  level = dd->perm[root->index];
765  }
766  if (!silent) (void) printf("(%d",level);
767  if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
768  if (!silent) (void) printf(",");
769  } else {
770  node = root->child;
771  while (node != NULL) {
772  assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
773  assert(node->parent == root);
774  cuddPrintVarGroups(dd,node,zdd,silent);
775  node = node->younger;
776  }
777  }
778  if (!silent) {
779  (void) printf("%d", (int) (level + root->size - 1));
780  if (root->flags != MTR_DEFAULT) {
781  (void) printf("|");
782  if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
783  if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
784  if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
785  }
786  (void) printf(")");
787  if (root->parent == NULL) (void) printf("\n");
788  }
789  assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
790  return;
791 
792 } /* end of cuddPrintVarGroups */
#define MTR_TERMINAL
Definition: mtr.h:95
MtrHalfWord flags
Definition: mtr.h:127
void cuddPrintVarGroups(DdManager *dd, MtrNode *root, int zdd, int silent)
Definition: cuddCheck.c:749
MtrHalfWord size
Definition: mtr.h:129
#define assert(ex)
Definition: util.h:141
#define MTR_FIXED
Definition: mtr.h:97
int * permZ
Definition: cuddInt.h:370
struct MtrNode * parent
Definition: mtr.h:131
#define MTR_DEFAULT
Definition: mtr.h:94
struct MtrNode * elder
Definition: mtr.h:133
#define MTR_TEST(node, flag)
Definition: mtr.h:150
struct MtrNode * younger
Definition: mtr.h:134
MtrHalfWord index
Definition: mtr.h:130
#define MTR_NEWNODE
Definition: mtr.h:98
MtrHalfWord low
Definition: mtr.h:128
Definition: mtr.h:126
struct MtrNode * child
Definition: mtr.h:132
int * perm
Definition: cuddInt.h:369
#define MTR_SOFT
Definition: mtr.h:96

◆ debugFindParent()

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 812 of file cuddCheck.c.

815 {
816  int i,j;
817  int slots;
818  DdNodePtr *nodelist;
819  DdNode *f;
820 
821  for (i = 0; i < cuddI(table,node->index); i++) {
822  nodelist = table->subtables[i].nodelist;
823  slots = table->subtables[i].slots;
824 
825  for (j=0;j<slots;j++) {
826  f = nodelist[j];
827  while (f != NULL) {
828  if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) {
829 #if SIZEOF_VOID_P == 8
830  (void) fprintf(table->out,"parent is at 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",
831  (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
832 #else
833  (void) fprintf(table->out,"parent is at 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",
834  (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
835 #endif
836  }
837  f = f->next;
838  }
839  }
840  }
841 
842 } /* end of debugFindParent */
DdHalfWord ref
Definition: cudd.h:272
Definition: cudd.h:270
#define Cudd_Regular(node)
Definition: cudd.h:384
DdSubtable * subtables
Definition: cuddInt.h:349
FILE * out
Definition: cuddInt.h:423
DdNode * next
Definition: cudd.h:273
DdNode ** nodelist
Definition: cuddInt.h:311
#define cuddT(node)
Definition: cuddInt.h:609
#define cuddI(dd, index)
Definition: cuddInt.h:659
unsigned int ptruint
Definition: cuddInt.h:250
DdHalfWord index
Definition: cudd.h:271
unsigned int slots
Definition: cuddInt.h:313
#define cuddE(node)
Definition: cuddInt.h:625

Variable Documentation

◆ DD_UNUSED

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