1 /**
2 @file
3
4 @ingroup cudd
5
6 @brief Functions for dynamic variable reordering.
7
8 @author Shipra Panda, Bernard Plessier, Fabio Somenzi
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "util.h"
47 #include "mtrInt.h"
48 #include "cuddInt.h"
49
50 /*---------------------------------------------------------------------------*/
51 /* Constant declarations */
52 /*---------------------------------------------------------------------------*/
53
54 /*---------------------------------------------------------------------------*/
55 /* Stucture declarations */
56 /*---------------------------------------------------------------------------*/
57
58 /*---------------------------------------------------------------------------*/
59 /* Type declarations */
60 /*---------------------------------------------------------------------------*/
61
62 /*---------------------------------------------------------------------------*/
63 /* Variable declarations */
64 /*---------------------------------------------------------------------------*/
65
66 /*---------------------------------------------------------------------------*/
67 /* Macro declarations */
68 /*---------------------------------------------------------------------------*/
69
70 /** \cond */
71
72 /*---------------------------------------------------------------------------*/
73 /* Static function prototypes */
74 /*---------------------------------------------------------------------------*/
75
76 static int ddUniqueCompare (void const *ptrX, void const *ptrY);
77 static Move * ddSwapAny (DdManager *table, int x, int y);
78 static int ddSiftingAux (DdManager *table, int x, int xLow, int xHigh);
79 static Move * ddSiftingUp (DdManager *table, int y, int xLow);
80 static Move * ddSiftingDown (DdManager *table, int x, int xHigh);
81 static int ddSiftingBackward (DdManager *table, int size, Move *moves);
82 static int ddReorderPreprocess (DdManager *table);
83 static int ddReorderPostprocess (DdManager *table);
84 static int ddShuffle (DdManager *table, int *permutation);
85 static int ddSiftUp (DdManager *table, int x, int xLow);
86 static void bddFixTree (DdManager *table, MtrNode *treenode);
87 static int ddUpdateMtrTree (DdManager *table, MtrNode *treenode, int *perm, int *invperm);
88 static int ddCheckPermuation (DdManager *table, MtrNode *treenode, int *perm, int *invperm);
89
90 /** \endcond */
91
92
93 /*---------------------------------------------------------------------------*/
94 /* Definition of exported functions */
95 /*---------------------------------------------------------------------------*/
96
97
98 /**
99 @brief Main dynamic reordering routine.
100
101 @details Calls one of the possible reordering procedures:
102 <ul>
103 <li>Swapping
104 <li>Sifting
105 <li>Symmetric Sifting
106 <li>Group Sifting
107 <li>Window Permutation
108 <li>Simulated Annealing
109 <li>Genetic Algorithm
110 <li>Dynamic Programming (exact)
111 </ul>
112 For sifting, symmetric sifting, group sifting, and window
113 permutation it is possible to request reordering to convergence.<p>
114 The core of all methods is the reordering procedure
115 cuddSwapInPlace() which swaps two adjacent variables and is based
116 on Rudell's paper.
117
118 @return 1 in case of success; 0 otherwise. In the case of symmetric
119 sifting (with and without convergence) returns 1 plus the number of
120 symmetric variables, in case of success.
121
122 @sideeffect Changes the variable order for all diagrams and clears
123 the cache.
124
125 */
126 int
Cudd_ReduceHeap(DdManager * table,Cudd_ReorderingType heuristic,int minsize)127 Cudd_ReduceHeap(
128 DdManager * table /**< %DD manager */,
129 Cudd_ReorderingType heuristic /**< method used for reordering */,
130 int minsize /**< bound below which no reordering occurs */)
131 {
132 DdHook *hook;
133 int result;
134 unsigned int nextDyn;
135 #ifdef DD_STATS
136 unsigned int initialSize;
137 unsigned int finalSize;
138 #endif
139 unsigned long localTime;
140
141 /* Don't reorder if there are too many dead nodes. */
142 if (table->keys - table->dead < (unsigned) minsize)
143 return(1);
144
145 if (heuristic == CUDD_REORDER_SAME) {
146 heuristic = table->autoMethod;
147 }
148 if (heuristic == CUDD_REORDER_NONE) {
149 return(1);
150 }
151
152 /* This call to Cudd_ReduceHeap does initiate reordering. Therefore
153 ** we count it.
154 */
155 table->reorderings++;
156
157 localTime = util_cpu_time();
158
159 /* Run the hook functions. */
160 hook = table->preReorderingHook;
161 while (hook != NULL) {
162 int res = (hook->f)(table, "BDD", (void *)heuristic);
163 if (res == 0) return(0);
164 hook = hook->next;
165 }
166
167 if (!ddReorderPreprocess(table)) return(0);
168 table->ddTotalNumberSwapping = 0;
169
170 if (table->keys > table->peakLiveNodes) {
171 table->peakLiveNodes = table->keys;
172 }
173 #ifdef DD_STATS
174 initialSize = (int) (table->keys - table->isolated);
175 table->totalNISwaps = 0;
176
177 switch(heuristic) {
178 case CUDD_REORDER_RANDOM:
179 case CUDD_REORDER_RANDOM_PIVOT:
180 (void) fprintf(table->out,"#:I_RANDOM ");
181 break;
182 case CUDD_REORDER_SIFT:
183 case CUDD_REORDER_SIFT_CONVERGE:
184 case CUDD_REORDER_SYMM_SIFT:
185 case CUDD_REORDER_SYMM_SIFT_CONV:
186 case CUDD_REORDER_GROUP_SIFT:
187 case CUDD_REORDER_GROUP_SIFT_CONV:
188 (void) fprintf(table->out,"#:I_SIFTING ");
189 break;
190 case CUDD_REORDER_WINDOW2:
191 case CUDD_REORDER_WINDOW3:
192 case CUDD_REORDER_WINDOW4:
193 case CUDD_REORDER_WINDOW2_CONV:
194 case CUDD_REORDER_WINDOW3_CONV:
195 case CUDD_REORDER_WINDOW4_CONV:
196 (void) fprintf(table->out,"#:I_WINDOW ");
197 break;
198 case CUDD_REORDER_ANNEALING:
199 (void) fprintf(table->out,"#:I_ANNEAL ");
200 break;
201 case CUDD_REORDER_GENETIC:
202 (void) fprintf(table->out,"#:I_GENETIC ");
203 break;
204 case CUDD_REORDER_LINEAR:
205 case CUDD_REORDER_LINEAR_CONVERGE:
206 (void) fprintf(table->out,"#:I_LINSIFT ");
207 break;
208 case CUDD_REORDER_EXACT:
209 (void) fprintf(table->out,"#:I_EXACT ");
210 break;
211 default:
212 return(0);
213 }
214 (void) fprintf(table->out,"%8d: initial size",initialSize);
215 #endif
216
217 /* See if we should use alternate threshold for maximum growth. */
218 if (table->reordCycle && table->reorderings % table->reordCycle == 0) {
219 double saveGrowth = table->maxGrowth;
220 table->maxGrowth = table->maxGrowthAlt;
221 result = cuddTreeSifting(table,heuristic);
222 table->maxGrowth = saveGrowth;
223 } else {
224 result = cuddTreeSifting(table,heuristic);
225 }
226
227 #ifdef DD_STATS
228 (void) fprintf(table->out,"\n");
229 finalSize = (int) (table->keys - table->isolated);
230 (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize);
231 (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n",
232 ((double)(util_cpu_time() - localTime)/1000.0));
233 (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n",
234 table->ddTotalNumberSwapping);
235 (void) fprintf(table->out,"#:M_REORDER %8d: NI swaps\n",
236 table->totalNISwaps);
237 #endif
238
239 if (result == 0)
240 return(0);
241
242 if (!ddReorderPostprocess(table))
243 return(0);
244
245 if (table->realign) {
246 if (!cuddZddAlignToBdd(table))
247 return(0);
248 }
249
250 nextDyn = (table->keys - table->constants.keys + 1) *
251 DD_DYN_RATIO + table->constants.keys;
252 if (table->reorderings < 20 || nextDyn > table->nextDyn)
253 table->nextDyn = nextDyn;
254 else
255 table->nextDyn += 20;
256 if (table->randomizeOrder != 0) {
257 table->nextDyn += Cudd_Random(table) & table->randomizeOrder;
258 }
259 table->reordered = 1;
260
261 /* Run hook functions. */
262 hook = table->postReorderingHook;
263 while (hook != NULL) {
264 int res = (hook->f)(table, "BDD", (void *)(ptruint)localTime);
265 if (res == 0) return(0);
266 hook = hook->next;
267 }
268 /* Update cumulative reordering time. */
269 table->reordTime += util_cpu_time() - localTime;
270
271 return(result);
272
273 } /* end of Cudd_ReduceHeap */
274
275
276 /**
277 @brief Reorders variables according to given permutation.
278
279 @details The i-th entry of the permutation array contains the index
280 of the variable that should be brought to the i-th level. The size
281 of the array should be equal or greater to the number of variables
282 currently in use.
283
284 @return 1 in case of success; 0 otherwise.
285
286 @sideeffect Changes the variable order for all diagrams and clears
287 the cache.
288
289 @see Cudd_ReduceHeap
290
291 */
292 int
Cudd_ShuffleHeap(DdManager * table,int * permutation)293 Cudd_ShuffleHeap(
294 DdManager * table /**< %DD manager */,
295 int * permutation /**< required variable permutation */)
296 {
297
298 int result;
299 int i;
300 int identity = 1;
301 int *perm;
302
303 /* Don't waste time in case of identity permutation. */
304 for (i = 0; i < table->size; i++) {
305 if (permutation[i] != table->invperm[i]) {
306 identity = 0;
307 break;
308 }
309 }
310 if (identity == 1) {
311 return(1);
312 }
313 if (!ddReorderPreprocess(table)) return(0);
314 if (table->keys > table->peakLiveNodes) {
315 table->peakLiveNodes = table->keys;
316 }
317
318 perm = ALLOC(int, table->size);
319 for (i = 0; i < table->size; i++)
320 perm[permutation[i]] = i;
321 if (!ddCheckPermuation(table,table->tree,perm,permutation)) {
322 FREE(perm);
323 return(0);
324 }
325 if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) {
326 FREE(perm);
327 return(0);
328 }
329 FREE(perm);
330
331 result = ddShuffle(table,permutation);
332
333 if (!ddReorderPostprocess(table)) return(0);
334
335 return(result);
336
337 } /* end of Cudd_ShuffleHeap */
338
339
340 /*---------------------------------------------------------------------------*/
341 /* Definition of internal functions */
342 /*---------------------------------------------------------------------------*/
343
344
345 /**
346 @brief Dynamically allocates a Node.
347
348 @details This procedure is similar to cuddAllocNode in Cudd_Table.c,
349 but it does not attempt garbage collection, because during
350 reordering there are no dead nodes.
351
352 @return a pointer to a new node if successful; NULL is memory is
353 full.
354
355 @sideeffect None
356
357 @see cuddAllocNode
358
359 */
360 DdNode *
cuddDynamicAllocNode(DdManager * table)361 cuddDynamicAllocNode(
362 DdManager * table)
363 {
364 int i;
365 DdNodePtr *mem;
366 DdNode *list, *node;
367 extern DD_OOMFP MMoutOfMemory;
368 DD_OOMFP saveHandler;
369
370 if (table->nextFree == NULL) { /* free list is empty */
371 /* Try to allocate a new block. */
372 saveHandler = MMoutOfMemory;
373 MMoutOfMemory = table->outOfMemCallback;
374 mem = (DdNodePtr *) ALLOC(DdNode, DD_MEM_CHUNK + 1);
375 MMoutOfMemory = saveHandler;
376 if (mem == NULL && table->stash != NULL) {
377 FREE(table->stash);
378 table->stash = NULL;
379 /* Inhibit resizing of tables. */
380 table->maxCacheHard = table->cacheSlots - 1;
381 table->cacheSlack = - (int) (table->cacheSlots + 1);
382 for (i = 0; i < table->size; i++) {
383 table->subtables[i].maxKeys <<= 2;
384 }
385 mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
386 }
387 if (mem == NULL) {
388 /* Out of luck. Call the default handler to do
389 ** whatever it specifies for a failed malloc. If this
390 ** handler returns, then set error code, print
391 ** warning, and return. */
392 (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1));
393 table->errorCode = CUDD_MEMORY_OUT;
394 #ifdef DD_VERBOSE
395 (void) fprintf(table->err,
396 "cuddDynamicAllocNode: out of memory");
397 (void) fprintf(table->err,"Memory in use = %lu\n",
398 table->memused);
399 #endif
400 return(NULL);
401 } else { /* successful allocation; slice memory */
402 size_t offset;
403 table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode);
404 mem[0] = (DdNode *) table->memoryList;
405 table->memoryList = mem;
406
407 /* Here we rely on the fact that the size of a DdNode is a
408 ** power of 2 and a multiple of the size of a pointer.
409 ** If we align one node, all the others will be aligned
410 ** as well. */
411 offset = (size_t) mem & (sizeof(DdNode) - 1);
412 mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
413 #ifdef DD_DEBUG
414 assert(((size_t) mem & (sizeof(DdNode) - 1)) == 0);
415 #endif
416 list = (DdNode *) mem;
417
418 i = 1;
419 do {
420 list[i - 1].ref = 0;
421 list[i - 1].next = &list[i];
422 } while (++i < DD_MEM_CHUNK);
423
424 list[DD_MEM_CHUNK-1].ref = 0;
425 list[DD_MEM_CHUNK - 1].next = NULL;
426
427 table->nextFree = &list[0];
428 }
429 } /* if free list empty */
430
431 node = table->nextFree;
432 table->nextFree = node->next;
433 return (node);
434
435 } /* end of cuddDynamicAllocNode */
436
437
438 /**
439 @brief Implementation of Rudell's sifting algorithm.
440
441 @details Assumes that no dead nodes are present.
442 <ol>
443 <li> Order all the variables according to the number of entries
444 in each unique table.
445 <li> Sift the variable up and down, remembering each time the
446 total size of the %DD heap.
447 <li> Select the best permutation.
448 <li> Repeat 3 and 4 for all variables.
449 </ol>
450
451 @return 1 if successful; 0 otherwise.
452
453 @sideeffect None
454
455 */
456 int
cuddSifting(DdManager * table,int lower,int upper)457 cuddSifting(
458 DdManager * table,
459 int lower,
460 int upper)
461 {
462 int i;
463 IndexKey *var;
464 int size;
465 int x;
466 int result;
467 #ifdef DD_STATS
468 int previousSize;
469 #endif
470
471 size = table->size;
472
473 /* Find order in which to sift variables. */
474 var = ALLOC(IndexKey,size);
475 if (var == NULL) {
476 table->errorCode = CUDD_MEMORY_OUT;
477 goto cuddSiftingOutOfMem;
478 }
479
480 for (i = 0; i < size; i++) {
481 x = table->perm[i];
482 var[i].index = i;
483 var[i].keys = table->subtables[x].keys;
484 }
485
486 util_qsort(var,size,sizeof(IndexKey),ddUniqueCompare);
487
488 /* Now sift. */
489 for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
490 if (table->ddTotalNumberSwapping >= table->siftMaxSwap)
491 break;
492 if (util_cpu_time() - table->startTime + table->reordTime
493 > table->timeLimit) {
494 table->autoDyn = 0; /* prevent further reordering */
495 break;
496 }
497 if (table->terminationCallback != NULL &&
498 table->terminationCallback(table->tcbArg)) {
499 table->autoDyn = 0; /* prevent further reordering */
500 break;
501 }
502 x = table->perm[var[i].index];
503
504 if (x < lower || x > upper || table->subtables[x].bindVar == 1)
505 continue;
506 #ifdef DD_STATS
507 previousSize = (int) (table->keys - table->isolated);
508 #endif
509 result = ddSiftingAux(table, x, lower, upper);
510 if (!result) goto cuddSiftingOutOfMem;
511 #ifdef DD_STATS
512 if (table->keys < (unsigned) previousSize + table->isolated) {
513 (void) fprintf(table->out,"-");
514 } else if (table->keys > (unsigned) previousSize + table->isolated) {
515 (void) fprintf(table->out,"+"); /* should never happen */
516 (void) fprintf(table->err,"\nSize increased from %d to %u while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i].index);
517 } else {
518 (void) fprintf(table->out,"=");
519 }
520 fflush(table->out);
521 #endif
522 }
523
524 FREE(var);
525
526 return(1);
527
528 cuddSiftingOutOfMem:
529
530 if (var != NULL) FREE(var);
531
532 return(0);
533
534 } /* end of cuddSifting */
535
536
537 /**
538 @brief Reorders variables by a sequence of (non-adjacent) swaps.
539
540 @details Implementation of Plessier's algorithm that reorders
541 variables by a sequence of (non-adjacent) swaps.
542 <ol>
543 <li> Select two variables (RANDOM or HEURISTIC).
544 <li> Permute these variables.
545 <li> If the nodes have decreased accept the permutation.
546 <li> Otherwise reconstruct the original heap.
547 <li> Loop.
548 </ol>
549
550 @return 1 in case of success; 0 otherwise.
551
552 @sideeffect None
553
554 */
555 int
cuddSwapping(DdManager * table,int lower,int upper,Cudd_ReorderingType heuristic)556 cuddSwapping(
557 DdManager * table,
558 int lower,
559 int upper,
560 Cudd_ReorderingType heuristic)
561 {
562 int i, j;
563 int max, keys;
564 int nvars;
565 int x, y;
566 int iterate;
567 int previousSize;
568 Move *moves, *move;
569 int pivot = 0;
570 int modulo;
571 int result;
572
573 #ifdef DD_DEBUG
574 /* Sanity check */
575 assert(lower >= 0 && upper < table->size && lower <= upper);
576 #endif
577
578 nvars = upper - lower + 1;
579 iterate = nvars;
580
581 for (i = 0; i < iterate; i++) {
582 if (table->ddTotalNumberSwapping >= table->siftMaxSwap)
583 break;
584 if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
585 max = -1;
586 for (j = lower; j <= upper; j++) {
587 if ((keys = table->subtables[j].keys) > max) {
588 max = keys;
589 pivot = j;
590 }
591 }
592
593 modulo = upper - pivot;
594 if (modulo == 0) {
595 y = pivot;
596 } else{
597 y = pivot + 1 + ((int) Cudd_Random(table) % modulo);
598 }
599
600 modulo = pivot - lower - 1;
601 if (modulo < 1) {
602 x = lower;
603 } else{
604 do {
605 x = (int) Cudd_Random(table) % modulo;
606 } while (x == y);
607 }
608 } else {
609 x = ((int) Cudd_Random(table) % nvars) + lower;
610 do {
611 y = ((int) Cudd_Random(table) % nvars) + lower;
612 } while (x == y);
613 }
614 previousSize = (int) (table->keys - table->isolated);
615 moves = ddSwapAny(table,x,y);
616 if (moves == NULL) goto cuddSwappingOutOfMem;
617 result = ddSiftingBackward(table,previousSize,moves);
618 if (!result) goto cuddSwappingOutOfMem;
619 while (moves != NULL) {
620 move = moves->next;
621 cuddDeallocMove(table, moves);
622 moves = move;
623 }
624 #ifdef DD_STATS
625 if (table->keys < (unsigned) previousSize + table->isolated) {
626 (void) fprintf(table->out,"-");
627 } else if (table->keys > (unsigned) previousSize + table->isolated) {
628 (void) fprintf(table->out,"+"); /* should never happen */
629 } else {
630 (void) fprintf(table->out,"=");
631 }
632 fflush(table->out);
633 #endif
634 #if 0
635 (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n",
636 table->keys - table->isolated);
637 #endif
638 }
639
640 return(1);
641
642 cuddSwappingOutOfMem:
643 while (moves != NULL) {
644 move = moves->next;
645 cuddDeallocMove(table, moves);
646 moves = move;
647 }
648
649 return(0);
650
651 } /* end of cuddSwapping */
652
653
654 /**
655 @brief Finds the next subtable with a larger index.
656
657 @return the index.
658
659 @sideeffect None
660
661 @see cuddNextLow
662
663 */
664 int
cuddNextHigh(DdManager * table,int x)665 cuddNextHigh(
666 DdManager * table,
667 int x)
668 {
669 (void) table; /* avoid warning */
670 return(x+1);
671
672 } /* end of cuddNextHigh */
673
674
675 /**
676 @brief Finds the next subtable with a smaller index.
677
678 @return the index.
679
680 @sideeffect None
681
682 @see cuddNextHigh
683
684 */
685 int
cuddNextLow(DdManager * table,int x)686 cuddNextLow(
687 DdManager * table,
688 int x)
689 {
690 (void) table; /* avoid warning */
691 return(x-1);
692
693 } /* end of cuddNextLow */
694
695
696 /**
697 @brief Swaps two adjacent variables.
698
699 @details It assumes that no dead nodes are present on entry to this
700 procedure. The procedure then guarantees that no dead nodes will be
701 present when it terminates. cuddSwapInPlace assumes that x < y.
702
703 @return the number of keys in the table if successful; 0 otherwise.
704
705 @sideeffect None
706
707 */
708 int
cuddSwapInPlace(DdManager * table,int x,int y)709 cuddSwapInPlace(
710 DdManager * table,
711 int x,
712 int y)
713 {
714 DdNodePtr *xlist, *ylist;
715 int xindex, yindex;
716 int xslots, yslots;
717 int xshift, yshift;
718 int oldxkeys, oldykeys;
719 int newxkeys, newykeys;
720 int comple, newcomplement;
721 int i;
722 Cudd_VariableType varType;
723 Cudd_LazyGroupType groupType;
724 int posn;
725 int isolated;
726 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
727 DdNode *g,*next;
728 DdNodePtr *previousP;
729 DdNode *tmp;
730 DdNode *sentinel = &(table->sentinel);
731 extern DD_OOMFP MMoutOfMemory;
732 DD_OOMFP saveHandler;
733
734 #ifdef DD_DEBUG
735 int count,idcheck;
736 #endif
737
738 #ifdef DD_DEBUG
739 assert(x < y);
740 assert(cuddNextHigh(table,x) == y);
741 assert(table->subtables[x].keys != 0);
742 assert(table->subtables[y].keys != 0);
743 assert(table->subtables[x].dead == 0);
744 assert(table->subtables[y].dead == 0);
745 #endif
746
747 table->ddTotalNumberSwapping++;
748
749 /* Get parameters of x subtable. */
750 xindex = table->invperm[x];
751 xlist = table->subtables[x].nodelist;
752 oldxkeys = table->subtables[x].keys;
753 xslots = table->subtables[x].slots;
754 xshift = table->subtables[x].shift;
755
756 /* Get parameters of y subtable. */
757 yindex = table->invperm[y];
758 ylist = table->subtables[y].nodelist;
759 oldykeys = table->subtables[y].keys;
760 yslots = table->subtables[y].slots;
761 yshift = table->subtables[y].shift;
762
763 if (!cuddTestInteract(table,xindex,yindex)) {
764 #ifdef DD_STATS
765 table->totalNISwaps++;
766 #endif
767 newxkeys = oldxkeys;
768 newykeys = oldykeys;
769 } else {
770 newxkeys = 0;
771 newykeys = oldykeys;
772
773 /* Check whether the two projection functions involved in this
774 ** swap are isolated. At the end, we'll be able to tell how many
775 ** isolated projection functions are there by checking only these
776 ** two functions again. This is done to eliminate the isolated
777 ** projection functions from the node count.
778 */
779 isolated = - ((table->vars[xindex]->ref == 1) +
780 (table->vars[yindex]->ref == 1));
781
782 /* The nodes in the x layer that do not depend on
783 ** y will stay there; the others are put in a chain.
784 ** The chain is handled as a LIFO; g points to the beginning.
785 */
786 g = NULL;
787 if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) &&
788 oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) {
789 for (i = 0; i < xslots; i++) {
790 previousP = &(xlist[i]);
791 f = *previousP;
792 while (f != sentinel) {
793 next = f->next;
794 f1 = cuddT(f); f0 = cuddE(f);
795 if (f1->index != (DdHalfWord) yindex &&
796 Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
797 /* stays */
798 newxkeys++;
799 *previousP = f;
800 previousP = &(f->next);
801 } else {
802 f->index = yindex;
803 f->next = g;
804 g = f;
805 }
806 f = next;
807 } /* while there are elements in the collision chain */
808 *previousP = sentinel;
809 } /* for each slot of the x subtable */
810 } else { /* resize xlist */
811 DdNode *h = NULL;
812 DdNodePtr *newxlist;
813 unsigned int newxslots;
814 int newxshift;
815 /* Empty current xlist. Nodes that stay go to list h;
816 ** nodes that move go to list g. */
817 for (i = 0; i < xslots; i++) {
818 f = xlist[i];
819 while (f != sentinel) {
820 next = f->next;
821 f1 = cuddT(f); f0 = cuddE(f);
822 if (f1->index != (DdHalfWord) yindex &&
823 Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
824 /* stays */
825 f->next = h;
826 h = f;
827 newxkeys++;
828 } else {
829 f->index = yindex;
830 f->next = g;
831 g = f;
832 }
833 f = next;
834 } /* while there are elements in the collision chain */
835 } /* for each slot of the x subtable */
836 /* Decide size of new subtable. */
837 newxshift = xshift;
838 newxslots = xslots;
839 while ((unsigned) oldxkeys > DD_MAX_SUBTABLE_DENSITY * newxslots) {
840 newxshift--;
841 newxslots <<= 1;
842 }
843 while ((unsigned) oldxkeys < newxslots &&
844 newxslots > table->initSlots) {
845 newxshift++;
846 newxslots >>= 1;
847 }
848 /* Try to allocate new table. Be ready to back off. */
849 saveHandler = MMoutOfMemory;
850 MMoutOfMemory = table->outOfMemCallback;
851 newxlist = ALLOC(DdNodePtr, newxslots);
852 MMoutOfMemory = saveHandler;
853 if (newxlist == NULL) {
854 (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i);
855 } else {
856 table->slots += ((int) newxslots - xslots);
857 table->minDead = (unsigned)
858 (table->gcFrac * (double) table->slots);
859 table->cacheSlack = (int)
860 ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO
861 * table->slots) - 2 * (int) table->cacheSlots;
862 table->memused +=
863 ((int) newxslots - xslots) * sizeof(DdNodePtr);
864 FREE(xlist);
865 xslots = newxslots;
866 xshift = newxshift;
867 xlist = newxlist;
868 }
869 /* Initialize new subtable. */
870 for (i = 0; i < xslots; i++) {
871 xlist[i] = sentinel;
872 }
873 /* Move nodes that were parked in list h to their new home. */
874 f = h;
875 while (f != NULL) {
876 next = f->next;
877 f1 = cuddT(f);
878 f0 = cuddE(f);
879 /* Check xlist for pair (f11,f01). */
880 posn = ddHash(f1, f0, xshift);
881 /* For each element tmp in collision list xlist[posn]. */
882 previousP = &(xlist[posn]);
883 tmp = *previousP;
884 while (f1 < cuddT(tmp)) {
885 previousP = &(tmp->next);
886 tmp = *previousP;
887 }
888 while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) {
889 previousP = &(tmp->next);
890 tmp = *previousP;
891 }
892 f->next = *previousP;
893 *previousP = f;
894 f = next;
895 }
896 }
897
898 #ifdef DD_COUNT
899 table->swapSteps += oldxkeys - newxkeys;
900 #endif
901 /* Take care of the x nodes that must be re-expressed.
902 ** They form a linked list pointed by g. Their index has been
903 ** already changed to yindex.
904 */
905 f = g;
906 while (f != NULL) {
907 next = f->next;
908 /* Find f1, f0, f11, f10, f01, f00. */
909 f1 = cuddT(f);
910 #ifdef DD_DEBUG
911 assert(!(Cudd_IsComplement(f1)));
912 #endif
913 if ((int) f1->index == yindex) {
914 f11 = cuddT(f1); f10 = cuddE(f1);
915 } else {
916 f11 = f10 = f1;
917 }
918 #ifdef DD_DEBUG
919 assert(!(Cudd_IsComplement(f11)));
920 #endif
921 f0 = cuddE(f);
922 comple = Cudd_IsComplement(f0);
923 f0 = Cudd_Regular(f0);
924 if ((int) f0->index == yindex) {
925 f01 = cuddT(f0); f00 = cuddE(f0);
926 } else {
927 f01 = f00 = f0;
928 }
929 if (comple) {
930 f01 = Cudd_Not(f01);
931 f00 = Cudd_Not(f00);
932 }
933 /* Decrease ref count of f1. */
934 cuddSatDec(f1->ref);
935 /* Create the new T child. */
936 if (f11 == f01) {
937 newf1 = f11;
938 cuddSatInc(newf1->ref);
939 } else {
940 /* Check xlist for triple (xindex,f11,f01). */
941 posn = ddHash(f11, f01, xshift);
942 /* For each element newf1 in collision list xlist[posn]. */
943 previousP = &(xlist[posn]);
944 newf1 = *previousP;
945 while (f11 < cuddT(newf1)) {
946 previousP = &(newf1->next);
947 newf1 = *previousP;
948 }
949 while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) {
950 previousP = &(newf1->next);
951 newf1 = *previousP;
952 }
953 if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
954 cuddSatInc(newf1->ref);
955 } else { /* no match */
956 newf1 = cuddDynamicAllocNode(table);
957 if (newf1 == NULL)
958 goto cuddSwapOutOfMem;
959 newf1->index = xindex; newf1->ref = 1;
960 cuddT(newf1) = f11;
961 cuddE(newf1) = f01;
962 /* Insert newf1 in the collision list xlist[posn];
963 ** increase the ref counts of f11 and f01.
964 */
965 newxkeys++;
966 newf1->next = *previousP;
967 *previousP = newf1;
968 cuddSatInc(f11->ref);
969 tmp = Cudd_Regular(f01);
970 cuddSatInc(tmp->ref);
971 }
972 }
973 cuddT(f) = newf1;
974 #ifdef DD_DEBUG
975 assert(!(Cudd_IsComplement(newf1)));
976 #endif
977
978 /* Do the same for f0, keeping complement dots into account. */
979 /* Decrease ref count of f0. */
980 tmp = Cudd_Regular(f0);
981 cuddSatDec(tmp->ref);
982 /* Create the new E child. */
983 if (f10 == f00) {
984 newf0 = f00;
985 tmp = Cudd_Regular(newf0);
986 cuddSatInc(tmp->ref);
987 } else {
988 /* make sure f10 is regular */
989 newcomplement = Cudd_IsComplement(f10);
990 if (newcomplement) {
991 f10 = Cudd_Not(f10);
992 f00 = Cudd_Not(f00);
993 }
994 /* Check xlist for triple (xindex,f10,f00). */
995 posn = ddHash(f10, f00, xshift);
996 /* For each element newf0 in collision list xlist[posn]. */
997 previousP = &(xlist[posn]);
998 newf0 = *previousP;
999 while (f10 < cuddT(newf0)) {
1000 previousP = &(newf0->next);
1001 newf0 = *previousP;
1002 }
1003 while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) {
1004 previousP = &(newf0->next);
1005 newf0 = *previousP;
1006 }
1007 if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
1008 cuddSatInc(newf0->ref);
1009 } else { /* no match */
1010 newf0 = cuddDynamicAllocNode(table);
1011 if (newf0 == NULL)
1012 goto cuddSwapOutOfMem;
1013 newf0->index = xindex; newf0->ref = 1;
1014 cuddT(newf0) = f10;
1015 cuddE(newf0) = f00;
1016 /* Insert newf0 in the collision list xlist[posn];
1017 ** increase the ref counts of f10 and f00.
1018 */
1019 newxkeys++;
1020 newf0->next = *previousP;
1021 *previousP = newf0;
1022 cuddSatInc(f10->ref);
1023 tmp = Cudd_Regular(f00);
1024 cuddSatInc(tmp->ref);
1025 }
1026 if (newcomplement) {
1027 newf0 = Cudd_Not(newf0);
1028 }
1029 }
1030 cuddE(f) = newf0;
1031
1032 /* Insert the modified f in ylist.
1033 ** The modified f does not already exists in ylist.
1034 ** (Because of the uniqueness of the cofactors.)
1035 */
1036 posn = ddHash(newf1, newf0, yshift);
1037 newykeys++;
1038 previousP = &(ylist[posn]);
1039 tmp = *previousP;
1040 while (newf1 < cuddT(tmp)) {
1041 previousP = &(tmp->next);
1042 tmp = *previousP;
1043 }
1044 while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
1045 previousP = &(tmp->next);
1046 tmp = *previousP;
1047 }
1048 f->next = *previousP;
1049 *previousP = f;
1050 f = next;
1051 } /* while f != NULL */
1052
1053 /* GC the y layer. */
1054
1055 /* For each node f in ylist. */
1056 for (i = 0; i < yslots; i++) {
1057 previousP = &(ylist[i]);
1058 f = *previousP;
1059 while (f != sentinel) {
1060 next = f->next;
1061 if (f->ref == 0) {
1062 tmp = cuddT(f);
1063 cuddSatDec(tmp->ref);
1064 tmp = Cudd_Regular(cuddE(f));
1065 cuddSatDec(tmp->ref);
1066 cuddDeallocNode(table,f);
1067 newykeys--;
1068 } else {
1069 *previousP = f;
1070 previousP = &(f->next);
1071 }
1072 f = next;
1073 } /* while f */
1074 *previousP = sentinel;
1075 } /* for i */
1076
1077 #ifdef DD_DEBUG
1078 #if 0
1079 (void) fprintf(table->out,"Swapping %d and %d\n",x,y);
1080 #endif
1081 count = 0;
1082 idcheck = 0;
1083 for (i = 0; i < yslots; i++) {
1084 f = ylist[i];
1085 while (f != sentinel) {
1086 count++;
1087 if (f->index != (DdHalfWord) yindex)
1088 idcheck++;
1089 f = f->next;
1090 }
1091 }
1092 if (count != newykeys) {
1093 (void) fprintf(table->out,
1094 "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",
1095 oldykeys,newykeys,count);
1096 }
1097 if (idcheck != 0)
1098 (void) fprintf(table->out,
1099 "Error in id's of ylist\twrong id's = %d\n",
1100 idcheck);
1101 count = 0;
1102 idcheck = 0;
1103 for (i = 0; i < xslots; i++) {
1104 f = xlist[i];
1105 while (f != sentinel) {
1106 count++;
1107 if (f->index != (DdHalfWord) xindex)
1108 idcheck++;
1109 f = f->next;
1110 }
1111 }
1112 if (count != newxkeys) {
1113 (void) fprintf(table->out,
1114 "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",
1115 oldxkeys,newxkeys,count);
1116 }
1117 if (idcheck != 0)
1118 (void) fprintf(table->out,
1119 "Error in id's of xlist\twrong id's = %d\n",
1120 idcheck);
1121 #endif
1122
1123 isolated += (table->vars[xindex]->ref == 1) +
1124 (table->vars[yindex]->ref == 1);
1125 table->isolated += (unsigned int) isolated;
1126 }
1127
1128 /* Set the appropriate fields in table. */
1129 table->subtables[x].nodelist = ylist;
1130 table->subtables[x].slots = yslots;
1131 table->subtables[x].shift = yshift;
1132 table->subtables[x].keys = newykeys;
1133 table->subtables[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY;
1134 i = table->subtables[x].bindVar;
1135 table->subtables[x].bindVar = table->subtables[y].bindVar;
1136 table->subtables[y].bindVar = i;
1137 /* Adjust fields for lazy sifting. */
1138 varType = table->subtables[x].varType;
1139 table->subtables[x].varType = table->subtables[y].varType;
1140 table->subtables[y].varType = varType;
1141 i = table->subtables[x].pairIndex;
1142 table->subtables[x].pairIndex = table->subtables[y].pairIndex;
1143 table->subtables[y].pairIndex = i;
1144 i = table->subtables[x].varHandled;
1145 table->subtables[x].varHandled = table->subtables[y].varHandled;
1146 table->subtables[y].varHandled = i;
1147 groupType = table->subtables[x].varToBeGrouped;
1148 table->subtables[x].varToBeGrouped = table->subtables[y].varToBeGrouped;
1149 table->subtables[y].varToBeGrouped = groupType;
1150
1151 table->subtables[y].nodelist = xlist;
1152 table->subtables[y].slots = xslots;
1153 table->subtables[y].shift = xshift;
1154 table->subtables[y].keys = newxkeys;
1155 table->subtables[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY;
1156
1157 table->perm[xindex] = y; table->perm[yindex] = x;
1158 table->invperm[x] = yindex; table->invperm[y] = xindex;
1159
1160 table->keys += newxkeys + newykeys - oldxkeys - oldykeys;
1161
1162 return((int)(table->keys - table->isolated));
1163
1164 cuddSwapOutOfMem:
1165 (void) fprintf(table->err,"Error: cuddSwapInPlace out of memory\n");
1166
1167 return (0);
1168
1169 } /* end of cuddSwapInPlace */
1170
1171
1172 /**
1173 @brief Reorders %BDD variables according to the order of the %ZDD
1174 variables.
1175
1176 @details This function can be called at the end of %ZDD
1177 reordering to insure that the order of the %BDD variables is
1178 consistent with the order of the %ZDD variables. The number of %ZDD
1179 variables must be a multiple of the number of %BDD variables. Let
1180 <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd
1181 then considers the %ZDD variables from <code>M*i</code> to
1182 <code>(M+1)*i-1</code> as corresponding to %BDD variable
1183 <code>i</code>. This function should be normally called from
1184 Cudd_zddReduceHeap, which clears the cache.
1185
1186 @return 1 in case of success; 0 otherwise.
1187
1188 @sideeffect Changes the %BDD variable order for all diagrams and performs
1189 garbage collection of the %BDD unique table.
1190
1191 @see Cudd_ShuffleHeap Cudd_zddReduceHeap
1192
1193 */
1194 int
cuddBddAlignToZdd(DdManager * table)1195 cuddBddAlignToZdd(
1196 DdManager * table /**< %DD manager */)
1197 {
1198 int *invperm; /* permutation array */
1199 int M; /* ratio of ZDD variables to BDD variables */
1200 int i; /* loop index */
1201 int result; /* return value */
1202
1203 /* We assume that a ratio of 0 is OK. */
1204 if (table->size == 0)
1205 return(1);
1206
1207 M = table->sizeZ / table->size;
1208 /* Check whether the number of ZDD variables is a multiple of the
1209 ** number of BDD variables.
1210 */
1211 if (M * table->size != table->sizeZ)
1212 return(0);
1213 /* Create and initialize the inverse permutation array. */
1214 invperm = ALLOC(int,table->size);
1215 if (invperm == NULL) {
1216 table->errorCode = CUDD_MEMORY_OUT;
1217 return(0);
1218 }
1219 for (i = 0; i < table->sizeZ; i += M) {
1220 int indexZ = table->invpermZ[i];
1221 int index = indexZ / M;
1222 invperm[i / M] = index;
1223 }
1224 /* Eliminate dead nodes. Do not scan the cache again, because we
1225 ** assume that Cudd_zddReduceHeap has already cleared it.
1226 */
1227 cuddGarbageCollect(table,0);
1228
1229 /* Initialize number of isolated projection functions. */
1230 table->isolated = 0;
1231 for (i = 0; i < table->size; i++) {
1232 if (table->vars[i]->ref == 1) table->isolated++;
1233 }
1234
1235 /* Initialize the interaction matrix. */
1236 result = cuddInitInteract(table);
1237 if (result == 0) return(0);
1238
1239 result = ddShuffle(table, invperm);
1240 FREE(invperm);
1241 /* Free interaction matrix. */
1242 FREE(table->interact);
1243 /* Fix the BDD variable group tree. */
1244 bddFixTree(table,table->tree);
1245 return(result);
1246
1247 } /* end of cuddBddAlignToZdd */
1248
1249 /*---------------------------------------------------------------------------*/
1250 /* Definition of static functions */
1251 /*---------------------------------------------------------------------------*/
1252
1253
1254 /**
1255 @brief Comparison function used by qsort.
1256
1257 @details Used to order the variables according to the number of keys
1258 in the subtables.
1259
1260 @return the difference in number of keys between the two variables
1261 being compared.
1262
1263 @sideeffect None
1264
1265 */
1266 static int
ddUniqueCompare(void const * ptrX,void const * ptrY)1267 ddUniqueCompare(
1268 void const * ptrX,
1269 void const * ptrY)
1270 {
1271 IndexKey const * pX = (IndexKey const *) ptrX;
1272 IndexKey const * pY = (IndexKey const *) ptrY;
1273 #if 0
1274 /* This would make the order stable, which would be good because of
1275 * it would platform-independent, but instability often produces
1276 * smaller BDDs.
1277 */
1278 if (pY->keys == pX->keys) {
1279 return(pX->index - pY->index);
1280 }
1281 #endif
1282 return(pY->keys - pX->keys);
1283
1284 } /* end of ddUniqueCompare */
1285
1286
1287 /**
1288 @brief Swaps any two variables.
1289
1290 @return the set of moves.
1291
1292 @sideeffect None
1293
1294 */
1295 static Move *
ddSwapAny(DdManager * table,int x,int y)1296 ddSwapAny(
1297 DdManager * table,
1298 int x,
1299 int y)
1300 {
1301 Move *move, *moves;
1302 int xRef,yRef;
1303 int xNext,yNext;
1304 int size;
1305 int limitSize;
1306 int tmp;
1307
1308 if (x >y) {
1309 tmp = x; x = y; y = tmp;
1310 }
1311
1312 xRef = x; yRef = y;
1313
1314 xNext = cuddNextHigh(table,x);
1315 yNext = cuddNextLow(table,y);
1316 moves = NULL;
1317 limitSize = (int) (table->keys - table->isolated);
1318
1319 for (;;) {
1320 if ( xNext == yNext) {
1321 size = cuddSwapInPlace(table,x,xNext);
1322 if (size == 0) goto ddSwapAnyOutOfMem;
1323 move = (Move *) cuddDynamicAllocNode(table);
1324 if (move == NULL) goto ddSwapAnyOutOfMem;
1325 move->x = x;
1326 move->y = xNext;
1327 move->size = size;
1328 move->next = moves;
1329 moves = move;
1330
1331 size = cuddSwapInPlace(table,yNext,y);
1332 if (size == 0) goto ddSwapAnyOutOfMem;
1333 move = (Move *) cuddDynamicAllocNode(table);
1334 if (move == NULL) goto ddSwapAnyOutOfMem;
1335 move->x = yNext;
1336 move->y = y;
1337 move->size = size;
1338 move->next = moves;
1339 moves = move;
1340
1341 size = cuddSwapInPlace(table,x,xNext);
1342 if (size == 0) goto ddSwapAnyOutOfMem;
1343 move = (Move *) cuddDynamicAllocNode(table);
1344 if (move == NULL) goto ddSwapAnyOutOfMem;
1345 move->x = x;
1346 move->y = xNext;
1347 move->size = size;
1348 move->next = moves;
1349 moves = move;
1350
1351 tmp = x; x = y; y = tmp;
1352
1353 } else if (x == yNext) {
1354
1355 size = cuddSwapInPlace(table,x,xNext);
1356 if (size == 0) goto ddSwapAnyOutOfMem;
1357 move = (Move *) cuddDynamicAllocNode(table);
1358 if (move == NULL) goto ddSwapAnyOutOfMem;
1359 move->x = x;
1360 move->y = xNext;
1361 move->size = size;
1362 move->next = moves;
1363 moves = move;
1364
1365 tmp = x; x = y; y = tmp;
1366
1367 } else {
1368 size = cuddSwapInPlace(table,x,xNext);
1369 if (size == 0) goto ddSwapAnyOutOfMem;
1370 move = (Move *) cuddDynamicAllocNode(table);
1371 if (move == NULL) goto ddSwapAnyOutOfMem;
1372 move->x = x;
1373 move->y = xNext;
1374 move->size = size;
1375 move->next = moves;
1376 moves = move;
1377
1378 size = cuddSwapInPlace(table,yNext,y);
1379 if (size == 0) goto ddSwapAnyOutOfMem;
1380 move = (Move *) cuddDynamicAllocNode(table);
1381 if (move == NULL) goto ddSwapAnyOutOfMem;
1382 move->x = yNext;
1383 move->y = y;
1384 move->size = size;
1385 move->next = moves;
1386 moves = move;
1387
1388 x = xNext;
1389 y = yNext;
1390 }
1391
1392 xNext = cuddNextHigh(table,x);
1393 yNext = cuddNextLow(table,y);
1394 if (xNext > yRef) break;
1395
1396 if ((double) size > table->maxGrowth * (double) limitSize) break;
1397 if (size < limitSize) limitSize = size;
1398 }
1399 if (yNext>=xRef) {
1400 size = cuddSwapInPlace(table,yNext,y);
1401 if (size == 0) goto ddSwapAnyOutOfMem;
1402 move = (Move *) cuddDynamicAllocNode(table);
1403 if (move == NULL) goto ddSwapAnyOutOfMem;
1404 move->x = yNext;
1405 move->y = y;
1406 move->size = size;
1407 move->next = moves;
1408 moves = move;
1409 }
1410
1411 return(moves);
1412
1413 ddSwapAnyOutOfMem:
1414 while (moves != NULL) {
1415 move = moves->next;
1416 cuddDeallocMove(table, moves);
1417 moves = move;
1418 }
1419 return(NULL);
1420
1421 } /* end of ddSwapAny */
1422
1423
1424 /**
1425 @brief Given xLow <= x <= xHigh moves x up and down between the
1426 boundaries.
1427
1428 @details Finds the best position and does the required changes.
1429
1430 @return 1 if successful; 0 otherwise.
1431
1432 @sideeffect None
1433
1434 */
1435 static int
ddSiftingAux(DdManager * table,int x,int xLow,int xHigh)1436 ddSiftingAux(
1437 DdManager * table,
1438 int x,
1439 int xLow,
1440 int xHigh)
1441 {
1442
1443 Move *move;
1444 Move *moveUp; /* list of up moves */
1445 Move *moveDown; /* list of down moves */
1446 int initialSize;
1447 int result;
1448
1449 initialSize = (int) (table->keys - table->isolated);
1450
1451 moveDown = NULL;
1452 moveUp = NULL;
1453
1454 if (x == xLow) {
1455 moveDown = ddSiftingDown(table,x,xHigh);
1456 /* At this point x --> xHigh unless bounding occurred. */
1457 if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1458 /* Move backward and stop at best position. */
1459 result = ddSiftingBackward(table,initialSize,moveDown);
1460 if (!result) goto ddSiftingAuxOutOfMem;
1461
1462 } else if (x == xHigh) {
1463 moveUp = ddSiftingUp(table,x,xLow);
1464 /* At this point x --> xLow unless bounding occurred. */
1465 if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1466 /* Move backward and stop at best position. */
1467 result = ddSiftingBackward(table,initialSize,moveUp);
1468 if (!result) goto ddSiftingAuxOutOfMem;
1469
1470 } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
1471 moveDown = ddSiftingDown(table,x,xHigh);
1472 /* At this point x --> xHigh unless bounding occurred. */
1473 if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1474 if (moveDown != NULL) {
1475 x = moveDown->y;
1476 }
1477 moveUp = ddSiftingUp(table,x,xLow);
1478 if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1479 /* Move backward and stop at best position */
1480 result = ddSiftingBackward(table,initialSize,moveUp);
1481 if (!result) goto ddSiftingAuxOutOfMem;
1482
1483 } else { /* must go up first: shorter */
1484 moveUp = ddSiftingUp(table,x,xLow);
1485 /* At this point x --> xLow unless bounding occurred. */
1486 if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1487 if (moveUp != NULL) {
1488 x = moveUp->x;
1489 }
1490 moveDown = ddSiftingDown(table,x,xHigh);
1491 if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1492 /* Move backward and stop at best position. */
1493 result = ddSiftingBackward(table,initialSize,moveDown);
1494 if (!result) goto ddSiftingAuxOutOfMem;
1495 }
1496
1497 while (moveDown != NULL) {
1498 move = moveDown->next;
1499 cuddDeallocMove(table, moveDown);
1500 moveDown = move;
1501 }
1502 while (moveUp != NULL) {
1503 move = moveUp->next;
1504 cuddDeallocMove(table, moveUp);
1505 moveUp = move;
1506 }
1507
1508 return(1);
1509
1510 ddSiftingAuxOutOfMem:
1511 if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
1512 while (moveDown != NULL) {
1513 move = moveDown->next;
1514 cuddDeallocMove(table, moveDown);
1515 moveDown = move;
1516 }
1517 }
1518 if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
1519 while (moveUp != NULL) {
1520 move = moveUp->next;
1521 cuddDeallocMove(table, moveUp);
1522 moveUp = move;
1523 }
1524 }
1525
1526 return(0);
1527
1528 } /* end of ddSiftingAux */
1529
1530
1531 /**
1532 @brief Sifts a variable up.
1533
1534 @details Moves y up until either it reaches the bound (xLow) or the
1535 size of the %DD heap increases too much.
1536
1537 @return the set of moves in case of success; NULL if memory is full.
1538
1539 @sideeffect None
1540
1541 */
1542 static Move *
ddSiftingUp(DdManager * table,int y,int xLow)1543 ddSiftingUp(
1544 DdManager * table,
1545 int y,
1546 int xLow)
1547 {
1548 Move *moves;
1549 Move *move;
1550 int x;
1551 int size;
1552 int limitSize;
1553 int xindex, yindex;
1554 int isolated;
1555 int L; /* lower bound on DD size */
1556 #ifdef DD_DEBUG
1557 int checkL;
1558 int z;
1559 int zindex;
1560 #endif
1561
1562 moves = NULL;
1563 yindex = table->invperm[y];
1564
1565 /* Initialize the lower bound.
1566 ** The part of the DD below y will not change.
1567 ** The part of the DD above y that does not interact with y will not
1568 ** change. The rest may vanish in the best case, except for
1569 ** the nodes at level xLow, which will not vanish, regardless.
1570 */
1571 limitSize = L = (int) (table->keys - table->isolated);
1572 for (x = xLow + 1; x < y; x++) {
1573 xindex = table->invperm[x];
1574 if (cuddTestInteract(table,xindex,yindex)) {
1575 isolated = table->vars[xindex]->ref == 1;
1576 L -= table->subtables[x].keys - isolated;
1577 }
1578 }
1579 isolated = table->vars[yindex]->ref == 1;
1580 L -= (int) table->subtables[y].keys - isolated;
1581
1582 x = cuddNextLow(table,y);
1583 while (x >= xLow && L <= limitSize) {
1584 xindex = table->invperm[x];
1585 #ifdef DD_DEBUG
1586 checkL = (int) (table->keys - table->isolated);
1587 for (z = xLow + 1; z < y; z++) {
1588 zindex = table->invperm[z];
1589 if (cuddTestInteract(table,zindex,yindex)) {
1590 isolated = table->vars[zindex]->ref == 1;
1591 checkL -= (int) table->subtables[z].keys - isolated;
1592 }
1593 }
1594 isolated = table->vars[yindex]->ref == 1;
1595 checkL -= (int) table->subtables[y].keys - isolated;
1596 assert(L == checkL);
1597 #endif
1598 size = cuddSwapInPlace(table,x,y);
1599 if (size == 0) goto ddSiftingUpOutOfMem;
1600 /* Update the lower bound. */
1601 if (cuddTestInteract(table,xindex,yindex)) {
1602 isolated = table->vars[xindex]->ref == 1;
1603 L += (int) table->subtables[y].keys - isolated;
1604 }
1605 move = (Move *) cuddDynamicAllocNode(table);
1606 if (move == NULL) goto ddSiftingUpOutOfMem;
1607 move->x = x;
1608 move->y = y;
1609 move->size = size;
1610 move->next = moves;
1611 moves = move;
1612 if ((double) size > (double) limitSize * table->maxGrowth) break;
1613 if (size < limitSize) limitSize = size;
1614 y = x;
1615 x = cuddNextLow(table,y);
1616 }
1617 return(moves);
1618
1619 ddSiftingUpOutOfMem:
1620 while (moves != NULL) {
1621 move = moves->next;
1622 cuddDeallocMove(table, moves);
1623 moves = move;
1624 }
1625 return((Move *) CUDD_OUT_OF_MEM);
1626
1627 } /* end of ddSiftingUp */
1628
1629
1630 /**
1631 @brief Sifts a variable down.
1632
1633 @details Moves x down until either it reaches the bound (xHigh) or
1634 the size of the %DD heap increases too much.
1635
1636 @return the set of moves in case of success; NULL if memory is full.
1637
1638 @sideeffect None
1639
1640 */
1641 static Move *
ddSiftingDown(DdManager * table,int x,int xHigh)1642 ddSiftingDown(
1643 DdManager * table,
1644 int x,
1645 int xHigh)
1646 {
1647 Move *moves;
1648 Move *move;
1649 int y;
1650 int size;
1651 int R; /* upper bound on node decrease */
1652 int limitSize;
1653 int xindex, yindex;
1654 int isolated;
1655 #ifdef DD_DEBUG
1656 int checkR;
1657 int z;
1658 int zindex;
1659 #endif
1660
1661 moves = NULL;
1662 /* Initialize R */
1663 xindex = table->invperm[x];
1664 limitSize = size = (int) (table->keys - table->isolated);
1665 R = 0;
1666 for (y = xHigh; y > x; y--) {
1667 yindex = table->invperm[y];
1668 if (cuddTestInteract(table,xindex,yindex)) {
1669 isolated = table->vars[yindex]->ref == 1;
1670 R += (int) table->subtables[y].keys - isolated;
1671 }
1672 }
1673
1674 y = cuddNextHigh(table,x);
1675 while (y <= xHigh && size - R < limitSize) {
1676 #ifdef DD_DEBUG
1677 checkR = 0;
1678 for (z = xHigh; z > x; z--) {
1679 zindex = table->invperm[z];
1680 if (cuddTestInteract(table,xindex,zindex)) {
1681 isolated = table->vars[zindex]->ref == 1;
1682 checkR += (int) table->subtables[z].keys - isolated;
1683 }
1684 }
1685 assert(R == checkR);
1686 #endif
1687 /* Update upper bound on node decrease. */
1688 yindex = table->invperm[y];
1689 if (cuddTestInteract(table,xindex,yindex)) {
1690 isolated = table->vars[yindex]->ref == 1;
1691 R -= (int) table->subtables[y].keys - isolated;
1692 }
1693 size = cuddSwapInPlace(table,x,y);
1694 if (size == 0) goto ddSiftingDownOutOfMem;
1695 move = (Move *) cuddDynamicAllocNode(table);
1696 if (move == NULL) goto ddSiftingDownOutOfMem;
1697 move->x = x;
1698 move->y = y;
1699 move->size = size;
1700 move->next = moves;
1701 moves = move;
1702 if ((double) size > (double) limitSize * table->maxGrowth) break;
1703 if (size < limitSize) limitSize = size;
1704 x = y;
1705 y = cuddNextHigh(table,x);
1706 }
1707 return(moves);
1708
1709 ddSiftingDownOutOfMem:
1710 while (moves != NULL) {
1711 move = moves->next;
1712 cuddDeallocMove(table, moves);
1713 moves = move;
1714 }
1715 return((Move *) CUDD_OUT_OF_MEM);
1716
1717 } /* end of ddSiftingDown */
1718
1719
1720 /**
1721 @brief Given a set of moves, returns the %DD heap to the position
1722 giving the minimum size.
1723
1724 @details In case of ties, returns to the closest position giving the
1725 minimum size.
1726
1727 @return 1 in case of success; 0 otherwise.
1728
1729 @sideeffect None
1730
1731 */
1732 static int
ddSiftingBackward(DdManager * table,int size,Move * moves)1733 ddSiftingBackward(
1734 DdManager * table,
1735 int size,
1736 Move * moves)
1737 {
1738 Move *move;
1739 int res;
1740
1741 for (move = moves; move != NULL; move = move->next) {
1742 if (move->size < size) {
1743 size = move->size;
1744 }
1745 }
1746
1747 for (move = moves; move != NULL; move = move->next) {
1748 if (move->size == size) return(1);
1749 res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1750 if (!res) return(0);
1751 }
1752
1753 return(1);
1754
1755 } /* end of ddSiftingBackward */
1756
1757
1758 /**
1759 @brief Prepares the %DD heap for dynamic reordering.
1760
1761 @details Does garbage collection, to guarantee that there are no
1762 dead nodes; clears the cache, which is invalidated by dynamic
1763 reordering; initializes the number of isolated projection functions;
1764 and initializes the interaction matrix.
1765
1766 @return 1 in case of success; 0 otherwise.
1767
1768 @sideeffect None
1769
1770 */
1771 static int
ddReorderPreprocess(DdManager * table)1772 ddReorderPreprocess(
1773 DdManager * table)
1774 {
1775 int i;
1776 int res;
1777
1778 /* Clear the cache. */
1779 cuddCacheFlush(table);
1780 cuddLocalCacheClearAll(table);
1781
1782 /* Eliminate dead nodes. Do not scan the cache again. */
1783 cuddGarbageCollect(table,0);
1784
1785 /* Initialize number of isolated projection functions. */
1786 table->isolated = 0;
1787 for (i = 0; i < table->size; i++) {
1788 if (table->vars[i]->ref == 1) table->isolated++;
1789 }
1790
1791 /* Initialize the interaction matrix. */
1792 res = cuddInitInteract(table);
1793 if (res == 0) return(0);
1794
1795 return(1);
1796
1797 } /* end of ddReorderPreprocess */
1798
1799
1800 /**
1801 @brief Cleans up at the end of reordering.
1802
1803 @sideeffect None
1804
1805 */
1806 static int
ddReorderPostprocess(DdManager * table)1807 ddReorderPostprocess(
1808 DdManager * table)
1809 {
1810
1811 #ifdef DD_VERBOSE
1812 (void) fflush(table->out);
1813 #endif
1814
1815 /* Free interaction matrix. */
1816 FREE(table->interact);
1817
1818 return(1);
1819
1820 } /* end of ddReorderPostprocess */
1821
1822
1823 /**
1824 @brief Reorders variables according to a given permutation.
1825
1826 @details The i-th permutation array contains the index of the
1827 variable that should be brought to the i-th level. ddShuffle assumes
1828 that no dead nodes are present and that the interaction matrix is
1829 properly initialized. The reordering is achieved by a series of
1830 upward sifts.
1831
1832 @return 1 if successful; 0 otherwise.
1833
1834 @sideeffect None
1835
1836 */
1837 static int
ddShuffle(DdManager * table,int * permutation)1838 ddShuffle(
1839 DdManager * table,
1840 int * permutation)
1841 {
1842 int index;
1843 int level;
1844 int position;
1845 int numvars;
1846 int result;
1847 #ifdef DD_STATS
1848 unsigned long localTime;
1849 int initialSize;
1850 int finalSize;
1851 int previousSize;
1852 #endif
1853
1854 table->ddTotalNumberSwapping = 0;
1855 #ifdef DD_STATS
1856 localTime = util_cpu_time();
1857 initialSize = table->keys - table->isolated;
1858 (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
1859 initialSize);
1860 table->totalNISwaps = 0;
1861 #endif
1862
1863 numvars = table->size;
1864
1865 for (level = 0; level < numvars; level++) {
1866 index = permutation[level];
1867 position = table->perm[index];
1868 #ifdef DD_STATS
1869 previousSize = table->keys - table->isolated;
1870 #endif
1871 result = ddSiftUp(table,position,level);
1872 if (!result) return(0);
1873 #ifdef DD_STATS
1874 if (table->keys < (unsigned) previousSize + table->isolated) {
1875 (void) fprintf(table->out,"-");
1876 } else if (table->keys > (unsigned) previousSize + table->isolated) {
1877 (void) fprintf(table->out,"+"); /* should never happen */
1878 } else {
1879 (void) fprintf(table->out,"=");
1880 }
1881 fflush(table->out);
1882 #endif
1883 }
1884
1885 #ifdef DD_STATS
1886 (void) fprintf(table->out,"\n");
1887 finalSize = table->keys - table->isolated;
1888 (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize);
1889 (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
1890 ((double)(util_cpu_time() - localTime)/1000.0));
1891 (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
1892 table->ddTotalNumberSwapping);
1893 (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",
1894 table->totalNISwaps);
1895 #endif
1896
1897 return(1);
1898
1899 } /* end of ddShuffle */
1900
1901
1902 /**
1903 @brief Moves one variable up.
1904
1905 @details Takes a variable from position x and sifts it up to
1906 position xLow; xLow should be less than or equal to x.
1907
1908 @return 1 if successful; 0 otherwise
1909
1910 @sideeffect None
1911
1912 */
1913 static int
ddSiftUp(DdManager * table,int x,int xLow)1914 ddSiftUp(
1915 DdManager * table,
1916 int x,
1917 int xLow)
1918 {
1919 int y;
1920 int size;
1921
1922 y = cuddNextLow(table,x);
1923 while (y >= xLow) {
1924 size = cuddSwapInPlace(table,y,x);
1925 if (size == 0) {
1926 return(0);
1927 }
1928 x = y;
1929 y = cuddNextLow(table,x);
1930 }
1931 return(1);
1932
1933 } /* end of ddSiftUp */
1934
1935
1936 /**
1937 @brief Fixes the %BDD variable group tree after a shuffle.
1938
1939 @details Assumes that the order of the variables in a terminal node
1940 has not been changed.
1941
1942 @sideeffect Changes the %BDD variable group tree.
1943
1944 */
1945 static void
bddFixTree(DdManager * table,MtrNode * treenode)1946 bddFixTree(
1947 DdManager * table,
1948 MtrNode * treenode)
1949 {
1950 if (treenode == NULL) return;
1951 treenode->low = ((int) treenode->index < table->size) ?
1952 (MtrHalfWord) table->perm[treenode->index] : treenode->index;
1953 if (treenode->child != NULL) {
1954 bddFixTree(table, treenode->child);
1955 }
1956 if (treenode->younger != NULL)
1957 bddFixTree(table, treenode->younger);
1958 if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
1959 treenode->parent->low = treenode->low;
1960 treenode->parent->index = treenode->index;
1961 }
1962 return;
1963
1964 } /* end of bddFixTree */
1965
1966
1967 /**
1968 @brief Updates the %BDD variable group tree before a shuffle.
1969
1970 @return 1 if successful; 0 otherwise.
1971
1972 @sideeffect Changes the %BDD variable group tree.
1973
1974 */
1975 static int
ddUpdateMtrTree(DdManager * table,MtrNode * treenode,int * perm,int * invperm)1976 ddUpdateMtrTree(
1977 DdManager * table,
1978 MtrNode * treenode,
1979 int * perm,
1980 int * invperm)
1981 {
1982 unsigned int i, size;
1983 int index, level, minLevel, maxLevel, minIndex;
1984
1985 if (treenode == NULL) return(1);
1986
1987 minLevel = CUDD_MAXINDEX;
1988 maxLevel = 0;
1989 minIndex = -1;
1990 /* i : level */
1991 for (i = treenode->low; i < treenode->low + treenode->size; i++) {
1992 index = table->invperm[i];
1993 level = perm[index];
1994 if (level < minLevel) {
1995 minLevel = level;
1996 minIndex = index;
1997 }
1998 if (level > maxLevel)
1999 maxLevel = level;
2000 }
2001 size = maxLevel - minLevel + 1;
2002 if (minIndex == -1) return(0);
2003 if (size == treenode->size) {
2004 treenode->low = minLevel;
2005 treenode->index = minIndex;
2006 } else {
2007 return(0);
2008 }
2009
2010 if (treenode->child != NULL) {
2011 if (!ddUpdateMtrTree(table, treenode->child, perm, invperm))
2012 return(0);
2013 }
2014 if (treenode->younger != NULL) {
2015 if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm))
2016 return(0);
2017 }
2018 return(1);
2019 }
2020
2021
2022 /**
2023 @brief Checks the %BDD variable group tree before a shuffle.
2024
2025 @return 1 if successful; 0 otherwise.
2026
2027 @sideeffect Changes the %BDD variable group tree.
2028
2029 */
2030 static int
ddCheckPermuation(DdManager * table,MtrNode * treenode,int * perm,int * invperm)2031 ddCheckPermuation(
2032 DdManager * table,
2033 MtrNode * treenode,
2034 int * perm,
2035 int * invperm)
2036 {
2037 unsigned int i, size;
2038 int index, level, minLevel, maxLevel;
2039
2040 if (treenode == NULL) return(1);
2041
2042 minLevel = table->size;
2043 maxLevel = 0;
2044 /* i : level */
2045 for (i = treenode->low; i < treenode->low + treenode->size; i++) {
2046 index = table->invperm[i];
2047 level = perm[index];
2048 if (level < minLevel)
2049 minLevel = level;
2050 if (level > maxLevel)
2051 maxLevel = level;
2052 }
2053 size = maxLevel - minLevel + 1;
2054 if (size != treenode->size)
2055 return(0);
2056
2057 if (treenode->child != NULL) {
2058 if (!ddCheckPermuation(table, treenode->child, perm, invperm))
2059 return(0);
2060 }
2061 if (treenode->younger != NULL) {
2062 if (!ddCheckPermuation(table, treenode->younger, perm, invperm))
2063 return(0);
2064 }
2065 return(1);
2066 }
2067