abc/src/bdd/cudd/cuddWindow.c
/**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]

******************************************************************************/
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.]


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 . ]
static int
ddPermuteWindow3(
  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;
#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;
    }
    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);
}
static int ddPermuteWindow3 ( 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 ; #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 ; } 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 ) ; }
Function
Synopsis [Tries all the permutations of the three variables between
x and x+2 and retains the best.]
Function Synopsis [ Tries all the permutations of the three variables between x and x + 2 and retains the best . ]
/* The permutation pattern is:
    ** (x,y)(y,z)
    ** repeated three times to get all 3! = 6 permutations.
    */ /* Now take the shortest route to the best permuytation.
    ** The initial permutation is ACB.
    */