Improved DSD.

5 files changed, 594 insertions, 119 deletions

diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 94b4ef07..61d71dfb 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -24,6 +24,7 @@
 #include "bool/bdc/bdc.h"
 #include "bool/dec/dec.h"
 #include "bool/kit/kit.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -541,20 +542,15 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
     }
     else if ( DecType == 4 )
     {
-//        extern void Dau_DsdTestOne( word t, int i );
-        if ( p->nVars != 6 )
-        {
-            printf( "Currently only works for 6 variables.\n" );
-            return;
-        }
-        // perform disjoint-support decomposition and count AIG nodes
-        // (non-DSD blocks are decomposed into 2:1 MUXes, each counting as 3 AIG nodes)
-        assert( p->nVars == 6 );
+        char pDsd[DAU_MAX_STR];
         for ( i = 0; i < p->nFuncs; i++ )
         {
             if ( fVerbose )
                 printf( "%7d :      ", i );
-//            Dau_DsdTestOne( *p->pFuncs[i], i );
+            Dau_DsdDecompose( p->pFuncs[i], p->nVars, 0, pDsd );
+            if ( fVerbose )
+                printf( "%s\n", pDsd );
+            nNodes += Dau_DsdCountAnds( pDsd );
         }
     }
     else assert( 0 );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 9281d6f8..eaaa7d2f 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -234,7 +234,6 @@ static inline void Abc_TtElemInit( word ** pTtElems, int nVars )
                 pTtElems[i][k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -257,6 +256,50 @@ static inline word Abc_Tt6Cofactor1( word t, int iVar )
     return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
 }
 
+static inline void Abc_TtCofactor0p( word * pOut, word * pIn, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+        pOut[0] = ((pIn[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pIn[0] & s_Truths6Neg[iVar]);
+    else if ( iVar <= 5 )
+    {
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+            pOut[w] = ((pIn[w] & s_Truths6Neg[iVar]) << shift) | (pIn[w] & s_Truths6Neg[iVar]);
+    }
+    else // if ( iVar > 5 )
+    {
+        word * pLimit = pIn + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
+            for ( i = 0; i < iStep; i++ )
+            {
+                pOut[i]         = pIn[i];
+                pOut[i + iStep] = pIn[i];
+            }
+    }    
+}
+static inline void Abc_TtCofactor1p( word * pOut, word * pIn, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+        pOut[0] = (pIn[0] & s_Truths6[iVar]) | ((pIn[0] & s_Truths6[iVar]) >> (1 << iVar));
+    else if ( iVar <= 5 )
+    {
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+            pOut[w] = (pIn[w] & s_Truths6[iVar]) | ((pIn[w] & s_Truths6[iVar]) >> shift);
+    }
+    else // if ( iVar > 5 )
+    {
+        word * pLimit = pIn + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
+            for ( i = 0; i < iStep; i++ )
+            {
+                pOut[i]         = pIn[i + iStep];
+                pOut[i + iStep] = pIn[i + iStep];
+            }
+    }    
+}
 static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
 {
     if ( nWords == 1 )
@@ -274,7 +317,7 @@ static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
         for ( ; pTruth < pLimit; pTruth += 2*iStep )
             for ( i = 0; i < iStep; i++ )
                 pTruth[i + iStep] = pTruth[i];
-    }    
+    }
 }
 static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
 {
@@ -293,7 +336,7 @@ static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
         for ( ; pTruth < pLimit; pTruth += 2*iStep )
             for ( i = 0; i < iStep; i++ )
                 pTruth[i] = pTruth[i + iStep];
-    }    
+    }
 }
 
 /**Function*************************************************************
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 277da3d3..51475f27 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -39,8 +39,8 @@
 
 ABC_NAMESPACE_HEADER_START
 
-#define DAU_MAX_VAR     8 // should be 6 or more
-#define DAU_MAX_STR    64
+#define DAU_MAX_VAR    16 // should be 6 or more
+#define DAU_MAX_STR   256
 #define DAU_MAX_WORD  (1<<(DAU_MAX_VAR-6))
 
 ////////////////////////////////////////////////////////////////////////
@@ -51,6 +51,10 @@ ABC_NAMESPACE_HEADER_START
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int Dau_DsdIsConst( char * p )  { return (p[0] == '0' || p[0] == '1') && p[1] == 0; }
+static inline int Dau_DsdIsConst0( char * p ) { return  p[0] == '0' && p[1] == 0; }
+static inline int Dau_DsdIsConst1( char * p ) { return  p[0] == '1' && p[1] == 0; }
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -62,6 +66,7 @@ extern int           Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitP
 extern word *        Dau_DsdToTruth( char * p, int nVars );
 extern word          Dau_Dsd6ToTruth( char * p );
 extern void          Dau_DsdNormalize( char * p );
+extern int           Dau_DsdCountAnds( char * pDsd );
 
 /*=== dauMerge.c  ==========================================================*/
 extern void          Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index 9863f0be..a3d377d0 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -45,6 +45,30 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Elementary truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word ** Dau_DsdTtElems()
