Version abc70328

3 files changed, 289 insertions, 71 deletions

diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 5d37a9e9..d779df7b 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -200,6 +200,23 @@ static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVa
             return 0;
     return 1;
 }
+static inline int Kit_TruthIsEqualWithPhase( unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    if ( (pIn0[0] & 1) == (pIn1[0] & 1) )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            if ( pIn0[w] != pIn1[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            if ( pIn0[w] != ~pIn1[w] )
+                return 0;
+    }
+    return 1;
+}
 static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
 {
     int w;
@@ -288,6 +305,30 @@ static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * p
     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = ~(pIn0[w] & pIn1[w]);
 }
+static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
+{
+    int w;
+    if ( fCompl0 && fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = ~(pIn0[w] | pIn1[w]);
+    }
+    else if ( fCompl0 && !fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = ~pIn0[w] & pIn1[w];
+    }
+    else if ( !fCompl0 && fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = pIn0[w] & ~pIn1[w];
+    }
+    else // if ( !fCompl0 && !fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = pIn0[w] & pIn1[w];
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                           ITERATORS                              ///
@@ -345,8 +386,8 @@ extern int             Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, in
 extern void            Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory );
 /*=== kitTruth.c ==========================================================*/
 extern void            Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
-extern void            Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
-extern void            Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
+extern void            Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
+extern void            Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
 extern int             Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthSupportSize( unsigned * pTruth, int nVars );
 extern unsigned        Kit_TruthSupport( unsigned * pTruth, int nVars );
@@ -364,6 +405,7 @@ extern void            Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern void            Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
+extern void            Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
 extern unsigned        Kit_TruthHash( unsigned * pIn, int nWords );
 extern unsigned        Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
 
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 0068a29a..b85aa4a4 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -40,23 +40,23 @@ typedef enum {
 
 struct Dsd_Obj_t_
 { 
-    unsigned       uSupp;              // the support of this node
-    unsigned       Id          :  6;   // the number of this node
-    unsigned       Type        :  3;   // none, const, var, AND, XOR, MUX, PRIME
-    unsigned       fMark       :  1;   // finished checking output
-    unsigned       Offset      : 16;   // offset to the truth table
-    unsigned       nFans       :  6;   // the number of fanins of this node
-    unsigned char  pFans[0];           // the fanin literals
+    unsigned       Id         : 6;  // the number of this node
+    unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
+    unsigned       fMark      : 1;  // finished checking output
+    unsigned       Offset     : 8;  // offset to the truth table
+    unsigned       nRefs      : 8;  // offset to the truth table
+    unsigned       nFans      : 6;  // the number of fanins of this node
+    unsigned char  pFans[0];        // the fanin literals
 };
 
 struct Dsd_Ntk_t_
 {
-    unsigned char  nVars;              // at most 16 (perhaps 18?)
-    unsigned char  nNodesAlloc;        // the number of allocated nodes (at most nVars)
-    unsigned char  nNodes;             // the number of nodes
-    unsigned char  Root;               // the root of the tree
-    unsigned *     pMem;               // memory for the truth tables (memory manager?)
-    Dsd_Obj_t *    pNodes[0];          // the nodes
+    unsigned char  nVars;           // at most 16 (perhaps 18?)
+    unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
+    unsigned char  nNodes;          // the number of nodes
+    unsigned char  Root;            // the root of the tree
+    unsigned *     pMem;            // memory for the truth tables (memory manager?)
+    Dsd_Obj_t *    pNodes[0];       // the nodes
 };
 
 static inline unsigned     Dsd_ObjOffset( int nFans )        { return (nFans >> 2) + ((nFans & 3) > 0); }
@@ -93,8 +93,8 @@ Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans )
     int nSize = sizeof(Dsd_Obj_t) + sizeof(unsigned) * (Dsd_ObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
     pObj = (Dsd_Obj_t *)ALLOC( char, nSize );
     memset( pObj, 0, nSize );
-    pObj->Type = Type;
     pObj->Id = pNtk->nVars + pNtk->nNodes;
+    pObj->Type = Type;
     pObj->nFans = nFans;
     pObj->Offset = Dsd_ObjOffset( nFans );
     // add the object
@@ -298,34 +298,32 @@ int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * pPar )
+void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, unsigned char * pPar )
 {
     Dsd_Obj_t * pRes, * pRes0, * pRes1;
     int nWords = Kit_TruthWordNum(pObj->nFans);
     unsigned * pTruth = Dsd_ObjTruth(pObj);
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
     unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
-    int nFans0, nFans1, iVar0, iVar1, nPairs;
+    int i, iVar0, iVar1, nFans0, nFans1, nPairs;
     int fEquals[2][2], fOppos, fPairs[4][4];
     unsigned j, k, nFansNew, uSupp0, uSupp1;
-    int i;
 
     assert( pObj->nFans > 0 );
     assert( pObj->Type == KIT_DSD_PRIME );
-    assert( pObj->uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
+    assert( uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
 
     // compress the truth table
-    if ( pObj->uSupp != Kit_BitMask(pObj->nFans) )
+    if ( uSupp != Kit_BitMask(pObj->nFans) )
     {
-        nFansNew = Kit_WordCountOnes(pObj->uSupp);
-        Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, pObj->uSupp );
-        Kit_TruthCopy( pTruth, pNtk->pMem, pObj->nFans );
+        nFansNew = Kit_WordCountOnes(uSupp);
+        Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, uSupp, 1 );
         for ( j = k = 0; j < pObj->nFans; j++ )
-            if ( pObj->uSupp & (1 << j) )
+            if ( uSupp & (1 << j) )
                 pObj->pFans[k++] = pObj->pFans[j];
         assert( k == nFansNew );
         pObj->nFans = k;
-        pObj->uSupp = Kit_BitMask(pObj->nFans);
+        uSupp = Kit_BitMask(pObj->nFans);
     }
 
     // consider the single variable case
@@ -363,7 +361,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             // check the MUX decomposition
             uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
             uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
-            assert( pObj->uSupp == (uSupp0 | uSupp1 | (1<<i)) );
+            assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
             if ( uSupp0 & uSupp1 )
                 continue;
             // perform MUX decomposition
@@ -376,25 +374,24 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             }
             Kit_TruthCopy( Dsd_ObjTruth(pRes0), pCofs2[0], pObj->nFans );        
             Kit_TruthCopy( Dsd_ObjTruth(pRes1), pCofs2[1], pObj->nFans ); 
