Adding new mapping feature.

src/aig/gia/giaIf.c

@@ -1572,7 +1572,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
             // perform sorting of cut leaves by delay, so that the slowest pin drives the fastest input of the LUT
             if ( !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && 
                  !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->nGateSize && !pIfMan->pPars->fEnableCheck75 && 
-                 !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune && !pIfMan->pPars->fUseCofVars )
+                 !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune && 
+                 !pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars )
                 If_CutRotatePins( pIfMan, pCutBest );
             // collect leaves of the best cut
             Vec_IntClear( vLeaves );
@@ -1678,6 +1679,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
                 Vec_IntPush( vMapping2, -Abc_Lit2Var(iTopLit) );
                 pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
             }
+            else if ( pIfMan->pPars->fUseAndVars && pIfMan->pPars->fDeriveLuts && (int)pCutBest->nLeaves > pIfMan->pPars->nLutSize/2 )
+            {
+                assert( 0 );
+            }
             else if ( (pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth) || pIfMan->pPars->fUseDsd || pIfMan->pPars->fUseTtPerm )
             {
                 word * pTruth = If_CutTruthW(pIfMan, pCutBest);
@@ -2133,6 +2138,7 @@ void Gia_ManTestStruct( Gia_Man_t * p )
     printf( "\n" );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaScript.c

@@ -324,8 +324,10 @@ Gia_Man_t * Gia_ManDupToBarBufs( Gia_Man_t * p, int nBarBufs )
     Gia_ManForEachAnd( p, pObj, i )
     {
         for ( ; k < nBarBufs; k++ )
-            if ( ~Gia_ObjFanin0Copy(Gia_ManCo(p, k)) )
+            if ( ~Gia_ObjFanin0(Gia_ManCo(p, k))->Value )
                 Gia_ManCi(p, nPiReal + k)->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, k)) );
+            else
+                break;
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
             pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);  

src/map/if/if.h

@@ -133,6 +133,7 @@ struct If_Par_t_
     int                fUseDsd;       // compute DSD of the cut functions
     int                fUseDsdTune;   // use matching based on precomputed manager
     int                fUseCofVars;   // use cofactoring variables
+    int                fUseAndVars;   // use bi-decomposition
     int                fUseTtPerm;    // compute truth tables of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
     int                fDoAverage;    // optimize average rather than maximum level
@@ -245,6 +246,7 @@ struct If_Man_t_
     Vec_Int_t *        vTtDsds[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into DSD
     Vec_Str_t *        vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations
     Vec_Str_t *        vTtVars[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into selected vars
+    Vec_Int_t *        vTtDecs[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into decomposition pattern
     Hash_IntMan_t *    vPairHash;     // hashing pairs of truth tables
     Vec_Int_t *        vPairRes;      // resulting truth table
     Vec_Str_t *        vPairPerms;    // resulting permutation

src/map/if/ifCut.c

@@ -754,9 +754,8 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
     if ( !pCut->fUseless && 
          (p->pPars->fUseDsd || p->pPars->fUseBat || 
           p->pPars->pLutStruct || p->pPars->fUserRecLib || 
-          p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || 
-          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || 
-          p->pPars->fEnableCheck75u) )
+          p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || 
+          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) )
     {
         If_Cut_t * pFirst = pCutSet->ppCuts[0];
         if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 )

src/map/if/ifMan.c

@@ -136,6 +136,17 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
         for ( v = 0; v < 6; v++ )
             p->vTtVars[v]  = p->vTtVars[6];
     }