+{
+    static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
+    if ( pTtElems[0] == NULL )
+    {
+        int v;
+        for ( v = 0; v <= DAU_MAX_VAR; v++ )
+            pTtElems[v] = TtElems[v];
+        Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
+    }
+    return pTtElems;
+}
+
+/**Function*************************************************************
+
   Synopsis    [DSD formula manipulation.]
 
   Description []
@@ -192,7 +216,7 @@ void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches )
         if ( *(q+1) == '{' )
             *p = q+1;
     }
-    if ( **p >= 'a' && **p <= 'f' ) // var
+    if ( **p >= 'a' && **p <= 'z' ) // var
         return;
     if ( **p == '(' || **p == '[' ) // and/or/xor
     {
@@ -232,11 +256,6 @@ void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches )
         assert( *p == q );
         return;
     }
-    if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
-    {
-        (*p)++;
-        return;
-    }
     assert( 0 );
 }
 void Dau_DsdNormalize( char * pDsd )
@@ -249,6 +268,61 @@ void Dau_DsdNormalize( char * pDsd )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DsdCountAnds_rec( char * pStr, char ** p, int * pMatches )
+{
+    if ( **p == '!' )
+        (*p)++;
+    while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
+        (*p)++;
+    if ( **p == '<' )
+    {
+        char * q = pStr + pMatches[*p - pStr];
+        if ( *(q+1) == '{' )
+            *p = q+1;
+    }
+    if ( **p >= 'a' && **p <= 'z' ) // var
+        return 0;
+    if ( **p == '(' || **p == '[' ) // and/or/xor
+    {
+        int Counter = 0, AddOn = (**p == '(')? 1 : 3;
+        char * q = pStr + pMatches[ *p - pStr ];
+        assert( *q == **p + 1 + (**p != '(') );
+        for ( (*p)++; *p < q; (*p)++ )
+            Counter += AddOn + Dau_DsdCountAnds_rec( pStr, p, pMatches );
+        assert( *p == q );
+        return Counter - AddOn;
+    }
+    if ( **p == '<' || **p == '{' ) // mux
+    {
+        int Counter = 3;
+        char * q = pStr + pMatches[ *p - pStr ];
+        assert( *q == **p + 1 + (**p != '(') );
+        for ( (*p)++; *p < q; (*p)++ )
+            Counter += Dau_DsdCountAnds_rec( pStr, p, pMatches );
+        assert( *p == q );
+        return Counter;
+    }
+    assert( 0 );
+    return 0;
+}
+int Dau_DsdCountAnds( char * pDsd )
+{
+    if ( pDsd[1] == 0 )
+        return 0;
+    return Dau_DsdCountAnds_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes truth table for the DSD formula.]
 
   Description []
@@ -393,73 +467,69 @@ word Dau_Dsd6ToTruth( char * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Dau_DsdTruth6Compose_rec( word Func, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars )
+void Dau_DsdTruth6Compose_rec( word Func, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )
 {
     if ( Func == 0 )
     {
-        Abc_TtConst0( pRes, Abc_TtWordNum(nVars) );
+        Abc_TtConst0( pRes, nWordsR );
         return;
     }
     if ( Func == ~(word)0 )
     {
-        Abc_TtConst1( pRes, Abc_TtWordNum(nVars) );
+        Abc_TtConst1( pRes, nWordsR );
         return;
     }
     assert( nVars > 0 );
     if ( --nVars == 0 )
     {
         assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
-        Abc_TtCopy( pRes, pFanins[0], Abc_TtWordNum(nVars), Func == s_Truths6Neg[0] );
+        Abc_TtCopy( pRes, pFanins[0], nWordsR, Func == s_Truths6Neg[0] );
         return;
     }
     if ( !Abc_Tt6HasVar(Func, nVars) )
     {
-        Dau_DsdTruth6Compose_rec( Func, pFanins, pRes, nVars );
+        Dau_DsdTruth6Compose_rec( Func, pFanins, pRes, nVars, nWordsR );
         return;
     }
     {
         word pTtTemp[2][DAU_MAX_WORD];
-        Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, pTtTemp[0], nVars );
-        Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, pTtTemp[1], nVars );
-        Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], Abc_TtWordNum(nVars) );
+        Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, pTtTemp[0], nVars, nWordsR );
+        Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, pTtTemp[1], nVars, nWordsR );
+        Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
         return;
     }
 }
-void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars )
+void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )
 {
-    int nWords;
+    int nWordsF;
     if ( nVars <= 6 )
     {
-        Dau_DsdTruth6Compose_rec( pFunc[0], pFanins, pRes, nVars );
+        Dau_DsdTruth6Compose_rec( pFunc[0], pFanins, pRes, nVars, nWordsR );
         return;
     }
-    nWords = Abc_TtWordNum( nVars );
-    if ( Abc_TtIsConst0(pFunc, nWords) )
+    nWordsF = Abc_TtWordNum( nVars );
+    assert( nWordsF > 1 );
+    if ( Abc_TtIsConst0(pFunc, nWordsF) )
     {
-        Abc_TtConst0( pRes, nWords );
+        Abc_TtConst0( pRes, nWordsR );
         return;
     }
-    if ( Abc_TtIsConst1(pFunc, nWords) )
+    if ( Abc_TtIsConst1(pFunc, nWordsF) )
     {
-        Abc_TtConst1( pRes, nWords );
+        Abc_TtConst1( pRes, nWordsR );
         return;
     }
     if ( !Abc_TtHasVar( pFunc, nVars, nVars-1 ) )
     {
-        Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVars-1 );
+        Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVars-1, nWordsR );
         return;
     }
     {
-        word pCofTemp[2][DAU_MAX_WORD];
         word pTtTemp[2][DAU_MAX_WORD];
         nVars--;
-        Abc_TtCopy( pCofTemp[0], pFunc, nWords, 0 );
-        Abc_TtCopy( pCofTemp[1], pFunc, nWords, 0 );
-        Abc_TtCofactor0( pCofTemp[0], nWords, nVars );
-        Abc_TtCofactor1( pCofTemp[1], nWords, nVars );
-        Dau_DsdTruthCompose_rec( pCofTemp[0], pFanins, pTtTemp[0], nVars );
-        Dau_DsdTruthCompose_rec( pCofTemp[1], pFanins, pTtTemp[1], nVars );
-        Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWords );
+        Dau_DsdTruthCompose_rec( pFunc,             pFanins, pTtTemp[0], nVars, nWordsR );
+        Dau_DsdTruthCompose_rec( pFunc + nWordsF/2, pFanins, pTtTemp[1], nVars, nWordsR );
+        Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
         return;
     }
 }
@@ -469,9 +539,9 @@ void Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches, word ** pTtElem
     int fCompl = 0;
     if ( **p == '!' )
         (*p)++, fCompl = 1;
-    if ( **p >= 'a' && **p <= 'f' ) // var
+    if ( **p >= 'a' && **p <= 'z' ) // var
     {
-        assert( **p - 'a' >= 0 && **p - 'a' < 6 );
+        assert( **p - 'a' >= 0 && **p - 'a' < nVars );
         Abc_TtCopy( pRes, pTtElems[**p - 'a'], nWords, fCompl );
         return;
     }
@@ -523,15 +593,15 @@ void Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches, word ** pTtElem
     {
         word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], pFunc[DAU_MAX_WORD];
         char * q;
-        int i, nVars = Abc_TtReadHex( pFunc, *p );
-        *p += Abc_TtHexDigitNum( nVars );
+        int i, nVarsF = Abc_TtReadHex( pFunc, *p );
+        *p += Abc_TtHexDigitNum( nVarsF );
         q = pStr + pMatches[ *p - pStr ];
         assert( **p == '{' && *q == '}' );
         for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
             Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pFanins[i], nVars );
-        assert( i == nVars );
+        assert( i == nVarsF );
         assert( *p == q );
-        Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nWords );
+        Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVarsF, nWords );
         if ( fCompl ) Abc_TtNot( pRes, nWords );
         return;
     }
@@ -539,19 +609,13 @@ void Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches, word ** pTtElem
 }
 word * Dau_DsdToTruth( char * p, int nVars )
 {
-    static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR] = {NULL};
-    int v, nWords = Abc_TtWordNum( nVars );
-    word * pRes;
-    if ( pTtElems[0] == NULL )
-    {
-        for ( v = 0; v < DAU_MAX_VAR; v++ )
-            pTtElems[v] = TtElems[v];
-        Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
-    }
-    pRes = pTtElems[DAU_MAX_VAR];
-    if ( p[0] == '0' && p[1] == 0 )
+    int nWords = Abc_TtWordNum( nVars );
+    word ** pTtElems = Dau_DsdTtElems();
+    word * pRes = pTtElems[DAU_MAX_VAR];
+    assert( nVars <= DAU_MAX_VAR );
+    if ( Dau_DsdIsConst0(p) )
         Abc_TtConst0( pRes, nWords );
-    else if ( p[0] == '1' && p[1] == 0 )
+    else if ( Dau_DsdIsConst1(p) )
         Abc_TtConst1( pRes, nWords );
     else
         Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p), pTtElems, pRes, nVars );
@@ -840,13 +904,11 @@ int Dau_DsdCheck1Step( word * pTruth, int nVarsInit )
     for ( v = 0; v < nVarsInit; v++ )
     {
         // try first cofactor
-        Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
-        Abc_TtCofactor0( pCofTemp, nWords, v );
+        Abc_TtCofactor0p( pCofTemp, pTruth, nWords, v );
         nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
         nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL );
         // try second cofactor
-        Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
-        Abc_TtCofactor1( pCofTemp, nWords, v );
+        Abc_TtCofactor1p( pCofTemp, pTruth, nWords, v );
         nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
         nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL );
         // compare cofactors
@@ -961,14 +1023,12 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars,
             Dau_DsdWriteString( p, "<" );
             Dau_DsdWriteVar( p, pVars[vBest], 0 );
             // split decomposition
-            Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
-            Abc_TtCofactor1( pCofTemp, nWords, vBest );
+            Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest );
             nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes );
             assert( nNonDecSize == 0 );
             Dau_DsdWriteString( p, pRes );
             // split decomposition
-            Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
-            Abc_TtCofactor0( pCofTemp, nWords, vBest );
+            Abc_TtCofactor0p( pCofTemp, pTruth, nWords, vBest );
             nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes );
             assert( nNonDecSize == 0 );
             Dau_DsdWriteString( p, pRes );
@@ -1090,7 +1150,7 @@ finish:
     p->nConsts++;
     Dau_DsdWriteVar( p, pVars[v], 0 );
     pVars[v] = pVars[nVars-1];
-    Abc_TtSwapVars( pTruth, 6, v, nVars-1 );
+    Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
     return 1;
 }
 int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
@@ -1116,11 +1176,12 @@ int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int n
 }
 static inline int Dau_Dsd6FindSupportOne( Dau_Dsd_t * p, word tCof0, word tCof1, int * pVars, int nVars, int v, int u )
 {
-    int Status = Dau_DsdLookupVarCache( p, pVars[v], pVars[u] );
+    int Status = p ? Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) : 0;
     if ( Status == 0 )
     {
         Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u);
-        Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
+        if ( p )
+            Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
     }
     return Status;
 }
@@ -1216,7 +1277,7 @@ finish:
     assert( pBuffer[0] );
     pVars[u] = Dau_DsdAddVarDef( p, pBuffer );
     pVars[v] = pVars[nVars-1];
-    Abc_TtSwapVars( pTruth, 6, v, 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;
@@ -1262,7 +1323,7 @@ static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word  * pTrut
     p1->fSplitPrime = 0;
     // move this variable to the top
     ABC_SWAP( int, pVars[v], pVars[nVars-1] );
-    Abc_TtSwapVars( pTruth, 6, v, nVars-1 );
+    Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
     // cofactor w.r.t the last variable
     tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
     tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
@@ -1292,9 +1353,6 @@ static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word  * pTrut
     word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 );
     int fEqual0 = (C00 == C10) && (C01 == C11);
     int fEqual1 = (C00 == C11) && (C01 == C10);
-//    assert( iVar0 < iVar1 );
-//    fEqual0 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 3 );
-//    fEqual1 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 2 );
     if ( fEqual0 || fEqual1 )
     {
         char pBuffer[10];
@@ -1304,11 +1362,11 @@ static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word  * pTrut
         pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
         // remove iVar1
         ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
-        Abc_TtSwapVars( pTruth, 6, iVar1, --nVars );
+        Abc_TtSwapVars( pTruth, nVars, iVar1, nVars-1 ); nVars--;
         // remove iVar0
         iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
         ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
-        Abc_TtSwapVars( pTruth, 6, iVar0, --nVars );
+        Abc_TtSwapVars( pTruth, nVars, iVar0, nVars-1 ); nVars--;
         // find the new var
         v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
         // remove single variables if possible
@@ -1389,17 +1447,364 @@ int Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word  * pTruth, int * pVars, int n
   SeeAlso     []
 
 ***********************************************************************/
