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

#5778

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-02 00:56:51 -07:00
parent 97115e5ebd
commit 229ea569f1
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/array_model.cpp
View file

@ -31,11 +31,11 @@ namespace array {
std::for_each(m_selects_range.begin(), m_selects_range.end(), delete_proc<select_set>()); std::for_each(m_selects_range.begin(), m_selects_range.end(), delete_proc<select_set>());
} }
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
if (!a.is_array(n->get_expr())) { if (!a.is_array(n->get_expr())) {
dep.insert(n, nullptr); dep.insert(n, nullptr);
return true; return true;
} }
for (euf::enode* p : euf::enode_parents(n->get_root())) { for (euf::enode* p : euf::enode_parents(n->get_root())) {
if (a.is_default(p->get_expr())) { if (a.is_default(p->get_expr())) {
dep.add(n, p); dep.add(n, p);
@ -47,6 +47,13 @@ namespace array {
for (unsigned i = 1; i < p->num_args(); ++i) for (unsigned i = 1; i < p->num_args(); ++i)
dep.add(n, p->get_arg(i)); dep.add(n, p->get_arg(i));
} }
if (a.is_array(n->get_expr())) {
for (euf::enode* p : *get_select_set(n)) {
dep.add(n, p);
for (unsigned i = 1; i < p->num_args(); ++i)
dep.add(n, p->get_arg(i));
}
}
for (euf::enode* k : euf::enode_class(n)) for (euf::enode* k : euf::enode_class(n))
if (a.is_const(k->get_expr())) if (a.is_const(k->get_expr()))
dep.add(n, k->get_arg(0)); dep.add(n, k->get_arg(0));