mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

count final checks

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-05 15:01:02 -08:00
parent 022a1fd3dd
commit 5f0ec936e4
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_solver.cpp
View file

@ -440,6 +440,7 @@ namespace euf {
} }
sat::check_result solver::check() { sat::check_result solver::check() {
++m_stats.m_final_checks;
TRACE("euf", s().display(tout);); TRACE("euf", s().display(tout););
bool give_up = false; bool give_up = false;
bool cont = false; bool cont = false;
@ -686,6 +687,7 @@ namespace euf {
for (auto* e : m_solvers) for (auto* e : m_solvers)
e->collect_statistics(st); e->collect_statistics(st);
st.update("euf ackerman", m_stats.m_ackerman); st.update("euf ackerman", m_stats.m_ackerman);
st.update("euf final check", m_stats.m_final_checks);
} }
enode* solver::copy(solver& dst_ctx, enode* src_n) { enode* solver::copy(solver& dst_ctx, enode* src_n) {

1
src/sat/smt/euf_solver.h
View file

@ -66,6 +66,7 @@ namespace euf {
// friend class sat::ba_solver; // friend class sat::ba_solver;
struct stats { struct stats {
unsigned m_ackerman; unsigned m_ackerman;
unsigned m_final_checks;
stats() { reset(); } stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
}; };