-int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
+static inline int Dau_DsdDecomposeSingleVarOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
 {
+    int nWords = Abc_TtWordNum(nVars);
+    // consider negative cofactors
+    if ( pTruth[0] & 1 )
+    {        
+        if ( Abc_TtCof0IsConst1( pTruth, nWords, v ) ) // !(ax)
+        {
+            Dau_DsdWriteString( p, "!(" );
+            Abc_TtCofactor1( pTruth, nWords, v );
+            Abc_TtNot( pTruth, nWords );
+            goto finish;            
+        }
+    }
+    else
+    {
+        if ( Abc_TtCof0IsConst0( pTruth, nWords, v ) ) // ax
+        {
+            Dau_DsdWriteString( p, "(" );
+            Abc_TtCofactor1( pTruth, nWords, v );
+            goto finish;            
+        }
+    }
+    // consider positive cofactors
+    if ( pTruth[nWords-1] >> 63 )
+    {        
+        if ( Abc_TtCof1IsConst1( pTruth, nWords, v ) ) // !(!ax)
+        {
+            Dau_DsdWriteString( p, "!(!" );
+            Abc_TtCofactor0( pTruth, nWords, v );
+            Abc_TtNot( pTruth, nWords );
+            goto finish;            
+        }
+    }
+    else
+    {
+        if ( Abc_TtCof1IsConst0( pTruth, nWords, v ) ) // !ax
+        {
+            Dau_DsdWriteString( p, "(!" );
+            Abc_TtCofactor0( pTruth, nWords, v );
+            goto finish;            
+        }
+    }
+    // consider equal cofactors
+    if ( Abc_TtCofsOpposite( pTruth, nWords, v ) ) // [ax]
+    {
+        Dau_DsdWriteString( p, "[" );
+        Abc_TtCofactor0( pTruth, nWords, v );
+        p->uConstMask |= (1 << p->nConsts);
+        goto finish;            
+    }
     return 0;
+
+finish:
+    p->nConsts++;
+    Dau_DsdWriteVar( p, pVars[v], 0 );
+    pVars[v] = pVars[nVars-1];
+    Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
+    return 1;
+}
+int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
+{
+    clock_t clk = clock();
+    assert( nVars > 1 );
+    while ( 1 )
+    {
+        int v;
+        for ( v = nVars - 1; v >= 0 && nVars > 1; v-- )
+            if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
+            {
+                nVars--;
+                break;
+            }
+        if ( v == -1 || nVars == 1 )
+            break;
+    }
+    if ( nVars == 1 )
+        Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
+    s_Times[0] += clock() - clk;
+    return nVars;
+}
+
+static inline int Dau_DsdFindSupportOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
+{
+    int nWords = Abc_TtWordNum(nVars);
+    int Status = p ? Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) : 0;
+    if ( Status == 0 )
+    {
+//        Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u);
+        if ( v < u )
+            Status = (!Abc_TtCheckEqualCofs(pTruth, nWords, v, u, 1, 3) << 1) | !Abc_TtCheckEqualCofs(pTruth, nWords, v, u, 0, 2);
+        else // if ( v > u )
+            Status = (!Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 2, 3) << 1) | !Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 1);
+        assert( Status != 0 );
+        if ( p )
+            Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
+    }
+    return Status;
+}
+static inline unsigned Dau_DsdFindSupports( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars, int v )
+{
+    int u;
+    unsigned uSupports = 0;
+//Kit_DsdPrintFromTruth( (unsigned *)&tCof0, 6 );printf( "\n" );
+//Kit_DsdPrintFromTruth( (unsigned *)&tCof1, 6 );printf( "\n" );
+    for ( u = 0; u < nVars; u++ )
+        if ( u != v )
+            uSupports |= (Dau_DsdFindSupportOne( p, pTruth, pVars, nVars, v, u ) << (2 * u));
+    return uSupports;
+}
+
+// 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 );
+//printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] );
+    if ( Status == 3 )
+    {
+        // both F(v=0) and F(v=1) depend on u
+//        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u
+        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) && Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 2) ) // 00=11 01=10 v+u
+        {
+            word pTtTemp[2][DAU_MAX_WORD];
+            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));
+            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 )
+    {
+        // F(v=0) does not depend on u; F(v=1) depends on u
+//        if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu
+        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 2) ) // 00=10 vu
+        {
+            word pTtTemp[2][DAU_MAX_WORD];
+            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));
+            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_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u
+        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) // 00=11 v!u
+        {
+            word pTtTemp[2][DAU_MAX_WORD];
+            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));
+            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 )
+    {
+        // F(v=0) depends on u; F(v=1) does not depend on u
+//        if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu
+        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) // 00=11 !vu
+        {
+            word pTtTemp[2][DAU_MAX_WORD];
+            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));
+            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_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u
+        if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 3) ) // 01=11 !v!u
+        {
+            word pTtTemp[2][DAU_MAX_WORD];
+            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));
+            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: 
+    // finalize decomposition
+    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;
 }
 int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
