Improvements to the truth table computations.

5 files changed, 889 insertions, 1100 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b973aba7..3b6746ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4937,6 +4937,7 @@ usage:
     Abc_Print( -2, "\t               2: semi-canonical form by counting 1s in cofactors\n" );
     Abc_Print( -2, "\t               3: Jake's hybrid semi-canonical form (fast)\n" );
     Abc_Print( -2, "\t               4: Jake's hybrid semi-canonical form (high-effort)\n" );
+    Abc_Print( -2, "\t               5: new fast hybrid semi-canonical form\n" );
     Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
     Abc_Print( -2, "\t-d       : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" );
     Abc_Print( -2, "\t-b       : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 759d91b3..ffcf00f7 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -23,6 +23,7 @@
 
 #include "bool/kit/kit.h"
 #include "bool/lucky/lucky.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -190,6 +191,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
         pAlgoName = "Jake's hybrid fast ";
     else if ( NpnType == 4 )
         pAlgoName = "Jake's hybrid good ";
+    else if ( NpnType == 5 )
+        pAlgoName = "new hybrid fast    ";
 
     assert( p->nVars <= 16 );
     if ( pAlgoName )
@@ -202,10 +205,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
     {
         for ( i = 0; i < p->nFuncs; i++ )
         {
-            extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i );
             if ( fVerbose )
                 printf( "%7d : ", i );
-            Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i );
             if ( fVerbose )
                 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
         }
@@ -261,6 +262,17 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
                 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
         }
     }
+    else if ( NpnType == 5 )
+    {
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            uCanonPhase = Abc_TtCanonicize( p->pFuncs[i], p->nVars, pCanonPerm );
+            if ( fVerbose )
+                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
+        }
+    }
     else assert( 0 );
     clk = clock() - clk;
     printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) );
