diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 11:20:07 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 11:20:07 -0700 |
| commit | 7bc2fb51995cc775be5a273e2854d7e2f7577ea7 (patch) | |
| tree | 5fd274521eec83824d4245bf3dc05afae04c8537 /src/sat/bmc/bmcBmc3.c | |
| parent | f9da2c790f68462fd68924c94ecf6f02d442632a (diff) | |
| download | abc-7bc2fb51995cc775be5a273e2854d7e2f7577ea7.tar.gz abc-7bc2fb51995cc775be5a273e2854d7e2f7577ea7.tar.bz2 abc-7bc2fb51995cc775be5a273e2854d7e2f7577ea7.zip | |
SAT variable profiling.
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index e3fb8c68..8d1f6ea8 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -761,8 +761,14 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne ) void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) { if ( p->pPars->fVerbose ) - printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. Hash overs = %d. UniProps = %d.\n", - p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps ); + { + int nUsedVars = sat_solver_count_usedvars(p->pSat); + printf( "LStart(P) = %d LDelta(Q) = %d LRatio(R) = %d ReduceDB = %d Vars = %d Used = %d (%.2f %%)\n", + p->pSat->nLearntStart, p->pSat->nLearntDelta, p->pSat->nLearntRatio, + p->pSat->nDBreduces, p->pSat->size, nUsedVars, 100.0*nUsedVars/p->pSat->size ); + printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. Hash overs = %d. UniProps = %d.\n", + p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps ); + } // Aig_ManCleanMarkA( p->pAig ); if ( p->vCexes ) { @@ -1642,7 +1648,7 @@ nTimeUndec += clock() - clk2; } printf( "%4d %s : ", f, fUnfinished ? "-" : "+" ); printf( "Var =%8.0f. ", (double)p->nSatVars ); - printf( "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) ); +// printf( "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); // printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); |