mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

remove the getter for solver statistics since we're getting the vals directly from the context

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-30 22:29:06 -07:00
parent 57d7e9fcf5
commit 82dee3032f
2 changed files with 0 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/util/statistics.cpp
View file

@ -81,21 +81,6 @@ struct str_lt {
typedef map<char const *, unsigned, str_hash_proc, str_eq_proc> key2val;
typedef map<char const *, double, str_hash_proc, str_eq_proc> key2dval;
double statistics::get_val(char const * key) const {
key2val m_u;
key2dval m_d;
mk_map(m_stats, m_u);
mk_map(m_d_stats, m_d);
unsigned val = 0;
double dval = 0.0;
if (m_u.find(key, val))
return static_cast<double>(val);
if (m_d.find(key, dval))
return dval;
return 0.0;
}
unsigned get_max_len(ptr_buffer<char> & keys) {
unsigned max = 0;
for (unsigned i = 0; i < static_cast<unsigned>(keys.size()); i++) {

1
src/util/statistics.h
View file

@ -40,7 +40,6 @@ public:
char const * get_key(unsigned idx) const;
unsigned get_uint_value(unsigned idx) const;
double get_double_value(unsigned idx) const;
double get_val(char const * key) const;
};
inline std::ostream& operator<<(std::ostream& out, statistics const& st) { return st.display(out); }