@@ -324,7 +336,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
 {
     if ( fVerbose )
         printf( "Using truth tables from file \"%s\"...\n", pFileName );
-    if ( NpnType >= 0 && NpnType <= 4 )
+    if ( NpnType >= 0 && NpnType <= 5 )
         Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
     else
         printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 236c0d62..c742aac9 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -61,6 +61,14 @@ static word s_CMasks6[5] = {
     0x000000000000FFFF
 };
 
+static word s_PMasks[5][3] = {
+    { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+    { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+    { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+    { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+    { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -161,10 +169,9 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
     return 1;
 }
 
- 
 /**Function*************************************************************
 
-  Synopsis    [Compares Cof0 and Cof1.]
+  Synopsis    []
 
   Description []
                
@@ -173,217 +180,42 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
+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 )
     {
-        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;
+            pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
     }
-    // if ( iVar > 5 )
+    else // 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;
+                pTruth[i + iStep] = pTruth[i];
     }    
 }
-static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
 {
-    assert( Num1 < Num2 && Num2 < 4 );
     if ( nWords == 1 )
+        pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
+    else if ( iVar <= 5 )
     {
-        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;
+            pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
     }
-    // if ( iVar > 5 )
+    else // 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 ( ; pTruth < pLimit; pTruth += 2*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;
+                pTruth[i] = pTruth[i + iStep];
     }    
 }
 
@@ -449,56 +281,6 @@ static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int
     }    
 }
 
-/**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*************************************************************
 
@@ -826,6 +608,10 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
   SeeAlso     []
 
 ***********************************************************************/
+static inline word Abc_Tt6Flip( word Truth, int iVar )
+{
+    return Truth = ((Truth << (1 << iVar)) & s_Truths6[iVar]) | ((Truth & s_Truths6[iVar]) >> (1 << iVar));
+}
 static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
 {
     if ( nWords == 1 )
@@ -857,9 +643,13 @@ static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
+static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar )
+{
+    return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar));
+}
 static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
 {
-    static word PMasks[5][3] = {
+    static word s_PMasks[5][3] = {
         { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
         { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
         { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
@@ -870,7 +660,7 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
     {
         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);
+            pTruth[i] = (pTruth[i] & s_PMasks[iVar][0]) | ((pTruth[i] & s_PMasks[iVar][1]) << Shift) | ((pTruth[i] & s_PMasks[iVar][2]) >> Shift);
     }
     else if ( iVar == 5 )
     {
@@ -888,10 +678,9 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
                 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] = {
+    static word Ps_PMasks[5][6][3] = {
         { 
             { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0  
             { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1  
@@ -940,18 +729,18 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
     assert( iVar < jVar && jVar < nVars );
     if ( nVars <= 6 )
     {
-        word * pMasks = PPMasks[iVar][jVar];
+        word * s_PMasks = Ps_PMasks[iVar][jVar];
         int shift = (1 << jVar) - (1 << iVar);
-        pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift);
+        pTruth[0] = (pTruth[0] & s_PMasks[0]) | ((pTruth[0] & s_PMasks[1]) << shift) | ((pTruth[0] & s_PMasks[2]) >> shift);
         return;
     }
     if ( jVar <= 5 )
     {
-        word * pMasks = PPMasks[iVar][jVar];
+        word * s_PMasks = Ps_PMasks[iVar][jVar];
         int nWords = Abc_TtWordNum(nVars);
         int w, shift = (1 << jVar) - (1 << iVar);
         for ( w = 0; w < nWords; w++ )
-            pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
+            pTruth[w] = (pTruth[w] & s_PMasks[0]) | ((pTruth[w] & s_PMasks[1]) << shift) | ((pTruth[w] & s_PMasks[2]) >> shift);
         return;
     }
     if ( iVar <= 5 && jVar > 5 )
@@ -984,6 +773,38 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
 
 /**Function*************************************************************
 
+  Synopsis    [Implemeting given NPN config.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
+{
+    int i, k, nWords = Abc_TtWordNum( nVars );
+    if ( (uCanonPhase >> nVars) & 1 )
+        Abc_TtNot( pTruth, nWords );
+    for ( i = 0; i < nVars; i++ )
+        if ( (uCanonPhase >> i) & 1 )
+            Abc_TtFlip( pTruth, nWords, i );
+    for ( i = 0; i < nVars; i++ )
+    {
+        for ( k = i; k < nVars; k++ )
+            if ( pCanonPerm[k] == i )
+                break;
+        assert( k < nVars );
+        if ( i == k )
+            continue;
+        Abc_TtSwapVars( pTruth, nVars, i, k );
+        ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -1024,220 +845,6 @@ static inline int Abc_TtCountOnes( word x )
   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++ )
-        if ( pTruth[k] )
-            Counter += Abc_TtCountOnes( pTruth[k] );
-    return Counter;
-}
-static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
-{
-    word Temp;
-    int i, k, Counter, nWords;
-    if ( nVars <= 6 )
-    {
-        for ( i = 0; i < nVars; i++ )
-            if ( pTruth[0] & s_Truths6Neg[i] )
-                pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
-            else
-                pStore[i] = 0;
-        return;
-    }
-    assert( nVars > 6 );
-    nWords = Abc_TtWordNum( nVars );
-    memset( pStore, 0, sizeof(int) * nVars );
-    for ( k = 0; k < nWords; k++ )
-    {
-        // count 1's for the first six variables
-        for ( i = 0; i < 6; i++ )
-            if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) )
-                pStore[i] += Abc_TtCountOnes( Temp );
-        // count 1's for all other variables
-        if ( pTruth[k] )
-        {
-            Counter = Abc_TtCountOnes( pTruth[k] );
-            for ( i = 6; i < nVars; i++ )
-                if ( (k & (1 << (i-6))) == 0 )
-                    pStore[i] += Counter;
-        }
-        k++;
-        // count 1's for all other variables
-        if ( pTruth[k] )
-        {
-            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 * pStoreOut )
-{
-    extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore );
-
-    int fOldSwap = 0;
-    int pStoreIn[17];
-    int * pStore = pStoreOut ? pStoreOut : pStoreIn;
-//    int pStore2[17];
-    int nWords = Abc_TtWordNum( nVars );
-    int i, Temp, nOnes;//, fChange;//, nSwaps = 0;//;
-    int k, BestK;
-    unsigned  uCanonPhase = 0;
-    assert( nVars <= 16 );
-    for ( i = 0; i < nVars; i++ )
-        pCanonPerm[i] = i;
-    // 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 );
-    pStore[nVars] = nOnes;
-//    Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore );
-
-//    Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 );
-//    for ( i = 0; i < nVars; i++ )
-//        assert( pStore[i] == pStore2[i] );
-
-    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]; 
-    }
-
-    if ( fOldSwap )
-    {
-        int fChange;
-        do {
-            fChange = 0;
-            for ( i = 0; i < nVars-1; i++ )
-            {
-    //            if ( pStore[i] <= pStore[i+1] )
-                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) )
-                {
-                    uCanonPhase ^= (1 << i);
-                    uCanonPhase ^= (1 << (i+1));
-                }
-                Abc_TtSwapAdjacent( pTruth, nWords, i );            
-                fChange = 1;
-    //            nSwaps++;
-            }
-        } while ( fChange );
-    }
-    else
-    {
-        for ( i = 0; i < nVars - 1; i++ )
-        {
-            BestK = i + 1;
-            for ( k = i + 2; k < nVars; k++ )
-    //            if ( pStore[BestK] > pStore[k] )
-                if ( pStore[BestK] < pStore[k] )
-                    BestK = k;
-    //        if ( pStore[i] <= pStore[BestK] )
-            if ( pStore[i] >= pStore[BestK] )
-                continue;
-           
-            Temp = pCanonPerm[i];
-            pCanonPerm[i] = pCanonPerm[BestK];
-            pCanonPerm[BestK] = Temp;
-        
-            Temp = pStore[i];
-            pStore[i] = pStore[BestK];
-            pStore[BestK] = Temp;
-        
-            if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
-            {
-                uCanonPhase ^= (1 << i);
-                uCanonPhase ^= (1 << BestK);
-            }
-            Abc_TtSwapVars( pTruth, nVars, i, BestK );
-    //        nSwaps++;
-        }
-    }
-
-
-//    printf( "%d ", nSwaps );
-/*
-    printf( "Minterms: " );
-    for ( i = 0; i < nVars; i++ )
-        printf( "%d ", pStore[i] );
-    printf( "\n" );
-*/
-    return uCanonPhase;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline void Abc_TtReverseVars( word * pTruth, int nVars )
 {
     int k;
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
new file mode 100644
index 00000000..b65a1b2c
--- /dev/null
+++ b/src/opt/dau/dau.h
@@ -0,0 +1,69 @@
+/**CFile****************************************************************
+
+  FileName    [dau.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware unmapping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: dau.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__DAU___h
+#define ABC__DAU___h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "misc/vec/vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dauCanon.c ==========================================================*/
+extern unsigned      Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index b66b276b..2853f238 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -30,10 +30,10 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 /**Function*************************************************************
 
-  Synopsis    [Generate reverse bytes.]
+  Synopsis    [Compares Cof0 and Cof1.]
 
   Description []
                
@@ -42,26 +42,80 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_TtReverseBypes()
+static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
 {
-    int i, k;
-    for ( i = 0; i < 256; i++ )
+    if ( nWords == 1 )
     {
-        int Mask = 0;
-        for ( k = 0; k < 8; k++ )
-            if ( (i >> k) & 1 )
-            Mask |= (1 << (7-k));
-//        printf( "%3d %3d\n", i, Mask );
-
-        if ( i % 16 == 0 )
-            printf( "\n" );
-        printf( "%-3d, ", Mask );
+        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    []
+  Synopsis    [Checks equality of pairs of cofactors w.r.t. adjacent variables.]
 
   Description []
                
@@ -70,722 +124,772 @@ void Abc_TtReverseBypes()
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_TtCofactorTest7( word * pTruth, int nVars, int N )
+static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
 {
-    word Cof[4][1024];
-    int i, nWords = Abc_TtWordNum( nVars );
-//    int Counter = 0;
-    for ( i = 0; i < nVars-1; i++ )
+    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 )
     {
-        Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[0], nWords, i );
-        Abc_TtCofactor0( Cof[0], nWords, i + 1 );
+        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;
+    }    
+}
 
-        Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[1], nWords, i );
-        Abc_TtCofactor0( Cof[1], nWords, i + 1 );
+/**Function*************************************************************
 
-        Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[2], nWords, i );
-        Abc_TtCofactor1( Cof[2], nWords, i + 1 );
+  Synopsis    [Compares pairs of cofactors w.r.t. adjacent variables.]
 
-        Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[3], nWords, i );
-        Abc_TtCofactor1( Cof[3], nWords, i + 1 );
+  Description []
+               
+  SideEffects []
 
-        if ( i == 5 && N == 4 )
-        {
-            printf( "\n" );
-            Abc_TtPrintHex( Cof[0], nVars );
-            Abc_TtPrintHex( Cof[1], nVars );
-            Abc_TtPrintHex( Cof[2], nVars );
-            Abc_TtPrintHex( Cof[3], nVars );
-        }
+  SeeAlso     []
 
-        assert( Abc_TtCompareRev(Cof[0], Cof[1], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) );
-        assert( Abc_TtCompareRev(Cof[0], Cof[2], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) );
-        assert( Abc_TtCompareRev(Cof[0], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) );
-        assert( Abc_TtCompareRev(Cof[1], Cof[2], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) );
-        assert( Abc_TtCompareRev(Cof[1], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) );
-        assert( Abc_TtCompareRev(Cof[2], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) );
-/*
-        Counter += Abc_TtCompare(Cof[0], Cof[1], nWords);
-        Counter += Abc_TtCompare(Cof[0], Cof[2], nWords);
-        Counter += Abc_TtCompare(Cof[0], Cof[3], nWords);
-        Counter += Abc_TtCompare(Cof[1], Cof[2], nWords);
-        Counter += Abc_TtCompare(Cof[1], Cof[3], nWords);
-        Counter += Abc_TtCompare(Cof[2], Cof[3], nWords);
-
-        Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 1);
-        Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 2);
-        Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 3);
-        Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 1, 2);
-        Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 1, 3);
-        Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 2, 3);
-*/ 
-    }
-}
-void Abc_TtCofactorTest2( word * pTruth, int nVars, int N )
+***********************************************************************/
+static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
 {
-//    word Cof[4][1024];
-    int i, j, nWords = Abc_TtWordNum( nVars );
-    int Counter = 0;
-    for ( i = 0; i < nVars-1; i++ )
-    for ( j = i+1; j < nVars; j++ )
+    assert( Num1 < Num2 && Num2 < 4 );
+    if ( nWords == 1 )
     {
-/*
-        Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[0], nWords, i );
-        Abc_TtCofactor0( Cof[0], nWords, j );
-
-        Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[1], nWords, i );
-        Abc_TtCofactor0( Cof[1], nWords, j );
-
-        Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[2], nWords, i );
-        Abc_TtCofactor1( Cof[2], nWords, j );
-
-        Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[3], nWords, i );
-        Abc_TtCofactor1( Cof[3], nWords, j );
-*/
-/*
-        if ( i == 0 && j == 1 && N == 0 )
+        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++ )
         {
-            printf( "\n" );
-            Abc_TtPrintHexSpecial( Cof[0], nVars ); printf( "\n" );
-            Abc_TtPrintHexSpecial( Cof[1], nVars ); printf( "\n" );
-            Abc_TtPrintHexSpecial( Cof[2], nVars ); printf( "\n" );
-            Abc_TtPrintHexSpecial( Cof[3], nVars ); printf( "\n" );
+            Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+            Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+            if ( Cof1 != Cof2 )
+                return Cof1 < Cof2 ? -1 : 1;
         }
-*/
-/*
-        assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) );
-        assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) );
-        assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) );
-        assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) );
-        assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) );
-        assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) );
-*/
-
-        Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1);
-        Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2);
-        Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3);
-        Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2);
-        Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3);
-        Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3);
-/*
-        Counter += Abc_TtEqual(Cof[0], Cof[1], nWords);
-        Counter += Abc_TtEqual(Cof[0], Cof[2], nWords);
-        Counter += Abc_TtEqual(Cof[0], Cof[3], nWords);
-        Counter += Abc_TtEqual(Cof[1], Cof[2], nWords);
-        Counter += Abc_TtEqual(Cof[1], Cof[3], nWords);
-        Counter += Abc_TtEqual(Cof[2], Cof[3], nWords);
-*/
+        return 0;
     }
-}
-void Abc_TtCofactorTest3( word * pTruth, int nVars, int N )
-{
-    word Cof[4][1024];
-    int i, j, nWords = Abc_TtWordNum( nVars );
-    for ( i = 0; i < nVars-1; i++ )
-    for ( j = i+1; j < nVars; j++ )
-    {
-        Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[0], nWords, i );
-        Abc_TtCofactor0( Cof[0], nWords, j );
-
-        Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[1], nWords, i );
-        Abc_TtCofactor0( Cof[1], nWords, j );
-
-        Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[2], nWords, i );
-        Abc_TtCofactor1( Cof[2], nWords, j );
-
-        Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[3], nWords, i );
-        Abc_TtCofactor1( Cof[3], nWords, j );
-
-        assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) );
-        assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) );
-        assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) );
-        assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) );
-        assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) );
-        assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) );
+    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;
+    }    
 }
