summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/aig/gia/giaIf.c8
-rw-r--r--src/aig/gia/giaScript.c4
-rw-r--r--src/map/if/if.h2
-rw-r--r--src/map/if/ifCut.c5
-rw-r--r--src/map/if/ifMan.c13
-rw-r--r--src/map/if/ifMap.c54
-rw-r--r--src/misc/util/utilTruth.h266
7 files changed, 332 insertions, 20 deletions
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 ===========================================================*/