luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changing enconding of the SAT solver return value in &bmcs.

This commit is contained in:
Alan Mishchenko 2017-08-16 14:41:36 +07:00
parent 23d36a8d56
commit c5131ca85f
1 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/sat/bmc/bmcBmcS.c
View File

@ -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 );
}