Version abc90118

3 files changed, 230 insertions, 37 deletions

diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 101cf2eb..e8dea11a 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -141,14 +141,14 @@ struct Kit_DsdMan_t_
 };
 
 #ifdef WIN32
-#define DLLEXPORT __declspec(dllexport)
-#define DLLIMPORT __declspec(dllimport)
+#define ABC_DLLEXPORT __declspec(dllexport)
+#define ABC_DLLIMPORT __declspec(dllimport)
 #else  /* defined(WIN32) */
-#define DLLIMPORT
+#define ABC_DLLIMPORT
 #endif /* defined(WIN32) */
 
 #ifndef ABC_DLL
-#define ABC_DLL DLLIMPORT
+#define ABC_DLL ABC_DLLIMPORT
 #endif
 
 static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
@@ -169,7 +169,9 @@ static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
 #define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
     for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
 #define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
-    for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
+    for ( i = 0; (i < (int)(pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
+#define Kit_DsdObjForEachFaninReverse( pNtk, pObj, iLit, i )                       \
+    for ( i = (int)(pObj)->nFans - 1; (i >= 0) && ((iLit) = (pObj)->pFans[i], 1); i-- )
 
 #define Kit_PlaForEachCube( pSop, nFanins, pCube )                \
     for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
@@ -528,6 +530,7 @@ extern Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nD
 extern void            Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
 extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
+extern Kit_DsdObj_t *  Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdGetSupports( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
@@ -586,6 +589,7 @@ extern void            Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t *
 /*=== 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, int fReturnIn );
+extern void            Kit_TruthPermute( unsigned * pOut, unsigned * pIn, int nVars, char * pPerm, 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 );
@@ -608,6 +612,7 @@ extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int i
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern int             Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
 extern void            Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
+extern void            Kit_TruthCountOnesInCofs0( 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/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 8d670419..75358093 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -139,9 +139,9 @@ Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
     Kit_DsdNtk_t * pNtk;
     pNtk = ALLOC( Kit_DsdNtk_t, 1 );
     memset( pNtk, 0, sizeof(Kit_DsdNtk_t) );
-    pNtk->pNodes = ALLOC( Kit_DsdObj_t *, nVars );
+    pNtk->pNodes = ALLOC( Kit_DsdObj_t *, nVars+1 );
     pNtk->nVars = nVars;
-    pNtk->nNodesAlloc = nVars;
+    pNtk->nNodesAlloc = nVars+1;
     pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
     return pNtk;
 }
@@ -303,10 +303,13 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
 ***********************************************************************/
 void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
 {
-    Kit_DsdNtk_t * pTemp;
+    Kit_DsdNtk_t * pTemp, * pTemp2;
     pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
-    Kit_DsdVerify( pTemp, pTruth, nVars ); 
-    Kit_DsdPrintExpanded( pTemp );
+//    Kit_DsdPrintExpanded( pTemp );
+    pTemp2 = Kit_DsdExpand( pTemp );
+    Kit_DsdPrint( stdout, pTemp2 );
+    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
+    Kit_DsdNtkFree( pTemp2 );
     Kit_DsdNtkFree( pTemp );
 }
 
@@ -392,7 +395,6 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
     pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
-
     // go through the minterms
     nMints = (1 << pObj->nFans);
     Kit_TruthClear( pTruthRes, pNtk->nVars );
@@ -406,6 +408,9 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
 */
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        if ( Kit_DsdLitIsCompl(iLit) )
+            Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
     pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
     Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
@@ -550,7 +555,6 @@ unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
     pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
-
     // go through the minterms
     nMints = (1 << pObj->nFans);
     Kit_TruthClear( pTruthRes, pNtk->nVars );
@@ -564,6 +568,9 @@ unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
 */
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        if ( Kit_DsdLitIsCompl(iLit) )
+            Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
     pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
     Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
@@ -747,7 +754,6 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
     pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
-
     // go through the minterms
     nMints = (1 << pObj->nFans);
     Kit_TruthClear( pTruthRes, pNtk->nVars );
@@ -761,8 +767,11 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
 */
+//    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+//        assert( !Kit_DsdLitIsCompl(iLit) );
     Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
-        assert( !Kit_DsdLitIsCompl(iLit) );
+        if ( Kit_DsdLitIsCompl(iLit) )
+            Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
     pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
     Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
@@ -957,7 +966,7 @@ int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of blocks of the given number of inputs.]
+  Synopsis    [Returns the size of the largest non-DSD block.]
 
   Description []
                
@@ -982,6 +991,34 @@ int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the largest non-DSD block.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj, * pObjMax = NULL;
+    unsigned i, nSizeMax = 0;
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        if ( pObj->Type != KIT_DSD_PRIME )
+            continue;
+        if ( nSizeMax < pObj->nFans )
+        {
+            nSizeMax = pObj->nFans;
+            pObjMax = pObj;
+        }
+    }
+    return pObjMax;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finds the union of supports of the non-DSD blocks.]
 
   Description []
@@ -1125,10 +1162,46 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
             Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
         }
     }
