diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-04 16:59:28 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-04 16:59:28 -0800 |
| commit | ef893337741de07a94d2cf6056b1ca6822a5e28e (patch) | |
| tree | 492478c47f3eb725a0c18becc02378468be0af2a /src/aig/saig/saigSimExt.c | |
| parent | 148a786b694b5cad9035e53f35a349d6274f0291 (diff) | |
| download | abc-ef893337741de07a94d2cf6056b1ca6822a5e28e.tar.gz abc-ef893337741de07a94d2cf6056b1ca6822a5e28e.tar.bz2 abc-ef893337741de07a94d2cf6056b1ca6822a5e28e.zip | |
Improved the speed of refinement algorithm in &abs_refine.
Diffstat (limited to 'src/aig/saig/saigSimExt.c')
| -rw-r--r-- | src/aig/saig/saigSimExt.c | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index 9828d17e..ac0fa697 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -28,10 +28,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define SAIG_ZER 1 -#define SAIG_ONE 2 -#define SAIG_UND 3 - static inline int Saig_ManSimInfoNot( int Value ) { if ( Value == SAIG_ZER ) @@ -521,7 +517,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Abc_C SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose ) { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; @@ -537,8 +533,10 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, A Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); -// vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + if ( fTryFour ) + vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + else + vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); |