source: vis_dev/glu-2.1/src/cuBdd/cuddTable.c @ 9

Last change on this file since 9 was 8, checked in by cecile, 14 years ago

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