diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-29 12:38:36 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-29 12:38:36 -0700 |
| commit | 2f3a9f91e51f6d1f8bab5e8b6b2fbb71fbd345ca (patch) | |
| tree | a631858580ec3fa6cef2497494820a3875db08c0 /src/aig/gia | |
| parent | 5d5ff3b99e111f3623e8b631d380b1d253810895 (diff) | |
| download | abc-2f3a9f91e51f6d1f8bab5e8b6b2fbb71fbd345ca.tar.gz abc-2f3a9f91e51f6d1f8bab5e8b6b2fbb71fbd345ca.tar.bz2 abc-2f3a9f91e51f6d1f8bab5e8b6b2fbb71fbd345ca.zip | |
Bug fix when &vta returns empty absraction.
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 3 | ||||
| -rw-r--r-- | 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 { |