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

Adding an option to bmc3 to use Satoko intead of the default SAT solver.

This commit is contained in:
Alan Mishchenko 2017-08-16 15:02:47 +07:00
parent 85eee2ea96
commit 7365052411
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -575,7 +575,7 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim
if ( !p->pPars->fVerbose )
return;
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
#ifdef ABC_USE_EXT_SOLVERS
#ifndef ABC_USE_EXT_SOLVERS
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]) );