-            pRes0->uSupp = uSupp0;
-            pRes1->uSupp = uSupp1;
             // update the current one
             pObj->Type = KIT_DSD_MUX;
             pObj->nFans = 3;
             pObj->pFans[0] = pObj->pFans[i];
-            pObj->pFans[1] = 2*pRes1->Id;
-            pObj->pFans[2] = 2*pRes0->Id;
+            pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
+            pObj->pFans[2] = 2*pRes0->Id; pRes0->nRefs++;
             // call recursively
-            Kit_DsdDecompose_rec( pNtk, pRes0, pObj->pFans + 2 );
-            Kit_DsdDecompose_rec( pNtk, pRes1, pObj->pFans + 1 );
+            Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 2 );
+            Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
             return;
         }
 //Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
 
         // create the new node
         pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+        pRes->nRefs++;
         pRes->nFans = 2;
-        pRes->pFans[0] = pObj->pFans[i];  pObj->pFans[i] = 127;  pObj->uSupp &= ~(1 << i);
+        pRes->pFans[0] = pObj->pFans[i];  pObj->pFans[i] = 127;  uSupp &= ~(1 << i);
         pRes->pFans[1] = 2*pObj->Id;
         // update the parent pointer
         *pPar = 2 * pRes->Id;
@@ -430,7 +427,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             assert( 0 );
         // decompose the remainder
         assert( Dsd_ObjTruth(pObj) == pTruth );