+    clock_t clk = clock();
+    while ( 1 )
+    {
+        int v, u, nVarsOld;
+        for ( v = nVars - 1; v > 0; v-- )
+        {
+            for ( u = v - 1; u >= 0; u-- )
+            {
+                if ( Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) )
+                    continue;
+                nVarsOld = nVars;
+                nVars = Dau_DsdDecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
+                if ( nVars == 0 )
+                {
+                    s_Times[1] += clock() - clk;
+                    return 0;
+                }
+                if ( nVarsOld > nVars )
+                    break;
+            }
+            if ( u >= 0 ) // found
+                break;
+        }
+        if ( v == 0 ) // not found
+            break;
+    }
+    s_Times[1] += clock() - clk;
+    return nVars;
+}
+
+// look for MUX-decomposable variable on top or at the bottom
+static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars, int v )
+{
+    extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
+    Dau_Dsd_t P1, * p1 = &P1;
+    word pTtCof[2][DAU_MAX_WORD];
+    int nWords = Abc_TtWordNum(nVars);
+    p1->fSplitPrime = 0;
+    // move this variable to the top
+    ABC_SWAP( int, pVars[v], pVars[nVars-1] );
+    Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
+    // cofactor w.r.t the last variable
+//    tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
+//    tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
+    Abc_TtCofactor0p( pTtCof[0], pTruth, nWords, nVars - 1 );
+    Abc_TtCofactor1p( pTtCof[1], pTruth, nWords, nVars - 1 );
+    // compose the result
+    Dau_DsdWriteString( p, "<" );
+    Dau_DsdWriteVar( p, pVars[nVars - 1], 0 );
+    // split decomposition
+    Dau_DsdDecomposeInt( p1, pTtCof[1], nVars - 1 );
+    Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
+    p->nSizeNonDec = p1->nSizeNonDec;
+    // split decomposition
+    Dau_DsdDecomposeInt( p1, pTtCof[0], nVars - 1 );
+    Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
+    Dau_DsdWriteString( p, ">" );
+    p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
     return 0;
 }
