diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 23:04:24 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 23:04:24 -0800 |
| commit | 7d7ce3ecd03059602f70f26612aabd4a2ec49422 (patch) | |
| tree | b811916386ecfb045cc08f9be78a43a2f0307f30 /src/sat/bmc/bmcMaj.c | |
| parent | c3dccf3020e467da9fa62c9f609bce86b55ccd0a (diff) | |
| download | abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.tar.gz abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.tar.bz2 abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.zip | |
New exact synthesis command 'allexact'.
Diffstat (limited to 'src/sat/bmc/bmcMaj.c')
| -rw-r--r-- | src/sat/bmc/bmcMaj.c | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 67dcb26c..92ff06ee 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -184,6 +184,7 @@ static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k ) } static inline int Maj_ManEval( Maj_Man_t * p ) { + int fUseMiddle = 1; static int Flag = 0; int i, k, iMint; word * pFanins[3]; for ( i = p->nVars + 2; i < p->nObjs; i++ ) @@ -192,10 +193,27 @@ static inline int Maj_ManEval( Maj_Man_t * p ) pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) ); Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords ); } - if ( Flag && p->nVars >= 6 ) - iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars ); + if ( fUseMiddle ) + { + iMint = -1; + for ( i = 0; i < (1 << p->nVars); i++ ) + { + int nOnes = Abc_TtBitCount16(i); + if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 ) + continue; + if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) ) + continue; + iMint = i; + break; + } + } else - iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars ); + { + if ( Flag && p->nVars >= 6 ) + iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars ); + else + iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars ); + } //Flag ^= 1; assert( iMint < (1 << p->nVars) ); return iMint; |