From 73ce5c5fc80397161403fa2aaaba56c25cecce92 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 13 Sep 2020 19:48:04 -0700
Subject: [PATCH] display similar to sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6ce7c69c8..ded691aa0 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2705,20 +2705,23 @@ namespace smt {
}
void context::log_stats() {
- size_t bin_lemmas = 0;
+ size_t bin_clauses = 0, bin_lemmas = 0;
for (watch_list const& w : m_watches) {
- bin_lemmas += w.end_literals() - w.begin_literals();
+ bin_clauses += w.end_literals() - w.begin_literals();
}
- bin_lemmas /= 2;
+ bin_clauses /= 2;
+ for (clause* cp : m_lemmas)
+ if (cp->get_num_literals() == 2)
+ ++bin_lemmas;
std::stringstream strm;
strm << "(smt.stats "
<< std::setw(4) << m_stats.m_num_restarts << " "
<< std::setw(6) << m_stats.m_num_conflicts << " "
<< std::setw(6) << m_stats.m_num_decisions << " "
<< std::setw(6) << m_stats.m_num_propagations << " "
- << std::setw(5) << m_aux_clauses.size() << "/" << bin_lemmas << " "
- << std::setw(5) << m_lemmas.size() << " "
- << std::setw(5) << m_stats.m_num_simplifications << " "
+ << std::setw(5) << (m_aux_clauses.size() + bin_clauses) << "/" << bin_clauses << " "
+ << std::setw(5) << m_lemmas.size(); if (bin_lemmas > 0) strm << "/" << bin_lemmas << " ";
+ strm << std::setw(5) << m_stats.m_num_simplifications << " "
<< std::setw(4) << m_stats.m_num_del_clauses << " "
<< std::setw(7) << mem_stat() << ")\n";