1 /**CFile***********************************************************************
2
3 FileName [cuddWindow.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions for variable reordering by window permutation.]
8
9 Description [Internal procedures included in this module:
10 <ul>
11 <li> cuddWindowReorder()
12 </ul>
13 Static procedures included in this module:
14 <ul>
15 <li> ddWindow2()
16 <li> ddWindowConv2()
17 <li> ddPermuteWindow3()
18 <li> ddWindow3()
19 <li> ddWindowConv3()
20 <li> ddPermuteWindow4()
21 <li> ddWindow4()
22 <li> ddWindowConv4()
23 </ul>]
24
25 Author [Fabio Somenzi]
26
27 Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
28
29 All rights reserved.
30
31 Redistribution and use in source and binary forms, with or without
32 modification, are permitted provided that the following conditions
33 are met:
34
35 Redistributions of source code must retain the above copyright
36 notice, this list of conditions and the following disclaimer.
37
38 Redistributions in binary form must reproduce the above copyright
39 notice, this list of conditions and the following disclaimer in the
40 documentation and/or other materials provided with the distribution.
41
42 Neither the name of the University of Colorado nor the names of its
43 contributors may be used to endorse or promote products derived from
44 this software without specific prior written permission.
45
46 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
47 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
48 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
49 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
50 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
51 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
52 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
53 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
54 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
55 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
56 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
57 POSSIBILITY OF SUCH DAMAGE.]
58
59 ******************************************************************************/
60
61 #include "util.h"
62 #include "cuddInt.h"
63
64 /*---------------------------------------------------------------------------*/
65 /* Constant declarations */
66 /*---------------------------------------------------------------------------*/
67
68
69 /*---------------------------------------------------------------------------*/
70 /* Stucture declarations */
71 /*---------------------------------------------------------------------------*/
72
73
74 /*---------------------------------------------------------------------------*/
75 /* Type declarations */
76 /*---------------------------------------------------------------------------*/
77
78
79 /*---------------------------------------------------------------------------*/
80 /* Variable declarations */
81 /*---------------------------------------------------------------------------*/
82
83 #ifndef lint
84 static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.15 2012/02/05 01:07:19 fabio Exp $";
85 #endif
86
87 #ifdef DD_STATS
88 extern int ddTotalNumberSwapping;
89 extern int ddTotalNISwaps;
90 #endif
91
92 /*---------------------------------------------------------------------------*/
93 /* Macro declarations */
94 /*---------------------------------------------------------------------------*/
95
96
97 /**AutomaticStart*************************************************************/
98
99 /*---------------------------------------------------------------------------*/
100 /* Static function prototypes */
101 /*---------------------------------------------------------------------------*/
102
103 static int ddWindow2 (DdManager *table, int low, int high);
104 static int ddWindowConv2 (DdManager *table, int low, int high);
105 static int ddPermuteWindow3 (DdManager *table, int x);
106 static int ddWindow3 (DdManager *table, int low, int high);
107 static int ddWindowConv3 (DdManager *table, int low, int high);
108 static int ddPermuteWindow4 (DdManager *table, int w);
109 static int ddWindow4 (DdManager *table, int low, int high);
110 static int ddWindowConv4 (DdManager *table, int low, int high);
111
112 /**AutomaticEnd***************************************************************/
113
114
115 /*---------------------------------------------------------------------------*/
116 /* Definition of exported functions */
117 /*---------------------------------------------------------------------------*/
118
119 /*---------------------------------------------------------------------------*/
120 /* Definition of internal functions */
121 /*---------------------------------------------------------------------------*/
122
123
124 /**Function********************************************************************
125
126 Synopsis [Reorders by applying the method of the sliding window.]
127
128 Description [Reorders by applying the method of the sliding window.
129 Tries all possible permutations to the variables in a window that
130 slides from low to high. The size of the window is determined by
131 submethod. Assumes that no dead nodes are present. Returns 1 in
132 case of success; 0 otherwise.]
133
134 SideEffects [None]
135
136 ******************************************************************************/
137 int
cuddWindowReorder(DdManager * table,int low,int high,Cudd_ReorderingType submethod)138 cuddWindowReorder(
139 DdManager * table /* DD table */,
140 int low /* lowest index to reorder */,
141 int high /* highest index to reorder */,
142 Cudd_ReorderingType submethod /* window reordering option */)
143 {
144
145 int res;
146 #ifdef DD_DEBUG
147 int supposedOpt;
148 #endif
149
150 switch (submethod) {
151 case CUDD_REORDER_WINDOW2:
152 res = ddWindow2(table,low,high);
153 break;
154 case CUDD_REORDER_WINDOW3:
155 res = ddWindow3(table,low,high);
156 break;
157 case CUDD_REORDER_WINDOW4:
158 res = ddWindow4(table,low,high);
159 break;
160 case CUDD_REORDER_WINDOW2_CONV:
161 res = ddWindowConv2(table,low,high);
162 break;
163 case CUDD_REORDER_WINDOW3_CONV:
164 res = ddWindowConv3(table,low,high);
165 #ifdef DD_DEBUG
166 supposedOpt = table->keys - table->isolated;
167 res = ddWindow3(table,low,high);
168 if (table->keys - table->isolated != (unsigned) supposedOpt) {
169 (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
170 table->keys - table->isolated, supposedOpt);
171 }
172 #endif
173 break;
174 case CUDD_REORDER_WINDOW4_CONV:
175 res = ddWindowConv4(table,low,high);
176 #ifdef DD_DEBUG
177 supposedOpt = table->keys - table->isolated;
178 res = ddWindow4(table,low,high);
179 if (table->keys - table->isolated != (unsigned) supposedOpt) {
180 (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
181 table->keys - table->isolated, supposedOpt);
182 }
183 #endif
184 break;
185 default: return(0);
186 }
187
188 return(res);
189
190 } /* end of cuddWindowReorder */
191
192
193 /*---------------------------------------------------------------------------*/
194 /* Definition of static functions */
195 /*---------------------------------------------------------------------------*/
196
197 /**Function********************************************************************
198
199 Synopsis [Reorders by applying a sliding window of width 2.]
200
201 Description [Reorders by applying a sliding window of width 2.
202 Tries both permutations of the variables in a window
203 that slides from low to high. Assumes that no dead nodes are
204 present. Returns 1 in case of success; 0 otherwise.]
205
206 SideEffects [None]
207
208 ******************************************************************************/
209 static int
ddWindow2(DdManager * table,int low,int high)210 ddWindow2(
211 DdManager * table,
212 int low,
213 int high)
214 {
215
216 int x;
217 int res;
218 int size;
219
220 #ifdef DD_DEBUG
221 assert(low >= 0 && high < table->size);
222 #endif
223
224 if (high-low < 1) return(0);
225
226 res = table->keys - table->isolated;
227 for (x = low; x < high; x++) {
228 size = res;
229 res = cuddSwapInPlace(table,x,x+1);
230 if (res == 0) return(0);
231 if (res >= size) { /* no improvement: undo permutation */
232 res = cuddSwapInPlace(table,x,x+1);
233 if (res == 0) return(0);
234 }
235 #ifdef DD_STATS
236 if (res < size) {
237 (void) fprintf(table->out,"-");
238 } else {
239 (void) fprintf(table->out,"=");
240 }
241 fflush(table->out);
242 #endif
243 }
244
245 return(1);
246
247 } /* end of ddWindow2 */
248
249
250 /**Function********************************************************************
251
252 Synopsis [Reorders by repeatedly applying a sliding window of width 2.]
253
254 Description [Reorders by repeatedly applying a sliding window of width
255 2. Tries both permutations of the variables in a window
256 that slides from low to high. Assumes that no dead nodes are
257 present. Uses an event-driven approach to determine convergence.
258 Returns 1 in case of success; 0 otherwise.]
259
260 SideEffects [None]
261
262 ******************************************************************************/
263 static int
ddWindowConv2(DdManager * table,int low,int high)264 ddWindowConv2(
265 DdManager * table,
266 int low,
267 int high)
268 {
269 int x;
270 int res;
271 int nwin;
272 int newevent;
273 int *events;
274 int size;
275
276 #ifdef DD_DEBUG
277 assert(low >= 0 && high < table->size);
278 #endif
279
280 if (high-low < 1) return(ddWindowConv2(table,low,high));
281
282 nwin = high-low;
283 events = ALLOC(int,nwin);
284 if (events == NULL) {
285 table->errorCode = CUDD_MEMORY_OUT;
286 return(0);
287 }
288 for (x=0; x<nwin; x++) {
289 events[x] = 1;
290 }
291
292 res = table->keys - table->isolated;
293 do {
294 newevent = 0;
295 for (x=0; x<nwin; x++) {
296 if (events[x]) {
297 size = res;
298 res = cuddSwapInPlace(table,x+low,x+low+1);
299 if (res == 0) {
300 FREE(events);
301 return(0);
302 }
303 if (res >= size) { /* no improvement: undo permutation */
304 res = cuddSwapInPlace(table,x+low,x+low+1);
305 if (res == 0) {
306 FREE(events);
307 return(0);
308 }
309 }
310 if (res < size) {
311 if (x < nwin-1) events[x+1] = 1;
312 if (x > 0) events[x-1] = 1;
313 newevent = 1;
314 }
315 events[x] = 0;
316 #ifdef DD_STATS
317 if (res < size) {
318 (void) fprintf(table->out,"-");
319 } else {
320 (void) fprintf(table->out,"=");
321 }
322 fflush(table->out);
323 #endif
324 }
325 }
326 #ifdef DD_STATS
327 if (newevent) {
328 (void) fprintf(table->out,"|");
329 fflush(table->out);
330 }
331 #endif
332 } while (newevent);
333
334 FREE(events);
335
336 return(1);
337
338 } /* end of ddWindowConv3 */
339
340
341 /**Function********************************************************************
342
343 Synopsis [Tries all the permutations of the three variables between
344 x and x+2 and retains the best.]
345
346 Description [Tries all the permutations of the three variables between
347 x and x+2 and retains the best. Assumes that no dead nodes are
348 present. Returns the index of the best permutation (1-6) in case of
349 success; 0 otherwise.Assumes that no dead nodes are present. Returns
350 the index of the best permutation (1-6) in case of success; 0
351 otherwise.]
352
353 SideEffects [None]
354
355 ******************************************************************************/
356 static int
ddPermuteWindow3(DdManager * table,int x)357 ddPermuteWindow3(
358 DdManager * table,
359 int x)
360 {
361 int y,z;
362 int size,sizeNew;
363 int best;
364
365 #ifdef DD_DEBUG
366 assert(table->dead == 0);
367 assert(x+2 < table->size);
368 #endif
369
370 size = table->keys - table->isolated;
371 y = x+1; z = y+1;
372
373 /* The permutation pattern is:
374 ** (x,y)(y,z)
375 ** repeated three times to get all 3! = 6 permutations.
376 */
377 #define ABC 1
378 best = ABC;
379
380 #define BAC 2
381 sizeNew = cuddSwapInPlace(table,x,y);
382 if (sizeNew < size) {
383 if (sizeNew == 0) return(0);
384 best = BAC;
385 size = sizeNew;
386 }
387 #define BCA 3
388 sizeNew = cuddSwapInPlace(table,y,z);
389 if (sizeNew < size) {
390 if (sizeNew == 0) return(0);
391 best = BCA;
392 size = sizeNew;
393 }
394 #define CBA 4
395 sizeNew = cuddSwapInPlace(table,x,y);
396 if (sizeNew < size) {
397 if (sizeNew == 0) return(0);
398 best = CBA;
399 size = sizeNew;
400 }
401 #define CAB 5
402 sizeNew = cuddSwapInPlace(table,y,z);
403 if (sizeNew < size) {
404 if (sizeNew == 0) return(0);
405 best = CAB;
406 size = sizeNew;
407 }
408 #define ACB 6
409 sizeNew = cuddSwapInPlace(table,x,y);
410 if (sizeNew < size) {
411 if (sizeNew == 0) return(0);
412 best = ACB;
413 size = sizeNew;
414 }
415
416 /* Now take the shortest route to the best permuytation.
417 ** The initial permutation is ACB.
418 */
419 switch(best) {
420 case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
421 case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
422 case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
423 case ACB: break;
424 case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
425 case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
426 break;
427 default: return(0);
428 }
429
430 #ifdef DD_DEBUG
431 assert(table->keys - table->isolated == (unsigned) size);
432 #endif
433
434 return(best);
435
436 } /* end of ddPermuteWindow3 */
437
438
439 /**Function********************************************************************
440
441 Synopsis [Reorders by applying a sliding window of width 3.]
442
443 Description [Reorders by applying a sliding window of width 3.
444 Tries all possible permutations to the variables in a
445 window that slides from low to high. Assumes that no dead nodes are
446 present. Returns 1 in case of success; 0 otherwise.]
447
448 SideEffects [None]
449
450 ******************************************************************************/
451 static int
ddWindow3(DdManager * table,int low,int high)452 ddWindow3(
453 DdManager * table,
454 int low,
455 int high)
456 {
457
458 int x;
459 int res;
460
461 #ifdef DD_DEBUG
462 assert(low >= 0 && high < table->size);
463 #endif
464
465 if (high-low < 2) return(ddWindow2(table,low,high));
466
467 for (x = low; x+1 < high; x++) {
468 res = ddPermuteWindow3(table,x);
469 if (res == 0) return(0);
470 #ifdef DD_STATS
471 if (res == ABC) {
472 (void) fprintf(table->out,"=");
473 } else {
474 (void) fprintf(table->out,"-");
475 }
476 fflush(table->out);
477 #endif
478 }
479
480 return(1);
481
482 } /* end of ddWindow3 */
483
484
485 /**Function********************************************************************
486
487 Synopsis [Reorders by repeatedly applying a sliding window of width 3.]
488
489 Description [Reorders by repeatedly applying a sliding window of width
490 3. Tries all possible permutations to the variables in a
491 window that slides from low to high. Assumes that no dead nodes are
492 present. Uses an event-driven approach to determine convergence.
493 Returns 1 in case of success; 0 otherwise.]
494
495 SideEffects [None]
496
497 ******************************************************************************/
498 static int
ddWindowConv3(DdManager * table,int low,int high)499 ddWindowConv3(
500 DdManager * table,
501 int low,
502 int high)
503 {
504 int x;
505 int res;
506 int nwin;
507 int newevent;
508 int *events;
509
510 #ifdef DD_DEBUG
511 assert(low >= 0 && high < table->size);
512 #endif
513
514 if (high-low < 2) return(ddWindowConv2(table,low,high));
515
516 nwin = high-low-1;
517 events = ALLOC(int,nwin);
518 if (events == NULL) {
519 table->errorCode = CUDD_MEMORY_OUT;
520 return(0);
521 }
522 for (x=0; x<nwin; x++) {
523 events[x] = 1;
524 }
525
526 do {
527 newevent = 0;
528 for (x=0; x<nwin; x++) {
529 if (events[x]) {
530 res = ddPermuteWindow3(table,x+low);
531 switch (res) {
532 case ABC:
533 break;
534 case BAC:
535 if (x < nwin-1) events[x+1] = 1;
536 if (x > 1) events[x-2] = 1;
537 newevent = 1;
538 break;
539 case BCA:
540 case CBA:
541 case CAB:
542 if (x < nwin-2) events[x+2] = 1;
543 if (x < nwin-1) events[x+1] = 1;
544 if (x > 0) events[x-1] = 1;
545 if (x > 1) events[x-2] = 1;
546 newevent = 1;
547 break;
548 case ACB:
549 if (x < nwin-2) events[x+2] = 1;
550 if (x > 0) events[x-1] = 1;
551 newevent = 1;
552 break;
553 default:
554 FREE(events);
555 return(0);
556 }
557 events[x] = 0;
558 #ifdef DD_STATS
559 if (res == ABC) {
560 (void) fprintf(table->out,"=");
561 } else {
562 (void) fprintf(table->out,"-");
563 }
564 fflush(table->out);
565 #endif
566 }
567 }
568 #ifdef DD_STATS
569 if (newevent) {
570 (void) fprintf(table->out,"|");
571 fflush(table->out);
572 }
573 #endif
574 } while (newevent);
575
576 FREE(events);
577
578 return(1);
579
580 } /* end of ddWindowConv3 */
581
582
583 /**Function********************************************************************
584
585 Synopsis [Tries all the permutations of the four variables between w
586 and w+3 and retains the best.]
587
588 Description [Tries all the permutations of the four variables between
589 w and w+3 and retains the best. Assumes that no dead nodes are
590 present. Returns the index of the best permutation (1-24) in case of
591 success; 0 otherwise.]
592
593 SideEffects [None]
594
595 ******************************************************************************/
596 static int
ddPermuteWindow4(DdManager * table,int w)597 ddPermuteWindow4(
598 DdManager * table,
599 int w)
600 {
601 int x,y,z;
602 int size,sizeNew;
603 int best;
604
605 #ifdef DD_DEBUG
606 assert(table->dead == 0);
607 assert(w+3 < table->size);
608 #endif
609
610 size = table->keys - table->isolated;
611 x = w+1; y = x+1; z = y+1;
612
613 /* The permutation pattern is:
614 * (w,x)(y,z)(w,x)(x,y)
615 * (y,z)(w,x)(y,z)(x,y)
616 * repeated three times to get all 4! = 24 permutations.
617 * This gives a hamiltonian circuit of Cayley's graph.
618 * The codes to the permutation are assigned in topological order.
619 * The permutations at lower distance from the final permutation are
620 * assigned lower codes. This way we can choose, between
621 * permutations that give the same size, one that requires the minimum
622 * number of swaps from the final permutation of the hamiltonian circuit.
623 * There is an exception to this rule: ABCD is given Code 1, to
624 * avoid oscillation when convergence is sought.
625 */
626 #define ABCD 1
627 best = ABCD;
628
629 #define BACD 7
630 sizeNew = cuddSwapInPlace(table,w,x);
631 if (sizeNew < size) {
632 if (sizeNew == 0) return(0);
633 best = BACD;
634 size = sizeNew;
635 }
636 #define BADC 13
637 sizeNew = cuddSwapInPlace(table,y,z);
638 if (sizeNew < size) {
639 if (sizeNew == 0) return(0);
640 best = BADC;
641 size = sizeNew;
642 }
643 #define ABDC 8
644 sizeNew = cuddSwapInPlace(table,w,x);
645 if (sizeNew < size || (sizeNew == size && ABDC < best)) {
646 if (sizeNew == 0) return(0);
647 best = ABDC;
648 size = sizeNew;
649 }
650 #define ADBC 14
651 sizeNew = cuddSwapInPlace(table,x,y);
652 if (sizeNew < size) {
653 if (sizeNew == 0) return(0);
654 best = ADBC;
655 size = sizeNew;
656 }
657 #define ADCB 9
658 sizeNew = cuddSwapInPlace(table,y,z);
659 if (sizeNew < size || (sizeNew == size && ADCB < best)) {
660 if (sizeNew == 0) return(0);
661 best = ADCB;
662 size = sizeNew;
663 }
664 #define DACB 15
665 sizeNew = cuddSwapInPlace(table,w,x);
666 if (sizeNew < size) {
667 if (sizeNew == 0) return(0);
668 best = DACB;
669 size = sizeNew;
670 }
671 #define DABC 20
672 sizeNew = cuddSwapInPlace(table,y,z);
673 if (sizeNew < size) {
674 if (sizeNew == 0) return(0);
675 best = DABC;
676 size = sizeNew;
677 }
678 #define DBAC 23
679 sizeNew = cuddSwapInPlace(table,x,y);
680 if (sizeNew < size) {
681 if (sizeNew == 0) return(0);
682 best = DBAC;
683 size = sizeNew;
684 }
685 #define BDAC 19
686 sizeNew = cuddSwapInPlace(table,w,x);
687 if (sizeNew < size || (sizeNew == size && BDAC < best)) {
688 if (sizeNew == 0) return(0);
689 best = BDAC;
690 size = sizeNew;
691 }
692 #define BDCA 21
693 sizeNew = cuddSwapInPlace(table,y,z);
694 if (sizeNew < size || (sizeNew == size && BDCA < best)) {
695 if (sizeNew == 0) return(0);
696 best = BDCA;
697 size = sizeNew;
698 }
699 #define DBCA 24
700 sizeNew = cuddSwapInPlace(table,w,x);
701 if (sizeNew < size) {
702 if (sizeNew == 0) return(0);
703 best = DBCA;
704 size = sizeNew;
705 }
706 #define DCBA 22
707 sizeNew = cuddSwapInPlace(table,x,y);
708 if (sizeNew < size || (sizeNew == size && DCBA < best)) {
709 if (sizeNew == 0) return(0);
710 best = DCBA;
711 size = sizeNew;
712 }
713 #define DCAB 18
714 sizeNew = cuddSwapInPlace(table,y,z);
715 if (sizeNew < size || (sizeNew == size && DCAB < best)) {
716 if (sizeNew == 0) return(0);
717 best = DCAB;
718 size = sizeNew;
719 }
720 #define CDAB 12
721 sizeNew = cuddSwapInPlace(table,w,x);
722 if (sizeNew < size || (sizeNew == size && CDAB < best)) {
723 if (sizeNew == 0) return(0);
724 best = CDAB;
725 size = sizeNew;
726 }
727 #define CDBA 17
728 sizeNew = cuddSwapInPlace(table,y,z);
729 if (sizeNew < size || (sizeNew == size && CDBA < best)) {
730 if (sizeNew == 0) return(0);
731 best = CDBA;
732 size = sizeNew;
733 }
734 #define CBDA 11
735 sizeNew = cuddSwapInPlace(table,x,y);
736 if (sizeNew < size || (sizeNew == size && CBDA < best)) {
737 if (sizeNew == 0) return(0);
738 best = CBDA;
739 size = sizeNew;
740 }
741 #define BCDA 16
742 sizeNew = cuddSwapInPlace(table,w,x);
743 if (sizeNew < size || (sizeNew == size && BCDA < best)) {
744 if (sizeNew == 0) return(0);
745 best = BCDA;
746 size = sizeNew;
747 }
748 #define BCAD 10
749 sizeNew = cuddSwapInPlace(table,y,z);
750 if (sizeNew < size || (sizeNew == size && BCAD < best)) {
751 if (sizeNew == 0) return(0);
752 best = BCAD;
753 size = sizeNew;
754 }
755 #define CBAD 5
756 sizeNew = cuddSwapInPlace(table,w,x);
757 if (sizeNew < size || (sizeNew == size && CBAD < best)) {
758 if (sizeNew == 0) return(0);
759 best = CBAD;
760 size = sizeNew;
761 }
762 #define CABD 3
763 sizeNew = cuddSwapInPlace(table,x,y);
764 if (sizeNew < size || (sizeNew == size && CABD < best)) {
765 if (sizeNew == 0) return(0);
766 best = CABD;
767 size = sizeNew;
768 }
769 #define CADB 6
770 sizeNew = cuddSwapInPlace(table,y,z);
771 if (sizeNew < size || (sizeNew == size && CADB < best)) {
772 if (sizeNew == 0) return(0);
773 best = CADB;
774 size = sizeNew;
775 }
776 #define ACDB 4
777 sizeNew = cuddSwapInPlace(table,w,x);
778 if (sizeNew < size || (sizeNew == size && ACDB < best)) {
779 if (sizeNew == 0) return(0);
780 best = ACDB;
781 size = sizeNew;
782 }
783 #define ACBD 2
784 sizeNew = cuddSwapInPlace(table,y,z);
785 if (sizeNew < size || (sizeNew == size && ACBD < best)) {
786 if (sizeNew == 0) return(0);
787 best = ACBD;
788 size = sizeNew;
789 }
790
791 /* Now take the shortest route to the best permutation.
792 ** The initial permutation is ACBD.
793 */
794 switch(best) {
795 case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
796 case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
797 case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
798 case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
799 case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
800 case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
801 case ACBD: break;
802 case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
803 case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
804 case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
805 if (!cuddSwapInPlace(table,x,y)) return(0);
806 if (!cuddSwapInPlace(table,y,z)) return(0);
807 break;
808 case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
809 case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
810 case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
811 case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
812 case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
813 break;
814 case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
815 case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
816 case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
817 if (!cuddSwapInPlace(table,y,z)) return(0);
818 break;
819 case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
820 case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
821 case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
822 case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
823 break;
824 case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
825 case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
826 if (!cuddSwapInPlace(table,x,y)) return(0);
827 break;
828 default: return(0);
829 }
830
831 #ifdef DD_DEBUG
832 assert(table->keys - table->isolated == (unsigned) size);
833 #endif
834
835 return(best);
836
837 } /* end of ddPermuteWindow4 */
838
839
840 /**Function********************************************************************
841
842 Synopsis [Reorders by applying a sliding window of width 4.]
843
844 Description [Reorders by applying a sliding window of width 4.
845 Tries all possible permutations to the variables in a
846 window that slides from low to high. Assumes that no dead nodes are
847 present. Returns 1 in case of success; 0 otherwise.]
848
849 SideEffects [None]
850
851 ******************************************************************************/
852 static int
ddWindow4(DdManager * table,int low,int high)853 ddWindow4(
854 DdManager * table,
855 int low,
856 int high)
857 {
858
859 int w;
860 int res;
861
862 #ifdef DD_DEBUG
863 assert(low >= 0 && high < table->size);
864 #endif
865
866 if (high-low < 3) return(ddWindow3(table,low,high));
867
868 for (w = low; w+2 < high; w++) {
869 res = ddPermuteWindow4(table,w);
870 if (res == 0) return(0);
871 #ifdef DD_STATS
872 if (res == ABCD) {
873 (void) fprintf(table->out,"=");
874 } else {
875 (void) fprintf(table->out,"-");
876 }
877 fflush(table->out);
878 #endif
879 }
880
881 return(1);
882
883 } /* end of ddWindow4 */
884
885
886 /**Function********************************************************************
887
888 Synopsis [Reorders by repeatedly applying a sliding window of width 4.]
889
890 Description [Reorders by repeatedly applying a sliding window of width
891 4. Tries all possible permutations to the variables in a
892 window that slides from low to high. Assumes that no dead nodes are
893 present. Uses an event-driven approach to determine convergence.
894 Returns 1 in case of success; 0 otherwise.]
895
896 SideEffects [None]
897
898 ******************************************************************************/
899 static int
ddWindowConv4(DdManager * table,int low,int high)900 ddWindowConv4(
901 DdManager * table,
902 int low,
903 int high)
904 {
905 int x;
906 int res;
907 int nwin;
908 int newevent;
909 int *events;
910
911 #ifdef DD_DEBUG
912 assert(low >= 0 && high < table->size);
913 #endif
914
915 if (high-low < 3) return(ddWindowConv3(table,low,high));
916
917 nwin = high-low-2;
918 events = ALLOC(int,nwin);
919 if (events == NULL) {
920 table->errorCode = CUDD_MEMORY_OUT;
921 return(0);
922 }
923 for (x=0; x<nwin; x++) {
924 events[x] = 1;
925 }
926
927 do {
928 newevent = 0;
929 for (x=0; x<nwin; x++) {
930 if (events[x]) {
931 res = ddPermuteWindow4(table,x+low);
932 switch (res) {
933 case ABCD:
934 break;
935 case BACD:
936 if (x < nwin-1) events[x+1] = 1;
937 if (x > 2) events[x-3] = 1;
938 newevent = 1;
939 break;
940 case BADC:
941 if (x < nwin-3) events[x+3] = 1;
942 if (x < nwin-1) events[x+1] = 1;
943 if (x > 0) events[x-1] = 1;
944 if (x > 2) events[x-3] = 1;
945 newevent = 1;
946 break;
947 case ABDC:
948 if (x < nwin-3) events[x+3] = 1;
949 if (x > 0) events[x-1] = 1;
950 newevent = 1;
951 break;
952 case ADBC:
953 case ADCB:
954 case ACDB:
955 if (x < nwin-3) events[x+3] = 1;
956 if (x < nwin-2) events[x+2] = 1;
957 if (x > 0) events[x-1] = 1;
958 if (x > 1) events[x-2] = 1;
959 newevent = 1;
960 break;
961 case DACB:
962 case DABC:
963 case DBAC:
964 case BDAC:
965 case BDCA:
966 case DBCA:
967 case DCBA:
968 case DCAB:
969 case CDAB:
970 case CDBA:
971 case CBDA:
972 case BCDA:
973 case CADB:
974 if (x < nwin-3) events[x+3] = 1;
975 if (x < nwin-2) events[x+2] = 1;
976 if (x < nwin-1) events[x+1] = 1;
977 if (x > 0) events[x-1] = 1;
978 if (x > 1) events[x-2] = 1;
979 if (x > 2) events[x-3] = 1;
980 newevent = 1;
981 break;
982 case BCAD:
983 case CBAD:
984 case CABD:
985 if (x < nwin-2) events[x+2] = 1;
986 if (x < nwin-1) events[x+1] = 1;
987 if (x > 1) events[x-2] = 1;
988 if (x > 2) events[x-3] = 1;
989 newevent = 1;
990 break;
991 case ACBD:
992 if (x < nwin-2) events[x+2] = 1;
993 if (x > 1) events[x-2] = 1;
994 newevent = 1;
995 break;
996 default:
997 FREE(events);
998 return(0);
999 }
1000 events[x] = 0;
1001 #ifdef DD_STATS
1002 if (res == ABCD) {
1003 (void) fprintf(table->out,"=");
1004 } else {
1005 (void) fprintf(table->out,"-");
1006 }
1007 fflush(table->out);
1008 #endif
1009 }
1010 }
1011 #ifdef DD_STATS
1012 if (newevent) {
1013 (void) fprintf(table->out,"|");
1014 fflush(table->out);
1015 }
1016 #endif
1017 } while (newevent);
1018
1019 FREE(events);
1020
1021 return(1);
1022
1023 } /* end of ddWindowConv4 */
1024