mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

throttle value smt -> sls

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-26 14:16:43 -08:00
parent d4100fc472
commit d3bf25ce85
5 changed files with 8 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sat_ddfw.cpp
View file

@ -430,7 +430,7 @@ namespace sat {
for (unsigned i = 0; i < num_vars(); ++i) for (unsigned i = 0; i < num_vars(); ++i)
m_model[i] = to_lbool(value(i)); m_model[i] = to_lbool(value(i));
save_priorities(); save_priorities();
if (m_plugin && !m_in_external_flip && m_restart_count == 0) if (m_plugin && !m_in_external_flip && m_restart_count == 0 && m_model_save_count++ % 10 == 0)
m_plugin->on_restart(); // import values if there are any updated ones. m_plugin->on_restart(); // import values if there are any updated ones.
if (m_plugin && !m_in_external_flip) if (m_plugin && !m_in_external_flip)
m_last_result = m_plugin->on_save_model(); m_last_result = m_plugin->on_save_model();

1
src/ast/sls/sat_ddfw.h
View file

@ -97,6 +97,7 @@ namespace sat {
uint64_t m_last_flips_for_shift = 0; uint64_t m_last_flips_for_shift = 0;
unsigned m_num_non_binary_clauses = 0; unsigned m_num_non_binary_clauses = 0;
unsigned m_restart_count = 0, m_reinit_count = 0; unsigned m_restart_count = 0, m_reinit_count = 0;
unsigned m_model_save_count = 0;
uint64_t m_restart_next = 0, m_reinit_next = 0; uint64_t m_restart_next = 0, m_reinit_next = 0;
uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0; uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0;
unsigned m_logs = 0; unsigned m_logs = 0;

4
src/ast/sls/sls_arith_base.cpp
View file

@ -1571,8 +1571,8 @@ namespace sls {
todo.push_back(op.m_arg1); todo.push_back(op.m_arg1);
todo.push_back(op.m_arg2); todo.push_back(op.m_arg2);
} }
if (m_vars[u].is_if_op()) { auto const& ui = m_vars[u];
auto const& ui = m_vars[u]; if (ui.is_if_op()) {
expr* c = nullptr, * th = nullptr, * el = nullptr; expr* c = nullptr, * th = nullptr, * el = nullptr;
VERIFY(m.is_ite(ui.m_expr, c, th, el)); VERIFY(m.is_ite(ui.m_expr, c, th, el));
todo.push_back(mk_var(th)); todo.push_back(mk_var(th));

6
src/ast/sls/sls_smt_plugin.cpp
View file

@ -212,7 +212,7 @@ namespace sls {
m_sat_phase[v] = ctx.get_best_phase(v); m_sat_phase[v] = ctx.get_best_phase(v);
} }
bool smt_plugin::export_to_sls() { bool smt_plugin::export_to_sls() {
bool updated = false; bool updated = false;
if (m_has_units) { if (m_has_units) {
std::lock_guard<std::mutex> lock(m_mutex); std::lock_guard<std::mutex> lock(m_mutex);
@ -274,7 +274,7 @@ namespace sls {
void smt_plugin::smt_values_to_sls() { void smt_plugin::smt_values_to_sls() {
if (ctx.parallel_mode()) { if (true || ctx.parallel_mode()) {
std::scoped_lock lock(m_mutex); std::scoped_lock lock(m_mutex);
m_sync_var_values.reset(); m_sync_var_values.reset();
for (auto const& [t, t_sync] : m_smt2sync_uninterp) { for (auto const& [t, t_sync] : m_smt2sync_uninterp) {
@ -310,9 +310,11 @@ namespace sls {
void smt_plugin::sls_phase_to_smt() { void smt_plugin::sls_phase_to_smt() {
if (!m_has_new_sls_phase) if (!m_has_new_sls_phase)
return; return;
#if 0
IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase. unsat size: " << m_min_unsat_size << "\n"); IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase. unsat size: " << m_min_unsat_size << "\n");
for (auto v : m_shared_bool_vars) for (auto v : m_shared_bool_vars)
ctx.force_phase(sat::literal(v, !m_sls_phase[v])); ctx.force_phase(sat::literal(v, !m_sls_phase[v]));
#endif
m_has_new_sls_phase = false; m_has_new_sls_phase = false;
} }

5
src/sat/smt/sls_solver.cpp
View file

@ -105,11 +105,6 @@ namespace sls {
m_smt_plugin->add_unit(lit); m_smt_plugin->add_unit(lit);
} }
} }
#if 0
if (ctx.has_new_best_phase())
m_smt_plugin->import_phase_from_smt();
#endif
m_smt_plugin->import_from_sls(); m_smt_plugin->import_from_sls();
} }