mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 06:16:09 +00:00
Code Activity

sat solver uses actual phase birthdate instead of preferred phase birthdate for bb ranking

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-24 22:59:34 -07:00
parent 35fd50238b
commit 78c06bcc50
2 changed files with 1 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_solver.cpp
View file

@ -1744,13 +1744,6 @@ namespace sat {
}
}
uint64_t solver::get_preferred_phase_birthdate(bool_var v) const {
bool use_best =
m_config.m_phase == PS_FROZEN ||
((m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH) && m_search_state == s_sat);
return use_best ? m_best_phase_birthdate[v] : m_phase_birthdate[v];
}
void solver::get_backbone_candidates(literal_vector& lits, unsigned max_num) {
struct candidate {
literal lit;
@ -1762,7 +1755,7 @@ namespace sat {
if (value(v) != l_undef || was_eliminated(v))
continue;
bool is_pos = guess(v);
cands.push_back({ literal(v, !is_pos), now - get_preferred_phase_birthdate(v) });
cands.push_back({ literal(v, !is_pos), now - get_phase_birthdate(v) });
}
std::stable_sort(cands.begin(), cands.end(),
[](candidate const& a, candidate const& b) { return a.age > b.age; });

1
src/sat/sat_solver.h
View file

@ -382,7 +382,6 @@ namespace sat {
bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); }
uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }
uint64_t get_best_phase_birthdate(bool_var b) const { return m_best_phase_birthdate.get(b, 0); }
uint64_t get_preferred_phase_birthdate(bool_var b) const;
void set_has_new_best_phase(bool b) { m_new_best_phase = b; }
bool has_new_best_phase() const { return m_new_best_phase; }
void move_to_front(bool_var b);