+static inline int Dau_DsdDecomposeTripleVarsInner( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
+{
+    int nWords = Abc_TtWordNum(nVars);
+    int iVar0 = Abc_TtSuppFindFirst(  uSupports & (~uSupports >> 1) & 0x55555555 ) >> 1;
+    int iVar1 = Abc_TtSuppFindFirst( ~uSupports & ( uSupports >> 1) & 0x55555555 ) >> 1;
+    int fEqual0, fEqual1;
+//    word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
+//    word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
+//    word C00 = Abc_Tt6Cofactor0( tCof0, iVar0 );
+//    word C01 = Abc_Tt6Cofactor1( tCof0, iVar0 );
+//    word C10 = Abc_Tt6Cofactor0( tCof1, iVar1 );
+//    word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 );
+//    int fEqual0 = (C00 == C10) && (C01 == C11);
+//    int fEqual1 = (C00 == C11) && (C01 == C10);
+    word pTtCof[2][DAU_MAX_WORD];
+    word pTtFour[2][2][DAU_MAX_WORD];
+    Abc_TtCofactor0p( pTtCof[0], pTruth, nWords, v );
+    Abc_TtCofactor1p( pTtCof[1], pTruth, nWords, v );
+    Abc_TtCofactor0p( pTtFour[0][0], pTtCof[0], nWords, iVar0 );
+    Abc_TtCofactor1p( pTtFour[0][1], pTtCof[0], nWords, iVar0 );
+    Abc_TtCofactor0p( pTtFour[1][0], pTtCof[1], nWords, iVar1 );
+    Abc_TtCofactor1p( pTtFour[1][1], pTtCof[1], nWords, iVar1 );
+    fEqual0 = Abc_TtEqual(pTtFour[0][0], pTtFour[1][0], nWords) && Abc_TtEqual(pTtFour[0][1], pTtFour[1][1], nWords);
+    fEqual1 = Abc_TtEqual(pTtFour[0][0], pTtFour[1][1], nWords) && Abc_TtEqual(pTtFour[0][1], pTtFour[1][0], nWords);
+    if ( fEqual0 || fEqual1 )
+    {
+        char pBuffer[10];
+        int VarId = pVars[iVar0];
+//        pTruth[0] = (s_Truths6[v] & C11) | (~s_Truths6[v] & C10);
+        Abc_TtMux( pTruth, Dau_DsdTtElems()[v], pTtFour[1][1], pTtFour[1][0], nWords );
+        sprintf( pBuffer, "<%c%c%s%c>", 'a' + pVars[v], 'a' + pVars[iVar1], fEqual1 ? "!":"", 'a' + pVars[iVar0] );
+        pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
+        // remove iVar1
+        ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
+        Abc_TtSwapVars( pTruth, nVars, iVar1, nVars-1 ); nVars--;
+        // remove iVar0
+        iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
+        ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
+        Abc_TtSwapVars( pTruth, nVars, iVar0, nVars-1 ); nVars--;
+        // find the new var
+        v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
+        // remove single variables if possible
+        if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
+            nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, --nVars );
+        return nVars;
+    }
+    return nVars;
+}
 int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
