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

refactor

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-11 15:40:38 -07:00
parent 5aa06b6333
commit 49d725f477
4 changed files with 11 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/sat/sat_solver.cpp
View file

@ -658,9 +658,7 @@ namespace sat {
return;
bool value = !l.sign();
set_phase(l.var(), value);
if (m_best_phase[l.var()] != value)
m_best_phase_birthdate[l.var()] = m_stats.m_conflicts;
m_best_phase[l.var()] = value;
set_best_phase(l.var(), value);
}
void solver::set_phase(bool_var v, bool value) {
@ -669,6 +667,12 @@ namespace sat {
m_phase[v] = value;
}
void solver::set_best_phase(bool_var v, bool value) {
if (m_best_phase[v] != value)
m_best_phase_birthdate[v] = m_stats.m_conflicts;
m_best_phase[v] = value;
}
struct solver::cmp_activity {
solver& s;
cmp_activity(solver& s):s(s) {}
@ -1404,9 +1408,7 @@ namespace sat {
if (mdl.size() == m_best_phase.size()) {
for (unsigned i = 0; i < m_best_phase.size(); ++i) {
bool is_true = l_true == mdl[i];
if (m_best_phase[i] != is_true)
m_best_phase_birthdate[i] = m_stats.m_conflicts;
m_best_phase[i] = is_true;
set_best_phase(i, is_true);
}
if (r == l_true) {
@ -2201,9 +2203,7 @@ namespace sat {
m_model[v] = value(v);
bool is_true = value(v) == l_true;
set_phase(v, is_true);
if (m_best_phase[v] != is_true)
m_best_phase_birthdate[v] = m_stats.m_conflicts;
m_best_phase[v] = is_true;
set_best_phase(v, is_true);
}
}
TRACE(sat_mc_bug, m_mc.display(tout););
@ -2980,9 +2980,7 @@ namespace sat {
IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n");
for (unsigned i = 0; i < head; ++i) {
bool_var v = m_trail[i].var();
if (m_best_phase[v] != m_phase[v])
m_best_phase_birthdate[v] = m_stats.m_conflicts;
m_best_phase[v] = m_phase[v];
set_best_phase(v, m_phase[v]);
}
set_has_new_best_phase(true);
}

1
src/sat/sat_solver.h
View file

@ -377,6 +377,7 @@ namespace sat {
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
void set_phase(literal l) override;
void set_phase(bool_var v, bool value);
void set_best_phase(bool_var v, bool value);
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); }
uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }

8
src/smt/smt_kernel.cpp
View file

@ -288,14 +288,6 @@ namespace smt {
m_imp->m_kernel.get_fparams().m_preprocess = f;
}
void kernel::reset_aux_statistics() {
m_imp->m_kernel.m_aux_stats.reset();
}
void kernel::add_aux_statistics(::statistics const& st) {
m_imp->m_kernel.m_aux_stats.copy(st);
}
context & kernel::get_context() {
return m_imp->m_kernel;
}

4
src/smt/smt_kernel.h
View file

@ -304,10 +304,6 @@ namespace smt {
void set_preprocess(bool f);
void reset_aux_statistics();
void add_aux_statistics(::statistics const& st);
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause);
/**