mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Sort cube candidates by activity with tie shuffling

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-12 17:26:55 +00:00 • committed by GitHub
parent af5bbb4566
commit 502309f246
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 22 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/smt/smt_solver.cpp
View file

@ -453,10 +453,11 @@ namespace {
expr_mark selected_vars;
for (expr* v : vars)
selected_vars.mark(v);
expr_ref_vector candidates(m);
expr_ref result(m);
double score = 0.0;
unsigned n = 0;
struct candidate {
expr* e;
double score;
};
vector<candidate> candidates;
ctx.pop_to_search_level();
for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
@ -467,22 +468,28 @@ namespace {
continue;
if (!vars.empty() && !selected_vars.is_marked(e))
continue;
candidates.push_back(e);
double new_score = ctx.get_activity(v);
// Match smt_parallel: cube split tie-breaking is independent
// of the per-worker SMT search seed.
if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) {
score = new_score;
result = e;
}
candidates.push_back({ e, ctx.get_activity(v) });
}
std::stable_sort(candidates.begin(), candidates.end(),
[](candidate const& a, candidate const& b) {
return a.score > b.score;
});
for (unsigned i = 0, j = 0; i < candidates.size(); i = j) {
j = i + 1;
while (j < candidates.size() && candidates[i].score == candidates[j].score)
++j;
if (j > i + 1)
shuffle(j - i, candidates.data() + i, m_rand);
}
vars.reset();
vars.append(candidates);
for (auto const& c : candidates)
vars.push_back(c.e);
expr_ref_vector lits(m);
if (result)
lits.push_back(result);
if (!candidates.empty())
lits.push_back(candidates[0].e);
return lits;
}