Improvements to the truth table computation in 'if' package.

4 files changed, 454 insertions, 12 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index ea5c589a..5c877c9d 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -353,8 +353,9 @@ static inline void       If_CutSetDataInt( If_Cut_t * pCut, int Data )       { *
 static inline int        If_CutLeaveNum( If_Cut_t * pCut )                   { return pCut->nLeaves;                             }
 static inline int *      If_CutLeaves( If_Cut_t * pCut )                     { return pCut->pLeaves;                             }
 static inline unsigned * If_CutTruth( If_Cut_t * pCut )                      { return pCut->pTruth;                              }
+static inline word *     If_CutTruthW( If_Cut_t * pCut )                     { return (word *)pCut->pTruth;                      }
 static inline unsigned   If_CutSuppMask( If_Cut_t * pCut )                   { return (~(unsigned)0) >> (32-pCut->nLeaves);      }
-static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
+static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 2 : (1 << (nVarsMax - 5)); }
 static inline int        If_CutPermWords( int nVarsMax )                     { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
 
 static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return pCut->fUser? (float)pCut->Cost : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves] : (float)1.0); }
@@ -505,8 +506,9 @@ extern void            If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, I
 extern void            If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
 /*=== ifTruth.c ===========================================================*/
 extern int             If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut );
-extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 extern void            If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars );
+extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern int             If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 /*=== ifUtil.c ============================================================*/
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
 extern void            If_ManCleanCutData( If_Man_t * p );
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 6946afa1..0ebdec1b 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -411,8 +411,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
     // set up elementary truth table of the unit cut
     if ( p->pPars->fTruth )
     {
-        int i, nTruthWords;
-        nTruthWords = pCut->nLimit <= 5 ? 1 : (1 << (pCut->nLimit - 5));
+        int i, nTruthWords = If_CutTruthWords(pCut->nLimit);
         for ( i = 0; i < nTruthWords; i++ )
             If_CutTruth(pCut)[i] = 0xAAAAAAAA;
     }
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index afc229e5..2d08aeac 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -212,8 +212,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         if ( p->pPars->fTruth )
         {
 //            clock_t clk = clock();
-            int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+//            int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+            int RetValue = If_CutComputeTruth2( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
 //            p->timeTruth += clock() - clk;
+
             pCut->fUseless = 0;
             if ( p->pPars->pFuncCell && RetValue < 2 )
             {
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index f0289695..87473767 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -43,29 +43,28 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-static inline int  If_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
 static inline void If_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
-    for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
         pOut[w] = ~pIn[w];
 }
 static inline void If_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
-    for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
         pOut[w] = pIn[w];
 }
 static inline void If_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
 {
     int w;
-    for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
         pOut[w] = ~(pIn0[w] & pIn1[w]);
 }
 static inline void If_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
 {
     int w;
-    for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
         pOut[w] = pIn0[w] & pIn1[w];
 }
 
