From 429f52ce15d1c10e71d98d8c1388b93809a425e1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 18 Feb 2017 14:20:10 -0800 Subject: Experiments with SAT sweeping. --- src/sat/bmc/bmcGen.c | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'src/sat/bmc/bmcGen.c') diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c index 5d84ce87..460c9fec 100644 --- a/src/sat/bmc/bmcGen.c +++ b/src/sat/bmc/bmcGen.c @@ -46,13 +46,13 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj ) { - return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi ); + return Vec_WrdEntryP( p->vSims, iObj * p->nSimWords ); } static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj ) { int w; word * pSims = Gia_ManMoObj( p, iObj ); - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = Gia_ManRandomW( 0 ); } static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj ) @@ -65,19 +65,19 @@ static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj ) if ( Gia_ObjFaninC0(pObj) ) { if ( Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = ~(pSims0[w] | pSims1[w]); else - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = ~pSims0[w] & pSims1[w]; } else { if ( Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = pSims0[w] & ~pSims1[w]; else - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = pSims0[w] & pSims1[w]; } } @@ -89,12 +89,12 @@ static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj ) word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) ); if ( Gia_ObjFaninC0(pObj) ) { - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = ~pSims0[w]; } else { - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = pSims0[w]; } } @@ -102,7 +102,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords ) { int i, iObj; Gia_ManRandomW( 1 ); - p->iPatsPi = nWords; + p->nSimWords = nWords; if ( p->vSims ) Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 ); else -- cgit v1.2.3