mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix re-entrancy bug between ddfw and theory solvers.

Browse source 
Flips triggered from external sources should not trigger callbacks.
This commit is contained in:
Nikolaj Bjorner 2025-01-22 10:59:52 -08:00
parent 071c9abd69
commit 72c7a9cf6a
4 changed files with 19 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -99,8 +99,8 @@ namespace sat {
m_last_flips = m_flips;
}
sat::bool_var ddfw::bool_flip() {
flet<bool> _in_bool_flip(m_in_bool_flip, true);
sat::bool_var ddfw::external_flip() {
flet<bool> _in_external_flip(m_in_external_flip, true);
double reward = 0;
bool_var v = pick_var(reward);
if (apply_flip(v, reward))
@ -135,7 +135,7 @@ namespace sat {
bool_var v0 = null_bool_var;
for (bool_var v : m_unsat_vars) {
r = reward(v);
if (m_in_bool_flip && m_plugin->is_external(v))
if (m_in_external_flip && m_plugin->is_external(v))
;
else if (r > 0.0)
sum_pos += score(r);
@ -146,7 +146,7 @@ namespace sat {
double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;
for (bool_var v : m_unsat_vars) {
r = reward(v);
if (m_in_bool_flip && m_plugin->is_external(v))
if (m_in_external_flip && m_plugin->is_external(v))
continue;
if (r > 0) {
lim_pos -= score(r);
@ -160,7 +160,7 @@ namespace sat {
return v0;
if (m_unsat_vars.empty())
return null_bool_var;
if (m_in_bool_flip)
if (m_in_external_flip)
return false;
return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
}
@ -258,6 +258,11 @@ namespace sat {
return true;
}
void ddfw::external_flip(bool_var v) {
flet<bool> _external_flip(m_in_external_flip, true);
flip(v);
}
void ddfw::flip(bool_var v) {
++m_flips;
m_limit.inc();
@ -417,7 +422,7 @@ namespace sat {
for (unsigned i = 0; i < num_vars(); ++i)
m_model[i] = to_lbool(value(i));
save_priorities();
if (m_plugin && !m_in_bool_flip)
if (m_plugin && !m_in_external_flip)
m_last_result = m_plugin->on_save_model();
}

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

@ -214,7 +214,9 @@ namespace sat {
bool_var_set m_rotate_tabu;
bool_var_vector m_new_tabu_vars;
bool m_in_bool_flip = false;
void flip(bool_var v);
bool m_in_external_flip = false;
public:
@ -265,9 +267,8 @@ namespace sat {
void remove_assumptions();
void flip(bool_var v);
sat::bool_var bool_flip();
void external_flip(sat::bool_var v);
sat::bool_var external_flip();
void shift_weights();

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

@ -238,6 +238,7 @@ namespace sls {
m_last_delta = delta;
if (!a.can_update_num(v, delta))
return;
ctx.rlimit().inc();
auto score = get_score(v, delta);
auto& vi = a.m_vars[v];
num_t abs_value = abs(vi.value() + delta);

4
src/ast/sls/sls_context.h
View file

@ -69,7 +69,7 @@ namespace sls {
virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
virtual void flip(sat::bool_var v) = 0;
virtual sat::bool_var bool_flip() = 0;
virtual sat::bool_var external_flip() = 0;
virtual bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) = 0;
virtual double reward(sat::bool_var v) = 0;
virtual double get_weigth(unsigned clause_idx) = 0;
@ -189,7 +189,7 @@ namespace sls {
void add_theory_axiom(expr* f) { add_assertion(f, false); }
void add_clause(sat::literal_vector const& lits);
void flip(sat::bool_var v) { s.flip(v); }
sat::bool_var bool_flip() { return s.bool_flip(); }
sat::bool_var bool_flip() { return s.external_flip(); }
void shift_weights() { s.shift_weights(); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
double reward(sat::bool_var v) { return s.reward(v); }