@@ -89,7 +88,7 @@ void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int i
         { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
         { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
     };
-    int nWords = If_TruthWordNum( nVars );
+    int nWords = If_CutTruthWords( nVars );
     int i, k, Step, Shift;
 
     assert( iVar < nVars - 1 );
@@ -245,7 +244,7 @@ void If_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, u
 ***********************************************************************/
 int If_CutTruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
 {
-    int nWords = If_TruthWordNum( nVars );
+    int nWords = If_CutTruthWords( nVars );
     int i, k, Step;
 
     assert( iVar < nVars );
@@ -449,6 +448,446 @@ int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut )
 }
 
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int  Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
+{
+    int w;
+    if ( fCompl )
+        for ( w = 0; w < nWords; w++ )
+            pOut[w] = ~pIn[w];
+    else
+        for ( w = 0; w < nWords; w++ )
+            pOut[w] = pIn[w];
+}
+static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
+{
+    int w;
+    if ( fCompl )
+        for ( w = 0; w < nWords; w++ )
+            pOut[w] = ~(pIn1[w] & pIn2[w]);
+    else
+        for ( w = 0; w < nWords; w++ )
+            pOut[w] = pIn1[w] & pIn2[w];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtSuppIsMinBase( int Supp )
+{
+    return (Supp & (Supp+1)) == 0;
+}
+static inline int Abc_Tt6HasVar( word t, int iVar )
+{
+    static word Truth6[6] = {
+        0xAAAAAAAAAAAAAAAA,
+        0xCCCCCCCCCCCCCCCC,
+        0xF0F0F0F0F0F0F0F0,
+        0xFF00FF00FF00FF00,
+        0xFFFF0000FFFF0000,
+        0xFFFFFFFF00000000
+    };
+    return (t & ~Truth6[iVar]) != ((t & Truth6[iVar]) >> (1<<iVar));
+}
+static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
+{
+    static word Truth6[6] = {
+        0xAAAAAAAAAAAAAAAA,
+        0xCCCCCCCCCCCCCCCC,
+        0xF0F0F0F0F0F0F0F0,
+        0xFF00FF00FF00FF00,
+        0xFFFF0000FFFF0000,
+        0xFFFFFFFF00000000
+    };
+    int nWords = Abc_TtWordNum( nVars );
+    assert( iVar < nVars );
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
+                return 1;
+        return 0;
+    }
+    else
+    {
+        int i, k, Step = (1 << (iVar - 6));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != t[Step+i] )
+                    return 1;
+            t += 2*Step;
+        }
+        return 0;
+    }
+}
+static inline int Abc_TtSupport( word * t, int nVars )
+{
+    int v, Supp = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtHasVar( t, nVars, v ) )
+            Supp |= (1 << v);
+    return Supp;
+}
+static inline int Abc_TtSupportSize( word * t, int nVars )
+{
+    int v, SuppSize = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtHasVar( t, nVars, v ) )
+            SuppSize++;
+    return SuppSize;
+}
+static inline int Abc_TtSupportAndSize( word * t, int nVars, int * pSuppSize )
+{
+    int v, Supp = 0;
+    *pSuppSize = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtHasVar( t, nVars, v ) )
+            Supp |= (1 << v), (*pSuppSize)++;
+    return Supp;
+}
+static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
+{
+    int v, Supp = 0;
+    *pSuppSize = 0;
+    assert( nVars <= 6 );
+    for ( v = 0; v < nVars; v++ )
+        if ( Abc_Tt6HasVar( t, v ) )
+            Supp |= (1 << v), (*pSuppSize)++;
+    return Supp;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word Abc_Tt6SwapVars( word Truth, int iVar, int jVar )
+{
+    static word PPMasks[6][6] = {
+        { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
+        { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
+        { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 },
+        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 },
+        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 },
+        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 }
+    };
+    int shift;
+    word low2High, high2Low; 
+    assert( iVar <= 5 && jVar <= 5 && iVar < jVar );
+    shift = (1 << jVar) - (1 << iVar);
+    low2High = (Truth & PPMasks[iVar][jVar - 1] ) << shift;
+    Truth &= ~PPMasks[iVar][jVar - 1];
+    high2Low = (Truth & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
+    Truth &= ~(PPMasks[iVar][jVar - 1] << shift);
+    return Truth | low2High | high2Low;
+}
+
+static inline void Abc_TtSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar )
+{
+    word low2High, high2Low, temp;
+    int nWords = Abc_TtWordNum(nVars);
+    int shift, step, iStep, jStep;
+    int w = 0, i = 0, j = 0;
+    static word PPMasks[6][6] = {
+        { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
+        { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
+        { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 },
+        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 },
+        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 },
+        { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 }
+    };
+    if ( iVar == jVar )
+        return;
+    if ( jVar < iVar )
+    {
+        int varTemp = jVar;
+        jVar = iVar;
+        iVar = varTemp;
+    }
+    if ( iVar <= 5 && jVar <= 5 )
+    {
+        shift = (1 << jVar) - (1 << iVar);
+        for ( w = 0; w < nWords; w++ )
+        {
+            low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift;
+            pTruth[w] &= ~PPMasks[iVar][jVar - 1];
+            high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
+            pTruth[w] &= ~(PPMasks[iVar][jVar - 1] << shift);
+            pTruth[w] = pTruth[w] | low2High | high2Low;
+        }
+    }
+    else if ( iVar <= 5 && jVar > 5 )
+    {
+        step = Abc_TtWordNum(jVar + 1)/2;
+        shift = 1 << iVar;
+        for ( w = 0; w < nWords; w += 2*step )
+        {
+            for (j = 0; j < step; j++)
+            {
+                low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift;
+                pTruth[w + j] &= ~PPMasks[iVar][5];
+                high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift;
+                pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift);
+                pTruth[w + j] |= high2Low;
+                pTruth[w + step + j] |= low2High;            
+            }
+        }
+    }
+    else
+    {
+        iStep = Abc_TtWordNum(iVar + 1)/2;
+        jStep = Abc_TtWordNum(jVar + 1)/2;
+        for (w = 0; w < nWords; w += 2*jStep)
+        {
+            for (i = 0; i < jStep; i += 2*iStep)
+            {
+                for (j = 0; j < iStep; j++)
+                {
+                    temp = pTruth[w + iStep + i + j];
+                    pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j];
+                    pTruth[w + jStep + i + j] = temp;
+                }
+            }
+        }
+    }    
+    if ( V2P && P2V )
+    {
+        V2P[P2V[iVar]] = jVar;
+        V2P[P2V[jVar]] = iVar;
+        P2V[iVar] ^= P2V[jVar];
+        P2V[jVar] ^= P2V[iVar];
+        P2V[iVar] ^= P2V[jVar];
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutTruthMinimize6( If_Man_t * p, If_Cut_t * pCut )
+{
+    unsigned uSupport;
+    int i, k, nSuppSize;
+    int nVars = If_CutLeaveNum(pCut);
+    // compute the support of the cut's function
+    uSupport = Abc_Tt6SupportAndSize( *If_CutTruthW(pCut), nVars, &nSuppSize );
+    if ( nSuppSize == If_CutLeaveNum(pCut) )
+        return 0;
+// TEMPORARY
+    if ( nSuppSize < 2 )
+    {
+        p->nSmallSupp++;
+        return 2;
+    }
+    // update leaves and signature
+    pCut->uSign = 0;
+    for ( i = k = 0; i < nVars; i++ )
+    {
+        if ( !(uSupport & (1 << i)) )
+            continue;    
+        pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
+        if ( k < i )
+        {
+            pCut->pLeaves[k] = pCut->pLeaves[i];
+            *If_CutTruthW(pCut) = Abc_Tt6SwapVars( *If_CutTruthW(pCut), k, i );
+        }
+        k++;
+    }
+    assert( k == nSuppSize );
+    pCut->nLeaves = nSuppSize;
+    // verify the result
+//    assert( nSuppSize == Abc_TtSupportSize(If_CutTruthW(pCut), nVars) );
+    return 1;
+}
+static inline word If_TruthStretch6( word Truth, If_Cut_t * pCut, If_Cut_t * pCut0 )
+{
+    int i, k;
+    for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
+    {
+        if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
+            continue;
+        assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
+        if ( k < i )
+            Truth = Abc_Tt6SwapVars( Truth, k, i );
+        k--;
+    }
+    return Truth;
+}
+static inline int If_CutComputeTruth6( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    word t0 = (fCompl0 ^ pCut0->fCompl) ? ~*If_CutTruthW(pCut0) : *If_CutTruthW(pCut0);
+    word t1 = (fCompl1 ^ pCut1->fCompl) ? ~*If_CutTruthW(pCut1) : *If_CutTruthW(pCut1);
+    assert( pCut->nLimit <= 6 );
+    t0 = If_TruthStretch6( t0, pCut, pCut0 );
+    t1 = If_TruthStretch6( t1, pCut, pCut1 );
+    *If_CutTruthW(pCut) = t0 & t1;
+    if ( p->pPars->fCutMin )
+        return If_CutTruthMinimize6( p, pCut );
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// this procedure handles special case reductions
+static inline int If_CutTruthMinimize21( If_Man_t * p, If_Cut_t * pCut ) 
+{
+    word * pTruth = If_CutTruthW(pCut);
+    int i, k, nVars = If_CutLeaveNum(pCut);
+    unsigned uSign = 0;
+    for ( i = k = 0; i < nVars; i++ )
+    {
+        if ( !Abc_TtHasVar( pTruth, nVars, i ) )
+            continue;
+        uSign |= If_ObjCutSign( pCut->pLeaves[i] );
+        if ( k < i )
+        {
+            pCut->pLeaves[k] = pCut->pLeaves[i];
+            Abc_TtSwapVars( pTruth, nVars, NULL, NULL, k, i );
+        }
+        k++;
+    }
+    if ( k == nVars )
+        return 0;
+    assert( k < nVars );
+    pCut->nLeaves = k;
+    pCut->uSign = uSign;
+// TEMPORARY
+    if ( pCut->nLeaves < 2 )
+    {
+        p->nSmallSupp++;
+        return 2;
+    }
+    // verify the result
+    assert( If_CutLeaveNum(pCut) == Abc_TtSupportSize(pTruth, nVars) );
+    return 1;
+}
+static inline int If_CutTruthMinimize2( If_Man_t * p, If_Cut_t * pCut )
+{
+    unsigned uSupport;
+    int i, k, nSuppSize;
+    int nVars = If_CutLeaveNum(pCut);
+    // compute the support of the cut's function
+    uSupport = Abc_TtSupportAndSize( If_CutTruthW(pCut), nVars, &nSuppSize );
+    if ( nSuppSize == If_CutLeaveNum(pCut) )
+        return 0;
+// TEMPORARY
+    if ( nSuppSize < 2 )
+    {
+        p->nSmallSupp++;
+        return 2;
+    }
+    // update leaves and signature
+    pCut->uSign = 0;
+    for ( i = k = 0; i < nVars; i++ )
+    {
+        if ( !(uSupport & (1 << i)) )
+            continue;    
+        pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
+        if ( k < i )
+        {
+            pCut->pLeaves[k] = pCut->pLeaves[i];
+            Abc_TtSwapVars( If_CutTruthW(pCut), pCut->nLimit, NULL, NULL, k, i );
+        }
+        k++;
+    }
+    assert( k == nSuppSize );
+    pCut->nLeaves = nSuppSize;
+    // verify the result
+//    assert( nSuppSize == Abc_TtSupportSize(If_CutTruthW(pCut), nVars) );
+    return 1;
+}
+static inline void If_TruthStretch2( word * pTruth, If_Cut_t * pCut, If_Cut_t * pCut0 )
+{
+    int i, k;
+    for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
+    {
+        if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
+            continue;
+        assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
+        if ( k < i )
+            Abc_TtSwapVars( pTruth, pCut->nLimit, NULL, NULL, k, i );
+        k--;
+    }
+}
+inline int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    int nWords;
+    if ( pCut->nLimit < 7 )
+        return If_CutComputeTruth6( p, pCut, pCut0, pCut1, fCompl0, fCompl1 );
+    nWords = Abc_TtWordNum( pCut->nLimit );
+    Abc_TtCopy( (word *)p->puTemp[0], If_CutTruthW(pCut0), nWords, fCompl0 ^ pCut0->fCompl );
+    Abc_TtCopy( (word *)p->puTemp[1], If_CutTruthW(pCut1), nWords, fCompl1 ^ pCut1->fCompl );
+    If_TruthStretch2( (word *)p->puTemp[0], pCut, pCut0 );
+    If_TruthStretch2( (word *)p->puTemp[1], pCut, pCut1 );
+    Abc_TtAnd( If_CutTruthW(pCut), (word *)p->puTemp[0], (word *)p->puTemp[1], nWords, 0 );
+    if ( p->pPars->fCutMin )
+        return If_CutTruthMinimize2( p, pCut );
+    return 0;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////