Commit 37b8a190 by Alan Mishchenko

Improving printout in the SAT solver.

parent c48925df
...@@ -1592,7 +1592,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit ...@@ -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.conflicts,
(double)s->stats.clauses, (double)s->stats.clauses,
(double)s->stats.clauses_literals, (double)s->stats.clauses_literals,
(double)nof_learnts, // (double)nof_learnts,
(double)0,
(double)s->stats.learnts, (double)s->stats.learnts,
(double)s->stats.learnts_literals, (double)s->stats.learnts_literals,
Ratio, Ratio,
......
...@@ -1765,7 +1765,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -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.conflicts,
(double)s->stats.clauses, (double)s->stats.clauses,
(double)s->stats.clauses_literals, (double)s->stats.clauses_literals,
(double)nof_learnts, // (double)nof_learnts,
(double)0,
(double)s->stats.learnts, (double)s->stats.learnts,
(double)s->stats.learnts_literals, (double)s->stats.learnts_literals,
(s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts, (s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment