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/ssw | |
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/ssw')
-rw-r--r-- | src/proof/ssw/ssw.h | 1 | ||||
-rw-r--r-- | src/proof/ssw/sswCore.c | 25 |
2 files changed, 24 insertions, 2 deletions
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index 9bd83964..c8275b7a 100644 --- a/src/proof/ssw/ssw.h +++ b/src/proof/ssw/ssw.h @@ -55,6 +55,7 @@ struct Ssw_Pars_t_ int nResimDelta; // the number of nodes to resimulate int nStepsMax; // (scorr only) the max number of induction steps int TimeLimit; // time out in seconds + int nLimitMax; // the limit on the number of iterations int fPolarFlip; // uses polarity adjustment int fLatchCorr; // perform register correspondence int fConstCorr; // perform constant correspondence diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c index 1036d7b4..b48db953 100644 --- a/src/proof/ssw/sswCore.c +++ b/src/proof/ssw/sswCore.c @@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) { int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques; Aig_Man_t * pAigNew; - int RetValue, nIter = -1; + int RetValue, nIter = -1, nPrev[4] = {0}; abctime clk, clkTotal = Abc_Clock(); // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); @@ -352,7 +352,7 @@ clk = Abc_Clock(); { printf( "Iterative refinement is stopped after iteration %d\n", nIter ); printf( "because the property output is no longer a candidate constant.\n" ); - // prepare to quite + // prepare to quit p->nLitsEnd = p->nLitsBeg; p->nNodesEnd = p->nNodesBeg; p->nRegsEnd = p->nRegsBeg; @@ -381,6 +381,27 @@ clk = Abc_Clock(); break; if ( p->pPars->pFunc ) ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); + if ( p->pPars->nLimitMax ) + { + int nCur = Ssw_ClassesCand1Num(p->ppClasses); + if ( nIter > 4 && nPrev[0] - nCur <= 4*p->pPars->nLimitMax ) + { + printf( "Iterative refinement is stopped after iteration %d\n", nIter ); + printf( "because the refinment is very slow.\n" ); + // prepare to quit + p->nLitsEnd = p->nLitsBeg; + p->nNodesEnd = p->nNodesBeg; + p->nRegsEnd = p->nRegsBeg; + // cleanup + Aig_ManSetPhase( p->pAig ); + Aig_ManCleanMarkB( p->pAig ); + return Aig_ManDupSimple( p->pAig ); + } + nPrev[0] = nPrev[1]; + nPrev[1] = nPrev[2]; + nPrev[2] = nPrev[3]; + nPrev[3] = nCur; + } } finalize: |