mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

neatify statistics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-14 16:45:04 -08:00
parent ed7cac8cc0
commit f238460597
1 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/sat/sat_solver.cpp
View file

@ -4387,24 +4387,24 @@ namespace sat {
}
void stats::collect_statistics(statistics & st) const {
st.update("mk bool var", m_mk_var);
st.update("mk binary clause", m_mk_bin_clause);
st.update("mk ternary clause", m_mk_ter_clause);
st.update("mk clause", m_mk_clause);
st.update("gc clause", m_gc_clause);
st.update("del clause", m_del_clause);
st.update("conflicts", m_conflict);
st.update("propagations", m_propagate);
st.update("decisions", m_decision);
st.update("binary propagations", m_bin_propagate);
st.update("ternary propagations", m_ter_propagate);
st.update("restarts", m_restart);
st.update("minimized lits", m_minimized_lits);
st.update("dyn subsumption resolution", m_dyn_sub_res);
st.update("blocked correction sets", m_blocked_corr_sets);
st.update("units", m_units);
st.update("elim bool vars res", m_elim_var_res);
st.update("elim bool vars bdd", m_elim_var_bdd);
st.update("sat mk clause 2ary", m_mk_bin_clause);
st.update("sat mk clause 3ary", m_mk_ter_clause);
st.update("sat mk clause nary", m_mk_clause);
st.update("sat mk var", m_mk_var);
st.update("sat gc clause", m_gc_clause);
st.update("sat del clause", m_del_clause);
st.update("sat conflicts", m_conflict);
st.update("sat decisions", m_decision);
st.update("sat propagations 2ary", m_bin_propagate);
st.update("sat propagations 3ary", m_ter_propagate);
st.update("sat propagations nary", m_propagate);
st.update("sat restarts", m_restart);
st.update("sat minimized lits", m_minimized_lits);
st.update("sat subs resolution dyn", m_dyn_sub_res);
st.update("sat blocked correction sets", m_blocked_corr_sets);
st.update("sat units", m_units);
st.update("sat elim bool vars res", m_elim_var_res);
st.update("sat elim bool vars bdd", m_elim_var_bdd);
}
void stats::reset() {