source: vis_dev/glu-2.3/src/cuBdd/cuddCheck.c @ 84

Last change on this file since 84 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 26.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddCheck.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions to check consistency of data structures.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_DebugCheck()
12                <li> Cudd_CheckKeys()
13                </ul>
14               Internal procedures included in this module:
15                <ul>
16                <li> cuddHeapProfile()
17                <li> cuddPrintNode()
18                <li> cuddPrintVarGroups()
19                </ul>
20               Static procedures included in this module:
21                <ul>
22                <li> debugFindParent()
23                </ul>
24                ]
25
26  SeeAlso     []
27
28  Author      [Fabio Somenzi]
29
30  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
31
32  All rights reserved.
33
34  Redistribution and use in source and binary forms, with or without
35  modification, are permitted provided that the following conditions
36  are met:
37
38  Redistributions of source code must retain the above copyright
39  notice, this list of conditions and the following disclaimer.
40
41  Redistributions in binary form must reproduce the above copyright
42  notice, this list of conditions and the following disclaimer in the
43  documentation and/or other materials provided with the distribution.
44
45  Neither the name of the University of Colorado nor the names of its
46  contributors may be used to endorse or promote products derived from
47  this software without specific prior written permission.
48
49  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60  POSSIBILITY OF SUCH DAMAGE.]
61
62******************************************************************************/
63
64#include "util.h"
65#include "cuddInt.h"
66
67/*---------------------------------------------------------------------------*/
68/* Constant declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Stucture declarations                                                     */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Type declarations                                                         */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Variable declarations                                                     */
84/*---------------------------------------------------------------------------*/
85
86#ifndef lint
87static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.35 2009/03/08 02:49:01 fabio Exp $";
88#endif
89
90/*---------------------------------------------------------------------------*/
91/* Macro declarations                                                        */
92/*---------------------------------------------------------------------------*/
93
94
95/**AutomaticStart*************************************************************/
96
97/*---------------------------------------------------------------------------*/
98/* Static function prototypes                                                */
99/*---------------------------------------------------------------------------*/
100
101static void debugFindParent (DdManager *table, DdNode *node);
102#if 0
103static void debugCheckParent (DdManager *table, DdNode *node);
104#endif
105
106/**AutomaticEnd***************************************************************/
107
108
109/*---------------------------------------------------------------------------*/
110/* Definition of exported functions                                          */
111/*---------------------------------------------------------------------------*/
112
113
114/**Function********************************************************************
115
116  Synopsis    [Checks for inconsistencies in the DD heap.]
117
118  Description [Checks for inconsistencies in the DD heap:
119  <ul>
120  <li> node has illegal index
121  <li> live node has dead children
122  <li> node has illegal Then or Else pointers
123  <li> BDD/ADD node has identical children
124  <li> ZDD node has zero then child
125  <li> wrong number of total nodes
126  <li> wrong number of dead nodes
127  <li> ref count error at node
128  </ul>
129  Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is
130  not enough memory; 1 otherwise.]
131
132  SideEffects [None]
133
134  SeeAlso     [Cudd_CheckKeys]
135
136******************************************************************************/
137int
138Cudd_DebugCheck(
139  DdManager * table)
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
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
169        totalNode = 0;
170        deadNode = 0;
171        for (j = 0; j < slots; j++) {   /* for each subtable slot */
172            f = nodelist[j];
173            while (f != sentinel) {
174                totalNode++;
175                if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
176                    if ((int) f->index != index) {
177                        (void) fprintf(table->err,
178                                       "Error: node has illegal index\n");
179                        cuddPrintNode(f,table->err);
180                        flag = 1;
181                    }
182                    if ((unsigned) cuddI(table,cuddT(f)->index) <= i ||
183                        (unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index)
184                        <= i) {
185                        (void) fprintf(table->err,
186                                       "Error: node has illegal children\n");
187                        cuddPrintNode(f,table->err);
188                        flag = 1;
189                    }
190                    if (Cudd_Regular(cuddT(f)) != cuddT(f)) {
191                        (void) fprintf(table->err,
192                                       "Error: node has illegal form\n");
193                        cuddPrintNode(f,table->err);
194                        flag = 1;
195                    }
196                    if (cuddT(f) == cuddE(f)) {
197                        (void) fprintf(table->err,
198                                       "Error: node has identical children\n");
199                        cuddPrintNode(f,table->err);
200                        flag = 1;
201                    }
202                    if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) {
203                        (void) fprintf(table->err,
204                                       "Error: live node has dead children\n");
205                        cuddPrintNode(f,table->err);
206                        flag =1;
207                    }
208                    /* Increment the internal reference count for the
209                    ** then child of the current node.
210                    */
211                    if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
212                        count++;
213                    } else {
214                        count = 1;
215                    }
216                    if (st_insert(edgeTable,(char *)cuddT(f),
217                    (char *)(long)count) == ST_OUT_OF_MEM) {
218                        st_free_table(edgeTable);
219                        return(CUDD_OUT_OF_MEM);
220                    }
221
222                    /* Increment the internal reference count for the
223                    ** else child of the current node.
224                    */
225                    if (st_lookup_int(edgeTable,(char *)Cudd_Regular(cuddE(f)),
226                                      &count)) {
227                        count++;
228                    } else {
229                        count = 1;
230                    }
231                    if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
232                    (char *)(long)count) == ST_OUT_OF_MEM) {
233                        st_free_table(edgeTable);
234                        return(CUDD_OUT_OF_MEM);
235                    }
236                } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
237                    deadNode++;
238#if 0
239                    debugCheckParent(table,f);
240#endif
241                } else {
242                    fprintf(table->err,
243                            "Error: node has illegal Then or Else pointers\n");
244                    cuddPrintNode(f,table->err);
245                    flag = 1;
246                }
247
248                f = f->next;
249            }   /* for each element of the collision list */
250        }       /* for each subtable slot */
251
252        if ((unsigned) totalNode != table->subtables[i].keys) {
253            fprintf(table->err,"Error: wrong number of total nodes\n");
254            flag = 1;
255        }
256        if ((unsigned) deadNode != table->subtables[i].dead) {
257            fprintf(table->err,"Error: wrong number of dead nodes\n");
258            flag = 1;
259        }
260    }   /* for each BDD/ADD subtable */
261
262    /* Check the ZDD subtables. */
263    for (i = 0; i < (unsigned) table->sizeZ; i++) {
264        index = table->invpermZ[i];
265        if (i != (unsigned) table->permZ[index]) {
266            (void) fprintf(table->err,
267                           "Permutation corrupted: invpermZ[%u] = %d\t permZ[%d] = %d in ZDD\n",
268                           i, index, index, table->permZ[index]);
269        }
270        nodelist = table->subtableZ[i].nodelist;
271        slots = table->subtableZ[i].slots;
272
273        totalNode = 0;
274        deadNode = 0;
275        for (j = 0; j < slots; j++) {   /* for each subtable slot */
276            f = nodelist[j];
277            while (f != NULL) {
278                totalNode++;
279                if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
280                    if ((int) f->index != index) {
281                        (void) fprintf(table->err,
282                                       "Error: ZDD node has illegal index\n");
283                        cuddPrintNode(f,table->err);
284                        flag = 1;
285                    }
286                    if (Cudd_IsComplement(cuddT(f)) ||
287                        Cudd_IsComplement(cuddE(f))) {
288                        (void) fprintf(table->err,
289                                       "Error: ZDD node has complemented children\n");
290                        cuddPrintNode(f,table->err);
291                        flag = 1;
292                    }
293                    if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i ||
294                    (unsigned) cuddIZ(table,cuddE(f)->index) <= i) {
295                        (void) fprintf(table->err,
296                                       "Error: ZDD node has illegal children\n");
297                        cuddPrintNode(f,table->err);
298                        cuddPrintNode(cuddT(f),table->err);
299                        cuddPrintNode(cuddE(f),table->err);
300                        flag = 1;
301                    }
302                    if (cuddT(f) == DD_ZERO(table)) {
303                        (void) fprintf(table->err,
304                                       "Error: ZDD node has zero then child\n");
305                        cuddPrintNode(f,table->err);
306                        flag = 1;
307                    }
308                    if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) {
309                        (void) fprintf(table->err,
310                                       "Error: ZDD live node has dead children\n");
311                        cuddPrintNode(f,table->err);
312                        flag =1;
313                    }
314                    /* Increment the internal reference count for the
315                    ** then child of the current node.
316                    */
317                    if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
318                        count++;
319                    } else {
320                        count = 1;
321                    }
322                    if (st_insert(edgeTable,(char *)cuddT(f),
323                    (char *)(long)count) == ST_OUT_OF_MEM) {
324                        st_free_table(edgeTable);
325                        return(CUDD_OUT_OF_MEM);
326                    }
327
328                    /* Increment the internal reference count for the
329                    ** else child of the current node.
330                    */
331                    if (st_lookup_int(edgeTable,(char *)cuddE(f),&count)) {
332                        count++;
333                    } else {
334                        count = 1;
335                    }
336                    if (st_insert(edgeTable,(char *)cuddE(f),
337                    (char *)(long)count) == ST_OUT_OF_MEM) {
338                        st_free_table(edgeTable);
339                        table->errorCode = CUDD_MEMORY_OUT;
340                        return(CUDD_OUT_OF_MEM);
341                    }
342                } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
343                    deadNode++;
344#if 0
345                    debugCheckParent(table,f);
346#endif
347                } else {
348                    fprintf(table->err,
349                            "Error: ZDD node has illegal Then or Else pointers\n");
350                    cuddPrintNode(f,table->err);
351                    flag = 1;
352                }
353
354                f = f->next;
355            }   /* for each element of the collision list */
356        }       /* for each subtable slot */
357
358        if ((unsigned) totalNode != table->subtableZ[i].keys) {
359            fprintf(table->err,
360                    "Error: wrong number of total nodes in ZDD\n");
361            flag = 1;
362        }
363        if ((unsigned) deadNode != table->subtableZ[i].dead) {
364            fprintf(table->err,
365                    "Error: wrong number of dead nodes in ZDD\n");
366            flag = 1;
367        }
368    }   /* for each ZDD subtable */
369
370    /* Check the constant table. */
371    nodelist = table->constants.nodelist;
372    slots = table->constants.slots;
373
374    totalNode = 0;
375    deadNode = 0;
376    for (j = 0; j < slots; j++) {
377        f = nodelist[j];
378        while (f != NULL) {
379            totalNode++;
380            if (f->ref != 0) {
381                if (f->index != CUDD_CONST_INDEX) {
382                    fprintf(table->err,"Error: node has illegal index\n");
383#if SIZEOF_VOID_P == 8
384                    fprintf(table->err,
385                            "       node 0x%lx, id = %u, ref = %u, value = %g\n",
386                            (ptruint)f,f->index,f->ref,cuddV(f));
387#else
388                    fprintf(table->err,
389                            "       node 0x%x, id = %hu, ref = %hu, value = %g\n",
390                            (ptruint)f,f->index,f->ref,cuddV(f));
391#endif
392                    flag = 1;
393                }
394            } else {
395                deadNode++;
396            }
397            f = f->next;
398        }
399    }
400    if ((unsigned) totalNode != table->constants.keys) {
401        (void) fprintf(table->err,
402                       "Error: wrong number of total nodes in constants\n");
403        flag = 1;
404    }
405    if ((unsigned) deadNode != table->constants.dead) {
406        (void) fprintf(table->err,
407                       "Error: wrong number of dead nodes in constants\n");
408        flag = 1;
409    }
410    gen = st_init_gen(edgeTable);
411    while (st_gen(gen, &f, &count)) {
412        if (count > (int)(f->ref) && f->ref != DD_MAXREF) {
413#if SIZEOF_VOID_P == 8
414            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));
415#else
416            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));
417#endif
418            debugFindParent(table,f);
419            flag = 1;
420        }
421    }
422    st_free_gen(gen);
423    st_free_table(edgeTable);
424
425    return (flag);
426
427} /* end of Cudd_DebugCheck */
428
429
430/**Function********************************************************************
431
432  Synopsis    [Checks for several conditions that should not occur.]
433
434  Description [Checks for the following conditions:
435  <ul>
436  <li>Wrong sizes of subtables.
437  <li>Wrong number of keys found in unique subtable.
438  <li>Wrong number of dead found in unique subtable.
439  <li>Wrong number of keys found in the constant table
440  <li>Wrong number of dead found in the constant table
441  <li>Wrong number of total slots found
442  <li>Wrong number of maximum keys found
443  <li>Wrong number of total dead found
444  </ul>
445  Reports the average length of non-empty lists. Returns the number of
446  subtables for which the number of keys is wrong.]
447
448  SideEffects [None]
449
450  SeeAlso     [Cudd_DebugCheck]
451
452******************************************************************************/
453int
454Cudd_CheckKeys(
455  DdManager * table)
456{
457    int size;
458    int i,j;
459    DdNodePtr *nodelist;
460    DdNode *node;
461    DdNode *sentinel = &(table->sentinel);
462    DdSubtable *subtable;
463    int keys;
464    int dead;
465    int count = 0;
466    int totalKeys = 0;
467    int totalSlots = 0;
468    int totalDead = 0;
469    int nonEmpty = 0;
470    unsigned int slots;
471    int logSlots;
472    int shift;
473
474    size = table->size;
475
476    for (i = 0; i < size; i++) {
477        subtable = &(table->subtables[i]);
478        nodelist = subtable->nodelist;
479        keys = subtable->keys;
480        dead = subtable->dead;
481        totalKeys += keys;
482        slots = subtable->slots;
483        shift = subtable->shift;
484        logSlots = sizeof(int) * 8 - shift;
485        if (((slots >> logSlots) << logSlots) != slots) {
486            (void) fprintf(table->err,
487                           "Unique table %d is not the right power of 2\n", i);
488            (void) fprintf(table->err,
489                           "    slots = %u shift = %d\n", slots, shift);
490        }
491        totalSlots += slots;
492        totalDead += dead;
493        for (j = 0; (unsigned) j < slots; j++) {
494            node = nodelist[j];
495            if (node != sentinel) {
496                nonEmpty++;
497            }
498            while (node != sentinel) {
499                keys--;
500                if (node->ref == 0) {
501                    dead--;
502                }
503                node = node->next;
504            }
505        }
506        if (keys != 0) {
507            (void) fprintf(table->err, "Wrong number of keys found \
508in unique table %d (difference=%d)\n", i, keys);
509            count++;
510        }
511        if (dead != 0) {
512            (void) fprintf(table->err, "Wrong number of dead found \
513in unique table no. %d (difference=%d)\n", i, dead);
514        }
515    }   /* for each BDD/ADD subtable */
516
517    /* Check the ZDD subtables. */
518    size = table->sizeZ;
519
520    for (i = 0; i < size; i++) {
521        subtable = &(table->subtableZ[i]);
522        nodelist = subtable->nodelist;
523        keys = subtable->keys;
524        dead = subtable->dead;
525        totalKeys += keys;
526        totalSlots += subtable->slots;
527        totalDead += dead;
528        for (j = 0; (unsigned) j < subtable->slots; j++) {
529            node = nodelist[j];
530            if (node != NULL) {
531                nonEmpty++;
532            }
533            while (node != NULL) {
534                keys--;
535                if (node->ref == 0) {
536                    dead--;
537                }
538                node = node->next;
539            }
540        }
541        if (keys != 0) {
542            (void) fprintf(table->err, "Wrong number of keys found \
543in ZDD unique table no. %d (difference=%d)\n", i, keys);
544            count++;
545        }
546        if (dead != 0) {
547            (void) fprintf(table->err, "Wrong number of dead found \
548in ZDD unique table no. %d (difference=%d)\n", i, dead);
549        }
550    }   /* for each ZDD subtable */
551
552    /* Check the constant table. */
553    subtable = &(table->constants);
554    nodelist = subtable->nodelist;
555    keys = subtable->keys;
556    dead = subtable->dead;
557    totalKeys += keys;
558    totalSlots += subtable->slots;
559    totalDead += dead;
560    for (j = 0; (unsigned) j < subtable->slots; j++) {
561        node = nodelist[j];
562        if (node != NULL) {
563            nonEmpty++;
564        }
565        while (node != NULL) {
566            keys--;
567            if (node->ref == 0) {
568                dead--;
569            }
570            node = node->next;
571        }
572    }
573    if (keys != 0) {
574        (void) fprintf(table->err, "Wrong number of keys found \
575in the constant table (difference=%d)\n", keys);
576        count++;
577    }
578    if (dead != 0) {
579        (void) fprintf(table->err, "Wrong number of dead found \
580in the constant table (difference=%d)\n", dead);
581    }
582    if ((unsigned) totalKeys != table->keys + table->keysZ) {
583        (void) fprintf(table->err, "Wrong number of total keys found \
584(difference=%d)\n", (int) (totalKeys-table->keys));
585    }
586    if ((unsigned) totalSlots != table->slots) {
587        (void) fprintf(table->err, "Wrong number of total slots found \
588(difference=%d)\n", (int) (totalSlots-table->slots));
589    }
590    if (table->minDead != (unsigned) (table->gcFrac * table->slots)) {
591        (void) fprintf(table->err, "Wrong number of minimum dead found \
592(%u vs. %u)\n", table->minDead,
593        (unsigned) (table->gcFrac * (double) table->slots));
594    }
595    if ((unsigned) totalDead != table->dead + table->deadZ) {
596        (void) fprintf(table->err, "Wrong number of total dead found \
597(difference=%d)\n", (int) (totalDead-table->dead));
598    }
599    (void)printf("Average length of non-empty lists = %g\n",
600    (double) table->keys / (double) nonEmpty);
601
602    return(count);
603
604} /* end of Cudd_CheckKeys */
605
606
607/*---------------------------------------------------------------------------*/
608/* Definition of internal functions                                          */
609/*---------------------------------------------------------------------------*/
610
611
612/**Function********************************************************************
613
614  Synopsis    [Prints information about the heap.]
615
616  Description [Prints to the manager's stdout the number of live nodes for each
617  level of the DD heap that contains at least one live node.  It also
618  prints a summary containing:
619  <ul>
620  <li> total number of tables;
621  <li> number of tables with live nodes;
622  <li> table with the largest number of live nodes;
623  <li> number of nodes in that table.
624  </ul>
625  If more than one table contains the maximum number of live nodes,
626  only the one of lowest index is reported. Returns 1 in case of success
627  and 0 otherwise.]
628
629  SideEffects [None]
630
631  SeeAlso     []
632
633******************************************************************************/
634int
635cuddHeapProfile(
636  DdManager * dd)
637{
638    int ntables = dd->size;
639    DdSubtable *subtables = dd->subtables;
640    int i,              /* loop index */
641        nodes,          /* live nodes in i-th layer */
642        retval,         /* return value of fprintf */
643        largest = -1,   /* index of the table with most live nodes */
644        maxnodes = -1,  /* maximum number of live nodes in a table */
645        nonempty = 0;   /* number of tables with live nodes */
646
647    /* Print header. */
648#if SIZEOF_VOID_P == 8
649    retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n",
650                     (ptruint) dd);
651#else
652    retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n",
653                     (ptruint) dd);
654#endif
655    if (retval == EOF) return 0;
656
657    /* Print number of live nodes for each nonempty table. */
658    for (i=0; i<ntables; i++) {
659        nodes = subtables[i].keys - subtables[i].dead;
660        if (nodes) {
661            nonempty++;
662            retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes);
663            if (retval == EOF) return 0;
664            if (nodes > maxnodes) {
665                maxnodes = nodes;
666                largest = i;
667            }
668        }
669    }
670
671    nodes = dd->constants.keys - dd->constants.dead;
672    if (nodes) {
673        nonempty++;
674        retval = fprintf(dd->out,"const: %5d nodes\n", nodes);
675        if (retval == EOF) return 0;
676        if (nodes > maxnodes) {
677            maxnodes = nodes;
678            largest = CUDD_CONST_INDEX;
679        }
680    }
681
682    /* Print summary. */
683    retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ",
684          ntables+1, nonempty, largest);
685    if (retval == EOF) return 0;
686    retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes);
687    if (retval == EOF) return 0;
688
689    return(1);
690
691} /* end of cuddHeapProfile */
692
693
694/**Function********************************************************************
695
696  Synopsis    [Prints out information on a node.]
697
698  Description [Prints out information on a node.]
699
700  SideEffects [None]
701
702  SeeAlso     []
703
704******************************************************************************/
705void
706cuddPrintNode(
707  DdNode * f,
708  FILE *fp)
709{
710    f = Cudd_Regular(f);
711#if SIZEOF_VOID_P == 8
712    (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));
713#else
714    (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));
715#endif
716
717} /* end of cuddPrintNode */
718
719
720
721/**Function********************************************************************
722
723  Synopsis    [Prints the variable groups as a parenthesized list.]
724
725  Description [Prints the variable groups as a parenthesized list.
726  For each group the level range that it represents is printed. After
727  each group, the group's flags are printed, preceded by a `|'.  For
728  each flag (except MTR_TERMINAL) a character is printed.
729  <ul>
730  <li>F: MTR_FIXED
731  <li>N: MTR_NEWNODE
732  <li>S: MTR_SOFT
733  </ul>
734  The second argument, silent, if different from 0, causes
735  Cudd_PrintVarGroups to only check the syntax of the group tree.]
736
737  SideEffects [None]
738
739  SeeAlso     []
740
741******************************************************************************/
742void
743cuddPrintVarGroups(
744  DdManager * dd /* manager */,
745  MtrNode * root /* root of the group tree */,
746  int zdd /* 0: BDD; 1: ZDD */,
747  int silent /* flag to check tree syntax only */)
748{
749    MtrNode *node;
750    int level;
751
752    assert(root != NULL);
753    assert(root->younger == NULL || root->younger->elder == root);
754    assert(root->elder == NULL || root->elder->younger == root);
755    if (zdd) {
756        level = dd->permZ[root->index];
757    } else {
758        level = dd->perm[root->index];
759    }
760    if (!silent) (void) printf("(%d",level);
761    if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
762        if (!silent) (void) printf(",");
763    } else {
764        node = root->child;
765        while (node != NULL) {
766            assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
767            assert(node->parent == root);
768            cuddPrintVarGroups(dd,node,zdd,silent);
769            node = node->younger;
770        }
771    }
772    if (!silent) {
773        (void) printf("%d", (int) (level + root->size - 1));
774        if (root->flags != MTR_DEFAULT) {
775            (void) printf("|");
776            if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
777            if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
778            if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
779        }
780        (void) printf(")");
781        if (root->parent == NULL) (void) printf("\n");
782    }
783    assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
784    return;
785
786} /* end of cuddPrintVarGroups */
787
788
789/*---------------------------------------------------------------------------*/
790/* Definition of static functions                                            */
791/*---------------------------------------------------------------------------*/
792
793
794/**Function********************************************************************
795
796  Synopsis    [Searches the subtables above node for its parents.]
797
798  Description []
799
800  SideEffects [None]
801
802  SeeAlso     []
803
804******************************************************************************/
805static void
806debugFindParent(
807  DdManager * table,
808  DdNode * node)
809{
810    int         i,j;
811    int         slots;
812    DdNodePtr   *nodelist;
813    DdNode      *f;
814
815    for (i = 0; i < cuddI(table,node->index); i++) {
816        nodelist = table->subtables[i].nodelist;
817        slots = table->subtables[i].slots;
818
819        for (j=0;j<slots;j++) {
820            f = nodelist[j];
821            while (f != NULL) {
822                if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) {
823#if SIZEOF_VOID_P == 8
824                    (void) fprintf(table->out,"parent is at 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",
825                        (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
826#else
827                    (void) fprintf(table->out,"parent is at 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",
828                        (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
829#endif
830                }
831                f = f->next;
832            }
833        }
834    }
835
836} /* end of debugFindParent */
837
838
839#if 0
840/**Function********************************************************************
841
842  Synopsis    [Reports an error if a (dead) node has a non-dead parent.]
843
844  Description [Searches all the subtables above node. Very expensive.
845  The same check is now implemented more efficiently in ddDebugCheck.]
846
847  SideEffects [None]
848
849  SeeAlso     [debugFindParent]
850
851******************************************************************************/
852static void
853debugCheckParent(
854  DdManager * table,
855  DdNode * node)
856{
857    int         i,j;
858    int         slots;
859    DdNode      **nodelist,*f;
860
861    for (i = 0; i < cuddI(table,node->index); i++) {
862        nodelist = table->subtables[i].nodelist;
863        slots = table->subtables[i].slots;
864
865        for (j=0;j<slots;j++) {
866            f = nodelist[j];
867            while (f != NULL) {
868                if ((Cudd_Regular(cuddE(f)) == node || cuddT(f) == node) && f->ref != 0) {
869                    (void) fprintf(table->err,
870                                   "error with zero ref count\n");
871                    (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));
872                    (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));
873                }
874                f = f->next;
875            }
876        }
877    }
878}
879#endif
Note: See TracBrowser for help on using the repository browser.