1 /**CFile***********************************************************************
3 FileName [cuddReorder.c]
7 Synopsis [Functions for dynamic variable reordering.]
9 Description [External procedures included in this file:
11 <li> Cudd_ReduceHeap()
12 <li> Cudd_ShuffleHeap()
14 Internal procedures included in this module:
16 <li> cuddDynamicAllocNode()
21 <li> cuddSwapInPlace()
22 <li> cuddBddAlignToZdd()
24 Static procedures included in this module:
26 <li> ddUniqueCompare()
31 <li> ddSiftingBackward()
32 <li> ddReorderPreprocess()
33 <li> ddReorderPostprocess()
39 Author [Shipra Panda, Bernard Plessier, Fabio Somenzi]
41 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
45 Redistribution and use in source and binary forms, with or without
46 modification, are permitted provided that the following conditions
49 Redistributions of source code must retain the above copyright
50 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
73 ******************************************************************************/
78 /*---------------------------------------------------------------------------*/
79 /* Constant declarations */
80 /*---------------------------------------------------------------------------*/
82 #define DD_MAX_SUBTABLE_SPARSITY 8
83 #define DD_SHRINK_FACTOR 2
85 /*---------------------------------------------------------------------------*/
86 /* Stucture declarations */
87 /*---------------------------------------------------------------------------*/
89 /*---------------------------------------------------------------------------*/
90 /* Type declarations */
91 /*---------------------------------------------------------------------------*/
93 /*---------------------------------------------------------------------------*/
94 /* Variable declarations */
95 /*---------------------------------------------------------------------------*/
98 static char rcsid
[] DD_UNUSED
= "$Id: cuddReorder.c,v 1.69 2009/02/21 18:24:10 fabio Exp $";
103 int ddTotalNumberSwapping
;
108 /*---------------------------------------------------------------------------*/
109 /* Macro declarations */
110 /*---------------------------------------------------------------------------*/
112 /**AutomaticStart*************************************************************/
114 /*---------------------------------------------------------------------------*/
115 /* Static function prototypes */
116 /*---------------------------------------------------------------------------*/
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
);
132 /**AutomaticEnd***************************************************************/
135 /*---------------------------------------------------------------------------*/
136 /* Definition of exported functions */
137 /*---------------------------------------------------------------------------*/
140 /**Function********************************************************************
142 Synopsis [Main dynamic reordering routine.]
144 Description [Main dynamic reordering routine.
145 Calls one of the possible reordering procedures:
149 <li>Symmetric Sifting
151 <li>Window Permutation
152 <li>Simulated Annealing
153 <li>Genetic Algorithm
154 <li>Dynamic Programming (exact)
157 For sifting, symmetric sifting, group sifting, and window
158 permutation it is possible to request reordering to convergence.<p>
160 The core of all methods is the reordering procedure
161 cuddSwapInPlace() which swaps two adjacent variables and is based
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.]
167 SideEffects [Changes the variable order for all diagrams and clears
170 ******************************************************************************/
173 DdManager
* table
/* DD manager */,
174 Cudd_ReorderingType heuristic
/* method used for reordering */,
175 int minsize
/* bound below which no reordering occurs */)
179 unsigned int nextDyn
;
181 unsigned int initialSize
;
182 unsigned int finalSize
;
186 /* Don't reorder if there are too many dead nodes. */
187 if (table
->keys
- table
->dead
< (unsigned) minsize
)
190 if (heuristic
== CUDD_REORDER_SAME
) {
191 heuristic
= table
->autoMethod
;
193 if (heuristic
== CUDD_REORDER_NONE
) {
197 /* This call to Cudd_ReduceHeap does initiate reordering. Therefore
200 table
->reorderings
++;
202 localTime
= util_cpu_time();
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);
212 if (!ddReorderPreprocess(table
)) return(0);
213 ddTotalNumberSwapping
= 0;
215 if (table
->keys
> table
->peakLiveNodes
) {
216 table
->peakLiveNodes
= table
->keys
;
219 initialSize
= table
->keys
- table
->isolated
;
223 case CUDD_REORDER_RANDOM
:
224 case CUDD_REORDER_RANDOM_PIVOT
:
225 (void) fprintf(table
->out
,"#:I_RANDOM ");
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 ");
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 ");
243 case CUDD_REORDER_ANNEALING
:
244 (void) fprintf(table
->out
,"#:I_ANNEAL ");
246 case CUDD_REORDER_GENETIC
:
247 (void) fprintf(table
->out
,"#:I_GENETIC ");
249 case CUDD_REORDER_LINEAR
:
250 case CUDD_REORDER_LINEAR_CONVERGE
:
251 (void) fprintf(table
->out
,"#:I_LINSIFT ");
253 case CUDD_REORDER_EXACT
:
254 (void) fprintf(table
->out
,"#:I_EXACT ");
259 (void) fprintf(table
->out
,"%8d: initial size",initialSize
);
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
;
269 result
= cuddTreeSifting(table
,heuristic
);
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
);
286 if (!ddReorderPostprocess(table
))
289 if (table
->realign
) {
290 if (!cuddZddAlignToBdd(table
))
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
;
299 table
->nextDyn
+= 20;
300 table
->reordered
= 1;
302 /* Run hook functions. */
303 hook
= table
->postReorderingHook
;
304 while (hook
!= NULL
) {
305 int res
= (hook
->f
)(table
, "BDD", (void *)localTime
);
306 if (res
== 0) return(0);
309 /* Update cumulative reordering time. */
310 table
->reordTime
+= util_cpu_time() - localTime
;
314 } /* end of Cudd_ReduceHeap */
317 /**Function********************************************************************
319 Synopsis [Reorders variables according to given permutation.]
321 Description [Reorders variables according to given permutation.
322 The i-th entry of the permutation array contains the index of the variable
323 that should be brought to the i-th level. The size of the array should be
324 equal or greater to the number of variables currently in use.
325 Returns 1 in case of success; 0 otherwise.]
327 SideEffects [Changes the variable order for all diagrams and clears
330 SeeAlso [Cudd_ReduceHeap]
332 ******************************************************************************/
335 DdManager
* table
/* DD manager */,
336 int * permutation
/* required variable permutation */)
344 /* Don't waste time in case of identity permutation. */
345 for (i
= 0; i
< table
->size
; i
++) {
346 if (permutation
[i
] != table
->invperm
[i
]) {
354 if (!ddReorderPreprocess(table
)) return(0);
355 if (table
->keys
> table
->peakLiveNodes
) {
356 table
->peakLiveNodes
= table
->keys
;
359 perm
= ALLOC(int, table
->size
);
360 for (i
= 0; i
< table
->size
; i
++)
361 perm
[permutation
[i
]] = i
;
362 if (!ddCheckPermuation(table
,table
->tree
,perm
,permutation
)) {
366 if (!ddUpdateMtrTree(table
,table
->tree
,perm
,permutation
)) {
372 result
= ddShuffle(table
,permutation
);
374 if (!ddReorderPostprocess(table
)) return(0);
378 } /* end of Cudd_ShuffleHeap */
381 /*---------------------------------------------------------------------------*/
382 /* Definition of internal functions */
383 /*---------------------------------------------------------------------------*/
386 /**Function********************************************************************
388 Synopsis [Dynamically allocates a Node.]
390 Description [Dynamically allocates a Node. This procedure is similar
391 to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage
392 collection, because during reordering there are no dead nodes.
393 Returns a pointer to a new node if successful; NULL is memory is
398 SeeAlso [cuddAllocNode]
400 ******************************************************************************/
402 cuddDynamicAllocNode(
408 extern DD_OOMFP MMoutOfMemory
;
409 DD_OOMFP saveHandler
;
411 if (table
->nextFree
== NULL
) { /* free list is empty */
412 /* Try to allocate a new block. */
413 saveHandler
= MMoutOfMemory
;
414 MMoutOfMemory
= Cudd_OutOfMem
;
415 mem
= (DdNodePtr
*) ALLOC(DdNode
, DD_MEM_CHUNK
+ 1);
416 MMoutOfMemory
= saveHandler
;
417 if (mem
== NULL
&& table
->stash
!= NULL
) {
420 /* Inhibit resizing of tables. */
421 table
->maxCacheHard
= table
->cacheSlots
- 1;
422 table
->cacheSlack
= - (int) (table
->cacheSlots
+ 1);
423 for (i
= 0; i
< table
->size
; i
++) {
424 table
->subtables
[i
].maxKeys
<<= 2;
426 mem
= (DdNodePtr
*) ALLOC(DdNode
,DD_MEM_CHUNK
+ 1);
429 /* Out of luck. Call the default handler to do
430 ** whatever it specifies for a failed malloc. If this
431 ** handler returns, then set error code, print
432 ** warning, and return. */
433 (*MMoutOfMemory
)(sizeof(DdNode
)*(DD_MEM_CHUNK
+ 1));
434 table
->errorCode
= CUDD_MEMORY_OUT
;
436 (void) fprintf(table
->err
,
437 "cuddDynamicAllocNode: out of memory");
438 (void) fprintf(table
->err
,"Memory in use = %lu\n",
442 } else { /* successful allocation; slice memory */
443 unsigned long offset
;
444 table
->memused
+= (DD_MEM_CHUNK
+ 1) * sizeof(DdNode
);
445 mem
[0] = (DdNode
*) table
->memoryList
;
446 table
->memoryList
= mem
;
448 /* Here we rely on the fact that the size of a DdNode is a
449 ** power of 2 and a multiple of the size of a pointer.
450 ** If we align one node, all the others will be aligned
452 offset
= (unsigned long) mem
& (sizeof(DdNode
) - 1);
453 mem
+= (sizeof(DdNode
) - offset
) / sizeof(DdNodePtr
);
455 assert(((unsigned long) mem
& (sizeof(DdNode
) - 1)) == 0);
457 list
= (DdNode
*) mem
;
462 list
[i
- 1].next
= &list
[i
];
463 } while (++i
< DD_MEM_CHUNK
);
465 list
[DD_MEM_CHUNK
-1].ref
= 0;
466 list
[DD_MEM_CHUNK
- 1].next
= NULL
;
468 table
->nextFree
= &list
[0];
470 } /* if free list empty */
472 node
= table
->nextFree
;
473 table
->nextFree
= node
->next
;
476 } /* end of cuddDynamicAllocNode */
479 /**Function********************************************************************
481 Synopsis [Implementation of Rudell's sifting algorithm.]
483 Description [Implementation of Rudell's sifting algorithm.
484 Assumes that no dead nodes are present.
486 <li> Order all the variables according to the number of entries
487 in each unique table.
488 <li> Sift the variable up and down, remembering each time the
489 total size of the DD heap.
490 <li> Select the best permutation.
491 <li> Repeat 3 and 4 for all variables.
493 Returns 1 if successful; 0 otherwise.]
497 ******************************************************************************/
515 /* Find order in which to sift variables. */
517 entry
= ALLOC(int,size
);
519 table
->errorCode
= CUDD_MEMORY_OUT
;
520 goto cuddSiftingOutOfMem
;
522 var
= ALLOC(int,size
);
524 table
->errorCode
= CUDD_MEMORY_OUT
;
525 goto cuddSiftingOutOfMem
;
528 for (i
= 0; i
< size
; i
++) {
530 entry
[i
] = table
->subtables
[x
].keys
;
534 qsort((void *)var
,size
,sizeof(int),(DD_QSFP
)ddUniqueCompare
);
537 for (i
= 0; i
< ddMin(table
->siftMaxVar
,size
); i
++) {
538 if (ddTotalNumberSwapping
>= table
->siftMaxSwap
)
540 x
= table
->perm
[var
[i
]];
542 if (x
< lower
|| x
> upper
|| table
->subtables
[x
].bindVar
== 1)
545 previousSize
= table
->keys
- table
->isolated
;
547 result
= ddSiftingAux(table
, x
, lower
, upper
);
548 if (!result
) goto cuddSiftingOutOfMem
;
550 if (table
->keys
< (unsigned) previousSize
+ table
->isolated
) {
551 (void) fprintf(table
->out
,"-");
552 } else if (table
->keys
> (unsigned) previousSize
+ table
->isolated
) {
553 (void) fprintf(table
->out
,"+"); /* should never happen */
554 (void) fprintf(table
->err
,"\nSize increased from %d to %d while sifting variable %d\n", previousSize
, table
->keys
- table
->isolated
, var
[i
]);
556 (void) fprintf(table
->out
,"=");
569 if (entry
!= NULL
) FREE(entry
);
570 if (var
!= NULL
) FREE(var
);
574 } /* end of cuddSifting */
577 /**Function********************************************************************
579 Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.]
581 Description [Implementation of Plessier's algorithm that reorders
582 variables by a sequence of (non-adjacent) swaps.
584 <li> Select two variables (RANDOM or HEURISTIC).
585 <li> Permute these variables.
586 <li> If the nodes have decreased accept the permutation.
587 <li> Otherwise reconstruct the original heap.
590 Returns 1 in case of success; 0 otherwise.]
594 ******************************************************************************/
600 Cudd_ReorderingType heuristic
)
615 assert(lower
>= 0 && upper
< table
->size
&& lower
<= upper
);
618 nvars
= upper
- lower
+ 1;
621 for (i
= 0; i
< iterate
; i
++) {
622 if (ddTotalNumberSwapping
>= table
->siftMaxSwap
)
624 if (heuristic
== CUDD_REORDER_RANDOM_PIVOT
) {
626 for (j
= lower
; j
<= upper
; j
++) {
627 if ((keys
= table
->subtables
[j
].keys
) > max
) {
633 modulo
= upper
- pivot
;
637 y
= pivot
+ 1 + ((int) Cudd_Random() % modulo
);
640 modulo
= pivot
- lower
- 1;
645 x
= (int) Cudd_Random() % modulo
;
649 x
= ((int) Cudd_Random() % nvars
) + lower
;
651 y
= ((int) Cudd_Random() % nvars
) + lower
;
654 previousSize
= table
->keys
- table
->isolated
;
655 moves
= ddSwapAny(table
,x
,y
);
656 if (moves
== NULL
) goto cuddSwappingOutOfMem
;
657 result
= ddSiftingBackward(table
,previousSize
,moves
);
658 if (!result
) goto cuddSwappingOutOfMem
;
659 while (moves
!= NULL
) {
661 cuddDeallocMove(table
, moves
);
665 if (table
->keys
< (unsigned) previousSize
+ table
->isolated
) {
666 (void) fprintf(table
->out
,"-");
667 } else if (table
->keys
> (unsigned) previousSize
+ table
->isolated
) {
668 (void) fprintf(table
->out
,"+"); /* should never happen */
670 (void) fprintf(table
->out
,"=");
675 (void) fprintf(table
->out
,"#:t_SWAPPING %8d: tmp size\n",
676 table
->keys
- table
->isolated
);
682 cuddSwappingOutOfMem
:
683 while (moves
!= NULL
) {
685 cuddDeallocMove(table
, moves
);
691 } /* end of cuddSwapping */
694 /**Function********************************************************************
696 Synopsis [Finds the next subtable with a larger index.]
698 Description [Finds the next subtable with a larger index. Returns the
703 SeeAlso [cuddNextLow]
705 ******************************************************************************/
713 } /* end of cuddNextHigh */
716 /**Function********************************************************************
718 Synopsis [Finds the next subtable with a smaller index.]
720 Description [Finds the next subtable with a smaller index. Returns the
725 SeeAlso [cuddNextHigh]
727 ******************************************************************************/
735 } /* end of cuddNextLow */
738 /**Function********************************************************************
740 Synopsis [Swaps two adjacent variables.]
742 Description [Swaps two adjacent variables. It assumes that no dead
743 nodes are present on entry to this procedure. The procedure then
744 guarantees that no dead nodes will be present when it terminates.
745 cuddSwapInPlace assumes that x < y. Returns the number of keys in
746 the table if successful; 0 otherwise.]
750 ******************************************************************************/
757 DdNodePtr
*xlist
, *ylist
;
761 int oldxkeys
, oldykeys
;
762 int newxkeys
, newykeys
;
763 int comple
, newcomplement
;
765 Cudd_VariableType varType
;
766 Cudd_LazyGroupType groupType
;
769 DdNode
*f
,*f0
,*f1
,*f01
,*f00
,*f11
,*f10
,*newf1
,*newf0
;
771 DdNodePtr
*previousP
;
773 DdNode
*sentinel
= &(table
->sentinel
);
774 extern DD_OOMFP MMoutOfMemory
;
775 DD_OOMFP saveHandler
;
783 assert(cuddNextHigh(table
,x
) == y
);
784 assert(table
->subtables
[x
].keys
!= 0);
785 assert(table
->subtables
[y
].keys
!= 0);
786 assert(table
->subtables
[x
].dead
== 0);
787 assert(table
->subtables
[y
].dead
== 0);
790 ddTotalNumberSwapping
++;
792 /* Get parameters of x subtable. */
793 xindex
= table
->invperm
[x
];
794 xlist
= table
->subtables
[x
].nodelist
;
795 oldxkeys
= table
->subtables
[x
].keys
;
796 xslots
= table
->subtables
[x
].slots
;
797 xshift
= table
->subtables
[x
].shift
;
799 /* Get parameters of y subtable. */
800 yindex
= table
->invperm
[y
];
801 ylist
= table
->subtables
[y
].nodelist
;
802 oldykeys
= table
->subtables
[y
].keys
;
803 yslots
= table
->subtables
[y
].slots
;
804 yshift
= table
->subtables
[y
].shift
;
806 if (!cuddTestInteract(table
,xindex
,yindex
)) {
816 /* Check whether the two projection functions involved in this
817 ** swap are isolated. At the end, we'll be able to tell how many
818 ** isolated projection functions are there by checking only these
819 ** two functions again. This is done to eliminate the isolated
820 ** projection functions from the node count.
822 isolated
= - ((table
->vars
[xindex
]->ref
== 1) +
823 (table
->vars
[yindex
]->ref
== 1));
825 /* The nodes in the x layer that do not depend on
826 ** y will stay there; the others are put in a chain.
827 ** The chain is handled as a LIFO; g points to the beginning.
830 if ((oldxkeys
>= xslots
|| (unsigned) xslots
== table
->initSlots
) &&
831 oldxkeys
<= DD_MAX_SUBTABLE_DENSITY
* xslots
) {
832 for (i
= 0; i
< xslots
; i
++) {
833 previousP
= &(xlist
[i
]);
835 while (f
!= sentinel
) {
837 f1
= cuddT(f
); f0
= cuddE(f
);
838 if (f1
->index
!= (DdHalfWord
) yindex
&&
839 Cudd_Regular(f0
)->index
!= (DdHalfWord
) yindex
) {
843 previousP
= &(f
->next
);
850 } /* while there are elements in the collision chain */
851 *previousP
= sentinel
;
852 } /* for each slot of the x subtable */
853 } else { /* resize xlist */
856 unsigned int newxslots
;
858 /* Empty current xlist. Nodes that stay go to list h;
859 ** nodes that move go to list g. */
860 for (i
= 0; i
< xslots
; i
++) {
862 while (f
!= sentinel
) {
864 f1
= cuddT(f
); f0
= cuddE(f
);
865 if (f1
->index
!= (DdHalfWord
) yindex
&&
866 Cudd_Regular(f0
)->index
!= (DdHalfWord
) yindex
) {
877 } /* while there are elements in the collision chain */
878 } /* for each slot of the x subtable */
879 /* Decide size of new subtable. */
882 while ((unsigned) oldxkeys
> DD_MAX_SUBTABLE_DENSITY
* newxslots
) {
886 while ((unsigned) oldxkeys
< newxslots
&&
887 newxslots
> table
->initSlots
) {
891 /* Try to allocate new table. Be ready to back off. */
892 saveHandler
= MMoutOfMemory
;
893 MMoutOfMemory
= Cudd_OutOfMem
;
894 newxlist
= ALLOC(DdNodePtr
, newxslots
);
895 MMoutOfMemory
= saveHandler
;
896 if (newxlist
== NULL
) {
897 (void) fprintf(table
->err
, "Unable to resize subtable %d for lack of memory\n", i
);
902 table
->slots
+= ((int) newxslots
- xslots
);
903 table
->minDead
= (unsigned)
904 (table
->gcFrac
* (double) table
->slots
);
905 table
->cacheSlack
= (int)
906 ddMin(table
->maxCacheHard
, DD_MAX_CACHE_TO_SLOTS_RATIO
907 * table
->slots
) - 2 * (int) table
->cacheSlots
;
909 ((int) newxslots
- xslots
) * sizeof(DdNodePtr
);
915 /* Initialize new subtable. */
916 for (i
= 0; i
< xslots
; i
++) {
919 /* Move nodes that were parked in list h to their new home. */
925 /* Check xlist for pair (f11,f01). */
926 posn
= ddHash(f1
, f0
, xshift
);
927 /* For each element tmp in collision list xlist[posn]. */
928 previousP
= &(xlist
[posn
]);
930 while (f1
< cuddT(tmp
)) {
931 previousP
= &(tmp
->next
);
934 while (f1
== cuddT(tmp
) && f0
< cuddE(tmp
)) {
935 previousP
= &(tmp
->next
);
938 f
->next
= *previousP
;
945 table
->swapSteps
+= oldxkeys
- newxkeys
;
947 /* Take care of the x nodes that must be re-expressed.
948 ** They form a linked list pointed by g. Their index has been
949 ** already changed to yindex.
954 /* Find f1, f0, f11, f10, f01, f00. */
957 assert(!(Cudd_IsComplement(f1
)));
959 if ((int) f1
->index
== yindex
) {
960 f11
= cuddT(f1
); f10
= cuddE(f1
);
965 assert(!(Cudd_IsComplement(f11
)));
968 comple
= Cudd_IsComplement(f0
);
969 f0
= Cudd_Regular(f0
);
970 if ((int) f0
->index
== yindex
) {
971 f01
= cuddT(f0
); f00
= cuddE(f0
);
979 /* Decrease ref count of f1. */
981 /* Create the new T child. */
984 cuddSatInc(newf1
->ref
);
986 /* Check xlist for triple (xindex,f11,f01). */
987 posn
= ddHash(f11
, f01
, xshift
);
988 /* For each element newf1 in collision list xlist[posn]. */
989 previousP
= &(xlist
[posn
]);
991 while (f11
< cuddT(newf1
)) {
992 previousP
= &(newf1
->next
);
995 while (f11
== cuddT(newf1
) && f01
< cuddE(newf1
)) {
996 previousP
= &(newf1
->next
);
999 if (cuddT(newf1
) == f11
&& cuddE(newf1
) == f01
) {
1000 cuddSatInc(newf1
->ref
);
1001 } else { /* no match */
1002 newf1
= cuddDynamicAllocNode(table
);
1004 goto cuddSwapOutOfMem
;
1005 newf1
->index
= xindex
; newf1
->ref
= 1;
1008 /* Insert newf1 in the collision list xlist[posn];
1009 ** increase the ref counts of f11 and f01.
1012 newf1
->next
= *previousP
;
1014 cuddSatInc(f11
->ref
);
1015 tmp
= Cudd_Regular(f01
);
1016 cuddSatInc(tmp
->ref
);
1021 assert(!(Cudd_IsComplement(newf1
)));
1024 /* Do the same for f0, keeping complement dots into account. */
1025 /* Decrease ref count of f0. */
1026 tmp
= Cudd_Regular(f0
);
1027 cuddSatDec(tmp
->ref
);
1028 /* Create the new E child. */
1031 tmp
= Cudd_Regular(newf0
);
1032 cuddSatInc(tmp
->ref
);
1034 /* make sure f10 is regular */
1035 newcomplement
= Cudd_IsComplement(f10
);
1036 if (newcomplement
) {
1037 f10
= Cudd_Not(f10
);
1038 f00
= Cudd_Not(f00
);
1040 /* Check xlist for triple (xindex,f10,f00). */
1041 posn
= ddHash(f10
, f00
, xshift
);
1042 /* For each element newf0 in collision list xlist[posn]. */
1043 previousP
= &(xlist
[posn
]);
1045 while (f10
< cuddT(newf0
)) {
1046 previousP
= &(newf0
->next
);
1049 while (f10
== cuddT(newf0
) && f00
< cuddE(newf0
)) {
1050 previousP
= &(newf0
->next
);
1053 if (cuddT(newf0
) == f10
&& cuddE(newf0
) == f00
) {
1054 cuddSatInc(newf0
->ref
);
1055 } else { /* no match */
1056 newf0
= cuddDynamicAllocNode(table
);
1058 goto cuddSwapOutOfMem
;
1059 newf0
->index
= xindex
; newf0
->ref
= 1;
1062 /* Insert newf0 in the collision list xlist[posn];
1063 ** increase the ref counts of f10 and f00.
1066 newf0
->next
= *previousP
;
1068 cuddSatInc(f10
->ref
);
1069 tmp
= Cudd_Regular(f00
);
1070 cuddSatInc(tmp
->ref
);
1072 if (newcomplement
) {
1073 newf0
= Cudd_Not(newf0
);
1078 /* Insert the modified f in ylist.
1079 ** The modified f does not already exists in ylist.
1080 ** (Because of the uniqueness of the cofactors.)
1082 posn
= ddHash(newf1
, newf0
, yshift
);
1084 previousP
= &(ylist
[posn
]);
1086 while (newf1
< cuddT(tmp
)) {
1087 previousP
= &(tmp
->next
);
1090 while (newf1
== cuddT(tmp
) && newf0
< cuddE(tmp
)) {
1091 previousP
= &(tmp
->next
);
1094 f
->next
= *previousP
;
1097 } /* while f != NULL */
1099 /* GC the y layer. */
1101 /* For each node f in ylist. */
1102 for (i
= 0; i
< yslots
; i
++) {
1103 previousP
= &(ylist
[i
]);
1105 while (f
!= sentinel
) {
1109 cuddSatDec(tmp
->ref
);
1110 tmp
= Cudd_Regular(cuddE(f
));
1111 cuddSatDec(tmp
->ref
);
1112 cuddDeallocNode(table
,f
);
1116 previousP
= &(f
->next
);
1120 *previousP
= sentinel
;
1125 (void) fprintf(table
->out
,"Swapping %d and %d\n",x
,y
);
1129 for (i
= 0; i
< yslots
; i
++) {
1131 while (f
!= sentinel
) {
1133 if (f
->index
!= (DdHalfWord
) yindex
)
1138 if (count
!= newykeys
) {
1139 (void) fprintf(table
->out
,
1140 "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",
1141 oldykeys
,newykeys
,count
);
1144 (void) fprintf(table
->out
,
1145 "Error in id's of ylist\twrong id's = %d\n",
1149 for (i
= 0; i
< xslots
; i
++) {
1151 while (f
!= sentinel
) {
1153 if (f
->index
!= (DdHalfWord
) xindex
)
1158 if (count
!= newxkeys
) {
1159 (void) fprintf(table
->out
,
1160 "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",
1161 oldxkeys
,newxkeys
,count
);
1164 (void) fprintf(table
->out
,
1165 "Error in id's of xlist\twrong id's = %d\n",
1169 isolated
+= (table
->vars
[xindex
]->ref
== 1) +
1170 (table
->vars
[yindex
]->ref
== 1);
1171 table
->isolated
+= isolated
;
1174 /* Set the appropriate fields in table. */
1175 table
->subtables
[x
].nodelist
= ylist
;
1176 table
->subtables
[x
].slots
= yslots
;
1177 table
->subtables
[x
].shift
= yshift
;
1178 table
->subtables
[x
].keys
= newykeys
;
1179 table
->subtables
[x
].maxKeys
= yslots
* DD_MAX_SUBTABLE_DENSITY
;
1180 i
= table
->subtables
[x
].bindVar
;
1181 table
->subtables
[x
].bindVar
= table
->subtables
[y
].bindVar
;
1182 table
->subtables
[y
].bindVar
= i
;
1183 /* Adjust filds for lazy sifting. */
1184 varType
= table
->subtables
[x
].varType
;
1185 table
->subtables
[x
].varType
= table
->subtables
[y
].varType
;
1186 table
->subtables
[y
].varType
= varType
;
1187 i
= table
->subtables
[x
].pairIndex
;
1188 table
->subtables
[x
].pairIndex
= table
->subtables
[y
].pairIndex
;
1189 table
->subtables
[y
].pairIndex
= i
;
1190 i
= table
->subtables
[x
].varHandled
;
1191 table
->subtables
[x
].varHandled
= table
->subtables
[y
].varHandled
;
1192 table
->subtables
[y
].varHandled
= i
;
1193 groupType
= table
->subtables
[x
].varToBeGrouped
;
1194 table
->subtables
[x
].varToBeGrouped
= table
->subtables
[y
].varToBeGrouped
;
1195 table
->subtables
[y
].varToBeGrouped
= groupType
;
1197 table
->subtables
[y
].nodelist
= xlist
;
1198 table
->subtables
[y
].slots
= xslots
;
1199 table
->subtables
[y
].shift
= xshift
;
1200 table
->subtables
[y
].keys
= newxkeys
;
1201 table
->subtables
[y
].maxKeys
= xslots
* DD_MAX_SUBTABLE_DENSITY
;
1203 table
->perm
[xindex
] = y
; table
->perm
[yindex
] = x
;
1204 table
->invperm
[x
] = yindex
; table
->invperm
[y
] = xindex
;
1206 table
->keys
+= newxkeys
+ newykeys
- oldxkeys
- oldykeys
;
1208 return(table
->keys
- table
->isolated
);
1211 (void) fprintf(table
->err
,"Error: cuddSwapInPlace out of memory\n");
1215 } /* end of cuddSwapInPlace */
1218 /**Function********************************************************************
1220 Synopsis [Reorders BDD variables according to the order of the ZDD
1223 Description [Reorders BDD variables according to the order of the
1224 ZDD variables. This function can be called at the end of ZDD
1225 reordering to insure that the order of the BDD variables is
1226 consistent with the order of the ZDD variables. The number of ZDD
1227 variables must be a multiple of the number of BDD variables. Let
1228 <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd
1229 then considers the ZDD variables from <code>M*i</code> to
1230 <code>(M+1)*i-1</code> as corresponding to BDD variable
1231 <code>i</code>. This function should be normally called from
1232 Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of
1233 success; 0 otherwise.]
1235 SideEffects [Changes the BDD variable order for all diagrams and performs
1236 garbage collection of the BDD unique table.]
1238 SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]
1240 ******************************************************************************/
1243 DdManager
* table
/* DD manager */)
1245 int *invperm
; /* permutation array */
1246 int M
; /* ratio of ZDD variables to BDD variables */
1247 int i
; /* loop index */
1248 int result
; /* return value */
1250 /* We assume that a ratio of 0 is OK. */
1251 if (table
->size
== 0)
1254 M
= table
->sizeZ
/ table
->size
;
1255 /* Check whether the number of ZDD variables is a multiple of the
1256 ** number of BDD variables.
1258 if (M
* table
->size
!= table
->sizeZ
)
1260 /* Create and initialize the inverse permutation array. */
1261 invperm
= ALLOC(int,table
->size
);
1262 if (invperm
== NULL
) {
1263 table
->errorCode
= CUDD_MEMORY_OUT
;
1266 for (i
= 0; i
< table
->sizeZ
; i
+= M
) {
1267 int indexZ
= table
->invpermZ
[i
];
1268 int index
= indexZ
/ M
;
1269 invperm
[i
/ M
] = index
;
1271 /* Eliminate dead nodes. Do not scan the cache again, because we
1272 ** assume that Cudd_zddReduceHeap has already cleared it.
1274 cuddGarbageCollect(table
,0);
1276 /* Initialize number of isolated projection functions. */
1277 table
->isolated
= 0;
1278 for (i
= 0; i
< table
->size
; i
++) {
1279 if (table
->vars
[i
]->ref
== 1) table
->isolated
++;
1282 /* Initialize the interaction matrix. */
1283 result
= cuddInitInteract(table
);
1284 if (result
== 0) return(0);
1286 result
= ddShuffle(table
, invperm
);
1288 /* Free interaction matrix. */
1289 FREE(table
->interact
);
1290 /* Fix the BDD variable group tree. */
1291 bddFixTree(table
,table
->tree
);
1294 } /* end of cuddBddAlignToZdd */
1296 /*---------------------------------------------------------------------------*/
1297 /* Definition of static functions */
1298 /*---------------------------------------------------------------------------*/
1301 /**Function********************************************************************
1303 Synopsis [Comparison function used by qsort.]
1305 Description [Comparison function used by qsort to order the
1306 variables according to the number of keys in the subtables.
1307 Returns the difference in number of keys between the two
1308 variables being compared.]
1312 ******************************************************************************/
1319 if (entry
[*ptrY
] == entry
[*ptrX
]) {
1320 return((*ptrX
) - (*ptrY
));
1323 return(entry
[*ptrY
] - entry
[*ptrX
]);
1325 } /* end of ddUniqueCompare */
1328 /**Function********************************************************************
1330 Synopsis [Swaps any two variables.]
1332 Description [Swaps any two variables. Returns the set of moves.]
1336 ******************************************************************************/
1351 tmp
= x
; x
= y
; y
= tmp
;
1356 xNext
= cuddNextHigh(table
,x
);
1357 yNext
= cuddNextLow(table
,y
);
1359 limitSize
= table
->keys
- table
->isolated
;
1362 if ( xNext
== yNext
) {
1363 size
= cuddSwapInPlace(table
,x
,xNext
);
1364 if (size
== 0) goto ddSwapAnyOutOfMem
;
1365 move
= (Move
*) cuddDynamicAllocNode(table
);
1366 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1373 size
= cuddSwapInPlace(table
,yNext
,y
);
1374 if (size
== 0) goto ddSwapAnyOutOfMem
;
1375 move
= (Move
*) cuddDynamicAllocNode(table
);
1376 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1383 size
= cuddSwapInPlace(table
,x
,xNext
);
1384 if (size
== 0) goto ddSwapAnyOutOfMem
;
1385 move
= (Move
*) cuddDynamicAllocNode(table
);
1386 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1393 tmp
= x
; x
= y
; y
= tmp
;
1395 } else if (x
== yNext
) {
1397 size
= cuddSwapInPlace(table
,x
,xNext
);
1398 if (size
== 0) goto ddSwapAnyOutOfMem
;
1399 move
= (Move
*) cuddDynamicAllocNode(table
);
1400 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1407 tmp
= x
; x
= y
; y
= tmp
;
1410 size
= cuddSwapInPlace(table
,x
,xNext
);
1411 if (size
== 0) goto ddSwapAnyOutOfMem
;
1412 move
= (Move
*) cuddDynamicAllocNode(table
);
1413 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1420 size
= cuddSwapInPlace(table
,yNext
,y
);
1421 if (size
== 0) goto ddSwapAnyOutOfMem
;
1422 move
= (Move
*) cuddDynamicAllocNode(table
);
1423 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1434 xNext
= cuddNextHigh(table
,x
);
1435 yNext
= cuddNextLow(table
,y
);
1436 if (xNext
> yRef
) break;
1438 if ((double) size
> table
->maxGrowth
* (double) limitSize
) break;
1439 if (size
< limitSize
) limitSize
= size
;
1442 size
= cuddSwapInPlace(table
,yNext
,y
);
1443 if (size
== 0) goto ddSwapAnyOutOfMem
;
1444 move
= (Move
*) cuddDynamicAllocNode(table
);
1445 if (move
== NULL
) goto ddSwapAnyOutOfMem
;
1456 while (moves
!= NULL
) {
1458 cuddDeallocMove(table
, moves
);
1463 } /* end of ddSwapAny */
1466 /**Function********************************************************************
1468 Synopsis [Given xLow <= x <= xHigh moves x up and down between the
1471 Description [Given xLow <= x <= xHigh moves x up and down between the
1472 boundaries. Finds the best position and does the required changes.
1473 Returns 1 if successful; 0 otherwise.]
1477 ******************************************************************************/
1487 Move
*moveUp
; /* list of up moves */
1488 Move
*moveDown
; /* list of down moves */
1492 initialSize
= table
->keys
- table
->isolated
;
1498 moveDown
= ddSiftingDown(table
,x
,xHigh
);
1499 /* At this point x --> xHigh unless bounding occurred. */
1500 if (moveDown
== (Move
*) CUDD_OUT_OF_MEM
) goto ddSiftingAuxOutOfMem
;
1501 /* Move backward and stop at best position. */
1502 result
= ddSiftingBackward(table
,initialSize
,moveDown
);
1503 if (!result
) goto ddSiftingAuxOutOfMem
;
1505 } else if (x
== xHigh
) {
1506 moveUp
= ddSiftingUp(table
,x
,xLow
);
1507 /* At this point x --> xLow unless bounding occurred. */
1508 if (moveUp
== (Move
*) CUDD_OUT_OF_MEM
) goto ddSiftingAuxOutOfMem
;
1509 /* Move backward and stop at best position. */
1510 result
= ddSiftingBackward(table
,initialSize
,moveUp
);
1511 if (!result
) goto ddSiftingAuxOutOfMem
;
1513 } else if ((x
- xLow
) > (xHigh
- x
)) { /* must go down first: shorter */
1514 moveDown
= ddSiftingDown(table
,x
,xHigh
);
1515 /* At this point x --> xHigh unless bounding occurred. */
1516 if (moveDown
== (Move
*) CUDD_OUT_OF_MEM
) goto ddSiftingAuxOutOfMem
;
1517 if (moveDown
!= NULL
) {
1520 moveUp
= ddSiftingUp(table
,x
,xLow
);
1521 if (moveUp
== (Move
*) CUDD_OUT_OF_MEM
) goto ddSiftingAuxOutOfMem
;
1522 /* Move backward and stop at best position */
1523 result
= ddSiftingBackward(table
,initialSize
,moveUp
);
1524 if (!result
) goto ddSiftingAuxOutOfMem
;
1526 } else { /* must go up first: shorter */
1527 moveUp
= ddSiftingUp(table
,x
,xLow
);
1528 /* At this point x --> xLow unless bounding occurred. */
1529 if (moveUp
== (Move
*) CUDD_OUT_OF_MEM
) goto ddSiftingAuxOutOfMem
;
1530 if (moveUp
!= NULL
) {
1533 moveDown
= ddSiftingDown(table
,x
,xHigh
);
1534 if (moveDown
== (Move
*) CUDD_OUT_OF_MEM
) goto ddSiftingAuxOutOfMem
;
1535 /* Move backward and stop at best position. */
1536 result
= ddSiftingBackward(table
,initialSize
,moveDown
);
1537 if (!result
) goto ddSiftingAuxOutOfMem
;
1540 while (moveDown
!= NULL
) {
1541 move
= moveDown
->next
;
1542 cuddDeallocMove(table
, moveDown
);
1545 while (moveUp
!= NULL
) {
1546 move
= moveUp
->next
;
1547 cuddDeallocMove(table
, moveUp
);
1553 ddSiftingAuxOutOfMem
:
1554 if (moveDown
!= (Move
*) CUDD_OUT_OF_MEM
) {
1555 while (moveDown
!= NULL
) {
1556 move
= moveDown
->next
;
1557 cuddDeallocMove(table
, moveDown
);
1561 if (moveUp
!= (Move
*) CUDD_OUT_OF_MEM
) {
1562 while (moveUp
!= NULL
) {
1563 move
= moveUp
->next
;
1564 cuddDeallocMove(table
, moveUp
);
1571 } /* end of ddSiftingAux */
1574 /**Function********************************************************************
1576 Synopsis [Sifts a variable up.]
1578 Description [Sifts a variable up. Moves y up until either it reaches
1579 the bound (xLow) or the size of the DD heap increases too much.
1580 Returns the set of moves in case of success; NULL if memory is full.]
1584 ******************************************************************************/
1598 int L
; /* lower bound on DD size */
1606 yindex
= table
->invperm
[y
];
1608 /* Initialize the lower bound.
1609 ** The part of the DD below y will not change.
1610 ** The part of the DD above y that does not interact with y will not
1611 ** change. The rest may vanish in the best case, except for
1612 ** the nodes at level xLow, which will not vanish, regardless.
1614 limitSize
= L
= table
->keys
- table
->isolated
;
1615 for (x
= xLow
+ 1; x
< y
; x
++) {
1616 xindex
= table
->invperm
[x
];
1617 if (cuddTestInteract(table
,xindex
,yindex
)) {
1618 isolated
= table
->vars
[xindex
]->ref
== 1;
1619 L
-= table
->subtables
[x
].keys
- isolated
;
1622 isolated
= table
->vars
[yindex
]->ref
== 1;
1623 L
-= table
->subtables
[y
].keys
- isolated
;
1625 x
= cuddNextLow(table
,y
);
1626 while (x
>= xLow
&& L
<= limitSize
) {
1627 xindex
= table
->invperm
[x
];
1629 checkL
= table
->keys
- table
->isolated
;
1630 for (z
= xLow
+ 1; z
< y
; z
++) {
1631 zindex
= table
->invperm
[z
];
1632 if (cuddTestInteract(table
,zindex
,yindex
)) {
1633 isolated
= table
->vars
[zindex
]->ref
== 1;
1634 checkL
-= table
->subtables
[z
].keys
- isolated
;
1637 isolated
= table
->vars
[yindex
]->ref
== 1;
1638 checkL
-= table
->subtables
[y
].keys
- isolated
;
1639 assert(L
== checkL
);
1641 size
= cuddSwapInPlace(table
,x
,y
);
1642 if (size
== 0) goto ddSiftingUpOutOfMem
;
1643 /* Update the lower bound. */
1644 if (cuddTestInteract(table
,xindex
,yindex
)) {
1645 isolated
= table
->vars
[xindex
]->ref
== 1;
1646 L
+= table
->subtables
[y
].keys
- isolated
;
1648 move
= (Move
*) cuddDynamicAllocNode(table
);
1649 if (move
== NULL
) goto ddSiftingUpOutOfMem
;
1655 if ((double) size
> (double) limitSize
* table
->maxGrowth
) break;
1656 if (size
< limitSize
) limitSize
= size
;
1658 x
= cuddNextLow(table
,y
);
1662 ddSiftingUpOutOfMem
:
1663 while (moves
!= NULL
) {
1665 cuddDeallocMove(table
, moves
);
1668 return((Move
*) CUDD_OUT_OF_MEM
);
1670 } /* end of ddSiftingUp */
1673 /**Function********************************************************************
1675 Synopsis [Sifts a variable down.]
1677 Description [Sifts a variable down. Moves x down until either it
1678 reaches the bound (xHigh) or the size of the DD heap increases too
1679 much. Returns the set of moves in case of success; NULL if memory is
1684 ******************************************************************************/
1695 int R
; /* upper bound on node decrease */
1707 xindex
= table
->invperm
[x
];
1708 limitSize
= size
= table
->keys
- table
->isolated
;
1710 for (y
= xHigh
; y
> x
; y
--) {
1711 yindex
= table
->invperm
[y
];
1712 if (cuddTestInteract(table
,xindex
,yindex
)) {
1713 isolated
= table
->vars
[yindex
]->ref
== 1;
1714 R
+= table
->subtables
[y
].keys
- isolated
;
1718 y
= cuddNextHigh(table
,x
);
1719 while (y
<= xHigh
&& size
- R
< limitSize
) {
1722 for (z
= xHigh
; z
> x
; z
--) {
1723 zindex
= table
->invperm
[z
];
1724 if (cuddTestInteract(table
,xindex
,zindex
)) {
1725 isolated
= table
->vars
[zindex
]->ref
== 1;
1726 checkR
+= table
->subtables
[z
].keys
- isolated
;
1729 assert(R
== checkR
);
1731 /* Update upper bound on node decrease. */
1732 yindex
= table
->invperm
[y
];
1733 if (cuddTestInteract(table
,xindex
,yindex
)) {
1734 isolated
= table
->vars
[yindex
]->ref
== 1;
1735 R
-= table
->subtables
[y
].keys
- isolated
;
1737 size
= cuddSwapInPlace(table
,x
,y
);
1738 if (size
== 0) goto ddSiftingDownOutOfMem
;
1739 move
= (Move
*) cuddDynamicAllocNode(table
);
1740 if (move
== NULL
) goto ddSiftingDownOutOfMem
;
1746 if ((double) size
> (double) limitSize
* table
->maxGrowth
) break;
1747 if (size
< limitSize
) limitSize
= size
;
1749 y
= cuddNextHigh(table
,x
);
1753 ddSiftingDownOutOfMem
:
1754 while (moves
!= NULL
) {
1756 cuddDeallocMove(table
, moves
);
1759 return((Move
*) CUDD_OUT_OF_MEM
);
1761 } /* end of ddSiftingDown */
1764 /**Function********************************************************************
1766 Synopsis [Given a set of moves, returns the DD heap to the position
1767 giving the minimum size.]
1769 Description [Given a set of moves, returns the DD heap to the
1770 position giving the minimum size. In case of ties, returns to the
1771 closest position giving the minimum size. Returns 1 in case of
1772 success; 0 otherwise.]
1776 ******************************************************************************/
1786 for (move
= moves
; move
!= NULL
; move
= move
->next
) {
1787 if (move
->size
< size
) {
1792 for (move
= moves
; move
!= NULL
; move
= move
->next
) {
1793 if (move
->size
== size
) return(1);
1794 res
= cuddSwapInPlace(table
,(int)move
->x
,(int)move
->y
);
1795 if (!res
) return(0);
1800 } /* end of ddSiftingBackward */
1803 /**Function********************************************************************
1805 Synopsis [Prepares the DD heap for dynamic reordering.]
1807 Description [Prepares the DD heap for dynamic reordering. Does
1808 garbage collection, to guarantee that there are no dead nodes;
1809 clears the cache, which is invalidated by dynamic reordering; initializes
1810 the number of isolated projection functions; and initializes the
1811 interaction matrix. Returns 1 in case of success; 0 otherwise.]
1815 ******************************************************************************/
1817 ddReorderPreprocess(
1823 /* Clear the cache. */
1824 cuddCacheFlush(table
);
1825 cuddLocalCacheClearAll(table
);
1827 /* Eliminate dead nodes. Do not scan the cache again. */
1828 cuddGarbageCollect(table
,0);
1830 /* Initialize number of isolated projection functions. */
1831 table
->isolated
= 0;
1832 for (i
= 0; i
< table
->size
; i
++) {
1833 if (table
->vars
[i
]->ref
== 1) table
->isolated
++;
1836 /* Initialize the interaction matrix. */
1837 res
= cuddInitInteract(table
);
1838 if (res
== 0) return(0);
1842 } /* end of ddReorderPreprocess */
1845 /**Function********************************************************************
1847 Synopsis [Cleans up at the end of reordering.]
1853 ******************************************************************************/
1855 ddReorderPostprocess(
1860 (void) fflush(table
->out
);
1863 /* Free interaction matrix. */
1864 FREE(table
->interact
);
1868 } /* end of ddReorderPostprocess */
1871 /**Function********************************************************************
1873 Synopsis [Reorders variables according to a given permutation.]
1875 Description [Reorders variables according to a given permutation.
1876 The i-th permutation array contains the index of the variable that
1877 should be brought to the i-th level. ddShuffle assumes that no
1878 dead nodes are present and that the interaction matrix is properly
1879 initialized. The reordering is achieved by a series of upward sifts.
1880 Returns 1 if successful; 0 otherwise.]
1886 ******************************************************************************/
1904 ddTotalNumberSwapping
= 0;
1906 localTime
= util_cpu_time();
1907 initialSize
= table
->keys
- table
->isolated
;
1908 (void) fprintf(table
->out
,"#:I_SHUFFLE %8d: initial size\n",
1913 numvars
= table
->size
;
1915 for (level
= 0; level
< numvars
; level
++) {
1916 index
= permutation
[level
];
1917 position
= table
->perm
[index
];
1919 previousSize
= table
->keys
- table
->isolated
;
1921 result
= ddSiftUp(table
,position
,level
);
1922 if (!result
) return(0);
1924 if (table
->keys
< (unsigned) previousSize
+ table
->isolated
) {
1925 (void) fprintf(table
->out
,"-");
1926 } else if (table
->keys
> (unsigned) previousSize
+ table
->isolated
) {
1927 (void) fprintf(table
->out
,"+"); /* should never happen */
1929 (void) fprintf(table
->out
,"=");
1936 (void) fprintf(table
->out
,"\n");
1937 finalSize
= table
->keys
- table
->isolated
;
1938 (void) fprintf(table
->out
,"#:F_SHUFFLE %8d: final size\n",finalSize
);
1939 (void) fprintf(table
->out
,"#:T_SHUFFLE %8g: total time (sec)\n",
1940 ((double)(util_cpu_time() - localTime
)/1000.0));
1941 (void) fprintf(table
->out
,"#:N_SHUFFLE %8d: total swaps\n",
1942 ddTotalNumberSwapping
);
1943 (void) fprintf(table
->out
,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps
);
1948 } /* end of ddShuffle */
1951 /**Function********************************************************************
1953 Synopsis [Moves one variable up.]
1955 Description [Takes a variable from position x and sifts it up to
1956 position xLow; xLow should be less than or equal to x.
1957 Returns 1 if successful; 0 otherwise]
1963 ******************************************************************************/
1973 y
= cuddNextLow(table
,x
);
1975 size
= cuddSwapInPlace(table
,y
,x
);
1980 y
= cuddNextLow(table
,x
);
1984 } /* end of ddSiftUp */
1987 /**Function********************************************************************
1989 Synopsis [Fixes the BDD variable group tree after a shuffle.]
1991 Description [Fixes the BDD variable group tree after a
1992 shuffle. Assumes that the order of the variables in a terminal node
1993 has not been changed.]
1995 SideEffects [Changes the BDD variable group tree.]
1999 ******************************************************************************/
2005 if (treenode
== NULL
) return;
2006 treenode
->low
= ((int) treenode
->index
< table
->size
) ?
2007 table
->perm
[treenode
->index
] : treenode
->index
;
2008 if (treenode
->child
!= NULL
) {
2009 bddFixTree(table
, treenode
->child
);
2011 if (treenode
->younger
!= NULL
)
2012 bddFixTree(table
, treenode
->younger
);
2013 if (treenode
->parent
!= NULL
&& treenode
->low
< treenode
->parent
->low
) {
2014 treenode
->parent
->low
= treenode
->low
;
2015 treenode
->parent
->index
= treenode
->index
;
2019 } /* end of bddFixTree */
2022 /**Function********************************************************************
2024 Synopsis [Updates the BDD variable group tree before a shuffle.]
2026 Description [Updates the BDD variable group tree before a shuffle.
2027 Returns 1 if successful; 0 otherwise.]
2029 SideEffects [Changes the BDD variable group tree.]
2033 ******************************************************************************/
2041 unsigned int i
, size
;
2042 int index
, level
, minLevel
, maxLevel
, minIndex
;
2044 if (treenode
== NULL
) return(1);
2046 minLevel
= CUDD_MAXINDEX
;
2050 for (i
= treenode
->low
; i
< treenode
->low
+ treenode
->size
; i
++) {
2051 index
= table
->invperm
[i
];
2052 level
= perm
[index
];
2053 if (level
< minLevel
) {
2057 if (level
> maxLevel
)
2060 size
= maxLevel
- minLevel
+ 1;
2061 if (minIndex
== -1) return(0);
2062 if (size
== treenode
->size
) {
2063 treenode
->low
= minLevel
;
2064 treenode
->index
= minIndex
;
2069 if (treenode
->child
!= NULL
) {
2070 if (!ddUpdateMtrTree(table
, treenode
->child
, perm
, invperm
))
2073 if (treenode
->younger
!= NULL
) {
2074 if (!ddUpdateMtrTree(table
, treenode
->younger
, perm
, invperm
))
2081 /**Function********************************************************************
2083 Synopsis [Checks the BDD variable group tree before a shuffle.]
2085 Description [Checks the BDD variable group tree before a shuffle.
2086 Returns 1 if successful; 0 otherwise.]
2088 SideEffects [Changes the BDD variable group tree.]
2092 ******************************************************************************/
2100 unsigned int i
, size
;
2101 int index
, level
, minLevel
, maxLevel
;
2103 if (treenode
== NULL
) return(1);
2105 minLevel
= table
->size
;
2108 for (i
= treenode
->low
; i
< treenode
->low
+ treenode
->size
; i
++) {
2109 index
= table
->invperm
[i
];
2110 level
= perm
[index
];
2111 if (level
< minLevel
)
2113 if (level
> maxLevel
)
2116 size
= maxLevel
- minLevel
+ 1;
2117 if (size
!= treenode
->size
)
2120 if (treenode
->child
!= NULL
) {
2121 if (!ddCheckPermuation(table
, treenode
->child
, perm
, invperm
))
2124 if (treenode
->younger
!= NULL
) {
2125 if (!ddCheckPermuation(table
, treenode
->younger
, perm
, invperm
))