-        Kit_DsdDecompose_rec( pNtk, pObj, pRes->pFans + 1 );
+        Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1 );
         return;
     }
     pObj->fMark = 1;
@@ -445,11 +442,12 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
         // check the existence of MUX decomposition
         uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
         uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
-        // if one of the cofs is a constant, it is time to check it again
+        assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
+        // if one of the cofs is a constant, it is time to check the output again
         if ( uSupp0 == 0 || uSupp1 == 0 )
         {
             pObj->fMark = 0;
-            Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
             return;
         }
         assert( uSupp0 && uSupp1 );
@@ -475,17 +473,18 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             {
                 // construct the MUX
                 pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_MUX, 3 );
+                pRes->nRefs++;
                 pRes->nFans = 3;
                 pRes->pFans[0] = pObj->pFans[i];     pObj->pFans[i] = 2 * pRes->Id; // remains in support
-                pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127;  pObj->uSupp &= ~(1 << iVar1);
-                pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127;  pObj->uSupp &= ~(1 << iVar0);
+                pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127;  uSupp &= ~(1 << iVar1);
+                pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127;  uSupp &= ~(1 << iVar0);
                 // update the node
                 if ( fEquals[0][0] && fEquals[0][1] )
                     Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
                 else
                     Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
                 // decompose the remainder
-                Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+                Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
                 return;
             }
         }
@@ -499,21 +498,22 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10 
             Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11 
             // compare equal pairs
-            fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[0][1], pObj->nFans);
-            fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][0], pObj->nFans);
-            fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][1], pObj->nFans);
-            fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][0], pObj->nFans);
-            fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][1], pObj->nFans);
-            fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual(pCofs4[1][0], pCofs4[1][1], pObj->nFans);
+            fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[0][1], pObj->nFans );
+            fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
+            fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
+            fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
+            fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
+            fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual( pCofs4[1][0], pCofs4[1][1], pObj->nFans );
             nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3];
             if ( nPairs != 3 && nPairs != 2 )
                 continue;
 
             // decomposition exists
             pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+            pRes->nRefs++;
             pRes->nFans = 2;
-            pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id;  // remains the support
-            pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127;       pObj->uSupp &= ~(1 << i);
+            pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id;  // remains in support
+            pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127;       uSupp &= ~(1 << i);
             if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
             {
                 pRes->pFans[0] ^= 1;  
@@ -548,7 +548,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
                 Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
             }
             // decompose the remainder
-            Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
             return;
         }
     }
@@ -569,6 +569,7 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 {
     Dsd_Ntk_t * pNtk;
     Dsd_Obj_t * pObj;
+    unsigned uSupp;
     int i, nVarsReal;
     assert( nVars <= 16 );
     pNtk = Kit_DsdNtkAlloc( pTruth, nVars );
@@ -579,9 +580,9 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
     for ( i = 0; i < nVars; i++ )
        pObj->pFans[i] = 2*i;
     Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars );
-    pObj->uSupp = Kit_TruthSupport( pTruth, nVars );
+    uSupp = Kit_TruthSupport( pTruth, nVars );
     // consider special cases
-    nVarsReal = Kit_WordCountOnes( pObj->uSupp );
+    nVarsReal = Kit_WordCountOnes( uSupp );
     if ( nVarsReal == 0 )
     {
         pObj->Type = KIT_DSD_CONST1;
@@ -593,11 +594,11 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
     {
         pObj->Type = KIT_DSD_VAR;
         pObj->nFans = 1;
-        pObj->pFans[0] = 2 * Kit_WordFindFirstBit( pObj->uSupp );
+        pObj->pFans[0] = 2 * Kit_WordFindFirstBit( uSupp );
         pObj->pFans[0] ^= (pTruth[0] & 1);
         return pNtk;
     }
-    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], &pNtk->Root );
+    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root );
     return pNtk;
 }
 
