mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

throttle save model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-12 19:09:25 -07:00
parent 2bd335db81
commit 9b54254fa2
2 changed files with 16 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -415,7 +415,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) if (m_plugin && m_unsat.empty())
m_plugin->on_save_model(); m_plugin->on_save_model();
} }
@ -431,15 +431,19 @@ namespace sat {
verbose_stream() << "unsat " << m_clauses[m_unsat[0]] << "\n"; verbose_stream() << "unsat " << m_clauses[m_unsat[0]] << "\n";
} }
#endif #endif
if (m_unsat.size() < m_min_sz) {
m_models.reset(); m_num_models.reserve(m_unsat.size() + 1);
// skip saving the first model. if (m_unsat.size() < m_min_sz)
for (unsigned v = 0; v < num_vars(); ++v) { m_models.reset();
int& b = bias(v);
if (abs(b) > 3) { m_min_sz = m_unsat.size();
b = b > 0 ? 3 : -3; m_num_models.reserve(m_min_sz + 1);
} m_num_models[m_min_sz]++;
}
if (m_num_models[m_min_sz] >= 10) {
if (m_num_models[m_min_sz] >= 200)
m_num_models[m_min_sz] = 10, m_restart_next = m_flips;
return;
} }
unsigned h = value_hash(); unsigned h = value_hash();
@ -456,7 +460,7 @@ namespace sat {
m_restart_next = m_flips; m_restart_next = m_flips;
m_models.erase(h); m_models.erase(h);
} }
m_min_sz = m_unsat.size();
} }
unsigned ddfw::value_hash() const { unsigned ddfw::value_hash() const {

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

@ -103,6 +103,7 @@ namespace sat {
unsigned m_min_sz = 0, m_steps_since_progress = 0; unsigned m_min_sz = 0, m_steps_since_progress = 0;
u_map<unsigned> m_models; u_map<unsigned> m_models;
stopwatch m_stopwatch; stopwatch m_stopwatch;
unsigned_vector m_num_models;
scoped_ptr<local_search_plugin> m_plugin = nullptr; scoped_ptr<local_search_plugin> m_plugin = nullptr;
std::function<bool(void)> m_parallel_sync; std::function<bool(void)> m_parallel_sync;