mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

fixes to hybrid mode

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-12 16:59:27 -08:00
parent 9770c00592
commit 943d881340
3 changed files with 23 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2479,6 +2479,20 @@ namespace sls {
if (get_bool_value(a) != ctx.is_true(v))
ctx.flip(v);
}
#if 0
for (auto idx : ctx.unsat()) {
auto const& cl = ctx.get_clause(idx);
verbose_stream() << "clause " << cl << "\n";
for (auto lit : cl) {
auto a = ctx.atom(lit.var());
if (a)
verbose_stream() << lit << " " << mk_bounded_pp(a, m) << " " << get_bool_value(a) << " " << ctx.is_true(lit) << "\n";
else
verbose_stream() << lit << " " << ctx.is_true(lit) << "\n";
}
}
#endif
}
template<typename num_t>
@ -2938,24 +2952,22 @@ namespace sls {
rescore();
m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
TRACE("arith", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";);
IF_VERBOSE(1, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
IF_VERBOSE(3, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
TRACE("arith", display(tout));
bool loop_again = true;
while (m.inc() && m_stats.m_moves < m_config.max_moves) {
loop_again = false;
m_stats.m_moves++;
check_restart();
auto t = get_candidate_unsat();
if (!t)
if (!t)
break;
auto& vars = get_fixable_exprs(t);
if (vars.empty())
return;
break;
if (ctx.rand(2047) < m_config.wp && apply_move(t, vars, arith_move_type::random_inc_dec))
continue;
@ -2965,9 +2977,8 @@ namespace sls {
if (apply_move(t, vars, arith_move_type::random_update))
recalibrate_weights();
loop_again = true;
}
if (loop_again)
if (m_stats.m_moves >= m_config.max_moves)
m_config.max_moves_base += 100;
finalize_bool_assignment();
}

1
src/ast/sls/sls_context.cpp
View file

@ -123,7 +123,6 @@ namespace sls {
propagate_boolean_assignment();
// verbose_stream() << "propagate " << unsat().size() << " " << m_new_constraint << "\n";
if (m_new_constraint || !unsat().empty())

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

@ -55,6 +55,7 @@ namespace sls {
m_ddfw = alloc(sat::ddfw);
m_ddfw->set_plugin(this);
m_ddfw->updt_params(ctx.get_params());
m_context.updt_params(ctx.get_params());
for (auto const& clause : clauses) {
m_ddfw->add(clause.size(), clause.data());
@ -72,7 +73,7 @@ namespace sls {
}
for (auto fml : fmls)
m_context.add_constraint(m_smt2sls_tr(fml));
m_context.add_input_assertion(m_smt2sls_tr(fml));
for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
expr* e = ctx.bool_var2expr(v);
@ -99,7 +100,7 @@ namespace sls {
if (!m_ddfw)
return;
m_result = m_ddfw->check(0, nullptr);
IF_VERBOSE(1, verbose_stream() << "sls-result " << m_result << "\n");
IF_VERBOSE(2, verbose_stream() << "sls-result " << m_result << "\n");
for (auto v : m_shared_bool_vars) {
auto w = m_smt_bool_var2sls_bool_var[v];
m_rewards[v] = m_ddfw->get_reward_avg(w);
@ -127,6 +128,7 @@ namespace sls {
SASSERT(m_completed);
mdl = nullptr;
m_ddfw->collect_statistics(st);
m_context.collect_statistics(st);
if (m_result == l_true && m_sls_model) {
ast_translation tr(m_sls, m);
mdl = m_sls_model->translate(tr);