+    if ( pPars->fUseAndVars )
+    {
+        for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ )
+        {
+            p->vTtDecs[v] = Vec_IntAlloc( 1000 );
+            Vec_IntPush( p->vTtDecs[v], 0 );
+            Vec_IntPush( p->vTtDecs[v], 0 );
+        }
+        for ( v = 0; v < 6; v++ )
+            p->vTtDecs[v]  = p->vTtDecs[6];
+    }
     if ( pPars->fUseBat )
     {
 //        abctime clk = Abc_Clock();
@@ -248,6 +259,8 @@ void If_ManStop( If_Man_t * p )
         Vec_StrFreeP( &p->vTtPerms[i] );
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_StrFreeP( &p->vTtVars[i] );
+    for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
+        Vec_IntFreeP( &p->vTtDecs[i] );
     Vec_IntFreeP( &p->vCutData );
     Vec_IntFreeP( &p->vPairRes );
     Vec_StrFreeP( &p->vPairPerms );

src/map/if/ifMap.c

@@ -99,7 +99,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     If_Cut_t * pCut0R, * pCut1R;
     int fFunc0R, fFunc1R;
     int i, k, v, iCutDsd, fChange;
-    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->pLutStruct != NULL;
+    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->pLutStruct != NULL;
     assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
     assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
 
@@ -270,23 +270,47 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 p->nCutsCountAll++;
                 p->nCutsCount[pCut->nLeaves]++;
             }
-            else if ( p->pPars->fUseCofVars )
+            else 
             {
-                int iCofVar = -1, truthId = Abc_Lit2Var(pCut->iCutFunc);
-                if ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) || Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId) == (char)-1 )
+                if ( p->pPars->fUseAndVars )
                 {
-                    while ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) )
-                        Vec_StrPush( p->vTtVars[pCut->nLeaves], (char)-1 );
-                    iCofVar = Abc_TtCheckCondDep( If_CutTruthWR(p, pCut), pCut->nLeaves, p->pPars->nLutSize / 2 );
-                    Vec_StrWriteEntry( p->vTtVars[pCut->nLeaves], truthId, (char)iCofVar );
+                    int iDecMask = -1, truthId = Abc_Lit2Var(pCut->iCutFunc);
+                    if ( truthId >= Vec_IntSize(p->vTtDecs[pCut->nLeaves]) || Vec_IntEntry(p->vTtDecs[pCut->nLeaves], truthId) == -1 )
+                    {
+                        while ( truthId >= Vec_IntSize(p->vTtDecs[pCut->nLeaves]) )
+                            Vec_IntPush( p->vTtDecs[pCut->nLeaves], -1 );
+                        if ( (int)pCut->nLeaves > p->pPars->nLutSize / 2 )
+                            iDecMask = Abc_TtProcessBiDec( If_CutTruthW(p, pCut), (int)pCut->nLeaves, p->pPars->nLutSize / 2 );
+                        else
+                            iDecMask = 0;
+                        Vec_IntWriteEntry( p->vTtDecs[pCut->nLeaves], truthId, iDecMask );
+                    }
+                    iDecMask = Vec_IntEntry(p->vTtDecs[pCut->nLeaves], truthId);
+                    assert( iDecMask >= 0 );
+                    pCut->fUseless = (int)(iDecMask == 0 && (int)pCut->nLeaves > p->pPars->nLutSize / 2);
+                    p->nCutsUselessAll += pCut->fUseless;
+                    p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
+                    p->nCutsCountAll++;
+                    p->nCutsCount[pCut->nLeaves]++;
+                }
+                if ( p->pPars->fUseCofVars && (!p->pPars->fUseAndVars || pCut->fUseless) )
+                {
+                    int iCofVar = -1, truthId = Abc_Lit2Var(pCut->iCutFunc);
+                    if ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) || Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId) == (char)-1 )
+                    {
+                        while ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) )
+                            Vec_StrPush( p->vTtVars[pCut->nLeaves], (char)-1 );
+                        iCofVar = Abc_TtCheckCondDep( If_CutTruthWR(p, pCut), pCut->nLeaves, p->pPars->nLutSize / 2 );
+                        Vec_StrWriteEntry( p->vTtVars[pCut->nLeaves], truthId, (char)iCofVar );
+                    }
+                    iCofVar = Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId);
+                    assert( iCofVar >= 0 && iCofVar <= (int)pCut->nLeaves );
+                    pCut->fUseless = (int)(iCofVar == (int)pCut->nLeaves && pCut->nLeaves > 0);
+                    p->nCutsUselessAll += pCut->fUseless;
+                    p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
+                    p->nCutsCountAll++;
+                    p->nCutsCount[pCut->nLeaves]++;
                 }
