diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-27 09:49:13 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-27 09:49:13 -0700 |
| commit | 0cad45fa900133942fedc7ea22bc4802e57d9ca0 (patch) | |
| tree | 95fa3328c6962997f1233146fb696f30560a08ab /src/opt/sfm | |
| parent | fb6eaaf5d9e26d7b0ac326fa17a8c7379b24df68 (diff) | |
| download | abc-0cad45fa900133942fedc7ea22bc4802e57d9ca0.tar.gz abc-0cad45fa900133942fedc7ea22bc4802e57d9ca0.tar.bz2 abc-0cad45fa900133942fedc7ea22bc4802e57d9ca0.zip | |
New MFS package.
Diffstat (limited to 'src/opt/sfm')
| -rw-r--r-- | src/opt/sfm/sfmCore.c | 7 | ||||
| -rw-r--r-- | src/opt/sfm/sfmNtk.c | 8 |
2 files changed, 9 insertions, 6 deletions
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 92f94562..f9d7e914 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -255,6 +255,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) { int i, k, Counter = 0; p->timeTotal = clock(); + if ( pPars->fVerbose ) + printf( "Performing MFS with %d fixed objected.\n", Vec_StrSum(p->vFixed) ); p->pPars = pPars; Sfm_NtkPrepare( p ); // Sfm_ComputeInterpolantCheck( p ); @@ -270,7 +272,10 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 ) continue; for ( k = 0; Sfm_NodeResub(p, i); k++ ) - ; + { +// Counter++; +// break; + } Counter += (k > 0); } p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p); diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 2042eaec..da5b4d60 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -57,7 +57,7 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) ); // POs have one fanout if ( i + nPos >= Vec_WecSize(vFanins) ) - assert( Vec_StrEntry(vFixed, i) == (char)0 ); + assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 ); } } @@ -254,8 +254,7 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode ) Sfm_ObjForEachFanin( p, iNode, iFanin, i ) { int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue ); - if ( Sfm_ObjFanoutNum(p, iFanin) == 0 ) - Sfm_NtkDeleteObj_rec( p, iFanin ); + Sfm_NtkDeleteObj_rec( p, iFanin ); } Vec_IntClear( Sfm_ObjFiArray(p, iNode) ); Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 ); @@ -281,8 +280,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth Sfm_ObjForEachFanin( p, iNode, iFanin, f ) { int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue ); - if ( Sfm_ObjFanoutNum(p, iFanin) == 0 ) - Sfm_NtkDeleteObj_rec( p, iFanin ); + Sfm_NtkDeleteObj_rec( p, iFanin ); } Vec_IntClear( Sfm_ObjFiArray(p, iNode) ); } |