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

update restart next

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-22 21:40:35 -08:00
parent ec3915218d
commit beb9d2e553
3 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -232,7 +232,7 @@ namespace sat {
m_reinit_next = m_config.m_reinit_base; m_reinit_next = m_config.m_reinit_base;
m_restart_count = 0; m_restart_count = 0;
m_restart_next = m_config.m_restart_base*2; m_restart_next = m_config.m_restart_base;
m_min_sz = m_clauses.size(); m_min_sz = m_clauses.size();
m_flips = 0; m_flips = 0;

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

@ -211,7 +211,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);
@ -275,7 +275,7 @@ 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_VERBOSE(2, verbose_stream() << "SLS -> SMT phase " << 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]));
m_has_new_sls_phase = false; m_has_new_sls_phase = false;

1
src/smt/theory_sls.cpp
View file

@ -243,7 +243,6 @@ namespace smt {
verbose_stream() << "\n"; verbose_stream() << "\n";
} }
#endif #endif
for (auto const& cl : m_shared_clauses) for (auto const& cl : m_shared_clauses)
if (all_of(cl, [this](sat::literal lit) { return ctx.get_assignment(lit) != l_true; })) if (all_of(cl, [this](sat::literal lit) { return ctx.get_assignment(lit) != l_true; }))
return false; return false;