mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

smt: skip m_watches probe for unwatched literals in relevancy propagator

Browse source 
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<expr*, relevancy_ehs*> 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>
This commit is contained in:
Lev Nachmanson 2026-07-03 08:03:44 -07:00
parent f15584cdae
commit caa34b7937
1 changed files with 18 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/smt/smt_relevancy.cpp
View file

@ -141,6 +141,13 @@ namespace smt {
typedef list<relevancy_eh *> relevancy_ehs;
obj_map<expr, relevancy_ehs *> m_relevant_ehs;
obj_map<expr, relevancy_ehs *> 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) {