distr/cudd/cuddRef.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddRef.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions that manipulate the reference counts.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_Ref()
  12                     <li> Cudd_RecursiveDeref()
  13                     <li> Cudd_IterDerefBdd()
  14                     <li> Cudd_DelayedDerefBdd()
  15                     <li> Cudd_RecursiveDerefZdd()
  16                     <li> Cudd_Deref()
  17                     <li> Cudd_CheckZeroRef()
  18                     </ul>
  19                Internal procedures included in this module:
  20                     <ul>
  21                     <li> cuddReclaim()
  22                     <li> cuddReclaimZdd()
  23                     <li> cuddClearDeathRow()
  24                     <li> cuddShrinkDeathRow()
  25                     <li> cuddIsInDeathRow()
  26                     <li> cuddTimesInDeathRow()
  27                     </ul>
  28               ]
  29
  30   SeeAlso     []
  31
  32   Author      [Fabio Somenzi]
  33
  34   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  35
  36   All rights reserved.
  37
  38   Redistribution and use in source and binary forms, with or without
  39   modification, are permitted provided that the following conditions
  40   are met:
  41
  42   Redistributions of source code must retain the above copyright
  43   notice, this list of conditions and the following disclaimer.
  44
  45   Redistributions in binary form must reproduce the above copyright
  46   notice, this list of conditions and the following disclaimer in the
  47   documentation and/or other materials provided with the distribution.
  48
  49   Neither the name of the University of Colorado nor the names of its
  50   contributors may be used to endorse or promote products derived from
  51   this software without specific prior written permission.
  52
  53   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  54   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  55   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  56   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  57   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  58   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  59   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  60   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  61   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  62   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  63   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  64   POSSIBILITY OF SUCH DAMAGE.]
  65
  66 ******************************************************************************/
  67
  68 #include "util.h"
  69 #include "cuddInt.h"
  70
  71 /*---------------------------------------------------------------------------*/
  72 /* Constant declarations                                                     */
  73 /*---------------------------------------------------------------------------*/
  74
  75
  76 /*---------------------------------------------------------------------------*/
  77 /* Stucture declarations                                                     */
  78 /*---------------------------------------------------------------------------*/
  79
  80
  81 /*---------------------------------------------------------------------------*/
  82 /* Type declarations                                                         */
  83 /*---------------------------------------------------------------------------*/
  84
  85
  86 /*---------------------------------------------------------------------------*/
  87 /* Variable declarations                                                     */
  88 /*---------------------------------------------------------------------------*/
  89
  90 #ifndef lint
  91 static char rcsid[] DD_UNUSED = "$Id: cuddRef.c,v 1.28 2004/08/13 18:04:50 fabio Exp $";
  92 #endif
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Macro declarations                                                        */
  96 /*---------------------------------------------------------------------------*/
  97
  98
  99 /**AutomaticStart*************************************************************/
 100
 101 /*---------------------------------------------------------------------------*/
 102 /* Static function prototypes                                                */
 103 /*---------------------------------------------------------------------------*/
 104
 105 /**AutomaticEnd***************************************************************/
 106
 107
 108 /*---------------------------------------------------------------------------*/
 109 /* Definition of exported functions                                          */
 110 /*---------------------------------------------------------------------------*/
 111
 112 /**Function********************************************************************
 113
 114   Synopsis [Increases the reference count of a node, if it is not
 115   saturated.]
 116
 117   Description []
 118
 119   SideEffects [None]
 120
 121   SeeAlso     [Cudd_RecursiveDeref Cudd_Deref]
 122
 123 ******************************************************************************/
 124 void
 125 Cudd_Ref(
 126   DdNode * n)
 127 {
 128
 129     n = Cudd_Regular(n);
 130
 131     cuddSatInc(n->ref);
 132
 133 } /* end of Cudd_Ref */
 134
 135
 136 /**Function********************************************************************
 137
 138   Synopsis    [Decreases the reference count of node n.]
 139
 140   Description [Decreases the reference count of node n. If n dies,
 141   recursively decreases the reference counts of its children.  It is
 142   used to dispose of a DD that is no longer needed.]
 143
 144   SideEffects [None]
 145
 146   SeeAlso     [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]
 147
 148 ******************************************************************************/
 149 void
 150 Cudd_RecursiveDeref(
 151   DdManager * table,
 152   DdNode * n)
 153 {
 154     DdNode *N;
 155     int ord;
 156     DdNodePtr *stack = table->stack;
 157     int SP = 1;
 158
 159     unsigned int live = table->keys - table->dead;
 160     if (live > table->peakLiveNodes) {
 161         table->peakLiveNodes = live;
 162     }
 163
 164     N = Cudd_Regular(n);
 165
 166     do {
 167 #ifdef DD_DEBUG
 168         assert(N->ref != 0);
 169 #endif
 170
 171         if (N->ref == 1) {
 172             N->ref = 0;
 173             table->dead++;
 174 #ifdef DD_STATS
 175             table->nodesDropped++;
 176 #endif
 177             if (cuddIsConstant(N)) {
 178                 table->constants.dead++;
 179                 N = stack[--SP];
 180             } else {
 181                 ord = table->perm[N->index];
 182                 stack[SP++] = Cudd_Regular(cuddE(N));
 183                 table->subtables[ord].dead++;
 184                 N = cuddT(N);
 185             }
 186         } else {
 187             cuddSatDec(N->ref);
 188             N = stack[--SP];
 189         }
 190     } while (SP != 0);
 191
 192 } /* end of Cudd_RecursiveDeref */
 193
 194
 195 /**Function********************************************************************
 196
 197   Synopsis    [Decreases the reference count of BDD node n.]
 198
 199   Description [Decreases the reference count of node n. If n dies,
 200   recursively decreases the reference counts of its children.  It is
 201   used to dispose of a BDD that is no longer needed. It is more
 202   efficient than Cudd_RecursiveDeref, but it cannot be used on
 203   ADDs. The greater efficiency comes from being able to assume that no
 204   constant node will ever die as a result of a call to this
 205   procedure.]
 206
 207   SideEffects [None]
 208
 209   SeeAlso     [Cudd_RecursiveDeref Cudd_DelayedDerefBdd]
 210
 211 ******************************************************************************/
 212 void
 213 Cudd_IterDerefBdd(
 214   DdManager * table,
 215   DdNode * n)
 216 {
 217     DdNode *N;
 218     int ord;
 219     DdNodePtr *stack = table->stack;
 220     int SP = 1;
 221
 222     unsigned int live = table->keys - table->dead;
 223     if (live > table->peakLiveNodes) {
 224         table->peakLiveNodes = live;
 225     }
 226
 227     N = Cudd_Regular(n);
 228
 229     do {
 230 #ifdef DD_DEBUG
 231         assert(N->ref != 0);
 232 #endif
 233
 234         if (N->ref == 1) {
 235             N->ref = 0;
 236             table->dead++;
 237 #ifdef DD_STATS
 238             table->nodesDropped++;
 239 #endif
 240             ord = table->perm[N->index];
 241             stack[SP++] = Cudd_Regular(cuddE(N));
 242             table->subtables[ord].dead++;
 243             N = cuddT(N);
 244         } else {
 245             cuddSatDec(N->ref);
 246             N = stack[--SP];
 247         }
 248     } while (SP != 0);
 249
 250 } /* end of Cudd_IterDerefBdd */
 251
 252
 253 /**Function********************************************************************
 254
 255   Synopsis    [Decreases the reference count of BDD node n.]
 256
 257   Description [Enqueues node n for later dereferencing. If the queue
 258   is full decreases the reference count of the oldest node N to make
 259   room for n. If N dies, recursively decreases the reference counts of
 260   its children.  It is used to dispose of a BDD that is currently not
 261   needed, but may be useful again in the near future. The dereferencing
 262   proper is done as in Cudd_IterDerefBdd.]
 263
 264   SideEffects [None]
 265
 266   SeeAlso     [Cudd_RecursiveDeref Cudd_IterDerefBdd]
 267
 268 ******************************************************************************/
 269 void
 270 Cudd_DelayedDerefBdd(
 271   DdManager * table,
 272   DdNode * n)
 273 {
 274     DdNode *N;
 275     int ord;
 276     DdNodePtr *stack;
 277     int SP;
 278
 279     unsigned int live = table->keys - table->dead;
 280     if (live > table->peakLiveNodes) {
 281         table->peakLiveNodes = live;
 282     }
 283
 284     n = Cudd_Regular(n);
 285 #ifdef DD_DEBUG
 286     assert(n->ref != 0);
 287 #endif
 288
 289 #ifdef DD_NO_DEATH_ROW
 290     N = n;
 291 #else
 292     if (cuddIsConstant(n) || n->ref > 1) {
 293 #ifdef DD_DEBUG
 294         assert(n->ref != 1 && (!cuddIsConstant(n) || n == DD_ONE(table)));
 295 #endif
 296         cuddSatDec(n->ref);
 297         return;
 298     }
 299
 300     N = table->deathRow[table->nextDead];
 301
 302     if (N != NULL) {
 303 #endif
 304 #ifdef DD_DEBUG
 305         assert(!Cudd_IsComplement(N));
 306 #endif
 307         stack = table->stack;
 308         SP = 1;
 309         do {
 310 #ifdef DD_DEBUG
 311             assert(N->ref != 0);
 312 #endif
 313             if (N->ref == 1) {
 314                 N->ref = 0;
 315                 table->dead++;
 316 #ifdef DD_STATS
 317                 table->nodesDropped++;
 318 #endif
 319                 ord = table->perm[N->index];
 320                 stack[SP++] = Cudd_Regular(cuddE(N));
 321                 table->subtables[ord].dead++;
 322                 N = cuddT(N);
 323             } else {
 324                 cuddSatDec(N->ref);
 325                 N = stack[--SP];
 326             }
 327         } while (SP != 0);
 328 #ifndef DD_NO_DEATH_ROW
 329     }
 330     table->deathRow[table->nextDead] = n;
 331
 332     /* Udate insertion point. */
 333     table->nextDead++;
 334     table->nextDead &= table->deadMask;
 335 #if 0
 336     if (table->nextDead == table->deathRowDepth) {
 337         if (table->deathRowDepth < table->looseUpTo / 2) {
 338             extern void (*MMoutOfMemory)(long);
 339             void (*saveHandler)(long) = MMoutOfMemory;
 340             DdNodePtr *newRow;
 341             MMoutOfMemory = Cudd_OutOfMem;
 342             newRow = REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
 343             MMoutOfMemory = saveHandler;
 344             if (newRow == NULL) {
 345                 table->nextDead = 0;
 346             } else {
 347                 int i;
 348                 table->memused += table->deathRowDepth;
 349                 i = table->deathRowDepth;
 350                 table->deathRowDepth <<= 1;
 351                 for (; i < table->deathRowDepth; i++) {
 352                     newRow[i] = NULL;
 353                 }
 354                 table->deadMask = table->deathRowDepth - 1;
 355                 table->deathRow = newRow;
 356             }
 357         } else {
 358             table->nextDead = 0;
 359         }
 360     }
 361 #endif
 362 #endif
 363
 364 } /* end of Cudd_DelayedDerefBdd */
 365
 366
 367 /**Function********************************************************************
 368
 369   Synopsis    [Decreases the reference count of ZDD node n.]
 370
 371   Description [Decreases the reference count of ZDD node n. If n dies,
 372   recursively decreases the reference counts of its children.  It is
 373   used to dispose of a ZDD that is no longer needed.]
 374
 375   SideEffects [None]
 376
 377   SeeAlso     [Cudd_Deref Cudd_Ref Cudd_RecursiveDeref]
 378
 379 ******************************************************************************/
 380 void
 381 Cudd_RecursiveDerefZdd(
 382   DdManager * table,
 383   DdNode * n)
 384 {
 385     DdNode *N;
 386     int ord;
 387     DdNodePtr *stack = table->stack;
 388     int SP = 1;
 389
 390     N = n;
 391
 392     do {
 393 #ifdef DD_DEBUG
 394         assert(N->ref != 0);
 395 #endif
 396
 397         cuddSatDec(N->ref);
 398
 399         if (N->ref == 0) {
 400             table->deadZ++;
 401 #ifdef DD_STATS
 402             table->nodesDropped++;
 403 #endif
 404 #ifdef DD_DEBUG
 405             assert(!cuddIsConstant(N));
 406 #endif
 407             ord = table->permZ[N->index];
 408             stack[SP++] = cuddE(N);
 409             table->subtableZ[ord].dead++;
 410             N = cuddT(N);
 411         } else {
 412             N = stack[--SP];
 413         }
 414     } while (SP != 0);
 415
 416 } /* end of Cudd_RecursiveDerefZdd */
 417
 418
 419 /**Function********************************************************************
 420
 421   Synopsis    [Decreases the reference count of node.]
 422
 423   Description [Decreases the reference count of node. It is primarily
 424   used in recursive procedures to decrease the ref count of a result
 425   node before returning it. This accomplishes the goal of removing the
 426   protection applied by a previous Cudd_Ref.]
 427
 428   SideEffects [None]
 429
 430   SeeAlso     [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]
 431
 432 ******************************************************************************/
 433 void
 434 Cudd_Deref(
 435   DdNode * node)
 436 {
 437     node = Cudd_Regular(node);
 438     cuddSatDec(node->ref);
 439
 440 } /* end of Cudd_Deref */
 441
 442
 443 /**Function********************************************************************
 444
 445   Synopsis [Checks the unique table for nodes with non-zero reference
 446   counts.]
 447
 448   Description [Checks the unique table for nodes with non-zero
 449   reference counts. It is normally called before Cudd_Quit to make sure
 450   that there are no memory leaks due to missing Cudd_RecursiveDeref's.
 451   Takes into account that reference counts may saturate and that the
 452   basic constants and the projection functions are referenced by the
 453   manager.  Returns the number of nodes with non-zero reference count.
 454   (Except for the cases mentioned above.)]
 455
 456   SideEffects [None]
 457
 458   SeeAlso     []
 459
 460 ******************************************************************************/
 461 int
 462 Cudd_CheckZeroRef(
 463   DdManager * manager)
 464 {
 465     int size;
 466     int i, j;
 467     int remain; /* the expected number of remaining references to one */
 468     DdNodePtr *nodelist;
 469     DdNode *node;
 470     DdNode *sentinel = &(manager->sentinel);
 471     DdSubtable *subtable;
 472     int count = 0;
 473     int index;
 474
 475 #ifndef DD_NO_DEATH_ROW
 476     cuddClearDeathRow(manager);
 477 #endif
 478
 479     /* First look at the BDD/ADD subtables. */
 480     remain = 1; /* reference from the manager */
 481     size = manager->size;
 482     remain += 2 * size; /* reference from the BDD projection functions */
 483
 484     for (i = 0; i < size; i++) {
 485         subtable = &(manager->subtables[i]);
 486         nodelist = subtable->nodelist;
 487         for (j = 0; (unsigned) j < subtable->slots; j++) {
 488             node = nodelist[j];
 489             while (node != sentinel) {
 490                 if (node->ref != 0 && node->ref != DD_MAXREF) {
 491                     index = (int) node->index;
 492                     if (node != manager->vars[index]) {
 493                         count++;
 494                     } else {
 495                         if (node->ref != 1) {
 496                             count++;
 497                         }
 498                     }
 499                 }
 500                 node = node->next;
 501             }
 502         }
 503     }
 504
 505     /* Then look at the ZDD subtables. */
 506     size = manager->sizeZ;
 507     if (size) /* references from ZDD universe */
 508         remain += 2;
 509
 510     for (i = 0; i < size; i++) {
 511         subtable = &(manager->subtableZ[i]);
 512         nodelist = subtable->nodelist;
 513         for (j = 0; (unsigned) j < subtable->slots; j++) {
 514             node = nodelist[j];
 515             while (node != NULL) {
 516                 if (node->ref != 0 && node->ref != DD_MAXREF) {
 517                     index = (int) node->index;
 518                     if (node == manager->univ[manager->permZ[index]]) {
 519                         if (node->ref > 2) {
 520                             count++;
 521                         }
 522                     } else {
 523                         count++;
 524                     }
 525                 }
 526                 node = node->next;
 527             }
 528         }
 529     }
 530
 531     /* Now examine the constant table. Plusinfinity, minusinfinity, and
 532     ** zero are referenced by the manager. One is referenced by the
 533     ** manager, by the ZDD universe, and by all projection functions.
 534     ** All other nodes should have no references.
 535     */
 536     nodelist = manager->constants.nodelist;
 537     for (j = 0; (unsigned) j < manager->constants.slots; j++) {
 538         node = nodelist[j];
 539         while (node != NULL) {
 540             if (node->ref != 0 && node->ref != DD_MAXREF) {
 541                 if (node == manager->one) {
 542                     if ((int) node->ref != remain) {
 543                         count++;
 544                     }
 545                 } else if (node == manager->zero ||
 546                 node == manager->plusinfinity ||
 547                 node == manager->minusinfinity) {
 548                     if (node->ref != 1) {
 549                         count++;
 550                     }
 551                 } else {
 552                     count++;
 553                 }
 554             }
 555             node = node->next;
 556         }
 557     }
 558     return(count);
 559
 560 } /* end of Cudd_CheckZeroRef */
 561
 562
 563 /*---------------------------------------------------------------------------*/
 564 /* Definition of internal functions                                          */
 565 /*---------------------------------------------------------------------------*/
 566
 567
 568 /**Function********************************************************************
 569
 570   Synopsis    [Brings children of a dead node back.]
 571
 572   Description []
 573
 574   SideEffects [None]
 575
 576   SeeAlso     [cuddReclaimZdd]
 577
 578 ******************************************************************************/
 579 void
 580 cuddReclaim(
 581   DdManager * table,
 582   DdNode * n)
 583 {
 584     DdNode *N;
 585     int ord;
 586     DdNodePtr *stack = table->stack;
 587     int SP = 1;
 588     double initialDead = table->dead;
 589
 590     N = Cudd_Regular(n);
 591
 592 #ifdef DD_DEBUG
 593     assert(N->ref == 0);
 594 #endif
 595
 596     do {
 597         if (N->ref == 0) {
 598             N->ref = 1;
 599             table->dead--;
 600             if (cuddIsConstant(N)) {
 601                 table->constants.dead--;
 602                 N = stack[--SP];
 603             } else {
 604                 ord = table->perm[N->index];
 605                 stack[SP++] = Cudd_Regular(cuddE(N));
 606                 table->subtables[ord].dead--;
 607                 N = cuddT(N);
 608             }
 609         } else {
 610             cuddSatInc(N->ref);
 611             N = stack[--SP];
 612         }
 613     } while (SP != 0);
 614
 615     N = Cudd_Regular(n);
 616     cuddSatDec(N->ref);
 617     table->reclaimed += initialDead - table->dead;
 618
 619 } /* end of cuddReclaim */
 620
 621
 622 /**Function********************************************************************
 623
 624   Synopsis    [Brings children of a dead ZDD node back.]
 625
 626   Description []
 627
 628   SideEffects [None]
 629
 630   SeeAlso     [cuddReclaim]
 631
 632 ******************************************************************************/
 633 void
 634 cuddReclaimZdd(
 635   DdManager * table,
 636   DdNode * n)
 637 {
 638     DdNode *N;
 639     int ord;
 640     DdNodePtr *stack = table->stack;
 641     int SP = 1;
 642
 643     N = n;
 644
 645 #ifdef DD_DEBUG
 646     assert(N->ref == 0);
 647 #endif
 648
 649     do {
 650         cuddSatInc(N->ref);
 651
 652         if (N->ref == 1) {
 653             table->deadZ--;
 654             table->reclaimed++;
 655 #ifdef DD_DEBUG
 656             assert(!cuddIsConstant(N));
 657 #endif
 658             ord = table->permZ[N->index];
 659             stack[SP++] = cuddE(N);
 660             table->subtableZ[ord].dead--;
 661             N = cuddT(N);
 662         } else {
 663             N = stack[--SP];
 664         }
 665     } while (SP != 0);
 666
 667     cuddSatDec(n->ref);
 668
 669 } /* end of cuddReclaimZdd */
 670
 671
 672 /**Function********************************************************************
 673
 674   Synopsis    [Shrinks the death row.]
 675
 676   Description [Shrinks the death row by a factor of four.]
 677
 678   SideEffects [None]
 679
 680   SeeAlso     [cuddClearDeathRow]
 681
 682 ******************************************************************************/
 683 void
 684 cuddShrinkDeathRow(
 685   DdManager *table)
 686 {
 687 #ifndef DD_NO_DEATH_ROW
 688     int i;
 689
 690     if (table->deathRowDepth > 3) {
 691         for (i = table->deathRowDepth/4; i < table->deathRowDepth; i++) {
 692             if (table->deathRow[i] == NULL) break;
 693             Cudd_IterDerefBdd(table,table->deathRow[i]);
 694             table->deathRow[i] = NULL;
 695         }
 696         table->deathRowDepth /= 4;
 697         table->deadMask = table->deathRowDepth - 1;
 698         if ((unsigned) table->nextDead > table->deadMask) {
 699             table->nextDead = 0;
 700         }
 701         table->deathRow = REALLOC(DdNodePtr, table->deathRow,
 702                                    table->deathRowDepth);
 703     }
 704 #endif
 705
 706 } /* end of cuddShrinkDeathRow */
 707
 708
 709 /**Function********************************************************************
 710
 711   Synopsis    [Clears the death row.]
 712
 713   Description []
 714
 715   SideEffects [None]
 716
 717   SeeAlso     [Cudd_DelayedDerefBdd Cudd_IterDerefBdd Cudd_CheckZeroRef
 718   cuddGarbageCollect]
 719
 720 ******************************************************************************/
 721 void
 722 cuddClearDeathRow(
 723   DdManager *table)
 724 {
 725 #ifndef DD_NO_DEATH_ROW
 726     int i;
 727
 728     for (i = 0; i < table->deathRowDepth; i++) {
 729         if (table->deathRow[i] == NULL) break;
 730         Cudd_IterDerefBdd(table,table->deathRow[i]);
 731         table->deathRow[i] = NULL;
 732     }
 733 #ifdef DD_DEBUG
 734     for (; i < table->deathRowDepth; i++) {
 735         assert(table->deathRow[i] == NULL);
 736     }
 737 #endif
 738     table->nextDead = 0;
 739 #endif
 740
 741 } /* end of cuddClearDeathRow */
 742
 743
 744 /**Function********************************************************************
 745
 746   Synopsis    [Checks whether a node is in the death row.]
 747
 748   Description [Checks whether a node is in the death row. Returns the
 749   position of the first occurrence if the node is present; -1
 750   otherwise.]
 751
 752   SideEffects [None]
 753
 754   SeeAlso     [Cudd_DelayedDerefBdd cuddClearDeathRow]
 755
 756 ******************************************************************************/
 757 int
 758 cuddIsInDeathRow(
 759   DdManager *dd,
 760   DdNode *f)
 761 {
 762 #ifndef DD_NO_DEATH_ROW
 763     int i;
 764
 765     for (i = 0; i < dd->deathRowDepth; i++) {
 766         if (f == dd->deathRow[i]) {
 767             return(i);
 768         }
 769     }
 770 #endif
 771
 772     return(-1);
 773
 774 } /* end of cuddIsInDeathRow */
 775
 776
 777 /**Function********************************************************************
 778
 779   Synopsis    [Counts how many times a node is in the death row.]
 780
 781   Description []
 782
 783   SideEffects [None]
 784
 785   SeeAlso     [Cudd_DelayedDerefBdd cuddClearDeathRow cuddIsInDeathRow]
 786
 787 ******************************************************************************/
 788 int
 789 cuddTimesInDeathRow(
 790   DdManager *dd,
 791   DdNode *f)
 792 {
 793     int count = 0;
 794 #ifndef DD_NO_DEATH_ROW
 795     int i;
 796
 797     for (i = 0; i < dd->deathRowDepth; i++) {
 798         count += f == dd->deathRow[i];
 799     }
 800 #endif
 801
 802     return(count);
 803
 804 } /* end of cuddTimesInDeathRow */
 805
 806 /*---------------------------------------------------------------------------*/
 807 /* Definition of static functions                                            */
 808 /*---------------------------------------------------------------------------*/