-    return 0;
+    clock_t clk = clock();
+    while ( 1 )
+    {
+        int v;
+//        Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
+        for ( v = nVars - 1; v >= 0; v-- )
+        {
+            unsigned uSupports = Dau_DsdFindSupports( p, pTruth, pVars, nVars, v );
+//            Dau_DsdPrintSupports( uSupports, nVars );
+            if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports
+                return Dau_DsdDecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v );
+            if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) &&
+                 Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor
+            {
+                int nVarsNew = Dau_DsdDecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports );
+                if ( nVarsNew == nVars )
+                    continue;
+                if ( nVarsNew == 0 )
+                {
+                    s_Times[2] += clock() - clk;
+                    return 0;
+                }
+                nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
+                if ( nVars == 0 )
+                {
+                    s_Times[2] += clock() - clk;
+                    return 0;
+                }
+                break;
+            }
+        }
+        if ( v == -1 )
+        {
+            s_Times[2] += clock() - clk;
+            return nVars;
+        }
+    }
+    assert( 0 );
+    return -1;
 }
 int Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
@@ -1449,7 +1854,7 @@ int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit )
     int Status = 0, nVars, pVars[16];
     Dau_DsdInitialize( p, nVarsInit );
     nVars = Dau_DsdMinBase( pTruth, nVarsInit, pVars );
