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_DsdDecomposeDoubleVarsOne( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars, int v, int u )
{
    char pBuffer[10] = { 0 }; 
    int nWords = Abc_TtWordNum(nVars);
    int Status = Dau_DsdFindSupportOne( p, pTruth, pVars, nVars, v, u );
    assert( v > u );
    if ( Status == 3 )
    {
        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) && Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 2) ) 
        {
            word pTtTemp[2][DAU_MAX_WORD];
            sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
            Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
            Abc_TtCofactor0( pTtTemp[0], nWords, u );
            Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
            Abc_TtCofactor1( pTtTemp[1], nWords, u );
            Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
            goto finish;
        }
    }
    else if ( Status == 2 )
    {
        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 2) ) 
        {
            word pTtTemp[2][DAU_MAX_WORD];
            sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
            Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
            Abc_TtCofactor0( pTtTemp[0], nWords, u );
            Abc_TtCofactor1p( pTtTemp[1], pTruth, nWords, v );
            Abc_TtCofactor1( pTtTemp[1], nWords, u );
            Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
            goto finish;
        }
        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) 
        {
            word pTtTemp[2][DAU_MAX_WORD];
            sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
            Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
            Abc_TtCofactor0( pTtTemp[0], nWords, u );
            Abc_TtCofactor1p( pTtTemp[1], pTruth, nWords, v );
            Abc_TtCofactor0( pTtTemp[1], nWords, u );
            Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
            goto finish;
        }
    }
    else if ( Status == 1 )
    {
        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) 
        {
            word pTtTemp[2][DAU_MAX_WORD];
            sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
            Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
            Abc_TtCofactor0( pTtTemp[0], nWords, u );
            Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
            Abc_TtCofactor1( pTtTemp[1], nWords, u );
            Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
            goto finish;
        }
        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 3) ) 
        {
            word pTtTemp[2][DAU_MAX_WORD];
            sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
            Abc_TtCofactor1p( pTtTemp[0], pTruth, nWords, v );
            Abc_TtCofactor1( pTtTemp[0], nWords, u );
            Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
            Abc_TtCofactor0( pTtTemp[1], nWords, u );
            Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
            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_DsdDecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) )
        nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, --nVars );
    return nVars;
}
static inline int Dau_DsdDecomposeDoubleVarsOne ( Dau_Dsd_t * p , word * pTruth , int * pVars , int nVars , int v , int u ) { char pBuffer [ 10 ] = { 0 } ; int nWords = Abc_TtWordNum ( nVars ) ; int Status = Dau_DsdFindSupportOne ( p , pTruth , pVars , nVars , v , u ) ; assert ( v > u ) ; if ( Status == 3 ) { if ( Abc_TtCheckEqualCofs ( pTruth , nWords , u , v , 0 , 3 ) && Abc_TtCheckEqualCofs ( pTruth , nWords , u , v , 1 , 2 ) ) { word pTtTemp [ 2 ] [ DAU_MAX_WORD ] ; sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; Abc_TtCofactor0p ( pTtTemp [ 0 ] , pTruth , nWords , v ) ; Abc_TtCofactor0 ( pTtTemp [ 0 ] , nWords , u ) ; Abc_TtCofactor0p ( pTtTemp [ 1 ] , pTruth , nWords , v ) ; Abc_TtCofactor1 ( pTtTemp [ 1 ] , nWords , u ) ; Abc_TtMux ( pTruth , Dau_DsdTtElems ( ) [ u ] , pTtTemp [ 1 ] , pTtTemp [ 0 ] , nWords ) ; goto finish ; } } else if ( Status == 2 ) { if ( Abc_TtCheckEqualCofs ( pTruth , nWords , u , v , 0 , 2 ) ) { word pTtTemp [ 2 ] [ DAU_MAX_WORD ] ; sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; Abc_TtCofactor0p ( pTtTemp [ 0 ] , pTruth , nWords , v ) ; Abc_TtCofactor0 ( pTtTemp [ 0 ] , nWords , u ) ; Abc_TtCofactor1p ( pTtTemp [ 1 ] , pTruth , nWords , v ) ; Abc_TtCofactor1 ( pTtTemp [ 1 ] , nWords , u ) ; Abc_TtMux ( pTruth , Dau_DsdTtElems ( ) [ u ] , pTtTemp [ 1 ] , pTtTemp [ 0 ] , nWords ) ; goto finish ; } if ( Abc_TtCheckEqualCofs ( pTruth , nWords , u , v , 0 , 3 ) ) { word pTtTemp [ 2 ] [ DAU_MAX_WORD ] ; sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; Abc_TtCofactor0p ( pTtTemp [ 0 ] , pTruth , nWords , v ) ; Abc_TtCofactor0 ( pTtTemp [ 0 ] , nWords , u ) ; Abc_TtCofactor1p ( pTtTemp [ 1 ] , pTruth , nWords , v ) ; Abc_TtCofactor0 ( pTtTemp [ 1 ] , nWords , u ) ; Abc_TtMux ( pTruth , Dau_DsdTtElems ( ) [ u ] , pTtTemp [ 1 ] , pTtTemp [ 0 ] , nWords ) ; goto finish ; } } else if ( Status == 1 ) { if ( Abc_TtCheckEqualCofs ( pTruth , nWords , u , v , 0 , 3 ) ) { word pTtTemp [ 2 ] [ DAU_MAX_WORD ] ; sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; Abc_TtCofactor0p ( pTtTemp [ 0 ] , pTruth , nWords , v ) ; Abc_TtCofactor0 ( pTtTemp [ 0 ] , nWords , u ) ; Abc_TtCofactor0p ( pTtTemp [ 1 ] , pTruth , nWords , v ) ; Abc_TtCofactor1 ( pTtTemp [ 1 ] , nWords , u ) ; Abc_TtMux ( pTruth , Dau_DsdTtElems ( ) [ u ] , pTtTemp [ 1 ] , pTtTemp [ 0 ] , nWords ) ; goto finish ; } if ( Abc_TtCheckEqualCofs ( pTruth , nWords , u , v , 1 , 3 ) ) { word pTtTemp [ 2 ] [ DAU_MAX_WORD ] ; sprintf ( pBuffer , " " , ' ' + pVars [ v ] , ' ' + pVars [ u ] ) ; Abc_TtCofactor1p ( pTtTemp [ 0 ] , pTruth , nWords , v ) ; Abc_TtCofactor1 ( pTtTemp [ 0 ] , nWords , u ) ; Abc_TtCofactor0p ( pTtTemp [ 1 ] , pTruth , nWords , v ) ; Abc_TtCofactor0 ( pTtTemp [ 1 ] , nWords , u ) ; Abc_TtMux ( pTruth , Dau_DsdTtElems ( ) [ u ] , pTtTemp [ 1 ] , pTtTemp [ 0 ] , nWords ) ; 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_DsdDecomposeSingleVarOne ( p , pTruth , pVars , -- nVars , u ) ) nVars = Dau_DsdDecomposeSingleVar ( 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]] ); // both F(v=0) and F(v=1) depend on u //        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u // 00=11 01=10 v+u //            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); // F(v=0) does not depend on u; F(v=1) depends on u //        if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu // 00=10 vu //            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); //        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u // 00=11 v!u //            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); // F(v=0) depends on u; F(v=1) does not depend on u //        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu // 00=11 !vu //            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); //        if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u // 01=11 !v!u //            pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)); // finalize decomposition