-
-void Abc_TtCofactorTest4( word * pTruth, int nVars, int N )
+static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
 {
-    word Cof[4][1024];
-    int i, j, nWords = Abc_TtWordNum( nVars );
-    int Sum = 0;
-    for ( i = 0; i < nVars-1; i++ )
-    for ( j = i+1; j < nVars; j++ )
-    {
-        Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[0], nWords, i );
-        Abc_TtCofactor0( Cof[0], nWords, j );
-
-        Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[1], nWords, i );
-        Abc_TtCofactor0( Cof[1], nWords, j );
-
-        Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[2], nWords, i );
-        Abc_TtCofactor1( Cof[2], nWords, j );
-
-        Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[3], nWords, i );
-        Abc_TtCofactor1( Cof[3], nWords, j );
-
-
-        Sum = 0;
-        Sum += Abc_TtEqual(Cof[0], Cof[1], nWords);
-        Sum += Abc_TtEqual(Cof[0], Cof[2], nWords);
-        Sum += Abc_TtEqual(Cof[0], Cof[3], nWords);
-        Sum += Abc_TtEqual(Cof[1], Cof[2], nWords);
-        Sum += Abc_TtEqual(Cof[1], Cof[3], nWords);
-        Sum += Abc_TtEqual(Cof[2], Cof[3], nWords);
-
-        assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) );
-        assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) );
-        assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) );
-        assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) );
-        assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) );
-        assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) );
+    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;
     }
