diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-21 14:08:38 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-21 14:08:38 -0400 |
| commit | 247dd95dd3d501527f11f453ac2c52661cee64be (patch) | |
| tree | a16c29d35fb410031d2548e8d1aa958f3fb9f206 /src/proof/abs | |
| parent | d32e51409ffb7b06589b12b04520ca57bf4eda86 (diff) | |
| download | abc-247dd95dd3d501527f11f453ac2c52661cee64be.tar.gz abc-247dd95dd3d501527f11f453ac2c52661cee64be.tar.bz2 abc-247dd95dd3d501527f11f453ac2c52661cee64be.zip | |
Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement.
Diffstat (limited to 'src/proof/abs')
| -rw-r--r-- | src/proof/abs/absGla.c | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 5daa953f..7a70cddb 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1658,6 +1658,12 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Vec_IntFree( vPPis ); if ( pPars->fVerbose ) Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 ); + // check if the number of objects is below limit + if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin/2) / 100 ) + { + Status = l_Undef; + goto finish; + } continue; } p->timeUnsat += Abc_Clock() - clk2; @@ -1823,6 +1829,8 @@ finish: Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 ) Abc_Print( 1, "GLA found the ratio of abstracted objects to exceed %d %% in frame %d. ", pPars->nRatioMin, p->pPars->iFrameProved+1 ); + else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin/2) / 100 ) + Abc_Print( 1, "GLA found the ratio of abstracted objects during refinement to exceed %d %% in frame %d. ", pPars->nRatioMin/2, p->pPars->iFrameProved+1 ); else Abc_Print( 1, "GLA finished %d frames and produced a %d-stable abstraction. ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); p->pPars->iFrame = p->pPars->iFrameProved; |