source: vis_dev/glu-2.3/src/cuBdd/cuddRef.c @ 100

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

library glu 2.3
File size: 20.2 KB
Line 
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
91static 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******************************************************************************/
124void
125Cudd_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******************************************************************************/
149void
150Cudd_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******************************************************************************/
212void
213Cudd_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******************************************************************************/
269void
270Cudd_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******************************************************************************/
380void
381Cudd_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******************************************************************************/
433void
434Cudd_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******************************************************************************/
461int
462Cudd_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******************************************************************************/
579void
580cuddReclaim(
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******************************************************************************/
633void
634cuddReclaimZdd(
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******************************************************************************/
683void
684cuddShrinkDeathRow(
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******************************************************************************/
721void
722cuddClearDeathRow(
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******************************************************************************/
757int
758cuddIsInDeathRow(
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******************************************************************************/
788int
789cuddTimesInDeathRow(
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/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.