abc/src/bdd/extrab/extraBddSymm.c
/**Function********************************************************************

  Synopsis    [Performs a recursive step of Extra_SymmPairsCompute.]

  Description [Returns the set of symmetric variable pairs represented as a set 
  of two-literal ZDD cubes. Both variables always appear in the positive polarity
  in the cubes. This function works without building new BDD nodes. Some relatively 
  small number of ZDD nodes may be built to ensure proper bookkeeping of the 
  symmetry information.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Performs a recursive step of Extra_SymmPairsCompute.]

Description [Returns the set of symmetric variable pairs represented as a set
of two-literal ZDD cubes. Both variables always appear in the positive polarity
in the cubes. This function works without building new BDD nodes. Some relatively
small number of ZDD nodes may be built to ensure proper bookkeeping of the
symmetry information.]




Function Synopsis [ Performs a recursive step of Extra_SymmPairsCompute . ] Description [ Returns the set of symmetric variable pairs represented as a set of two - literal ZDD cubes . Both variables always appear in the positive polarity in the cubes . This function works without building new BDD nodes . Some relatively small number of ZDD nodes may be built to ensure proper bookkeeping of the symmetry information . ]
DdNode * 
extraZddSymmPairsCompute( 
  DdManager * dd,   
  DdNode * bFunc,   
  DdNode * bVars )  
{
    DdNode * zRes;
    DdNode * bFR = Cudd_Regular(bFunc); 
    if ( cuddIsConstant(bFR) )
    {
        int nVars, i;
        nVars = Extra_bddSuppSize( dd, bVars );
        if ( nVars < 2 )
            return z0;
        else
        {
            DdNode * bVarsK;
            bVarsK = bVars;
            for ( i = 0; i < nVars-2; i++ )
                bVarsK = cuddT( bVarsK );
            return extraZddTuplesFromBdd( dd, bVarsK, bVars );
        }
    }
    assert( bVars != b1 );
    if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars)) )
        return zRes;
    else
    {
        DdNode * zRes0, * zRes1;
        DdNode * zTemp, * zPlus, * zSymmVars;             
        DdNode * bF0, * bF1;             
        DdNode * bVarsNew;
        int nVarsExtra;
        int LevelF;
        nVarsExtra = 0;
        LevelF = dd->perm[bFR->index];
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
            nVarsExtra++; 
        assert( bFR->index == bVarsNew->index );
        if ( bFR != bFunc ) 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
        zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) );
        if ( zRes0 == NULL )
            return NULL;
        cuddRef( zRes0 );
        if ( zRes0 == z0 )
            zRes = zRes0;  
        else
        {
            zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
        }
        zSymmVars = extraZddGetSymmetricVars( dd, bF1, bF0, cuddT(bVarsNew) );
        if ( zSymmVars == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zSymmVars );
        if ( zSymmVars == z0 )
            Cudd_RecursiveDerefZdd( dd, zSymmVars );
        else
        {
            zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                Cudd_RecursiveDerefZdd( dd, zSymmVars );
                return NULL;
            }
            cuddRef( zPlus );
            cuddDeref( zSymmVars );
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        if ( nVarsExtra )
        {
            DdNode * bVarsExtra;
            int nVars;
            bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc );  
            if ( bVarsExtra == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( bVarsExtra );
            Extra
            nVars = Extra_bddSuppSize( dd, bVarsExtra );
            if ( nVars < 2 )
            {
                Cudd_RecursiveDeref( dd, bVarsExtra );
            }
            else
            {
                int i;
                DdNode * bVarsK;
                bVarsK = bVarsExtra;
                for ( i = 0; i < nVars-2; i++ )
                    bVarsK = cuddT( bVarsK );
                zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra );
                if ( zPlus == NULL )
                {
                    Cudd_RecursiveDeref( dd, bVarsExtra );
                    Cudd_RecursiveDerefZdd( dd, zRes );
                    return NULL;
                }
                cuddRef( zPlus );
                Cudd_RecursiveDeref( dd, bVarsExtra );
                zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
                if ( zRes == NULL )
                {
                    Cudd_RecursiveDerefZdd( dd, zTemp );
                    Cudd_RecursiveDerefZdd( dd, zPlus );
                    return NULL;
                }
                cuddRef( zRes );
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
            }
        }
        cuddDeref( zRes );
        cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes);
        return zRes;
    }
}
DdNode * extraZddSymmPairsCompute ( DdManager * dd , DdNode * bFunc , DdNode * bVars ) { DdNode * zRes ; DdNode * bFR = Cudd_Regular ( bFunc ) ; if ( cuddIsConstant ( bFR ) ) { int nVars , i ; nVars = Extra_bddSuppSize ( dd , bVars ) ; if ( nVars < 2 ) return z0 ; else { DdNode * bVarsK ; bVarsK = bVars ; for ( i = 0 ; i < nVars - 2 ; i ++ ) bVarsK = cuddT ( bVarsK ) ; return extraZddTuplesFromBdd ( dd , bVarsK , bVars ) ; } } assert ( bVars != b1 ) ; if ( ( zRes = cuddCacheLookup2Zdd ( dd , extraZddSymmPairsCompute , bFunc , bVars ) ) ) return zRes ; else { DdNode * zRes0 , * zRes1 ; DdNode * zTemp , * zPlus , * zSymmVars ; DdNode * bF0 , * bF1 ; DdNode * bVarsNew ; int nVarsExtra ; int LevelF ; nVarsExtra = 0 ; LevelF = dd -> perm [ bFR -> index ] ; for ( bVarsNew = bVars ; LevelF > dd -> perm [ bVarsNew -> index ] ; bVarsNew = cuddT ( bVarsNew ) ) nVarsExtra ++ ; assert ( bFR -> index == bVarsNew -> index ) ; if ( bFR != bFunc ) { bF0 = Cudd_Not ( cuddE ( bFR ) ) ; bF1 = Cudd_Not ( cuddT ( bFR ) ) ; } else { bF0 = cuddE ( bFR ) ; bF1 = cuddT ( bFR ) ; } zRes0 = extraZddSymmPairsCompute ( dd , bF0 , cuddT ( bVarsNew ) ) ; if ( zRes0 == NULL ) return NULL ; cuddRef ( zRes0 ) ; if ( zRes0 == z0 ) zRes = zRes0 ; else { zRes1 = extraZddSymmPairsCompute ( dd , bF1 , cuddT ( bVarsNew ) ) ; if ( zRes1 == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes0 ) ; return NULL ; } cuddRef ( zRes1 ) ; zRes = cuddZddIntersect ( dd , zRes0 , zRes1 ) ; if ( zRes == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes0 ) ; Cudd_RecursiveDerefZdd ( dd , zRes1 ) ; return NULL ; } cuddRef ( zRes ) ; Cudd_RecursiveDerefZdd ( dd , zRes0 ) ; Cudd_RecursiveDerefZdd ( dd , zRes1 ) ; } zSymmVars = extraZddGetSymmetricVars ( dd , bF1 , bF0 , cuddT ( bVarsNew ) ) ; if ( zSymmVars == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes ) ; return NULL ; } cuddRef ( zSymmVars ) ; if ( zSymmVars == z0 ) Cudd_RecursiveDerefZdd ( dd , zSymmVars ) ; else { zPlus = cuddZddGetNode ( dd , 2 * bFR -> index , zSymmVars , z0 ) ; if ( zPlus == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes ) ; Cudd_RecursiveDerefZdd ( dd , zSymmVars ) ; return NULL ; } cuddRef ( zPlus ) ; cuddDeref ( zSymmVars ) ; zRes = cuddZddUnion ( dd , zTemp = zRes , zPlus ) ; if ( zRes == NULL ) { Cudd_RecursiveDerefZdd ( dd , zTemp ) ; Cudd_RecursiveDerefZdd ( dd , zPlus ) ; return NULL ; } cuddRef ( zRes ) ; Cudd_RecursiveDerefZdd ( dd , zTemp ) ; Cudd_RecursiveDerefZdd ( dd , zPlus ) ; } if ( nVarsExtra ) { DdNode * bVarsExtra ; int nVars ; bVarsExtra = extraBddReduceVarSet ( dd , bVars , bFunc ) ; if ( bVarsExtra == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes ) ; return NULL ; } cuddRef ( bVarsExtra ) ; nVars = Extra_bddSuppSize ( dd , bVarsExtra ) ; if ( nVars < 2 ) { Cudd_RecursiveDeref ( dd , bVarsExtra ) ; } else { int i ; DdNode * bVarsK ; bVarsK = bVarsExtra ; for ( i = 0 ; i < nVars - 2 ; i ++ ) bVarsK = cuddT ( bVarsK ) ; zPlus = extraZddTuplesFromBdd ( dd , bVarsK , bVarsExtra ) ; if ( zPlus == NULL ) { Cudd_RecursiveDeref ( dd , bVarsExtra ) ; Cudd_RecursiveDerefZdd ( dd , zRes ) ; return NULL ; } cuddRef ( zPlus ) ; Cudd_RecursiveDeref ( dd , bVarsExtra ) ; zRes = cuddZddUnion ( dd , zTemp = zRes , zPlus ) ; if ( zRes == NULL ) { Cudd_RecursiveDerefZdd ( dd , zTemp ) ; Cudd_RecursiveDerefZdd ( dd , zPlus ) ; return NULL ; } cuddRef ( zRes ) ; Cudd_RecursiveDerefZdd ( dd , zTemp ) ; Cudd_RecursiveDerefZdd ( dd , zPlus ) ; } } cuddDeref ( zRes ) ; cuddCacheInsert2 ( dd , extraZddSymmPairsCompute , bFunc , bVars , zRes ) ; return zRes ; } }
Function
Synopsis    [Performs a recursive step of Extra_SymmPairsCompute.]
Function Synopsis [ Performs a recursive step of Extra_SymmPairsCompute . ]
/* the manager */ /* the function whose symmetries are computed */ /* the set of variables on which this function depends */ // determine how many vars are in the bVars // create the BDD bVarsK corresponding to K = 2; // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F // count how many extra vars are there in bVars // the indexes (level) of variables should be synchronized now // cofactor the function // bFunc is complemented  // solve subproblems // if there is no symmetries in the negative cofactor // there is no need to test the positive cofactor // zRes takes reference // only those variables are pair-wise symmetric  // that are pair-wise symmetric in both cofactors // therefore, intersect the solutions // consider the current top-most variable and find all the vars // that are pairwise symmetric with it // these variables are returned as a set of ZDD singletons // attach the topmost variable to the set, to get the variable pairs // use the positive polarity ZDD variable for the purpose // there is no need to do so, if zSymmVars is empty // add these variable pairs to the result // only zRes is referenced at this point // if we skipped some variables, these variables cannot be symmetric with // any variables that are currently in the support of bF, but they can be  // symmetric with the variables that are in bVars but not in the support of bF // it is possible to improve this step: // (1) there is no need to enter here, if nVarsExtra < 2 // create the set of topmost nVarsExtra in bVars // remove from bVars all the variable that are in the support of bFunc // determine how many vars are in the bVarsExtra // create the BDD bVarsK corresponding to K = 2; // create the 2 variable tuples // add these to the result /* insert the result into cache */