diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-30 11:39:21 +0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-30 11:39:21 +0800 |
| commit | d103c4e28687ee9d91766c7d1057107e0100e7e3 (patch) | |
| tree | cc4ce137a35dc633bc1ec5861b008a39b9afbeeb /src/sat/bmc/bmcBmcS.c | |
| parent | ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 (diff) | |
| download | abc-d103c4e28687ee9d91766c7d1057107e0100e7e3.tar.gz abc-d103c4e28687ee9d91766c7d1057107e0100e7e3.tar.bz2 abc-d103c4e28687ee9d91766c7d1057107e0100e7e3.zip | |
Small changes to printouts in &bmcs.
Diffstat (limited to 'src/sat/bmc/bmcBmcS.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index ea8ec2f6..99cc99dc 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -851,11 +851,13 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) { + abctime clk = Abc_Clock(); int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, (f+k) * Gia_ManPoNum(pGia) + i) ); int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 ); if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) break; status = Bmcs_ManPerform_Solve( p, iLit, WorkerThread, ThData, pPars->nProcs, &Solver ); + p->timeSat += Abc_Clock() - clk; if ( status == l_False ) // unsat { if ( i == Gia_ManPoNum(pGia)-1 ) @@ -896,11 +898,11 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ThData[i].fWorking = 1; } p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSat; - Bmcs_ManPrintTime( p ); - Bmcs_ManStop( p ); if ( RetValue == -1 && !pPars->fNotVerbose ) printf( "No output failed in %d frames. ", f + (k < pPars->nFramesAdd ? k+1 : 0) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Bmcs_ManPrintTime( p ); + Bmcs_ManStop( p ); return RetValue; } |