cuddCheck.c 31.1 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9
/**CFile***********************************************************************

  FileName    [cuddCheck.c]

  PackageName [cudd]

  Synopsis    [Functions to check consistency of data structures.]

  Description [External procedures included in this module:
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
                <ul>
                <li> Cudd_DebugCheck()
                <li> Cudd_CheckKeys()
                </ul>
               Internal procedures included in this module:
                <ul>
                <li> cuddHeapProfile()
                <li> cuddPrintNode()
                <li> cuddPrintVarGroups()
                </ul>
               Static procedures included in this module:
                <ul>
                <li> debugFindParent()
                </ul>
                ]
Alan Mishchenko committed
25 26 27 28 29

  SeeAlso     []

  Author      [Fabio Somenzi]

30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
  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.]
Alan Mishchenko committed
61 62 63

******************************************************************************/

64
#include "misc/util/util_hack.h"
Alan Mishchenko committed
65 66
#include "cuddInt.h"

67 68 69
ABC_NAMESPACE_IMPL_START


70

Alan Mishchenko committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


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

#ifndef lint
91
static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.35 2009/03/08 02:49:01 fabio Exp $";
Alan Mishchenko committed
92 93 94 95 96 97 98 99 100 101 102 103 104
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

105
static void debugFindParent (DdManager *table, DdNode *node);
Alan Mishchenko committed
106
#if 0
107
static void debugCheckParent (DdManager *table, DdNode *node);
Alan Mishchenko committed
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
#endif

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Checks for inconsistencies in the DD heap.]

  Description [Checks for inconsistencies in the DD heap:
  <ul>
  <li> node has illegal index
  <li> live node has dead children
  <li> node has illegal Then or Else pointers
  <li> BDD/ADD node has identical children
  <li> ZDD node has zero then child
  <li> wrong number of total nodes
  <li> wrong number of dead nodes
  <li> ref count error at node
  </ul>
  Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is
  not enough memory; 1 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_CheckKeys]

