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

read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-22 14:07:29 +01:00
parent a214dc32e8
commit fb5bbb8074
3 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_setup.cpp
View file

@ -834,7 +834,6 @@ namespace smt {
// there are some other cases where relevancy propagation is harmful.
//
void setup::setup_relevancy(static_features& st) {
return;
if (st.m_has_bv && !st.m_has_fpa && st.m_num_quantifiers == 0)
m_params.m_relevancy_lvl = 0;
}

15
src/smt/theory_array.cpp
View file

@ -30,8 +30,6 @@ namespace smt {
m_find(*this),
m_trail_stack(),
m_final_check_idx(0) {
if (!ctx.relevancy())
m_params.m_array_laziness = 0;
}
theory_array::~theory_array() {
@ -39,6 +37,10 @@ namespace smt {
m_var_data.reset();
}
void theory_array::init_search_eh() {
m_final_check_idx = 0;
}
void theory_array::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
// v1 is the new root
TRACE("array",
@ -77,7 +79,7 @@ namespace smt {
if (is_store(n))
d->m_stores.push_back(n);
ctx.attach_th_var(n, this, r);
if (m_params.m_array_laziness <= 1 && is_store(n))
if (laziness() <= 1 && is_store(n))
instantiate_axiom1(n);
return r;
}
@ -238,6 +240,7 @@ namespace smt {
// Internalize the term. If it has already been internalized, return false.
//
bool theory_array::internalize_term_core(app * n) {
TRACE("array_bug", tout << mk_bounded_pp(n, m) << "\n";);
for (expr* arg : *n)
ctx.internalize(arg, false);
@ -275,7 +278,7 @@ namespace smt {
mk_var(arg0);
if (m_params.m_array_laziness == 0) {
if (laziness() == 0) {
theory_var v_arg = arg0->get_th_var(get_id());
SASSERT(v_arg != null_theory_var);
@ -320,7 +323,7 @@ namespace smt {
}
void theory_array::relevant_eh(app * n) {
if (m_params.m_array_laziness == 0)
if (laziness() == 0)
return;
if (m.is_ite(n)) {
TRACE("array", tout << "relevant ite " << mk_pp(n, m) << "\n";);
@ -338,7 +341,7 @@ namespace smt {
}
else {
SASSERT(is_store(n));
if (m_params.m_array_laziness > 1)
if (laziness() > 1)
instantiate_axiom1(e);
add_parent_store(v_arg, e);
}

3
src/smt/theory_array.h
View file

@ -34,6 +34,7 @@ namespace smt {
};
class theory_array : public theory_array_base {
unsigned laziness() const { return ctx.relevancy()?m_params.m_array_laziness:0; }
protected:
typedef union_find<theory_array> th_union_find;
@ -64,7 +65,7 @@ namespace smt {
void pop_scope_eh(unsigned num_scopes) override;
final_check_status final_check_eh() override;
void reset_eh() override;
void init_search_eh() override { m_final_check_idx = 0; }
void init_search_eh() override;
void set_prop_upward(theory_var v) override;
virtual void set_prop_upward(enode* n);