From 2f3a9f91e51f6d1f8bab5e8b6b2fbb71fbd345ca Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jun 2012 12:38:36 -0700 Subject: Bug fix when &vta returns empty absraction. --- src/aig/gia/giaAbsGla.c | 3 ++- src/aig/gia/giaAbsVta.c | 35 ++++++++++++++++++++--------------- 2 files changed, 22 insertions(+), 16 deletions(-) diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 1732c92e..56c65011 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -854,7 +854,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) pPars->fDumpVabs = nDumpOld; // create gate classes Vec_IntFreeP( &pAig->vGateClasses ); - pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses ); + if ( pAig->vObjClasses ) + pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses ); Vec_IntFreeP( &pAig->vObjClasses ); } if ( RetValue == 0 || pAig->vGateClasses == NULL ) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 7e4288fc..24856d17 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1630,24 +1630,29 @@ finish: // analize the results if ( pCex == NULL ) { - assert( Vec_PtrSize(p->vCores) > 0 ); - if ( pAig->vObjClasses != NULL ) - Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); - Vec_IntFreeP( &pAig->vObjClasses ); - pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); - if ( Status == -1 ) + if ( Vec_PtrSize(p->vCores) == 0 ) + Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " ); + else { - if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) - Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); - else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) - Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); - else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 ) - Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); + assert( Vec_PtrSize(p->vCores) > 0 ); + if ( pAig->vObjClasses != NULL ) + Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); + Vec_IntFreeP( &pAig->vObjClasses ); + pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); + if ( Status == -1 ) + { + if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) + Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); + else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) + Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); + else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 ) + Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); + else + Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); + } else - Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); + Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); } - else - Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); } else { -- cgit v1.2.3