From d80bbe74007e972e3b7a7667eaccf1599288c702 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 16 Aug 2017 15:46:02 +0700
Subject: Adding runtime profile to &bmcs.
---
src/sat/bmc/bmcBmcS.c | 27 ++++++++++++++++++++++++++-
1 file changed, 26 insertions(+), 1 deletion(-)
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c
index e1533779..1bfcd9d0 100644
--- a/src/sat/bmc/bmcBmcS.c
+++ b/src/sat/bmc/bmcBmcS.c
@@ -81,6 +81,10 @@ struct Bmcs_Man_t_
int nSatVars; // number of SAT variables used
int nSatVarsOld; // number of SAT variables used
int fStopNow; // signal when it is time to stop
+ abctime timeUnf; // runtime of unfolding
+ abctime timeCnf; // runtime of CNF generation
+ abctime timeSat; // runtime of the solvers
+ abctime timeOth; // other runtime
};
//static inline int * Bmcs_ManCopies( Bmcs_Man_t * p, int f ) { return (int*)Vec_PtrEntry(&p->vGia2Fr, f % Vec_PtrSize(&p->vGia2Fr)); }
@@ -533,12 +537,15 @@ Gia_Man_t * Bmcs_ManUnfold( Bmcs_Man_t * p, int f, int nFramesAdd )
}
Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd )
{
+ abctime clk = Abc_Clock();
Gia_Man_t * pNew = Bmcs_ManUnfold( p, f, nFramesAdd );
Cnf_Dat_t * pCnf;
Gia_Obj_t * pObj;
int i, iVar, * pMap;
+ p->timeUnf += Abc_Clock() - clk;
if ( pNew == NULL )
return NULL;
+ clk = Abc_Clock();
pCnf = Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 );
pMap = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
pMap[0] = 0;
@@ -555,6 +562,7 @@ Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd )
for ( i = 0; i < pCnf->nLiterals; i++ )
pCnf->pClauses[0][i] = Abc_Lit2LitV( pMap, pCnf->pClauses[0][i] );
ABC_FREE( pMap );
+ p->timeCnf += Abc_Clock() - clk;
return pCnf;
}
@@ -579,7 +587,7 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim
Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) );
Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) );
Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) );
- Abc_Print( 1, "Conf =%7.0f. ", (double)solver_conflictnum(p->pSats[0]) );
+ Abc_Print( 1, "Conf =%9.0f. ", (double)solver_conflictnum(p->pSats[0]) );
#else
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses );
@@ -591,6 +599,17 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim
printf( "\n" );
fflush( stdout );
}
+void Bmcs_ManPrintTime( Bmcs_Man_t * p )
+{
+ abctime clkTotal = p->timeUnf + p->timeCnf + p->timeSat + p->timeOth;
+ if ( !p->pPars->fVerbose )
+ return;
+ ABC_PRTP( "Unfolding ", p->timeUnf, clkTotal );
+ ABC_PRTP( "CNF generation", p->timeCnf, clkTotal );
+ ABC_PRTP( "SAT solving ", p->timeSat, clkTotal );
+ ABC_PRTP( "Other ", p->timeOth, clkTotal );
+ ABC_PRTP( "TOTAL ", clkTotal , clkTotal );
+}
Abc_Cex_t * Bmcs_ManGenerateCex( Bmcs_Man_t * p, int i, int f, int s )
{
Abc_Cex_t * pCex = Abc_CexMakeTriv( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), Gia_ManPoNum(p->pGia), f*Gia_ManPoNum(p->pGia)+i );
@@ -643,11 +662,13 @@ int Bmcs_ManPerformOne( 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 = bmc_sat_solver_solve( p->pSats[0], &iLit, 1 );
+ p->timeSat += Abc_Clock() - clk;
if ( status == l_False ) // unsat
{
if ( i == Gia_ManPoNum(pGia)-1 )
@@ -680,6 +701,8 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( k < pPars->nFramesAdd )
break;
}
+ 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) );
@@ -873,6 +896,8 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
ThData[i].pSat = NULL;
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) );
--
cgit v1.2.3