-}
-
-void Abc_TtCofactorTest6( word * pTruth, int nVars, int N )
-{
-//    word Cof[4][1024];
-    int i, nWords = Abc_TtWordNum( nVars );
-//    if ( N != 30 )
-//        return;
-    printf( "\n   " );
-    Abc_TtPrintHex( pTruth, nVars );
-//    Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
-
-    for ( i = nVars - 1; i >= 0; i-- )
+    if ( iVar <= 4 )
     {
-/*
-        Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[0], nWords, i );
-        printf( "-  " );
-        Abc_TtPrintHex( Cof[0], nVars );
-
-        Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[1], nWords, i );
-        printf( "+  " );
-        Abc_TtPrintHex( Cof[1], nVars );
-*/
-        if ( Abc_TtCompare1VarCofsRev( pTruth, nWords, i ) == -1 )
+        word Cof1, Cof2;
+        int w, shift = (1 << iVar);
+        for ( w = nWords - 1; w >= 0; w-- )
         {
-            printf( "%d  ", i );
-            Abc_TtFlip( pTruth, nWords, i );
-            Abc_TtPrintHex( pTruth, nVars );
-//            Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
+            Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+            Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+            if ( Cof1 != Cof2 )
+                return Cof1 < Cof2 ? -1 : 1;
         }
-
-
-/*
-        Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
-        Abc_TtCofactor0( Cof[0], nWords, i );
-
-        Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
-        Abc_TtCofactor1( Cof[1], nWords, i );
-
-        assert( Abc_TtCompareRev(Cof[0], Cof[1], nWords) == Abc_TtCompare1VarCofsRev(pTruth, nWords, i) );
-*/
+        return 0;
     }
-    i = 0;
-}
-
-int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
-{
-    static word pCopy[1024];
-    static word pBest[1024];
-
-    if ( fSwapOnly )
+    if ( iVar == 5 )
     {
-        Abc_TtCopy( pCopy, pTruth, nWords, 0 );
-        Abc_TtSwapAdjacent( pCopy, nWords, i );
-        if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
-        {
-            Abc_TtCopy( pTruth, pCopy, nWords, 0 );
-            return 1;
-        }
+        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;
     }
-
-    // save two copies
-    Abc_TtCopy( pCopy, pTruth, nWords, 0 );
-    Abc_TtCopy( pBest, pTruth, nWords, 0 );
-
-    // PXY
-    // 001
-    Abc_TtFlip( pCopy, nWords, i );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 011
-    Abc_TtFlip( pCopy, nWords, i+1 );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 010
-    Abc_TtFlip( pCopy, nWords, i );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 110
-    Abc_TtSwapAdjacent( pCopy, nWords, i );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 111
-    Abc_TtFlip( pCopy, nWords, i+1 );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 101
-    Abc_TtFlip( pCopy, nWords, i );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 100
-    Abc_TtFlip( pCopy, nWords, i+1 );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    // PXY
-    // 000
-    Abc_TtSwapAdjacent( pCopy, nWords, i );
-    if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
-        Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
-    assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
-    if ( Abc_TtEqual( pTruth, pBest, nWords ) )
+    // 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;
-    assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
-    Abc_TtCopy( pTruth, pBest, nWords, 0 );
-    return 1;
+    }    
 }
 
+/**Function*************************************************************
 
-int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, char * pCanonPerm, unsigned * puCanonPhase, int fSwapOnly )
-{
-    static word pCopy1[1024];
-    int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23;
-    unsigned uPhaseInit = *puCanonPhase;
-    int RetValue = 0;
-
-    if ( fSwapOnly )
-    {
-        fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
-        if ( fComp12 < 0 ) // Cof1 < Cof2
-        {
-            Abc_TtSwapAdjacent( pTruth, nWords, i );
-            RetValue = 1;
+  Synopsis    [Minterm counting in all cofactors.]
 
-            if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
-            {
-                *puCanonPhase ^= (1 << i);
-                *puCanonPhase ^= (1 << (i+1));
-            }
+  Description []
+               
+  SideEffects []
 
-            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
-        }
-        return RetValue;
-    }
+  SeeAlso     []
 
-    Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
-  
-    fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
-    fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
-    if ( fComp23 >= 0 ) // Cof2 >= Cof3 
+***********************************************************************/
+static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
+{   
+    int nWords = Abc_TtWordNum( nVars );
+    int k, Counter = 0;
+    for ( k = 0; k < nWords; k++ )
+        if ( pTruth[k] )
+            Counter += Abc_TtCountOnes( pTruth[k] );
+    return Counter;
+}
+static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
+{
+    word Temp;
+    int i, k, Counter, nWords;
+    if ( nVars <= 6 )
     {
-        if ( fComp01 >= 0 ) // Cof0 >= Cof1
-        {
-            fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
-            if ( fComp13 < 0 ) // Cof1 < Cof3 
-            {
-                Abc_TtFlip( pTruth, nWords, i + 1 );
-                *puCanonPhase ^= (1 << (i+1));
-                RetValue = 1;
-            }
-            else if ( fComp13 == 0 ) // Cof1 == Cof3 
-            {
-                fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
-                if ( fComp02 < 0 )
-                {
-                    Abc_TtFlip( pTruth, nWords, i + 1 );
-                    *puCanonPhase ^= (1 << (i+1));
-                    RetValue = 1;
-                }
-            }
-            // else   Cof1 > Cof3 -- do nothing
-        }
-        else // Cof0 < Cof1
-        {
-            fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
-            if ( fComp03 < 0 ) // Cof0 < Cof3
-            {
-                Abc_TtFlip( pTruth, nWords, i );
-                Abc_TtFlip( pTruth, nWords, i + 1 );
-                *puCanonPhase ^= (1 << i);
-                *puCanonPhase ^= (1 << (i+1));
-                RetValue = 1;
-            }
-            else //  Cof0 >= Cof3
-            {
-                if ( fComp23 == 0 ) // can flip Cof0 and Cof1
-                {
-                    Abc_TtFlip( pTruth, nWords, i );
-                    *puCanonPhase ^= (1 << i);
-                    RetValue = 1;
-                }
-            }
-        }
+        for ( i = 0; i < nVars; i++ )
+            pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
+        return;
     }
-    else // Cof2 < Cof3 
+    assert( nVars > 6 );
+    nWords = Abc_TtWordNum( nVars );
+    memset( pStore, 0, sizeof(int) * nVars );
+    for ( k = 0; k < nWords; k++ )
     {
-        if ( fComp01 >= 0 ) // Cof0 >= Cof1
+        // count 1's for the first six variables
+        for ( i = 0; i < 6; i++ )
+            if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) )
+                pStore[i] += Abc_TtCountOnes( Temp );
+        // count 1's for all other variables
+        if ( pTruth[k] )
         {
-            fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
-            if ( fComp12 > 0 ) // Cof1 > Cof2 
-            {
-                Abc_TtFlip( pTruth, nWords, i );
-                *puCanonPhase ^= (1 << i);
-            }
-            else if ( fComp12 == 0 ) // Cof1 == Cof2 
-            {
-                Abc_TtFlip( pTruth, nWords, i );
-                Abc_TtFlip( pTruth, nWords, i + 1 );
-                *puCanonPhase ^= (1 << i);
-                *puCanonPhase ^= (1 << (i+1));
-            }
-            else // Cof1 < Cof2
-            {
-                Abc_TtFlip( pTruth, nWords, i + 1 );
-                *puCanonPhase ^= (1 << (i+1));
-                if ( fComp01 == 0 )
-                {
-                    Abc_TtFlip( pTruth, nWords, i );
-                    *puCanonPhase ^= (1 << i);
-                }
-            }
+            Counter = Abc_TtCountOnes( pTruth[k] );
+            for ( i = 6; i < nVars; i++ )
+                if ( (k & (1 << (i-6))) == 0 )
+                    pStore[i] += Counter;
         }
