mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fallback stats

Browse source
This commit is contained in:
Jakob Rath 2022-08-04 08:51:24 +02:00
parent b9588af07a
commit 014fe4e3fd
2 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/solver.cpp
View file

@ -554,6 +554,7 @@ namespace polysat {
m_justification[v] = justification::unassigned();
if (!is_valid) {
LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
++m_stats.m_num_viable_fallback;
// Try to find a valid replacement value
switch (m_viable_fallback.find_viable(v, val)) {
case dd::find_t::singleton:
@ -1194,12 +1195,13 @@ namespace polysat {
}
void solver::collect_statistics(statistics& st) const {
st.update("polysat iterations", m_stats.m_num_iterations);
st.update("polysat decisions", m_stats.m_num_decisions);
st.update("polysat conflicts", m_stats.m_num_conflicts);
st.update("polysat bailouts", m_stats.m_num_bailouts);
st.update("polysat propagations", m_stats.m_num_propagations);
st.update("polysat restarts", m_stats.m_num_restarts);
st.update("polysat iterations", m_stats.m_num_iterations);
st.update("polysat decisions", m_stats.m_num_decisions);
st.update("polysat conflicts", m_stats.m_num_conflicts);
st.update("polysat bailouts", m_stats.m_num_bailouts);
st.update("polysat propagations", m_stats.m_num_propagations);
st.update("polysat restarts", m_stats.m_num_restarts);
st.update("polysat viable fallback", m_stats.m_num_viable_fallback);
}
bool solver::invariant() {

1
src/math/polysat/solver.h
View file

@ -54,6 +54,7 @@ namespace polysat {
unsigned m_num_conflicts;
unsigned m_num_bailouts;
unsigned m_num_restarts;
unsigned m_num_viable_fallback; ///< how often did we query the univariate solver
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};