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