1 /**CFile***********************************************************************
2
3 FileName [cuddZddReord.c]
4
5 PackageName [cudd]
6
7 Synopsis [Procedures for dynamic variable ordering of ZDDs.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_zddReduceHeap()
12 <li> Cudd_zddShuffleHeap()
13 </ul>
14 Internal procedures included in this module:
15 <ul>
16 <li> cuddZddAlignToBdd()
17 <li> cuddZddNextHigh()
18 <li> cuddZddNextLow()
19 <li> cuddZddUniqueCompare()
20 <li> cuddZddSwapInPlace()
21 <li> cuddZddSwapping()
22 <li> cuddZddSifting()
23 </ul>
24 Static procedures included in this module:
25 <ul>
26 <li> zddSwapAny()
27 <li> cuddZddSiftingAux()
28 <li> cuddZddSiftingUp()
29 <li> cuddZddSiftingDown()
30 <li> cuddZddSiftingBackward()
31 <li> zddReorderPreprocess()
32 <li> zddReorderPostprocess()
33 <li> zddShuffle()
34 <li> zddSiftUp()
35 </ul>
36 ]
37
38 SeeAlso []
39
40 Author [Hyong-Kyoon Shin, In-Ho Moon]
41
42 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
43
44 All rights reserved.
45
46 Redistribution and use in source and binary forms, with or without
47 modification, are permitted provided that the following conditions
48 are met:
49
50 Redistributions of source code must retain the above copyright
51 notice, this list of conditions and the following disclaimer.
52
53 Redistributions in binary form must reproduce the above copyright
54 notice, this list of conditions and the following disclaimer in the
55 documentation and/or other materials provided with the distribution.
56
57 Neither the name of the University of Colorado nor the names of its
58 contributors may be used to endorse or promote products derived from
59 this software without specific prior written permission.
60
61 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72 POSSIBILITY OF SUCH DAMAGE.]
73
74 ******************************************************************************/
75
76 #include "misc/util/util_hack.h"
77 #include "cuddInt.h"
78
79 ABC_NAMESPACE_IMPL_START
80
81
82
83 /*---------------------------------------------------------------------------*/
84 /* Constant declarations */
85 /*---------------------------------------------------------------------------*/
86
87 #define DD_MAX_SUBTABLE_SPARSITY 8
88 #define DD_SHRINK_FACTOR 2
89
90 /*---------------------------------------------------------------------------*/
91 /* Stucture declarations */
92 /*---------------------------------------------------------------------------*/
93
94
95 /*---------------------------------------------------------------------------*/
96 /* Type declarations */
97 /*---------------------------------------------------------------------------*/
98
99
100 /*---------------------------------------------------------------------------*/
101 /* Variable declarations */
102 /*---------------------------------------------------------------------------*/
103
104 #ifndef lint
105 static char rcsid[] DD_UNUSED = "$Id: cuddZddReord.c,v 1.47 2004/08/13 18:04:53 fabio Exp $";
106 #endif
107
108 int *zdd_entry;
109
110 int zddTotalNumberSwapping;
111
112 static DdNode *empty;
113
114
115 /*---------------------------------------------------------------------------*/
116 /* Macro declarations */
117 /*---------------------------------------------------------------------------*/
118
119
120 /**AutomaticStart*************************************************************/
121
122 /*---------------------------------------------------------------------------*/
123 /* Static function prototypes */
124 /*---------------------------------------------------------------------------*/
125
126 static Move * zddSwapAny (DdManager *table, int x, int y);
127 static int cuddZddSiftingAux (DdManager *table, int x, int x_low, int x_high);
128 static Move * cuddZddSiftingUp (DdManager *table, int x, int x_low, int initial_size);
129 static Move * cuddZddSiftingDown (DdManager *table, int x, int x_high, int initial_size);
130 static int cuddZddSiftingBackward (DdManager *table, Move *moves, int size);
131 static void zddReorderPreprocess (DdManager *table);
132 static int zddReorderPostprocess (DdManager *table);
133 static int zddShuffle (DdManager *table, int *permutation);
134 static int zddSiftUp (DdManager *table, int x, int xLow);
135 static void zddFixTree (DdManager *table, MtrNode *treenode);
136
137 /**AutomaticEnd***************************************************************/
138
139
140 /*---------------------------------------------------------------------------*/
141 /* Definition of exported functions */
142 /*---------------------------------------------------------------------------*/
143
144
145 /**Function********************************************************************
146
147 Synopsis [Main dynamic reordering routine for ZDDs.]
148
149 Description [Main dynamic reordering routine for ZDDs.
150 Calls one of the possible reordering procedures:
151 <ul>
152 <li>Swapping
153 <li>Sifting
154 <li>Symmetric Sifting
155 </ul>
156
157 For sifting and symmetric sifting it is possible to request reordering
158 to convergence.<p>
159
160 The core of all methods is the reordering procedure
161 cuddZddSwapInPlace() which swaps two adjacent variables.
162 Returns 1 in case of success; 0 otherwise. In the case of symmetric
163 sifting (with and without convergence) returns 1 plus the number of
164 symmetric variables, in case of success.]
165
166 SideEffects [Changes the variable order for all ZDDs and clears
167 the cache.]
168
169 ******************************************************************************/
170 int
Cudd_zddReduceHeap(DdManager * table,Cudd_ReorderingType heuristic,int minsize)171 Cudd_zddReduceHeap(
172 DdManager * table /* DD manager */,
173 Cudd_ReorderingType heuristic /* method used for reordering */,
174 int minsize /* bound below which no reordering occurs */)
175 {
176 DdHook *hook;
177 int result;
178 unsigned int nextDyn;
179 #ifdef DD_STATS
180 unsigned int initialSize;
181 unsigned int finalSize;
182 #endif
183 long localTime;
184
185 /* Don't reorder if there are too many dead nodes. */
186 if (table->keysZ - table->deadZ < (unsigned) minsize)
187 return(1);
188
189 if (heuristic == CUDD_REORDER_SAME) {
190 heuristic = table->autoMethodZ;
191 }
192 if (heuristic == CUDD_REORDER_NONE) {
193 return(1);
194 }
195
196 /* This call to Cudd_zddReduceHeap does initiate reordering. Therefore
197 ** we count it.
198 */
199 table->reorderings++;
200 empty = table->zero;
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, "ZDD", (void *)heuristic);
208 if (res == 0) return(0);
209 hook = hook->next;
210 }
211
212 /* Clear the cache and collect garbage. */
213 zddReorderPreprocess(table);
214 zddTotalNumberSwapping = 0;
215
216 #ifdef DD_STATS
217 initialSize = table->keysZ;
218
219 switch(heuristic) {
220 case CUDD_REORDER_RANDOM:
221 case CUDD_REORDER_RANDOM_PIVOT:
222 (void) fprintf(table->out,"#:I_RANDOM ");
223 break;
224 case CUDD_REORDER_SIFT:
225 case CUDD_REORDER_SIFT_CONVERGE:
226 case CUDD_REORDER_SYMM_SIFT:
227 case CUDD_REORDER_SYMM_SIFT_CONV:
228 (void) fprintf(table->out,"#:I_SIFTING ");
229 break;
230 case CUDD_REORDER_LINEAR:
231 case CUDD_REORDER_LINEAR_CONVERGE:
232 (void) fprintf(table->out,"#:I_LINSIFT ");
233 break;
234 default:
235 (void) fprintf(table->err,"Unsupported ZDD reordering method\n");
236 return(0);
237 }
238 (void) fprintf(table->out,"%8d: initial size",initialSize);
239 #endif
240
241 result = cuddZddTreeSifting(table,heuristic);
242
243 #ifdef DD_STATS
244 (void) fprintf(table->out,"\n");
245 finalSize = table->keysZ;
246 (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize);
247 (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n",
248 ((double)(util_cpu_time() - localTime)/1000.0));
249 (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n",
250 zddTotalNumberSwapping);
251 #endif
252
253 if (result == 0)
254 return(0);
255
256 if (!zddReorderPostprocess(table))
257 return(0);
258
259 if (table->realignZ) {
260 if (!cuddBddAlignToZdd(table))
261 return(0);
262 }
263
264 nextDyn = table->keysZ * DD_DYN_RATIO;
265 if (table->reorderings < 20 || nextDyn > table->nextDyn)
266 table->nextDyn = nextDyn;
267 else
268 table->nextDyn += 20;
269
270 table->reordered = 1;
271
272 /* Run hook functions. */
273 hook = table->postReorderingHook;
274 while (hook != NULL) {
275 int res = (hook->f)(table, "ZDD", (void *)localTime);
276 if (res == 0) return(0);
277 hook = hook->next;
278 }
279 /* Update cumulative reordering time. */
280 table->reordTime += util_cpu_time() - localTime;
281
282 return(result);
283
284 } /* end of Cudd_zddReduceHeap */
285
286
287 /**Function********************************************************************
288
289 Synopsis [Reorders ZDD variables according to given permutation.]
290
291 Description [Reorders ZDD variables according to given permutation.
292 The i-th entry of the permutation array contains the index of the variable
293 that should be brought to the i-th level. The size of the array should be
294 equal or greater to the number of variables currently in use.
295 Returns 1 in case of success; 0 otherwise.]
296
297 SideEffects [Changes the ZDD variable order for all diagrams and clears
298 the cache.]
299
300 SeeAlso [Cudd_zddReduceHeap]
301
302 ******************************************************************************/
303 int
Cudd_zddShuffleHeap(DdManager * table,int * permutation)304 Cudd_zddShuffleHeap(
305 DdManager * table /* DD manager */,
306 int * permutation /* required variable permutation */)
307 {
308
309 int result;
310
311 empty = table->zero;
312 zddReorderPreprocess(table);
313
314 result = zddShuffle(table,permutation);
315
316 if (!zddReorderPostprocess(table)) return(0);
317
318 return(result);
319
320 } /* end of Cudd_zddShuffleHeap */
321
322
323 /*---------------------------------------------------------------------------*/
324 /* Definition of internal functions */
325 /*---------------------------------------------------------------------------*/
326
327
328 /**Function********************************************************************
329
330 Synopsis [Reorders ZDD variables according to the order of the BDD
331 variables.]
332
333 Description [Reorders ZDD variables according to the order of the
334 BDD variables. This function can be called at the end of BDD
335 reordering to insure that the order of the ZDD variables is
336 consistent with the order of the BDD variables. The number of ZDD
337 variables must be a multiple of the number of BDD variables. Let
338 <code>M</code> be the ratio of the two numbers. cuddZddAlignToBdd
339 then considers the ZDD variables from <code>M*i</code> to
340 <code>(M+1)*i-1</code> as corresponding to BDD variable
341 <code>i</code>. This function should be normally called from
342 Cudd_ReduceHeap, which clears the cache. Returns 1 in case of
343 success; 0 otherwise.]
344
345 SideEffects [Changes the ZDD variable order for all diagrams and performs
346 garbage collection of the ZDD unique table.]
347
348 SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap]
349
350 ******************************************************************************/
351 int
cuddZddAlignToBdd(DdManager * table)352 cuddZddAlignToBdd(
353 DdManager * table /* DD manager */)
354 {
355 int *invpermZ; /* permutation array */
356 int M; /* ratio of ZDD variables to BDD variables */
357 int i,j; /* loop indices */
358 int result; /* return value */
359
360 /* We assume that a ratio of 0 is OK. */
361 if (table->sizeZ == 0)
362 return(1);
363
364 empty = table->zero;
365 M = table->sizeZ / table->size;
366 /* Check whether the number of ZDD variables is a multiple of the
367 ** number of BDD variables.
368 */
369 if (M * table->size != table->sizeZ)
370 return(0);
371 /* Create and initialize the inverse permutation array. */
372 invpermZ = ABC_ALLOC(int,table->sizeZ);
373 if (invpermZ == NULL) {
374 table->errorCode = CUDD_MEMORY_OUT;
375 return(0);
376 }
377 for (i = 0; i < table->size; i++) {
378 int index = table->invperm[i];
379 int indexZ = index * M;
380 int levelZ = table->permZ[indexZ];
381 levelZ = (levelZ / M) * M;
382 for (j = 0; j < M; j++) {
383 invpermZ[M * i + j] = table->invpermZ[levelZ + j];
384 }
385 }
386 /* Eliminate dead nodes. Do not scan the cache again, because we
387 ** assume that Cudd_ReduceHeap has already cleared it.
388 */
389 cuddGarbageCollect(table,0);
390
391 result = zddShuffle(table, invpermZ);
392 ABC_FREE(invpermZ);
393 /* Fix the ZDD variable group tree. */
394 zddFixTree(table,table->treeZ);
395 return(result);
396
397 } /* end of cuddZddAlignToBdd */
398
399
400 /**Function********************************************************************
401
402 Synopsis [Finds the next subtable with a larger index.]
403
404 Description [Finds the next subtable with a larger index. Returns the
405 index.]
406
407 SideEffects [None]
408
409 SeeAlso []
410
411 ******************************************************************************/
412 int
cuddZddNextHigh(DdManager * table,int x)413 cuddZddNextHigh(
414 DdManager * table,
415 int x)
416 {
417 return(x + 1);
418
419 } /* end of cuddZddNextHigh */
420
421
422 /**Function********************************************************************
423
424 Synopsis [Finds the next subtable with a smaller index.]
425
426 Description [Finds the next subtable with a smaller index. Returns the
427 index.]
428
429 SideEffects [None]
430
431 SeeAlso []
432
433 ******************************************************************************/
434 int
cuddZddNextLow(DdManager * table,int x)435 cuddZddNextLow(
436 DdManager * table,
437 int x)
438 {
439 return(x - 1);
440
441 } /* end of cuddZddNextLow */
442
443
444 /**Function********************************************************************
445
446 Synopsis [Comparison function used by qsort.]
447
448 Description [Comparison function used by qsort to order the
449 variables according to the number of keys in the subtables.
450 Returns the difference in number of keys between the two
451 variables being compared.]
452
453 SideEffects [None]
454
455 SeeAlso []
456
457 ******************************************************************************/
458 int
cuddZddUniqueCompare(int * ptr_x,int * ptr_y)459 cuddZddUniqueCompare(
460 int * ptr_x,
461 int * ptr_y)
462 {
463 return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]);
464
465 } /* end of cuddZddUniqueCompare */
466
467
468 /**Function********************************************************************
469
470 Synopsis [Swaps two adjacent variables.]
471
472 Description [Swaps two adjacent variables. It assumes that no dead
473 nodes are present on entry to this procedure. The procedure then
474 guarantees that no dead nodes will be present when it terminates.
475 cuddZddSwapInPlace assumes that x < y. Returns the number of keys in
476 the table if successful; 0 otherwise.]
477
478 SideEffects [None]
479
480 SeeAlso []
481
482 ******************************************************************************/
483 int
cuddZddSwapInPlace(DdManager * table,int x,int y)484 cuddZddSwapInPlace(
485 DdManager * table,
486 int x,
487 int y)
488 {
489 DdNodePtr *xlist, *ylist;
490 int xindex, yindex;
491 int xslots, yslots;
492 int xshift, yshift;
493 int oldxkeys, oldykeys;
494 int newxkeys, newykeys;
495 int i;
496 int posn;
497 DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00;
498 DdNode *newf1=NULL, *newf0, *next;
499 DdNodePtr g, *lastP, *previousP;
500
501 #ifdef DD_DEBUG
502 assert(x < y);
503 assert(cuddZddNextHigh(table,x) == y);
504 assert(table->subtableZ[x].keys != 0);
505 assert(table->subtableZ[y].keys != 0);
506 assert(table->subtableZ[x].dead == 0);
507 assert(table->subtableZ[y].dead == 0);
508 #endif
509
510 zddTotalNumberSwapping++;
511
512 /* Get parameters of x subtable. */
513 xindex = table->invpermZ[x];
514 xlist = table->subtableZ[x].nodelist;
515 oldxkeys = table->subtableZ[x].keys;
516 xslots = table->subtableZ[x].slots;
517 xshift = table->subtableZ[x].shift;
518 newxkeys = 0;
519
520 yindex = table->invpermZ[y];
521 ylist = table->subtableZ[y].nodelist;
522 oldykeys = table->subtableZ[y].keys;
523 yslots = table->subtableZ[y].slots;
524 yshift = table->subtableZ[y].shift;
525 newykeys = oldykeys;
526
527 /* The nodes in the x layer that don't depend on y directly
528 ** will stay there; the others are put in a chain.
529 ** The chain is handled as a FIFO; g points to the beginning and
530 ** last points to the end.
531 */
532
533 g = NULL;
534 lastP = &g;
535 for (i = 0; i < xslots; i++) {
536 previousP = &(xlist[i]);
537 f = *previousP;
538 while (f != NULL) {
539 next = f->next;
540 f1 = cuddT(f); f0 = cuddE(f);
541 if ((f1->index != (DdHalfWord) yindex) &&
542 (f0->index != (DdHalfWord) yindex)) { /* stays */
543 newxkeys++;
544 *previousP = f;
545 previousP = &(f->next);
546 } else {
547 f->index = yindex;
548 *lastP = f;
549 lastP = &(f->next);
550 }
551 f = next;
552 } /* while there are elements in the collision chain */
553 *previousP = NULL;
554 } /* for each slot of the x subtable */
555 *lastP = NULL;
556
557
558 #ifdef DD_COUNT
559 table->swapSteps += oldxkeys - newxkeys;
560 #endif
561 /* Take care of the x nodes that must be re-expressed.
562 ** They form a linked list pointed by g. Their index has been
563 ** changed to yindex already.
564 */
565 f = g;
566 while (f != NULL) {
567 next = f->next;
568 /* Find f1, f0, f11, f10, f01, f00. */
569 f1 = cuddT(f);
570 if ((int) f1->index == yindex) {
571 f11 = cuddT(f1); f10 = cuddE(f1);
572 } else {
573 f11 = empty; f10 = f1;
574 }
575 f0 = cuddE(f);
576 if ((int) f0->index == yindex) {
577 f01 = cuddT(f0); f00 = cuddE(f0);
578 } else {
579 f01 = empty; f00 = f0;
580 }
581
582 /* Decrease ref count of f1. */
583 cuddSatDec(f1->ref);
584 /* Create the new T child. */
585 if (f11 == empty) {
586 if (f01 != empty) {
587 newf1 = f01;
588 cuddSatInc(newf1->ref);
589 }
590 /* else case was already handled when finding nodes
591 ** with both children below level y
592 */
593 } else {
594 /* Check xlist for triple (xindex, f11, f01). */
595 posn = ddHash(cuddF2L(f11), cuddF2L(f01), xshift);
596 /* For each element newf1 in collision list xlist[posn]. */
597 newf1 = xlist[posn];
598 while (newf1 != NULL) {
599 if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
600 cuddSatInc(newf1->ref);
601 break; /* match */
602 }
603 newf1 = newf1->next;
604 } /* while newf1 */
605 if (newf1 == NULL) { /* no match */
606 newf1 = cuddDynamicAllocNode(table);
607 if (newf1 == NULL)
608 goto zddSwapOutOfMem;
609 newf1->index = xindex; newf1->ref = 1;
610 cuddT(newf1) = f11;
611 cuddE(newf1) = f01;
612 /* Insert newf1 in the collision list xlist[pos];
613 ** increase the ref counts of f11 and f01
614 */
615 newxkeys++;
616 newf1->next = xlist[posn];
617 xlist[posn] = newf1;
618 cuddSatInc(f11->ref);
619 cuddSatInc(f01->ref);
620 }
621 }
622 cuddT(f) = newf1;
623
624 /* Do the same for f0. */
625 /* Decrease ref count of f0. */
626 cuddSatDec(f0->ref);
627 /* Create the new E child. */
628 if (f10 == empty) {
629 newf0 = f00;
630 cuddSatInc(newf0->ref);
631 } else {
632 /* Check xlist for triple (xindex, f10, f00). */
633 posn = ddHash(cuddF2L(f10), cuddF2L(f00), xshift);
634 /* For each element newf0 in collision list xlist[posn]. */
635 newf0 = xlist[posn];
636 while (newf0 != NULL) {
637 if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
638 cuddSatInc(newf0->ref);
639 break; /* match */
640 }
641 newf0 = newf0->next;
642 } /* while newf0 */
643 if (newf0 == NULL) { /* no match */
644 newf0 = cuddDynamicAllocNode(table);
645 if (newf0 == NULL)
646 goto zddSwapOutOfMem;
647 newf0->index = xindex; newf0->ref = 1;
648 cuddT(newf0) = f10; cuddE(newf0) = f00;
649 /* Insert newf0 in the collision list xlist[posn];
650 ** increase the ref counts of f10 and f00.
651 */
652 newxkeys++;
653 newf0->next = xlist[posn];
654 xlist[posn] = newf0;
655 cuddSatInc(f10->ref);
656 cuddSatInc(f00->ref);
657 }
658 }
659 cuddE(f) = newf0;
660
661 /* Insert the modified f in ylist.
662 ** The modified f does not already exists in ylist.
663 ** (Because of the uniqueness of the cofactors.)
664 */
665 posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), yshift);
666 newykeys++;
667 f->next = ylist[posn];
668 ylist[posn] = f;
669 f = next;
670 } /* while f != NULL */
671
672 /* GC the y layer. */
673
674 /* For each node f in ylist. */
675 for (i = 0; i < yslots; i++) {
676 previousP = &(ylist[i]);
677 f = *previousP;
678 while (f != NULL) {
679 next = f->next;
680 if (f->ref == 0) {
681 cuddSatDec(cuddT(f)->ref);
682 cuddSatDec(cuddE(f)->ref);
683 cuddDeallocNode(table, f);
684 newykeys--;
685 } else {
686 *previousP = f;
687 previousP = &(f->next);
688 }
689 f = next;
690 } /* while f */
691 *previousP = NULL;
692 } /* for i */
693
694 /* Set the appropriate fields in table. */
695 table->subtableZ[x].nodelist = ylist;
696 table->subtableZ[x].slots = yslots;
697 table->subtableZ[x].shift = yshift;
698 table->subtableZ[x].keys = newykeys;
699 table->subtableZ[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY;
700
701 table->subtableZ[y].nodelist = xlist;
702 table->subtableZ[y].slots = xslots;
703 table->subtableZ[y].shift = xshift;
704 table->subtableZ[y].keys = newxkeys;
705 table->subtableZ[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY;
706
707 table->permZ[xindex] = y; table->permZ[yindex] = x;
708 table->invpermZ[x] = yindex; table->invpermZ[y] = xindex;
709
710 table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
711
712 /* Update univ section; univ[x] remains the same. */
713 table->univ[y] = cuddT(table->univ[x]);
714
715 return (table->keysZ);
716
717 zddSwapOutOfMem:
718 (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
719
720 return (0);
721
722 } /* end of cuddZddSwapInPlace */
723
724
725 /**Function********************************************************************
726
727 Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.]
728
729 Description [Implementation of Plessier's algorithm that reorders
730 variables by a sequence of (non-adjacent) swaps.
731 <ol>
732 <li> Select two variables (RANDOM or HEURISTIC).
733 <li> Permute these variables.
734 <li> If the nodes have decreased accept the permutation.
735 <li> Otherwise reconstruct the original heap.
736 <li> Loop.
737 </ol>
738 Returns 1 in case of success; 0 otherwise.]
739
740 SideEffects [None]
741
742 SeeAlso []
743
744 ******************************************************************************/
745 int
cuddZddSwapping(DdManager * table,int lower,int upper,Cudd_ReorderingType heuristic)746 cuddZddSwapping(
747 DdManager * table,
748 int lower,
749 int upper,
750 Cudd_ReorderingType heuristic)
751 {
752 int i, j;
753 int max, keys;
754 int nvars;
755 int x, y;
756 int iterate;
757 int previousSize;
758 Move *moves, *move;
759 int pivot = -1;
760 int modulo;
761 int result;
762
763 #ifdef DD_DEBUG
764 /* Sanity check */
765 assert(lower >= 0 && upper < table->sizeZ && lower <= upper);
766 #endif
767
768 nvars = upper - lower + 1;
769 iterate = nvars;
770
771 for (i = 0; i < iterate; i++) {
772 if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
773 /* Find pivot <= id with maximum keys. */
774 for (max = -1, j = lower; j <= upper; j++) {
775 if ((keys = table->subtableZ[j].keys) > max) {
776 max = keys;
777 pivot = j;
778 }
779 }
780
781 modulo = upper - pivot;
782 if (modulo == 0) {
783 y = pivot; /* y = nvars-1 */
784 } else {
785 /* y = random # from {pivot+1 .. nvars-1} */
786 y = pivot + 1 + (int) (Cudd_Random() % modulo);
787 }
788
789 modulo = pivot - lower - 1;
790 if (modulo < 1) { /* if pivot = 1 or 0 */
791 x = lower;
792 } else {
793 do { /* x = random # from {0 .. pivot-2} */
794 x = (int) Cudd_Random() % modulo;
795 } while (x == y);
796 /* Is this condition really needed, since x and y
797 are in regions separated by pivot? */
798 }
799 } else {
800 x = (int) (Cudd_Random() % nvars) + lower;
801 do {
802 y = (int) (Cudd_Random() % nvars) + lower;
803 } while (x == y);
804 }
805
806 previousSize = table->keysZ;
807 moves = zddSwapAny(table, x, y);
808 if (moves == NULL)
809 goto cuddZddSwappingOutOfMem;
810
811 result = cuddZddSiftingBackward(table, moves, previousSize);
812 if (!result)
813 goto cuddZddSwappingOutOfMem;
814
815 while (moves != NULL) {
816 move = moves->next;
817 cuddDeallocMove(table, moves);
818 moves = move;
819 }
820 #ifdef DD_STATS
821 if (table->keysZ < (unsigned) previousSize) {
822 (void) fprintf(table->out,"-");
823 } else if (table->keysZ > (unsigned) previousSize) {
824 (void) fprintf(table->out,"+"); /* should never happen */
825 } else {
826 (void) fprintf(table->out,"=");
827 }
828 fflush(table->out);
829 #endif
830 }
831
832 return(1);
833
834 cuddZddSwappingOutOfMem:
835 while (moves != NULL) {
836 move = moves->next;
837 cuddDeallocMove(table, moves);
838 moves = move;
839 }
840 return(0);
841
842 } /* end of cuddZddSwapping */
843
844
845 /**Function********************************************************************
846
847 Synopsis [Implementation of Rudell's sifting algorithm.]
848
849 Description [Implementation of Rudell's sifting algorithm.
850 Assumes that no dead nodes are present.
851 <ol>
852 <li> Order all the variables according to the number of entries
853 in each unique table.
854 <li> Sift the variable up and down, remembering each time the
855 total size of the DD heap.
856 <li> Select the best permutation.
857 <li> Repeat 3 and 4 for all variables.
858 </ol>
859 Returns 1 if successful; 0 otherwise.]
860
861 SideEffects [None]
862
863 SeeAlso []
864
865 ******************************************************************************/
866 int
cuddZddSifting(DdManager * table,int lower,int upper)867 cuddZddSifting(
868 DdManager * table,
869 int lower,
870 int upper)
871 {
872 int i;
873 int *var;
874 int size;
875 int x;
876 int result;
877 #ifdef DD_STATS
878 int previousSize;
879 #endif
880
881 size = table->sizeZ;
882
883 /* Find order in which to sift variables. */
884 var = NULL;
885 zdd_entry = ABC_ALLOC(int, size);
886 if (zdd_entry == NULL) {
887 table->errorCode = CUDD_MEMORY_OUT;
888 goto cuddZddSiftingOutOfMem;
889 }
890 var = ABC_ALLOC(int, size);
891 if (var == NULL) {
892 table->errorCode = CUDD_MEMORY_OUT;
893 goto cuddZddSiftingOutOfMem;
894 }
895
896 for (i = 0; i < size; i++) {
897 x = table->permZ[i];
898 zdd_entry[i] = table->subtableZ[x].keys;
899 var[i] = i;
900 }
901
902 qsort((void *)var, (size_t)size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
903
904 /* Now sift. */
905 for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
906 if (zddTotalNumberSwapping >= table->siftMaxSwap)
907 break;
908 x = table->permZ[var[i]];
909 if (x < lower || x > upper) continue;
910 #ifdef DD_STATS
911 previousSize = table->keysZ;
912 #endif
913 result = cuddZddSiftingAux(table, x, lower, upper);
914 if (!result)
915 goto cuddZddSiftingOutOfMem;
916 #ifdef DD_STATS
917 if (table->keysZ < (unsigned) previousSize) {
918 (void) fprintf(table->out,"-");
919 } else if (table->keysZ > (unsigned) previousSize) {
920 (void) fprintf(table->out,"+"); /* should never happen */
921 (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
922 } else {
923 (void) fprintf(table->out,"=");
924 }
925 fflush(table->out);
926 #endif
927 }
928
929 ABC_FREE(var);
930 ABC_FREE(zdd_entry);
931
932 return(1);
933
934 cuddZddSiftingOutOfMem:
935
936 if (zdd_entry != NULL) ABC_FREE(zdd_entry);
937 if (var != NULL) ABC_FREE(var);
938
939 return(0);
940
941 } /* end of cuddZddSifting */
942
943
944 /*---------------------------------------------------------------------------*/
945 /* Definition of static functions */
946 /*---------------------------------------------------------------------------*/
947
948
949 /**Function********************************************************************
950
951 Synopsis [Swaps any two variables.]
952
953 Description [Swaps any two variables. Returns the set of moves.]
954
955 SideEffects [None]
956
957 SeeAlso []
958
959 ******************************************************************************/
960 static Move *
zddSwapAny(DdManager * table,int x,int y)961 zddSwapAny(
962 DdManager * table,
963 int x,
964 int y)
965 {
966 Move *move, *moves;
967 int tmp, size;
968 int x_ref, y_ref;
969 int x_next, y_next;
970 int limit_size;
971
972 if (x > y) { /* make x precede y */
973 tmp = x; x = y; y = tmp;
974 }
975
976 x_ref = x; y_ref = y;
977
978 x_next = cuddZddNextHigh(table, x);
979 y_next = cuddZddNextLow(table, y);
980 moves = NULL;
981 limit_size = table->keysZ;
982
983 for (;;) {
984 if (x_next == y_next) { /* x < x_next = y_next < y */
985 size = cuddZddSwapInPlace(table, x, x_next);
986 if (size == 0)
987 goto zddSwapAnyOutOfMem;
988 move = (Move *) cuddDynamicAllocNode(table);
989 if (move == NULL)
990 goto zddSwapAnyOutOfMem;
991 move->x = x;
992 move->y = x_next;
993 move->size = size;
994 move->next = moves;
995 moves = move;
996
997 size = cuddZddSwapInPlace(table, y_next, y);
998 if (size == 0)
999 goto zddSwapAnyOutOfMem;
1000 move = (Move *)cuddDynamicAllocNode(table);
1001 if (move == NULL)
1002 goto zddSwapAnyOutOfMem;
1003 move->x = y_next;
1004 move->y = y;
1005 move->size = size;
1006 move->next = moves;
1007 moves = move;
1008
1009 size = cuddZddSwapInPlace(table, x, x_next);
1010 if (size == 0)
1011 goto zddSwapAnyOutOfMem;
1012 move = (Move *)cuddDynamicAllocNode(table);
1013 if (move == NULL)
1014 goto zddSwapAnyOutOfMem;
1015 move->x = x;
1016 move->y = x_next;
1017 move->size = size;
1018 move->next = moves;
1019 moves = move;
1020
1021 tmp = x; x = y; y = tmp;
1022
1023 } else if (x == y_next) { /* x = y_next < y = x_next */
1024 size = cuddZddSwapInPlace(table, x, x_next);
1025 if (size == 0)
1026 goto zddSwapAnyOutOfMem;
1027 move = (Move *)cuddDynamicAllocNode(table);
1028 if (move == NULL)
1029 goto zddSwapAnyOutOfMem;
1030 move->x = x;
1031 move->y = x_next;
1032 move->size = size;
1033 move->next = moves;
1034 moves = move;
1035
1036 tmp = x; x = y; y = tmp;
1037 } else {
1038 size = cuddZddSwapInPlace(table, x, x_next);
1039 if (size == 0)
1040 goto zddSwapAnyOutOfMem;
1041 move = (Move *)cuddDynamicAllocNode(table);
1042 if (move == NULL)
1043 goto zddSwapAnyOutOfMem;
1044 move->x = x;
1045 move->y = x_next;
1046 move->size = size;
1047 move->next = moves;
1048 moves = move;
1049
1050 size = cuddZddSwapInPlace(table, y_next, y);
1051 if (size == 0)
1052 goto zddSwapAnyOutOfMem;
1053 move = (Move *)cuddDynamicAllocNode(table);
1054 if (move == NULL)
1055 goto zddSwapAnyOutOfMem;
1056 move->x = y_next;
1057 move->y = y;
1058 move->size = size;
1059 move->next = moves;
1060 moves = move;
1061
1062 x = x_next; y = y_next;
1063 }
1064
1065 x_next = cuddZddNextHigh(table, x);
1066 y_next = cuddZddNextLow(table, y);
1067 if (x_next > y_ref)
1068 break; /* if x == y_ref */
1069
1070 if ((double) size > table->maxGrowth * (double) limit_size)
1071 break;
1072 if (size < limit_size)
1073 limit_size = size;
1074 }
1075 if (y_next >= x_ref) {
1076 size = cuddZddSwapInPlace(table, y_next, y);
1077 if (size == 0)
1078 goto zddSwapAnyOutOfMem;
1079 move = (Move *)cuddDynamicAllocNode(table);
1080 if (move == NULL)
1081 goto zddSwapAnyOutOfMem;
1082 move->x = y_next;
1083 move->y = y;
1084 move->size = size;
1085 move->next = moves;
1086 moves = move;
1087 }
1088
1089 return(moves);
1090
1091 zddSwapAnyOutOfMem:
1092 while (moves != NULL) {
1093 move = moves->next;
1094 cuddDeallocMove(table, moves);
1095 moves = move;
1096 }
1097 return(NULL);
1098
1099 } /* end of zddSwapAny */
1100
1101
1102 /**Function********************************************************************
1103
1104 Synopsis [Given xLow <= x <= xHigh moves x up and down between the
1105 boundaries.]
1106
1107 Description [Given xLow <= x <= xHigh moves x up and down between the
1108 boundaries. Finds the best position and does the required changes.
1109 Returns 1 if successful; 0 otherwise.]
1110
1111 SideEffects [None]
1112
1113 SeeAlso []
1114
1115 ******************************************************************************/
1116 static int
cuddZddSiftingAux(DdManager * table,int x,int x_low,int x_high)1117 cuddZddSiftingAux(
1118 DdManager * table,
1119 int x,
1120 int x_low,
1121 int x_high)
1122 {
1123 Move *move;
1124 Move *moveUp; /* list of up move */
1125 Move *moveDown; /* list of down move */
1126
1127 int initial_size;
1128 int result;
1129
1130 initial_size = table->keysZ;
1131
1132 #ifdef DD_DEBUG
1133 assert(table->subtableZ[x].keys > 0);
1134 #endif
1135
1136 moveDown = NULL;
1137 moveUp = NULL;
1138
1139 if (x == x_low) {
1140 moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
1141 /* after that point x --> x_high */
1142 if (moveDown == NULL)
1143 goto cuddZddSiftingAuxOutOfMem;
1144 result = cuddZddSiftingBackward(table, moveDown,
1145 initial_size);
1146 /* move backward and stop at best position */
1147 if (!result)
1148 goto cuddZddSiftingAuxOutOfMem;
1149
1150 }
1151 else if (x == x_high) {
1152 moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
1153 /* after that point x --> x_low */
1154 if (moveUp == NULL)
1155 goto cuddZddSiftingAuxOutOfMem;
1156 result = cuddZddSiftingBackward(table, moveUp, initial_size);
1157 /* move backward and stop at best position */
1158 if (!result)
1159 goto cuddZddSiftingAuxOutOfMem;
1160 }
1161 else if ((x - x_low) > (x_high - x)) {
1162 /* must go down first:shorter */
1163 moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
1164 /* after that point x --> x_high */
1165 if (moveDown == NULL)
1166 goto cuddZddSiftingAuxOutOfMem;
1167 moveUp = cuddZddSiftingUp(table, moveDown->y, x_low,
1168 initial_size);
1169 if (moveUp == NULL)
1170 goto cuddZddSiftingAuxOutOfMem;
1171 result = cuddZddSiftingBackward(table, moveUp, initial_size);
1172 /* move backward and stop at best position */
1173 if (!result)
1174 goto cuddZddSiftingAuxOutOfMem;
1175 }
1176 else {
1177 moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
1178 /* after that point x --> x_high */
1179 if (moveUp == NULL)
1180 goto cuddZddSiftingAuxOutOfMem;
1181 moveDown = cuddZddSiftingDown(table, moveUp->x, x_high,
1182 initial_size);
1183 /* then move up */
1184 if (moveDown == NULL)
1185 goto cuddZddSiftingAuxOutOfMem;
1186 result = cuddZddSiftingBackward(table, moveDown,
1187 initial_size);
1188 /* move backward and stop at best position */
1189 if (!result)
1190 goto cuddZddSiftingAuxOutOfMem;
1191 }
1192
1193 while (moveDown != NULL) {
1194 move = moveDown->next;
1195 cuddDeallocMove(table, moveDown);
1196 moveDown = move;
1197 }
1198 while (moveUp != NULL) {
1199 move = moveUp->next;
1200 cuddDeallocMove(table, moveUp);
1201 moveUp = move;
1202 }
1203
1204 return(1);
1205
1206 cuddZddSiftingAuxOutOfMem:
1207 while (moveDown != NULL) {
1208 move = moveDown->next;
1209 cuddDeallocMove(table, moveDown);
1210 moveDown = move;
1211 }
1212 while (moveUp != NULL) {
1213 move = moveUp->next;
1214 cuddDeallocMove(table, moveUp);
1215 moveUp = move;
1216 }
1217
1218 return(0);
1219
1220 } /* end of cuddZddSiftingAux */
1221
1222
1223 /**Function********************************************************************
1224
1225 Synopsis [Sifts a variable up.]
1226
1227 Description [Sifts a variable up. Moves y up until either it reaches
1228 the bound (x_low) or the size of the ZDD heap increases too much.
1229 Returns the set of moves in case of success; NULL if memory is full.]
1230
1231 SideEffects [None]
1232
1233 SeeAlso []
1234
1235 ******************************************************************************/
1236 static Move *
cuddZddSiftingUp(DdManager * table,int x,int x_low,int initial_size)1237 cuddZddSiftingUp(
1238 DdManager * table,
1239 int x,
1240 int x_low,
1241 int initial_size)
1242 {
1243 Move *moves;
1244 Move *move;
1245 int y;
1246 int size;
1247 int limit_size = initial_size;
1248
1249 moves = NULL;
1250 y = cuddZddNextLow(table, x);
1251 while (y >= x_low) {
1252 size = cuddZddSwapInPlace(table, y, x);
1253 if (size == 0)
1254 goto cuddZddSiftingUpOutOfMem;
1255 move = (Move *)cuddDynamicAllocNode(table);
1256 if (move == NULL)
1257 goto cuddZddSiftingUpOutOfMem;
1258 move->x = y;
1259 move->y = x;
1260 move->size = size;
1261 move->next = moves;
1262 moves = move;
1263
1264 if ((double)size > (double)limit_size * table->maxGrowth)
1265 break;
1266 if (size < limit_size)
1267 limit_size = size;
1268
1269 x = y;
1270 y = cuddZddNextLow(table, x);
1271 }
1272 return(moves);
1273
1274 cuddZddSiftingUpOutOfMem:
1275 while (moves != NULL) {
1276 move = moves->next;
1277 cuddDeallocMove(table, moves);
1278 moves = move;
1279 }
1280 return(NULL);
1281
1282 } /* end of cuddZddSiftingUp */
1283
1284
1285 /**Function********************************************************************
1286
1287 Synopsis [Sifts a variable down.]
1288
1289 Description [Sifts a variable down. Moves x down until either it
1290 reaches the bound (x_high) or the size of the ZDD heap increases too
1291 much. Returns the set of moves in case of success; NULL if memory is
1292 full.]
1293
1294 SideEffects [None]
1295
1296 SeeAlso []
1297
1298 ******************************************************************************/
1299 static Move *
cuddZddSiftingDown(DdManager * table,int x,int x_high,int initial_size)1300 cuddZddSiftingDown(
1301 DdManager * table,
1302 int x,
1303 int x_high,
1304 int initial_size)
1305 {
1306 Move *moves;
1307 Move *move;
1308 int y;
1309 int size;
1310 int limit_size = initial_size;
1311
1312 moves = NULL;
1313 y = cuddZddNextHigh(table, x);
1314 while (y <= x_high) {
1315 size = cuddZddSwapInPlace(table, x, y);
1316 if (size == 0)
1317 goto cuddZddSiftingDownOutOfMem;
1318 move = (Move *)cuddDynamicAllocNode(table);
1319 if (move == NULL)
1320 goto cuddZddSiftingDownOutOfMem;
1321 move->x = x;
1322 move->y = y;
1323 move->size = size;
1324 move->next = moves;
1325 moves = move;
1326
1327 if ((double)size > (double)limit_size * table->maxGrowth)
1328 break;
1329 if (size < limit_size)
1330 limit_size = size;
1331
1332 x = y;
1333 y = cuddZddNextHigh(table, x);
1334 }
1335 return(moves);
1336
1337 cuddZddSiftingDownOutOfMem:
1338 while (moves != NULL) {
1339 move = moves->next;
1340 cuddDeallocMove(table, moves);
1341 moves = move;
1342 }
1343 return(NULL);
1344
1345 } /* end of cuddZddSiftingDown */
1346
1347
1348 /**Function********************************************************************
1349
1350 Synopsis [Given a set of moves, returns the ZDD heap to the position
1351 giving the minimum size.]
1352
1353 Description [Given a set of moves, returns the ZDD heap to the
1354 position giving the minimum size. In case of ties, returns to the
1355 closest position giving the minimum size. Returns 1 in case of
1356 success; 0 otherwise.]
1357
1358 SideEffects [None]
1359
1360 SeeAlso []
1361
1362 ******************************************************************************/
1363 static int
cuddZddSiftingBackward(DdManager * table,Move * moves,int size)1364 cuddZddSiftingBackward(
1365 DdManager * table,
1366 Move * moves,
1367 int size)
1368 {
1369 int i;
1370 int i_best;
1371 Move *move;
1372 int res;
1373
1374 /* Find the minimum size among moves. */
1375 i_best = -1;
1376 for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1377 if (move->size < size) {
1378 i_best = i;
1379 size = move->size;
1380 }
1381 }
1382
1383 for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1384 if (i == i_best)
1385 break;
1386 res = cuddZddSwapInPlace(table, move->x, move->y);
1387 if (!res)
1388 return(0);
1389 if (i_best == -1 && res == size)
1390 break;
1391 }
1392
1393 return(1);
1394
1395 } /* end of cuddZddSiftingBackward */
1396
1397
1398 /**Function********************************************************************
1399
1400 Synopsis [Prepares the ZDD heap for dynamic reordering.]
1401
1402 Description [Prepares the ZDD heap for dynamic reordering. Does
1403 garbage collection, to guarantee that there are no dead nodes;
1404 and clears the cache, which is invalidated by dynamic reordering.]
1405
1406 SideEffects [None]
1407
1408 ******************************************************************************/
1409 static void
zddReorderPreprocess(DdManager * table)1410 zddReorderPreprocess(
1411 DdManager * table)
1412 {
1413
1414 /* Clear the cache. */
1415 cuddCacheFlush(table);
1416
1417 /* Eliminate dead nodes. Do not scan the cache again. */
1418 cuddGarbageCollect(table,0);
1419
1420 return;
1421
1422 } /* end of ddReorderPreprocess */
1423
1424
1425 /**Function********************************************************************
1426
1427 Synopsis [Shrinks almost empty ZDD subtables at the end of reordering
1428 to guarantee that they have a reasonable load factor.]
1429
1430 Description [Shrinks almost empty subtables at the end of reordering to
1431 guarantee that they have a reasonable load factor. However, if there many
1432 nodes are being reclaimed, then no resizing occurs. Returns 1 in case of
1433 success; 0 otherwise.]
1434
1435 SideEffects [None]
1436
1437 ******************************************************************************/
1438 static int
zddReorderPostprocess(DdManager * table)1439 zddReorderPostprocess(
1440 DdManager * table)
1441 {
1442 int i, j, posn;
1443 DdNodePtr *nodelist, *oldnodelist;
1444 DdNode *node, *next;
1445 unsigned int slots, oldslots;
1446 extern DD_OOMFP MMoutOfMemory;
1447 DD_OOMFP saveHandler;
1448
1449 #ifdef DD_VERBOSE
1450 (void) fflush(table->out);
1451 #endif
1452
1453 /* If we have very many reclaimed nodes, we do not want to shrink
1454 ** the subtables, because this will lead to more garbage
1455 ** collections. More garbage collections mean shorter mean life for
1456 ** nodes with zero reference count; hence lower probability of finding
1457 ** a result in the cache.
1458 */
1459 if (table->reclaimed > table->allocated / 2) return(1);
1460
1461 /* Resize subtables. */
1462 for (i = 0; i < table->sizeZ; i++) {
1463 int shift;
1464 oldslots = table->subtableZ[i].slots;
1465 if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY ||
1466 oldslots <= table->initSlots) continue;
1467 oldnodelist = table->subtableZ[i].nodelist;
1468 slots = oldslots >> 1;
1469 saveHandler = MMoutOfMemory;
1470 MMoutOfMemory = Cudd_OutOfMem;
1471 nodelist = ABC_ALLOC(DdNodePtr, slots);
1472 MMoutOfMemory = saveHandler;
1473 if (nodelist == NULL) {
1474 return(1);
1475 }
1476 table->subtableZ[i].nodelist = nodelist;
1477 table->subtableZ[i].slots = slots;
1478 table->subtableZ[i].shift++;
1479 table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1480 #ifdef DD_VERBOSE
1481 (void) fprintf(table->err,
1482 "shrunk layer %d (%d keys) from %d to %d slots\n",
1483 i, table->subtableZ[i].keys, oldslots, slots);
1484 #endif
1485
1486 for (j = 0; (unsigned) j < slots; j++) {
1487 nodelist[j] = NULL;
1488 }
1489 shift = table->subtableZ[i].shift;
1490 for (j = 0; (unsigned) j < oldslots; j++) {
1491 node = oldnodelist[j];
1492 while (node != NULL) {
1493 next = node->next;
1494 posn = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
1495 node->next = nodelist[posn];
1496 nodelist[posn] = node;
1497 node = next;
1498 }
1499 }
1500 ABC_FREE(oldnodelist);
1501
1502 table->memused += (slots - oldslots) * sizeof(DdNode *);
1503 table->slots += slots - oldslots;
1504 table->minDead = (unsigned) (table->gcFrac * (double) table->slots);
1505 table->cacheSlack = (int) ddMin(table->maxCacheHard,
1506 DD_MAX_CACHE_TO_SLOTS_RATIO*table->slots) -
1507 2 * (int) table->cacheSlots;
1508 }
1509 /* We don't look at the constant subtable, because it is not
1510 ** affected by reordering.
1511 */
1512
1513 return(1);
1514
1515 } /* end of zddReorderPostprocess */
1516
1517
1518 /**Function********************************************************************
1519
1520 Synopsis [Reorders ZDD variables according to a given permutation.]
1521
1522 Description [Reorders ZDD variables according to a given permutation.
1523 The i-th permutation array contains the index of the variable that
1524 should be brought to the i-th level. zddShuffle assumes that no
1525 dead nodes are present. The reordering is achieved by a series of
1526 upward sifts. Returns 1 if successful; 0 otherwise.]
1527
1528 SideEffects [None]
1529
1530 SeeAlso []
1531
1532 ******************************************************************************/
1533 static int
zddShuffle(DdManager * table,int * permutation)1534 zddShuffle(
1535 DdManager * table,
1536 int * permutation)
1537 {
1538 int index;
1539 int level;
1540 int position;
1541 int numvars;
1542 int result;
1543 #ifdef DD_STATS
1544 long localTime;
1545 int initialSize;
1546 int finalSize;
1547 int previousSize;
1548 #endif
1549
1550 zddTotalNumberSwapping = 0;
1551 #ifdef DD_STATS
1552 localTime = util_cpu_time();
1553 initialSize = table->keysZ;
1554 (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
1555 initialSize);
1556 #endif
1557
1558 numvars = table->sizeZ;
1559
1560 for (level = 0; level < numvars; level++) {
1561 index = permutation[level];
1562 position = table->permZ[index];
1563 #ifdef DD_STATS
1564 previousSize = table->keysZ;
1565 #endif
1566 result = zddSiftUp(table,position,level);
1567 if (!result) return(0);
1568 #ifdef DD_STATS
1569 if (table->keysZ < (unsigned) previousSize) {
1570 (void) fprintf(table->out,"-");
1571 } else if (table->keysZ > (unsigned) previousSize) {
1572 (void) fprintf(table->out,"+"); /* should never happen */
1573 } else {
1574 (void) fprintf(table->out,"=");
1575 }
1576 fflush(table->out);
1577 #endif
1578 }
1579
1580 #ifdef DD_STATS
1581 (void) fprintf(table->out,"\n");
1582 finalSize = table->keysZ;
1583 (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize);
1584 (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
1585 ((double)(util_cpu_time() - localTime)/1000.0));
1586 (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
1587 zddTotalNumberSwapping);
1588 #endif
1589
1590 return(1);
1591
1592 } /* end of zddShuffle */
1593
1594
1595 /**Function********************************************************************
1596
1597 Synopsis [Moves one ZDD variable up.]
1598
1599 Description [Takes a ZDD variable from position x and sifts it up to
1600 position xLow; xLow should be less than or equal to x.
1601 Returns 1 if successful; 0 otherwise]
1602
1603 SideEffects [None]
1604
1605 SeeAlso []
1606
1607 ******************************************************************************/
1608 static int
zddSiftUp(DdManager * table,int x,int xLow)1609 zddSiftUp(
1610 DdManager * table,
1611 int x,
1612 int xLow)
1613 {
1614 int y;
1615 int size;
1616
1617 y = cuddZddNextLow(table,x);
1618 while (y >= xLow) {
1619 size = cuddZddSwapInPlace(table,y,x);
1620 if (size == 0) {
1621 return(0);
1622 }
1623 x = y;
1624 y = cuddZddNextLow(table,x);
1625 }
1626 return(1);
1627
1628 } /* end of zddSiftUp */
1629
1630
1631 /**Function********************************************************************
1632
1633 Synopsis [Fixes the ZDD variable group tree after a shuffle.]
1634
1635 Description [Fixes the ZDD variable group tree after a
1636 shuffle. Assumes that the order of the variables in a terminal node
1637 has not been changed.]
1638
1639 SideEffects [Changes the ZDD variable group tree.]
1640
1641 SeeAlso []
1642
1643 ******************************************************************************/
1644 static void
zddFixTree(DdManager * table,MtrNode * treenode)1645 zddFixTree(
1646 DdManager * table,
1647 MtrNode * treenode)
1648 {
1649 if (treenode == NULL) return;
1650 treenode->low = ((int) treenode->index < table->sizeZ) ?
1651 table->permZ[treenode->index] : treenode->index;
1652 if (treenode->child != NULL) {
1653 zddFixTree(table, treenode->child);
1654 }
1655 if (treenode->younger != NULL)
1656 zddFixTree(table, treenode->younger);
1657 if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
1658 treenode->parent->low = treenode->low;
1659 treenode->parent->index = treenode->index;
1660 }
1661 return;
1662
1663 } /* end of zddFixTree */
1664
1665
1666 ABC_NAMESPACE_IMPL_END
1667
1668
1669