******************************************************************************/
int
Cudd_DebugCheck(
  DdManager * table)
{
    unsigned int i;
146 147 148 149 150
    int         j,count;
    int         slots;
    DdNodePtr   *nodelist;
    DdNode      *f;
    DdNode      *sentinel = &(table->sentinel);
151 152
    st__table    *edgeTable;     /* stores internal ref count for each node */
    st__generator        *gen;
153 154 155 156 157 158
    int         flag = 0;
    int         totalNode;
    int         deadNode;
    int         index;


159
    edgeTable = st__init_table( st__ptrcmp, st__ptrhash);
Alan Mishchenko committed
160 161 162 163
    if (edgeTable == NULL) return(CUDD_OUT_OF_MEM);

    /* Check the BDD/ADD subtables. */
    for (i = 0; i < (unsigned) table->size; i++) {
164 165
        index = table->invperm[i];
        if (i != (unsigned) table->perm[index]) {
Alan Mishchenko committed
166
            (void) fprintf(table->err,
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
                           "Permutation corrupted: invperm[%u] = %d\t perm[%d] = %d\n",
                           i, index, index, table->perm[index]);
        }
        nodelist = table->subtables[i].nodelist;
        slots = table->subtables[i].slots;

        totalNode = 0;
        deadNode = 0;
        for (j = 0; j < slots; j++) {   /* for each subtable slot */
            f = nodelist[j];
            while (f != sentinel) {
                totalNode++;
                if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
                    if ((int) f->index != index) {
                        (void) fprintf(table->err,
                                       "Error: node has illegal index\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if ((unsigned) cuddI(table,cuddT(f)->index) <= i ||
                        (unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index)
                        <= i) {
                        (void) fprintf(table->err,
                                       "Error: node has illegal children\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if (Cudd_Regular(cuddT(f)) != cuddT(f)) {
                        (void) fprintf(table->err,
                                       "Error: node has illegal form\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if (cuddT(f) == cuddE(f)) {
                        (void) fprintf(table->err,
                                       "Error: node has identical children\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) {
                        (void) fprintf(table->err,
                                       "Error: live node has dead children\n");
                        cuddPrintNode(f,table->err);
                        flag =1;
                    }
                    /* Increment the internal reference count for the
                    ** then child of the current node.
                    */
215
                    if ( st__lookup_int(edgeTable,(char *)cuddT(f),&count)) {
216 217 218 219
                        count++;
                    } else {
                        count = 1;
                    }
220 221 222
                    if ( st__insert(edgeTable,(char *)cuddT(f),
                    (char *)(long)count) == st__OUT_OF_MEM) {
                        st__free_table(edgeTable);
223 224 225 226 227 228
                        return(CUDD_OUT_OF_MEM);
                    }

                    /* Increment the internal reference count for the
                    ** else child of the current node.
                    */
229
                    if ( st__lookup_int(edgeTable,(char *)Cudd_Regular(cuddE(f)),
230 231 232 233 234
                                      &count)) {
                        count++;
                    } else {
                        count = 1;
                    }
235 236 237
                    if ( st__insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
                    (char *)(long)count) == st__OUT_OF_MEM) {
                        st__free_table(edgeTable);
238 239 240 241
                        return(CUDD_OUT_OF_MEM);
                    }
                } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
                    deadNode++;
Alan Mishchenko committed
242
#if 0
243
                    debugCheckParent(table,f);
Alan Mishchenko committed
244
#endif
245 246 247 248 249 250 251 252 253 254 255 256 257
                } else {
                    fprintf(table->err,
                            "Error: node has illegal Then or Else pointers\n");
                    cuddPrintNode(f,table->err);
                    flag = 1;
                }

                f = f->next;
            }   /* for each element of the collision list */
        }       /* for each subtable slot */

        if ((unsigned) totalNode != table->subtables[i].keys) {
            fprintf(table->err,"Error: wrong number of total nodes\n");
Alan Mishchenko committed
258 259
            flag = 1;
        }
260 261 262 263 264
        if ((unsigned) deadNode != table->subtables[i].dead) {
            fprintf(table->err,"Error: wrong number of dead nodes\n");
            flag = 1;
        }
    }   /* for each BDD/ADD subtable */
Alan Mishchenko committed
265 266 267

    /* Check the ZDD subtables. */
    for (i = 0; i < (unsigned) table->sizeZ; i++) {
268 269
        index = table->invpermZ[i];
        if (i != (unsigned) table->permZ[index]) {
Alan Mishchenko committed
270
            (void) fprintf(table->err,
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320
                           "Permutation corrupted: invpermZ[%u] = %d\t permZ[%d] = %d in ZDD\n",
                           i, index, index, table->permZ[index]);
        }
        nodelist = table->subtableZ[i].nodelist;
        slots = table->subtableZ[i].slots;

        totalNode = 0;
        deadNode = 0;
        for (j = 0; j < slots; j++) {   /* for each subtable slot */
            f = nodelist[j];
            while (f != NULL) {
                totalNode++;
                if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) {
                    if ((int) f->index != index) {
                        (void) fprintf(table->err,
                                       "Error: ZDD node has illegal index\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if (Cudd_IsComplement(cuddT(f)) ||
                        Cudd_IsComplement(cuddE(f))) {
                        (void) fprintf(table->err,
                                       "Error: ZDD node has complemented children\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i ||
                    (unsigned) cuddIZ(table,cuddE(f)->index) <= i) {
                        (void) fprintf(table->err,
                                       "Error: ZDD node has illegal children\n");
                        cuddPrintNode(f,table->err);
                        cuddPrintNode(cuddT(f),table->err);
                        cuddPrintNode(cuddE(f),table->err);
                        flag = 1;
                    }
                    if (cuddT(f) == DD_ZERO(table)) {
                        (void) fprintf(table->err,
                                       "Error: ZDD node has zero then child\n");
                        cuddPrintNode(f,table->err);
                        flag = 1;
                    }
                    if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) {
                        (void) fprintf(table->err,
                                       "Error: ZDD live node has dead children\n");
                        cuddPrintNode(f,table->err);
                        flag =1;
                    }
                    /* Increment the internal reference count for the
                    ** then child of the current node.
                    */
321
                    if ( st__lookup_int(edgeTable,(char *)cuddT(f),&count)) {
322 323 324 325
                        count++;
                    } else {
                        count = 1;
                    }
326 327 328
                    if ( st__insert(edgeTable,(char *)cuddT(f),
                    (char *)(long)count) == st__OUT_OF_MEM) {
                        st__free_table(edgeTable);
329 330 331 332 333 334
                        return(CUDD_OUT_OF_MEM);
                    }

                    /* Increment the internal reference count for the
                    ** else child of the current node.
                    */
335
                    if ( st__lookup_int(edgeTable,(char *)cuddE(f),&count)) {
336 337 338 339
                        count++;
                    } else {
                        count = 1;
                    }
340 341 342
                    if ( st__insert(edgeTable,(char *)cuddE(f),
                    (char *)(long)count) == st__OUT_OF_MEM) {
                        st__free_table(edgeTable);
343 344 345 346 347
                        table->errorCode = CUDD_MEMORY_OUT;
                        return(CUDD_OUT_OF_MEM);
                    }
                } else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
                    deadNode++;
Alan Mishchenko committed
348
#if 0
349
                    debugCheckParent(table,f);
Alan Mishchenko committed
350
#endif
351 352 353 354 355 356 357 358 359 360 361 362
                } else {
                    fprintf(table->err,
                            "Error: ZDD node has illegal Then or Else pointers\n");
                    cuddPrintNode(f,table->err);
                    flag = 1;
                }

                f = f->next;
            }   /* for each element of the collision list */
        }       /* for each subtable slot */

        if ((unsigned) totalNode != table->subtableZ[i].keys) {
Alan Mishchenko committed
363
            fprintf(table->err,
364
                    "Error: wrong number of total nodes in ZDD\n");
Alan Mishchenko committed
365 366
            flag = 1;
        }
367 368 369 370 371 372
        if ((unsigned) deadNode != table->subtableZ[i].dead) {
            fprintf(table->err,
                    "Error: wrong number of dead nodes in ZDD\n");
            flag = 1;
        }
    }   /* for each ZDD subtable */
Alan Mishchenko committed
373 374 375 376 377 378 379 380

    /* Check the constant table. */
    nodelist = table->constants.nodelist;
    slots = table->constants.slots;

    totalNode = 0;
    deadNode = 0;
    for (j = 0; j < slots; j++) {
381 382 383 384 385 386
        f = nodelist[j];
        while (f != NULL) {
            totalNode++;
            if (f->ref != 0) {
                if (f->index != CUDD_CONST_INDEX) {
                    fprintf(table->err,"Error: node has illegal index\n");
Alan Mishchenko committed
387
#if SIZEOF_VOID_P == 8
388 389 390
                    fprintf(table->err,
                            "       node 0x%lx, id = %u, ref = %u, value = %g\n",
                            (ptruint)f,f->index,f->ref,cuddV(f));
Alan Mishchenko committed
391
#else
392 393 394
                    fprintf(table->err,
                            "       node 0x%x, id = %hu, ref = %hu, value = %g\n",
                            (ptruint)f,f->index,f->ref,cuddV(f));
Alan Mishchenko committed
395
#endif
396 397 398 399 400 401
                    flag = 1;
                }
            } else {
                deadNode++;
            }
            f = f->next;
Alan Mishchenko committed
402 403 404
        }
    }
    if ((unsigned) totalNode != table->constants.keys) {
405 406 407
        (void) fprintf(table->err,
                       "Error: wrong number of total nodes in constants\n");
        flag = 1;
Alan Mishchenko committed
408 409
    }
    if ((unsigned) deadNode != table->constants.dead) {
410 411 412
        (void) fprintf(table->err,
                       "Error: wrong number of dead nodes in constants\n");
        flag = 1;
Alan Mishchenko committed
413
    }
414 415
    gen = st__init_gen(edgeTable);
    while ( st__gen(gen, (const char **)&f, (char **)&count)) {
416
        if (count > (int)(f->ref) && f->ref != DD_MAXREF) {
Alan Mishchenko committed
417
#if SIZEOF_VOID_P == 8
418
            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));
Alan Mishchenko committed
419
#else
420
            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));