-        else // Cof0 < Cof1
+        k++;
+        // count 1's for all other variables
+        if ( pTruth[k] )
         {
-            fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
-            if ( fComp02 == -1 ) // Cof0 < Cof2 
-            {
-                Abc_TtFlip( pTruth, nWords, i );
-                Abc_TtFlip( pTruth, nWords, i + 1 );
-                *puCanonPhase ^= (1 << i);
-                *puCanonPhase ^= (1 << (i+1));
-            }
-            else if ( fComp02 == 0 ) // Cof0 == Cof2
-            {
-                fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
-                if ( fComp13 >= 0 ) // Cof1 >= Cof3 
-                {
-                    Abc_TtFlip( pTruth, nWords, i );
-                    *puCanonPhase ^= (1 << i);
-                }
-                else // Cof1 < Cof3 
-                {
-                    Abc_TtFlip( pTruth, nWords, i );
-                    Abc_TtFlip( pTruth, nWords, i + 1 );
-                    *puCanonPhase ^= (1 << i);
-                    *puCanonPhase ^= (1 << (i+1));
-                }
-            }
-            else // Cof0 > Cof2
-            {
-                Abc_TtFlip( pTruth, nWords, i );
-                *puCanonPhase ^= (1 << i);
-            }
+            Counter = Abc_TtCountOnes( pTruth[k] );
+            for ( i = 6; i < nVars; i++ )
+                if ( (k & (1 << (i-6))) == 0 )
+                    pStore[i] += Counter;
         }
-        RetValue = 1;
-    }
-    // perform final swap if needed
-    fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
-    if ( fComp12 < 0 ) // Cof1 < Cof2
-    {
-        Abc_TtSwapAdjacent( pTruth, nWords, i );
-        RetValue = 1;
+    } 
+}
 
-        if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
-        {
-            *puCanonPhase ^= (1 << i);
-            *puCanonPhase ^= (1 << (i+1));
-        }
+/**Function*************************************************************
 
-        ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
-    }
+  Synopsis    [Minterm counting in all cofactors.]
 
-    if ( RetValue == 1 )
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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++ )
     {
-        if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
-        {
-            Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
-            // undo the flips
-            *puCanonPhase = uPhaseInit; 
-            // undo the swap
-            if ( fComp12 < 0 ) // Cof1 < Cof2
-                ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
-            RetValue = 0;
-        }
+        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]];
     }
-    return RetValue;
 }
 
+/**Function*************************************************************
 
-void Abc_TtCofactorTest__( word * pTruth, int nVars, int N )
-{
-    char pCanonPerm[16];
-    unsigned uCanonPhase;
-    static word pCopy1[1024];
-    static word pCopy2[1024];
-    int i, nWords = Abc_TtWordNum( nVars );
-    static int Counter = 0;
+  Synopsis    [Minterm counting in all cofactors.]
 
-//    pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2];
-//    nVars = 3;
+  Description []
+               
+  SideEffects []
 
-/*
-    printf( "\n" );
-    Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
-    Abc_TtPrintBinary( pTruth, nVars );
-    printf( "\n" );
-*/
+  SeeAlso     []
 
-//    for ( i = nVars - 2; i >= 0; i-- )
-    for ( i = 3; i < nVars - 1; i++ )
+***********************************************************************/
+int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, 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 nMints0, nMints1;
+    if ( Truth == 0 )
+        return 0;
+    if ( ~Truth == 0 )
     {
-/*
-        word Cof0s = Abc_Tt6Cof0( pTruth[0], i+1 );
-        word Cof1s = Abc_Tt6Cof1( pTruth[0], i+1 );
-
-        word Cof0 = Abc_Tt6Cof0( Cof0s, i );
-        word Cof1 = Abc_Tt6Cof1( Cof0s, i );
-        word Cof2 = Abc_Tt6Cof0( Cof1s, i );
-        word Cof3 = Abc_Tt6Cof1( Cof1s, i );
-
-        Abc_TtPrintBinary( &Cof0, 6 );
-        Abc_TtPrintBinary( &Cof1, 6 );
-        Abc_TtPrintBinary( &Cof2, 6 );
-        Abc_TtPrintBinary( &Cof3, 6 );
-
-        printf( "01 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) );
-        printf( "02 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) );
-        printf( "03 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) );
-        printf( "12 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) );
-        printf( "13 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) );
-        printf( "23 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) );
-
-        if ( i == 0 && N == 74 )
+        int i;
+        for ( i = 0; i <= iVar; i++ )
+            pStore[i] += nBytes * 4;
+        return nBytes * 8;
+    }
+    if ( nBytes == 1 )
+    {
+        assert( iVar == 2 );
+        pStore[0] += bit_count[ Truth & 0x55 ];
+        pStore[1] += bit_count[ Truth & 0x33 ];
+        pStore[2] += bit_count[ Truth & 0x0F ];
+        return bit_count[ Truth & 0xFF ];
+    }
+    nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof0(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof1(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    pStore[iVar] += nMints0;
+    return nMints0 + nMints1;
+}
+
+int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore )
+{
+    int nMints0, nMints1;
+    if ( nWords == 1 )
+    {
+        assert( iVar == 5 );
+        return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore );
+    }
+    assert( nWords > 1 );
+    assert( iVar > 5 );
+    if ( pTruth[0] & 1 )
+    {
+        if ( Abc_TtIsConst1( pTruth, nWords ) )
         {
-            int s = 0;
-            continue;
+            int i;
+            for ( i = 0; i <= iVar; i++ )
+                pStore[i] += nWords * 32;
+            return nWords * 64;
         }
-*/
-        Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
-        Abc_TtCofactorPermNaive( pCopy1, i, nWords, 0 );
-
-        Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
-        Abc_TtCofactorPerm( pCopy2, i, nWords, pCanonPerm, &uCanonPhase, 0 );
-
-//        assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
-        if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
-            Counter++;
-
     }
