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