Alan Mishchenko committed
421
#endif
422 423 424
            debugFindParent(table,f);
            flag = 1;
        }
Alan Mishchenko committed
425
    }
426 427
    st__free_gen(gen);
    st__free_table(edgeTable);
Alan Mishchenko committed
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480

    return (flag);

} /* end of Cudd_DebugCheck */


/**Function********************************************************************

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

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

  SideEffects [None]

  SeeAlso     [Cudd_DebugCheck]

******************************************************************************/
int
Cudd_CheckKeys(
  DdManager * table)
{
    int size;
    int i,j;
    DdNodePtr *nodelist;
    DdNode *node;
    DdNode *sentinel = &(table->sentinel);
    DdSubtable *subtable;
    int keys;
    int dead;
    int count = 0;
    int totalKeys = 0;
    int totalSlots = 0;
    int totalDead = 0;
    int nonEmpty = 0;
    unsigned int slots;
    int logSlots;
    int shift;

    size = table->size;

    for (i = 0; i < size; i++) {
481 482 483 484 485 486 487 488 489 490 491 492 493
        subtable = &(table->subtables[i]);
        nodelist = subtable->nodelist;
        keys = subtable->keys;
        dead = subtable->dead;
        totalKeys += keys;
        slots = subtable->slots;
        shift = subtable->shift;
        logSlots = sizeof(int) * 8 - shift;
        if (((slots >> logSlots) << logSlots) != slots) {
            (void) fprintf(table->err,
                           "Unique table %d is not the right power of 2\n", i);
            (void) fprintf(table->err,
                           "    slots = %u shift = %d\n", slots, shift);
Alan Mishchenko committed
494
        }
495 496 497 498 499 500 501 502 503 504 505 506 507 508
        totalSlots += slots;
        totalDead += dead;
        for (j = 0; (unsigned) j < slots; j++) {
            node = nodelist[j];
            if (node != sentinel) {
                nonEmpty++;
            }
            while (node != sentinel) {
                keys--;
                if (node->ref == 0) {
                    dead--;
                }
                node = node->next;
            }
Alan Mishchenko committed
509
        }
510 511
        if (keys != 0) {
            (void) fprintf(table->err, "Wrong number of keys found \
Alan Mishchenko committed
512
in unique table %d (difference=%d)\n", i, keys);
513 514 515 516
            count++;
        }
        if (dead != 0) {
            (void) fprintf(table->err, "Wrong number of dead found \
Alan Mishchenko committed
517
in unique table no. %d (difference=%d)\n", i, dead);
518 519
        }
    }   /* for each BDD/ADD subtable */
Alan Mishchenko committed
520 521 522 523 524

    /* Check the ZDD subtables. */
    size = table->sizeZ;

    for (i = 0; i < size; i++) {
525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
        subtable = &(table->subtableZ[i]);
        nodelist = subtable->nodelist;
        keys = subtable->keys;
        dead = subtable->dead;
        totalKeys += keys;
        totalSlots += subtable->slots;
        totalDead += dead;
        for (j = 0; (unsigned) j < subtable->slots; j++) {
            node = nodelist[j];
            if (node != NULL) {
                nonEmpty++;
            }
            while (node != NULL) {
                keys--;
                if (node->ref == 0) {
                    dead--;
                }
                node = node->next;
            }
Alan Mishchenko committed
544
        }
545 546
        if (keys != 0) {
            (void) fprintf(table->err, "Wrong number of keys found \
Alan Mishchenko committed
547
in ZDD unique table no. %d (difference=%d)\n", i, keys);
548 549 550 551
            count++;
        }
        if (dead != 0) {
            (void) fprintf(table->err, "Wrong number of dead found \
Alan Mishchenko committed
552
in ZDD unique table no. %d (difference=%d)\n", i, dead);
553 554
        }
    }   /* for each ZDD subtable */
Alan Mishchenko committed
555 556 557 558 559 560 561 562 563 564

    /* Check the constant table. */
    subtable = &(table->constants);
    nodelist = subtable->nodelist;
    keys = subtable->keys;
    dead = subtable->dead;
    totalKeys += keys;
    totalSlots += subtable->slots;
    totalDead += dead;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
565 566 567 568 569 570 571 572 573 574
        node = nodelist[j];
        if (node != NULL) {
            nonEmpty++;
        }
        while (node != NULL) {
            keys--;
            if (node->ref == 0) {
                dead--;
            }
            node = node->next;
Alan Mishchenko committed
575 576 577
        }
    }
    if (keys != 0) {
578
        (void) fprintf(table->err, "Wrong number of keys found \
Alan Mishchenko committed
579
in the constant table (difference=%d)\n", keys);
580
        count++;
Alan Mishchenko committed
581 582
    }
    if (dead != 0) {
583
        (void) fprintf(table->err, "Wrong number of dead found \
Alan Mishchenko committed
584 585 586
in the constant table (difference=%d)\n", dead);
    }
    if ((unsigned) totalKeys != table->keys + table->keysZ) {
587 588
        (void) fprintf(table->err, "Wrong number of total keys found \
(difference=%d)\n", (int) (totalKeys-table->keys));
Alan Mishchenko committed
589 590
    }
    if ((unsigned) totalSlots != table->slots) {
591 592
        (void) fprintf(table->err, "Wrong number of total slots found \
(difference=%d)\n", (int) (totalSlots-table->slots));
Alan Mishchenko committed
593 594
    }
    if (table->minDead != (unsigned) (table->gcFrac * table->slots)) {
595 596 597
        (void) fprintf(table->err, "Wrong number of minimum dead found \
(%u vs. %u)\n", table->minDead,
        (unsigned) (table->gcFrac * (double) table->slots));
Alan Mishchenko committed
598 599
    }
    if ((unsigned) totalDead != table->dead + table->deadZ) {
600 601
        (void) fprintf(table->err, "Wrong number of total dead found \
(difference=%d)\n", (int) (totalDead-table->dead));
Alan Mishchenko committed
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643
    }
    (void)printf("Average length of non-empty lists = %g\n",
    (double) table->keys / (double) nonEmpty);

    return(count);

} /* end of Cudd_CheckKeys */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**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:
  <ul>
  <li> total number of tables;
  <li> number of tables with live nodes;
  <li> table with the largest number of live nodes;
  <li> number of nodes in that table.
  </ul>
  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     []

******************************************************************************/
int
cuddHeapProfile(
  DdManager * dd)
{
    int ntables = dd->size;
    DdSubtable *subtables = dd->subtables;
644 645 646 647 648 649
    int i,              /* loop index */
        nodes,          /* live nodes in i-th layer */
        retval,         /* return value of fprintf */
        largest = -1,   /* index of the table with most live nodes */
        maxnodes = -1,  /* maximum number of live nodes in a table */
        nonempty = 0;   /* number of tables with live nodes */
Alan Mishchenko committed
650 651 652 653

    /* Print header. */
#if SIZEOF_VOID_P == 8
    retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n",
654
                     (ptruint) dd);
Alan Mishchenko committed
655 656
#else
    retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n",
657
                     (ptruint) dd);
Alan Mishchenko committed
658 659 660 661 662
#endif
    if (retval == EOF) return 0;

    /* Print number of live nodes for each nonempty table. */
    for (i=0; i<ntables; i++) {
663 664 665 666 667 668 669 670 671
        nodes = subtables[i].keys - subtables[i].dead;
        if (nodes) {
            nonempty++;
            retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes);
            if (retval == EOF) return 0;
            if (nodes > maxnodes) {
                maxnodes = nodes;
                largest = i;
            }
Alan Mishchenko committed
672 673 674 675 676
        }
    }

    nodes = dd->constants.keys - dd->constants.dead;
    if (nodes) {
677 678 679 680 681 682 683
        nonempty++;
        retval = fprintf(dd->out,"const: %5d nodes\n", nodes);
        if (retval == EOF) return 0;
        if (nodes > maxnodes) {
            maxnodes = nodes;
            largest = CUDD_CONST_INDEX;
        }
Alan Mishchenko committed
684 685 686 687
    }

    /* Print summary. */
    retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ",
688
          ntables+1, nonempty, largest);
Alan Mishchenko committed
689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715
    if (retval == EOF) return 0;
    retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes);
    if (retval == EOF) return 0;

    return(1);

} /* end of cuddHeapProfile */