-    if ( Counter % 1000 == 0 )
-        printf( "%d ", Counter );
-
+    else 
+    {
+        if ( Abc_TtIsConst0( pTruth, nWords ) )
+            return 0;
+    }
+    nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth,            iVar - 1, nWords/2, pStore );
+    nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore );
+    pStore[iVar] += nMints0;
+    return nMints0 + nMints1;
+}
+int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore )
+{
+    memset( pStore, 0, sizeof(int) * nVars );
+    assert( nVars >= 3 );
+    if ( nVars <= 6 )
+        return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore );
+    else
+        return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore );
 }
 
 
+/**Function*************************************************************
 
-void Abc_TtCofactorTest8( word * pTruth, int nVars, int N )
-{
-    int fVerbose = 0;
-    int i;
-    int nWords = Abc_TtWordNum( nVars );
+  Synopsis    []
 
-    if ( fVerbose )
-        printf( "\n   " ), Abc_TtPrintHex( pTruth, nVars );
+  Description []
+               
+  SideEffects []
 
-    if ( fVerbose )
-    printf( "Round 1\n" );
-    for ( i = nVars - 2; i >= 0; i-- )
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut )
+{
+    int fOldSwap = 0;
+    int pStoreIn[17];
+    int * pStore = pStoreOut ? pStoreOut : pStoreIn;
+    int i, nOnes, nWords = Abc_TtWordNum( nVars );
+    unsigned uCanonPhase = 0;
+    assert( nVars <= 16 );
+    for ( i = 0; i < nVars; i++ )
+        pCanonPerm[i] = i;
+    // normalize polarity    
+    nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
+    if ( nOnes > nWords * 32 )
     {
-        if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
-        {
-            if ( fVerbose )
-                printf( "%d  ", i ), Abc_TtPrintHex( pTruth, nVars );
-        }
+        Abc_TtNot( pTruth, nWords );
+        nOnes = nWords*64 - nOnes;
+        uCanonPhase |= (1 << nVars);
     }
-
-    if ( fVerbose )
-    printf( "Round 2\n" );
-    for ( i = 0; i < nVars - 1; i++ )
+    // normalize phase
+    Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+    pStore[nVars] = nOnes;
+    for ( i = 0; i < nVars; i++ )
     {
-        if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
-        {
-            if ( fVerbose )
-                printf( "%d  ", i ), Abc_TtPrintHex( pTruth, nVars );
-        }
+        if ( pStore[i] >= nOnes - pStore[i] )
+            continue;
+        Abc_TtFlip( pTruth, nWords, i );
+        uCanonPhase |= (1 << i);
+        pStore[i] = nOnes - pStore[i]; 
     }
-
-    return;
-
-    if ( fVerbose )
-    printf( "Round 3\n" );
-    for ( i = nVars - 2; i >= 0; i-- )
+    // normalize permutation
+    if ( fOldSwap )
     {
-        if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
-        {
-            if ( fVerbose )
-                printf( "%d  ", i ), Abc_TtPrintHex( pTruth, nVars );
-        }
+        int fChange;
+        do {
+            fChange = 0;
+            for ( i = 0; i < nVars-1; i++ )
+            {
+                if ( pStore[i] <= pStore[i+1] )
+    //            if ( pStore[i] >= pStore[i+1] )
+                    continue;
+                ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
+                ABC_SWAP( int, pStore[i], pStore[i+1] );
+                if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
+                {
+                    uCanonPhase ^= (1 << i);
+                    uCanonPhase ^= (1 << (i+1));
+                }
+                Abc_TtSwapAdjacent( pTruth, nWords, i );            
+                fChange = 1;
+    //            nSwaps++;
+            }
+        } 
+        while ( fChange );
     }
-
-    if ( fVerbose )
-    printf( "Round 4\n" );
-    for ( i = 0; i < nVars - 1; i++ )
+    else
     {
-        if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
+        int k, BestK;
+        for ( i = 0; i < nVars - 1; i++ )
         {
-            if ( fVerbose )
-                printf( "%d  ", i ), Abc_TtPrintHex( pTruth, nVars );
+            BestK = i + 1;
+            for ( k = i + 2; k < nVars; k++ )
+                if ( pStore[BestK] > pStore[k] )
+    //            if ( pStore[BestK] < pStore[k] )
+                    BestK = k;
+            if ( pStore[i] <= pStore[BestK] )
+    //        if ( pStore[i] >= pStore[BestK] )
+                continue;
+            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
+            ABC_SWAP( int, pStore[i], pStore[BestK] );
+            if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
+            {
+                uCanonPhase ^= (1 << i);
+                uCanonPhase ^= (1 << BestK);
+            }
+            Abc_TtSwapVars( pTruth, nVars, i, BestK );
+    //        nSwaps++;
         }
     }
-    i = 0;
+    return uCanonPhase;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_TtCofactorTest10( word * pTruth, int nVars, int N )
 {
     static word pCopy1[1024];
     static word pCopy2[1024];
     int nWords = Abc_TtWordNum( nVars );
     int i;
-
     for ( i = 0; i < nVars - 1; i++ )
     {
 //        Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
-
         Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
         Abc_TtSwapAdjacent( pCopy1, nWords, i );
 //        Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
-
         Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
         Abc_TtSwapVars( pCopy2, nVars, i, i+1 );
 //        Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
-
         assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
     }
 }
 
+/**Function*************************************************************
 
-void Abc_TtCofactorTest111( word * pTruth, int nVars, int N )
-{
-    char pCanonPerm[32];
-    static word pCopy1[1024];
-    static word pCopy2[1024];
-    int nWords = Abc_TtWordNum( nVars );
-
-//        Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
+  Synopsis    [Naive evaluation.]
 
-    Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
-//    Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm );
-//        Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
+  Description []
+               
+  SideEffects []
 
-    Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
-    Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL );
-//        Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
+  SeeAlso     []
 
-    assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
+***********************************************************************/
+int Abc_Tt6CofactorPermNaive( word * pTruth, int i, int fSwapOnly )
+{
+    if ( fSwapOnly )
+    {
+        word Copy = Abc_Tt6SwapAdjacent( pTruth[0], i );
+        if ( pTruth[0] > Copy )
+        {
+            pTruth[0] = Copy;
+            return 4;
+        }
+        return 0;
+    }
+    {
+        word Copy = pTruth[0];
+        word Best = pTruth[0];
+        int Config = 0;
+        // PXY
+        // 001
+        Copy = Abc_Tt6Flip( Copy, i );
+        if ( Best > Copy )
+            Best = Copy, Config = 1;
+        // PXY
+        // 011
+        Copy = Abc_Tt6Flip( Copy, i+1 );
+        if ( Best > Copy )
+            Best = Copy, Config = 3;
+        // PXY
+        // 010
+        Copy = Abc_Tt6Flip( Copy, i );
+        if ( Best > Copy )
+            Best = Copy, Config = 2;
+        // PXY
+        // 110
+        Copy = Abc_Tt6SwapAdjacent( Copy, i );
+        if ( Best > Copy )
+            Best = Copy, Config = 6;
+        // PXY
+        // 111
+        Copy = Abc_Tt6Flip( Copy, i+1 );
+        if ( Best > Copy )
+            Best = Copy, Config = 7;
+        // PXY
+        // 101
+        Copy = Abc_Tt6Flip( Copy, i );
+        if ( Best > Copy )
+            Best = Copy, Config = 5;
+        // PXY
+        // 100
+        Copy = Abc_Tt6Flip( Copy, i+1 );
+        if ( Best > Copy )
+            Best = Copy, Config = 4;
+        // PXY
+        // 000
+        Copy = Abc_Tt6SwapAdjacent( Copy, i );
+        assert( Copy == pTruth[0] );
+        assert( Best <= pTruth[0] );
+        pTruth[0] = Best;
+        return Config;
+    }
+}
+int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
+{
+    if ( fSwapOnly )
+    {
+        static word pCopy[1024];
+        Abc_TtCopy( pCopy, pTruth, nWords, 0 );
+        Abc_TtSwapAdjacent( pCopy, nWords, i );
+        if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
+        {
+            Abc_TtCopy( pTruth, pCopy, nWords, 0 );
+            return 4;
+        }
+        return 0;
+    }
+    {
+        static word pCopy[1024];
+        static word pBest[1024];
+        int Config = 0;
+        // save two copies
+        Abc_TtCopy( pCopy, pTruth, nWords, 0 );
+        Abc_TtCopy( pBest, pTruth, nWords, 0 );
+        // PXY
+        // 001
+        Abc_TtFlip( pCopy, nWords, i );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 1;
+        // PXY
+        // 011
+        Abc_TtFlip( pCopy, nWords, i+1 );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 3;
+        // PXY
+        // 010
+        Abc_TtFlip( pCopy, nWords, i );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 2;
+        // PXY
+        // 110
+        Abc_TtSwapAdjacent( pCopy, nWords, i );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 6;
+        // PXY
+        // 111
+        Abc_TtFlip( pCopy, nWords, i+1 );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 7;
+        // PXY
+        // 101
+        Abc_TtFlip( pCopy, nWords, i );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 5;
+        // PXY
+        // 100
+        Abc_TtFlip( pCopy, nWords, i+1 );
+        if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+            Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 4;
+        // PXY
+        // 000
+        Abc_TtSwapAdjacent( pCopy, nWords, i );
+        assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
+        if ( Config == 0 )
+            return 0;
+        assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
+        Abc_TtCopy( pTruth, pBest, nWords, 0 );
+        return Config;
+    }
 }
 
 
