diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecCorr.c | 36 | ||||
| -rw-r--r-- | src/proof/ssw/ssw.h | 1 | ||||
| -rw-r--r-- | src/proof/ssw/sswCore.c | 25 |
4 files changed, 58 insertions, 5 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 ); 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: |