abc/src/opt/dau/dauDsd.c
// checks decomposability with respect to the pair (v, u)
checks decomposability with respect to the pair (v, u)
checks decomposability with respect to the pair ( v u )
static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars, int v, int u )
{
    char pBuffer[10] = { 0 }; 
    word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
    word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
    int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u );
    assert( v > u );
    if ( Status == 3 )
    {
        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) 
        {
            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
            sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
            goto finish;
        }
    }
    else if ( Status == 2 )
    {
        if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) 
        {
            sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
            goto finish;
        }
        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) 
        {
            sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
            goto finish;
        }
    }
    else if ( Status == 1 )
    {
        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) 
        {
            sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
            goto finish;
        }
        if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) 
        {
            sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u));
            goto finish;
        }
    }
    return nVars;
finish: 
    assert( pBuffer[0] );
    pVars[u] = Dau_DsdAddVarDef( p, pBuffer );
    pVars[v] = pVars[nVars-1];
    Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
    if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) )
        nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars );
    return nVars;
}
static inline int Dau_Dsd6DecomposeDoubleVarsOne ( Dau_Dsd_t * p , word * pTruth , int * pVars , int nVars , int v , int u ) { char pBuffer [ 10 ] = { 0 } ; word tCof0 = Abc_Tt6Cofactor0 ( pTruth [ 0 ] , v ) ; word tCof1 = Abc_Tt6Cofactor1 ( pTruth [ 0 ] , v ) ; int Status = Dau_Dsd6FindSupportOne ( p , tCof0 , tCof1 , pVars , nVars , v , u ) ; assert ( v > u ) ; if ( Status == 3 ) { if ( Abc_Tt6Cof0EqualCof1 ( tCof0 , tCof1 , u ) && Abc_Tt6Cof0EqualCof1 ( tCof1 , tCof0 , u ) ) { pTruth [ 0 ] = ( s_Truths6 [ u ] & Abc_Tt6Cofactor1 ( tCof0 , u ) ) | ( ~ s_Truths6 [ u ] & Abc_Tt6Cofactor0 ( tCof0 , u ) ) ; sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; goto finish ; } } else if ( Status == 2 ) { if ( Abc_Tt6Cof0EqualCof0 ( tCof0 , tCof1 , u ) ) { sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; pTruth [ 0 ] = ( s_Truths6 [ u ] & Abc_Tt6Cofactor1 ( tCof1 , u ) ) | ( ~ s_Truths6 [ u ] & Abc_Tt6Cofactor0 ( tCof0 , u ) ) ; goto finish ; } if ( Abc_Tt6Cof0EqualCof1 ( tCof0 , tCof1 , u ) ) { sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; pTruth [ 0 ] = ( s_Truths6 [ u ] & Abc_Tt6Cofactor0 ( tCof1 , u ) ) | ( ~ s_Truths6 [ u ] & Abc_Tt6Cofactor0 ( tCof0 , u ) ) ; goto finish ; } } else if ( Status == 1 ) { if ( Abc_Tt6Cof0EqualCof1 ( tCof0 , tCof1 , u ) ) { sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; pTruth [ 0 ] = ( s_Truths6 [ u ] & Abc_Tt6Cofactor1 ( tCof0 , u ) ) | ( ~ s_Truths6 [ u ] & Abc_Tt6Cofactor0 ( tCof0 , u ) ) ; goto finish ; } if ( Abc_Tt6Cof1EqualCof1 ( tCof0 , tCof1 , u ) ) { sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; pTruth [ 0 ] = ( s_Truths6 [ u ] & Abc_Tt6Cofactor0 ( tCof0 , u ) ) | ( ~ s_Truths6 [ u ] & Abc_Tt6Cofactor1 ( tCof1 , u ) ) ; goto finish ; } } return nVars ; finish : assert ( pBuffer [ 0 ] ) ; pVars [ u ] = Dau_DsdAddVarDef ( p , pBuffer ) ; pVars [ v ] = pVars [ nVars - 1 ] ; Abc_TtSwapVars ( pTruth , nVars , v , nVars - 1 ) ; if ( Dau_Dsd6DecomposeSingleVarOne ( p , pTruth , pVars , -- nVars , u ) ) nVars = Dau_Dsd6DecomposeSingleVar ( p , pTruth , pVars , -- nVars ) ; return nVars ; }
checks decomposability with respect to the pair (v, u)
checks decomposability with respect to the pair ( v u )
//printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] ); //    Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" ); // both F(v=0) and F(v=1) depend on u // v+u // F(v=0) does not depend on u; F(v=1) depends on u // vu // v!u // F(v=0) depends on u; F(v=1) does not depend on u // !vu // !v!u // finalize decomposition