#include "util_hack.h"
#include "cuddInt.h"
Go to the source code of this file.
Defines | |
#define | ABC 1 |
#define | BAC 2 |
#define | BCA 3 |
#define | CBA 4 |
#define | CAB 5 |
#define | ACB 6 |
#define | ABCD 1 |
#define | BACD 7 |
#define | BADC 13 |
#define | ABDC 8 |
#define | ADBC 14 |
#define | ADCB 9 |
#define | DACB 15 |
#define | DABC 20 |
#define | DBAC 23 |
#define | BDAC 19 |
#define | BDCA 21 |
#define | DBCA 24 |
#define | DCBA 22 |
#define | DCAB 18 |
#define | CDAB 12 |
#define | CDBA 17 |
#define | CBDA 11 |
#define | BCDA 16 |
#define | BCAD 10 |
#define | CBAD 5 |
#define | CABD 3 |
#define | CADB 6 |
#define | ACDB 4 |
#define | ACBD 2 |
Functions | |
static int ddWindow2 | ARGS ((DdManager *table, int low, int high)) |
static int ddPermuteWindow3 | ARGS ((DdManager *table, int x)) |
static int ddPermuteWindow4 | ARGS ((DdManager *table, int w)) |
int | cuddWindowReorder (DdManager *table, int low, int high, Cudd_ReorderingType submethod) |
static int | ddWindow2 (DdManager *table, int low, int high) |
static int | ddWindowConv2 (DdManager *table, int low, int high) |
static int | ddPermuteWindow3 (DdManager *table, int x) |
static int | ddWindow3 (DdManager *table, int low, int high) |
static int | ddWindowConv3 (DdManager *table, int low, int high) |
static int | ddPermuteWindow4 (DdManager *table, int w) |
static int | ddWindow4 (DdManager *table, int low, int high) |
static int | ddWindowConv4 (DdManager *table, int low, int high) |
Variables | |
static char rcsid[] | DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $" |
#define ABC 1 |
#define ABCD 1 |
#define ABDC 8 |
#define ACB 6 |
#define ACBD 2 |
#define ACDB 4 |
#define ADBC 14 |
#define ADCB 9 |
#define BAC 2 |
#define BACD 7 |
#define BADC 13 |
#define BCA 3 |
#define BCAD 10 |
#define BCDA 16 |
#define BDAC 19 |
#define BDCA 21 |
#define CAB 5 |
#define CABD 3 |
#define CADB 6 |
#define CBA 4 |
#define CBAD 5 |
#define CBDA 11 |
#define CDAB 12 |
#define CDBA 17 |
#define DABC 20 |
#define DACB 15 |
#define DBAC 23 |
#define DBCA 24 |
#define DCAB 18 |
#define DCBA 22 |
static int ddPermuteWindow4 ARGS | ( | (DdManager *table, int w) | ) | [static] |
static int ddPermuteWindow3 ARGS | ( | (DdManager *table, int x) | ) | [static] |
static int ddWindowConv4 ARGS | ( | (DdManager *table, int low, int high) | ) | [static] |
AutomaticStart
int cuddWindowReorder | ( | DdManager * | table, | |
int | low, | |||
int | high, | |||
Cudd_ReorderingType | submethod | |||
) |
AutomaticEnd Function********************************************************************
Synopsis [Reorders by applying the method of the sliding window.]
Description [Reorders by applying the method of the sliding window. Tries all possible permutations to the variables in a window that slides from low to high. The size of the window is determined by submethod. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 111 of file cuddWindow.c.
00116 { 00117 00118 int res; 00119 #ifdef DD_DEBUG 00120 int supposedOpt; 00121 #endif 00122 00123 switch (submethod) { 00124 case CUDD_REORDER_WINDOW2: 00125 res = ddWindow2(table,low,high); 00126 break; 00127 case CUDD_REORDER_WINDOW3: 00128 res = ddWindow3(table,low,high); 00129 break; 00130 case CUDD_REORDER_WINDOW4: 00131 res = ddWindow4(table,low,high); 00132 break; 00133 case CUDD_REORDER_WINDOW2_CONV: 00134 res = ddWindowConv2(table,low,high); 00135 break; 00136 case CUDD_REORDER_WINDOW3_CONV: 00137 res = ddWindowConv3(table,low,high); 00138 #ifdef DD_DEBUG 00139 supposedOpt = table->keys - table->isolated; 00140 res = ddWindow3(table,low,high); 00141 if (table->keys - table->isolated != (unsigned) supposedOpt) { 00142 (void) fprintf(table->err, "Convergence failed! (%d != %d)\n", 00143 table->keys - table->isolated, supposedOpt); 00144 } 00145 #endif 00146 break; 00147 case CUDD_REORDER_WINDOW4_CONV: 00148 res = ddWindowConv4(table,low,high); 00149 #ifdef DD_DEBUG 00150 supposedOpt = table->keys - table->isolated; 00151 res = ddWindow4(table,low,high); 00152 if (table->keys - table->isolated != (unsigned) supposedOpt) { 00153 (void) fprintf(table->err,"Convergence failed! (%d != %d)\n", 00154 table->keys - table->isolated, supposedOpt); 00155 } 00156 #endif 00157 break; 00158 default: return(0); 00159 } 00160 00161 return(res); 00162 00163 } /* end of cuddWindowReorder */
static int ddPermuteWindow3 | ( | DdManager * | table, | |
int | x | |||
) | [static] |
Function********************************************************************
Synopsis [Tries all the permutations of the three variables between x and x+2 and retains the best.]
Description [Tries all the permutations of the three variables between x and x+2 and retains the best. Assumes that no dead nodes are present. Returns the index of the best permutation (1-6) in case of success; 0 otherwise.Assumes that no dead nodes are present. Returns the index of the best permutation (1-6) in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 330 of file cuddWindow.c.
00333 { 00334 int y,z; 00335 int size,sizeNew; 00336 int best; 00337 00338 #ifdef DD_DEBUG 00339 assert(table->dead == 0); 00340 assert(x+2 < table->size); 00341 #endif 00342 00343 size = table->keys - table->isolated; 00344 y = x+1; z = y+1; 00345 00346 /* The permutation pattern is: 00347 ** (x,y)(y,z) 00348 ** repeated three times to get all 3! = 6 permutations. 00349 */ 00350 #define ABC 1 00351 best = ABC; 00352 00353 #define BAC 2 00354 sizeNew = cuddSwapInPlace(table,x,y); 00355 if (sizeNew < size) { 00356 if (sizeNew == 0) return(0); 00357 best = BAC; 00358 size = sizeNew; 00359 } 00360 #define BCA 3 00361 sizeNew = cuddSwapInPlace(table,y,z); 00362 if (sizeNew < size) { 00363 if (sizeNew == 0) return(0); 00364 best = BCA; 00365 size = sizeNew; 00366 } 00367 #define CBA 4 00368 sizeNew = cuddSwapInPlace(table,x,y); 00369 if (sizeNew < size) { 00370 if (sizeNew == 0) return(0); 00371 best = CBA; 00372 size = sizeNew; 00373 } 00374 #define CAB 5 00375 sizeNew = cuddSwapInPlace(table,y,z); 00376 if (sizeNew < size) { 00377 if (sizeNew == 0) return(0); 00378 best = CAB; 00379 size = sizeNew; 00380 } 00381 #define ACB 6 00382 sizeNew = cuddSwapInPlace(table,x,y); 00383 if (sizeNew < size) { 00384 if (sizeNew == 0) return(0); 00385 best = ACB; 00386 size = sizeNew; 00387 } 00388 00389 /* Now take the shortest route to the best permuytation. 00390 ** The initial permutation is ACB. 00391 */ 00392 switch(best) { 00393 case BCA: if (!cuddSwapInPlace(table,y,z)) return(0); 00394 case CBA: if (!cuddSwapInPlace(table,x,y)) return(0); 00395 case ABC: if (!cuddSwapInPlace(table,y,z)) return(0); 00396 case ACB: break; 00397 case BAC: if (!cuddSwapInPlace(table,y,z)) return(0); 00398 case CAB: if (!cuddSwapInPlace(table,x,y)) return(0); 00399 break; 00400 default: return(0); 00401 } 00402 00403 #ifdef DD_DEBUG 00404 assert(table->keys - table->isolated == (unsigned) size); 00405 #endif 00406 00407 return(best); 00408 00409 } /* end of ddPermuteWindow3 */
static int ddPermuteWindow4 | ( | DdManager * | table, | |
int | w | |||
) | [static] |
Function********************************************************************
Synopsis [Tries all the permutations of the four variables between w and w+3 and retains the best.]
Description [Tries all the permutations of the four variables between w and w+3 and retains the best. Assumes that no dead nodes are present. Returns the index of the best permutation (1-24) in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 570 of file cuddWindow.c.
00573 { 00574 int x,y,z; 00575 int size,sizeNew; 00576 int best; 00577 00578 #ifdef DD_DEBUG 00579 assert(table->dead == 0); 00580 assert(w+3 < table->size); 00581 #endif 00582 00583 size = table->keys - table->isolated; 00584 x = w+1; y = x+1; z = y+1; 00585 00586 /* The permutation pattern is: 00587 * (w,x)(y,z)(w,x)(x,y) 00588 * (y,z)(w,x)(y,z)(x,y) 00589 * repeated three times to get all 4! = 24 permutations. 00590 * This gives a hamiltonian circuit of Cayley's graph. 00591 * The codes to the permutation are assigned in topological order. 00592 * The permutations at lower distance from the final permutation are 00593 * assigned lower codes. This way we can choose, between 00594 * permutations that give the same size, one that requires the minimum 00595 * number of swaps from the final permutation of the hamiltonian circuit. 00596 * There is an exception to this rule: ABCD is given Code 1, to 00597 * avoid oscillation when convergence is sought. 00598 */ 00599 #define ABCD 1 00600 best = ABCD; 00601 00602 #define BACD 7 00603 sizeNew = cuddSwapInPlace(table,w,x); 00604 if (sizeNew < size) { 00605 if (sizeNew == 0) return(0); 00606 best = BACD; 00607 size = sizeNew; 00608 } 00609 #define BADC 13 00610 sizeNew = cuddSwapInPlace(table,y,z); 00611 if (sizeNew < size) { 00612 if (sizeNew == 0) return(0); 00613 best = BADC; 00614 size = sizeNew; 00615 } 00616 #define ABDC 8 00617 sizeNew = cuddSwapInPlace(table,w,x); 00618 if (sizeNew < size || (sizeNew == size && ABDC < best)) { 00619 if (sizeNew == 0) return(0); 00620 best = ABDC; 00621 size = sizeNew; 00622 } 00623 #define ADBC 14 00624 sizeNew = cuddSwapInPlace(table,x,y); 00625 if (sizeNew < size) { 00626 if (sizeNew == 0) return(0); 00627 best = ADBC; 00628 size = sizeNew; 00629 } 00630 #define ADCB 9 00631 sizeNew = cuddSwapInPlace(table,y,z); 00632 if (sizeNew < size || (sizeNew == size && ADCB < best)) { 00633 if (sizeNew == 0) return(0); 00634 best = ADCB; 00635 size = sizeNew; 00636 } 00637 #define DACB 15 00638 sizeNew = cuddSwapInPlace(table,w,x); 00639 if (sizeNew < size) { 00640 if (sizeNew == 0) return(0); 00641 best = DACB; 00642 size = sizeNew; 00643 } 00644 #define DABC 20 00645 sizeNew = cuddSwapInPlace(table,y,z); 00646 if (sizeNew < size) { 00647 if (sizeNew == 0) return(0); 00648 best = DABC; 00649 size = sizeNew; 00650 } 00651 #define DBAC 23 00652 sizeNew = cuddSwapInPlace(table,x,y); 00653 if (sizeNew < size) { 00654 if (sizeNew == 0) return(0); 00655 best = DBAC; 00656 size = sizeNew; 00657 } 00658 #define BDAC 19 00659 sizeNew = cuddSwapInPlace(table,w,x); 00660 if (sizeNew < size || (sizeNew == size && BDAC < best)) { 00661 if (sizeNew == 0) return(0); 00662 best = BDAC; 00663 size = sizeNew; 00664 } 00665 #define BDCA 21 00666 sizeNew = cuddSwapInPlace(table,y,z); 00667 if (sizeNew < size || (sizeNew == size && BDCA < best)) { 00668 if (sizeNew == 0) return(0); 00669 best = BDCA; 00670 size = sizeNew; 00671 } 00672 #define DBCA 24 00673 sizeNew = cuddSwapInPlace(table,w,x); 00674 if (sizeNew < size) { 00675 if (sizeNew == 0) return(0); 00676 best = DBCA; 00677 size = sizeNew; 00678 } 00679 #define DCBA 22 00680 sizeNew = cuddSwapInPlace(table,x,y); 00681 if (sizeNew < size || (sizeNew == size && DCBA < best)) { 00682 if (sizeNew == 0) return(0); 00683 best = DCBA; 00684 size = sizeNew; 00685 } 00686 #define DCAB 18 00687 sizeNew = cuddSwapInPlace(table,y,z); 00688 if (sizeNew < size || (sizeNew == size && DCAB < best)) { 00689 if (sizeNew == 0) return(0); 00690 best = DCAB; 00691 size = sizeNew; 00692 } 00693 #define CDAB 12 00694 sizeNew = cuddSwapInPlace(table,w,x); 00695 if (sizeNew < size || (sizeNew == size && CDAB < best)) { 00696 if (sizeNew == 0) return(0); 00697 best = CDAB; 00698 size = sizeNew; 00699 } 00700 #define CDBA 17 00701 sizeNew = cuddSwapInPlace(table,y,z); 00702 if (sizeNew < size || (sizeNew == size && CDBA < best)) { 00703 if (sizeNew == 0) return(0); 00704 best = CDBA; 00705 size = sizeNew; 00706 } 00707 #define CBDA 11 00708 sizeNew = cuddSwapInPlace(table,x,y); 00709 if (sizeNew < size || (sizeNew == size && CBDA < best)) { 00710 if (sizeNew == 0) return(0); 00711 best = CBDA; 00712 size = sizeNew; 00713 } 00714 #define BCDA 16 00715 sizeNew = cuddSwapInPlace(table,w,x); 00716 if (sizeNew < size || (sizeNew == size && BCDA < best)) { 00717 if (sizeNew == 0) return(0); 00718 best = BCDA; 00719 size = sizeNew; 00720 } 00721 #define BCAD 10 00722 sizeNew = cuddSwapInPlace(table,y,z); 00723 if (sizeNew < size || (sizeNew == size && BCAD < best)) { 00724 if (sizeNew == 0) return(0); 00725 best = BCAD; 00726 size = sizeNew; 00727 } 00728 #define CBAD 5 00729 sizeNew = cuddSwapInPlace(table,w,x); 00730 if (sizeNew < size || (sizeNew == size && CBAD < best)) { 00731 if (sizeNew == 0) return(0); 00732 best = CBAD; 00733 size = sizeNew; 00734 } 00735 #define CABD 3 00736 sizeNew = cuddSwapInPlace(table,x,y); 00737 if (sizeNew < size || (sizeNew == size && CABD < best)) { 00738 if (sizeNew == 0) return(0); 00739 best = CABD; 00740 size = sizeNew; 00741 } 00742 #define CADB 6 00743 sizeNew = cuddSwapInPlace(table,y,z); 00744 if (sizeNew < size || (sizeNew == size && CADB < best)) { 00745 if (sizeNew == 0) return(0); 00746 best = CADB; 00747 size = sizeNew; 00748 } 00749 #define ACDB 4 00750 sizeNew = cuddSwapInPlace(table,w,x); 00751 if (sizeNew < size || (sizeNew == size && ACDB < best)) { 00752 if (sizeNew == 0) return(0); 00753 best = ACDB; 00754 size = sizeNew; 00755 } 00756 #define ACBD 2 00757 sizeNew = cuddSwapInPlace(table,y,z); 00758 if (sizeNew < size || (sizeNew == size && ACBD < best)) { 00759 if (sizeNew == 0) return(0); 00760 best = ACBD; 00761 size = sizeNew; 00762 } 00763 00764 /* Now take the shortest route to the best permutation. 00765 ** The initial permutation is ACBD. 00766 */ 00767 switch(best) { 00768 case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0); 00769 case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0); 00770 case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0); 00771 case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0); 00772 case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0); 00773 case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0); 00774 case ACBD: break; 00775 case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0); 00776 case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0); 00777 case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0); 00778 if (!cuddSwapInPlace(table,x,y)) return(0); 00779 if (!cuddSwapInPlace(table,y,z)) return(0); 00780 break; 00781 case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0); 00782 case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0); 00783 case DACB: if (!cuddSwapInPlace(table,y,z)) return(0); 00784 case BACD: if (!cuddSwapInPlace(table,x,y)) return(0); 00785 case CABD: if (!cuddSwapInPlace(table,w,x)) return(0); 00786 break; 00787 case DABC: if (!cuddSwapInPlace(table,y,z)) return(0); 00788 case BADC: if (!cuddSwapInPlace(table,x,y)) return(0); 00789 case CADB: if (!cuddSwapInPlace(table,w,x)) return(0); 00790 if (!cuddSwapInPlace(table,y,z)) return(0); 00791 break; 00792 case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0); 00793 case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0); 00794 case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0); 00795 case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0); 00796 break; 00797 case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0); 00798 case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0); 00799 if (!cuddSwapInPlace(table,x,y)) return(0); 00800 break; 00801 default: return(0); 00802 } 00803 00804 #ifdef DD_DEBUG 00805 assert(table->keys - table->isolated == (unsigned) size); 00806 #endif 00807 00808 return(best); 00809 00810 } /* end of ddPermuteWindow4 */
static int ddWindow2 | ( | DdManager * | table, | |
int | low, | |||
int | high | |||
) | [static] |
Function********************************************************************
Synopsis [Reorders by applying a sliding window of width 2.]
Description [Reorders by applying a sliding window of width 2. Tries both permutations of the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 183 of file cuddWindow.c.
00187 { 00188 00189 int x; 00190 int res; 00191 int size; 00192 00193 #ifdef DD_DEBUG 00194 assert(low >= 0 && high < table->size); 00195 #endif 00196 00197 if (high-low < 1) return(0); 00198 00199 res = table->keys - table->isolated; 00200 for (x = low; x < high; x++) { 00201 size = res; 00202 res = cuddSwapInPlace(table,x,x+1); 00203 if (res == 0) return(0); 00204 if (res >= size) { /* no improvement: undo permutation */ 00205 res = cuddSwapInPlace(table,x,x+1); 00206 if (res == 0) return(0); 00207 } 00208 #ifdef DD_STATS 00209 if (res < size) { 00210 (void) fprintf(table->out,"-"); 00211 } else { 00212 (void) fprintf(table->out,"="); 00213 } 00214 fflush(table->out); 00215 #endif 00216 } 00217 00218 return(1); 00219 00220 } /* end of ddWindow2 */
static int ddWindow3 | ( | DdManager * | table, | |
int | low, | |||
int | high | |||
) | [static] |
Function********************************************************************
Synopsis [Reorders by applying a sliding window of width 3.]
Description [Reorders by applying a sliding window of width 3. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 425 of file cuddWindow.c.
00429 { 00430 00431 int x; 00432 int res; 00433 00434 #ifdef DD_DEBUG 00435 assert(low >= 0 && high < table->size); 00436 #endif 00437 00438 if (high-low < 2) return(ddWindow2(table,low,high)); 00439 00440 for (x = low; x+1 < high; x++) { 00441 res = ddPermuteWindow3(table,x); 00442 if (res == 0) return(0); 00443 #ifdef DD_STATS 00444 if (res == ABC) { 00445 (void) fprintf(table->out,"="); 00446 } else { 00447 (void) fprintf(table->out,"-"); 00448 } 00449 fflush(table->out); 00450 #endif 00451 } 00452 00453 return(1); 00454 00455 } /* end of ddWindow3 */
static int ddWindow4 | ( | DdManager * | table, | |
int | low, | |||
int | high | |||
) | [static] |
Function********************************************************************
Synopsis [Reorders by applying a sliding window of width 4.]
Description [Reorders by applying a sliding window of width 4. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 826 of file cuddWindow.c.
00830 { 00831 00832 int w; 00833 int res; 00834 00835 #ifdef DD_DEBUG 00836 assert(low >= 0 && high < table->size); 00837 #endif 00838 00839 if (high-low < 3) return(ddWindow3(table,low,high)); 00840 00841 for (w = low; w+2 < high; w++) { 00842 res = ddPermuteWindow4(table,w); 00843 if (res == 0) return(0); 00844 #ifdef DD_STATS 00845 if (res == ABCD) { 00846 (void) fprintf(table->out,"="); 00847 } else { 00848 (void) fprintf(table->out,"-"); 00849 } 00850 fflush(table->out); 00851 #endif 00852 } 00853 00854 return(1); 00855 00856 } /* end of ddWindow4 */
static int ddWindowConv2 | ( | DdManager * | table, | |
int | low, | |||
int | high | |||
) | [static] |
Function********************************************************************
Synopsis [Reorders by repeatedly applying a sliding window of width 2.]
Description [Reorders by repeatedly applying a sliding window of width 2. Tries both permutations of the variables in a window that slides from low to high. Assumes that no dead nodes are present. Uses an event-driven approach to determine convergence. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 237 of file cuddWindow.c.
00241 { 00242 int x; 00243 int res; 00244 int nwin; 00245 int newevent; 00246 int *events; 00247 int size; 00248 00249 #ifdef DD_DEBUG 00250 assert(low >= 0 && high < table->size); 00251 #endif 00252 00253 if (high-low < 1) return(ddWindowConv2(table,low,high)); 00254 00255 nwin = high-low; 00256 events = ALLOC(int,nwin); 00257 if (events == NULL) { 00258 table->errorCode = CUDD_MEMORY_OUT; 00259 return(0); 00260 } 00261 for (x=0; x<nwin; x++) { 00262 events[x] = 1; 00263 } 00264 00265 res = table->keys - table->isolated; 00266 do { 00267 newevent = 0; 00268 for (x=0; x<nwin; x++) { 00269 if (events[x]) { 00270 size = res; 00271 res = cuddSwapInPlace(table,x+low,x+low+1); 00272 if (res == 0) { 00273 FREE(events); 00274 return(0); 00275 } 00276 if (res >= size) { /* no improvement: undo permutation */ 00277 res = cuddSwapInPlace(table,x+low,x+low+1); 00278 if (res == 0) { 00279 FREE(events); 00280 return(0); 00281 } 00282 } 00283 if (res < size) { 00284 if (x < nwin-1) events[x+1] = 1; 00285 if (x > 0) events[x-1] = 1; 00286 newevent = 1; 00287 } 00288 events[x] = 0; 00289 #ifdef DD_STATS 00290 if (res < size) { 00291 (void) fprintf(table->out,"-"); 00292 } else { 00293 (void) fprintf(table->out,"="); 00294 } 00295 fflush(table->out); 00296 #endif 00297 } 00298 } 00299 #ifdef DD_STATS 00300 if (newevent) { 00301 (void) fprintf(table->out,"|"); 00302 fflush(table->out); 00303 } 00304 #endif 00305 } while (newevent); 00306 00307 FREE(events); 00308 00309 return(1); 00310 00311 } /* end of ddWindowConv3 */
static int ddWindowConv3 | ( | DdManager * | table, | |
int | low, | |||
int | high | |||
) | [static] |
Function********************************************************************
Synopsis [Reorders by repeatedly applying a sliding window of width 3.]
Description [Reorders by repeatedly applying a sliding window of width 3. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Uses an event-driven approach to determine convergence. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 472 of file cuddWindow.c.
00476 { 00477 int x; 00478 int res; 00479 int nwin; 00480 int newevent; 00481 int *events; 00482 00483 #ifdef DD_DEBUG 00484 assert(low >= 0 && high < table->size); 00485 #endif 00486 00487 if (high-low < 2) return(ddWindowConv2(table,low,high)); 00488 00489 nwin = high-low-1; 00490 events = ALLOC(int,nwin); 00491 if (events == NULL) { 00492 table->errorCode = CUDD_MEMORY_OUT; 00493 return(0); 00494 } 00495 for (x=0; x<nwin; x++) { 00496 events[x] = 1; 00497 } 00498 00499 do { 00500 newevent = 0; 00501 for (x=0; x<nwin; x++) { 00502 if (events[x]) { 00503 res = ddPermuteWindow3(table,x+low); 00504 switch (res) { 00505 case ABC: 00506 break; 00507 case BAC: 00508 if (x < nwin-1) events[x+1] = 1; 00509 if (x > 1) events[x-2] = 1; 00510 newevent = 1; 00511 break; 00512 case BCA: 00513 case CBA: 00514 case CAB: 00515 if (x < nwin-2) events[x+2] = 1; 00516 if (x < nwin-1) events[x+1] = 1; 00517 if (x > 0) events[x-1] = 1; 00518 if (x > 1) events[x-2] = 1; 00519 newevent = 1; 00520 break; 00521 case ACB: 00522 if (x < nwin-2) events[x+2] = 1; 00523 if (x > 0) events[x-1] = 1; 00524 newevent = 1; 00525 break; 00526 default: 00527 FREE(events); 00528 return(0); 00529 } 00530 events[x] = 0; 00531 #ifdef DD_STATS 00532 if (res == ABC) { 00533 (void) fprintf(table->out,"="); 00534 } else { 00535 (void) fprintf(table->out,"-"); 00536 } 00537 fflush(table->out); 00538 #endif 00539 } 00540 } 00541 #ifdef DD_STATS 00542 if (newevent) { 00543 (void) fprintf(table->out,"|"); 00544 fflush(table->out); 00545 } 00546 #endif 00547 } while (newevent); 00548 00549 FREE(events); 00550 00551 return(1); 00552 00553 } /* end of ddWindowConv3 */
static int ddWindowConv4 | ( | DdManager * | table, | |
int | low, | |||
int | high | |||
) | [static] |
Function********************************************************************
Synopsis [Reorders by repeatedly applying a sliding window of width 4.]
Description [Reorders by repeatedly applying a sliding window of width 4. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Uses an event-driven approach to determine convergence. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 873 of file cuddWindow.c.
00877 { 00878 int x; 00879 int res; 00880 int nwin; 00881 int newevent; 00882 int *events; 00883 00884 #ifdef DD_DEBUG 00885 assert(low >= 0 && high < table->size); 00886 #endif 00887 00888 if (high-low < 3) return(ddWindowConv3(table,low,high)); 00889 00890 nwin = high-low-2; 00891 events = ALLOC(int,nwin); 00892 if (events == NULL) { 00893 table->errorCode = CUDD_MEMORY_OUT; 00894 return(0); 00895 } 00896 for (x=0; x<nwin; x++) { 00897 events[x] = 1; 00898 } 00899 00900 do { 00901 newevent = 0; 00902 for (x=0; x<nwin; x++) { 00903 if (events[x]) { 00904 res = ddPermuteWindow4(table,x+low); 00905 switch (res) { 00906 case ABCD: 00907 break; 00908 case BACD: 00909 if (x < nwin-1) events[x+1] = 1; 00910 if (x > 2) events[x-3] = 1; 00911 newevent = 1; 00912 break; 00913 case BADC: 00914 if (x < nwin-3) events[x+3] = 1; 00915 if (x < nwin-1) events[x+1] = 1; 00916 if (x > 0) events[x-1] = 1; 00917 if (x > 2) events[x-3] = 1; 00918 newevent = 1; 00919 break; 00920 case ABDC: 00921 if (x < nwin-3) events[x+3] = 1; 00922 if (x > 0) events[x-1] = 1; 00923 newevent = 1; 00924 break; 00925 case ADBC: 00926 case ADCB: 00927 case ACDB: 00928 if (x < nwin-3) events[x+3] = 1; 00929 if (x < nwin-2) events[x+2] = 1; 00930 if (x > 0) events[x-1] = 1; 00931 if (x > 1) events[x-2] = 1; 00932 newevent = 1; 00933 break; 00934 case DACB: 00935 case DABC: 00936 case DBAC: 00937 case BDAC: 00938 case BDCA: 00939 case DBCA: 00940 case DCBA: 00941 case DCAB: 00942 case CDAB: 00943 case CDBA: 00944 case CBDA: 00945 case BCDA: 00946 case CADB: 00947 if (x < nwin-3) events[x+3] = 1; 00948 if (x < nwin-2) events[x+2] = 1; 00949 if (x < nwin-1) events[x+1] = 1; 00950 if (x > 0) events[x-1] = 1; 00951 if (x > 1) events[x-2] = 1; 00952 if (x > 2) events[x-3] = 1; 00953 newevent = 1; 00954 break; 00955 case BCAD: 00956 case CBAD: 00957 case CABD: 00958 if (x < nwin-2) events[x+2] = 1; 00959 if (x < nwin-1) events[x+1] = 1; 00960 if (x > 1) events[x-2] = 1; 00961 if (x > 2) events[x-3] = 1; 00962 newevent = 1; 00963 break; 00964 case ACBD: 00965 if (x < nwin-2) events[x+2] = 1; 00966 if (x > 1) events[x-2] = 1; 00967 newevent = 1; 00968 break; 00969 default: 00970 FREE(events); 00971 return(0); 00972 } 00973 events[x] = 0; 00974 #ifdef DD_STATS 00975 if (res == ABCD) { 00976 (void) fprintf(table->out,"="); 00977 } else { 00978 (void) fprintf(table->out,"-"); 00979 } 00980 fflush(table->out); 00981 #endif 00982 } 00983 } 00984 #ifdef DD_STATS 00985 if (newevent) { 00986 (void) fprintf(table->out,"|"); 00987 fflush(table->out); 00988 } 00989 #endif 00990 } while (newevent); 00991 00992 FREE(events); 00993 00994 return(1); 00995 00996 } /* end of ddWindowConv4 */
char rcsid [] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddWindow.c]
PackageName [cudd]
Synopsis [Functions for window permutation]
Description [Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 57 of file cuddWindow.c.