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

collect-statistics additions

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-06-03 20:45:42 +01:00
parent b54ef3623b
commit 626b9160bf
1 changed files with 17 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/tactic/core/collect_statistics_tactic.cpp
View file

@ -133,8 +133,14 @@ protected:
params_ref prms; params_ref prms;
prms.set_bool("pp.single_line", true); prms.set_bool("pp.single_line", true);
std::stringstream ss; std::stringstream ss;
ss << mk_ismt2_pp(s, m, prms); ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")";
m_stats[ss.str().c_str()]++; m_stats[ss.str()]++;
if (s->get_info()->get_num_parameters() > 0) {
std::stringstream ssname;
ssname << "(declare-sort (_ " << s->get_name() << " *))";
m_stats[ssname.str()]++;
}
} }
} }
@ -160,8 +166,16 @@ protected:
prms.set_bool("pp.single_line", true); prms.set_bool("pp.single_line", true);
std::stringstream ss; std::stringstream ss;
ss << mk_ismt2_pp(f, m, prms); ss << mk_ismt2_pp(f, m, prms);
m_stats[ss.str().c_str()]++; m_stats[ss.str()]++;
std::stringstream ssfname;
if (f->get_num_parameters() > 0)
ssfname << "(declare-fun (_ " << f->get_name() << " *) *)";
else
ssfname << "(declare-fun " << f->get_name() << " *)";
m_stats[ssfname.str()]++;
} }
m_stats["function-applications"]++; m_stats["function-applications"]++;
} }
}; };