mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Refactor array_plugin in sls to improve handling of select expressions with multiple arguments

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-07 15:12:39 -07:00
parent 2f2559d670
commit 25c19b61dd
2 changed files with 32 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/sls/sls_array_plugin.cpp
View file

@ -193,7 +193,7 @@ namespace sls {
g.merge(n1, n2, nullptr);
}
for (auto lit : ctx.root_literals()) {
if (!ctx.is_true(lit))
if (!ctx.is_true(lit) || lit.sign())
continue;
auto e = ctx.atom(lit.var());
expr* x, * y;
@ -209,16 +209,14 @@ namespace sls {
for (auto n : g.nodes()) {
if (!n->is_root() || !a.is_array(n->get_expr()))
continue;
kv.insert(n, obj_map<euf::enode, euf::enode*>());
kv.insert(n, select2value());
for (auto p : euf::enode_parents(n)) {
if (!a.is_select(p->get_expr()))
continue;
SASSERT(p->num_args() == 2);
if (p->get_arg(0)->get_root() != n->get_root())
continue;
auto idx = p->get_arg(1)->get_root();
auto val = p->get_root();
kv[n].insert(idx, val);
kv[n].insert(select_args(p), val);
}
}
display(verbose_stream());
@ -242,7 +240,7 @@ namespace sls {
for (auto [k, v] : kv[n]) {
ptr_vector<expr> args;
args.push_back(r);
args.push_back(k->get_expr());
args.push_back(k.sel->get_arg(1)->get_expr());
args.push_back(v->get_expr());
r = a.mk_store(args);
}
@ -257,7 +255,10 @@ namespace sls {
out << m_g->pp(n) << " -> {";
char const* sp = "";
for (auto& [k, v] : kvs) {
out << sp << m_g->pp(k) << " -> " << m_g->pp(v);
out << sp;
for (unsigned i = 1; i < k.sel->num_args(); ++i)
out << m_g->pp(k.sel->get_arg(i)->get_root()) << " ";
out << "-> " << m_g->pp(v);
sp = " ";
}
out << "}\n";

25
src/ast/sls/sls_array_plugin.h
View file

@ -23,7 +23,30 @@ Author:
namespace sls {
class array_plugin : public plugin {
typedef obj_map<euf::enode, obj_map<euf::enode, euf::enode*>> kv;
struct select_args {
euf::enode* sel = nullptr;
select_args(euf::enode* s) : sel(s) {}
select_args() {}
};
struct select_args_hash {
unsigned operator()(select_args const& a) const {
unsigned h = 0;
for (unsigned i = 1; i < a.sel->num_args(); ++i)
h ^= a.sel->get_arg(i)->get_root()->hash();
return h;
};
};
struct select_args_eq {
bool operator()(select_args const& a, select_args const& b) const {
SASSERT(a.sel->num_args() == b.sel->num_args());
for (unsigned i = 1; i < a.sel->num_args(); ++i)
if (a.sel->get_arg(i)->get_root() != b.sel->get_arg(i)->get_root())
return false;
return true;
}
};
typedef map<select_args, euf::enode*, select_args_hash, select_args_eq> select2value;
typedef obj_map<euf::enode, select2value> kv;
array_util a;
scoped_ptr<euf::egraph> m_g;