diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-04-24 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-04-24 08:01:00 -0700 |
| commit | d7a048d738381651b53340684e26f06b78b8a78c (patch) | |
| tree | 82f7bea9d0750a388494e6fffceb61cfeff969b7 /src/aig/saig/saigAbs.c | |
| parent | 77fab468ad32d15de5c065c211f6f74371670940 (diff) | |
| download | abc-d7a048d738381651b53340684e26f06b78b8a78c.tar.gz abc-d7a048d738381651b53340684e26f06b78b8a78c.tar.bz2 abc-d7a048d738381651b53340684e26f06b78b8a78c.zip | |
Version abc90424
Diffstat (limited to 'src/aig/saig/saigAbs.c')
| -rw-r--r-- | src/aig/saig/saigAbs.c | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index a2a915f7..f6845acd 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -869,9 +869,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, Aig_ManPrintStats( pResult ); else printf( " -----------------------------------------------------\n" ); + if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio ) + { + printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio ); + break; + } } } - Vec_IntFree( vFlops ); return pResult; } |