mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

restore use of value_hash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-14 10:46:31 -07:00
parent f136d46fb4
commit 54cce7b10b
2 changed files with 16 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -432,19 +432,26 @@ namespace sat {
}
#endif
m_num_models.reserve(m_unsat.size() + 1);
if (m_unsat.size() < m_min_sz)
m_models.reset();
m_min_sz = m_unsat.size();
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)
#if 0
m_num_models.reserve(m_min_sz + 1);
unsigned nm = m_num_models[m_min_sz]++;
if (nm >= 10) {
if (nm >= 200)
m_num_models[m_min_sz] = 10, m_restart_next = m_flips;
if (nm % 1 == 0) {
for (unsigned v = 0; v < num_vars(); ++v)
bias(v) += value(v) ? 1 : -1;
}
return;
}
#endif
unsigned h = value_hash();
unsigned occs = 0;

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

@ -137,8 +137,10 @@ namespace sls {
while (slit != flit);
// flip the last literal on the replay stack
IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
ctx.add_clause(lits);
ctx.flip(flit.var());
m_replay_stack.back().neg();
}
void euf_plugin::replay() {
@ -342,7 +344,7 @@ namespace sls {
m_values.insert(t);
}
}
//validate_model();
// validate_model();
return true;
}
@ -483,7 +485,7 @@ namespace sls {
}
void euf_plugin::collect_statistics(statistics& st) const {
st.update("sls.euf-conflict", m_stats.m_num_conflicts);
st.update("sls-euf-conflict", m_stats.m_num_conflicts);
}
void euf_plugin::reset_statistics() {