mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 02:25:32 +00:00
Code Activity

display similar to sat solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-13 19:48:04 -07:00
parent 796e2fd9eb
commit 73ce5c5fc8
1 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_context.cpp
View file

@ -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";