diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 14:41:36 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 14:41:36 +0700 |
| commit | c5131ca85fed7d75f84bd95c252e01751ce1351a (patch) | |
| tree | 94579b69141ea470dd6ae23a41d49d01dceb4b2d /src/sat/bmc/bmcBmcS.c | |
| parent | 23d36a8d5665d7a586777c9723c4aa803b253fc1 (diff) | |
| download | abc-c5131ca85fed7d75f84bd95c252e01751ce1351a.tar.gz abc-c5131ca85fed7d75f84bd95c252e01751ce1351a.tar.bz2 abc-c5131ca85fed7d75f84bd95c252e01751ce1351a.zip | |
Changing enconding of the SAT solver return value in &bmcs.
Diffstat (limited to 'src/sat/bmc/bmcBmcS.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 1366ce31..62db26eb 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -573,14 +573,15 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim int fUnfinished = 0; if ( !p->pPars->fVerbose ) return; - Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); - Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); // solver_varnum(p->pSats[0]) - Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses ); // solver_clausenum(p->pSats[0]) - Abc_Print( 1, "Conf =%7.0f. ", (double)0 ); // solver_conflictnum(p->pSats[0]) + Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); + Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) ); + Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) ); + Abc_Print( 1, "Conf =%7.0f. ", (double)solver_conflictnum(p->pSats[0]) ); if ( p->pPars->nProcs > 1 ) - Abc_Print( 1, "S = %3d. ", Solver ); - Abc_Print( 1, "%4.0f MB", 1.0*((int)Gia_ManMemory(p->pFrames) + Vec_IntMemory(&p->vFr2Sat))/(1<<20) ); - Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkStart)/(float)(CLOCKS_PER_SEC) ); + Abc_Print( 1, "S = %3d. ", Solver ); + Abc_Print( 1, "%4.0f MB", 1.0*((int)Gia_ManMemory(p->pFrames) + Vec_IntMemory(&p->vFr2Sat))/(1<<20) ); + Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkStart)/(float)(CLOCKS_PER_SEC) ); printf( "\n" ); fflush( stdout ); } |