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