diff options
Diffstat (limited to 'src/aig/saig/saigBmc3.c')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index a67f84f3..cf19947a 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1248,11 +1248,11 @@ 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( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%5.0f Mb", 1.0+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 ); +// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); +// ABC_PRMn( "SAT", 42 * 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" ); @@ -1310,11 +1310,11 @@ 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( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%5.0f Mb", 1.0+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 ); +// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); +// ABC_PRMn( "SAT", 42 * 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" ); @@ -1329,8 +1329,8 @@ clkOther += clock() - clk2; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { -// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); -// ABC_PRM( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); +// 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" ); |