/**Function********************************************************************

  Synopsis    [Prints out information on a node.]

  Description [Prints out information on a node.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddPrintNode(
  DdNode * f,
  FILE *fp)
{
    f = Cudd_Regular(f);
#if SIZEOF_VOID_P == 8
716
    (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));
Alan Mishchenko committed
717
#else
718
    (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));
Alan Mishchenko committed
719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759
#endif

} /* end of cuddPrintNode */



/**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.
  <ul>
  <li>F: MTR_FIXED
  <li>N: MTR_NEWNODE
  <li>S: MTR_SOFT
  </ul>
  The second argument, silent, if different from 0, causes
  Cudd_PrintVarGroups to only check the syntax of the group tree.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddPrintVarGroups(
  DdManager * dd /* manager */,
  MtrNode * root /* root of the group tree */,
  int zdd /* 0: BDD; 1: ZDD */,
  int silent /* flag to check tree syntax only */)
{
    MtrNode *node;
    int level;

    assert(root != NULL);
    assert(root->younger == NULL || root->younger->elder == root);
    assert(root->elder == NULL || root->elder->younger == root);
    if (zdd) {
760
        level = dd->permZ[root->index];
Alan Mishchenko committed
761
    } else {
762
        level = dd->perm[root->index];
Alan Mishchenko committed
763 764 765
    }
    if (!silent) (void) printf("(%d",level);
    if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
766
        if (!silent) (void) printf(",");
Alan Mishchenko committed
767
    } else {
768 769 770 771 772 773 774
        node = root->child;
        while (node != NULL) {
            assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
            assert(node->parent == root);
            cuddPrintVarGroups(dd,node,zdd,silent);
            node = node->younger;
        }
Alan Mishchenko committed
775 776
    }
    if (!silent) {
777 778 779 780 781 782 783 784 785
        (void) printf("%d", (int) (level + root->size - 1));
        if (root->flags != MTR_DEFAULT) {
            (void) printf("|");
            if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
            if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
            if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
        }
        (void) printf(")");
        if (root->parent == NULL) (void) printf("\n");
Alan Mishchenko committed
786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814
    }
    assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
    return;

} /* end of cuddPrintVarGroups */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

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

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
debugFindParent(
  DdManager * table,
  DdNode * node)
{
    int         i,j;
815 816 817 818
    int         slots;
    DdNodePtr   *nodelist;
    DdNode      *f;

Alan Mishchenko committed
819
    for (i = 0; i < cuddI(table,node->index); i++) {
820 821
        nodelist = table->subtables[i].nodelist;
        slots = table->subtables[i].slots;
Alan Mishchenko committed
822

823 824 825 826
        for (j=0;j<slots;j++) {
            f = nodelist[j];
            while (f != NULL) {
                if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) {
Alan Mishchenko committed
827
#if SIZEOF_VOID_P == 8
828 829
                    (void) fprintf(table->out,"parent is at 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",
                        (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
Alan Mishchenko committed
830
#else
831 832
                    (void) fprintf(table->out,"parent is at 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",
                        (ptruint)f,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
Alan Mishchenko committed
833
#endif
834 835 836
                }
                f = f->next;
            }
Alan Mishchenko committed
837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861
        }
    }

} /* end of debugFindParent */


#if 0
/**Function********************************************************************

  Synopsis    [Reports an error if a (dead) node has a non-dead parent.]

  Description [Searches all the subtables above node. Very expensive.
  The same check is now implemented more efficiently in ddDebugCheck.]

  SideEffects [None]

  SeeAlso     [debugFindParent]

******************************************************************************/
static void
debugCheckParent(
  DdManager * table,
  DdNode * node)
{
    int         i,j;
862 863
    int         slots;
    DdNode      **nodelist,*f;
Alan Mishchenko committed
864

865 866 867 868 869 870 871 872 873 874 875 876 877 878 879
    for (i = 0; i < cuddI(table,node->index); i++) {
        nodelist = table->subtables[i].nodelist;
        slots = table->subtables[i].slots;

        for (j=0;j<slots;j++) {
            f = nodelist[j];
            while (f != NULL) {
                if ((Cudd_Regular(cuddE(f)) == node || cuddT(f) == node) && f->ref != 0) {
                    (void) fprintf(table->err,
                                   "error with zero ref count\n");
                    (void) fprintf(table->err,"parent is 0x%x, id = %u, ref = %u, then = 0x%x, else = 0x%x\n",f,f->index,f->ref,cuddT(f),cuddE(f));
                    (void) fprintf(table->err,"child  is 0x%x, id = %u, ref = %u, then = 0x%x, else = 0x%x\n",node,node->index,node->ref,cuddT(node),cuddE(node));
                }
                f = f->next;
            }
Alan Mishchenko committed
880 881 882 883
        }
    }
}
#endif
884 885


886 887
ABC_NAMESPACE_IMPL_END