diff options
-rw-r--r-- | src/aig/gia/giaAbs.c | 7 | ||||
-rw-r--r-- | src/aig/saig/saigGlaPba.c | 6 | ||||
-rw-r--r-- | src/base/abci/abc.c | 13 |
3 files changed, 14 insertions, 12 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index ab964c51..165bc996 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -484,8 +484,11 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) pGia->vGateClasses = vGateClasses; } // clean up the abstraction map - pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); - Gia_ManStop( pGiaAbs ); + if ( pGia->vGateClasses ) + { + pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); + Gia_ManStop( pGiaAbs ); + } if ( p->fVerbose ) Gia_ManPrintStats( pGia, 0 ); return 1; diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index fce2372f..50f6fce8 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -579,7 +579,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in return NULL; } sat_solver_set_random( p->pSat, fSkipRand ); - p->timePre += Abc_Clock(1,0); + p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; // set runtime limit if ( TimeLimit ) @@ -593,8 +593,8 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in Aig_Gla2ManStop( p ); return NULL; } - p->timeSat += Abc_Clock(1,0); - p->timeTotal = Abc_Clock(0,0); + p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; + p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC; // print stats if ( fVerbose ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 81b82f73..32ed17eb 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28952,8 +28952,8 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) Saig_ParBmc_t Pars, * pPars = &Pars; int c, fNaiveCnf = 0; Saig_ParBmcSetDefaultParams( pPars ); - pPars->nStart = 0; // (pAbc->nFrames >= 0) ? pAbc->nFrames : 0; - pPars->nFramesMax = 0; // pPars->nStart + 10; + pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0; + pPars->nFramesMax = 0; pPars->nConfLimit = 0; pPars->nTimeOut = 60; Extra_UtilGetoptReset(); @@ -29054,10 +29054,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf ); - if ( pPars->nStart == 0 ) +// if ( pPars->nStart == 0 ) pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); -// printf( "This command is currently not enabled.\n" ); return 0; usage: @@ -29090,8 +29089,8 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) Saig_ParBmc_t Pars, * pPars = &Pars; int c; Saig_ParBmcSetDefaultParams( pPars ); - pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0; - pPars->nFramesMax = 10; //pPars->nStart + 10; + pPars->nStart = 0; + pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10; pPars->nConfLimit = 0; pPars->fSkipRand = 0; Extra_UtilGetoptReset(); @@ -29183,7 +29182,7 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nStart ) Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" ); pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars ); - if ( pPars->nStart == 0 ) +// if ( pPars->nStart == 0 ) pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; |