mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix #3532

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-29 12:32:23 -07:00
parent 0b10cb3312
commit c142f99127
3 changed files with 31 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/array_factory.cpp
View file

@ -72,6 +72,7 @@ expr * array_factory::get_some_value(sort * s) {
}
bool array_factory::mk_two_diff_values_for(sort * s) {
TRACE("array_factory", tout << mk_pp(s, m_manager) << "\n";);
DEBUG_CODE({
value_set * set = 0;
SASSERT(!m_sort2value_set.find(s, set) || set->size() <= 1);
@ -112,6 +113,7 @@ bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
v1 = *it;
++it;
v2 = *it;
TRACE("array_factory", tout << v1 << " " << v2 << "\n";);
return true;
}

40
src/smt/theory_array_base.cpp
View file

@ -509,26 +509,42 @@ namespace smt {
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
}
#else
bool theory_array_base::has_array_ext(enode* n) {
enode* r = n;
do {
if (is_array_ext(n->get_owner()))
return true;
n = n->get_next();
}
while (r != n);
return false;
}
void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
TRACE("array_shared", tout << "collecting shared vars...\n";);
TRACE("array", tout << "collecting shared vars...\n";);
context & ctx = get_context();
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)) {
enode * n = get_enode(i);
if (!ctx.is_relevant(n) || !is_array_sort(n)) {
continue;
}
enode * r = n->get_root();
if (!r->is_marked()){
if(is_array_sort(r) && ctx.is_shared(r)) {
TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
theory_var r_th_var = r->get_th_var(get_id());
SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);
if (r->is_marked()) {
continue;
}
// array extensionality terms may be produced in nested arrays.
// they have to be treated as shared to resolve equalities.
// issue #3532
if (ctx.is_shared(r) || has_array_ext(r)) {
TRACE("array", tout << "new shared var: #" << r->get_owner_id() << "\n";);
theory_var r_th_var = r->get_th_var(get_id());
SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);
}
r->set_mark();
to_unmark.push_back(r);
}
}
to_unmark.push_back(r);
}
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
}

1
src/smt/theory_array_base.h
View file

@ -60,6 +60,7 @@ namespace smt {
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_owner()); }
bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_owner()); }
bool is_set_carde(enode const* n) const { return is_set_card(n->get_owner()); }
bool has_array_ext(enode* n);
app * mk_select(unsigned num_args, expr * const * args);