+/**Function*************************************************************
 
+  Synopsis    [Smart evaluation.]
 
-void Abc_TtCofactorMinimize( word * pTruth, int nVars, int N )
-{
-    char pCanonPerm[16];
-    unsigned uCanonPhase;
-    int i, fVerbose = 0;
-    int nWords = Abc_TtWordNum( nVars );
+  Description []
+               
+  SideEffects []
 
-    if ( fVerbose )
-        printf( "\n   " ), Abc_TtPrintHex( pTruth, nVars );
+  SeeAlso     []
 
-    if ( fVerbose )
-    printf( "Round 1\n" );
-    for ( i = nVars - 2; i >= 0; i-- )
+***********************************************************************/
+int Abc_TtCofactorPermConfig( word * pTruth, int i, int nWords, int fSwapOnly, int fNaive )
+{
+    if ( nWords == 1 )
+        return Abc_Tt6CofactorPermNaive( pTruth, i, fSwapOnly );
+    if ( fNaive )
+        return Abc_TtCofactorPermNaive( pTruth, i, nWords, fSwapOnly );
+    if ( fSwapOnly )
     {
-        if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
+        if ( Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ) < 0 ) // Cof1 < Cof2
         {
-            if ( fVerbose )
-                printf( "%d  ", i ), Abc_TtPrintHex( pTruth, nVars );
+            Abc_TtSwapAdjacent( pTruth, nWords, i );
+            return 4;
         }
+        return 0;
     }
