From 014fe4e3fde9e49c78a98ab4f4b8c49a7c7cc0be Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 4 Aug 2022 08:51:24 +0200 Subject: [PATCH] fallback stats --- src/math/polysat/solver.cpp | 14 ++++++++------ src/math/polysat/solver.h | 1 + 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index c65da431e..6dada445b 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -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() { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index da3921f1d..2b4c7bd18 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -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(); } };