source: vis_dev/glu-2.3/src/cuBdd/cuddTable.c @ 82

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

library glu 2.3
File size: 90.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddTable.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Unique table management functions.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_Prime()
12                </ul>
13        Internal procedures included in this module:
14                <ul>
15                <li> cuddAllocNode()
16                <li> cuddInitTable()
17                <li> cuddFreeTable()
18                <li> cuddGarbageCollect()
19                <li> cuddZddGetNode()
20                <li> cuddZddGetNodeIVO()
21                <li> cuddUniqueInter()
22                <li> cuddUniqueInterIVO()
23                <li> cuddUniqueInterZdd()
24                <li> cuddUniqueConst()
25                <li> cuddRehash()
26                <li> cuddShrinkSubtable()
27                <li> cuddInsertSubtables()
28                <li> cuddDestroySubtables()
29                <li> cuddResizeTableZdd()
30                <li> cuddSlowTableGrowth()
31                </ul>
32        Static procedures included in this module:
33                <ul>
34                <li> ddRehashZdd()
35                <li> ddResizeTable()
36                <li> cuddFindParent()
37                <li> cuddOrderedInsert()
38                <li> cuddOrderedThread()
39                <li> cuddRotateLeft()
40                <li> cuddRotateRight()
41                <li> cuddDoRebalance()
42                <li> cuddCheckCollisionOrdering()
43                </ul>]
44
45  SeeAlso     []
46
47  Author      [Fabio Somenzi]
48
49  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
50
51  All rights reserved.
52
53  Redistribution and use in source and binary forms, with or without
54  modification, are permitted provided that the following conditions
55  are met:
56
57  Redistributions of source code must retain the above copyright
58  notice, this list of conditions and the following disclaimer.
59
60  Redistributions in binary form must reproduce the above copyright
61  notice, this list of conditions and the following disclaimer in the
62  documentation and/or other materials provided with the distribution.
63
64  Neither the name of the University of Colorado nor the names of its
65  contributors may be used to endorse or promote products derived from
66  this software without specific prior written permission.
67
68  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
69  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
70  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
71  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
72  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
73  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
74  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
75  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
76  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
77  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
78  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
79  POSSIBILITY OF SUCH DAMAGE.]
80
81******************************************************************************/
82
83#include "util.h"
84#include "cuddInt.h"
85
86/*---------------------------------------------------------------------------*/
87/* Constant declarations                                                     */
88/*---------------------------------------------------------------------------*/
89
90#ifndef DD_UNSORTED_FREE_LIST
91#ifdef DD_RED_BLACK_FREE_LIST
92/* Constants for red/black trees. */
93#define DD_STACK_SIZE 128
94#define DD_RED   0
95#define DD_BLACK 1
96#define DD_PAGE_SIZE 8192
97#define DD_PAGE_MASK ~(DD_PAGE_SIZE - 1)
98#endif
99#endif
100
101/*---------------------------------------------------------------------------*/
102/* Stucture declarations                                                     */
103/*---------------------------------------------------------------------------*/
104
105/* This is a hack for when CUDD_VALUE_TYPE is double */
106typedef union hack {
107    CUDD_VALUE_TYPE value;
108    unsigned int bits[2];
109} hack;
110
111/*---------------------------------------------------------------------------*/
112/* Type declarations                                                         */
113/*---------------------------------------------------------------------------*/
114
115/*---------------------------------------------------------------------------*/
116/* Variable declarations                                                     */
117/*---------------------------------------------------------------------------*/
118
119#ifndef lint
120static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.122 2009/02/19 16:24:28 fabio Exp $";
121#endif
122
123/*---------------------------------------------------------------------------*/
124/* Macro declarations                                                        */
125/*---------------------------------------------------------------------------*/
126
127
128#ifndef DD_UNSORTED_FREE_LIST
129#ifdef DD_RED_BLACK_FREE_LIST
130/* Macros for red/black trees. */
131#define DD_INSERT_COMPARE(x,y) \
132        (((ptruint) (x) & DD_PAGE_MASK) - ((ptruint) (y) & DD_PAGE_MASK))
133#define DD_COLOR(p)  ((p)->index)
134#define DD_IS_BLACK(p) ((p)->index == DD_BLACK)
135#define DD_IS_RED(p) ((p)->index == DD_RED)
136#define DD_LEFT(p) cuddT(p)
137#define DD_RIGHT(p) cuddE(p)
138#define DD_NEXT(p) ((p)->next)
139#endif
140#endif
141
142
143/**AutomaticStart*************************************************************/
144
145/*---------------------------------------------------------------------------*/
146/* Static function prototypes                                                */
147/*---------------------------------------------------------------------------*/
148
149static void ddRehashZdd (DdManager *unique, int i);
150static int ddResizeTable (DdManager *unique, int index);
151static int cuddFindParent (DdManager *table, DdNode *node);
152DD_INLINE static void ddFixLimits (DdManager *unique);
153#ifdef DD_RED_BLACK_FREE_LIST
154static void cuddOrderedInsert (DdNodePtr *root, DdNodePtr node);
155static DdNode * cuddOrderedThread (DdNode *root, DdNode *list);
156static void cuddRotateLeft (DdNodePtr *nodeP);
157static void cuddRotateRight (DdNodePtr *nodeP);
158static void cuddDoRebalance (DdNodePtr **stack, int stackN);
159#endif
160static void ddPatchTree (DdManager *dd, MtrNode *treenode);
161#ifdef DD_DEBUG
162static int cuddCheckCollisionOrdering (DdManager *unique, int i, int j);
163#endif
164static void ddReportRefMess (DdManager *unique, int i, const char *caller);
165
166/**AutomaticEnd***************************************************************/
167
168
169/*---------------------------------------------------------------------------*/
170/* Definition of exported functions                                          */
171/*---------------------------------------------------------------------------*/
172
173
174/**Function********************************************************************
175
176  Synopsis    [Returns the next prime &gt;= p.]
177
178  Description []
179
180  SideEffects [None]
181
182******************************************************************************/
183unsigned int
184Cudd_Prime(
185  unsigned int  p)
186{
187    int i,pn;
188
189    p--;
190    do {
191        p++;
192        if (p&1) {
193            pn = 1;
194            i = 3;
195            while ((unsigned) (i * i) <= p) {
196                if (p % i == 0) {
197                    pn = 0;
198                    break;
199                }
200                i += 2;
201            }
202        } else {
203            pn = 0;
204        }
205    } while (!pn);
206    return(p);
207
208} /* end of Cudd_Prime */
209
210
211/*---------------------------------------------------------------------------*/
212/* Definition of internal functions                                          */
213/*---------------------------------------------------------------------------*/
214
215
216/**Function********************************************************************
217
218  Synopsis    [Fast storage allocation for DdNodes in the table.]
219
220  Description [Fast storage allocation for DdNodes in the table. The
221  first 4 bytes of a chunk contain a pointer to the next block; the
222  rest contains DD_MEM_CHUNK spaces for DdNodes.  Returns a pointer to
223  a new node if successful; NULL is memory is full.]
224
225  SideEffects [None]
226
227  SeeAlso     [cuddDynamicAllocNode]
228
229******************************************************************************/
230DdNode *
231cuddAllocNode(
232  DdManager * unique)
233{
234    int i;
235    DdNodePtr *mem;
236    DdNode *list, *node;
237    extern DD_OOMFP MMoutOfMemory;
238    DD_OOMFP saveHandler;
239
240    if (unique->nextFree == NULL) {     /* free list is empty */
241        /* Check for exceeded limits. */
242        if ((unique->keys - unique->dead) + (unique->keysZ - unique->deadZ) >
243            unique->maxLive) {
244            unique->errorCode = CUDD_TOO_MANY_NODES;
245            return(NULL);
246        }
247        if (unique->stash == NULL || unique->memused > unique->maxmemhard) {
248            (void) cuddGarbageCollect(unique,1);
249            mem = NULL;
250        }
251        if (unique->nextFree == NULL) {
252            if (unique->memused > unique->maxmemhard) {
253                unique->errorCode = CUDD_MAX_MEM_EXCEEDED;
254                return(NULL);
255            }
256            /* Try to allocate a new block. */
257            saveHandler = MMoutOfMemory;
258            MMoutOfMemory = Cudd_OutOfMem;
259            mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
260            MMoutOfMemory = saveHandler;
261            if (mem == NULL) {
262                /* No more memory: Try collecting garbage. If this succeeds,
263                ** we end up with mem still NULL, but unique->nextFree !=
264                ** NULL. */
265                if (cuddGarbageCollect(unique,1) == 0) {
266                    /* Last resort: Free the memory stashed away, if there
267                    ** any. If this succeeeds, mem != NULL and
268                    ** unique->nextFree still NULL. */
269                    if (unique->stash != NULL) {
270                        FREE(unique->stash);
271                        unique->stash = NULL;
272                        /* Inhibit resizing of tables. */
273                        cuddSlowTableGrowth(unique);
274                        /* Now try again. */
275                        mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
276                    }
277                    if (mem == NULL) {
278                        /* Out of luck. Call the default handler to do
279                        ** whatever it specifies for a failed malloc.
280                        ** If this handler returns, then set error code,
281                        ** print warning, and return. */
282                        (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1));
283                        unique->errorCode = CUDD_MEMORY_OUT;
284#ifdef DD_VERBOSE
285                        (void) fprintf(unique->err,
286                                       "cuddAllocNode: out of memory");
287                        (void) fprintf(unique->err, "Memory in use = %lu\n",
288                                       unique->memused);
289#endif
290                        return(NULL);
291                    }
292                }
293            }
294            if (mem != NULL) {  /* successful allocation; slice memory */
295                ptruint offset;
296                unique->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode);
297                mem[0] = (DdNodePtr) unique->memoryList;
298                unique->memoryList = mem;
299
300                /* Here we rely on the fact that a DdNode is as large
301                ** as 4 pointers.  */
302                offset = (ptruint) mem & (sizeof(DdNode) - 1);
303                mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
304                assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0);
305                list = (DdNode *) mem;
306
307                i = 1;
308                do {
309                    list[i - 1].ref = 0;
310                    list[i - 1].next = &list[i];
311                } while (++i < DD_MEM_CHUNK);
312
313                list[DD_MEM_CHUNK-1].ref = 0;
314                list[DD_MEM_CHUNK-1].next = NULL;
315
316                unique->nextFree = &list[0];
317            }
318        }
319    }
320    unique->allocated++;
321    node = unique->nextFree;
322    unique->nextFree = node->next;
323    return(node);
324
325} /* end of cuddAllocNode */
326
327
328/**Function********************************************************************
329
330  Synopsis    [Creates and initializes the unique table.]
331
332  Description [Creates and initializes the unique table. Returns a pointer
333  to the table if successful; NULL otherwise.]
334
335  SideEffects [None]
336
337  SeeAlso     [Cudd_Init cuddFreeTable]
338
339******************************************************************************/
340DdManager *
341cuddInitTable(
342  unsigned int numVars  /* Initial number of BDD variables (and subtables) */,
343  unsigned int numVarsZ /* Initial number of ZDD variables (and subtables) */,
344  unsigned int numSlots /* Initial size of the BDD subtables */,
345  unsigned int looseUpTo /* Limit for fast table growth */)
346{
347    DdManager   *unique = ALLOC(DdManager,1);
348    int         i, j;
349    DdNodePtr   *nodelist;
350    DdNode      *sentinel;
351    unsigned int slots;
352    int shift;
353
354    if (unique == NULL) {
355        return(NULL);
356    }
357    sentinel = &(unique->sentinel);
358    sentinel->ref = 0;
359    sentinel->index = 0;
360    cuddT(sentinel) = NULL;
361    cuddE(sentinel) = NULL;
362    sentinel->next = NULL;
363    unique->epsilon = DD_EPSILON;
364    unique->maxGrowth = DD_MAX_REORDER_GROWTH;
365    unique->maxGrowthAlt = 2.0 * DD_MAX_REORDER_GROWTH;
366    unique->reordCycle = 0;     /* do not use alternate threshold */
367    unique->size = numVars;
368    unique->sizeZ = numVarsZ;
369    unique->maxSize = ddMax(DD_DEFAULT_RESIZE, numVars);
370    unique->maxSizeZ = ddMax(DD_DEFAULT_RESIZE, numVarsZ);
371
372    /* Adjust the requested number of slots to a power of 2. */
373    slots = 8;
374    while (slots < numSlots) {
375        slots <<= 1;
376    }
377    unique->initSlots = slots;
378    shift = sizeof(int) * 8 - cuddComputeFloorLog2(slots);
379
380    unique->slots = (numVars + numVarsZ + 1) * slots;
381    unique->keys = 0;
382    unique->maxLive = ~0;       /* very large number */
383    unique->keysZ = 0;
384    unique->dead = 0;
385    unique->deadZ = 0;
386    unique->gcFrac = DD_GC_FRAC_HI;
387    unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
388    unique->looseUpTo = looseUpTo;
389    unique->gcEnabled = 1;
390    unique->allocated = 0;
391    unique->reclaimed = 0;
392    unique->subtables = ALLOC(DdSubtable,unique->maxSize);
393    if (unique->subtables == NULL) {
394        FREE(unique);
395        return(NULL);
396    }
397    unique->subtableZ = ALLOC(DdSubtable,unique->maxSizeZ);
398    if (unique->subtableZ == NULL) {
399        FREE(unique->subtables);
400        FREE(unique);
401        return(NULL);
402    }
403    unique->perm = ALLOC(int,unique->maxSize);
404    if (unique->perm == NULL) {
405        FREE(unique->subtables);
406        FREE(unique->subtableZ);
407        FREE(unique);
408        return(NULL);
409    }
410    unique->invperm = ALLOC(int,unique->maxSize);
411    if (unique->invperm == NULL) {
412        FREE(unique->subtables);
413        FREE(unique->subtableZ);
414        FREE(unique->perm);
415        FREE(unique);
416        return(NULL);
417    }
418    unique->permZ = ALLOC(int,unique->maxSizeZ);
419    if (unique->permZ == NULL) {
420        FREE(unique->subtables);
421        FREE(unique->subtableZ);
422        FREE(unique->perm);
423        FREE(unique->invperm);
424        FREE(unique);
425        return(NULL);
426    }
427    unique->invpermZ = ALLOC(int,unique->maxSizeZ);
428    if (unique->invpermZ == NULL) {
429        FREE(unique->subtables);
430        FREE(unique->subtableZ);
431        FREE(unique->perm);
432        FREE(unique->invperm);
433        FREE(unique->permZ);
434        FREE(unique);
435        return(NULL);
436    }
437    unique->map = NULL;
438    unique->stack = ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1);
439    if (unique->stack == NULL) {
440        FREE(unique->subtables);
441        FREE(unique->subtableZ);
442        FREE(unique->perm);
443        FREE(unique->invperm);
444        FREE(unique->permZ);
445        FREE(unique->invpermZ);
446        FREE(unique);
447        return(NULL);
448    }
449    unique->stack[0] = NULL; /* to suppress harmless UMR */
450
451#ifndef DD_NO_DEATH_ROW
452    unique->deathRowDepth = 1 << cuddComputeFloorLog2(unique->looseUpTo >> 2);
453    unique->deathRow = ALLOC(DdNodePtr,unique->deathRowDepth);
454    if (unique->deathRow == NULL) {
455        FREE(unique->subtables);
456        FREE(unique->subtableZ);
457        FREE(unique->perm);
458        FREE(unique->invperm);
459        FREE(unique->permZ);
460        FREE(unique->invpermZ);
461        FREE(unique->stack);
462        FREE(unique);
463        return(NULL);
464    }
465    for (i = 0; i < unique->deathRowDepth; i++) {
466        unique->deathRow[i] = NULL;
467    }
468    unique->nextDead = 0;
469    unique->deadMask = unique->deathRowDepth - 1;
470#endif
471
472    for (i = 0; (unsigned) i < numVars; i++) {
473        unique->subtables[i].slots = slots;
474        unique->subtables[i].shift = shift;
475        unique->subtables[i].keys = 0;
476        unique->subtables[i].dead = 0;
477        unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
478        unique->subtables[i].bindVar = 0;
479        unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
480        unique->subtables[i].pairIndex = 0;
481        unique->subtables[i].varHandled = 0;
482        unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE;
483
484        nodelist = unique->subtables[i].nodelist = ALLOC(DdNodePtr,slots);
485        if (nodelist == NULL) {
486            for (j = 0; j < i; j++) {
487                FREE(unique->subtables[j].nodelist);
488            }
489            FREE(unique->subtables);
490            FREE(unique->subtableZ);
491            FREE(unique->perm);
492            FREE(unique->invperm);
493            FREE(unique->permZ);
494            FREE(unique->invpermZ);
495            FREE(unique->stack);
496            FREE(unique);
497            return(NULL);
498        }
499        for (j = 0; (unsigned) j < slots; j++) {
500            nodelist[j] = sentinel;
501        }
502        unique->perm[i] = i;
503        unique->invperm[i] = i;
504    }
505    for (i = 0; (unsigned) i < numVarsZ; i++) {
506        unique->subtableZ[i].slots = slots;
507        unique->subtableZ[i].shift = shift;
508        unique->subtableZ[i].keys = 0;
509        unique->subtableZ[i].dead = 0;
510        unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
511        nodelist = unique->subtableZ[i].nodelist = ALLOC(DdNodePtr,slots);
512        if (nodelist == NULL) {
513            for (j = 0; (unsigned) j < numVars; j++) {
514                FREE(unique->subtables[j].nodelist);
515            }
516            FREE(unique->subtables);
517            for (j = 0; j < i; j++) {
518                FREE(unique->subtableZ[j].nodelist);
519            }
520            FREE(unique->subtableZ);
521            FREE(unique->perm);
522            FREE(unique->invperm);
523            FREE(unique->permZ);
524            FREE(unique->invpermZ);
525            FREE(unique->stack);
526            FREE(unique);
527            return(NULL);
528        }
529        for (j = 0; (unsigned) j < slots; j++) {
530            nodelist[j] = NULL;
531        }
532        unique->permZ[i] = i;
533        unique->invpermZ[i] = i;
534    }
535    unique->constants.slots = slots;
536    unique->constants.shift = shift;
537    unique->constants.keys = 0;
538    unique->constants.dead = 0;
539    unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
540    nodelist = unique->constants.nodelist = ALLOC(DdNodePtr,slots);
541    if (nodelist == NULL) {
542        for (j = 0; (unsigned) j < numVars; j++) {
543            FREE(unique->subtables[j].nodelist);
544        }
545        FREE(unique->subtables);
546        for (j = 0; (unsigned) j < numVarsZ; j++) {
547            FREE(unique->subtableZ[j].nodelist);
548        }
549        FREE(unique->subtableZ);
550        FREE(unique->perm);
551        FREE(unique->invperm);
552        FREE(unique->permZ);
553        FREE(unique->invpermZ);
554        FREE(unique->stack);
555        FREE(unique);
556        return(NULL);
557    }
558    for (j = 0; (unsigned) j < slots; j++) {
559        nodelist[j] = NULL;
560    }
561
562    unique->memoryList = NULL;
563    unique->nextFree = NULL;
564
565    unique->memused = sizeof(DdManager) + (unique->maxSize + unique->maxSizeZ)
566        * (sizeof(DdSubtable) + 2 * sizeof(int)) + (numVars + 1) *
567        slots * sizeof(DdNodePtr) +
568        (ddMax(unique->maxSize,unique->maxSizeZ) + 1) * sizeof(DdNodePtr);
569#ifndef DD_NO_DEATH_ROW
570    unique->memused += unique->deathRowDepth * sizeof(DdNodePtr);
571#endif
572
573    /* Initialize fields concerned with automatic dynamic reordering */
574    unique->reorderings = 0;
575    unique->autoDyn = 0;        /* initially disabled */
576    unique->autoDynZ = 0;       /* initially disabled */
577    unique->realign = 0;        /* initially disabled */
578    unique->realignZ = 0;       /* initially disabled */
579    unique->reordered = 0;
580    unique->autoMethod = CUDD_REORDER_SIFT;
581    unique->autoMethodZ = CUDD_REORDER_SIFT;
582    unique->nextDyn = DD_FIRST_REORDER;
583    unique->countDead = ~0;
584    unique->siftMaxVar = DD_SIFT_MAX_VAR;
585    unique->siftMaxSwap = DD_SIFT_MAX_SWAPS;
586    unique->tree = NULL;
587    unique->treeZ = NULL;
588    unique->groupcheck = CUDD_GROUP_CHECK7;
589    unique->recomb = DD_DEFAULT_RECOMB;
590    unique->symmviolation = 0;
591    unique->arcviolation = 0;
592    unique->populationSize = 0;
593    unique->numberXovers = 0;
594    unique->linear = NULL;
595    unique->linearSize = 0;
596
597    /* Initialize ZDD universe. */
598    unique->univ = (DdNodePtr *)NULL;
599
600    /* Initialize auxiliary fields. */
601    unique->localCaches = NULL;
602    unique->preGCHook = NULL;
603    unique->postGCHook = NULL;
604    unique->preReorderingHook = NULL;
605    unique->postReorderingHook = NULL;
606    unique->out = stdout;
607    unique->err = stderr;
608    unique->errorCode = CUDD_NO_ERROR;
609
610    /* Initialize statistical counters. */
611    unique->maxmemhard = ~ 0UL;
612    unique->garbageCollections = 0;
613    unique->GCTime = 0;
614    unique->reordTime = 0;
615#ifdef DD_STATS
616    unique->nodesDropped = 0;
617    unique->nodesFreed = 0;
618#endif
619    unique->peakLiveNodes = 0;
620#ifdef DD_UNIQUE_PROFILE
621    unique->uniqueLookUps = 0;
622    unique->uniqueLinks = 0;
623#endif
624#ifdef DD_COUNT
625    unique->recursiveCalls = 0;
626    unique->swapSteps = 0;
627#ifdef DD_STATS
628    unique->nextSample = 250000;
629#endif
630#endif
631
632    return(unique);
633
634} /* end of cuddInitTable */
635
636
637/**Function********************************************************************
638
639  Synopsis    [Frees the resources associated to a unique table.]
640
641  Description []
642
643  SideEffects [None]
644
645  SeeAlso     [cuddInitTable]
646
647******************************************************************************/
648void
649cuddFreeTable(
650  DdManager * unique)
651{
652    DdNodePtr *next;
653    DdNodePtr *memlist = unique->memoryList;
654    int i;
655
656    if (unique->univ != NULL) cuddZddFreeUniv(unique);
657    while (memlist != NULL) {
658        next = (DdNodePtr *) memlist[0];        /* link to next block */
659        FREE(memlist);
660        memlist = next;
661    }
662    unique->nextFree = NULL;
663    unique->memoryList = NULL;
664
665    for (i = 0; i < unique->size; i++) {
666        FREE(unique->subtables[i].nodelist);
667    }
668    for (i = 0; i < unique->sizeZ; i++) {
669        FREE(unique->subtableZ[i].nodelist);
670    }
671    FREE(unique->constants.nodelist);
672    FREE(unique->subtables);
673    FREE(unique->subtableZ);
674    FREE(unique->acache);
675    FREE(unique->perm);
676    FREE(unique->permZ);
677    FREE(unique->invperm);
678    FREE(unique->invpermZ);
679    FREE(unique->vars);
680    if (unique->map != NULL) FREE(unique->map);
681    FREE(unique->stack);
682#ifndef DD_NO_DEATH_ROW
683    FREE(unique->deathRow);
684#endif
685    if (unique->tree != NULL) Mtr_FreeTree(unique->tree);
686    if (unique->treeZ != NULL) Mtr_FreeTree(unique->treeZ);
687    if (unique->linear != NULL) FREE(unique->linear);
688    while (unique->preGCHook != NULL)
689        Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK);
690    while (unique->postGCHook != NULL)
691        Cudd_RemoveHook(unique,unique->postGCHook->f,CUDD_POST_GC_HOOK);
692    while (unique->preReorderingHook != NULL)
693        Cudd_RemoveHook(unique,unique->preReorderingHook->f,
694                        CUDD_PRE_REORDERING_HOOK);
695    while (unique->postReorderingHook != NULL)
696        Cudd_RemoveHook(unique,unique->postReorderingHook->f,
697                        CUDD_POST_REORDERING_HOOK);
698    FREE(unique);
699
700} /* end of cuddFreeTable */
701
702
703/**Function********************************************************************
704
705  Synopsis    [Performs garbage collection on the unique tables.]
706
707  Description [Performs garbage collection on the BDD and ZDD unique tables.
708  If clearCache is 0, the cache is not cleared. This should only be
709  specified if the cache has been cleared right before calling
710  cuddGarbageCollect. (As in the case of dynamic reordering.)
711  Returns the total number of deleted nodes.]
712
713  SideEffects [None]
714
715  SeeAlso     []
716
717******************************************************************************/
718int
719cuddGarbageCollect(
720  DdManager * unique,
721  int  clearCache)
722{
723    DdHook      *hook;
724    DdCache     *cache = unique->cache;
725    DdNode      *sentinel = &(unique->sentinel);
726    DdNodePtr   *nodelist;
727    int         i, j, deleted, totalDeleted, totalDeletedZ;
728    DdCache     *c;
729    DdNode      *node,*next;
730    DdNodePtr   *lastP;
731    int         slots;
732    long        localTime;
733#ifndef DD_UNSORTED_FREE_LIST
734#ifdef DD_RED_BLACK_FREE_LIST
735    DdNodePtr   tree;
736#else
737    DdNodePtr *memListTrav, *nxtNode;
738    DdNode *downTrav, *sentry;
739    int k;
740#endif
741#endif
742
743#ifndef DD_NO_DEATH_ROW
744    cuddClearDeathRow(unique);
745#endif
746
747    hook = unique->preGCHook;
748    while (hook != NULL) {
749        int res = (hook->f)(unique,"DD",NULL);
750        if (res == 0) return(0);
751        hook = hook->next;
752    }
753
754    if (unique->dead + unique->deadZ == 0) {
755        hook = unique->postGCHook;
756        while (hook != NULL) {
757            int res = (hook->f)(unique,"DD",NULL);
758            if (res == 0) return(0);
759            hook = hook->next;
760        }
761        return(0);
762    }
763
764    /* If many nodes are being reclaimed, we want to resize the tables
765    ** more aggressively, to reduce the frequency of garbage collection.
766    */
767    if (clearCache && unique->gcFrac == DD_GC_FRAC_LO &&
768        unique->slots <= unique->looseUpTo && unique->stash != NULL) {
769        unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
770#ifdef DD_VERBOSE
771        (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_HI);
772        (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
773#endif
774        unique->gcFrac = DD_GC_FRAC_HI;
775        return(0);
776    }
777
778    localTime = util_cpu_time();
779
780    unique->garbageCollections++;
781#ifdef DD_VERBOSE
782    (void) fprintf(unique->err,
783                   "garbage collecting (%d dead BDD nodes out of %d, min %d)...",
784                   unique->dead, unique->keys, unique->minDead);
785    (void) fprintf(unique->err,
786                   "                   (%d dead ZDD nodes out of %d)...",
787                   unique->deadZ, unique->keysZ);
788#endif
789
790    /* Remove references to garbage collected nodes from the cache. */
791    if (clearCache) {
792        slots = unique->cacheSlots;
793        for (i = 0; i < slots; i++) {
794            c = &cache[i];
795            if (c->data != NULL) {
796                if (cuddClean(c->f)->ref == 0 ||
797                cuddClean(c->g)->ref == 0 ||
798                (((ptruint)c->f & 0x2) && Cudd_Regular(c->h)->ref == 0) ||
799                (c->data != DD_NON_CONSTANT &&
800                Cudd_Regular(c->data)->ref == 0)) {
801                    c->data = NULL;
802                    unique->cachedeletions++;
803                }
804            }
805        }
806        cuddLocalCacheClearDead(unique);
807    }
808
809    /* Now return dead nodes to free list. Count them for sanity check. */
810    totalDeleted = 0;
811#ifndef DD_UNSORTED_FREE_LIST
812#ifdef DD_RED_BLACK_FREE_LIST
813    tree = NULL;
814#endif
815#endif
816
817    for (i = 0; i < unique->size; i++) {
818        if (unique->subtables[i].dead == 0) continue;
819        nodelist = unique->subtables[i].nodelist;
820
821        deleted = 0;
822        slots = unique->subtables[i].slots;
823        for (j = 0; j < slots; j++) {
824            lastP = &(nodelist[j]);
825            node = *lastP;
826            while (node != sentinel) {
827                next = node->next;
828                if (node->ref == 0) {
829                    deleted++;
830#ifndef DD_UNSORTED_FREE_LIST
831#ifdef DD_RED_BLACK_FREE_LIST
832#ifdef __osf__
833#pragma pointer_size save
834#pragma pointer_size short
835#endif
836                    cuddOrderedInsert(&tree,node);
837#ifdef __osf__
838#pragma pointer_size restore
839#endif
840#endif
841#else
842                    cuddDeallocNode(unique,node);
843#endif
844                } else {
845                    *lastP = node;
846                    lastP = &(node->next);
847                }
848                node = next;
849            }
850            *lastP = sentinel;
851        }
852        if ((unsigned) deleted != unique->subtables[i].dead) {
853            ddReportRefMess(unique, i, "cuddGarbageCollect");
854        }
855        totalDeleted += deleted;
856        unique->subtables[i].keys -= deleted;
857        unique->subtables[i].dead = 0;
858    }
859    if (unique->constants.dead != 0) {
860        nodelist = unique->constants.nodelist;
861        deleted = 0;
862        slots = unique->constants.slots;
863        for (j = 0; j < slots; j++) {
864            lastP = &(nodelist[j]);
865            node = *lastP;
866            while (node != NULL) {
867                next = node->next;
868                if (node->ref == 0) {
869                    deleted++;
870#ifndef DD_UNSORTED_FREE_LIST
871#ifdef DD_RED_BLACK_FREE_LIST
872#ifdef __osf__
873#pragma pointer_size save
874#pragma pointer_size short
875#endif
876                    cuddOrderedInsert(&tree,node);
877#ifdef __osf__
878#pragma pointer_size restore
879#endif
880#endif
881#else
882                    cuddDeallocNode(unique,node);
883#endif
884                } else {
885                    *lastP = node;
886                    lastP = &(node->next);
887                }
888                node = next;
889            }
890            *lastP = NULL;
891        }
892        if ((unsigned) deleted != unique->constants.dead) {
893            ddReportRefMess(unique, CUDD_CONST_INDEX, "cuddGarbageCollect");
894        }
895        totalDeleted += deleted;
896        unique->constants.keys -= deleted;
897        unique->constants.dead = 0;
898    }
899    if ((unsigned) totalDeleted != unique->dead) {
900        ddReportRefMess(unique, -1, "cuddGarbageCollect");
901    }
902    unique->keys -= totalDeleted;
903    unique->dead = 0;
904#ifdef DD_STATS
905    unique->nodesFreed += (double) totalDeleted;
906#endif
907
908    totalDeletedZ = 0;
909
910    for (i = 0; i < unique->sizeZ; i++) {
911        if (unique->subtableZ[i].dead == 0) continue;
912        nodelist = unique->subtableZ[i].nodelist;
913
914        deleted = 0;
915        slots = unique->subtableZ[i].slots;
916        for (j = 0; j < slots; j++) {
917            lastP = &(nodelist[j]);
918            node = *lastP;
919            while (node != NULL) {
920                next = node->next;
921                if (node->ref == 0) {
922                    deleted++;
923#ifndef DD_UNSORTED_FREE_LIST
924#ifdef DD_RED_BLACK_FREE_LIST
925#ifdef __osf__
926#pragma pointer_size save
927#pragma pointer_size short
928#endif
929                    cuddOrderedInsert(&tree,node);
930#ifdef __osf__
931#pragma pointer_size restore
932#endif
933#endif
934#else
935                    cuddDeallocNode(unique,node);
936#endif
937                } else {
938                    *lastP = node;
939                    lastP = &(node->next);
940                }
941                node = next;
942            }
943            *lastP = NULL;
944        }
945        if ((unsigned) deleted != unique->subtableZ[i].dead) {
946            ddReportRefMess(unique, i, "cuddGarbageCollect");
947        }
948        totalDeletedZ += deleted;
949        unique->subtableZ[i].keys -= deleted;
950        unique->subtableZ[i].dead = 0;
951    }
952
953    /* No need to examine the constant table for ZDDs.
954    ** If we did we should be careful not to count whatever dead
955    ** nodes we found there among the dead ZDD nodes. */
956    if ((unsigned) totalDeletedZ != unique->deadZ) {
957        ddReportRefMess(unique, -1, "cuddGarbageCollect");
958    }
959    unique->keysZ -= totalDeletedZ;
960    unique->deadZ = 0;
961#ifdef DD_STATS
962    unique->nodesFreed += (double) totalDeletedZ;
963#endif
964
965
966#ifndef DD_UNSORTED_FREE_LIST
967#ifdef DD_RED_BLACK_FREE_LIST
968    unique->nextFree = cuddOrderedThread(tree,unique->nextFree);
969#else
970    memListTrav = unique->memoryList;
971    sentry = NULL;
972    while (memListTrav != NULL) {
973        ptruint offset;
974        nxtNode = (DdNodePtr *)memListTrav[0];
975        offset = (ptruint) memListTrav & (sizeof(DdNode) - 1);
976        memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
977        downTrav = (DdNode *)memListTrav;
978        k = 0;
979        do {
980            if (downTrav[k].ref == 0) {
981                if (sentry == NULL) {
982                    unique->nextFree = sentry = &downTrav[k];
983                } else {
984                    /* First hook sentry->next to the dead node and then
985                    ** reassign sentry to the dead node. */
986                    sentry = (sentry->next = &downTrav[k]);
987                }
988            }
989        } while (++k < DD_MEM_CHUNK);
990        memListTrav = nxtNode;
991    }
992    sentry->next = NULL;
993#endif
994#endif
995
996    unique->GCTime += util_cpu_time() - localTime;
997
998    hook = unique->postGCHook;
999    while (hook != NULL) {
1000        int res = (hook->f)(unique,"DD",NULL);
1001        if (res == 0) return(0);
1002        hook = hook->next;
1003    }
1004
1005#ifdef DD_VERBOSE
1006    (void) fprintf(unique->err," done\n");
1007#endif
1008
1009    return(totalDeleted+totalDeletedZ);
1010
1011} /* end of cuddGarbageCollect */
1012
1013
1014/**Function********************************************************************
1015
1016  Synopsis [Wrapper for cuddUniqueInterZdd.]
1017
1018  Description [Wrapper for cuddUniqueInterZdd, which applies the ZDD
1019  reduction rule. Returns a pointer to the result node under normal
1020  conditions; NULL if reordering occurred or memory was exhausted.]
1021
1022  SideEffects [None]
1023
1024  SeeAlso     [cuddUniqueInterZdd]
1025
1026******************************************************************************/
1027DdNode *
1028cuddZddGetNode(
1029  DdManager * zdd,
1030  int  id,
1031  DdNode * T,
1032  DdNode * E)
1033{
1034    DdNode      *node;
1035
1036    if (T == DD_ZERO(zdd))
1037        return(E);
1038    node = cuddUniqueInterZdd(zdd, id, T, E);
1039    return(node);
1040
1041} /* end of cuddZddGetNode */
1042
1043
1044/**Function********************************************************************
1045
1046  Synopsis [Wrapper for cuddUniqueInterZdd that is independent of variable
1047  ordering.]
1048
1049  Description [Wrapper for cuddUniqueInterZdd that is independent of
1050  variable ordering (IVO). This function does not require parameter
1051  index to precede the indices of the top nodes of g and h in the
1052  variable order.  Returns a pointer to the result node under normal
1053  conditions; NULL if reordering occurred or memory was exhausted.]
1054
1055  SideEffects [None]
1056
1057  SeeAlso     [cuddZddGetNode cuddZddIsop]
1058
1059******************************************************************************/
1060DdNode *
1061cuddZddGetNodeIVO(
1062  DdManager * dd,
1063  int  index,
1064  DdNode * g,
1065  DdNode * h)
1066{
1067    DdNode      *f, *r, *t;
1068    DdNode      *zdd_one = DD_ONE(dd);
1069    DdNode      *zdd_zero = DD_ZERO(dd);
1070
1071    f = cuddUniqueInterZdd(dd, index, zdd_one, zdd_zero);
1072    if (f == NULL) {
1073        return(NULL);
1074    }
1075    cuddRef(f);
1076    t = cuddZddProduct(dd, f, g);
1077    if (t == NULL) {
1078        Cudd_RecursiveDerefZdd(dd, f);
1079        return(NULL);
1080    }
1081    cuddRef(t);
1082    Cudd_RecursiveDerefZdd(dd, f);
1083    r = cuddZddUnion(dd, t, h);
1084    if (r == NULL) {
1085        Cudd_RecursiveDerefZdd(dd, t);
1086        return(NULL);
1087    }
1088    cuddRef(r);
1089    Cudd_RecursiveDerefZdd(dd, t);
1090
1091    cuddDeref(r);
1092    return(r);
1093
1094} /* end of cuddZddGetNodeIVO */
1095
1096
1097/**Function********************************************************************
1098
1099  Synopsis    [Checks the unique table for the existence of an internal node.]
1100
1101  Description [Checks the unique table for the existence of an internal
1102  node. If it does not exist, it creates a new one.  Does not
1103  modify the reference count of whatever is returned.  A newly created
1104  internal node comes back with a reference count 0.  For a newly
1105  created node, increments the reference counts of what T and E point
1106  to.  Returns a pointer to the new node if successful; NULL if memory
1107  is exhausted or if reordering took place.]
1108
1109  SideEffects [None]
1110
1111  SeeAlso     [cuddUniqueInterZdd]
1112
1113******************************************************************************/
1114DdNode *
1115cuddUniqueInter(
1116  DdManager * unique,
1117  int  index,
1118  DdNode * T,
1119  DdNode * E)
1120{
1121    int pos;
1122    unsigned int level;
1123    int retval;
1124    DdNodePtr *nodelist;
1125    DdNode *looking;
1126    DdNodePtr *previousP;
1127    DdSubtable *subtable;
1128    int gcNumber;
1129
1130#ifdef DD_UNIQUE_PROFILE
1131    unique->uniqueLookUps++;
1132#endif
1133
1134    if (index >= unique->size) {
1135        if (!ddResizeTable(unique,index)) return(NULL);
1136    }
1137
1138    level = unique->perm[index];
1139    subtable = &(unique->subtables[level]);
1140
1141#ifdef DD_DEBUG
1142    assert(level < (unsigned) cuddI(unique,T->index));
1143    assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
1144#endif
1145
1146    pos = ddHash(T, E, subtable->shift);
1147    nodelist = subtable->nodelist;
1148    previousP = &(nodelist[pos]);
1149    looking = *previousP;
1150
1151    while (T < cuddT(looking)) {
1152        previousP = &(looking->next);
1153        looking = *previousP;
1154#ifdef DD_UNIQUE_PROFILE
1155        unique->uniqueLinks++;
1156#endif
1157    }
1158    while (T == cuddT(looking) && E < cuddE(looking)) {
1159        previousP = &(looking->next);
1160        looking = *previousP;
1161#ifdef DD_UNIQUE_PROFILE
1162        unique->uniqueLinks++;
1163#endif
1164    }
1165    if (T == cuddT(looking) && E == cuddE(looking)) {
1166        if (looking->ref == 0) {
1167            cuddReclaim(unique,looking);
1168        }
1169        return(looking);
1170    }
1171
1172    /* countDead is 0 if deads should be counted and ~0 if they should not. */
1173    if (unique->autoDyn &&
1174    unique->keys - (unique->dead & unique->countDead) >= unique->nextDyn) {
1175#ifdef DD_DEBUG
1176        retval = Cudd_DebugCheck(unique);
1177        if (retval != 0) return(NULL);
1178        retval = Cudd_CheckKeys(unique);
1179        if (retval != 0) return(NULL);
1180#endif
1181        retval = Cudd_ReduceHeap(unique,unique->autoMethod,10); /* 10 = whatever */
1182        if (retval == 0) unique->reordered = 2;
1183#ifdef DD_DEBUG
1184        retval = Cudd_DebugCheck(unique);
1185        if (retval != 0) unique->reordered = 2;
1186        retval = Cudd_CheckKeys(unique);
1187        if (retval != 0) unique->reordered = 2;
1188#endif
1189        return(NULL);
1190    }
1191
1192    if (subtable->keys > subtable->maxKeys) {
1193        if (unique->gcEnabled &&
1194            ((unique->dead > unique->minDead) ||
1195            ((unique->dead > unique->minDead / 2) &&
1196            (subtable->dead > subtable->keys * 0.95)))) { /* too many dead */
1197            (void) cuddGarbageCollect(unique,1);
1198        } else {
1199            cuddRehash(unique,(int)level);
1200        }
1201        /* Update pointer to insertion point. In the case of rehashing,
1202        ** the slot may have changed. In the case of garbage collection,
1203        ** the predecessor may have been dead. */
1204        pos = ddHash(T, E, subtable->shift);
1205        nodelist = subtable->nodelist;
1206        previousP = &(nodelist[pos]);
1207        looking = *previousP;
1208
1209        while (T < cuddT(looking)) {
1210            previousP = &(looking->next);
1211            looking = *previousP;
1212#ifdef DD_UNIQUE_PROFILE
1213            unique->uniqueLinks++;
1214#endif
1215        }
1216        while (T == cuddT(looking) && E < cuddE(looking)) {
1217            previousP = &(looking->next);
1218            looking = *previousP;
1219#ifdef DD_UNIQUE_PROFILE
1220            unique->uniqueLinks++;
1221#endif
1222        }
1223    }
1224
1225    gcNumber = unique->garbageCollections;
1226    looking = cuddAllocNode(unique);
1227    if (looking == NULL) {
1228        return(NULL);
1229    }
1230    unique->keys++;
1231    subtable->keys++;
1232
1233    if (gcNumber != unique->garbageCollections) {
1234        DdNode *looking2;
1235        pos = ddHash(T, E, subtable->shift);
1236        nodelist = subtable->nodelist;
1237        previousP = &(nodelist[pos]);
1238        looking2 = *previousP;
1239
1240        while (T < cuddT(looking2)) {
1241            previousP = &(looking2->next);
1242            looking2 = *previousP;
1243#ifdef DD_UNIQUE_PROFILE
1244            unique->uniqueLinks++;
1245#endif
1246        }
1247        while (T == cuddT(looking2) && E < cuddE(looking2)) {
1248            previousP = &(looking2->next);
1249            looking2 = *previousP;
1250#ifdef DD_UNIQUE_PROFILE
1251            unique->uniqueLinks++;
1252#endif
1253        }
1254    }
1255    looking->index = index;
1256    cuddT(looking) = T;
1257    cuddE(looking) = E;
1258    looking->next = *previousP;
1259    *previousP = looking;
1260    cuddSatInc(T->ref);         /* we know T is a regular pointer */
1261    cuddRef(E);
1262
1263#ifdef DD_DEBUG
1264    cuddCheckCollisionOrdering(unique,level,pos);
1265#endif
1266
1267    return(looking);
1268
1269} /* end of cuddUniqueInter */
1270
1271
1272/**Function********************************************************************
1273
1274  Synopsis [Wrapper for cuddUniqueInter that is independent of variable
1275  ordering.]
1276
1277  Description [Wrapper for cuddUniqueInter that is independent of
1278  variable ordering (IVO). This function does not require parameter
1279  index to precede the indices of the top nodes of T and E in the
1280  variable order.  Returns a pointer to the result node under normal
1281  conditions; NULL if reordering occurred or memory was exhausted.]
1282
1283  SideEffects [None]
1284
1285  SeeAlso     [cuddUniqueInter Cudd_MakeBddFromZddCover]
1286
1287******************************************************************************/
1288DdNode *
1289cuddUniqueInterIVO(
1290  DdManager * unique,
1291  int  index,
1292  DdNode * T,
1293  DdNode * E)
1294{
1295    DdNode *result;
1296    DdNode *v;
1297
1298    v = cuddUniqueInter(unique, index, DD_ONE(unique),
1299                        Cudd_Not(DD_ONE(unique)));
1300    if (v == NULL)
1301        return(NULL);
1302    cuddRef(v);
1303    result = cuddBddIteRecur(unique, v, T, E);
1304    Cudd_RecursiveDeref(unique, v);
1305    return(result);
1306}
1307
1308
1309/**Function********************************************************************
1310
1311  Synopsis    [Checks the unique table for the existence of an internal
1312  ZDD node.]
1313
1314  Description [Checks the unique table for the existence of an internal
1315  ZDD node. If it does not exist, it creates a new one.  Does not
1316  modify the reference count of whatever is returned.  A newly created
1317  internal node comes back with a reference count 0.  For a newly
1318  created node, increments the reference counts of what T and E point
1319  to.  Returns a pointer to the new node if successful; NULL if memory
1320  is exhausted or if reordering took place.]
1321
1322  SideEffects [None]
1323
1324  SeeAlso     [cuddUniqueInter]
1325
1326******************************************************************************/
1327DdNode *
1328cuddUniqueInterZdd(
1329  DdManager * unique,
1330  int  index,
1331  DdNode * T,
1332  DdNode * E)
1333{
1334    int pos;
1335    unsigned int level;
1336    int retval;
1337    DdNodePtr *nodelist;
1338    DdNode *looking;
1339    DdSubtable *subtable;
1340
1341#ifdef DD_UNIQUE_PROFILE
1342    unique->uniqueLookUps++;
1343#endif
1344
1345    if (index >= unique->sizeZ) {
1346        if (!cuddResizeTableZdd(unique,index)) return(NULL);
1347    }
1348
1349    level = unique->permZ[index];
1350    subtable = &(unique->subtableZ[level]);
1351
1352#ifdef DD_DEBUG
1353    assert(level < (unsigned) cuddIZ(unique,T->index));
1354    assert(level < (unsigned) cuddIZ(unique,Cudd_Regular(E)->index));
1355#endif
1356
1357    if (subtable->keys > subtable->maxKeys) {
1358        if (unique->gcEnabled && ((unique->deadZ > unique->minDead) ||
1359        (10 * subtable->dead > 9 * subtable->keys))) {  /* too many dead */
1360            (void) cuddGarbageCollect(unique,1);
1361        } else {
1362            ddRehashZdd(unique,(int)level);
1363        }
1364    }
1365
1366    pos = ddHash(T, E, subtable->shift);
1367    nodelist = subtable->nodelist;
1368    looking = nodelist[pos];
1369
1370    while (looking != NULL) {
1371        if (cuddT(looking) == T && cuddE(looking) == E) {
1372            if (looking->ref == 0) {
1373                cuddReclaimZdd(unique,looking);
1374            }
1375            return(looking);
1376        }
1377        looking = looking->next;
1378#ifdef DD_UNIQUE_PROFILE
1379        unique->uniqueLinks++;
1380#endif
1381    }
1382
1383    /* countDead is 0 if deads should be counted and ~0 if they should not. */
1384    if (unique->autoDynZ &&
1385    unique->keysZ - (unique->deadZ & unique->countDead) >= unique->nextDyn) {
1386#ifdef DD_DEBUG
1387        retval = Cudd_DebugCheck(unique);
1388        if (retval != 0) return(NULL);
1389        retval = Cudd_CheckKeys(unique);
1390        if (retval != 0) return(NULL);
1391#endif
1392        retval = Cudd_zddReduceHeap(unique,unique->autoMethodZ,10); /* 10 = whatever */
1393        if (retval == 0) unique->reordered = 2;
1394#ifdef DD_DEBUG
1395        retval = Cudd_DebugCheck(unique);
1396        if (retval != 0) unique->reordered = 2;
1397        retval = Cudd_CheckKeys(unique);
1398        if (retval != 0) unique->reordered = 2;
1399#endif
1400        return(NULL);
1401    }
1402
1403    unique->keysZ++;
1404    subtable->keys++;
1405
1406    looking = cuddAllocNode(unique);
1407    if (looking == NULL) return(NULL);
1408    looking->index = index;
1409    cuddT(looking) = T;
1410    cuddE(looking) = E;
1411    looking->next = nodelist[pos];
1412    nodelist[pos] = looking;
1413    cuddRef(T);
1414    cuddRef(E);
1415
1416    return(looking);
1417
1418} /* end of cuddUniqueInterZdd */
1419
1420
1421/**Function********************************************************************
1422
1423  Synopsis    [Checks the unique table for the existence of a constant node.]
1424
1425  Description [Checks the unique table for the existence of a constant node.
1426  If it does not exist, it creates a new one.  Does not
1427  modify the reference count of whatever is returned.  A newly created
1428  internal node comes back with a reference count 0.  Returns a
1429  pointer to the new node.]
1430
1431  SideEffects [None]
1432
1433******************************************************************************/
1434DdNode *
1435cuddUniqueConst(
1436  DdManager * unique,
1437  CUDD_VALUE_TYPE  value)
1438{
1439    int pos;
1440    DdNodePtr *nodelist;
1441    DdNode *looking;
1442    hack split;
1443
1444#ifdef DD_UNIQUE_PROFILE
1445    unique->uniqueLookUps++;
1446#endif
1447
1448    if (unique->constants.keys > unique->constants.maxKeys) {
1449        if (unique->gcEnabled && ((unique->dead > unique->minDead) ||
1450        (10 * unique->constants.dead > 9 * unique->constants.keys))) {  /* too many dead */
1451            (void) cuddGarbageCollect(unique,1);
1452        } else {
1453            cuddRehash(unique,CUDD_CONST_INDEX);
1454        }
1455    }
1456
1457    cuddAdjust(value); /* for the case of crippled infinities */
1458
1459    if (ddAbs(value) < unique->epsilon) {
1460        value = 0.0;
1461    }
1462    split.value = value;
1463
1464    pos = ddHash(split.bits[0], split.bits[1], unique->constants.shift);
1465    nodelist = unique->constants.nodelist;
1466    looking = nodelist[pos];
1467
1468    /* Here we compare values both for equality and for difference less
1469     * than epsilon. The first comparison is required when values are
1470     * infinite, since Infinity - Infinity is NaN and NaN < X is 0 for
1471     * every X.
1472     */
1473    while (looking != NULL) {
1474        if (looking->type.value == value ||
1475        ddEqualVal(looking->type.value,value,unique->epsilon)) {
1476            if (looking->ref == 0) {
1477                cuddReclaim(unique,looking);
1478            }
1479            return(looking);
1480        }
1481        looking = looking->next;
1482#ifdef DD_UNIQUE_PROFILE
1483        unique->uniqueLinks++;
1484#endif
1485    }
1486
1487    unique->keys++;
1488    unique->constants.keys++;
1489
1490    looking = cuddAllocNode(unique);
1491    if (looking == NULL) return(NULL);
1492    looking->index = CUDD_CONST_INDEX;
1493    looking->type.value = value;
1494    looking->next = nodelist[pos];
1495    nodelist[pos] = looking;
1496
1497    return(looking);
1498
1499} /* end of cuddUniqueConst */
1500
1501
1502/**Function********************************************************************
1503
1504  Synopsis    [Rehashes a unique subtable.]
1505
1506  Description [Doubles the size of a unique subtable and rehashes its
1507  contents.]
1508
1509  SideEffects [None]
1510
1511  SeeAlso     []
1512
1513******************************************************************************/
1514void
1515cuddRehash(
1516  DdManager * unique,
1517  int i)
1518{
1519    unsigned int slots, oldslots;
1520    int shift, oldshift;
1521    int j, pos;
1522    DdNodePtr *nodelist, *oldnodelist;
1523    DdNode *node, *next;
1524    DdNode *sentinel = &(unique->sentinel);
1525    hack split;
1526    extern DD_OOMFP MMoutOfMemory;
1527    DD_OOMFP saveHandler;
1528
1529    if (unique->gcFrac == DD_GC_FRAC_HI && unique->slots > unique->looseUpTo) {
1530        unique->gcFrac = DD_GC_FRAC_LO;
1531        unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots);
1532#ifdef DD_VERBOSE
1533        (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_LO);
1534        (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
1535#endif
1536    }
1537
1538    if (unique->gcFrac != DD_GC_FRAC_MIN && unique->memused > unique->maxmem) {
1539        unique->gcFrac = DD_GC_FRAC_MIN;
1540        unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots);
1541#ifdef DD_VERBOSE
1542        (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_MIN);
1543        (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
1544#endif
1545        cuddShrinkDeathRow(unique);
1546        if (cuddGarbageCollect(unique,1) > 0) return;
1547    }
1548
1549    if (i != CUDD_CONST_INDEX) {
1550        oldslots = unique->subtables[i].slots;
1551        oldshift = unique->subtables[i].shift;
1552        oldnodelist = unique->subtables[i].nodelist;
1553
1554        /* Compute the new size of the subtable. */
1555        slots = oldslots << 1;
1556        shift = oldshift - 1;
1557
1558        saveHandler = MMoutOfMemory;
1559        MMoutOfMemory = Cudd_OutOfMem;
1560        nodelist = ALLOC(DdNodePtr, slots);
1561        MMoutOfMemory = saveHandler;
1562        if (nodelist == NULL) {
1563            (void) fprintf(unique->err,
1564                           "Unable to resize subtable %d for lack of memory\n",
1565                           i);
1566            /* Prevent frequent resizing attempts. */
1567            (void) cuddGarbageCollect(unique,1);
1568            if (unique->stash != NULL) {
1569                FREE(unique->stash);
1570                unique->stash = NULL;
1571                /* Inhibit resizing of tables. */
1572                cuddSlowTableGrowth(unique);
1573            }
1574            return;
1575        }
1576        unique->subtables[i].nodelist = nodelist;
1577        unique->subtables[i].slots = slots;
1578        unique->subtables[i].shift = shift;
1579        unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1580
1581        /* Move the nodes from the old table to the new table.
1582        ** This code depends on the type of hash function.
1583        ** It assumes that the effect of doubling the size of the table
1584        ** is to retain one more bit of the 32-bit hash value.
1585        ** The additional bit is the LSB. */
1586        for (j = 0; (unsigned) j < oldslots; j++) {
1587            DdNodePtr *evenP, *oddP;
1588            node = oldnodelist[j];
1589            evenP = &(nodelist[j<<1]);
1590            oddP = &(nodelist[(j<<1)+1]);
1591            while (node != sentinel) {
1592                next = node->next;
1593                pos = ddHash(cuddT(node), cuddE(node), shift);
1594                if (pos & 1) {
1595                    *oddP = node;
1596                    oddP = &(node->next);
1597                } else {
1598                    *evenP = node;
1599                    evenP = &(node->next);
1600                }
1601                node = next;
1602            }
1603            *evenP = *oddP = sentinel;
1604        }
1605        FREE(oldnodelist);
1606
1607#ifdef DD_VERBOSE
1608        (void) fprintf(unique->err,
1609                       "rehashing layer %d: keys %d dead %d new size %d\n",
1610                       i, unique->subtables[i].keys,
1611                       unique->subtables[i].dead, slots);
1612#endif
1613    } else {
1614        oldslots = unique->constants.slots;
1615        oldshift = unique->constants.shift;
1616        oldnodelist = unique->constants.nodelist;
1617
1618        /* The constant subtable is never subjected to reordering.
1619        ** Therefore, when it is resized, it is because it has just
1620        ** reached the maximum load. We can safely just double the size,
1621        ** with no need for the loop we use for the other tables.
1622        */
1623        slots = oldslots << 1;
1624        shift = oldshift - 1;
1625        saveHandler = MMoutOfMemory;
1626        MMoutOfMemory = Cudd_OutOfMem;
1627        nodelist = ALLOC(DdNodePtr, slots);
1628        MMoutOfMemory = saveHandler;
1629        if (nodelist == NULL) {
1630            (void) fprintf(unique->err,
1631                           "Unable to resize constant subtable for lack of memory\n");
1632            (void) cuddGarbageCollect(unique,1);
1633            for (j = 0; j < unique->size; j++) {
1634                unique->subtables[j].maxKeys <<= 1;
1635            }
1636            unique->constants.maxKeys <<= 1;
1637            return;
1638        }
1639        unique->constants.slots = slots;
1640        unique->constants.shift = shift;
1641        unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1642        unique->constants.nodelist = nodelist;
1643        for (j = 0; (unsigned) j < slots; j++) {
1644            nodelist[j] = NULL;
1645        }
1646        for (j = 0; (unsigned) j < oldslots; j++) {
1647            node = oldnodelist[j];
1648            while (node != NULL) {
1649                next = node->next;
1650                split.value = cuddV(node);
1651                pos = ddHash(split.bits[0], split.bits[1], shift);
1652                node->next = nodelist[pos];
1653                nodelist[pos] = node;
1654                node = next;
1655            }
1656        }
1657        FREE(oldnodelist);
1658
1659#ifdef DD_VERBOSE
1660        (void) fprintf(unique->err,
1661                       "rehashing constants: keys %d dead %d new size %d\n",
1662                       unique->constants.keys,unique->constants.dead,slots);
1663#endif
1664    }
1665
1666    /* Update global data */
1667
1668    unique->memused += (slots - oldslots) * sizeof(DdNodePtr);
1669    unique->slots += (slots - oldslots);
1670    ddFixLimits(unique);
1671
1672} /* end of cuddRehash */
1673
1674
1675/**Function********************************************************************
1676
1677  Synopsis    [Shrinks a subtable.]
1678
1679  Description [Shrinks a subtable.]
1680
1681  SideEffects [None]
1682
1683  SeeAlso     [cuddRehash]
1684
1685******************************************************************************/
1686void
1687cuddShrinkSubtable(
1688  DdManager *unique,
1689  int i)
1690{
1691    int j;
1692    int shift, posn;
1693    DdNodePtr *nodelist, *oldnodelist;
1694    DdNode *node, *next;
1695    DdNode *sentinel = &(unique->sentinel);
1696    unsigned int slots, oldslots;
1697    extern DD_OOMFP MMoutOfMemory;
1698    DD_OOMFP saveHandler;
1699
1700    oldnodelist = unique->subtables[i].nodelist;
1701    oldslots = unique->subtables[i].slots;
1702    slots = oldslots >> 1;
1703    saveHandler = MMoutOfMemory;
1704    MMoutOfMemory = Cudd_OutOfMem;
1705    nodelist = ALLOC(DdNodePtr, slots);
1706    MMoutOfMemory = saveHandler;
1707    if (nodelist == NULL) {
1708        return;
1709    }
1710    unique->subtables[i].nodelist = nodelist;
1711    unique->subtables[i].slots = slots;
1712    unique->subtables[i].shift++;
1713    unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1714#ifdef DD_VERBOSE
1715    (void) fprintf(unique->err,
1716                   "shrunk layer %d (%d keys) from %d to %d slots\n",
1717                   i, unique->subtables[i].keys, oldslots, slots);
1718#endif
1719
1720    for (j = 0; (unsigned) j < slots; j++) {
1721        nodelist[j] = sentinel;
1722    }
1723    shift = unique->subtables[i].shift;
1724    for (j = 0; (unsigned) j < oldslots; j++) {
1725        node = oldnodelist[j];
1726        while (node != sentinel) {
1727            DdNode *looking, *T, *E;
1728            DdNodePtr *previousP;
1729            next = node->next;
1730            posn = ddHash(cuddT(node), cuddE(node), shift);
1731            previousP = &(nodelist[posn]);
1732            looking = *previousP;
1733            T = cuddT(node);
1734            E = cuddE(node);
1735            while (T < cuddT(looking)) {
1736                previousP = &(looking->next);
1737                looking = *previousP;
1738#ifdef DD_UNIQUE_PROFILE
1739                unique->uniqueLinks++;
1740#endif
1741            }
1742            while (T == cuddT(looking) && E < cuddE(looking)) {
1743                previousP = &(looking->next);
1744                looking = *previousP;
1745#ifdef DD_UNIQUE_PROFILE
1746                unique->uniqueLinks++;
1747#endif
1748            }
1749            node->next = *previousP;
1750            *previousP = node;
1751            node = next;
1752        }
1753    }
1754    FREE(oldnodelist);
1755
1756    unique->memused += ((long) slots - (long) oldslots) * sizeof(DdNode *);
1757    unique->slots += slots - oldslots;
1758    unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
1759    unique->cacheSlack = (int)
1760        ddMin(unique->maxCacheHard,DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots)
1761        - 2 * (int) unique->cacheSlots;
1762
1763} /* end of cuddShrinkSubtable */
1764
1765
1766/**Function********************************************************************
1767
1768  Synopsis [Inserts n new subtables in a unique table at level.]
1769
1770  Description [Inserts n new subtables in a unique table at level.
1771  The number n should be positive, and level should be an existing level.
1772  Returns 1 if successful; 0 otherwise.]
1773
1774  SideEffects [None]
1775
1776  SeeAlso     [cuddDestroySubtables]
1777
1778******************************************************************************/
1779int
1780cuddInsertSubtables(
1781  DdManager * unique,
1782  int  n,
1783  int  level)
1784{
1785    DdSubtable *newsubtables;
1786    DdNodePtr *newnodelist;
1787    DdNodePtr *newvars;
1788    DdNode *sentinel = &(unique->sentinel);
1789    int oldsize,newsize;
1790    int i,j,index,reorderSave;
1791    unsigned int numSlots = unique->initSlots;
1792    int *newperm, *newinvperm, *newmap;
1793    DdNode *one, *zero;
1794
1795#ifdef DD_DEBUG
1796    assert(n > 0 && level < unique->size);
1797#endif
1798
1799    oldsize = unique->size;
1800    /* Easy case: there is still room in the current table. */
1801    if (oldsize + n <= unique->maxSize) {
1802        /* Shift the tables at and below level. */
1803        for (i = oldsize - 1; i >= level; i--) {
1804            unique->subtables[i+n].slots    = unique->subtables[i].slots;
1805            unique->subtables[i+n].shift    = unique->subtables[i].shift;
1806            unique->subtables[i+n].keys     = unique->subtables[i].keys;
1807            unique->subtables[i+n].maxKeys  = unique->subtables[i].maxKeys;
1808            unique->subtables[i+n].dead     = unique->subtables[i].dead;
1809            unique->subtables[i+n].nodelist = unique->subtables[i].nodelist;
1810            unique->subtables[i+n].bindVar  = unique->subtables[i].bindVar;
1811            unique->subtables[i+n].varType  = unique->subtables[i].varType;
1812            unique->subtables[i+n].pairIndex  = unique->subtables[i].pairIndex;
1813            unique->subtables[i+n].varHandled = unique->subtables[i].varHandled;
1814            unique->subtables[i+n].varToBeGrouped =
1815                unique->subtables[i].varToBeGrouped;
1816
1817            index                           = unique->invperm[i];
1818            unique->invperm[i+n]            = index;
1819            unique->perm[index]            += n;
1820        }
1821        /* Create new subtables. */
1822        for (i = 0; i < n; i++) {
1823            unique->subtables[level+i].slots = numSlots;
1824            unique->subtables[level+i].shift = sizeof(int) * 8 -
1825                cuddComputeFloorLog2(numSlots);
1826            unique->subtables[level+i].keys = 0;
1827            unique->subtables[level+i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
1828            unique->subtables[level+i].dead = 0;
1829            unique->subtables[level+i].bindVar = 0;
1830            unique->subtables[level+i].varType = CUDD_VAR_PRIMARY_INPUT;
1831            unique->subtables[level+i].pairIndex = 0;
1832            unique->subtables[level+i].varHandled = 0;
1833            unique->subtables[level+i].varToBeGrouped = CUDD_LAZY_NONE;
1834
1835            unique->perm[oldsize+i] = level + i;
1836            unique->invperm[level+i] = oldsize + i;
1837            newnodelist = unique->subtables[level+i].nodelist =
1838                ALLOC(DdNodePtr, numSlots);
1839            if (newnodelist == NULL) {
1840                unique->errorCode = CUDD_MEMORY_OUT;
1841                return(0);
1842            }
1843            for (j = 0; (unsigned) j < numSlots; j++) {
1844                newnodelist[j] = sentinel;
1845            }
1846        }
1847        if (unique->map != NULL) {
1848            for (i = 0; i < n; i++) {
1849                unique->map[oldsize+i] = oldsize + i;
1850            }
1851        }
1852    } else {
1853        /* The current table is too small: we need to allocate a new,
1854        ** larger one; move all old subtables, and initialize the new
1855        ** subtables.
1856        */
1857        newsize = oldsize + n + DD_DEFAULT_RESIZE;
1858#ifdef DD_VERBOSE
1859        (void) fprintf(unique->err,
1860                       "Increasing the table size from %d to %d\n",
1861            unique->maxSize, newsize);
1862#endif
1863        /* Allocate memory for new arrays (except nodelists). */
1864        newsubtables = ALLOC(DdSubtable,newsize);
1865        if (newsubtables == NULL) {
1866            unique->errorCode = CUDD_MEMORY_OUT;
1867            return(0);
1868        }
1869        newvars = ALLOC(DdNodePtr,newsize);
1870        if (newvars == NULL) {
1871            unique->errorCode = CUDD_MEMORY_OUT;
1872            FREE(newsubtables);
1873            return(0);
1874        }
1875        newperm = ALLOC(int,newsize);
1876        if (newperm == NULL) {
1877            unique->errorCode = CUDD_MEMORY_OUT;
1878            FREE(newsubtables);
1879            FREE(newvars);
1880            return(0);
1881        }
1882        newinvperm = ALLOC(int,newsize);
1883        if (newinvperm == NULL) {
1884            unique->errorCode = CUDD_MEMORY_OUT;
1885            FREE(newsubtables);
1886            FREE(newvars);
1887            FREE(newperm);
1888            return(0);
1889        }
1890        if (unique->map != NULL) {
1891            newmap = ALLOC(int,newsize);
1892            if (newmap == NULL) {
1893                unique->errorCode = CUDD_MEMORY_OUT;
1894                FREE(newsubtables);
1895                FREE(newvars);
1896                FREE(newperm);
1897                FREE(newinvperm);
1898                return(0);
1899            }
1900            unique->memused += (newsize - unique->maxSize) * sizeof(int);
1901        }
1902        unique->memused += (newsize - unique->maxSize) * ((numSlots+1) *
1903            sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
1904        /* Copy levels before insertion points from old tables. */
1905        for (i = 0; i < level; i++) {
1906            newsubtables[i].slots = unique->subtables[i].slots;
1907            newsubtables[i].shift = unique->subtables[i].shift;
1908            newsubtables[i].keys = unique->subtables[i].keys;
1909            newsubtables[i].maxKeys = unique->subtables[i].maxKeys;
1910            newsubtables[i].dead = unique->subtables[i].dead;
1911            newsubtables[i].nodelist = unique->subtables[i].nodelist;
1912            newsubtables[i].bindVar = unique->subtables[i].bindVar;
1913            newsubtables[i].varType = unique->subtables[i].varType;
1914            newsubtables[i].pairIndex = unique->subtables[i].pairIndex;
1915            newsubtables[i].varHandled = unique->subtables[i].varHandled;
1916            newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped;
1917
1918            newvars[i] = unique->vars[i];
1919            newperm[i] = unique->perm[i];
1920            newinvperm[i] = unique->invperm[i];
1921        }
1922        /* Finish initializing permutation for new table to old one. */
1923        for (i = level; i < oldsize; i++) {
1924            newperm[i] = unique->perm[i];
1925        }
1926        /* Initialize new levels. */
1927        for (i = level; i < level + n; i++) {
1928            newsubtables[i].slots = numSlots;
1929            newsubtables[i].shift = sizeof(int) * 8 -
1930                cuddComputeFloorLog2(numSlots);
1931            newsubtables[i].keys = 0;
1932            newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
1933            newsubtables[i].dead = 0;
1934            newsubtables[i].bindVar = 0;
1935            newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
1936            newsubtables[i].pairIndex = 0;
1937            newsubtables[i].varHandled = 0;
1938            newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE;
1939
1940            newperm[oldsize + i - level] = i;
1941            newinvperm[i] = oldsize + i - level;
1942            newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
1943            if (newnodelist == NULL) {
1944                /* We are going to leak some memory.  We should clean up. */
1945                unique->errorCode = CUDD_MEMORY_OUT;
1946                return(0);
1947            }
1948            for (j = 0; (unsigned) j < numSlots; j++) {
1949                newnodelist[j] = sentinel;
1950            }
1951        }
1952        /* Copy the old tables for levels past the insertion point. */
1953        for (i = level; i < oldsize; i++) {
1954            newsubtables[i+n].slots    = unique->subtables[i].slots;
1955            newsubtables[i+n].shift    = unique->subtables[i].shift;
1956            newsubtables[i+n].keys     = unique->subtables[i].keys;
1957            newsubtables[i+n].maxKeys  = unique->subtables[i].maxKeys;
1958            newsubtables[i+n].dead     = unique->subtables[i].dead;
1959            newsubtables[i+n].nodelist = unique->subtables[i].nodelist;
1960            newsubtables[i+n].bindVar  = unique->subtables[i].bindVar;
1961            newsubtables[i+n].varType  = unique->subtables[i].varType;
1962            newsubtables[i+n].pairIndex  = unique->subtables[i].pairIndex;
1963            newsubtables[i+n].varHandled  = unique->subtables[i].varHandled;
1964            newsubtables[i+n].varToBeGrouped  =
1965                unique->subtables[i].varToBeGrouped;
1966
1967            newvars[i]                 = unique->vars[i];
1968            index                      = unique->invperm[i];
1969            newinvperm[i+n]            = index;
1970            newperm[index]            += n;
1971        }
1972        /* Update the map. */
1973        if (unique->map != NULL) {
1974            for (i = 0; i < oldsize; i++) {
1975                newmap[i] = unique->map[i];
1976            }
1977            for (i = oldsize; i < oldsize + n; i++) {
1978                newmap[i] = i;
1979            }
1980            FREE(unique->map);
1981            unique->map = newmap;
1982        }
1983        /* Install the new tables and free the old ones. */
1984        FREE(unique->subtables);
1985        unique->subtables = newsubtables;
1986        unique->maxSize = newsize;
1987        FREE(unique->vars);
1988        unique->vars = newvars;
1989        FREE(unique->perm);
1990        unique->perm = newperm;
1991        FREE(unique->invperm);
1992        unique->invperm = newinvperm;
1993        /* Update the stack for iterative procedures. */
1994        if (newsize > unique->maxSizeZ) {
1995            FREE(unique->stack);
1996            unique->stack = ALLOC(DdNodePtr,newsize + 1);
1997            if (unique->stack == NULL) {
1998                unique->errorCode = CUDD_MEMORY_OUT;
1999                return(0);
2000            }
2001            unique->stack[0] = NULL; /* to suppress harmless UMR */
2002            unique->memused +=
2003                (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
2004                * sizeof(DdNode *);
2005        }
2006    }
2007    /* Update manager parameters to account for the new subtables. */
2008    unique->slots += n * numSlots;
2009    ddFixLimits(unique);
2010    unique->size += n;
2011
2012    /* Now that the table is in a coherent state, create the new
2013    ** projection functions. We need to temporarily disable reordering,
2014    ** because we cannot reorder without projection functions in place.
2015    **/
2016    one = unique->one;
2017    zero = Cudd_Not(one);
2018
2019    reorderSave = unique->autoDyn;
2020    unique->autoDyn = 0;
2021    for (i = oldsize; i < oldsize + n; i++) {
2022        unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
2023        if (unique->vars[i] == NULL) {
2024            unique->autoDyn = reorderSave;
2025            /* Shift everything back so table remains coherent. */
2026            for (j = oldsize; j < i; j++) {
2027                Cudd_IterDerefBdd(unique,unique->vars[j]);
2028                cuddDeallocNode(unique,unique->vars[j]);
2029                unique->vars[j] = NULL;
2030            }
2031            for (j = level; j < oldsize; j++) {
2032                unique->subtables[j].slots    = unique->subtables[j+n].slots;
2033                unique->subtables[j].slots    = unique->subtables[j+n].slots;
2034                unique->subtables[j].shift    = unique->subtables[j+n].shift;
2035                unique->subtables[j].keys     = unique->subtables[j+n].keys;
2036                unique->subtables[j].maxKeys  =
2037                    unique->subtables[j+n].maxKeys;
2038                unique->subtables[j].dead     = unique->subtables[j+n].dead;
2039                FREE(unique->subtables[j].nodelist);
2040                unique->subtables[j].nodelist =
2041                    unique->subtables[j+n].nodelist;
2042                unique->subtables[j+n].nodelist = NULL;
2043                unique->subtables[j].bindVar  =
2044                    unique->subtables[j+n].bindVar;
2045                unique->subtables[j].varType  =
2046                    unique->subtables[j+n].varType;
2047                unique->subtables[j].pairIndex =
2048                    unique->subtables[j+n].pairIndex;
2049                unique->subtables[j].varHandled =
2050                    unique->subtables[j+n].varHandled;
2051                unique->subtables[j].varToBeGrouped =
2052                    unique->subtables[j+n].varToBeGrouped;
2053                index                         = unique->invperm[j+n];
2054                unique->invperm[j]            = index;
2055                unique->perm[index]          -= n;
2056            }
2057            unique->size = oldsize;
2058            unique->slots -= n * numSlots;
2059            ddFixLimits(unique);
2060            (void) Cudd_DebugCheck(unique);
2061            return(0);
2062        }
2063        cuddRef(unique->vars[i]);
2064    }
2065    if (unique->tree != NULL) {
2066        unique->tree->size += n;
2067        unique->tree->index = unique->invperm[0];
2068        ddPatchTree(unique,unique->tree);
2069    }
2070    unique->autoDyn = reorderSave;
2071
2072    return(1);
2073
2074} /* end of cuddInsertSubtables */
2075
2076
2077/**Function********************************************************************
2078
2079  Synopsis [Destroys the n most recently created subtables in a unique table.]
2080
2081  Description [Destroys the n most recently created subtables in a unique
2082  table.  n should be positive. The subtables should not contain any live
2083  nodes, except the (isolated) projection function. The projection
2084  functions are freed.  Returns 1 if successful; 0 otherwise.]
2085
2086  SideEffects [The variable map used for fast variable substitution is
2087  destroyed if it exists. In this case the cache is also cleared.]
2088
2089  SeeAlso     [cuddInsertSubtables Cudd_SetVarMap]
2090
2091******************************************************************************/
2092int
2093cuddDestroySubtables(
2094  DdManager * unique,
2095  int  n)
2096{
2097    DdSubtable *subtables;
2098    DdNodePtr *nodelist;
2099    DdNodePtr *vars;
2100    int firstIndex, lastIndex;
2101    int index, level, newlevel;
2102    int lowestLevel;
2103    int shift;
2104    int found;
2105
2106    /* Sanity check and set up. */
2107    if (n <= 0) return(0);
2108    if (n > unique->size) n = unique->size;
2109
2110    subtables = unique->subtables;
2111    vars = unique->vars;
2112    firstIndex = unique->size - n;
2113    lastIndex  = unique->size;
2114
2115    /* Check for nodes labeled by the variables being destroyed
2116    ** that may still be in use.  It is allowed to destroy a variable
2117    ** only if there are no such nodes. Also, find the lowest level
2118    ** among the variables being destroyed. This will make further
2119    ** processing more efficient.
2120    */
2121    lowestLevel = unique->size;
2122    for (index = firstIndex; index < lastIndex; index++) {
2123        level = unique->perm[index];
2124        if (level < lowestLevel) lowestLevel = level;
2125        nodelist = subtables[level].nodelist;
2126        if (subtables[level].keys - subtables[level].dead != 1) return(0);
2127        /* The projection function should be isolated. If the ref count
2128        ** is 1, everything is OK. If the ref count is saturated, then
2129        ** we need to make sure that there are no nodes pointing to it.
2130        ** As for the external references, we assume the application is
2131        ** responsible for them.
2132        */
2133        if (vars[index]->ref != 1) {
2134            if (vars[index]->ref != DD_MAXREF) return(0);
2135            found = cuddFindParent(unique,vars[index]);
2136            if (found) {
2137                return(0);
2138            } else {
2139                vars[index]->ref = 1;
2140            }
2141        }
2142        Cudd_RecursiveDeref(unique,vars[index]);
2143    }
2144
2145    /* Collect garbage, because we cannot afford having dead nodes pointing
2146    ** to the dead nodes in the subtables being destroyed.
2147    */
2148    (void) cuddGarbageCollect(unique,1);
2149
2150    /* Here we know we can destroy our subtables. */
2151    for (index = firstIndex; index < lastIndex; index++) {
2152        level = unique->perm[index];
2153        nodelist = subtables[level].nodelist;
2154#ifdef DD_DEBUG
2155        assert(subtables[level].keys == 0);
2156#endif
2157        FREE(nodelist);
2158        unique->memused -= sizeof(DdNodePtr) * subtables[level].slots;
2159        unique->slots -= subtables[level].slots;
2160        unique->dead -= subtables[level].dead;
2161    }
2162
2163    /* Here all subtables to be destroyed have their keys field == 0 and
2164    ** their hash tables have been freed.
2165    ** We now scan the subtables from level lowestLevel + 1 to level size - 1,
2166    ** shifting the subtables as required. We keep a running count of
2167    ** how many subtables have been moved, so that we know by how many
2168    ** positions each subtable should be shifted.
2169    */
2170    shift = 1;
2171    for (level = lowestLevel + 1; level < unique->size; level++) {
2172        if (subtables[level].keys == 0) {
2173            shift++;
2174            continue;
2175        }
2176        newlevel = level - shift;
2177        subtables[newlevel].slots = subtables[level].slots;
2178        subtables[newlevel].shift = subtables[level].shift;
2179        subtables[newlevel].keys = subtables[level].keys;
2180        subtables[newlevel].maxKeys = subtables[level].maxKeys;
2181        subtables[newlevel].dead = subtables[level].dead;
2182        subtables[newlevel].nodelist = subtables[level].nodelist;
2183        index = unique->invperm[level];
2184        unique->perm[index] = newlevel;
2185        unique->invperm[newlevel]  = index;
2186        subtables[newlevel].bindVar = subtables[level].bindVar;
2187        subtables[newlevel].varType = subtables[level].varType;
2188        subtables[newlevel].pairIndex = subtables[level].pairIndex;
2189        subtables[newlevel].varHandled = subtables[level].varHandled;
2190        subtables[newlevel].varToBeGrouped = subtables[level].varToBeGrouped;
2191    }
2192    /* Destroy the map. If a surviving variable is
2193    ** mapped to a dying variable, and the map were used again,
2194    ** an out-of-bounds access to unique->vars would result. */
2195    if (unique->map != NULL) {
2196        cuddCacheFlush(unique);
2197        FREE(unique->map);
2198        unique->map = NULL;
2199    }
2200
2201    unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
2202    unique->size -= n;
2203
2204    return(1);
2205
2206} /* end of cuddDestroySubtables */
2207
2208
2209/**Function********************************************************************
2210
2211  Synopsis [Increases the number of ZDD subtables in a unique table so
2212  that it meets or exceeds index.]
2213
2214  Description [Increases the number of ZDD subtables in a unique table so
2215  that it meets or exceeds index.  When new ZDD variables are created, it
2216  is possible to preserve the functions unchanged, or it is possible to
2217  preserve the covers unchanged, but not both. cuddResizeTableZdd preserves
2218  the covers.  Returns 1 if successful; 0 otherwise.]
2219
2220  SideEffects [None]
2221
2222  SeeAlso     [ddResizeTable]
2223
2224******************************************************************************/
2225int
2226cuddResizeTableZdd(
2227  DdManager * unique,
2228  int  index)
2229{
2230    DdSubtable *newsubtables;
2231    DdNodePtr *newnodelist;
2232    int oldsize,newsize;
2233    int i,j,reorderSave;
2234    unsigned int numSlots = unique->initSlots;
2235    int *newperm, *newinvperm;
2236
2237    oldsize = unique->sizeZ;
2238    /* Easy case: there is still room in the current table. */
2239    if (index < unique->maxSizeZ) {
2240        for (i = oldsize; i <= index; i++) {
2241            unique->subtableZ[i].slots = numSlots;
2242            unique->subtableZ[i].shift = sizeof(int) * 8 -
2243                cuddComputeFloorLog2(numSlots);
2244            unique->subtableZ[i].keys = 0;
2245            unique->subtableZ[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2246            unique->subtableZ[i].dead = 0;
2247            unique->permZ[i] = i;
2248            unique->invpermZ[i] = i;
2249            newnodelist = unique->subtableZ[i].nodelist =
2250                ALLOC(DdNodePtr, numSlots);
2251            if (newnodelist == NULL) {
2252                unique->errorCode = CUDD_MEMORY_OUT;
2253                return(0);
2254            }
2255            for (j = 0; (unsigned) j < numSlots; j++) {
2256                newnodelist[j] = NULL;
2257            }
2258        }
2259    } else {
2260        /* The current table is too small: we need to allocate a new,
2261        ** larger one; move all old subtables, and initialize the new
2262        ** subtables up to index included.
2263        */
2264        newsize = index + DD_DEFAULT_RESIZE;
2265#ifdef DD_VERBOSE
2266        (void) fprintf(unique->err,
2267                       "Increasing the ZDD table size from %d to %d\n",
2268            unique->maxSizeZ, newsize);
2269#endif
2270        newsubtables = ALLOC(DdSubtable,newsize);
2271        if (newsubtables == NULL) {
2272            unique->errorCode = CUDD_MEMORY_OUT;
2273            return(0);
2274        }
2275        newperm = ALLOC(int,newsize);
2276        if (newperm == NULL) {
2277            unique->errorCode = CUDD_MEMORY_OUT;
2278            return(0);
2279        }
2280        newinvperm = ALLOC(int,newsize);
2281        if (newinvperm == NULL) {
2282            unique->errorCode = CUDD_MEMORY_OUT;
2283            return(0);
2284        }
2285        unique->memused += (newsize - unique->maxSizeZ) * ((numSlots+1) *
2286            sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
2287        if (newsize > unique->maxSize) {
2288            FREE(unique->stack);
2289            unique->stack = ALLOC(DdNodePtr,newsize + 1);
2290            if (unique->stack == NULL) {
2291                unique->errorCode = CUDD_MEMORY_OUT;
2292                return(0);
2293            }
2294            unique->stack[0] = NULL; /* to suppress harmless UMR */
2295            unique->memused +=
2296                (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
2297                * sizeof(DdNode *);
2298        }
2299        for (i = 0; i < oldsize; i++) {
2300            newsubtables[i].slots = unique->subtableZ[i].slots;
2301            newsubtables[i].shift = unique->subtableZ[i].shift;
2302            newsubtables[i].keys = unique->subtableZ[i].keys;
2303            newsubtables[i].maxKeys = unique->subtableZ[i].maxKeys;
2304            newsubtables[i].dead = unique->subtableZ[i].dead;
2305            newsubtables[i].nodelist = unique->subtableZ[i].nodelist;
2306            newperm[i] = unique->permZ[i];
2307            newinvperm[i] = unique->invpermZ[i];
2308        }
2309        for (i = oldsize; i <= index; i++) {
2310            newsubtables[i].slots = numSlots;
2311            newsubtables[i].shift = sizeof(int) * 8 -
2312                cuddComputeFloorLog2(numSlots);
2313            newsubtables[i].keys = 0;
2314            newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2315            newsubtables[i].dead = 0;
2316            newperm[i] = i;
2317            newinvperm[i] = i;
2318            newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
2319            if (newnodelist == NULL) {
2320                unique->errorCode = CUDD_MEMORY_OUT;
2321                return(0);
2322            }
2323            for (j = 0; (unsigned) j < numSlots; j++) {
2324                newnodelist[j] = NULL;
2325            }
2326        }
2327        FREE(unique->subtableZ);
2328        unique->subtableZ = newsubtables;
2329        unique->maxSizeZ = newsize;
2330        FREE(unique->permZ);
2331        unique->permZ = newperm;
2332        FREE(unique->invpermZ);
2333        unique->invpermZ = newinvperm;
2334    }
2335    unique->slots += (index + 1 - unique->sizeZ) * numSlots;
2336    ddFixLimits(unique);
2337    unique->sizeZ = index + 1;
2338
2339    /* Now that the table is in a coherent state, update the ZDD
2340    ** universe. We need to temporarily disable reordering,
2341    ** because we cannot reorder without universe in place.
2342    */
2343
2344    reorderSave = unique->autoDynZ;
2345    unique->autoDynZ = 0;
2346    cuddZddFreeUniv(unique);
2347    if (!cuddZddInitUniv(unique)) {
2348        unique->autoDynZ = reorderSave;
2349        return(0);
2350    }
2351    unique->autoDynZ = reorderSave;
2352
2353    return(1);
2354
2355} /* end of cuddResizeTableZdd */
2356
2357
2358/**Function********************************************************************
2359
2360  Synopsis    [Adjusts parameters of a table to slow down its growth.]
2361
2362  Description []
2363
2364  SideEffects [None]
2365
2366  SeeAlso     []
2367
2368******************************************************************************/
2369void
2370cuddSlowTableGrowth(
2371  DdManager *unique)
2372{
2373    int i;
2374
2375    unique->maxCacheHard = unique->cacheSlots - 1;
2376    unique->cacheSlack = - (int) (unique->cacheSlots + 1);
2377    for (i = 0; i < unique->size; i++) {
2378        unique->subtables[i].maxKeys <<= 2;
2379    }
2380    unique->gcFrac = DD_GC_FRAC_MIN;
2381    unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots);
2382    cuddShrinkDeathRow(unique);
2383    (void) fprintf(unique->err,"Slowing down table growth: ");
2384    (void) fprintf(unique->err,"GC fraction = %.2f\t", unique->gcFrac);
2385    (void) fprintf(unique->err,"minDead = %u\n", unique->minDead);
2386
2387} /* end of cuddSlowTableGrowth */
2388
2389
2390/*---------------------------------------------------------------------------*/
2391/* Definition of static functions                                            */
2392/*---------------------------------------------------------------------------*/
2393
2394
2395/**Function********************************************************************
2396
2397  Synopsis    [Rehashes a ZDD unique subtable.]
2398
2399  Description []
2400
2401  SideEffects [None]
2402
2403  SeeAlso     [cuddRehash]
2404
2405******************************************************************************/
2406static void
2407ddRehashZdd(
2408  DdManager * unique,
2409  int  i)
2410{
2411    unsigned int slots, oldslots;
2412    int shift, oldshift;
2413    int j, pos;
2414    DdNodePtr *nodelist, *oldnodelist;
2415    DdNode *node, *next;
2416    extern DD_OOMFP MMoutOfMemory;
2417    DD_OOMFP saveHandler;
2418
2419    if (unique->slots > unique->looseUpTo) {
2420        unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots);
2421#ifdef DD_VERBOSE
2422        if (unique->gcFrac == DD_GC_FRAC_HI) {
2423            (void) fprintf(unique->err,"GC fraction = %.2f\t",
2424                           DD_GC_FRAC_LO);
2425            (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
2426        }
2427#endif
2428        unique->gcFrac = DD_GC_FRAC_LO;
2429    }
2430
2431    assert(i != CUDD_MAXINDEX);
2432    oldslots = unique->subtableZ[i].slots;
2433    oldshift = unique->subtableZ[i].shift;
2434    oldnodelist = unique->subtableZ[i].nodelist;
2435
2436    /* Compute the new size of the subtable. Normally, we just
2437    ** double.  However, after reordering, a table may be severely
2438    ** overloaded. Therefore, we iterate. */
2439    slots = oldslots;
2440    shift = oldshift;
2441    do {
2442        slots <<= 1;
2443        shift--;
2444    } while (slots * DD_MAX_SUBTABLE_DENSITY < unique->subtableZ[i].keys);
2445
2446    saveHandler = MMoutOfMemory;
2447    MMoutOfMemory = Cudd_OutOfMem;
2448    nodelist = ALLOC(DdNodePtr, slots);
2449    MMoutOfMemory = saveHandler;
2450    if (nodelist == NULL) {
2451        (void) fprintf(unique->err,
2452                       "Unable to resize ZDD subtable %d for lack of memory.\n",
2453                       i);
2454        (void) cuddGarbageCollect(unique,1);
2455        for (j = 0; j < unique->sizeZ; j++) {
2456            unique->subtableZ[j].maxKeys <<= 1;
2457        }
2458        return;
2459    }
2460    unique->subtableZ[i].nodelist = nodelist;
2461    unique->subtableZ[i].slots = slots;
2462    unique->subtableZ[i].shift = shift;
2463    unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
2464    for (j = 0; (unsigned) j < slots; j++) {
2465        nodelist[j] = NULL;
2466    }
2467    for (j = 0; (unsigned) j < oldslots; j++) {
2468        node = oldnodelist[j];
2469        while (node != NULL) {
2470            next = node->next;
2471            pos = ddHash(cuddT(node), cuddE(node), shift);
2472            node->next = nodelist[pos];
2473            nodelist[pos] = node;
2474            node = next;
2475        }
2476    }
2477    FREE(oldnodelist);
2478
2479#ifdef DD_VERBOSE
2480    (void) fprintf(unique->err,
2481                   "rehashing layer %d: keys %d dead %d new size %d\n",
2482                   i, unique->subtableZ[i].keys,
2483                   unique->subtableZ[i].dead, slots);
2484#endif
2485
2486    /* Update global data. */
2487    unique->memused += (slots - oldslots) * sizeof(DdNode *);
2488    unique->slots += (slots - oldslots);
2489    ddFixLimits(unique);
2490
2491} /* end of ddRehashZdd */
2492
2493
2494/**Function********************************************************************
2495
2496  Synopsis [Increases the number of subtables in a unique table so
2497  that it meets or exceeds index.]
2498
2499  Description [Increases the number of subtables in a unique table so
2500  that it meets or exceeds index. Returns 1 if successful; 0 otherwise.]
2501
2502  SideEffects [None]
2503
2504  SeeAlso     [cuddResizeTableZdd]
2505
2506******************************************************************************/
2507static int
2508ddResizeTable(
2509  DdManager * unique,
2510  int index)
2511{
2512    DdSubtable *newsubtables;
2513    DdNodePtr *newnodelist;
2514    DdNodePtr *newvars;
2515    DdNode *sentinel = &(unique->sentinel);
2516    int oldsize,newsize;
2517    int i,j,reorderSave;
2518    int numSlots = unique->initSlots;
2519    int *newperm, *newinvperm, *newmap;
2520    DdNode *one, *zero;
2521
2522    oldsize = unique->size;
2523    /* Easy case: there is still room in the current table. */
2524    if (index < unique->maxSize) {
2525        for (i = oldsize; i <= index; i++) {
2526            unique->subtables[i].slots = numSlots;
2527            unique->subtables[i].shift = sizeof(int) * 8 -
2528                cuddComputeFloorLog2(numSlots);
2529            unique->subtables[i].keys = 0;
2530            unique->subtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2531            unique->subtables[i].dead = 0;
2532            unique->subtables[i].bindVar = 0;
2533            unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
2534            unique->subtables[i].pairIndex = 0;
2535            unique->subtables[i].varHandled = 0;
2536            unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE;
2537
2538            unique->perm[i] = i;
2539            unique->invperm[i] = i;
2540            newnodelist = unique->subtables[i].nodelist =
2541                ALLOC(DdNodePtr, numSlots);
2542            if (newnodelist == NULL) {
2543                for (j = oldsize; j < i; j++) {
2544                    FREE(unique->subtables[j].nodelist);
2545                }
2546                unique->errorCode = CUDD_MEMORY_OUT;
2547                return(0);
2548            }
2549            for (j = 0; j < numSlots; j++) {
2550                newnodelist[j] = sentinel;
2551            }
2552        }
2553        if (unique->map != NULL) {
2554            for (i = oldsize; i <= index; i++) {
2555                unique->map[i] = i;
2556            }
2557        }
2558    } else {
2559        /* The current table is too small: we need to allocate a new,
2560        ** larger one; move all old subtables, and initialize the new
2561        ** subtables up to index included.
2562        */
2563        newsize = index + DD_DEFAULT_RESIZE;
2564#ifdef DD_VERBOSE
2565        (void) fprintf(unique->err,
2566                       "Increasing the table size from %d to %d\n",
2567                       unique->maxSize, newsize);
2568#endif
2569        newsubtables = ALLOC(DdSubtable,newsize);
2570        if (newsubtables == NULL) {
2571            unique->errorCode = CUDD_MEMORY_OUT;
2572            return(0);
2573        }
2574        newvars = ALLOC(DdNodePtr,newsize);
2575        if (newvars == NULL) {
2576            FREE(newsubtables);
2577            unique->errorCode = CUDD_MEMORY_OUT;
2578            return(0);
2579        }
2580        newperm = ALLOC(int,newsize);
2581        if (newperm == NULL) {
2582            FREE(newsubtables);
2583            FREE(newvars);
2584            unique->errorCode = CUDD_MEMORY_OUT;
2585            return(0);
2586        }
2587        newinvperm = ALLOC(int,newsize);
2588        if (newinvperm == NULL) {
2589            FREE(newsubtables);
2590            FREE(newvars);
2591            FREE(newperm);
2592            unique->errorCode = CUDD_MEMORY_OUT;
2593            return(0);
2594        }
2595        if (unique->map != NULL) {
2596            newmap = ALLOC(int,newsize);
2597            if (newmap == NULL) {
2598                FREE(newsubtables);
2599                FREE(newvars);
2600                FREE(newperm);
2601                FREE(newinvperm);
2602                unique->errorCode = CUDD_MEMORY_OUT;
2603                return(0);
2604            }
2605            unique->memused += (newsize - unique->maxSize) * sizeof(int);
2606        }
2607        unique->memused += (newsize - unique->maxSize) * ((numSlots+1) *
2608            sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
2609        if (newsize > unique->maxSizeZ) {
2610            FREE(unique->stack);
2611            unique->stack = ALLOC(DdNodePtr,newsize + 1);
2612            if (unique->stack == NULL) {
2613                FREE(newsubtables);
2614                FREE(newvars);
2615                FREE(newperm);
2616                FREE(newinvperm);
2617                if (unique->map != NULL) {
2618                    FREE(newmap);
2619                }
2620                unique->errorCode = CUDD_MEMORY_OUT;
2621                return(0);
2622            }
2623            unique->stack[0] = NULL; /* to suppress harmless UMR */
2624            unique->memused +=
2625                (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
2626                * sizeof(DdNode *);
2627        }
2628        for (i = 0; i < oldsize; i++) {
2629            newsubtables[i].slots = unique->subtables[i].slots;
2630            newsubtables[i].shift = unique->subtables[i].shift;
2631            newsubtables[i].keys = unique->subtables[i].keys;
2632            newsubtables[i].maxKeys = unique->subtables[i].maxKeys;
2633            newsubtables[i].dead = unique->subtables[i].dead;
2634            newsubtables[i].nodelist = unique->subtables[i].nodelist;
2635            newsubtables[i].bindVar = unique->subtables[i].bindVar;
2636            newsubtables[i].varType = unique->subtables[i].varType;
2637            newsubtables[i].pairIndex = unique->subtables[i].pairIndex;
2638            newsubtables[i].varHandled = unique->subtables[i].varHandled;
2639            newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped;
2640
2641            newvars[i] = unique->vars[i];
2642            newperm[i] = unique->perm[i];
2643            newinvperm[i] = unique->invperm[i];
2644        }
2645        for (i = oldsize; i <= index; i++) {
2646            newsubtables[i].slots = numSlots;
2647            newsubtables[i].shift = sizeof(int) * 8 -
2648                cuddComputeFloorLog2(numSlots);
2649            newsubtables[i].keys = 0;
2650            newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2651            newsubtables[i].dead = 0;
2652            newsubtables[i].bindVar = 0;
2653            newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
2654            newsubtables[i].pairIndex = 0;
2655            newsubtables[i].varHandled = 0;
2656            newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE;
2657
2658            newperm[i] = i;
2659            newinvperm[i] = i;
2660            newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
2661            if (newnodelist == NULL) {
2662                unique->errorCode = CUDD_MEMORY_OUT;
2663                return(0);
2664            }
2665            for (j = 0; j < numSlots; j++) {
2666                newnodelist[j] = sentinel;
2667            }
2668        }
2669        if (unique->map != NULL) {
2670            for (i = 0; i < oldsize; i++) {
2671                newmap[i] = unique->map[i];
2672            }
2673            for (i = oldsize; i <= index; i++) {
2674                newmap[i] = i;
2675            }
2676            FREE(unique->map);
2677            unique->map = newmap;
2678        }
2679        FREE(unique->subtables);
2680        unique->subtables = newsubtables;
2681        unique->maxSize = newsize;
2682        FREE(unique->vars);
2683        unique->vars = newvars;
2684        FREE(unique->perm);
2685        unique->perm = newperm;
2686        FREE(unique->invperm);
2687        unique->invperm = newinvperm;
2688    }
2689
2690    /* Now that the table is in a coherent state, create the new
2691    ** projection functions. We need to temporarily disable reordering,
2692    ** because we cannot reorder without projection functions in place.
2693    **/
2694    one = unique->one;
2695    zero = Cudd_Not(one);
2696
2697    unique->size = index + 1;
2698    unique->slots += (index + 1 - oldsize) * numSlots;
2699    ddFixLimits(unique);
2700
2701    reorderSave = unique->autoDyn;
2702    unique->autoDyn = 0;
2703    for (i = oldsize; i <= index; i++) {
2704        unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
2705        if (unique->vars[i] == NULL) {
2706            unique->autoDyn = reorderSave;
2707            for (j = oldsize; j < i; j++) {
2708                Cudd_IterDerefBdd(unique,unique->vars[j]);
2709                cuddDeallocNode(unique,unique->vars[j]);
2710                unique->vars[j] = NULL;
2711            }
2712            for (j = oldsize; j <= index; j++) {
2713                FREE(unique->subtables[j].nodelist);
2714                unique->subtables[j].nodelist = NULL;
2715            }
2716            unique->size = oldsize;
2717            unique->slots -= (index + 1 - oldsize) * numSlots;
2718            ddFixLimits(unique);
2719            return(0);
2720        }
2721        cuddRef(unique->vars[i]);
2722    }
2723    unique->autoDyn = reorderSave;
2724
2725    return(1);
2726
2727} /* end of ddResizeTable */
2728
2729
2730/**Function********************************************************************
2731
2732  Synopsis    [Searches the subtables above node for a parent.]
2733
2734  Description [Searches the subtables above node for a parent. Returns 1
2735  as soon as one parent is found. Returns 0 is the search is fruitless.]
2736
2737  SideEffects [None]
2738
2739  SeeAlso     []
2740
2741******************************************************************************/
2742static int
2743cuddFindParent(
2744  DdManager * table,
2745  DdNode * node)
2746{
2747    int         i,j;
2748    int         slots;
2749    DdNodePtr   *nodelist;
2750    DdNode      *f;
2751
2752    for (i = cuddI(table,node->index) - 1; i >= 0; i--) {
2753        nodelist = table->subtables[i].nodelist;
2754        slots = table->subtables[i].slots;
2755
2756        for (j = 0; j < slots; j++) {
2757            f = nodelist[j];
2758            while (cuddT(f) > node) {
2759                f = f->next;
2760            }
2761            while (cuddT(f) == node && Cudd_Regular(cuddE(f)) > node) {
2762                f = f->next;
2763            }
2764            if (cuddT(f) == node && Cudd_Regular(cuddE(f)) == node) {
2765                return(1);
2766            }
2767        }
2768    }
2769
2770    return(0);
2771
2772} /* end of cuddFindParent */
2773
2774
2775/**Function********************************************************************
2776
2777  Synopsis    [Adjusts the values of table limits.]
2778
2779  Description [Adjusts the values of table fields controlling the.
2780  sizes of subtables and computed table. If the computed table is too small
2781  according to the new values, it is resized.]
2782
2783  SideEffects [Modifies manager fields. May resize computed table.]
2784
2785  SeeAlso     []
2786
2787******************************************************************************/
2788DD_INLINE
2789static void
2790ddFixLimits(
2791  DdManager *unique)
2792{
2793    unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
2794    unique->cacheSlack = (int) ddMin(unique->maxCacheHard,
2795        DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots) -
2796        2 * (int) unique->cacheSlots;
2797    if (unique->cacheSlots < unique->slots/2 && unique->cacheSlack >= 0)
2798        cuddCacheResize(unique);
2799    return;
2800
2801} /* end of ddFixLimits */
2802
2803
2804#ifndef DD_UNSORTED_FREE_LIST
2805#ifdef DD_RED_BLACK_FREE_LIST
2806/**Function********************************************************************
2807
2808  Synopsis    [Inserts a DdNode in a red/black search tree.]
2809
2810  Description [Inserts a DdNode in a red/black search tree. Nodes from
2811  the same "page" (defined by DD_PAGE_MASK) are linked in a LIFO list.]
2812
2813  SideEffects [None]
2814
2815  SeeAlso     [cuddOrderedThread]
2816
2817******************************************************************************/
2818static void
2819cuddOrderedInsert(
2820  DdNodePtr * root,
2821  DdNodePtr node)
2822{
2823    DdNode *scan;
2824    DdNodePtr *scanP;
2825    DdNodePtr *stack[DD_STACK_SIZE];
2826    int stackN = 0;
2827
2828    scanP = root;
2829    while ((scan = *scanP) != NULL) {
2830        stack[stackN++] = scanP;
2831        if (DD_INSERT_COMPARE(node, scan) == 0) { /* add to page list */
2832            DD_NEXT(node) = DD_NEXT(scan);
2833            DD_NEXT(scan) = node;
2834            return;
2835        }
2836        scanP = (node < scan) ? &DD_LEFT(scan) : &DD_RIGHT(scan);
2837    }
2838    DD_RIGHT(node) = DD_LEFT(node) = DD_NEXT(node) = NULL;
2839    DD_COLOR(node) = DD_RED;
2840    *scanP = node;
2841    stack[stackN] = &node;
2842    cuddDoRebalance(stack,stackN);
2843
2844} /* end of cuddOrderedInsert */
2845
2846
2847/**Function********************************************************************
2848
2849  Synopsis    [Threads all the nodes of a search tree into a linear list.]
2850
2851  Description [Threads all the nodes of a search tree into a linear
2852  list. For each node of the search tree, the "left" child, if non-null, has
2853  a lower address than its parent, and the "right" child, if non-null, has a
2854  higher address than its parent.
2855  The list is sorted in order of increasing addresses. The search
2856  tree is destroyed as a result of this operation. The last element of
2857  the linear list is made to point to the address passed in list. Each
2858  node if the search tree is a linearly-linked list of nodes from the
2859  same memory page (as defined in DD_PAGE_MASK). When a node is added to
2860  the linear list, all the elements of the linked list are added.]
2861
2862  SideEffects [The search tree is destroyed as a result of this operation.]
2863
2864  SeeAlso     [cuddOrderedInsert]
2865
2866******************************************************************************/
2867static DdNode *
2868cuddOrderedThread(
2869  DdNode * root,
2870  DdNode * list)
2871{
2872    DdNode *current, *next, *prev, *end;
2873
2874    current = root;
2875    /* The first word in the node is used to implement a stack that holds
2876    ** the nodes from the root of the tree to the current node. Here we
2877    ** put the root of the tree at the bottom of the stack.
2878    */
2879    *((DdNodePtr *) current) = NULL;
2880
2881    while (current != NULL) {
2882        if (DD_RIGHT(current) != NULL) {
2883            /* If possible, we follow the "right" link. Eventually we'll
2884            ** find the node with the largest address in the current tree.
2885            ** In this phase we use the first word of a node to implemen
2886            ** a stack of the nodes on the path from the root to "current".
2887            ** Also, we disconnect the "right" pointers to indicate that
2888            ** we have already followed them.
2889            */
2890            next = DD_RIGHT(current);
2891            DD_RIGHT(current) = NULL;
2892            *((DdNodePtr *)next) = current;
2893            current = next;
2894        } else {
2895            /* We can't proceed along the "right" links any further.
2896            ** Hence "current" is the largest element in the current tree.
2897            ** We make this node the new head of "list". (Repeating this
2898            ** operation until the tree is empty yields the desired linear
2899            ** threading of all nodes.)
2900            */
2901            prev = *((DdNodePtr *) current); /* save prev node on stack in prev */
2902            /* Traverse the linked list of current until the end. */
2903            for (end = current; DD_NEXT(end) != NULL; end = DD_NEXT(end));
2904            DD_NEXT(end) = list; /* attach "list" at end and make */
2905            list = current;   /* "current" the new head of "list" */
2906            /* Now, if current has a "left" child, we push it on the stack.
2907            ** Otherwise, we just continue with the parent of "current".
2908            */
2909            if (DD_LEFT(current) != NULL) {
2910                next = DD_LEFT(current);
2911                *((DdNodePtr *) next) = prev;
2912                current = next;
2913            } else {
2914                current = prev;
2915            }
2916        }
2917    }
2918
2919    return(list);
2920
2921} /* end of cuddOrderedThread */
2922
2923
2924/**Function********************************************************************
2925
2926  Synopsis    [Performs the left rotation for red/black trees.]
2927
2928  Description []
2929
2930  SideEffects [None]
2931
2932  SeeAlso     [cuddRotateRight]
2933
2934******************************************************************************/
2935DD_INLINE
2936static void
2937cuddRotateLeft(
2938  DdNodePtr * nodeP)
2939{
2940    DdNode *newRoot;
2941    DdNode *oldRoot = *nodeP;
2942
2943    *nodeP = newRoot = DD_RIGHT(oldRoot);
2944    DD_RIGHT(oldRoot) = DD_LEFT(newRoot);
2945    DD_LEFT(newRoot) = oldRoot;
2946
2947} /* end of cuddRotateLeft */
2948
2949
2950/**Function********************************************************************
2951
2952  Synopsis    [Performs the right rotation for red/black trees.]
2953
2954  Description []
2955
2956  SideEffects [None]
2957
2958  SeeAlso     [cuddRotateLeft]
2959
2960******************************************************************************/
2961DD_INLINE
2962static void
2963cuddRotateRight(
2964  DdNodePtr * nodeP)
2965{
2966    DdNode *newRoot;
2967    DdNode *oldRoot = *nodeP;
2968
2969    *nodeP = newRoot = DD_LEFT(oldRoot);
2970    DD_LEFT(oldRoot) = DD_RIGHT(newRoot);
2971    DD_RIGHT(newRoot) = oldRoot;
2972
2973} /* end of cuddRotateRight */
2974
2975
2976/**Function********************************************************************
2977
2978  Synopsis    [Rebalances a red/black tree.]
2979
2980  Description []
2981
2982  SideEffects [None]
2983
2984  SeeAlso     []
2985
2986******************************************************************************/
2987static void
2988cuddDoRebalance(
2989  DdNodePtr ** stack,
2990  int  stackN)
2991{
2992    DdNodePtr *xP, *parentP, *grandpaP;
2993    DdNode *x, *y, *parent, *grandpa;
2994
2995    xP = stack[stackN];
2996    x = *xP;
2997    /* Work our way back up, re-balancing the tree. */
2998    while (--stackN >= 0) {
2999        parentP = stack[stackN];
3000        parent = *parentP;
3001        if (DD_IS_BLACK(parent)) break;
3002        /* Since the root is black, here a non-null grandparent exists. */
3003        grandpaP = stack[stackN-1];
3004        grandpa = *grandpaP;
3005        if (parent == DD_LEFT(grandpa)) {
3006            y = DD_RIGHT(grandpa);
3007            if (y != NULL && DD_IS_RED(y)) {
3008                DD_COLOR(parent) = DD_BLACK;
3009                DD_COLOR(y) = DD_BLACK;
3010                DD_COLOR(grandpa) = DD_RED;
3011                x = grandpa;
3012                stackN--;
3013            } else {
3014                if (x == DD_RIGHT(parent)) {
3015                    cuddRotateLeft(parentP);
3016                    DD_COLOR(x) = DD_BLACK;
3017                } else {
3018                    DD_COLOR(parent) = DD_BLACK;
3019                }
3020                DD_COLOR(grandpa) = DD_RED;
3021                cuddRotateRight(grandpaP);
3022                break;
3023            }
3024        } else {
3025            y = DD_LEFT(grandpa);
3026            if (y != NULL && DD_IS_RED(y)) {
3027                DD_COLOR(parent) = DD_BLACK;
3028                DD_COLOR(y) = DD_BLACK;
3029                DD_COLOR(grandpa) = DD_RED;
3030                x = grandpa;
3031                stackN--;
3032            } else {
3033                if (x == DD_LEFT(parent)) {
3034                    cuddRotateRight(parentP);
3035                    DD_COLOR(x) = DD_BLACK;
3036                } else {
3037                    DD_COLOR(parent) = DD_BLACK;
3038                }
3039                DD_COLOR(grandpa) = DD_RED;
3040                cuddRotateLeft(grandpaP);
3041            }
3042        }
3043    }
3044    DD_COLOR(*(stack[0])) = DD_BLACK;
3045
3046} /* end of cuddDoRebalance */
3047#endif
3048#endif
3049
3050
3051/**Function********************************************************************
3052
3053  Synopsis    [Fixes a variable tree after the insertion of new subtables.]
3054
3055  Description [Fixes a variable tree after the insertion of new subtables.
3056  After such an insertion, the low fields of the tree below the insertion
3057  point are inconsistent.]
3058
3059  SideEffects [None]
3060
3061  SeeAlso     []
3062
3063******************************************************************************/
3064static void
3065ddPatchTree(
3066  DdManager *dd,
3067  MtrNode *treenode)
3068{
3069    MtrNode *auxnode = treenode;
3070
3071    while (auxnode != NULL) {
3072        auxnode->low = dd->perm[auxnode->index];
3073        if (auxnode->child != NULL) {
3074            ddPatchTree(dd, auxnode->child);
3075        }
3076        auxnode = auxnode->younger;
3077    }
3078
3079    return;
3080
3081} /* end of ddPatchTree */
3082
3083
3084#ifdef DD_DEBUG
3085/**Function********************************************************************
3086
3087  Synopsis    [Checks whether a collision list is ordered.]
3088
3089  Description []
3090
3091  SideEffects [None]
3092
3093  SeeAlso     []
3094
3095******************************************************************************/
3096static int
3097cuddCheckCollisionOrdering(
3098  DdManager *unique,
3099  int i,
3100  int j)
3101{
3102    int slots;
3103    DdNode *node, *next;
3104    DdNodePtr *nodelist;
3105    DdNode *sentinel = &(unique->sentinel);
3106
3107    nodelist = unique->subtables[i].nodelist;
3108    slots = unique->subtables[i].slots;
3109    node = nodelist[j];
3110    if (node == sentinel) return(1);
3111    next = node->next;
3112    while (next != sentinel) {
3113        if (cuddT(node) < cuddT(next) ||
3114            (cuddT(node) == cuddT(next) && cuddE(node) < cuddE(next))) {
3115            (void) fprintf(unique->err,
3116                           "Unordered list: index %u, position %d\n", i, j);
3117            return(0);
3118        }
3119        node = next;
3120        next = node->next;
3121    }
3122    return(1);
3123
3124} /* end of cuddCheckCollisionOrdering */
3125#endif
3126
3127
3128
3129
3130/**Function********************************************************************
3131
3132  Synopsis    [Reports problem in garbage collection.]
3133
3134  Description []
3135
3136  SideEffects [None]
3137
3138  SeeAlso     [cuddGarbageCollect cuddGarbageCollectZdd]
3139
3140******************************************************************************/
3141static void
3142ddReportRefMess(
3143  DdManager *unique /* manager */,
3144  int i /* table in which the problem occurred */,
3145  const char *caller /* procedure that detected the problem */)
3146{
3147    if (i == CUDD_CONST_INDEX) {
3148        (void) fprintf(unique->err,
3149                           "%s: problem in constants\n", caller);
3150    } else if (i != -1) {
3151        (void) fprintf(unique->err,
3152                           "%s: problem in table %d\n", caller, i);
3153    }
3154    (void) fprintf(unique->err, "  dead count != deleted\n");
3155    (void) fprintf(unique->err, "  This problem is often due to a missing \
3156call to Cudd_Ref\n  or to an extra call to Cudd_RecursiveDeref.\n  \
3157See the CUDD Programmer's Guide for additional details.");
3158    abort();
3159
3160} /* end of ddReportRefMess */
Note: See TracBrowser for help on using the repository browser.