-    assert( nVars > 0 && nVars <= 6 );
+    assert( nVars > 0 && nVars <= nVarsInit );
     if ( nVars == 1 )
         Dau_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) );
     else if ( nVars <= 6 )
@@ -1465,9 +1870,9 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes
     p->fSplitPrime = fSplitPrime;
     p->nSizeNonDec = 0;
     if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
-        pRes[0] = '0', pRes[1] = 0;
+        { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
     else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
-        pRes[0] = '1', pRes[1] = 0;
+        { if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
     else 
     {
         int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
@@ -1478,6 +1883,7 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes
         if ( fSplitPrime && Status == 2 )
             return -1;
     }
+//    assert( p->nSizeNonDec == 0 );
     return p->nSizeNonDec;
 }
 
@@ -1501,17 +1907,56 @@ void Dau_DsdTest44()
     nNonDec = 0;
 }
 
-void Dau_DsdTest33()
+
+
+void Dau_DsdTest888()
+{
+    char pDsd[DAU_MAX_STR];
+    int nVars = 9;
+//    char * pStr = "[(abc)(def)(ghi)]";
+//    char * pStr = "[a!b!(c!d[e(fg)hi])]";
+//    char * pStr = "[(abc)(def)]";
+//    char * pStr = "[(abc)(def)]";
+//    char * pStr = "[abcdefg]";
+//    char * pStr = "[<abc>(de[ghi])]";
+    char * pStr = "(<abc>(<def><ghi>))";
+    word * pTruth = Dau_DsdToTruth( pStr, 9 );
+    int i, Status;
+//    Kit_DsdPrintFromTruth( (unsigned *)pTruth, 9 ); printf( "\n" );
+/*
+    for ( i = 0; i < 6; i++ )
+    {
+        unsigned uSupp = Dau_Dsd6FindSupports( NULL, pTruth, NULL, 6, i );
+        Dau_DsdPrintSupports( uSupp, 6 );
+    }
+*/
+/*
+    printf( "\n" );
+    for ( i = 0; i < nVars; i++ )
+    {
+        unsigned uSupp = Dau_DsdFindSupports( NULL, pTruth, NULL, nVars, i );
+        Dau_DsdPrintSupports( uSupp, nVars );
+    }
+*/
+    Status = Dau_DsdDecompose( pTruth, nVars, 0, pDsd );
+    i = 0;
+}
+
+void Dau_DsdTest()
 {
-    char * pFileName = "_npn/npn/dsd06.txt";
+    int nVars = 10;
+    int nWords = Abc_TtWordNum(nVars);
+    char * pFileName = "_npn/npn/dsd10.txt";
     FILE * pFile = fopen( pFileName, "rb" );
-    word t, t1, t2;
-    char pBuffer[100];
+    word Tru[2][DAU_MAX_WORD], * pTruth;
+    char pBuffer[DAU_MAX_STR];
     char pRes[DAU_MAX_STR];
     int nSizeNonDec;
     int i, Counter = 0;
     clock_t clk = clock();
-    while ( fgets( pBuffer, 100, pFile ) != NULL )
+    return;
+
+    while ( fgets( pBuffer, DAU_MAX_STR, pFile ) != NULL )
     {
         char * pStr2 = pBuffer + strlen(pBuffer)-1;
         if ( *pStr2 == '\n' )
@@ -1522,21 +1967,24 @@ void Dau_DsdTest33()
             continue;
         Counter++; 
 
-        for ( i = 0; i < 1000; i++ )
+        for ( i = 0; i < 10; i++ )
         {
             Dau_DsdPermute( pBuffer );
-            t = t1 = Dau_Dsd6ToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer );
-            nSizeNonDec = Dau_DsdDecompose( &t, 6, 0, pRes );
+
+            pTruth = Dau_DsdToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer, nVars );
+            Abc_TtCopy( Tru[0], pTruth, nWords, 0 );
+            Abc_TtCopy( Tru[1], pTruth, nWords, 0 );
+            nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, pRes );
             Dau_DsdNormalize( pRes );
 //            pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0;
             assert( nSizeNonDec == 0 );
