mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 14:26:10 +00:00
Code Activity

refactor phase update

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-11 15:28:48 -07:00
parent e06ca1489e
commit 5aa06b6333
2 changed files with 26 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

72
src/sat/sat_solver.cpp
View file

@ -657,11 +657,16 @@ namespace sat {
if (l.var() >= num_vars()) if (l.var() >= num_vars())
return; return;
bool value = !l.sign(); bool value = !l.sign();
if (m_phase[l.var()] != value) set_phase(l.var(), value);
m_phase_birthdate[l.var()] = m_stats.m_conflicts;
if (m_best_phase[l.var()] != value) if (m_best_phase[l.var()] != value)
m_best_phase_birthdate[l.var()] = m_stats.m_conflicts; m_best_phase_birthdate[l.var()] = m_stats.m_conflicts;
m_best_phase[l.var()] = m_phase[l.var()] = value; m_best_phase[l.var()] = value;
}
void solver::set_phase(bool_var v, bool value) {
if (m_phase[v] != value)
m_phase_birthdate[v] = m_stats.m_conflicts;
m_phase[v] = value;
} }
struct solver::cmp_activity { struct solver::cmp_activity {
@ -915,9 +920,7 @@ namespace sat {
m_assignment[(~l).index()] = l_false; m_assignment[(~l).index()] = l_false;
bool_var v = l.var(); bool_var v = l.var();
m_justification[v] = j; m_justification[v] = j;
if (m_phase[v] != !l.sign()) set_phase(v, !l.sign());
m_phase_birthdate[v] = m_stats.m_conflicts;
m_phase[v] = !l.sign();
m_assigned_since_gc[v] = true; m_assigned_since_gc[v] = true;
m_trail.push_back(l); m_trail.push_back(l);
@ -2197,11 +2200,9 @@ namespace sat {
if (!was_eliminated(v)) { if (!was_eliminated(v)) {
m_model[v] = value(v); m_model[v] = value(v);
bool is_true = value(v) == l_true; bool is_true = value(v) == l_true;
if (m_phase[v] != is_true) set_phase(v, is_true);
m_phase_birthdate[v] = m_stats.m_conflicts;
if (m_best_phase[v] != is_true) if (m_best_phase[v] != is_true)
m_best_phase_birthdate[v] = m_stats.m_conflicts; m_best_phase_birthdate[v] = m_stats.m_conflicts;
m_phase[v] = is_true;
m_best_phase[v] = is_true; m_best_phase[v] = is_true;
} }
} }
@ -2972,9 +2973,7 @@ namespace sat {
bool_var v = m_trail[i].var(); bool_var v = m_trail[i].var();
TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";); TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";);
bool value = m_rand() % 2 == 0; bool value = m_rand() % 2 == 0;
if (m_phase[v] != value) set_phase(v, value);
m_phase_birthdate[v] = m_stats.m_conflicts;
m_phase[v] = value;
} }
if (is_sat_phase() && head >= m_best_phase_size) { if (is_sat_phase() && head >= m_best_phase_size) {
m_best_phase_size = head; m_best_phase_size = head;
@ -3032,18 +3031,12 @@ namespace sat {
void solver::do_rephase() { void solver::do_rephase() {
switch (m_config.m_phase) { switch (m_config.m_phase) {
case PS_ALWAYS_TRUE: case PS_ALWAYS_TRUE:
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i)
if (!m_phase[i]) set_phase(i, true);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = true;
}
break; break;
case PS_ALWAYS_FALSE: case PS_ALWAYS_FALSE:
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i)
if (m_phase[i]) set_phase(i, false);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = false;
}
break; break;
case PS_FROZEN: case PS_FROZEN:
break; break;
@ -3052,23 +3045,16 @@ namespace sat {
case 0: case 0:
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i) {
bool value = (m_rand() % 2) == 0; bool value = (m_rand() % 2) == 0;
if (m_phase[i] != value) set_phase(i, value);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = value;
} }
break; break;
case 1: case 1:
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i)
if (m_phase[i]) set_phase(i, false);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = false;
}
break; break;
case 2: case 2:
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i)
m_phase_birthdate[i] = m_stats.m_conflicts; set_phase(i, !m_phase[i]);
m_phase[i] = !m_phase[i];
}
break; break;
default: default:
break; break;
@ -3076,29 +3062,21 @@ namespace sat {
break; break;
case PS_SAT_CACHING: case PS_SAT_CACHING:
if (m_search_state == s_sat) if (m_search_state == s_sat)
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i)
if (m_phase[i] != m_best_phase[i]) set_phase(i, m_best_phase[i]);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = m_best_phase[i];
}
break; break;
case PS_RANDOM: case PS_RANDOM:
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i) {
bool value = (m_rand() % 2) == 0; bool value = (m_rand() % 2) == 0;
if (m_phase[i] != value) set_phase(i, value);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = value;
} }
break; break;
case PS_LOCAL_SEARCH: case PS_LOCAL_SEARCH:
if (m_search_state == s_sat) { if (m_search_state == s_sat) {
if (m_rand() % 2 == 0) if (m_rand() % 2 == 0)
bounded_local_search(); bounded_local_search();
for (unsigned i = 0; i < m_phase.size(); ++i) { for (unsigned i = 0; i < m_phase.size(); ++i)
if (m_phase[i] != m_best_phase[i]) set_phase(i, m_best_phase[i]);
m_phase_birthdate[i] = m_stats.m_conflicts;
m_phase[i] = m_best_phase[i];
}
} }
break; break;

1
src/sat/sat_solver.h
View file

@ -376,6 +376,7 @@ namespace sat {
void set_eliminated(bool_var v, bool f) override; void set_eliminated(bool_var v, bool f) override;
bool was_eliminated(literal l) const { return was_eliminated(l.var()); } bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
void set_phase(literal l) override; void set_phase(literal l) override;
void set_phase(bool_var v, bool value);
bool get_phase(bool_var b) { return m_phase.get(b, false); } bool get_phase(bool_var b) { return m_phase.get(b, false); }
bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); } 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_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }