Improvements to the truth table computations.

7 files changed, 997 insertions, 242 deletions

diff --git a/abclib.dsp b/abclib.dsp
index c0ad64cc..e963e7a8 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1975,6 +1975,10 @@ SOURCE=.\src\opt\dau\dau.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\dau\dauCanon.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\dau\dauCore.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 0e3f41f9..06732d2b 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -202,8 +202,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
     {
         for ( i = 0; i < p->nFuncs; i++ )
         {
+            extern void Abc_TtConfactorTest( word * pTruth, int nVars, int i );
             if ( fVerbose )
                 printf( "%7d : ", i );
+            Abc_TtConfactorTest( p->pFuncs[i], p->nVars, i );
             if ( fVerbose )
                 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
         }
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index bb31dc1f..78a0fa99 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -119,6 +119,7 @@ extern int          Extra_ReadHexadecimal( unsigned Sign[], char * pString, int
 extern void         Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars );
 extern void         Extra_PrintHexadecimalString( char * pString, unsigned Sign[], int nVars );
 extern void         Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars );
+extern void         Extra_PrintHexReverse( FILE * pFile, unsigned * pTruth, int nVars );
 extern void         Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine );
 
 /*=== extraUtilReader.c ========================================================*/
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index c0810e4b..721cbb12 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -561,6 +561,24 @@ void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars )
     }
 //    fprintf( pFile, "\n" );
 }
+void Extra_PrintHexReverse( FILE * pFile, unsigned * pTruth, int nVars )
+{
+    int nMints, nDigits, Digit, k;
+
+    // write the number into the file
+    fprintf( pFile, "0x" );
+    nMints  = (1 << nVars);
+    nDigits = nMints / 4;
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = ((pTruth[k/8] >> (k * 4)) & 15);
+        if ( Digit < 10 )
+            fprintf( pFile, "%d", Digit );
+        else
+            fprintf( pFile, "%c", 'A' + Digit-10 );
+    }
+//    fprintf( pFile, "\n" );
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index fe3eda63..2b4e17a7 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -198,6 +198,7 @@ typedef unsigned __int64 ABC_UINT64_T;
 #endif /* defined(PLATFORM) */
 
 typedef ABC_UINT64_T word;
+typedef ABC_INT64_T iword;
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 6bfb5699..30508498 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -44,6 +44,23 @@ static word s_Truths6[6] = {
     0xFFFFFFFF00000000
 };
 
