diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-16 18:57:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-16 18:57:53 -0700 |
| commit | 8b2b4fb6b86680c4dd4ea74979d425a87257d7fe (patch) | |
| tree | 019831919ae56fab599f9989a9fb04f1571cedd4 | |
| parent | 9cbd97b5ef6836c230bedca29494e991648bedc3 (diff) | |
| download | abc-8b2b4fb6b86680c4dd4ea74979d425a87257d7fe.tar.gz abc-8b2b4fb6b86680c4dd4ea74979d425a87257d7fe.tar.bz2 abc-8b2b4fb6b86680c4dd4ea74979d425a87257d7fe.zip | |
Improving printouts in &gla.
| -rw-r--r-- | src/proof/abs/absGla.c | 25 |
1 files changed, 8 insertions, 17 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 5cb7148c..1369015d 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1836,26 +1836,17 @@ finish: Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d. ", p->pPars->iFrameProved+1, iFrameTryToProve ); else if ( pAig->pCexSeq == NULL ) { -// if ( pAig->vGateClasses != NULL ) -// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); - if ( Status == l_Undef ) - { - if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) - Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); - else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) - Abc_Print( 1, "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, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, p->pPars->iFrameProved+1 ); - else - Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", p->pPars->iFrameProved+1 ); - } + if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) + Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); + else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) + 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 - { - p->pPars->iFrame = p->pPars->iFrameProved; - Abc_Print( 1, "GLA completed %d frames and produced a %d-stable abstraction. ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); - } + 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; } else { |