-    // if the incoming phase is complemented, absorb it into the prime node
-    if ( Kit_DsdLitIsCompl(iLit) )
-        Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
-    return Kit_DsdVar2Lit( pObjNew->Id, 0 );
+
+    if ( pObj->nFans == 3 && 
+        (pTruthNew[0] == 0xCACACACA || pTruthNew[0] == 0xC5C5C5C5 || 
+         pTruthNew[0] == 0x3A3A3A3A || pTruthNew[0] == 0x35353535) )
+    {
+        // translate into regular MUXes
+        if ( pTruthNew[0] == 0xC5C5C5C5 )
+            pObjNew->pFans[0] = Kit_DsdLitNot(pObjNew->pFans[0]);
+        else if ( pTruthNew[0] == 0x3A3A3A3A )
+            pObjNew->pFans[1] = Kit_DsdLitNot(pObjNew->pFans[1]);
+        else if ( pTruthNew[0] == 0x35353535 )
+        {
+            pObjNew->pFans[0] = Kit_DsdLitNot(pObjNew->pFans[0]);
+            pObjNew->pFans[1] = Kit_DsdLitNot(pObjNew->pFans[1]);
+        }
+        pTruthNew[0] = 0xCACACACA;
+        // resolve the complemented control input
+        if ( Kit_DsdLitIsCompl(pObjNew->pFans[2]) )
+        {
+            unsigned char Temp = pObjNew->pFans[0];
+            pObjNew->pFans[0] = pObjNew->pFans[1];
+            pObjNew->pFans[1] = Temp;
+            pObjNew->pFans[2] = Kit_DsdLitNot(pObjNew->pFans[2]);
+        }
+        // resolve the complemented true input
+        if ( Kit_DsdLitIsCompl(pObjNew->pFans[1]) )
+        {
+            iLit = Kit_DsdLitNot(iLit);
+            pObjNew->pFans[0] = Kit_DsdLitNot(pObjNew->pFans[0]);
+            pObjNew->pFans[1] = Kit_DsdLitNot(pObjNew->pFans[1]);
+        }
+        return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
+    }
+    else
+    {
+        // if the incoming phase is complemented, absorb it into the prime node
+        if ( Kit_DsdLitIsCompl(iLit) )
+            Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
+        return Kit_DsdVar2Lit( pObjNew->Id, 0 );
+    }
 }
 
 /**Function*************************************************************
@@ -1834,7 +1907,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
             return;
         }
     }
-/*
+
     // if all decomposition methods failed and we are still above the limit, perform MUX-decomposition
     if ( nDecMux > 0 && (int)pObj->nFans > nDecMux )
     {
@@ -1852,14 +1925,14 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
         assert( pObj->Type == KIT_DSD_PRIME );
         pTruth[0] = 0xCACACACA;
         pObj->nFans = 3;
+        pObj->pFans[2] = pObj->pFans[iBestVar];
         pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
         pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
-        pObj->pFans[2] = pObj->pFans[iBestVar];
         // call recursively
         Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
         Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
     }
-*/
+
 }
 
 /**Function*************************************************************
@@ -1959,6 +2032,27 @@ Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars )
 ***********************************************************************/
 Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux )
 {
+/*
+    Kit_DsdNtk_t * pNew;
+    Kit_DsdObj_t * pObjNew;
+    assert( nVars <= 16 );
+    // create a new network
+    pNew = Kit_DsdNtkAlloc( nVars );
+    // consider simple special cases
+    if ( nVars == 0 )
+    {
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
+        pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, (int)(pTruth[0] == 0) );
+        return pNew;
+    }
+    if ( nVars == 1 )
+    {
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
+        pObjNew->pFans[0] = Kit_DsdVar2Lit( 0, 0 );
+        pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, (int)(pTruth[0] != 0xAAAAAAAA) );
+        return pNew;
+    }
+*/
     return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
 }
 
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index 9ddc7562..3f9188c7 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -155,7 +155,7 @@ void Kit_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int
   of variables is nVars. The total number of variables in nVarsAll. The last argument
   (Phase) contains shows where the variables should go.]
                
