diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-18 23:52:41 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-18 23:52:41 -0700 |
| commit | 1fe2ba9ac0787906573f7b1cadf5ff535ee7444f (patch) | |
| tree | 7bad88053a17eee658f19c573bf2f6a418f8466c /src/aig | |
| parent | 6b2da3978f69aa107568ed2a03845376d136a9b4 (diff) | |
| download | abc-1fe2ba9ac0787906573f7b1cadf5ff535ee7444f.tar.gz abc-1fe2ba9ac0787906573f7b1cadf5ff535ee7444f.tar.bz2 abc-1fe2ba9ac0787906573f7b1cadf5ff535ee7444f.zip | |
Enabling &gla for combinational miters.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 15 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 2 |
2 files changed, 9 insertions, 8 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index bc9a0505..9891a904 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1391,6 +1391,8 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p ) { nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj); assert( nUsageCount >= 0 ); + if ( nUsageCount == 0 ) + nUsageCount++; pGiaObj = Gla_ManGiaObj( p, pObj ); if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) ) { @@ -1918,15 +1920,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) clk2 = clock(); vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); assert( (vCore != NULL) == (Status == 1) ); - if ( Status == -1 ) // resource limit is reached + if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached { - Gla_ManRollBack( p ); - goto finish; - } - // check timeout - if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) - { - Gla_ManRollBack( p ); + if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration + Gla_ManRollBack( p ); goto finish; } if ( vCore != NULL ) @@ -2053,6 +2050,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) } finish: // analize the results + if ( p->pPars->fVerbose ) + printf( "\n" ); if ( pCex == NULL ) { if ( pAig->vGateClasses != NULL ) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 85d51a42..7d4bc65a 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1698,6 +1698,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) } finish: // analize the results + if ( p->pPars->fVerbose ) + printf( "\n" ); if ( pCex == NULL ) { if ( Vec_PtrSize(p->vCores) == 0 ) |