@@ -615,16 +616,15 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
 {
     Dsd_Ntk_t * pNtk0, * pNtk1;
-    Dsd_Obj_t * pRoot;
+//    Dsd_Obj_t * pRoot;
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
     unsigned i, * pTruth;
     int fVerbose = 1;
 
-//    pTruth = pTruthInit;
-
-    pRoot = Dsd_NtkRoot(pNtk);
-    pTruth = Dsd_ObjTruth(pRoot);
-    assert( pRoot->nFans == pNtk->nVars );
+    pTruth = pTruthInit;
+//    pRoot = Dsd_NtkRoot(pNtk);
+//    pTruth = Dsd_ObjTruth(pRoot);
+//    assert( pRoot->nFans == pNtk->nVars );
 
     if ( fVerbose )
     {
@@ -632,6 +632,7 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
 //        Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) ); 
         Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars ); 
         printf( "\n" );
+        Kit_DsdPrint( stdout, pNtk );
     }
     for ( i = 0; i < pNtk->nVars; i++ )
     {
@@ -676,8 +677,9 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 //    if ( Kit_DsdFindLargeBox(pNtk, Dsd_NtkRoot(pNtk)) )
 //        Kit_DsdPrint( stdout, pNtk );
 
-    if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 8 )
-        Kit_DsdTestCofs( pNtk, pTruth );
+//    if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
+
+    Kit_DsdTestCofs( pNtk, pTruth );
 
     Kit_DsdNtkFree( pNtk );
 }
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 5ac85524..62d4cf14 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -168,7 +168,7 @@ void Kit_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
+void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
 {
     unsigned * pTemp;
     int i, k, Var = nVars - 1, Counter = 0;
@@ -185,7 +185,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
         }
     assert( Var == -1 );
     // swap if it was moved an even number of times
-    if ( !(Counter & 1) )
+    if ( fReturnIn ^ !(Counter & 1) )
         Kit_TruthCopy( pOut, pIn, nVarsAll );
 }
 
@@ -202,7 +202,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
+void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
 {
     unsigned * pTemp;
     int i, k, Var = 0, Counter = 0;
@@ -219,7 +219,7 @@ void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
         }
     assert( Var == nVars );
     // swap if it was moved an even number of times
-    if ( !(Counter & 1) )
+    if ( fReturnIn ^ !(Counter & 1) )
         Kit_TruthCopy( pOut, pIn, nVarsAll );
 }
 
@@ -1080,6 +1080,28 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1's in each cofactor.]
+
+  Description [Verifies the above procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
+        pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
+        Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
+        pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
+    }
+}
 
 /**Function*************************************************************
 
@@ -1191,6 +1213,7 @@ unsigned Kit_TruthHash( unsigned * pIn, int nWords )
 ***********************************************************************/
 unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore )
 {
+//    short pStore2[32];
     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
     int nWords = Kit_TruthWordNum( nVars );
     int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
@@ -1198,20 +1221,26 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
 
     // canonicize output
     uCanonPhase = 0;
+/*
     nOnes = Kit_TruthCountOnes(pIn, nVars);
-    if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
+    if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
     {
         uCanonPhase |= (1 << nVars);
         Kit_TruthNot( pIn, pIn, nVars );
     }
-
+*/
     // collect the minterm counts
     Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
+//    Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
+//    for ( i = 0; i < 2*nVars; i++ )
+//    {
+//        assert( pStore[i] == pStore2[i] );
+//    }
 
     // canonicize phase
     for ( i = 0; i < nVars; i++ )
     {
-        if ( pStore[2*i+0] <= pStore[2*i+1] )
+        if ( pStore[2*i+0] >= pStore[2*i+1] )
             continue;
         uCanonPhase |= (1 << i);
         Temp = pStore[2*i+0];
@@ -1229,7 +1258,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
         fChange = 0;
         for ( i = 0; i < nVars-1; i++ )
         {
-            if ( pStore[2*i] <= pStore[2*(i+1)] )
+            if ( pStore[2*i] >= pStore[2*(i+1)] )
                 continue;
             Counter++;
             fChange = 1;
@@ -1246,17 +1275,24 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
             pStore[2*i+1] = pStore[2*(i+1)+1];
             pStore[2*(i+1)+1] = Temp;
 
+            // if the polarity of variables is different, swap them
+            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
+            {
+                uCanonPhase ^= (1 << i);
+                uCanonPhase ^= (1 << (i+1));
+            }
+
             Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
             pTemp = pIn; pIn = pOut; pOut = pTemp;
         }
     } while ( fChange );
 
 /*
-    Kit_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
+    Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
     for ( i = 0; i < nVars; i++ )
         printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
     printf( "  C = %d\n", Counter );
-    Kit_PrintHexadecimal( stdout, pIn, nVars );
+    Extra_PrintHexadecimal( stdout, pIn, nVars );
     printf( "\n" );
 */
 
@@ -1337,6 +1373,144 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
     return uCanonPhase;
 }
 
