diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2022-04-24 08:53:57 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2022-04-24 08:53:57 -0700 |
commit | 8e13245ed06099734d10942715488ff2dc5b3186 (patch) | |
tree | 39f2e7fe6c1f22be0b0f1754ac7bfed706665ac1 /src/proof/cec | |
parent | b79f37ae57c891640240f1b5a39c70d58f75d8ac (diff) | |
download | abc-8e13245ed06099734d10942715488ff2dc5b3186.tar.gz abc-8e13245ed06099734d10942715488ff2dc5b3186.tar.bz2 abc-8e13245ed06099734d10942715488ff2dc5b3186.zip |
Adding switch to stop scorr if refinement is too slow.
Diffstat (limited to 'src/proof/cec')
-rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
-rw-r--r-- | src/proof/cec/cecCorr.c | 36 |
2 files changed, 34 insertions, 3 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 40aa9799..92a08b3e 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -149,6 +149,7 @@ struct Cec_ParCor_t_ int nBTLimit; // conflict limit at a node int nLevelMax; // (scorr only) the max number of levels int nStepsMax; // (scorr only) the max number of induction steps + int nLimitMax; // (scorr only) stop after this many iterations if little or no improvement int fLatchCorr; // consider only latch outputs int fConstCorr; // consider only constants int fUseRings; // use rings diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index ce7e0885..8614ab07 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -756,6 +756,21 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte Abc_Print( 1, "%c ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' ); Abc_PrintTime( 1, "T", Time ); } +int Cec_ManCountLits( Gia_Man_t * p ) +{ + int i, CounterX = 0, Counter0 = 0, Counter = 0; + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + { + if ( Gia_ObjIsNone(p, i) ) + CounterX++; + else if ( Gia_ObjIsConst(p, i) ) + Counter0++; + else if ( Gia_ObjIsHead(p, i) ) + Counter++; + } + CounterX -= Gia_ManCoNum(p); + return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; +} /**Function************************************************************* @@ -777,7 +792,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr Vec_Int_t * vCexStore; Cec_ManSim_t * pSim; Gia_Man_t * pSrm; - int fChanges, RetValue; + int fChanges, RetValue, i; // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; @@ -791,7 +806,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->fVerbose = pPars->fVerbose; fChanges = 1; - while ( fChanges ) + for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ ) { abctime clkBmc = Abc_Clock(); fChanges = 0; @@ -918,7 +933,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Cec_ManSim_t * pSim; Gia_Man_t * pSrm; - int r, RetValue; + int r, RetValue, nPrev[4] = {0}; abctime clkTotal = Abc_Clock(); abctime clkSat = 0, clkSim = 0, clkSrm = 0; abctime clk2, clk = Abc_Clock(); @@ -1031,6 +1046,21 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ManSimStop( pSim ); return 0; } + if ( pPars->nLimitMax ) + { + int nCur = Cec_ManCountLits(pAig); + if ( r > 4 && nPrev[0] - nCur <= 4*pPars->nLimitMax ) + { + printf( "Iterative refinement is stopped after iteration %d\n", r ); + printf( "because refinement does not proceed quickly.\n" ); + Cec_ManSimStop( pSim ); + return 0; + } + nPrev[0] = nPrev[1]; + nPrev[1] = nPrev[2]; + nPrev[2] = nPrev[3]; + nPrev[3] = nCur; + } } if ( pPars->fVerbose ) Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk ); |