From caa34b793715cc666addbfda5d51699e63b00979 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 3 Jul 2026 08:03:44 -0700 Subject: [PATCH] smt: skip m_watches probe for unwatched literals in relevancy propagator Add a monotonic over-approximating membership filter (uint_set m_is_watched[2]) parallel to m_watches in the relevancy propagator so get_watches() can early-return for the common unwatched-literal case, skipping the obj_map pointer-hash probe (a likely cache miss) at the assign_eh hot path. The filter is monotonic: ids are inserted when a watch list is created and never cleared on erase/pop, so it stays a superset of the live watch keys. It can therefore only produce false positives (which fall through to the normal m_watches.find(), still correct) and never false negatives, so observable solver behavior is unchanged. Correctness verified: identical results across the 60-file ABVFP (SV-COMP UltimateAutomizer) corpus with model_validate=true. Note on impact: this is a safe, low-risk micro-optimization. On the available benchmarks assign_eh is only ~1% of whole-program self-time (measured by sampling), so the wall-time gain is small (within noise, ~0-1%); the change is a cache/allocation win at the named hot path rather than a large speedup. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/smt_relevancy.cpp | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 3f24a4e11c..fcaf604558 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -141,6 +141,13 @@ namespace smt { typedef list relevancy_ehs; obj_map m_relevant_ehs; obj_map m_watches[2]; + // Over-approximating membership filter for m_watches: contains a superset + // of the expr ids that have (or ever had) a watch list for the given phase. + // It is monotonic (never cleared on erase/pop), so it can only yield false + // positives, never false negatives. This lets get_watches() skip the + // obj_map pointer-hash probe for the common unwatched-literal case at the + // assign_eh hotspot. + uint_set m_is_watched[2]; struct eh_trail { enum class kind { POS_WATCH, NEG_WATCH, HANDLER }; kind m_kind; @@ -185,17 +192,23 @@ namespace smt { } relevancy_ehs * get_watches(expr * n, bool val) { + unsigned idx = val ? 1 : 0; + if (!m_is_watched[idx].contains(n->get_id())) + return nullptr; relevancy_ehs * r = nullptr; - m_watches[val ? 1 : 0].find(n, r); - SASSERT(m_watches[val ? 1 : 0].contains(n) || r == 0); + m_watches[idx].find(n, r); + SASSERT(m_watches[idx].contains(n) || r == 0); return r; } void set_watches(expr * n, bool val, relevancy_ehs * ehs) { + unsigned idx = val ? 1 : 0; if (ehs == nullptr) - m_watches[val ? 1 : 0].erase(n); - else - m_watches[val ? 1 : 0].insert(n, ehs); + m_watches[idx].erase(n); + else { + m_watches[idx].insert(n, ehs); + m_is_watched[idx].insert(n->get_id()); + } } void push_trail(eh_trail const & t) {