mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fixup interpretation building

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-18 13:34:55 -07:00
parent aa2292d5c4
commit a72ad44200
1 changed files with 55 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

91
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -276,8 +276,15 @@ namespace sls {
if (n->is_root()) if (n->is_root())
add_dep(n, deps); add_dep(n, deps);
auto trace_assignment = [&](euf::enode* n) {
for (auto sib : euf::enode_class(n))
tout << g->bpp(sib) << " ";
tout << " <- " << mk_bounded_pp(m_values.get(n->get_id()), m) << "\n";
};
deps.topological_sort(); deps.topological_sort();
expr_ref_vector args(m); expr_ref_vector args(m);
euf::enode_vector leaves, worklist;
obj_map<euf::enode, euf::enode_vector> leaf2root;
// walk topological sort in order of leaves to roots, attaching values to nodes. // walk topological sort in order of leaves to roots, attaching values to nodes.
for (euf::enode* n : deps.top_sorted()) { for (euf::enode* n : deps.top_sorted()) {
SASSERT(n->is_root()); SASSERT(n->is_root());
@ -289,8 +296,10 @@ namespace sls {
if (!dt.is_datatype(e)) if (!dt.is_datatype(e))
continue; continue;
euf::enode* con = get_constructor(n); euf::enode* con = get_constructor(n);
if (!con) if (!con) {
leaves.push_back(n);
continue; continue;
}
auto f = con->get_decl(); auto f = con->get_decl();
args.reset(); args.reset();
bool has_null = false; bool has_null = false;
@ -299,6 +308,7 @@ namespace sls {
auto val_arg = m_values.get(arg->get_root_id()); auto val_arg = m_values.get(arg->get_root_id());
if (!val_arg) if (!val_arg)
has_null = true; has_null = true;
leaf2root.insert_if_not_there(arg->get_root(), euf::enode_vector()).push_back(n);
args.push_back(val_arg); args.push_back(val_arg);
} }
else else
@ -307,13 +317,14 @@ namespace sls {
if (!has_null) { if (!has_null) {
m_values.setx(id, m.mk_app(f, args)); m_values.setx(id, m.mk_app(f, args));
m_model->register_value(m_values.get(id)); m_model->register_value(m_values.get(id));
TRACE("dt", tout << "Set interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); TRACE("dt", tout << "Set interpretation "; trace_assignment(n););
} }
} }
TRACE("dt", TRACE("dt",
for (euf::enode* n : deps.top_sorted()) { for (euf::enode* n : deps.top_sorted()) {
tout << g->bpp(n) << ": "; tout << g->bpp(n) << ": ";
tout << g->bpp(get_constructor(n)) << " :: ";
auto s = deps.get_dep(n); auto s = deps.get_dep(n);
if (s) { if (s) {
tout << " -> "; tout << " -> ";
@ -324,43 +335,51 @@ namespace sls {
} }
); );
// assign fresh values to uninterpeted nodes // attach fresh values to each leaf, walk up parents to assign them values.
for (euf::enode* n : deps.top_sorted()) { while (!leaves.empty()) {
SASSERT(worklist.empty());
SASSERT(n->is_root()); auto n = leaves.back();
expr* e = n->get_expr(); leaves.pop_back();
if (!dt.is_datatype(e)) SASSERT(!get_constructor(n));
continue; auto v = m_model->get_fresh_value(n->get_sort());
if (!v)
v = m_model->get_some_value(n->get_sort());
SASSERT(v);
unsigned id = n->get_id(); unsigned id = n->get_id();
if (m_values.get(id, nullptr)) m_values.setx(id, v);
continue; TRACE("dt", tout << "Fresh interpretation "; trace_assignment(n););
auto con = get_constructor(n); worklist.push_back(n);
if (!con) {
auto v = m_model->get_fresh_value(e->get_sort()); while (!worklist.empty()) {
if (!v) n = worklist.back();
v = m_model->get_some_value(e->get_sort()); worklist.pop_back();
SASSERT(v); if (!leaf2root.contains(n))
m_values.setx(id, v); continue;
TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); for (auto p : leaf2root[n]) {
continue; auto con = get_constructor(p);
} SASSERT(con);
TRACE("dt", tout << g->bpp(con) << " = " << g->bpp(n) << "\n"); auto f = con->get_decl();
auto f = con->get_decl(); args.reset();
args.reset(); bool has_missing = false;
for (auto arg : euf::enode_args(con)) { for (auto arg : euf::enode_args(con)) {
if (dt.is_datatype(arg->get_sort())) { if (dt.is_datatype(arg->get_sort())) {
auto* arg_val = m_values.get(arg->get_root_id()); auto arg_val = m_values.get(arg->get_root_id());
CTRACE("dt", !arg_val, tout << "Missing value for " << g->bpp(arg) << " " << g->bpp(arg->get_root()) << "\n"); if (!arg_val)
if (!arg_val) has_missing = true;
arg_val = m_model->get_some_value(arg->get_expr()->get_sort()); args.push_back(arg_val);
args.push_back(arg_val); }
else
args.push_back(ctx.get_value(arg->get_expr()));
}
if (has_missing)
continue;
worklist.push_back(p);
SASSERT(all_of(args, [&](expr* e) { return e != nullptr; }));
m_values.setx(p->get_id(), m.mk_app(f, args));
TRACE("dt", tout << "Patched interpretation "; trace_assignment(p););
m_model->register_value(m_values.get(p->get_id()));
} }
else
args.push_back(ctx.get_value(arg->get_expr()));
} }
SASSERT(all_of(args, [&](expr* e) { return e != nullptr; }));
m_values.setx(id, m.mk_app(f, args));
TRACE("dt", tout << "Patched interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
} }
} }