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

  Synopsis    [Performs the recursive step of Extra_bddCheckVarsSymmetric().]

  Description [Returns b0 if the variables are not symmetric. Returns b1 if the
  variables can be symmetric. The variables are represented in the form of a 
  two-variable cube. In case the cube contains one variable (below Var1 level),
  the cube's pointer is complemented if the variable Var1 occurred on the 
  current path; otherwise, the cube's pointer is regular. Uses additional 
  complemented bit (Hash_Not) to mark the result if in the BDD rooted that this
  node there is a branch passing though the node labeled with Var2.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Performs the recursive step of Extra_bddCheckVarsSymmetric().]

Description [Returns b0 if the variables are not symmetric. Returns b1 if the
variables can be symmetric. The variables are represented in the form of a
two-variable cube. In case the cube contains one variable (below Var1 level),
the cube's pointer is complemented if the variable Var1 occurred on the
current path; otherwise, the cube's pointer is regular. Uses additional
complemented bit (Hash_Not) to mark the result if in the BDD rooted that this
node there is a branch passing though the node labeled with Var2.]




Function Synopsis [ Performs the recursive step of Extra_bddCheckVarsSymmetric () . ] Description [ Returns b0 if the variables are not symmetric . Returns b1 if the variables can be symmetric . The variables are represented in the form of a two - variable cube . In case the cube contains one variable ( below Var1 level ) the cube ' s pointer is complemented if the variable Var1 occurred on the current path ; otherwise the cube ' s pointer is regular . Uses additional complemented bit ( Hash_Not ) to mark the result if in the BDD rooted that this node there is a branch passing though the node labeled with Var2 . ]
DdNode * extraBddCheckVarsSymmetric( 
  DdManager * dd,    
  DdNode * bF,
  DdNode * bVars) 
{
    DdNode * bRes;
    if ( bF == b0 )
        return b1;
    assert( bVars != b1 );
    if ( (bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars)) )
        return bRes;
    else
    {
        DdNode * bRes0, * bRes1;
        DdNode * bF0, * bF1;             
        DdNode * bFR = Cudd_Regular(bF);
        int LevelF = cuddI(dd,bFR->index);
        DdNode * bVarsR = Cudd_Regular(bVars);
        int fVar1Pres;
        int iLev1;
        int iLev2;
        if ( bVarsR != bVars ) 
        {
            assert( cuddT(bVarsR) == b1 );
            fVar1Pres = 1;                    
            iLev1 = -1;                       
            iLev2 = dd->perm[bVarsR->index];  
        }
        else  
        {
            fVar1Pres = 0;                    
            if ( cuddT(bVars) == b1 )
            {
                iLev1 = -1;                              
                iLev2 = dd->perm[bVars->index];         
            }
            else
            {
                assert( cuddT(cuddT(bVars)) == b1 );
                iLev1 = dd->perm[bVars->index];         
                iLev2 = dd->perm[cuddT(bVars)->index];  
            }
        }
        if ( LevelF < iLev2 )
        {
            if ( bFR != bF ) 
            {
                bF0 = Cudd_Not( cuddE(bFR) );
                bF1 = Cudd_Not( cuddT(bFR) );
            }
            else
            {
                bF0 = cuddE(bFR);
                bF1 = cuddT(bFR);
            }
        }
        else
            bF0 = bF1 = NULL;
        if ( LevelF < iLev1 )
        {
            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
            assert( bRes0 != z0 );
            if ( bRes0 == b0 )
                bRes = b0;
            else
                bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars );
            assert( bRes != z0 );
        }
        else if ( LevelF == iLev1 )
        {
            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) );
            if ( bRes0 == b0 )
                bRes = b0;
            else
            {
                bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) );
                if ( bRes1 == b0 )
                    bRes = b0;
                else
                {
                    if ( bRes0 == z0 || bRes1 == z0 )
                        bRes = b1;
                    else
                        bRes = b0;
                }
            }
        }
        else if ( LevelF < iLev2 )
        {
            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
            if ( bRes0 == b0 )
                bRes = b0;
            else
            {
                bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars );
                if ( bRes1 == b0 )
                    bRes = b0;
                else
                {
                    if ( bRes0 == z0 || bRes1 == z0 )
                        bRes = z0;
                    else
                        bRes = b1;
                }
            }
        }
        else if ( LevelF == iLev2 )
        {
            if ( fVar1Pres )
                bRes = z0;
            else 
                bRes = b0;
        }
        else 
        {
            bRes = b1;
        }
        cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes);
        return bRes;
    }
}
DdNode * extraBddCheckVarsSymmetric ( DdManager * dd , DdNode * bF , DdNode * bVars ) { DdNode * bRes ; if ( bF == b0 ) return b1 ; assert ( bVars != b1 ) ; if ( ( bRes = cuddCacheLookup2 ( dd , extraBddCheckVarsSymmetric , bF , bVars ) ) ) return bRes ; else { DdNode * bRes0 , * bRes1 ; DdNode * bF0 , * bF1 ; DdNode * bFR = Cudd_Regular ( bF ) ; int LevelF = cuddI ( dd , bFR -> index ) ; DdNode * bVarsR = Cudd_Regular ( bVars ) ; int fVar1Pres ; int iLev1 ; int iLev2 ; if ( bVarsR != bVars ) { assert ( cuddT ( bVarsR ) == b1 ) ; fVar1Pres = 1 ; iLev1 = -1 ; iLev2 = dd -> perm [ bVarsR -> index ] ; } else { fVar1Pres = 0 ; if ( cuddT ( bVars ) == b1 ) { iLev1 = -1 ; iLev2 = dd -> perm [ bVars -> index ] ; } else { assert ( cuddT ( cuddT ( bVars ) ) == b1 ) ; iLev1 = dd -> perm [ bVars -> index ] ; iLev2 = dd -> perm [ cuddT ( bVars ) -> index ] ; } } if ( LevelF < iLev2 ) { if ( bFR != bF ) { bF0 = Cudd_Not ( cuddE ( bFR ) ) ; bF1 = Cudd_Not ( cuddT ( bFR ) ) ; } else { bF0 = cuddE ( bFR ) ; bF1 = cuddT ( bFR ) ; } } else bF0 = bF1 = NULL ; if ( LevelF < iLev1 ) { bRes0 = extraBddCheckVarsSymmetric ( dd , bF0 , bVars ) ; assert ( bRes0 != z0 ) ; if ( bRes0 == b0 ) bRes = b0 ; else bRes = extraBddCheckVarsSymmetric ( dd , bF1 , bVars ) ; assert ( bRes != z0 ) ; } else if ( LevelF == iLev1 ) { bRes0 = extraBddCheckVarsSymmetric ( dd , bF0 , Cudd_Not ( cuddT ( bVars ) ) ) ; if ( bRes0 == b0 ) bRes = b0 ; else { bRes1 = extraBddCheckVarsSymmetric ( dd , bF1 , Cudd_Not ( cuddT ( bVars ) ) ) ; if ( bRes1 == b0 ) bRes = b0 ; else { if ( bRes0 == z0 || bRes1 == z0 ) bRes = b1 ; else bRes = b0 ; } } } else if ( LevelF < iLev2 ) { bRes0 = extraBddCheckVarsSymmetric ( dd , bF0 , bVars ) ; if ( bRes0 == b0 ) bRes = b0 ; else { bRes1 = extraBddCheckVarsSymmetric ( dd , bF1 , bVars ) ; if ( bRes1 == b0 ) bRes = b0 ; else { if ( bRes0 == z0 || bRes1 == z0 ) bRes = z0 ; else bRes = b1 ; } } } else if ( LevelF == iLev2 ) { if ( fVar1Pres ) bRes = z0 ; else bRes = b0 ; } else { bRes = b1 ; } cuddCacheInsert2 ( dd , extraBddCheckVarsSymmetric , bF , bVars , bRes ) ; return bRes ; } }
Function
Synopsis    [Performs the recursive step of Extra_bddCheckVarsSymmetric().]
Function Synopsis [ Performs the recursive step of Extra_bddCheckVarsSymmetric () . ]
/* the DD manager */ // cube's pointer is complemented // the first var is present on the path // we are already below the first var level // the level of the second var // cube's pointer is NOT complemented // the first var is absent on the path // we are already below the first var level  // the level of the second var // the level of the first var  // the level of the second var // cofactor the function // the cofactors are needed only if we are above the second level // bFunc is complemented  // consider five cases: // (1) F is above iLev1 // (2) F is on the level iLev1 // (3) F is between iLev1 and iLev2 // (4) F is on the level iLev2 // (5) F is below iLev2 // (1) F is above iLev1 // the returned result cannot have the hash attribute // because we still did not reach the level of Var1; // the attribute never travels above the level of Var1 //          assert( !Hash_IsComplement( bRes0 ) ); //          assert( !Hash_IsComplement( bRes ) ); // (2) F is on the level iLev1 //                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) ) // (3) F is between iLev1 and iLev2 //                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) ) //                      bRes = Hash_Not( b1 ); // (4) F is on the level iLev2 // this is the only place where the hash attribute (Hash_Not) can be added  // to the result; it can be added only if the path came through the node // lebeled with Var1; therefore, the hash attribute cannot be returned // to the caller function //              bRes = Hash_Not( b1 ); // (5) F is below iLev2 // if ( LevelF > iLev2 ) // it is possible that the path goes through the node labeled by Var1 // and still everything is okay; we do not label with Hash_Not here // because the path does not go through node labeled by Var2