-            t2 = Dau_Dsd6ToTruth( pRes );
-            if ( t1 != t2 )
+            pTruth = Dau_DsdToTruth( pRes, nVars );
+            if ( !Abc_TtEqual( pTruth, Tru[0], nWords ) )
             {
     //        Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
     //        printf( "  " );
     //        Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 );
-                printf( "%s -> %s \n", pBuffer, pStr2 );
+                printf( "%s -> %s \n", pBuffer, pRes );
                 printf( "Verification failed.\n" );
             }
         }
@@ -1551,8 +1999,6 @@ void Dau_DsdTest33()
     fclose( pFile );
 }
 
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c
index f5117e5b..af4eff9c 100644
--- a/src/opt/dau/dauMerge.c
+++ b/src/opt/dau/dauMerge.c
@@ -31,21 +31,6 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
- 
-/**Function*************************************************************
-
-  Synopsis    [Substitution storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Dau_DsdIsConst( char * p )  { return (p[0] == '0' || p[0] == '1') && p[1] == 0; }
-static inline int Dau_DsdIsConst0( char * p ) { return  p[0] == '0' && p[1] == 0; }
-static inline int Dau_DsdIsConst1( char * p ) { return  p[0] == '1' && p[1] == 0; }
 
 
 /**Function*************************************************************
@@ -328,7 +313,7 @@ int Dau_DsdMergeStatus_rec( char * pStr, char ** p, int * pMatches, int nShared,
                 pStatus[pTemp - pStr] = -1;
         }
     }
-    if ( **p >= 'a' && **p <= 'f' ) // var
+    if ( **p >= 'a' && **p <= 'z' ) // var
         return pStatus[*p - pStr] = (**p - 'a' < nShared) ? 0 : 3;
     if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
     {
@@ -417,7 +402,7 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p
                     Dau_DsdMergeStoreAddToOutputChar( pS, *pTemp );
         }
     }
-    if ( **p >= 'a' && **p <= 'f' ) // var
+    if ( **p >= 'a' && **p <= 'z' ) // var
     {
         if ( fWrite )
             Dau_DsdMergeStoreAddToOutputChar( pS, **p );
@@ -544,7 +529,7 @@ void Dau_DsdRemoveBraces_rec( char * pStr, char ** p, int * pMatches )
         if ( *(q+1) == '{' )
             *p = q+1;
     }
-    if ( **p >= 'a' && **p <= 'f' ) // var
+    if ( **p >= 'a' && **p <= 'z' ) // var
         return;
     if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) 
     {
@@ -773,7 +758,7 @@ printf( "%s\n", pRes );
 }
 
 
-void Dau_DsdTest()
+void Dau_DsdTest66()
 {
     int Perm0[DAU_MAX_VAR] = { 0, 1, 2, 3, 4, 5 };
 //    int pMatches[DAU_MAX_STR];