From b379b3ee20266a4dcfc11f9113326f764846d79e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 11 Dec 2014 20:45:41 -0800 Subject: Adding new mapping feature. --- src/aig/gia/giaIf.c | 8 +- src/aig/gia/giaScript.c | 4 +- src/map/if/if.h | 2 + src/map/if/ifCut.c | 5 +- src/map/if/ifMan.c | 13 +++ src/map/if/ifMap.c | 54 +++++++--- src/misc/util/utilTruth.h | 266 ++++++++++++++++++++++++++++++++++++++++++++++ 7 files changed, 332 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 7d0047dc..46e08675 100644 --- a/src/aig/gia/giaIf.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaScript.c b/src/aig/gia/giaScript.c index b4408226..9ccb832b 100644 --- a/src/aig/gia/giaScript.c +++ b/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); diff --git a/src/map/if/if.h b/src/map/if/if.h index d77ac536..6a47a52b 100644 --- a/src/map/if/if.h +++ b/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 diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index 7b9ad3c1..adf00740 100644 --- a/src/map/if/ifCut.c +++ b/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 ) diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 472a1b1e..80d1f429 100644 --- a/src/map/if/ifMan.c +++ b/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 ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index e192c90e..32e3ce15 100644 --- a/src/map/if/ifMap.c +++ b/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]++; } } diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 0b52b3f4..645b639c 100644 --- a/src/misc/util/utilTruth.h +++ b/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 ===========================================================*/ -- cgit v1.2.3