-
-    if ( fVerbose )
-    printf( "Round 2\n" );
-    for ( i = 0; i < nVars - 1; i++ )
-    {
-        if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
+    {  
+        int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0;
+        fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
+        fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
+        if ( fComp23 >= 0 ) // Cof2 >= Cof3 
         {
-            if ( fVerbose )
-                printf( "%d  ", i ), Abc_TtPrintHex( pTruth, nVars );
+            if ( fComp01 >= 0 ) // Cof0 >= Cof1
+            {
+                fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
+                if ( fComp13 < 0 ) // Cof1 < Cof3 
+                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
+                else if ( fComp13 == 0 ) // Cof1 == Cof3 
+                {
+                    fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
+                    if ( fComp02 < 0 )
+                        Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
+                }
+                // else   Cof1 > Cof3 -- do nothing
+            }
+            else // Cof0 < Cof1
+            {
+                fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
+                if ( fComp03 < 0 ) // Cof0 < Cof3
+                {
+                    Abc_TtFlip( pTruth, nWords, i );
+                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+                }
+                else //  Cof0 >= Cof3
+                {
+                    if ( fComp23 == 0 ) // can flip Cof0 and Cof1
+                        Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+                }
+            }
+        }
+        else // Cof2 < Cof3 
+        {
+            if ( fComp01 >= 0 ) // Cof0 >= Cof1
+            {
+                fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
+                if ( fComp12 > 0 ) // Cof1 > Cof2 
+                    Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+                else if ( fComp12 == 0 ) // Cof1 == Cof2 
+                {
+                    Abc_TtFlip( pTruth, nWords, i );
+                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+                }
+                else // Cof1 < Cof2
+                {
+                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
+                    if ( fComp01 == 0 )
+                        Abc_TtFlip( pTruth, nWords, i ), Config ^= 1;
+                }
+            }
+            else // Cof0 < Cof1
+            {
+                fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
+                if ( fComp02 == -1 ) // Cof0 < Cof2 
+                {
+                    Abc_TtFlip( pTruth, nWords, i );
+                    Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+                }
+                else if ( fComp02 == 0 ) // Cof0 == Cof2
+                {
+                    fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
+                    if ( fComp13 >= 0 ) // Cof1 >= Cof3 
+                        Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+                    else // Cof1 < Cof3 
+                    {
+                        Abc_TtFlip( pTruth, nWords, i );
+                        Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+                    }
+                }
+                else // Cof0 > Cof2
+                    Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+            }
         }
+        // perform final swap if needed
+        fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
+        if ( fComp12 < 0 ) // Cof1 < Cof2
+            Abc_TtSwapAdjacent( pTruth, nWords, i ), Config ^= 4;
+        return Config;
     }
 }
-
-
-void Abc_TtCofactorVerify( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
+int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char * pCanonPerm, unsigned * puCanonPhase, int fNaive )
 {
-    int i, k, nWords = Abc_TtWordNum( nVars );
-    if ( (uCanonPhase >> nVars) & 1 )
-        Abc_TtNot( pTruth, nWords );
-    for ( i = 0; i < nVars; i++ )
-        if ( (uCanonPhase >> i) & 1 )
-            Abc_TtFlip( pTruth, nWords, i );
-    for ( i = 0; i < nVars; i++ )
+    if ( fSwapOnly )
     {
-        for ( k = i; k < nVars; k++ )
-            if ( pCanonPerm[k] == i )
-                break;
-        assert( k < nVars );
-        if ( i == k )
-            continue;
-        Abc_TtSwapVars( pTruth, nVars, i, k );
-        ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
+        int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 );
+        if ( Config )
+        {
+            if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
+            {
+                *puCanonPhase ^= (1 << i);
+                *puCanonPhase ^= (1 << (i+1));
+            }
+            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
+        }
+        return Config;
+    }
+    {
+        static word pCopy1[1024];
+        int Config;
+        Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
+        Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 0, fNaive );
+        if ( Config == 0 )
+            return 0;
+        if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
+        {
+            Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
+            return 0;
+        }
+        // improved
+        if ( Config & 1 )
+            *puCanonPhase ^= (1 << i);
+        if ( Config & 2 )
+            *puCanonPhase ^= (1 << (i+1));
+        if ( Config & 4 )
+        {
+            if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
+            {
+                *puCanonPhase ^= (1 << i);
+                *puCanonPhase ^= (1 << (i+1));
+            }
+            ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
+        }
+        return Config;
     }
 }
 
-//#define CANON_VERIFY
+/**Function*************************************************************
+
+  Synopsis    [Semi-canonical form computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
 
-void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
+***********************************************************************/
+//#define CANON_VERIFY
+unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
 {
     int pStoreIn[17];
-    char pCanonPerm[16];
     unsigned uCanonPhase;
-    int i, nWords = Abc_TtWordNum( nVars );
+    int i, k, nWords = Abc_TtWordNum( nVars );
+    int fNaive = 1;
 
 #ifdef CANON_VERIFY
     char pCanonPermCopy[16];
@@ -795,31 +899,26 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
 #endif
 
     uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
-
-    for ( i = nVars - 2; i >= 0; i-- )
-        if ( pStoreIn[i] == pStoreIn[i+1] )
-            Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-//            Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
-
-    for ( i = 1; i < nVars - 1; i++ )
-        if ( pStoreIn[i] == pStoreIn[i+1] )
-            Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-//            Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
-
-    for ( i = nVars - 3; i >= 0; i-- )
-        if ( pStoreIn[i] == pStoreIn[i+1] )
-            Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-//            Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
-
-    for ( i = 1; i < nVars - 1; i++ )
-        if ( pStoreIn[i] == pStoreIn[i+1] )
-            Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-//            Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
+    for ( k = 0; k < 3; k++ )
+    {
+        int fChanges = 0;
+        for ( i = nVars - 2; i >= 0; i-- )
+            if ( pStoreIn[i] == pStoreIn[i+1] )
+                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
+        if ( !fChanges )
+            break;
+        fChanges = 0;
+        for ( i = 1; i < nVars - 1; i++ )
+            if ( pStoreIn[i] == pStoreIn[i+1] )
+                fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
+        if ( !fChanges )
+            break;
+    }
 
 #ifdef CANON_VERIFY
     Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
     memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
-    Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
+    Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
     if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
         printf( "Canonical form verification failed!\n" );
 #endif
@@ -831,6 +930,7 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
         i = 0;
     }
 */
+    return uCanonPhase;
 }