diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-03-25 12:17:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-03-25 12:17:12 -0700 |
| commit | a277d450bf7c624392d41739788f115f1d655556 (patch) | |
| tree | d24c5a50f62bbc12e0d93b1e78d5be9dfe65c80e | |
| parent | c7bc6b63298f532270b6c696a6f36545429dfb52 (diff) | |
| download | abc-a277d450bf7c624392d41739788f115f1d655556.tar.gz abc-a277d450bf7c624392d41739788f115f1d655556.tar.bz2 abc-a277d450bf7c624392d41739788f115f1d655556.zip | |
Experiments with simulation-based engines.
| -rw-r--r-- | src/aig/gia/giaSimBase.c | 9 | ||||
| -rw-r--r-- | src/misc/util/utilTruth.h | 17 | ||||
| -rw-r--r-- | src/sat/bsat/satClause.h | 3 |
3 files changed, 25 insertions, 4 deletions
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index afa13691..9f07da15 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -936,9 +936,12 @@ Vec_Wrd_t * Gia_ManSimRelDeriveFuncs2( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOut else { printf( "The relation was successfully determized with don't-cares for %d patterns.\n", 64 * nWords ); - printf( "Don't-cares in each output:" ); for ( k = 0; k < nOuts; k++ ) - printf( " %d = %d", k, nDCs[k] ); + { + int nOffs = Abc_TtCountOnesVec( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), nWords ); + int nOns = Abc_TtCountOnesVec( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), nWords ); + printf( "%4d : Off = %6d On = %6d Dc = %6d (%6.2f %%)", k, nOffs, nOns, nDCs[k], 100.0*nDCs[k]/(64*nWords) ); + } printf( "\n" ); } Gia_ManSimRelCheckFuncs( p, vRel, nOuts, vFuncs ); @@ -1512,7 +1515,7 @@ void Gia_RsbUpdateRemove( Gia_RsbMan_t * p, int Index ) int Gia_RsbRemovalCost( Gia_RsbMan_t * p, int Index ) { Vec_Int_t * vTemp[2][2]; - unsigned Mask = Abc_InfoMask( Index ); + //unsigned Mask = Abc_InfoMask( Index ); int m, m2, Cost = 0, nLeaves = 1 << Vec_IntSize(p->vObjs); assert( Vec_WecSize(p->vSets[0]) == (1 << Vec_IntSize(p->vObjs)) ); assert( Vec_WecSize(p->vSets[1]) == (1 << Vec_IntSize(p->vObjs)) ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 3716e9dd..18bae556 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1835,6 +1835,23 @@ static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, in Count += Abc_TtCountOnes( pMask[w] & x[w] ); return Count; } +static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords ) +{ + int w, Count = 0; + if ( !fComp0 && !fComp1 ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & x0[w] & x1[w] ); + else if ( fComp0 && !fComp1 ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & x1[w] ); + else if ( !fComp0 && fComp1 ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & x0[w] & ~x1[w] ); + else + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & ~x1[w] ); + return Count; +} static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords ) { int w, Count = 0; diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index d2ed3b75..74e685c3 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -88,7 +88,8 @@ static inline void Sat_MemWriteLimit( int * p, int nInts ) { p[0] = nI static inline int Sat_MemHandPage( Sat_Mem_t * p, cla h ) { return h >> p->nPageSize; } static inline int Sat_MemHandShift( Sat_Mem_t * p, cla h ) { return h & p->uPageMask; } -static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; } +//static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; } +static inline int Sat_MemIntSize( int size, int lrn ) { return 2*((size + 2 + lrn)/2); } static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); } static inline int Sat_MemClauseSize2( clause * p ) { return Sat_MemIntSize(p->size, 1); } |