-  SideEffects []
+  SideEffects [The input truth table is modified.]
 
   SeeAlso     []
 
@@ -189,7 +189,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
   of variables is nVars. The total number of variables in nVarsAll. The last argument
   (Phase) contains shows what variables should remain.]
                
-  SideEffects []
+  SideEffects [The input truth table is modified.]
 
   SeeAlso     []
 
@@ -215,6 +215,43 @@ void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
         Kit_TruthCopy( pOut, pIn, nVarsAll );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Implement give permutation.]
+
+  Description [The input and output truth tables are in pIn/pOut. 
+  The number of variables is nVars. Permutation is in pPerm.]
+               
+  SideEffects [The input truth table is modified.]
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthPermute( unsigned * pOut, unsigned * pIn, int nVars, char * pPerm, int fReturnIn )
+{
+    int * pTemp;
+    int i, Temp, fChange, Counter = 0;
+    do {
+        fChange = 0;
+        for ( i = 0; i < nVars-1; i++ )
+        {
+            assert( pPerm[i] != pPerm[i+1] );
+            if ( pPerm[i] <= pPerm[i+1] )
+                continue;
+            Counter++;
+            fChange = 1;
+
+            Temp = pPerm[i];
+            pPerm[i] = pPerm[i+1];
+            pPerm[i+1] = Temp;
+
+            Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
+            pTemp = pIn; pIn = pOut; pOut = pTemp;
+        }
+    } while ( fChange );
+    if ( fReturnIn ^ !(Counter & 1) )
+        Kit_TruthCopy( pOut, pIn, nVars );
+}
 
 /**Function*************************************************************
 
@@ -1291,6 +1328,60 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of 1's in each negative cofactor.]
+
+  Description [The resulting numbers are stored in the array of shorts, 
+  whose length is nVars. The number of 1's is counted in a different
+  space than the original function. For example, if the function depends 
+  on k variables, the cofactors are assumed to depend on k-1 variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Counter;
+    memset( pStore, 0, sizeof(short) * nVars );
+    if ( nVars <= 5 )
+    {
+        if ( nVars > 0 )
+            pStore[0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
+        if ( nVars > 1 )
+            pStore[1] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
+        if ( nVars > 2 )
+            pStore[2] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
+        if ( nVars > 3 )
+            pStore[3] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
+        if ( nVars > 4 )
+            pStore[4] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
+        return;
+    }
+    // nVars >= 6
+    // count 1's for all other variables
+    for ( k = 0; k < nWords; k++ )
+    {
+        Counter = Kit_WordCountOnes( pTruth[k] );
+        for ( i = 5; i < nVars; i++ )
+            if ( (k & (1 << (i-5))) == 0 )
+                pStore[i] += Counter;
+    }
+    // count 1's for the first five variables
+    for ( k = 0; k < nWords/2; k++ )
+    {
+        pStore[0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
+        pStore[1] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
+        pStore[2] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
+        pStore[3] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
+        pStore[4] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
+        pTruth += 2;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of 1's in each cofactor.]
 
   Description [Verifies the above procedure.]
@@ -1440,16 +1531,17 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int 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] );
-//    }
-
+/*
+    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];
@@ -1463,11 +1555,12 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
 
     // permute
     Counter = 0;
+
     do {
         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;
@@ -1485,17 +1578,18 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
             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));
-            }
+//            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 );
 
+
 /*
     Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
     for ( i = 0; i < nVars; i++ )