mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Update smt_context_pp.cpp

Browse source 
print units in statistics
This commit is contained in:
Nikolaj Bjorner 2023-02-28 17:38:36 -08:00
parent 5974a2dc58
commit 76aad689c6
1 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_context_pp.cpp
View file

@ -704,14 +704,20 @@ namespace smt {
for (clause* cp : m_lemmas)
if (cp->get_num_literals() == 2)
++bin_lemmas;
auto num_units = [&]() {
if (m_scopes.empty())
return m_assigned_literals.size();
else
return m_scopes[0].m_assigned_literals_lim;
};
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_clauses) << "/" << bin_clauses << " "
<< std::setw(5) << m_lemmas.size(); if (bin_lemmas > 0) strm << "/" << bin_lemmas << " ";
<< std::setw(5) << (m_aux_clauses.size() + bin_clauses) << "/" << bin_clauses << "/" << num_units()
<< std::setw(7) << 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";
@ -739,8 +745,8 @@ namespace smt {
m_last_position_log = m_stats.m_num_restarts;
// restarts decisions clauses simplifications memory
// conflicts propagations lemmas deletions
int adjust[9] = { -3, -3, -3, -3, -3, -3, -4, -4, -1 };
char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin ", ":lemmas ", ":simplify ", ":deletions", ":memory" };
int adjust[9] = { -3, -3, -3, -3, -3, -4, -4, -4, -1 };
char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin/units ", ":lemmas ", ":simplify ", ":deletions", ":memory" };
std::stringstream l1, l2;
l1 << "(smt.stats ";