diff options
Diffstat (limited to 'src/proof/ssc/sscSim.c')
-rw-r--r-- | src/proof/ssc/sscSim.c | 45 |
1 files changed, 40 insertions, 5 deletions
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c index 9a2c1033..d28db432 100644 --- a/src/proof/ssc/sscSim.c +++ b/src/proof/ssc/sscSim.c @@ -82,6 +82,24 @@ static inline int Ssc_SimFindBit( word * pSim, int nWords ) return -1; } +static inline int Ssc_SimCountBitsWord( word x ) +{ + x = x - ((x >> 1) & ABC_CONST(0x5555555555555555)); + x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333)); + x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F); + x = x + (x >> 8); + x = x + (x >> 16); + x = x + (x >> 32); + return (int)(x & 0xFF); +} +static inline int Ssc_SimCountBits( word * pSim, int nWords ) +{ + int w, Counter = 0; + for ( w = 0; w < nWords; w++ ) + Counter += Ssc_SimCountBitsWord(pSim[w]); + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -245,6 +263,14 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) ); return vInit; } +Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ) +{ + Vec_Int_t * vInit; + Ssc_GiaRandomPiPattern( p, 1, NULL ); + Ssc_GiaSimRound( p ); + vInit = Ssc_GiaGetOneSim( p ); + return vInit; +} /**Function************************************************************* @@ -257,13 +283,22 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ) +int Ssc_GiaCountCaresSim( Gia_Man_t * p ) { - Vec_Int_t * vInit; - Ssc_GiaRandomPiPattern( p, 1, NULL ); + Gia_Obj_t * pObj; + int i, Count, nWords = Gia_ObjSimWords( p ); + word * pRes = ABC_FALLOC( word, nWords ); + Gia_ManForEachPo( p, pObj, i ) + Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 ); + Count = Ssc_SimCountBits( pRes, nWords ); + ABC_FREE( pRes ); + return Count; +} +int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords ) +{ + Ssc_GiaRandomPiPattern( p, nWords, NULL ); Ssc_GiaSimRound( p ); - vInit = Ssc_GiaGetOneSim( p ); - return vInit; + return Ssc_GiaCountCaresSim( p ); } //////////////////////////////////////////////////////////////////////// |