diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 12:24:30 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 12:24:30 -0700 |
| commit | d3a4dce10e89fa86f0feb2a7b53debdaa60fa3e4 (patch) | |
| tree | 725c0657404f52b38b30526e10fdd9aaed73cd4b /src/sat/bmc/bmcBmc3.c | |
| parent | cc7d3e3747f0e1f397945eaac63120401a49d5c1 (diff) | |
| download | abc-d3a4dce10e89fa86f0feb2a7b53debdaa60fa3e4.tar.gz abc-d3a4dce10e89fa86f0feb2a7b53debdaa60fa3e4.tar.bz2 abc-d3a4dce10e89fa86f0feb2a7b53debdaa60fa3e4.zip | |
Updating bmc3 printout to show the number of failed outputs.
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index c60be593..a6a7e71b 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1519,9 +1519,9 @@ clkOther += clock() - clk2; printf( "%4d %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( "Cnf =%7.0f. ", (double)p->pSat->stats.conflicts ); // printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); - printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) ); + printf( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) ); // ABC_PRT( "Time", clock() - clk ); printf( "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) ); printf( "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); @@ -1577,9 +1577,11 @@ clkOther += clock() - clk2; printf( "%4d %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( "Cnf =%7.0f. ",(double)p->pSat->stats.conflicts ); // printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); - printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) ); + printf( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) ); + if ( pPars->fSolveAll ) + printf( "CEX =%7d. ", pPars->nFailOuts ); // ABC_PRT( "Time", clock() - clk ); // printf( "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) ); printf( "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) ); |