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 | |
| parent | f9da2c790f68462fd68924c94ecf6f02d442632a (diff) | |
| download | abc-7bc2fb51995cc775be5a273e2854d7e2f7577ea7.tar.gz abc-7bc2fb51995cc775be5a273e2854d7e2f7577ea7.tar.bz2 abc-7bc2fb51995cc775be5a273e2854d7e2f7577ea7.zip | |
SAT variable profiling.
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 12 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 62bed4c1..7222ad1d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21479,7 +21479,7 @@ usage: Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract ); Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart ); Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta ); - Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce ); + Abc_Print( -2, "\t-R num : percentage to keep for learned clause removal [default = %d]\n", pPars->nLearnedPerce ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); 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 ); |