Towards better Boolean matching.

3 files changed, 646 insertions, 1 deletions

diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index dc34a22a..7ffe63be 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -1900,7 +1900,9 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteT
 void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit )
 {
     char pRes[DAU_MAX_STR];
-    Dau_DsdDecompose( pTruth, nVarsInit, 0, 1, pRes );
+    word pTemp[DAU_MAX_WORD];
+    Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
+    Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
     fprintf( pFile, "%s\n", pRes );
 }
 
diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c
new file mode 100644
index 00000000..65821027
--- /dev/null
+++ b/src/opt/dau/dauNonDsd.c
@@ -0,0 +1,642 @@
+/**CFile****************************************************************
+
+  FileName    [dauNonDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware unmapping.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: dauNonDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dauInt.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the bit count for the first 256 integer numbers
+static int BitCount8[256] = {
+    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+static inline BitCount16( int i ) { return BitCount8[i & 0xFF] + BitCount8[i >> 8]; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Checks decomposability with given BS variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Dau_DecGetMinterm( word * p, int g, int nVarsS, int uMaskAll )
+{
+    int m, c, v;
+    for ( m = c = v = 0; v < nVarsS; v++ )
+        if ( !((uMaskAll >> v) & 1) ) // not shared bound set variable
+        {
+            if ( (g >> v) & 1 )
+                m |= (1 << c);
+            c++;
+        }
+    assert( c >= 2 );
+    p[m>>6] |= (((word)1)<<(m & 63));                               
+}
+static inline int Dau_DecCheckSet5( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
+{
+    int fFound0 = 0, fFound1 = 0;
+    int g, gMax = (1 << (nVars - nVarsF));
+    int Shift = 6 - nVarsF, Mask = (1 << Shift) - 1;
+    word Mask2 = (((word)1) << (1 << nVarsF)) - 1;
+    word Cof0 = 0, Cof1 = 0, Value;
+    assert( nVarsF >= 1 && nVarsF <= 5 );
+    if ( pDec ) *pDec = 0;
+    for ( g = 0; g < gMax; g++ )
+        if ( (g & uMaskAll) == uMaskValue ) // this minterm g matches shared variable minterm uMaskValue
+        {
+            Value = (p[g>>Shift] >> ((g&Mask)<<nVarsF)) & Mask2;
+            if ( !fFound0 )
+                Cof0 = Value, fFound0 = 1;
+            else if ( Cof0 == Value )
+                continue;
+            else if ( !fFound1 )
+            {
+                Cof1 = Value, fFound1 = 1;
+                if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+            }
+            else if ( Cof1 == Value )
+            {
+                if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+                continue;
+            }
+            else
+                return 0;            
+        }
+    if ( pCof0 )
+    {
+        assert( fFound0 );
+        Cof1 = fFound1 ? Cof1 : Cof0;
+        *pCof0 = Abc_Tt6Stretch( Cof0, nVarsF );
+        *pCof1 = Abc_Tt6Stretch( Cof1, nVarsF );
+    }
+    return 1;
+}
+static inline int Dau_DecCheckSet6( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
+{
+    int fFound0 = 0, fFound1 = 0;
+    int g, gMax = (1 << (nVars - nVarsF));
+    int nWords = Abc_TtWordNum(nVarsF);
+    word * Cof0 = NULL, * Cof1 = NULL;
+    assert( nVarsF >= 6 && nVarsF <= nVars - 2 );
+    if ( pDec ) *pDec = 0;
+    for ( g = 0; g < gMax; g++ )
+        if ( (g & uMaskAll) == uMaskValue )
+        {
+            if ( !fFound0 )
+                Cof0 = p + g * nWords, fFound0 = 1;
+            else if ( !memcmp(Cof0, p + g * nWords, sizeof(word) * nWords) )
+                continue;
+            else if ( !fFound1 )
+            {
+                Cof1 = p + g * nWords, fFound1 = 1;
+                if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+            }
+            else if ( !memcmp(Cof1, p + g * nWords, sizeof(word) * nWords) )
+            {
+                if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
+                continue;
+            }
+            else
+                return 0;            
+        }
+    if ( pCof0 )
+    {
+        assert( fFound0 );
+        Cof1 = fFound1 ? Cof1 : Cof0;
+        memcpy( pCof0, Cof0, sizeof(word) * nWords );
+        memcpy( pCof1, Cof1, sizeof(word) * nWords );
+    }
+    return 1;
+}
+static inline int Dau_DecCheckSetAny( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
+{
+    assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
+    if ( nVarsF < 6 )
+        return Dau_DecCheckSet5( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
+    else
+        return Dau_DecCheckSet6( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
+}
+int Dau_DecCheckSetTop( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word ** pCof0, word ** pCof1, word ** pDec )
+{
+    int i, pVarsS[16];
+    int v, m, mMax = (1 << nVarsS), uMaskValue;
+    assert( nVars >= 3 && nVars <= 16 );
+    assert( nVars == nVarsF + nVarsB );
+    assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
+    assert( nVarsB >= 2 && nVarsB <= nVars - 1 );
+    assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 );
+    if ( nVarsS == 0 )
+        return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 );
+    // collect shared variables
+    assert( maskS > 0 && maskS < (1 << nVarsB) );
+    for ( i = 0, v = 0; v < nVarsB; v++ )
+        if ( (maskS >> v) & 1 )
+            pVarsS[i++] = v;
+    assert( i == nVarsS );
+    // go through shared set minterms
+    for ( m = 0; m < mMax; m++ )
+    {
+        // generate share set mask
+        uMaskValue = 0;
+        for ( v = 0; v < nVarsS; v++ )
+            if ( (m >> v) & 1 )
+                uMaskValue |= (1 << pVarsS[v]);
+        assert( (maskS & uMaskValue) == uMaskValue );
+        // check decomposition
+        if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) )
+            return 0;
+    }
+   return 1;
+}
+ 
+
+/**Function*************************************************************
+
+  Synopsis    [Variable sets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Dau_DecCreateSet( int * pVarsB, int sizeB, int maskS )
+{
+    unsigned uSet = 0; int v;
+    for ( v = 0; v < sizeB; v++ )
+    {
+        uSet |= (1 <<  (pVarsB[v] << 1));
+        if ( (maskS >> v) & 1 )
+        uSet |= (1 << ((pVarsB[v] << 1)+1));
+    }
+    return uSet;
+}
+static inline int Dau_DecSetHas01( unsigned Mask )
+{
+    return (Mask & ((~Mask) >> 1) & 0x55555555);
+}
+static inline int Dau_DecSetIsContained( Vec_Int_t * vSets, unsigned New )
+// Old=abcD contains New=abcDE
+// Old=abcD contains New=abCD
+{
+    unsigned Old;
+    int i, Entry;
+    Vec_IntForEachEntry( vSets, Entry, i )
+    {
+        Old = (unsigned)Entry;
+        if ( (Old & ~New) == 0 && !Dau_DecSetHas01(~Old & New))
+            return 1;
+    }
+    return 0;
+}
+void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine )
+{
+    int v, Counter = 0;
+    int nUnique = 0, nShared = 0, nFree = 0;
+    for ( v = 0; v < nVars; v++ )
+    {
+        int Value = ((set >> (v << 1)) & 3);
+        if ( Value == 1 )
+            nUnique++;
+        else if ( Value == 3 )
+            nShared++;
+        else if ( Value == 0 )
+            nFree++;
+        else assert( 0 );
+    }
+    printf( "S =%2d  D =%2d  C =%2d   ", nShared, nUnique+nShared, nShared+nFree+1 );
+
+    printf( "x=" );
+    for ( v = 0; v < nVars; v++ )
+    {
+        int Value = ((set >> (v << 1)) & 3);
+        if ( Value == 1 )
+            printf( "%c", 'a' + v ), Counter++;
+        else if ( Value == 3 )
+            printf( "%c", 'A' + v ), Counter++;
+        else assert( Value == 0 );
+    }
+    printf( " y=x" );
+    for ( v = 0; v < nVars; v++ )
+    {
+        int Value = ((set >> (v << 1)) & 3);
+        if ( Value == 0 )
+            printf( "%c", 'a' + v ), Counter++;
+        else if ( Value == 3 )
+            printf( "%c", 'A' + v ), Counter++;
+    }
+    for ( ; Counter < 15; Counter++ )
+        printf( " " );
+    if ( fNewLine )
+        printf( "\n" );
+}
+unsigned Dau_DecReadSet( char * pStr )
+{
+    unsigned uSet = 0; int v;
+    for ( v = 0; pStr[v]; v++ )
+    {
+        if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
+            uSet |= (1 << ((pStr[v] - 'a') << 1));
+        else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' )
+            uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1));
+        else break;
+    }
+    return uSet;
+}
+void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars )
+{
+    int i, Entry;
+    printf( "The set contains %d entries:\n", Vec_IntSize(vSets) );
+    Vec_IntForEachEntry( vSets, Entry, i )
+        Dau_DecPrintSet( (unsigned)Entry, nVars, 1 );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find decomposable bound-sets of the given function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB, int sizeB )
+{
+    int v, c = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( !((maskB >> v) & 1) )
+            Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
+    assert( c == nVars - sizeB );
+}
+Vec_Int_t * Dau_DecFindSets( word * p, int nVars )
+{
+    Vec_Int_t * vSets = Vec_IntAlloc( 32 );
+    int V2P[16], P2V[16], pVarsB[16];
+    int Limit = (1 << nVars);
+    int c, v, sizeB, sizeS, maskB, maskS;
+    unsigned setMixed;
+    for ( v = 0; v < nVars; v++ )
+        assert( Abc_TtHasVar( p, nVars, v ) );
+    // initialize permutation
+    for ( v = 0; v < nVars; v++ )
+        V2P[v] = P2V[v] = v;
+    // iterate through bound sets of each size in increasing order
+    for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size
+    for ( maskB = 0; maskB < Limit; maskB++ ) // bound set
+    if ( BitCount16(maskB) == sizeB )
+    {
+        // permute variables to have bound set on top
+        Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB );
+        // collect bound set vars on levels nVars-sizeB to nVars-1
+        for ( c = 0; c < sizeB; c++ )
+            pVarsB[c] = P2V[nVars-sizeB+c];
+        // check disjoint
+        if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) )
+        {
+            Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) );
+            continue;
+        }
+        if ( sizeB == 2 )
+            continue;
+        // iterate through shared sets of each size in the increasing order
+        for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ )   // shared set size
+//        sizeS = 1; 
+        for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set
+        if ( BitCount16(maskS) == sizeS )
+        {
+            setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS );
+//            printf( "Considering %10d ", setMixed );
+//            Dau_DecPrintSet( setMixed, nVars );
+            // check if it exists
+            if ( Dau_DecSetIsContained(vSets, setMixed) )
+                continue;
+            // check if it can be added
+            if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) )
+                Vec_IntPush( vSets, setMixed );
+        }
+    }
+    return vSets;
+}
+void Dau_DecFindSetsTest2()
+{
+    Vec_Int_t * vSets;
+    word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
+    word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
+    word t  = (~s_Truths6[0] & a0)           | (s_Truths6[0] & a1); 
+//    word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
+//    word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
+//    word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
+//    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
+//    word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
+    int nVars = 5;
+
+    vSets   = Dau_DecFindSets( &t, nVars );
+    Dau_DecPrintSets( vSets, nVars );
+    Vec_IntFree( vSets );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces variables in the string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dau_DecVarReplace( char * pStr, int * pPerm, int nVars )
+{
+    int v;
+    for ( v = 0; pStr[v]; v++ )
+        if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
+        {
+            assert( pStr[v] - 'a' < nVars );
+            pStr[v] = 'a' + pPerm[pStr[v] - 'a'];
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes with the given bound-set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DecDecomposeSet( word * pInit, int nVars, unsigned uSet, word * pComp, word * pDec, int * pPermC, int * pPermD, int * pnVarsC, int * pnVarsD )
+{
+    word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64];
+    word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD;
+    int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16];
+    int nVarsU = 0, nVarsS = 0, nVarsF = 0;
+    int nWords = Abc_TtWordNum(nVars);
+    int v, d, c, Status, nDecs;
+    assert( nVars <= 16 );
+    for ( v = 0; v < nVars; v++ )
+        V2P[v] = P2V[v] = v;
+    memcpy( p, pInit, sizeof(word) * nWords );
+    // sort variables
+    for ( v = 0; v < nVars; v++ )
+    {
+        int Value = (uSet >> (v<<1)) & 3;
+        if ( Value == 0 )
+            pVarsF[nVarsF++] = v;
+        else if ( Value == 1 )
+            pVarsU[nVarsU++] = v;
+        else if ( Value == 3 )
+            pVarsS[nVarsS++] = v;
+        else assert(0);
+    }
+    assert( nVarsS >= 0 && nVarsS <= 6 );
+    assert( nVarsF + nVarsS + 1 <= 6 );
+    assert( nVarsU + nVarsS <= 6 );
+    // init space for decomposition functions
+    nDecs = (1 << nVarsS);
+    for ( d = 0; d < nDecs; d++ )
+    {
+        pCof0[d] = Cof0 + d;
+        pCof1[d] = Cof1 + d;
+        pDecs[d] = Decs + d;
+    }
+    // permute variables
+    c = 0;
+    for ( v = 0; v < nVarsF; v++ )
+       Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ );
+    for ( v = 0; v < nVarsS; v++ )
+       Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ );
+    for ( v = 0; v < nVarsU; v++ )
+       Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ );
+    assert( c == nVars );
+    // check decomposition
+    Status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs );
+    if ( !Status )
+        return 0;
+    // compute cofactors
+    assert( nVarsF + nVarsS < 6 );
+    for ( d = 0; d < nDecs; d++ )
+    {
+        Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]);
+        pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU );
+    }
+    // compute the resulting functions
+    pComp[0] = 0;
+    pDec[0] = 0;
+    for ( d = 0; d < nDecs; d++ )
+    {
+        // compute minterms for composition/decomposition function
+        MintC = MintD = ~((word)0);
+        for ( v = 0; v < nVarsS; v++ )
+        {
+            MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
+            MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
+        }
+        // derive functions
+        pComp[0] |= MintC & Cof[d];
+        pDec[0] |= MintD & pDecs[d][0];
+    }
+    // derive variable permutations
+    if ( pPermC )
+    {
+        for ( v = 0; v < nVarsF; v++ )
+            pPermC[v] = pVarsF[v];
+        for ( v = 0; v < nVarsS; v++ )
+            pPermC[nVarsF+v] = pVarsS[v];
+        pPermC[nVarsF + nVarsS] = nVars;
+    }
+    if ( pPermD )
+    {
+        for ( v = 0; v < nVarsU; v++ )
+            pPermD[v] = pVarsU[v];
+        for ( v = 0; v < nVarsS; v++ )
+            pPermD[nVarsU+v] = pVarsS[v];
+    }
+    if ( pnVarsC )
+        *pnVarsC = nVarsF + nVarsS + 1;
+    if ( pnVarsD )
+        *pnVarsD = nVarsU + nVarsS;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD )
+{
+    word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16
+    int nWordsC = Abc_TtWordNum(nVars+1);
+    int nWordsD = Abc_TtWordNum(nVars);
+    assert( nVars < 16 );
+    memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC );
+    memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD );
+//    Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" );
+//    Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" );
+    if ( nVars >= 6 )
+    {
+        assert( nWordsD >= 1 );
+        assert( nWordsC > 1 );
+        Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD );
+    }
+    else
+    {
+        word pC0 = Abc_Tt6Stretch( pC[0], nVars );
+        word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars );
+        Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD );
+    }
+    if ( Abc_TtEqual(pInit, pRes, nWordsD) )
+        printf( "      Verification successful\n" );
+    else
+        printf( "      Verification failed\n" );
+    return 1;
+}
+int Dau_DecPerform( word * p, int nVars, unsigned uSet )
+{
+    word tComp = 0, tDec = 0;
+    char pDsdC[1000], pDsdD[1000];
+    int pPermC[16], pPermD[16], nVarsC, nVarsD;
+    int status, ResC, ResD;
+    status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec, pPermC, pPermD, &nVarsC, &nVarsD );
+//    Dau_DecPrintSet( uSet, nVars );    
+//    printf( "Decomposition %s\n", status ? "exists" : "does not exist" );
+    if ( !status )
+    {
+        printf( "  Decomposition does not exist\n" );
+        return 0;
+    }
+//    Dau_DsdPrintFromTruth( stdout, p, nVars );     //printf( "\n" );
+//    Dau_DsdPrintFromTruth( stdout, &tComp, nVars ); //printf( "\n" );
+//    Dau_DsdPrintFromTruth( stdout, &tDec, nVars );  //printf( "\n" );
+    // decompose
+    ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC );
+    ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD );
+/*
+    printf( "%s\n", pDsdC );
+    printf( "%s\n", pDsdD );
+    for ( v = 0; v < nVarsC; v++ )
+        printf( "%d ", pPermC[v] );
+    printf( "\n" );
+    for ( v = 0; v < nVarsD; v++ )
+        printf( "%d ", pPermD[v] );
+    printf( "\n" );
+*/
+    // replace variables
+    Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
+    Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
+    printf( "%24s  ", pDsdD );
+    printf( "%24s  ", pDsdC );
+    Dau_DecVerify( p, nVars, pDsdC, pDsdD );
+    return 1;
+}
+void Dau_DecTrySets( word * p, int nVars )
+{
+    Vec_Int_t * vSets;
+    word t0 = *p;
+    int i, Entry;
+    vSets = Dau_DecFindSets( p, nVars );
+    Dau_DsdPrintFromTruth( stdout, &t0, nVars ); 
+    printf( "There are %d support-reducing decompositions:\n", Vec_IntSize(vSets) );
+    Vec_IntForEachEntry( vSets, Entry, i )
+    {
+        unsigned uSet = (unsigned)Entry;
+        Dau_DecPrintSet( uSet, nVars, 0 );
+        Dau_DecPerform( &t0, nVars, uSet );
+    }
+//    printf( "\n" );
+    Vec_IntFree( vSets );
+}
+
+void Dau_DecFindSetsTest3()
+{
+    word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
+    word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
+    word t  = (~s_Truths6[0] & a0)           | (s_Truths6[0] & a1); 
+//    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
+    int nVars = 6;
+    char * pStr = "Bcd";
+//    char * pStr = "Abcd";
+//    char * pStr = "ab";
+    unsigned uSet = Dau_DecReadSet( pStr );
+    Dau_DecPerform( &t, nVars, uSet );
+}
+
+void Dau_DecFindSetsTest()
+{
+    int nVars = 6;
+//    word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
+//    word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
+//    word t  = (~s_Truths6[0] & a0)           | (s_Truths6[0] & a1); 
+//    word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
+//    word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
+//    word t = ABC_CONST(0x00000000901FFFFF); // some funct
+    word t = ABC_CONST(0x000030F00D0D3FFF); // some funct
+//    word t = ABC_CONST(0x00000000690006FF); // some funct
+//    word t = ABC_CONST(0x7000F80007FF0FFF); // some funct
+//    word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var
+//    word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
+//    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
+//    word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
+    Dau_DecTrySets( &t, nVars );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make
index f339810b..190e30e4 100644
--- a/src/opt/dau/module.make
+++ b/src/opt/dau/module.make
@@ -5,4 +5,5 @@ SRC +=    src/opt/dau/dauCanon.c \
     src/opt/dau/dauEnum.c \
     src/opt/dau/dauGia.c \
     src/opt/dau/dauMerge.c \
+    src/opt/dau/dauNonDsd.c \
     src/opt/dau/dauTree.c