diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-15 09:51:33 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-15 09:51:33 -0700 |
| commit | 675b0892a88a7332c8949e4fd4741ce56642fb5e (patch) | |
| tree | 01d90cdf1e54fea0468d593bfb02972408c4cb0e /src/aig | |
| parent | 2f1f0ac93dbd280dbe944e258ab48296759d3493 (diff) | |
| download | abc-675b0892a88a7332c8949e4fd4741ce56642fb5e.tar.gz abc-675b0892a88a7332c8949e4fd4741ce56642fb5e.tar.bz2 abc-675b0892a88a7332c8949e4fd4741ce56642fb5e.zip | |
Reporing memory usage by the SAT solver in 'bmc3'.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index fb19783a..a67f84f3 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1242,13 +1242,14 @@ clkOther += clock() - clk2; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { - printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); - printf( "Var =%8.0f. ", (double)p->nSatVars ); - printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); - printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); + printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); + printf( "Var =%8.0f. ", (double)p->nSatVars ); + 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 ); // ABC_PRT( "Time", clock() - clk ); - printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); // ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); @@ -1309,7 +1310,8 @@ clkOther += clock() - clk2; printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); - printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); // ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); |