+static word s_Truths6Neg[6] = {
+    0x5555555555555555,
+    0x3333333333333333,
+    0x0F0F0F0F0F0F0F0F,
+    0x00FF00FF00FF00FF,
+    0x0000FFFF0000FFFF,
+    0x00000000FFFFFFFF
+};
+
+static word s_CMasks6[5] = {
+    0x1111111111111111,
+    0x0303030303030303,
+    0x000F000F000F000F,
+    0x000000FF000000FF,
+    0x000000000000FFFF
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -76,6 +93,12 @@ static inline int  Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nV
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Abc_TtNot( word * pOut, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = ~pOut[w];
+}
 static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
 {
     int w;
@@ -96,6 +119,368 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
         for ( w = 0; w < nWords; w++ )
             pOut[w] = pIn1[w] & pIn2[w];
 }
+static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn1[w] != pIn2[w] )
+            return 0;
+    return 1;
+}
+static inline int Abc_TtCompare( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn1[w] != pIn2[w] )
+            return (pIn1[w] < pIn2[w]) ? -1 : 1;
+    return 0;
+}
+static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = nWords - 1; w >= 0; w-- )
+        if ( pIn1[w] != pIn2[w] )
+            return (pIn1[w] < pIn2[w]) ? -1 : 1;
+    return 0;
+}
+
+ 
+/**Function*************************************************************
+
+  Synopsis    [Compares Cof0 and Cof1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+    {
+        word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
+        word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
+        if ( Cof0 != Cof1 )
+            return Cof0 < Cof1 ? -1 : 1;
+        return 0;
+    }
+    if ( iVar <= 5 )
+    {
+        word Cof0, Cof1;
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+        {
+            Cof0 = pTruth[w] & s_Truths6Neg[iVar];
+            Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
+            if ( Cof0 != Cof1 )
+                return Cof0 < Cof1 ? -1 : 1;
+        }
+        return 0;
+    }
+    // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        assert( nWords >= 2 );
+        for ( ; pTruth < pLimit; pTruth += 2*iStep )
+            for ( i = 0; i < iStep; i++ )
+                if ( pTruth[i] != pTruth[i + iStep] )
+                    return pTruth[i] < pTruth[i + iStep] ? -1 : 1;
+        return 0;
+    }    
+}
+static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+    {
+        word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
+        word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
+        if ( Cof0 != Cof1 )
+            return Cof0 < Cof1 ? -1 : 1;
+        return 0;
+    }
+    if ( iVar <= 5 )
+    {
+        word Cof0, Cof1;
+        int w, shift = (1 << iVar);
+        for ( w = nWords - 1; w >= 0; w-- )
+        {
+            Cof0 = pTruth[w] & s_Truths6Neg[iVar];
+            Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
+            if ( Cof0 != Cof1 )
+                return Cof0 < Cof1 ? -1 : 1;
+        }
+        return 0;
+    }
+    // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        assert( nWords >= 2 );
+        for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep )
+            for ( i = iStep - 1; i >= 0; i-- )
+                if ( pLimit[i] != pLimit[i + iStep] )
+                    return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
+        return 0;
+    }    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks pairs of cofactors w.r.t. adjacent variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+{
+    assert( Num1 < Num2 && Num2 < 4 );
+    if ( nWords == 1 )
+        return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]);
+    if ( iVar <= 4 )
+    {
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+            if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) )
+                return 0;
+        return 1;
+    }
+    if ( iVar == 5 )
+    {
+        unsigned * pTruthU = (unsigned *)pTruth;
+        unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+        assert( nWords >= 2 );
+        for ( ; pTruthU < pLimitU; pTruthU += 4 )
+            if ( pTruthU[Num2] != pTruthU[Num1] )
+                return 0;
+        return 1;
+    }
+    // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        assert( nWords >= 4 );
+        for ( ; pTruth < pLimit; pTruth += 4*iStep )
+            for ( i = 0; i < iStep; i++ )
+                if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] )
+                    return 0;
+        return 1;
+    }    
+}
+static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+{
+    assert( Num1 < Num2 && Num2 < 4 );
+    if ( nWords == 1 )
+    {
+        word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
+        word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
+        if ( Cof1 != Cof2 )
+            return Cof1 < Cof2 ? -1 : 1;
+        return 0;
+    }
+    if ( iVar <= 4 )
+    {
+        word Cof1, Cof2;
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+        {
+            Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+            Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+            if ( Cof1 != Cof2 )
+                return Cof1 < Cof2 ? -1 : 1;
+        }
+        return 0;
+    }
+    if ( iVar == 5 )
+    {
+        unsigned * pTruthU = (unsigned *)pTruth;
+        unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+        assert( nWords >= 2 );
+        for ( ; pTruthU < pLimitU; pTruthU += 4 )
+            if ( pTruthU[Num1] != pTruthU[Num2] )
+                return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1;
+        return 0;
+    }
+    // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        int Offset1 = Num1*iStep;
+        int Offset2 = Num2*iStep;
+        assert( nWords >= 4 );
+        for ( ; pTruth < pLimit; pTruth += 4*iStep )
+            for ( i = 0; i < iStep; i++ )
+                if ( pTruth[i + Offset1] != pTruth[i + Offset2] )
+                    return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1;
+        return 0;
+    }    
+}
+static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+{
+    assert( Num1 < Num2 && Num2 < 4 );
+    if ( nWords == 1 )
+    {
+        word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
+        word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
+        if ( Cof1 != Cof2 )
+            return Cof1 < Cof2 ? -1 : 1;
+        return 0;
+    }
+    if ( iVar <= 4 )
+    {
+        word Cof1, Cof2;
+        int w, shift = (1 << iVar);
+        for ( w = nWords - 1; w >= 0; w-- )
+        {
+            Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+            Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+            if ( Cof1 != Cof2 )
+                return Cof1 < Cof2 ? -1 : 1;
+        }
+        return 0;
+    }
+    if ( iVar == 5 )
+    {
+        unsigned * pTruthU = (unsigned *)pTruth;
+        unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+        assert( nWords >= 2 );
+        for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 )
+            if ( pLimitU[Num1] != pLimitU[Num2] )
+                return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1;
+        return 0;
+    }
+    // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        int Offset1 = Num1*iStep;
+        int Offset2 = Num2*iStep;
+        assert( nWords >= 4 );
+        for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep )
+            for ( i = iStep - 1; i >= 0; i-- )
+                if ( pLimit[i + Offset1] != pLimit[i + Offset2] )
+                    return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1;
+        return 0;
+    }    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks pairs of cofactors w.r.t. two variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int jVar, int Num1, int Num2 )
+{
+    assert( Num1 < Num2 && Num2 < 4 );
+    assert( iVar < jVar );
+    if ( nWords == 1 )
+    {
+        word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
+        int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
+        int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
+        return ((pTruth[0] >> shift1) & Mask) == ((pTruth[0] >> shift2) & Mask);
+    }
+    if ( jVar <= 5 )
+    {
+        word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
+        int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
+        int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
+        int w;
+        for ( w = 0; w < nWords; w++ )
+            if ( ((pTruth[w] >> shift1) & Mask) != ((pTruth[w] >> shift2) & Mask) )
+                return 0;
+        return 1;
+    }
+    if ( iVar <= 5 && jVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int j, jStep = Abc_TtWordNum(jVar);
+        int shift1 = (Num1 & 1) * (1 << iVar);
+        int shift2 = (Num2 & 1) * (1 << iVar);
+        int Offset1 = (Num1 >> 1) * jStep;
+        int Offset2 = (Num2 >> 1) * jStep;
+        for ( ; pTruth < pLimit; pTruth += 2*jStep )
+            for ( j = 0; j < jStep; j++ )
+                if ( ((pTruth[j + Offset1] >> shift1) & s_Truths6Neg[iVar]) != ((pTruth[j + Offset2] >> shift2) & s_Truths6Neg[iVar]) )
+                    return 0;
+        return 1;
+    }
+    {
+        word * pLimit = pTruth + nWords;
+        int j, jStep = Abc_TtWordNum(jVar);
+        int i, iStep = Abc_TtWordNum(iVar);
+        int Offset1 = (Num1 >> 1) * jStep + (Num1 & 1) * iStep;
+        int Offset2 = (Num2 >> 1) * jStep + (Num2 & 1) * iStep;
+        for ( ; pTruth < pLimit; pTruth += 2*jStep )
+            for ( i = 0; i < jStep; i += 2*iStep )
+                for ( j = 0; j < iStep; j++ )
+                    if ( pTruth[Offset1 + i + j] != pTruth[Offset2 + i + j] )
+                        return 0;
+        return 1;
+    }    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+        pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]);
+    else if ( iVar <= 5 )
+    {
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+            pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
+    }
+    else // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(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 )
+{
+    if ( nWords == 1 )
+        pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
+    else if ( iVar <= 5 )
+    {
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+            pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
+    }
+    else // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        for ( ; pTruth < pLimit; pTruth += 2*iStep )
+            for ( i = 0; i < iStep; i++ )
+                pTruth[i] = pTruth[i + iStep];
+    }    
+}
 
 
 /**Function*************************************************************
@@ -109,13 +494,238 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == 0;                                          }
+static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar];                         }
+static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0;                                             }
+static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar];                               }
+static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); } 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0        ) return 0; return 1; }
+static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
+
+static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( t[i] & s_Truths6Neg[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( (t[i] & s_Truths6Neg[iVar]) != s_Truths6Neg[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( ~t[i] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( t[i] & s_Truths6[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i+Step] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( ~t[i+Step] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != ~t[i+Step] )
+                    return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtPrintDigit( int Digit )
+{
+    assert( Digit >= 0 && Digit < 16 );
+    if ( Digit < 10 )
+        printf( "%d", Digit );
+    else
+        printf( "%c", 'A' + Digit-10 );
+}
+static inline void Abc_TtPrintHex( word * pTruth, int nVars )
+{
+    word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
+    int k, nDigits = 1 << (nVars-2);
+    assert( nVars >= 2 );
+    for ( pThis = pTruth; pThis < pLimit; pThis++ )
+        for ( k = 0; k < 16; k++ )
+            Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+    printf( "\n" );
+}
+static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
+{
+    word * pThis;
+    int k, nDigits = 1 << (nVars-2);
+    assert( nVars >= 2 );
+    for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
+        for ( k = 15; k >= 0; k-- )
+            Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+    printf( "\n" );
+}
+static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
+{
+    word * pThis;
+    int k, nDigits = 1 << (nVars-2);
+    assert( nVars >= 2 );
+    for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
+        for ( k = 0; k < 16; k++ )
+            Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
+{
+    word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
+    int k, nDigits = 1 << (nVars-2);
+    assert( nVars >= 2 );
+    for ( pThis = pTruth; pThis < pLimit; pThis++ )
+        for ( k = 0; k < 64; k++ )
+            printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtSuppFindFirst( int Supp )
+{
+    int i;
+    assert( Supp > 0 );
+    for ( i = 0; i < 32; i++ )
+        if ( Supp & (1 << i) )
+            return i;
+    return -1;
+}
+static inline int Abc_TtSuppOnlyOne( int Supp )
+{
+    assert( Supp > 0 );
+    return (Supp & (Supp-1)) == 0;
+}
 static inline int Abc_TtSuppIsMinBase( int Supp )
 {
+    assert( Supp > 0 );
     return (Supp & (Supp+1)) == 0;
 }
 static inline int Abc_Tt6HasVar( word t, int iVar )
 {
-    return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]);
+    return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]);
 }
 static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
 {
@@ -125,7 +735,7 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
     {
         int i, Shift = (1 << iVar);
         for ( i = 0; i < nWords; i++ )
-            if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
+            if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
                 return 1;
         return 0;
     }
@@ -188,6 +798,69 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+        pTruth[0] = ((pTruth[0] << (1 << iVar)) & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
+    else if ( iVar <= 5 )
+    {
+        int w, shift = (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+            pTruth[w] = ((pTruth[w] << shift) & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
+    }
+    else // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        for ( ; pTruth < pLimit; pTruth += 2*iStep )
+            for ( i = 0; i < iStep; i++ )
+                ABC_SWAP( word, pTruth[i], pTruth[i + iStep] );
+    }    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
+{
+    static word PMasks[5][3] = {
+        { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+        { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+        { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+        { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+        { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+    };
+    if ( iVar < 5 )
+    {
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = (pTruth[i] & PMasks[iVar][0]) | ((pTruth[i] & PMasks[iVar][1]) << Shift) | ((pTruth[i] & PMasks[iVar][2]) >> Shift);
+    }
+    else if ( iVar == 5 )
+    {
+        unsigned * pTruthU = (unsigned *)pTruth;
+        unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+        for ( ; pTruthU < pLimitU; pTruthU += 4 )
+            ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] );
+    }
+    else // if ( iVar > 5 )
+    {
+        word * pLimit = pTruth + nWords;
+        int i, iStep = Abc_TtWordNum(iVar);
+        for ( ; pTruth < pLimit; pTruth += 4*iStep )
+            for ( i = 0; i < iStep; i++ )
+                ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] );
+    }
+}
+
 static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
 {
     static word PPMasks[5][6][3] = {
@@ -270,106 +943,239 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
         }
         else
         {
-            word temp, * pLimit = pTruth + Abc_TtWordNum(nVars);
+            word * pLimit = pTruth + Abc_TtWordNum(nVars);
             int i, iStep = Abc_TtWordNum(iVar);
             int j, jStep = Abc_TtWordNum(jVar);
             for ( ; pTruth < pLimit; pTruth += 2*jStep )
                 for ( i = 0; i < jStep; i += 2*iStep )
                     for ( j = 0; j < iStep; j++ )
-                    {
-                        temp = pTruth[iStep + i + j];
-                        pTruth[iStep + i + j] = pTruth[jStep + i + j];
-                        pTruth[jStep + i + j] = temp;
-                    }
+                        ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
         }    
     }
 }
 
-static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar )
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCountOnesSlow( word t )
 {
-    static word PPMasks[6][6] = {
-        { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
-        { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
-        { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 },
-        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 },
-        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 },
-        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 }
-    };
+    t =    (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555);
+    t =    (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333);
+    t =    (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F);
+    t =    (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF);
+    t =    (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF);
+    return (t & 0x00000000FFFFFFFF) +  (t>>32);
+}
+static inline int Abc_TtCountOnes( word x )
+{
+    x = x - ((x >> 1) & 0x5555555555555555);   
+    x = (x & 0x3333333333333333) + ((x >> 2) & 0x3333333333333333);    
+    x = (x + (x >> 4)) & 0x0F0F0F0F0F0F0F0F;    
+    x = x + (x >> 8);
+    x = x + (x >> 16);
+    x = x + (x >> 32); 
+    return (int)(x & 0xFF);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
+{   
+    int nWords = Abc_TtWordNum( nVars );
+    int k, Counter = 0;
+    for ( k = 0; k < nWords; k++ )
+        Counter += Abc_TtCountOnes( pTruth[k] );
+    return Counter;
+}
+static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
+{
+    int i, k, Counter, nWords;
+    memset( pStore, 0, sizeof(int) * nVars );
     if ( nVars <= 6 )
     {
-        int shift;
-        word low2High, high2Low; 
-        assert( iVar <= 5 && jVar <= 5 && iVar < jVar );
-        shift = (1 << jVar) - (1 << iVar);
-        low2High = (pTruth[0] & PPMasks[iVar][jVar - 1] ) << shift;
-        pTruth[0] &= ~PPMasks[iVar][jVar - 1];
-        high2Low = (pTruth[0] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
-        pTruth[0] &= ~(PPMasks[iVar][jVar - 1] << shift);
-        pTruth[0] |= low2High | high2Low;
+        for ( i = 0; i < nVars; i++ )
+            pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
+        return;
     }
-    else
+    assert( nVars > 6 );
+    nWords = Abc_TtWordNum( nVars );
+    for ( k = 0; k < nWords; k++ )
     {
-        word low2High, high2Low, temp;
-        int nWords = Abc_TtWordNum(nVars);
-        int shift, step, iStep, jStep;
-        int w = 0, i = 0, j = 0;
-        if ( iVar == jVar )
-            return;
-        if ( jVar < iVar )
-            ABC_SWAP( int, iVar, jVar );
-        if ( iVar <= 5 && jVar <= 5 )
-        {
-            shift = (1 << jVar) - (1 << iVar);
-            for ( w = 0; w < nWords; w++ )
-            {
-                low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift;
-                pTruth[w] &= ~PPMasks[iVar][jVar - 1];
-                high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
-                pTruth[w] &= ~(PPMasks[iVar][jVar - 1] << shift);
-                pTruth[w] |= low2High | high2Low;
-            }
-        }
-        else if ( iVar <= 5 && jVar > 5 )
+        // count 1's for the first six variables
+        for ( i = 0; i < 6; i++ )
+            pStore[i] += Abc_TtCountOnes( (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i)) );
+        // count 1's for all other variables
+        Counter = Abc_TtCountOnes( pTruth[k] );
+        for ( i = 6; i < nVars; i++ )
+            if ( (k & (1 << (i-6))) == 0 )
+                pStore[i] += Counter;
+        // count 1's for all other variables
+        Counter = Abc_TtCountOnes( pTruth[++k] );
+        for ( i = 6; i < nVars; i++ )
+            if ( (k & (1 << (i-6))) == 0 )
+                pStore[i] += Counter;
+    } 
+}
+static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore )
+{
+    static int bit_count[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
+    };
+    int i, k, nBytes;
+    unsigned char * pTruthC = (unsigned char *)pTruth;
+    nBytes = 8 * Abc_TtWordNum( nVars );
+    memset( pStore, 0, sizeof(int) * nVars );
+    for ( k = 0; k < nBytes; k++ )
+    {
+        pStore[0] += bit_count[ pTruthC[k] & 0x55 ];
+        pStore[1] += bit_count[ pTruthC[k] & 0x33 ];
+        pStore[2] += bit_count[ pTruthC[k] & 0x0F ];
+        for ( i = 3; i < nVars; i++ )
+            if ( (k & (1 << (i-3))) == 0 )
+                pStore[i] += bit_count[pTruthC[k]];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm )
+{
+    int pStore[16];
+    int nWords = Abc_TtWordNum( nVars );
+    int i, Temp, fChange, nOnes;
+    unsigned  uCanonPhase = 0;
+    assert( nVars <= 16 );
+    // normalize polarity    
+    nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
+    if ( nOnes > nWords * 32 )
+    {
+        Abc_TtNot( pTruth, nWords );
+        nOnes = nWords*64 - nOnes;
+        uCanonPhase |= (1 << nVars);
+    }
+    // normalize phase
+    Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( pStore[i] >= nOnes - pStore[i] )
+            continue;
+        Abc_TtFlip( pTruth, nWords, i );
+        uCanonPhase |= (1 << i);
+        pStore[i] = nOnes - pStore[i]; 
+    }
+    
+    do {
+        fChange = 0;
+        for ( i = 0; i < nVars-1; i++ )
         {
-            step = Abc_TtWordNum(jVar + 1)/2;
-            shift = 1 << iVar;
-            for ( w = 0; w < nWords; w += 2*step )
+            if ( pStore[i] <= pStore[i+1] )
+                continue;            
+           
+            Temp = pCanonPerm[i];
+            pCanonPerm[i] = pCanonPerm[i+1];
+            pCanonPerm[i+1] = Temp;
+            
+            Temp = pStore[i];
+            pStore[i] = pStore[i+1];
+            pStore[i+1] = Temp;
+            
+            if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
             {
-                for (j = 0; j < step; j++)
-                {
-                    low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift;
-                    pTruth[w + j] &= ~PPMasks[iVar][5];
-                    high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift;
-                    pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift);
-                    pTruth[w + j] |= high2Low;
-                    pTruth[w + step + j] |= low2High;            
-                }
+                uCanonPhase ^= (1 << i);
+                uCanonPhase ^= (1 << (i+1));
             }
+            Abc_TtSwapAdjacent( pTruth, nWords, i );            
+            fChange = 1;
         }
-        else
-        {
-            iStep = Abc_TtWordNum(iVar + 1)/2;
-            jStep = Abc_TtWordNum(jVar + 1)/2;
-            for (w = 0; w < nWords; w += 2*jStep)
-            {
-                for (i = 0; i < jStep; i += 2*iStep)
-                {
-                    for (j = 0; j < iStep; j++)
-                    {
-                        temp = pTruth[w + iStep + i + j];
-                        pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j];
-                        pTruth[w + jStep + i + j] = temp;
-                    }
-                }
-            }
-        }    
-    }
+    } while ( fChange );
+    return uCanonPhase;
 }
 
 
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtReverseVars( word * pTruth, int nVars )
+{
+    int k;
+    for ( k = 0; k < nVars/2 ; k++ )
+        Abc_TtSwapVars( pTruth, nVars, k, nVars - 1 - k );
+}
+static inline void Abc_TtReverseBits( word * pTruth, int nVars )
+{
+    static unsigned char pMirror[256] = {
+          0, 128,  64, 192,  32, 160,  96, 224,  16, 144,  80, 208,  48, 176, 112, 240,
+          8, 136,  72, 200,  40, 168, 104, 232,  24, 152,  88, 216,  56, 184, 120, 248,
+          4, 132,  68, 196,  36, 164, 100, 228,  20, 148,  84, 212,  52, 180, 116, 244,
+         12, 140,  76, 204,  44, 172, 108, 236,  28, 156,  92, 220,  60, 188, 124, 252,
+          2, 130,  66, 194,  34, 162,  98, 226,  18, 146,  82, 210,  50, 178, 114, 242,
+         10, 138,  74, 202,  42, 170, 106, 234,  26, 154,  90, 218,  58, 186, 122, 250,
+          6, 134,  70, 198,  38, 166, 102, 230,  22, 150,  86, 214,  54, 182, 118, 246,
+         14, 142,  78, 206,  46, 174, 110, 238,  30, 158,  94, 222,  62, 190, 126, 254,
+          1, 129,  65, 193,  33, 161,  97, 225,  17, 145,  81, 209,  49, 177, 113, 241,
+          9, 137,  73, 201,  41, 169, 105, 233,  25, 153,  89, 217,  57, 185, 121, 249,
+          5, 133,  69, 197,  37, 165, 101, 229,  21, 149,  85, 213,  53, 181, 117, 245,
+         13, 141,  77, 205,  45, 173, 109, 237,  29, 157,  93, 221,  61, 189, 125, 253,
+          3, 131,  67, 195,  35, 163,  99, 227,  19, 147,  83, 211,  51, 179, 115, 243,
+         11, 139,  75, 203,  43, 171, 107, 235,  27, 155,  91, 219,  59, 187, 123, 251,
+          7, 135,  71, 199,  39, 167, 103, 231,  23, 151,  87, 215,  55, 183, 119, 247,
+         15, 143,  79, 207,  47, 175, 111, 239,  31, 159,  95, 223,  63, 191, 127, 255
+    };
+    unsigned char Temp, * pTruthC = (unsigned char *)pTruth;
+    int i, nBytes = (nVars > 6) ? (1 << (nVars - 3)) : 8;
+    for ( i = 0; i < nBytes/2; i++ )
+    {
+        Temp = pMirror[pTruthC[i]];
+        pTruthC[i] = pMirror[pTruthC[nBytes-1-i]];
+        pTruthC[nBytes-1-i] = Temp;
+    }
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Stretch truthtable to have more input variables.]
 
   Description []
@@ -379,7 +1185,7 @@ static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar
   SeeAlso     []
 
 ***********************************************************************/
