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

#5778 - ensure arrays used inside of extensionality function are treated as shared

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-25 17:17:59 +01:00
parent 0a665b0fa0
commit 8e2f09b517
2 changed files with 9 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/array_axioms.cpp
View file

@ -629,12 +629,14 @@ namespace array {
euf::enode * n = var2enode(i); euf::enode * n = var2enode(i);
if (!is_array(n)) if (!is_array(n))
continue; continue;
CTRACE("array", !ctx.is_relevant(n), tout << "not relevant: " << ctx.bpp(n) << "\n");
if (!ctx.is_relevant(n)) if (!ctx.is_relevant(n))
continue; continue;
euf::enode * r = n->get_root(); euf::enode * r = n->get_root();
if (r->is_marked1()) if (r->is_marked1())
continue; continue;
// arrays used as indices in other arrays have to be treated as shared issue #3532, #3529 // arrays used as indices in other arrays have to be treated as shared issue #3532, #3529
CTRACE("array", !ctx.is_shared(r) && !is_shared_arg(r), tout << "not shared: " << ctx.bpp(r) << "\n");
if (ctx.is_shared(r) || is_shared_arg(r)) if (ctx.is_shared(r) || is_shared_arg(r))
roots.push_back(r->get_th_var(get_id())); roots.push_back(r->get_th_var(get_id()));
r->mark1(); r->mark1();
@ -655,6 +657,8 @@ namespace array {
return true; return true;
if (a.is_const(e)) if (a.is_const(e))
return true; return true;
if (a.is_ext(e))
return true;
} }
return false; return false;

36
src/smt/theory_array_base.cpp
View file

@ -473,39 +473,12 @@ namespace smt {
return false; return false;
} }
#if 0
void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
TRACE("array_shared", tout << "collecting shared vars...\n";);
ptr_buffer<enode> to_unmark;
unsigned num_vars = get_num_vars();
for (unsigned i = 0; i < num_vars; i++) {
enode * n = get_enode(i);
if (ctx.is_relevant(n) && ctx.is_shared(n)) {
enode * r = n->get_root();
if (!r->is_marked() && is_array_sort(r)) {
TRACE("array_shared", tout << "new shared var: #" << r->get_expr_id() << "\n";);
r->set_mark();
to_unmark.push_back(r);
theory_var r_th_var = r->get_var(get_id());
SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);
}
}
}
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
}
#else
bool theory_array_base::is_select_arg(enode* r) { bool theory_array_base::is_select_arg(enode* r) {
for (enode* n : r->get_parents()) { for (enode* n : r->get_parents())
if (is_select(n)) { if (is_select(n))
for (unsigned i = 1; i < n->get_num_args(); ++i) { for (unsigned i = 1; i < n->get_num_args(); ++i)
if (r == n->get_arg(i)->get_root()) { if (r == n->get_arg(i)->get_root())
return true; return true;
}
}
}
}
return false; return false;
} }
@ -536,7 +509,6 @@ namespace smt {
TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(result.size(), (unsigned*)result.data()) << "\n";); TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(result.size(), (unsigned*)result.data()) << "\n";);
unmark_enodes(to_unmark.size(), to_unmark.data()); unmark_enodes(to_unmark.size(), to_unmark.data());
} }
#endif
/** /**
\brief Create interface variables for shared array variables. \brief Create interface variables for shared array variables.