-                iCofVar = Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId);
-                assert( iCofVar >= 0 && iCofVar <= (int)pCut->nLeaves );
-                pCut->fUseless = (int)(iCofVar == (int)pCut->nLeaves && pCut->nLeaves > 0);
-                p->nCutsUselessAll += pCut->fUseless;
-                p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
-                p->nCutsCountAll++;
-                p->nCutsCount[pCut->nLeaves]++;
             }
         }
         

src/misc/util/utilTruth.h

@@ -2269,6 +2269,272 @@ static inline void Unm_ManCheckTest()
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Checks existence of bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtComputeGraph( word * pTruth, int v, int nVars, int * pGraph )
+{
+    word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 )
+    word Cof00[64], Cof01[64], Cof10[64], Cof11[64];
+    word CofXor, CofAndTest; 
+    int i, w, nWords = Abc_TtWordNum(nVars);
+    pGraph[v] |= (1 << v);
+    if ( v == nVars - 1 )
+        return;
+    assert( v < nVars - 1 );
+    Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
+    Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
+    for ( i = v + 1; i < nVars; i++ )
+    {
+        Abc_TtCofactor0p( Cof00, Cof0, nWords, i );
+        Abc_TtCofactor1p( Cof01, Cof0, nWords, i );
+        Abc_TtCofactor0p( Cof10, Cof1, nWords, i );
+        Abc_TtCofactor1p( Cof11, Cof1, nWords, i );
+        for ( w = 0; w < nWords; w++ )
+        {
+            CofXor     =  Cof00[w] ^ Cof01[w]  ^  Cof10[w] ^ Cof11[w];
+            CofAndTest = (Cof00[w] & Cof01[w]) | (Cof10[w] & Cof11[w]);
+            if ( CofXor & CofAndTest )
+            {
+                pGraph[v] |= (1 << i);
+                pGraph[i] |= (1 << v);
+            }
+            else if ( CofXor & ~CofAndTest )
+            {
+                pGraph[v] |= (1 << (16+i));
+                pGraph[i] |= (1 << (16+v));
+            }
+        }
+    }
+}
+static inline void Abc_TtPrintVarSet( int Mask, int nVars )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+        if ( (Mask >> i) & 1 )
+            printf( "1" );
+        else
+            printf( "." );
+}
+static inline void Abc_TtPrintBiDec( word * pTruth, int nVars )
+{
+    int v, pGraph[12] = {0};
+    assert( nVars <= 12 );
+    for ( v = 0; v < nVars; v++ )
+    {
+        Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
+        Abc_TtPrintVarSet( pGraph[v], nVars );
+        printf( "    " );
+        Abc_TtPrintVarSet( pGraph[v] >> 16, nVars );
+        printf( "\n" );
+    }
+}
+static inline int Abc_TtVerifyBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word wThis, word wThat )
+{
+    int pVarsThis[12], pVarsThat[12], pVarsAll[12];
+    int nThis = Abc_TtBitCount16(This);
+    int nThat = Abc_TtBitCount16(That);
+    int i, k, nWords = Abc_TtWordNum(nVars);
+    word pThis[64] = {wThis}, pThat[64] = {wThat};
+    assert( nVars <= 12 );
+    for ( i = 0; i < nVars; i++ )
+        pVarsAll[i] = i;
+    for ( i = k = 0; i < nVars; i++ )
+        if ( (This >> i) & 1 )
+            pVarsThis[k++] = i;
+    assert( k == nThis );
+    for ( i = k = 0; i < nVars; i++ )
+        if ( (That >> i) & 1 )
+            pVarsThat[k++] = i;
+    assert( k == nThat );
+    Abc_TtStretch6( pThis, nThis, nVars );
+    Abc_TtStretch6( pThat, nThat, nVars );
+    Abc_TtExpand( pThis, nVars, pVarsThis, nThis, pVarsAll, nVars );
+    Abc_TtExpand( pThat, nVars, pVarsThat, nThat, pVarsAll, nVars );
+    for ( k = 0; k < nWords; k++ )
+        if ( pTruth[k] != (pThis[k] & pThat[k]) )
+            return 0;
+    return 1;
+}
+static inline void Abc_TtExist( word * pTruth, int iVar, int nWords )
+{
+    word Cof0[64], Cof1[64]; 
+    Abc_TtCofactor0p( Cof0, pTruth, nWords, iVar );
+    Abc_TtCofactor1p( Cof1, pTruth, nWords, iVar );
+    Abc_TtOr( pTruth, Cof0, Cof1, nWords );
+}
+static inline int Abc_TtCheckBiDec( word * pTruth, int nVars, int This, int That )
+{
+    int VarMask[2] = {This & ~That, That & ~This};
+    int v, c, nWords = Abc_TtWordNum(nVars);
+    word pTempR[2][64]; 
+    for ( c = 0; c < 2; c++ )
+    {
+        Abc_TtCopy( pTempR[c], pTruth, nWords, 0 );
+        for ( v = 0; v < nVars; v++ )
+            if ( ((VarMask[c] >> v) & 1) )
+                Abc_TtExist( pTempR[c], v, nWords );
+    }
+    for ( v = 0; v < nWords; v++ )
+        if ( ~pTruth[v] & pTempR[0][v] & pTempR[1][v] )
+            return 0;
+    return 1;
+}
+static inline word Abc_TtDeriveBiDecOne( word * pTruth, int nVars, int This )
+{
+    word pTemp[64]; 
+    int nThis = Abc_TtBitCount16(This);
+    int v, nWords = Abc_TtWordNum(nVars);
+    Abc_TtCopy( pTemp, pTruth, nWords, 0 );
+    for ( v = 0; v < nVars; v++ )
+        if ( !((This >> v) & 1) )
+            Abc_TtExist( pTemp, v, nWords );
+    Abc_TtShrink( pTemp, nThis, nVars, This );
+    return Abc_Tt6Stretch( pTemp[0], nThis );
+}
+static inline void Abc_TtDeriveBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word * pThis, word * pThat )
+{
+    assert( Abc_TtBitCount16(This) <= nSuppLim );
+    assert( Abc_TtBitCount16(That) <= nSuppLim );
+    pThis[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, This );
+    pThat[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, That );
+    if ( !Abc_TtVerifyBiDec(pTruth, nVars, This, That, nSuppLim, pThis[0], pThat[0] ) )
+        printf( "Bi-decomposition verification failed.\n" );
+}
+// detect simple case of decomposition with topmost AND gate
+static inline int Abc_TtCheckBiDecSimple( word * pTruth, int nVars, int nSuppLim )
+{
+    word Cof0[64], Cof1[64]; 
+    int v, Res = 0, nDecVars = 0, nWords = Abc_TtWordNum(nVars);
+    for ( v = 0; v < nVars; v++ )
+    {
+        Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
+        Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
+        if ( !Abc_TtIsConst0(Cof0, nWords) && !Abc_TtIsConst0(Cof1, nWords) )
+            continue;
+        nDecVars++;
+        Res |= 1 << v;
+        if ( nDecVars >= nVars - nSuppLim )
+            return ((Res ^ (int)Abc_Tt6Mask(nVars)) << 16) | Res;
+    }
+    return 0;
+}
+static inline int Abc_TtProcessBiDec( word * pTruth, int nVars, int nSuppLim )
+{
+    int i, v, Res, nSupp, CountShared = 0, pGraph[12] = {0};
+    assert( nSuppLim < nVars && nVars <= 12 );
+    assert( 2 <= nSuppLim && nSuppLim <= 6 );
+    Res = Abc_TtCheckBiDecSimple( pTruth, nVars, nSuppLim );
+    if ( Res )
+        return Res;
+    for ( v = 0; v < nVars; v++ )
+    {
+        Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
+        nSupp = Abc_TtBitCount16(pGraph[v] & 0xFFFF);
+        if ( nSupp > nSuppLim ) 
+        {
+            // this variable is shared - check if the limit is exceeded
+            if ( ++CountShared > 2*nSuppLim - nVars )
+                return 0;
+        }
+        else if ( nVars - nSupp <= nSuppLim )
+        {
+            int This = pGraph[v] & 0xFFFF;
+            int That = This ^ (int)Abc_Tt6Mask(nVars);
+            // find the other component
+            int Graph = That;
+            for ( i = 0; i < nVars; i++ )
+                if ( (That >> i) & 1 )
+                    Graph |= pGraph[i] & 0xFFFF;
+            // check if this can be done
+            if ( Abc_TtBitCount16(Graph) > nSuppLim )
+                continue;
+            // try decomposition
+            if ( Abc_TtCheckBiDec(pTruth, nVars, This, Graph) )
+                return (Graph << 16) | This;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tests decomposition procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLim )
+{
+    word This, That, pTemp[64];
+    int Res, resThis, resThat, nThis, nThat;
+    int nWords = Abc_TtWordNum(nVars);
+    Abc_TtCopy( pTemp, pTruth, nWords, 0 );
+    Res = Abc_TtProcessBiDec( pTemp, nVars, nSuppLim );
+    if ( Res == 0 )
+    {
+        //Dau_DsdPrintFromTruth( pTemp, nVars );
+        //printf( "Non_dec\n\n" );
+        return;
+    }
+
+    resThis = Res & 0xFFFF;
+    resThat = Res >> 16;
+
+    Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
+    return;
+
+    //if ( !(resThis & resThat) )
+    //    return;
+
+//    Dau_DsdPrintFromTruth( pTemp, nVars );
+
+    nThis = Abc_TtBitCount16(resThis);
+    nThat = Abc_TtBitCount16(resThat);
+
+    printf( "Variable sets:    " );
+    Abc_TtPrintVarSet( resThis, nVars );
+    printf( "    " );
+    Abc_TtPrintVarSet( resThat, nVars );
+    printf( "\n" );
+    Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
+//    Dau_DsdPrintFromTruth( &This, nThis );
+//    Dau_DsdPrintFromTruth( &That, nThat );
+    printf( "\n" );
+}
+static inline void Abc_TtProcessBiDecExperiment()
+{
+    int nVars = 3;
+    int nSuppLim = 2;
+    int Res, resThis, resThat;
+    word This, That;
+//    word t = ABC_CONST(0x8000000000000000);
+//    word t = (s_Truths6[0] | s_Truths6[1]) & (s_Truths6[2] | s_Truths6[3] | s_Truths6[4] | s_Truths6[5]);
+//    word t = ((s_Truths6[0] & s_Truths6[1]) | (~s_Truths6[1] & s_Truths6[2]));
+    word t = ((s_Truths6[0] | s_Truths6[1]) & (s_Truths6[1] | s_Truths6[2]));
+    Abc_TtPrintBiDec( &t, nVars );
+    Res = Abc_TtProcessBiDec( &t, nVars, nSuppLim );
+    resThis = Res & 0xFFFF;
+    resThat = Res >> 16;
+    Abc_TtDeriveBiDec( &t, nVars, resThis, resThat, nSuppLim, &This, &That );
+//    Dau_DsdPrintFromTruth( &This, Abc_TtBitCount16(resThis) );
+//    Dau_DsdPrintFromTruth( &That, Abc_TtBitCount16(resThat) );
+    nVars = nSuppLim;
+}
+
 /*=== utilTruth.c ===========================================================*/