-static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
+static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
 {
     int w, i, step, nWords;
     if ( nVarS == nVarB )
@@ -394,7 +1200,7 @@ static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
         for ( i = 0; i < step; i++ )
             pInOut[w + i] = pInOut[i];              
 }
-static void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
+static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
 {
     int w, i, step, nWords;
     if ( nVarS == nVarB )
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index f6367304..d319e62d 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -478,163 +478,6 @@ void Dau_DsdTestOne( word t, int i )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0        ) return 0; return 1; }
-static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
-
-static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar ) 
-{ 
-    if ( iVar < 6 )
-    {
-        int i;
-        for ( i = 0; i < nWords; i++ )
-            if ( t[i] & ~s_Truths6[iVar] )
-                return 0;
-        return 1;
-    }
-    else
-    {
-        int i, Step = (1 << (iVar - 6));
-        word * tLimit = t + nWords;
-        for ( ; t < tLimit; t += 2*Step )
-            for ( i = 0; i < Step; i++ )
-                if ( t[i] )
-                    return 0;
-        return 1;
-    }
-}
-static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar ) 
-{ 
-    if ( iVar < 6 )
-    {
-        int i;
-        for ( i = 0; i < nWords; i++ )
-            if ( (t[i] & ~s_Truths6[iVar]) != ~s_Truths6[iVar] )
-                return 0;
-        return 1;
-    }
-    else
-    {
-        int i, Step = (1 << (iVar - 6));
-        word * tLimit = t + nWords;
-        for ( ; t < tLimit; t += 2*Step )
-            for ( i = 0; i < Step; i++ )
-                if ( t[i] != ~(word)0 )
-                    return 0;
-        return 1;
-    }
-}
-static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar ) 
-{ 
-    if ( iVar < 6 )
-    {
-        int i;
-        for ( i = 0; i < nWords; i++ )
-            if ( t[i] & s_Truths6[iVar] )
-                return 0;
-        return 1;
-    }
-    else
-    {
-        int i, Step = (1 << (iVar - 6));
-        word * tLimit = t + nWords;
-        for ( ; t < tLimit; t += 2*Step )
-            for ( i = 0; i < Step; i++ )
-                if ( t[i+Step] )
-                    return 0;
-        return 1;
-    }
-}
-static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar ) 
-{ 
-    if ( iVar < 6 )
-    {
-        int i;
-        for ( i = 0; i < nWords; i++ )
-            if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
-                return 0;
-        return 1;
-    }
-    else
-    {
-        int i, Step = (1 << (iVar - 6));
-        word * tLimit = t + nWords;
-        for ( ; t < tLimit; t += 2*Step )
-            for ( i = 0; i < Step; i++ )
-                if ( t[i+Step] != ~(word)0 )
-                    return 0;
-        return 1;
-    }
-}
-static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) 
-{ 
-    if ( iVar < 6 )
-    {
-        int i, Shift = (1 << iVar);
-        for ( i = 0; i < nWords; i++ )
-            if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
-                return 0;
-        return 1;
-    }
-    else
-    {
-        int i, Step = (1 << (iVar - 6));
-        word * tLimit = t + nWords;
-        for ( ; t < tLimit; t += 2*Step )
-            for ( i = 0; i < Step; i++ )
-                if ( t[i] != ~t[i+Step] )
-                    return 0;
-        return 1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Abc_TtCof0HasVar( word * t, int nWords, int iVarI, int iVarJ ) 
-{
-    assert( iVarI > iVarJ );
-    if ( iVarI < 6 )
-    {
-        int i, Shift = (1 << iVarJ);
-        for ( i = 0; i < nWords; i++ )
-            if ( (((t[i] & ~s_Truths6[iVarI]) << Shift) & s_Truths6[iVarJ]) != ((t[i] & ~s_Truths6[iVarI]) & s_Truths6[iVarJ]) )
-                return 0;
-        return 1;
-    }
-    else if ( iVarI == 6 )
-    {
-    }
-    else
-    {
-        int i, Step = (1 << (iVarJ - 6));
-        word * tLimit = t + nWords;
-        for ( ; t < tLimit; t += 2*Step )
-            for ( i = 0; i < Step; i++ )
-                if ( t[i] != t[i+Step] )
-                    return 0;
-        return 1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Dau_DsdMinimize( word * p, int * pVars, int nVars )
 {
     int i, k;
@@ -683,16 +526,18 @@ int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos,
 ***********************************************************************/
 int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
 {
-    int v, nWords = Abc_TtWordNum( nVars );
+    int v, u, nWords = Abc_TtWordNum( nVars );
     nVars = Dau_DsdMinimize( p, pVars, nVars );
     if ( nVars <= 6 )
         return Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
+    // consider negative cofactors
     if ( p[0] & 1 )
     {
         // check for !(ax)
         for ( v = 0; v < nVars; v++ )
-        if ( Abc_TtCof0IsConst0( p, nWords, v ) )
+        if ( Abc_TtCof0IsConst1( p, nWords, v ) )
         {
+            pBuffer[Pos++] = '!';
             pBuffer[Pos++] = '(';
             pBuffer[Pos++] = 'a' + pVars[v];
             Abc_TtSwapVars( p, nVars, v, nVars - 1 );
@@ -706,9 +551,8 @@ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, c
     {
         // check for ax
         for ( v = 0; v < nVars; v++ )
-        if ( Abc_TtCof0IsConst1( p, nWords, v ) )
+        if ( Abc_TtCof0IsConst0( p, nWords, v ) )
         {
-            pBuffer[Pos++] = '!';
             pBuffer[Pos++] = '(';
             pBuffer[Pos++] = 'a' + pVars[v];
             Abc_TtSwapVars( p, nVars, v, nVars - 1 );
@@ -718,6 +562,7 @@ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, c
             return Pos;
         }
     }
+    // consider positive cofactors
     if ( (p[nWords-1] >> 63) & 1 )
     {
         // check for !(!ax)
@@ -764,7 +609,85 @@ int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, c
         return Pos;
     }
 
-    return 0;
+    // consider two-variable cofactors
+    for ( v = nVars - 1; v > 0; v-- )
+    {
+        unsigned uSupp0 = 0, uSupp1 = 0;
+        for ( u = v - 1; u >= 0; u-- )
+        {
+            if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 1 ) )
+            {
+                uSupp0 |= (1 << u);
+                if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 2, 3 ) )
+                {
+                    uSupp1 |= (1 << u);
+                    // check XOR decomposition
+                    if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 3 ) && Abc_TtCheckEqualCofs( p, nWords, u, v, 1, 2 ) )
+                    {
+                        // perform XOR (u, v)
+                        return Pos;
+                    }
+                }
+                else
+                {
+                    // F(v=0) does not depend on u; F(v=1) depends on u
+                    if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 2 ) )
+                    {
+                        // perform AND (u, v)
+                        return Pos;
+                    }
+                    if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 3 ) )
+                    {
+                        // perform AND (u, v)
+                        return Pos;
+                    }
+                }
+            }
+            else if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 2, 3 ) )
+            {
+                uSupp1 |= (1 << u);
+                // F(v=0) depends on u; F(v=1) does not depend on u
+                if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 0, 2 ) )
+                {
+                    // perform AND (u, v)
+                    return Pos;
+                }
+                if ( Abc_TtCheckEqualCofs( p, nWords, u, v, 1, 2 ) )
+                {
+                    // perform AND (u, v)
+                    return Pos;
+                }
+            }
+            else assert( 0 );
+        }
+        // check MUX decomposition w.r.t. u
+        if ( (uSupp0 & uSupp1) == 0 )
+        {
+            // perform MUX( v, F(v=1), F(v=0) )
+        }
+        // check MUX decomposition w.r.t. u
+        if ( Abc_TtSuppOnlyOne( uSupp0 & ~uSupp1 ) && Abc_TtSuppOnlyOne( ~uSupp0 & uSupp1 ) )
+        {
+            // check MUX 
+            int iVar0 = Abc_TtSuppFindFirst( uSupp0 );
+            int iVar1 = Abc_TtSuppFindFirst( uSupp1 );
+            int fEqual0, fEqual1;
+
+            if ( iVar0 > iVar1 )
+                ABC_SWAP( int, iVar0, iVar1 );
+
+            // check existence conditions
+            assert( iVar0 < iVar1 );
+            fEqual0 = Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 1, 3 );
+            fEqual1 = Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( p, nWords, iVar0, iVar1, 1, 2 );
+            if ( fEqual0 || fEqual1 )
+            {
+                // perform MUX( v, F(v=1), F(v=0) )
+                return Pos;
+            }
+        }
+    }
+    return Pos;
 }