abc/src/bdd/cudd/cuddGroup.c
/**Function********************************************************************

  Synopsis    [Checks for extended symmetry of x and y.]

  Description [Checks for extended symmetry of x and y. Returns 1 in
  case of extended symmetry; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Checks for extended symmetry of x and y.]

Description [Checks for extended symmetry of x and y. Returns 1 in
case of extended symmetry; 0 otherwise.]


Function Synopsis [ Checks for extended symmetry of x and y . ] Description [ Checks for extended symmetry of x and y . Returns 1 in case of extended symmetry ; 0 otherwise . ]
static int
ddExtSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
    DdNode *one;
    unsigned comple;    
    int notproj;        
    int arccount;       
    int TotalRefCount;  
    int counter;        
    int arccounter;     
    int i;
    int xindex;
    int yindex;
    int res;
    int slots;
    DdNodePtr *list;
    DdNode *sentinel = &(table->sentinel);
    xindex = table->invperm[x];
    yindex = table->invperm[y];
    if (!cuddTestInteract(table,xindex,yindex))
        return(0);
#ifdef DD_DEBUG
    if (table->subtables[x].keys == 1) {
        assert(table->vars[xindex]->ref != 1);
    }
    if (table->subtables[y].keys == 1) {
        assert(table->vars[yindex]->ref != 1);
    }
#endif
#ifdef DD_STATS
    extsymmcalls++;
#endif
    arccount = 0;
    counter = (int) (table->subtables[x].keys *
              (table->symmviolation/100.0) + 0.5);
    one = DD_ONE(table);
    slots = table->subtables[x].slots;
    list = table->subtables[x].nodelist;
    for (i = 0; i < slots; i++) {
        f = list[i];
        while (f != sentinel) {
            f1 = cuddT(f);
            f0 = Cudd_Regular(cuddE(f));
            comple = Cudd_IsComplement(cuddE(f));
            notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;
            if (f1->index == (unsigned) yindex) {
                arccount++;
                f11 = cuddT(f1); f10 = cuddE(f1);
            } else {
                if ((int) f0->index != yindex) {
                    if (notproj) {
                        if (counter == 0)
                            return(0);
                        counter--; 
                    }
                }
                f11 = f10 = f1;
            }
            if ((int) f0->index == yindex) {
                arccount++;
                f01 = cuddT(f0); f00 = cuddE(f0);
            } else {
                f01 = f00 = f0;
            }
            if (comple) {
                f01 = Cudd_Not(f01);
                f00 = Cudd_Not(f00);
            }
            if (notproj) {
                if (f01 != f10 && f11 != f00) {
                    if (counter == 0)
                        return(0);
                    counter--;
                }
            }
            f = f->next;
        } 
    } 
    TotalRefCount = -1; 
    slots = table->subtables[y].slots;
    list = table->subtables[y].nodelist;
    for (i = 0; i < slots; i++) {
        f = list[i];
        while (f != sentinel) {
            TotalRefCount += f->ref;
            f = f->next;
        }
    }
    arccounter = (int) (table->subtables[y].keys *
                 (table->arcviolation/100.0) + 0.5);
    res = arccount >= TotalRefCount - arccounter;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    if (res) {
        (void) fprintf(table->out,
                       "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
                       xindex,yindex,x,y);
    }
#endif
#ifdef DD_STATS
    if (res)
        extsymm++;
#endif
    return(res);
}
static int ddExtSymmCheck ( DdManager * table , int x , int y ) { DdNode * f , * f0 , * f1 , * f01 , * f00 , * f11 , * f10 ; DdNode * one ; unsigned comple ; int notproj ; int arccount ; int TotalRefCount ; int counter ; int arccounter ; int i ; int xindex ; int yindex ; int res ; int slots ; DdNodePtr * list ; DdNode * sentinel = & ( table -> sentinel ) ; xindex = table -> invperm [ x ] ; yindex = table -> invperm [ y ] ; if ( ! cuddTestInteract ( table , xindex , yindex ) ) return ( 0 ) ; #ifdef DD_DEBUG if ( table -> subtables [ x ] . keys == 1 ) { assert ( table -> vars [ xindex ] -> ref != 1 ) ; } if ( table -> subtables [ y ] . keys == 1 ) { assert ( table -> vars [ yindex ] -> ref != 1 ) ; } #endif #ifdef DD_STATS extsymmcalls ++ ; #endif arccount = 0 ; counter = ( int ) ( table -> subtables [ x ] . keys * ( table -> symmviolation / 100.0 ) + 0.5 ) ; one = DD_ONE ( table ) ; slots = table -> subtables [ x ] . slots ; list = table -> subtables [ x ] . nodelist ; for ( i = 0 ; i < slots ; i ++ ) { f = list [ i ] ; while ( f != sentinel ) { f1 = cuddT ( f ) ; f0 = Cudd_Regular ( cuddE ( f ) ) ; comple = Cudd_IsComplement ( cuddE ( f ) ) ; notproj = f1 != one || f0 != one || f -> ref != ( DdHalfWord ) 1 ; if ( f1 -> index == ( unsigned ) yindex ) { arccount ++ ; f11 = cuddT ( f1 ) ; f10 = cuddE ( f1 ) ; } else { if ( ( int ) f0 -> index != yindex ) { if ( notproj ) { if ( counter == 0 ) return ( 0 ) ; counter -- ; } } f11 = f10 = f1 ; } if ( ( int ) f0 -> index == yindex ) { arccount ++ ; f01 = cuddT ( f0 ) ; f00 = cuddE ( f0 ) ; } else { f01 = f00 = f0 ; } if ( comple ) { f01 = Cudd_Not ( f01 ) ; f00 = Cudd_Not ( f00 ) ; } if ( notproj ) { if ( f01 != f10 && f11 != f00 ) { if ( counter == 0 ) return ( 0 ) ; counter -- ; } } f = f -> next ; } } TotalRefCount = -1 ; slots = table -> subtables [ y ] . slots ; list = table -> subtables [ y ] . nodelist ; for ( i = 0 ; i < slots ; i ++ ) { f = list [ i ] ; while ( f != sentinel ) { TotalRefCount += f -> ref ; f = f -> next ; } } arccounter = ( int ) ( table -> subtables [ y ] . keys * ( table -> arcviolation / 100.0 ) + 0.5 ) ; res = arccount >= TotalRefCount - arccounter ; #if defined ( DD_DEBUG ) && defined ( DD_VERBOSE ) if ( res ) { ( void ) fprintf ( table -> out , " \t \t \n " , xindex , yindex , x , y ) ; } #endif #ifdef DD_STATS if ( res ) extsymm ++ ; #endif return ( res ) ; }
Function
Synopsis    [Checks for extended symmetry of x and y.]
Function Synopsis [ Checks for extended symmetry of x and y . ]
/* f0 is complemented */ /* f is not a projection function */ /* number of arcs from layer x to layer y */ /* total reference count of layer y minus 1 */ /* number of nodes of layer x that are allowed */ /* to violate extended symmetry conditions */ /* number of arcs into layer y that are allowed */ /* to come from layers other than x */ /* If the two variables do not interact, we do not want to merge them. */ /* Checks that x and y do not contain just the projection functions.
    ** With the test on interaction, these test become redundant,
    ** because an isolated projection function does not interact with
    ** any other variable.
    */ /* Find f1, f0, f11, f10, f01, f00. */ /* If f is an isolated projection function it is
                    ** allowed to bypass layer y.
                    */ /* f bypasses layer y */ /* Unless we are looking at a projection function
            ** without external references except the one from the
            ** table, we insist that f01 == f10 or f11 == f00
            */ /* while */ /* for */ /* Calculate the total reference counts of y */ /* -1 for projection function */