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