mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

optimizing array final check

Browse source
This commit is contained in:
Ken McMillan 2014-09-30 11:21:34 -07:00
parent 13b61d894c
commit 4c71e9479d
1 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_array_base.cpp
View file

@ -376,8 +376,10 @@ namespace smt {
enode_vector::const_iterator end = r->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
#if 0
if (!ctx.is_relevant(parent))
continue;
#endif
unsigned num_args = parent->get_num_args();
if (is_store(parent)) {
SET_ARRAY(parent->get_arg(0));
@ -399,6 +401,7 @@ namespace smt {
return false;
}
#if 0
void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
TRACE("array_shared", tout << "collecting shared vars...\n";);
context & ctx = get_context();
@ -420,6 +423,29 @@ namespace smt {
}
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
}
#else
void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
TRACE("array_shared", 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 * r = n->get_root();
if (!r->is_marked() && 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);
}
r->set_mark();
to_unmark.push_back(r);
}
}
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
}
#endif
/**
\brief Create interface variables for shared array variables.