📄 cuddwindow.c
字号:
/**CFile*********************************************************************** FileName [cuddWindow.c] PackageName [cudd] Synopsis [Functions for window permutation] Description [Internal procedures included in this module: <ul> <li> cuddWindowReorder() </ul> Static procedures included in this module: <ul> <li> ddWindow2() <li> ddWindowConv2() <li> ddPermuteWindow3() <li> ddWindow3() <li> ddWindowConv3() <li> ddPermuteWindow4() <li> ddWindow4() <li> ddWindowConv4() </ul>] 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.]******************************************************************************/#include "util.h"#include "cuddInt.h"/*---------------------------------------------------------------------------*//* Constant declarations *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Stucture declarations *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Type declarations *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Variable declarations *//*---------------------------------------------------------------------------*/#ifndef lintstatic char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";#endif#ifdef DD_STATSextern int ddTotalNumberSwapping;extern int ddTotalNISwaps;#endif/*---------------------------------------------------------------------------*//* Macro declarations *//*---------------------------------------------------------------------------*//**AutomaticStart*************************************************************//*---------------------------------------------------------------------------*//* Static function prototypes *//*---------------------------------------------------------------------------*/static int ddWindow2 ARGS((DdManager *table, int low, int high));static int ddWindowConv2 ARGS((DdManager *table, int low, int high));static int ddPermuteWindow3 ARGS((DdManager *table, int x));static int ddWindow3 ARGS((DdManager *table, int low, int high));static int ddWindowConv3 ARGS((DdManager *table, int low, int high));static int ddPermuteWindow4 ARGS((DdManager *table, int w));static int ddWindow4 ARGS((DdManager *table, int low, int high));static int ddWindowConv4 ARGS((DdManager *table, int low, int high));/**AutomaticEnd***************************************************************//*---------------------------------------------------------------------------*//* Definition of exported functions *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Definition of internal functions *//*---------------------------------------------------------------------------*//**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]******************************************************************************/intcuddWindowReorder( DdManager * table /* DD table */, int low /* lowest index to reorder */, int high /* highest index to reorder */, Cudd_ReorderingType submethod /* window reordering option */){ int res;#ifdef DD_DEBUG int supposedOpt;#endif switch (submethod) { case CUDD_REORDER_WINDOW2: res = ddWindow2(table,low,high); break; case CUDD_REORDER_WINDOW3: res = ddWindow3(table,low,high); break; case CUDD_REORDER_WINDOW4: res = ddWindow4(table,low,high); break; case CUDD_REORDER_WINDOW2_CONV: res = ddWindowConv2(table,low,high); break; case CUDD_REORDER_WINDOW3_CONV: res = ddWindowConv3(table,low,high);#ifdef DD_DEBUG supposedOpt = table->keys - table->isolated; res = ddWindow3(table,low,high); if (table->keys - table->isolated != (unsigned) supposedOpt) { (void) fprintf(table->err, "Convergence failed! (%d != %d)\n", table->keys - table->isolated, supposedOpt); }#endif break; case CUDD_REORDER_WINDOW4_CONV: res = ddWindowConv4(table,low,high);#ifdef DD_DEBUG supposedOpt = table->keys - table->isolated; res = ddWindow4(table,low,high); if (table->keys - table->isolated != (unsigned) supposedOpt) { (void) fprintf(table->err,"Convergence failed! (%d != %d)\n", table->keys - table->isolated, supposedOpt); }#endif break; default: return(0); } return(res);} /* end of cuddWindowReorder *//*---------------------------------------------------------------------------*//* Definition of static functions *//*---------------------------------------------------------------------------*//**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]******************************************************************************/static intddWindow2( DdManager * table, int low, int high){ int x; int res; int size;#ifdef DD_DEBUG assert(low >= 0 && high < table->size);#endif if (high-low < 1) return(0); res = table->keys - table->isolated; for (x = low; x < high; x++) { size = res; res = cuddSwapInPlace(table,x,x+1); if (res == 0) return(0); if (res >= size) { /* no improvement: undo permutation */ res = cuddSwapInPlace(table,x,x+1); if (res == 0) return(0); }#ifdef DD_STATS if (res < size) { (void) fprintf(table->out,"-"); } else { (void) fprintf(table->out,"="); } fflush(table->out);#endif } return(1);} /* end of ddWindow2 *//**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]******************************************************************************/static intddWindowConv2( DdManager * table, int low, int high){ int x; int res; int nwin; int newevent; int *events; int size;#ifdef DD_DEBUG assert(low >= 0 && high < table->size);#endif if (high-low < 1) return(ddWindowConv2(table,low,high)); nwin = high-low; events = ALLOC(int,nwin); if (events == NULL) { table->errorCode = CUDD_MEMORY_OUT; return(0); } for (x=0; x<nwin; x++) { events[x] = 1; } res = table->keys - table->isolated; do { newevent = 0; for (x=0; x<nwin; x++) { if (events[x]) { size = res; res = cuddSwapInPlace(table,x+low,x+low+1); if (res == 0) { FREE(events); return(0); } if (res >= size) { /* no improvement: undo permutation */ res = cuddSwapInPlace(table,x+low,x+low+1); if (res == 0) { FREE(events); return(0); } } if (res < size) { if (x < nwin-1) events[x+1] = 1; if (x > 0) events[x-1] = 1; newevent = 1; } events[x] = 0;#ifdef DD_STATS if (res < size) { (void) fprintf(table->out,"-"); } else { (void) fprintf(table->out,"="); } fflush(table->out);#endif } }#ifdef DD_STATS if (newevent) { (void) fprintf(table->out,"|"); fflush(table->out); }#endif } while (newevent); FREE(events); return(1);} /* end of ddWindowConv3 *//**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]******************************************************************************/static intddPermuteWindow3( DdManager * table, int x){ int y,z; int size,sizeNew; int best;#ifdef DD_DEBUG assert(table->dead == 0); assert(x+2 < table->size);#endif size = table->keys - table->isolated; y = x+1; z = y+1; /* The permutation pattern is: ** (x,y)(y,z) ** repeated three times to get all 3! = 6 permutations. */#define ABC 1 best = ABC;#define BAC 2 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { if (sizeNew == 0) return(0); best = BAC; size = sizeNew; }#define BCA 3 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size) { if (sizeNew == 0) return(0); best = BCA; size = sizeNew; }#define CBA 4 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { if (sizeNew == 0) return(0); best = CBA; size = sizeNew; }#define CAB 5 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size) { if (sizeNew == 0) return(0); best = CAB; size = sizeNew; }#define ACB 6 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { if (sizeNew == 0) return(0); best = ACB; size = sizeNew; } /* Now take the shortest route to the best permuytation. ** The initial permutation is ACB. */ switch(best) { case BCA: if (!cuddSwapInPlace(table,y,z)) return(0); case CBA: if (!cuddSwapInPlace(table,x,y)) return(0); case ABC: if (!cuddSwapInPlace(table,y,z)) return(0); case ACB: break; case BAC: if (!cuddSwapInPlace(table,y,z)) return(0); case CAB: if (!cuddSwapInPlace(table,x,y)) return(0); break; default: return(0); }#ifdef DD_DEBUG assert(table->keys - table->isolated == (unsigned) size);#endif return(best);} /* end of ddPermuteWindow3 *//**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]******************************************************************************/static intddWindow3( DdManager * table, int low, int high){ int x; int res;#ifdef DD_DEBUG assert(low >= 0 && high < table->size);#endif if (high-low < 2) return(ddWindow2(table,low,high)); for (x = low; x+1 < high; x++) { res = ddPermuteWindow3(table,x); if (res == 0) return(0);#ifdef DD_STATS if (res == ABC) { (void) fprintf(table->out,"="); } else { (void) fprintf(table->out,"-"); } fflush(table->out);#endif } return(1);} /* end of ddWindow3 *//**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]******************************************************************************/static intddWindowConv3( DdManager * table, int low, int high){ int x; int res; int nwin; int newevent; int *events;#ifdef DD_DEBUG assert(low >= 0 && high < table->size);#endif if (high-low < 2) return(ddWindowConv2(table,low,high)); nwin = high-low-1; events = ALLOC(int,nwin); if (events == NULL) { table->errorCode = CUDD_MEMORY_OUT; return(0); } for (x=0; x<nwin; x++) { events[x] = 1; } do {
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -