diff options
Diffstat (limited to 'src/proof/ssw/sswCore.c')
| -rw-r--r-- | src/proof/ssw/sswCore.c | 25 |
1 files changed, 23 insertions, 2 deletions
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: |