+ 
+/**Function*************************************************************
+
+  Synopsis    [Fast counting minterms in the cofactors of a function.]
+
+  Description [Returns the total number of minterms in the function.
+  The resulting array (pRes) contains the number of minterms in 0-cofactor
+  w.r.t. each variables. The additional array (pBytes) is used for internal 
+  storage. It should have the size equal to the number of truth table bytes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytes )
+{
+    // the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
+    static unsigned Table[256] = {
+        0x00000000, 0x01010101, 0x01010001, 0x02020102, 0x01000101, 0x02010202, 0x02010102, 0x03020203,
+        0x01000001, 0x02010102, 0x02010002, 0x03020103, 0x02000102, 0x03010203, 0x03010103, 0x04020204,
+        0x00010101, 0x01020202, 0x01020102, 0x02030203, 0x01010202, 0x02020303, 0x02020203, 0x03030304,
+        0x01010102, 0x02020203, 0x02020103, 0x03030204, 0x02010203, 0x03020304, 0x03020204, 0x04030305,
+        0x00010001, 0x01020102, 0x01020002, 0x02030103, 0x01010102, 0x02020203, 0x02020103, 0x03030204,
+        0x01010002, 0x02020103, 0x02020003, 0x03030104, 0x02010103, 0x03020204, 0x03020104, 0x04030205,
+        0x00020102, 0x01030203, 0x01030103, 0x02040204, 0x01020203, 0x02030304, 0x02030204, 0x03040305,
+        0x01020103, 0x02030204, 0x02030104, 0x03040205, 0x02020204, 0x03030305, 0x03030205, 0x04040306,
+        0x00000101, 0x01010202, 0x01010102, 0x02020203, 0x01000202, 0x02010303, 0x02010203, 0x03020304,
+        0x01000102, 0x02010203, 0x02010103, 0x03020204, 0x02000203, 0x03010304, 0x03010204, 0x04020305,
+        0x00010202, 0x01020303, 0x01020203, 0x02030304, 0x01010303, 0x02020404, 0x02020304, 0x03030405,
+        0x01010203, 0x02020304, 0x02020204, 0x03030305, 0x02010304, 0x03020405, 0x03020305, 0x04030406,
+        0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
+        0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
+        0x00020203, 0x01030304, 0x01030204, 0x02040305, 0x01020304, 0x02030405, 0x02030305, 0x03040406,
+        0x01020204, 0x02030305, 0x02030205, 0x03040306, 0x02020305, 0x03030406, 0x03030306, 0x04040407,
+        0x00000001, 0x01010102, 0x01010002, 0x02020103, 0x01000102, 0x02010203, 0x02010103, 0x03020204,
+        0x01000002, 0x02010103, 0x02010003, 0x03020104, 0x02000103, 0x03010204, 0x03010104, 0x04020205,
+        0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
+        0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
+        0x00010002, 0x01020103, 0x01020003, 0x02030104, 0x01010103, 0x02020204, 0x02020104, 0x03030205,
+        0x01010003, 0x02020104, 0x02020004, 0x03030105, 0x02010104, 0x03020205, 0x03020105, 0x04030206,
+        0x00020103, 0x01030204, 0x01030104, 0x02040205, 0x01020204, 0x02030305, 0x02030205, 0x03040306,
+        0x01020104, 0x02030205, 0x02030105, 0x03040206, 0x02020205, 0x03030306, 0x03030206, 0x04040307,
+        0x00000102, 0x01010203, 0x01010103, 0x02020204, 0x01000203, 0x02010304, 0x02010204, 0x03020305,
+        0x01000103, 0x02010204, 0x02010104, 0x03020205, 0x02000204, 0x03010305, 0x03010205, 0x04020306,
+        0x00010203, 0x01020304, 0x01020204, 0x02030305, 0x01010304, 0x02020405, 0x02020305, 0x03030406,
+        0x01010204, 0x02020305, 0x02020205, 0x03030306, 0x02010305, 0x03020406, 0x03020306, 0x04030407,
+        0x00010103, 0x01020204, 0x01020104, 0x02030205, 0x01010204, 0x02020305, 0x02020205, 0x03030306,
+        0x01010104, 0x02020205, 0x02020105, 0x03030206, 0x02010205, 0x03020306, 0x03020206, 0x04030307,
+        0x00020204, 0x01030305, 0x01030205, 0x02040306, 0x01020305, 0x02030406, 0x02030306, 0x03040407,
+        0x01020205, 0x02030306, 0x02030206, 0x03040307, 0x02020306, 0x03030407, 0x03030307, 0x04040408
+    };
+    unsigned uSum;
+    unsigned char * pTruthC, * pLimit;
+    int i, iVar, Step, nWords, nBytes, nTotal;
+
+    assert( nVars <= 20 );
+
+    // clear storage
+    memset( pRes, 0, sizeof(int) * nVars );
+
+    // count the number of one's in 0-cofactors of the first three variables
+    nTotal = uSum = 0;
+    nWords = Kit_TruthWordNum( nVars );
+    nBytes = nWords * 4;
+    pTruthC = (unsigned char *)pTruth;
+    pLimit = pTruthC + nBytes;
+    for ( ; pTruthC < pLimit; pTruthC++ )
+    {
+        uSum += Table[*pTruthC];
+        *pBytes++ = (Table[*pTruthC] & 0xff);
+        if ( (uSum & 0xff) > 246 )
+        {
+            nTotal += (uSum & 0xff);
+            pRes[0] += ((uSum >>  8) & 0xff);
+            pRes[2] += ((uSum >> 16) & 0xff);
+            pRes[3] += ((uSum >> 24) & 0xff);
+            uSum = 0;
+        }
+    }
+    if ( uSum )
+    {
+        nTotal += (uSum & 0xff);
+        pRes[0] += ((uSum >>  8) & 0xff);
+        pRes[1] += ((uSum >> 16) & 0xff);
+        pRes[2] += ((uSum >> 24) & 0xff);
+    }
+
+    // count all other variables
+    for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
+        for ( i = 0; i < nBytes; i += Step + Step )
+        {
+            pRes[iVar] += pBytes[i];
+            pBytes[i] += pBytes[i+Step];
+        }
+    assert( pBytes[0] == nTotal );
+    assert( iVar == nVars );
+    return nTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast counting minterms for the functions.]
+
+  Description [Returns 0 if the function is a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCountMintermsPrecomp()
+{
+    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
+    };
+    unsigned i, uWord;
+    for ( i = 0; i < 256; i++ )
+    {
+        if ( i % 8 == 0 )
+            printf( "\n" );
+        uWord  =  bit_count[i];
+        uWord |= (bit_count[i & 0x55] <<  8);
+        uWord |= (bit_count[i & 0x33] << 16);
+        uWord |= (bit_count[i & 0x0f] << 24);
+        printf( "0x" );
+        Extra_PrintHexadecimal( stdout, &uWord, 5 );
+        printf( ", " );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////