diff options
| -rw-r--r-- | src/base/abci/abc.c | 12 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 16 |
2 files changed, 18 insertions, 10 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index adb3fe47..de686068 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -20906,6 +20906,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ); Saig_ParBmc_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc); + Vec_Ptr_t * vSeqModelVec = NULL; char * pLogFileName = NULL; int fOrDecomp = 0; int c; @@ -21056,18 +21057,19 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + vSeqModelVec = pNtk->vSeqModelVec; pNtk->vSeqModelVec = NULL; if ( pLogFileName ) Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" ); if ( pPars->fSolveAll && pPars->fDropSatOuts ) { - if ( pNtk->vSeqModelVec == NULL ) + if ( vSeqModelVec == NULL ) Abc_Print( 1,"The array of counter-examples is not available.\n" ); - else if ( Vec_PtrSize(pNtk->vSeqModelVec) != Abc_NtkPoNum(pNtk) ) + else if ( Vec_PtrSize(vSeqModelVec) != Abc_NtkPoNum(pNtk) ) Abc_Print( 1,"The array size does not match the number of outputs.\n" ); else { extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose ); - Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose ); + Abc_NtkDropSatOutputs( pNtk, vSeqModelVec, pPars->fVerbose ); pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 ); if ( pNtkRes == NULL ) { @@ -21077,9 +21079,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } } - if ( pNtk->vSeqModelVec ) + if ( vSeqModelVec ) { - Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); pAbc->nFrames = -1; } return 0; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index a6a7e71b..48028f76 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1358,6 +1358,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) clock_t clk, clk2, clkOther = 0, clkTotal = clock(); clock_t nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0; clock_t nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); + clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0; // create BMC manager p = Saig_Bmc3ManStart( pAig ); p->pPars = pPars; @@ -1478,9 +1479,11 @@ clkOther += clock() - clk2; // solve th is output fUnfinished = 0; sat_solver_compress( p->pSat ); +clk2 = clock(); status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_False ) { +nTimeUnsat += clock() - clk2; if ( 1 ) { // add final unit clause @@ -1501,6 +1504,7 @@ clkOther += clock() - clk2; } else if ( status == l_True ) { +nTimeSat += clock() - clk2; fFirst = 0; if ( !pPars->fSolveAll ) { @@ -1555,6 +1559,7 @@ clkOther += clock() - clk2; } else { +nTimeUndec += clock() - clk2; assert( status == l_Undef ); if ( pPars->nFramesJump ) { @@ -1605,11 +1610,12 @@ clkOther += clock() - clk2; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { -// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); -// ABC_PRMn( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); -// printf( "Simples = %6d. ", p->nBufNum ); -// printf( "Dups = %6d. ", p->nDupNum ); -// printf( "\n" ); + printf( "Runtime: " ); + printf( "CNF = %.1f sec (%.1f %%) ", 1.0*clkOther/CLOCKS_PER_SEC, 100.0*clkOther/(clock() - clkTotal) ); + printf( "UNSAT = %.1f sec (%.1f %%) ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(clock() - clkTotal) ); + printf( "SAT = %.1f sec (%.1f %%) ", 1.0*nTimeSat/CLOCKS_PER_SEC, 100.0*nTimeSat/(clock() - clkTotal) ); + printf( "UNDEC = %.1f sec (%.1f %%)", 1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(clock() - clkTotal) ); + printf( "\n" ); } Saig_Bmc3ManStop( p ); fflush( stdout ); |