summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-01-13 20:57:26 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-01-13 20:57:26 -0800
commit37b8a190baa91c69dcbd4300f03e209e19fb5b9b (patch)
treefc473dbca5755a06e2e8112517b96c9af8480535 /src/sat/bsat
parentc48925dfb66f9194d00cd560aba9c724919fe3f1 (diff)
downloadabc-37b8a190baa91c69dcbd4300f03e209e19fb5b9b.tar.gz
abc-37b8a190baa91c69dcbd4300f03e209e19fb5b9b.tar.bz2
abc-37b8a190baa91c69dcbd4300f03e209e19fb5b9b.zip
Improving printout in the SAT solver.
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satSolver.c3
-rw-r--r--src/sat/bsat/satSolver2.c3
2 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 188a504f..8a3cbc33 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1592,7 +1592,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
(double)s->stats.conflicts,
(double)s->stats.clauses,
(double)s->stats.clauses_literals,
- (double)nof_learnts,
+// (double)nof_learnts,
+ (double)0,
(double)s->stats.learnts,
(double)s->stats.learnts_literals,
Ratio,
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 1f46d88c..f4625d51 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1765,7 +1765,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
(double)s->stats.conflicts,
(double)s->stats.clauses,
(double)s->stats.clauses_literals,
- (double)nof_learnts,
+// (double)nof_learnts,
+ (double)0,
(double)s->stats.learnts,
(double)s->stats.learnts_literals,
(s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts,