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