distr/cudd/cuddCheck.c

   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
  87 static 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
 101 static void debugFindParent (DdManager *table, DdNode *node);
 102 #if 0
 103 static 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 ******************************************************************************/
 137 int
 138 Cudd_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 ******************************************************************************/
 453 int
 454 Cudd_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 \
 508 in 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 \
 513 in 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 \
 543 in 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 \
 548 in 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 \
 575 in the constant table (difference=%d)\n", keys);
 576         count++;
 577     }
 578     if (dead != 0) {
 579         (void) fprintf(table->err, "Wrong number of dead found \
 580 in 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 ******************************************************************************/
 634 int
 635 cuddHeapProfile(
 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 ******************************************************************************/
 705 void
 706 cuddPrintNode(
 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 ******************************************************************************/
 742 void
 743 cuddPrintVarGroups(
 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 ******************************************************************************/
 805 static void
 806 debugFindParent(
 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 ******************************************************************************/
 852 static void
 853 debugCheckParent(
 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