mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 18:43:45 +00:00
Code Activity

move statistics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-15 20:09:19 -07:00
parent d137f25b65
commit 7dea14f732
3 changed files with 36 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/seq/seq_nielsen.cpp
View file

@ -27,6 +27,7 @@ Author:
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/th_rewriter.h"
#include "util/hashtable.h"
#include "util/statistics.h"
#include <algorithm>
#include <cstdlib>
#include <sstream>
@ -2142,7 +2143,7 @@ namespace seq {
++m_stats.m_num_unknown;
return search_result::unknown;
}
catch(const std::exception& ex) {
catch(const std::exception&) {
#ifdef Z3DEBUG
std::string dot = to_dot();
#endif
@ -4451,4 +4452,35 @@ namespace seq {
return true;
}
// -----------------------------------------------------------------------
// Statistics collection
// -----------------------------------------------------------------------
void nielsen_graph::collect_statistics(::statistics& st) const {
st.update("nseq solve calls", m_stats.m_num_solve_calls);
st.update("nseq dfs nodes", m_stats.m_num_dfs_nodes);
st.update("nseq sat", m_stats.m_num_sat);
st.update("nseq unsat", m_stats.m_num_unsat);
st.update("nseq unknown", m_stats.m_num_unknown);
st.update("nseq simplify clash", m_stats.m_num_simplify_conflict);
st.update("nseq extensions", m_stats.m_num_extensions);
st.update("nseq fresh vars", m_stats.m_num_fresh_vars);
st.update("nseq max depth", m_stats.m_max_depth);
// modifier breakdown
st.update("nseq mod det", m_stats.m_mod_det);
st.update("nseq mod power epsilon", m_stats.m_mod_power_epsilon);
st.update("nseq mod num cmp", m_stats.m_mod_num_cmp);
st.update("nseq mod const num unwind", m_stats.m_mod_const_num_unwinding);
st.update("nseq mod eq split", m_stats.m_mod_eq_split);
st.update("nseq mod star intr", m_stats.m_mod_star_intr);
st.update("nseq mod gpower intr", m_stats.m_mod_gpower_intr);
st.update("nseq mod const nielsen", m_stats.m_mod_const_nielsen);
st.update("nseq mod regex char", m_stats.m_mod_regex_char_split);
st.update("nseq mod regex var", m_stats.m_mod_regex_var_split);
st.update("nseq mod power split", m_stats.m_mod_power_split);
st.update("nseq mod var nielsen", m_stats.m_mod_var_nielsen);
st.update("nseq mod var num unwind", m_stats.m_mod_var_num_unwinding);
}
}

1
src/smt/seq/seq_nielsen.h
View file

@ -879,6 +879,7 @@ namespace seq {
// accumulated search statistics
nielsen_stats const& stats() const { return m_stats; }
void reset_stats() { m_stats.reset(); }
void collect_statistics(::statistics& st) const;
// generate arithmetic length constraints from the root node's string
// equalities and regex memberships. For each non-trivial equation lhs = rhs,

30
src/smt/theory_nseq.cpp
View file

@ -522,34 +522,8 @@ namespace smt {
st.update("nseq conflicts", m_num_conflicts);
st.update("nseq final checks", m_num_final_checks);
st.update("nseq length axioms", m_num_length_axioms);
// Nielsen graph search metrics
auto const& ns = m_nielsen.stats();
st.update("nseq solve calls", ns.m_num_solve_calls);
st.update("nseq dfs nodes", ns.m_num_dfs_nodes);
st.update("nseq sat", ns.m_num_sat);
st.update("nseq unsat", ns.m_num_unsat);
st.update("nseq unknown", ns.m_num_unknown);
st.update("nseq simplify clash", ns.m_num_simplify_conflict);
st.update("nseq extensions", ns.m_num_extensions);
st.update("nseq fresh vars", ns.m_num_fresh_vars);
st.update("nseq max depth", ns.m_max_depth);
// modifier breakdown
st.update("nseq mod det", ns.m_mod_det);
st.update("nseq mod power epsilon", ns.m_mod_power_epsilon);
st.update("nseq mod num cmp", ns.m_mod_num_cmp);
st.update("nseq mod const num unwind", ns.m_mod_const_num_unwinding);
st.update("nseq mod eq split", ns.m_mod_eq_split);
st.update("nseq mod star intr", ns.m_mod_star_intr);
st.update("nseq mod gpower intr", ns.m_mod_gpower_intr);
st.update("nseq mod const nielsen", ns.m_mod_const_nielsen);
st.update("nseq mod regex char", ns.m_mod_regex_char_split);
st.update("nseq mod regex var", ns.m_mod_regex_var_split);
st.update("nseq mod power split", ns.m_mod_power_split);
st.update("nseq mod var nielsen", ns.m_mod_var_nielsen);
st.update("nseq mod var num unwind", ns.m_mod_var_num_unwinding);
st.update("nseq ho unfolds", m_num_ho_unfolds);
st.update("nseq ho unfolds", m_num_ho_unfolds);
m_nielsen.collect_statistics(st);
}
void theory_nseq::display(std::ostream& out) const {