From 247dd95dd3d501527f11f453ac2c52661cee64be Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 21 Sep 2013 14:08:38 -0400 Subject: Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement. --- src/proof/abs/absGla.c | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/proof/abs') 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; -- cgit v1.2.3