diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-09 11:54:26 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-09 11:54:26 -0700 |
| commit | 069e9d4f2cc70aa859fe41a1ecbdec851f5f8501 (patch) | |
| tree | 9622f641bf2ada2f94960067b6ac1ee561ccb182 /src | |
| parent | f935dcd3693efa2d0938bcbfe8a7f90182826b82 (diff) | |
| download | abc-069e9d4f2cc70aa859fe41a1ecbdec851f5f8501.tar.gz abc-069e9d4f2cc70aa859fe41a1ecbdec851f5f8501.tar.bz2 abc-069e9d4f2cc70aa859fe41a1ecbdec851f5f8501.zip | |
Towards better Boolean matching.
Diffstat (limited to 'src')
| -rw-r--r-- | src/opt/dau/dauNonDsd.c | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c index e247b739..4e46f382 100644 --- a/src/opt/dau/dauNonDsd.c +++ b/src/opt/dau/dauNonDsd.c @@ -535,7 +535,7 @@ int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD ) int Dau_DecPerform( word * p, int nVars, unsigned uSet ) { Vec_Wrd_t * vUnique = Vec_WrdAlloc( 10 ); - word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, MintC, MintD; + word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD; char pDsdC[1000], pDsdD[1000]; int pPermC[16], pPermD[16], nVarsC, nVarsD, nVarsS, nVarsU, nVarsF, nPairs; int i, m, v, status, ResC, ResD; @@ -571,20 +571,24 @@ int Dau_DecPerform( word * p, int nVars, unsigned uSet ) if ( i & 1 ) continue; // create miterms with this polarity - MintC = MintD = ~(word)0; + FuncC = FuncD = 0; for ( m = 0; m < (1 << nVarsS); m++ ) { + word MintC, MintD; if ( !((i >> m) & 1) ) continue; + MintC = MintD = ~(word)0; for ( v = 0; v < nVarsS; v++ ) { MintC &= ((m >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v]; MintD &= ((m >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v]; } + FuncC |= MintC; + FuncD |= MintD; } // uncomplement given variables - tComp = (~s_Truths6[nVarsF + nVarsS] & ((tComp0 & ~MintC) | (tComp1 & MintC))) | (s_Truths6[nVarsF + nVarsS] & ((tComp1 & ~MintC) | (tComp0 & MintC))); - tDec = tDec0 ^ MintD; + tComp = (~s_Truths6[nVarsF + nVarsS] & ((tComp0 & ~FuncC) | (tComp1 & FuncC))) | (s_Truths6[nVarsF + nVarsS] & ((tComp1 & ~FuncC) | (tComp0 & FuncC))); + tDec = tDec0 ^ FuncD; // skip this variables if ( Vec_WrdFind( vUnique, tDec ) >= 0 ) continue; @@ -595,7 +599,9 @@ int Dau_DecPerform( word * p, int nVars, unsigned uSet ) // replace variables Dau_DecVarReplace( pDsdD, pPermD, nVarsD ); Dau_DecVarReplace( pDsdC, pPermC, nVarsC ); - printf( " " ); + // report + printf( " " ); + printf( "%3d : ", Vec_WrdSize(vUnique) ); printf( "%24s ", pDsdD ); printf( "%24s ", pDsdC ); Dau_DecVerify( p, nVars, pDsdC, pDsdD ); |