mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 07:15:26 +00:00
Code Activity

#5778

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-06 08:17:27 +02:00
parent cebbc71330
commit 2f63747c7b
1 changed files with 17 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,19 +36,13 @@ namespace array {
dep.insert(n, nullptr); dep.insert(n, nullptr);
return true; return true;
} }
for (euf::enode* p : euf::enode_parents(n->get_root())) {
if (a.is_default(p->get_expr())) {
dep.add(n, p);
continue;
}
if (!a.is_select(p->get_expr()))
continue;
dep.add(n, p);
for (unsigned i = 1; i < p->num_args(); ++i)
dep.add(n, p->get_arg(i));
}
if (a.is_array(n->get_expr())) { if (a.is_array(n->get_expr())) {
for (euf::enode* p : euf::enode_parents(n->get_root()))
if (a.is_default(p->get_expr()))
dep.add(n, p);
for (euf::enode* p : *get_select_set(n)) { for (euf::enode* p : *get_select_set(n)) {
SASSERT(n != p);
dep.add(n, p); dep.add(n, p);
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));
@ -57,10 +51,15 @@ namespace array {
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));
for (euf::enode* k : euf::enode_class(n))
if (a.is_const(k->get_expr())) {
SASSERT(n != k->get_arg(0));
}
theory_var v = get_th_var(n); theory_var v = get_th_var(n);
euf::enode* d = get_default(v); euf::enode* d = get_default(v);
if (d) if (d)
dep.add(n, d); dep.add(n, d);
SASSERT(n != d);
if (!dep.deps().contains(n)) if (!dep.deps().contains(n))
dep.insert(n, nullptr); dep.insert(n, nullptr);
return true; return true;
@ -127,6 +126,12 @@ namespace array {
if (!value || value == fi->get_else()) if (!value || value == fi->get_else())
continue; continue;
args.reset(); args.reset();
for (unsigned i = 1; i < p->num_args(); ++i) {
if (!values.get(p->get_arg(i)->get_root_id())) {
TRACE("array", tout << ctx.bpp(p->get_arg(i)) << "\n");
}
SASSERT(values.get(p->get_arg(i)->get_root_id()));
}
for (unsigned i = 1; i < p->num_args(); ++i) for (unsigned i = 1; i < p->num_args(); ++i)
args.push_back(values.get(p->get_arg(i)->get_root_id())); args.push_back(values.get(p->get_arg(i)->get_root_id()));
fi->insert_entry(args.data(), value); fi->insert_entry(args.data(), value);