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

redo dfs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-17 12:59:59 -07:00
parent 69c28f8652
commit 7b42ab5264
1 changed files with 67 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -311,9 +311,22 @@ namespace sls {
} }
} }
TRACE("dt",
for (euf::enode* n : deps.top_sorted()) {
tout << g->bpp(n) << ": ";
auto s = deps.get_dep(n);
if (s) {
tout << " -> ";
for (auto t : *s)
tout << g->bpp(t) << " ";
}
tout << "\n";
}
);
// assign fresh values to uninterpeted nodes // assign fresh values to uninterpeted nodes
for (euf::enode* n : deps.top_sorted()) { for (euf::enode* n : deps.top_sorted()) {
TRACE("dt", tout << g->bpp(n) << "\n");
SASSERT(n->is_root()); SASSERT(n->is_root());
expr* e = n->get_expr(); expr* e = n->get_expr();
if (!dt.is_datatype(e)) if (!dt.is_datatype(e))
@ -331,11 +344,17 @@ namespace sls {
TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
continue; continue;
} }
TRACE("dt", tout << g->bpp(con) << " = " << g->bpp(n) << "\n");
auto f = con->get_decl(); auto f = con->get_decl();
args.reset(); args.reset();
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())) {
args.push_back(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)
arg_val = m_model->get_some_value(arg->get_expr()->get_sort());
args.push_back(arg_val);
}
else else
args.push_back(ctx.get_value(arg->get_expr())); args.push_back(ctx.get_value(arg->get_expr()));
} }
@ -376,9 +395,27 @@ namespace sls {
bool datatype_plugin::propagate() { bool datatype_plugin::propagate() {
enum color_t { white, grey, black }; enum color_t { white, grey, black };
svector<color_t> color; svector<color_t> color;
unsigned_vector dfsnum; svector<std::tuple<euf::enode*, unsigned>> todo;
svector<std::tuple<unsigned, euf::enode*, unsigned>> todo;
obj_map<sort, ptr_vector<expr>> sorts; obj_map<sort, ptr_vector<expr>> sorts;
auto set_conflict = [&](euf::enode* n, unsigned parent_idx) {
expr_ref_vector diseqs(m);
while (true) {
auto [n2, parent_idx2] = todo[parent_idx];
auto con2 = get_constructor(n2);
if (n2 != con2)
diseqs.push_back(m.mk_not(m.mk_eq(n2->get_expr(), con2->get_expr())));
parent_idx = parent_idx2;
if (n2->get_root() == n->get_root()) {
if (n != n2)
diseqs.push_back(m.mk_not(m.mk_eq(n->get_expr(), n2->get_expr())));
break;
}
}
IF_VERBOSE(1, verbose_stream() << "cycle\n"; for (auto e : diseqs) verbose_stream() << mk_pp(e, m) << "\n";);
ctx.add_constraint(m.mk_or(diseqs));
};
for (auto n : g->nodes()) { for (auto n : g->nodes()) {
if (!n->is_root()) if (!n->is_root())
continue; continue;
@ -395,16 +432,14 @@ namespace sls {
if (c == black) if (c == black)
continue; continue;
dfsnum.setx(e->get_id(), 0, UINT_MAX);
// dfs traversal of enodes, starting with n, // dfs traversal of enodes, starting with n,
// with outgoing edges the arguments of con, where con // with outgoing edges the arguments of con, where con
// is a node in the same congruence class as n that is a constructor. // is a node in the same congruence class as n that is a constructor.
// For every cycle accumulate a conflict. // For every cycle accumulate a conflict.
todo.push_back({ 0, n, 0 }); todo.push_back({ n, 0});
while (!todo.empty()) { while (!todo.empty()) {
auto [depth, n, parent_idx] = todo.back(); auto [n, parent_idx] = todo.back();
unsigned id = n->get_root_id(); unsigned id = n->get_root_id();
c = color.get(id, white); c = color.get(id, white);
euf::enode* con; euf::enode* con;
@ -415,40 +450,34 @@ namespace sls {
todo.pop_back(); todo.pop_back();
break; break;
case grey: case grey:
if (dfsnum.get(id, UINT_MAX) < depth) { case white: {
expr_ref_vector diseqs(m); bool new_child = false;
while (true) {
auto [depth2, n2, parent_idx2] = todo[parent_idx];
auto con2 = get_constructor(n2);
if (n2 != con2)
diseqs.push_back(m.mk_not(m.mk_eq(n2->get_expr(), con2->get_expr())));
parent_idx = parent_idx2;
if (n2->get_root() == n->get_root()) {
diseqs.push_back(m.mk_not(m.mk_eq(n->get_expr(), n2->get_expr())));
break;
}
}
IF_VERBOSE(1,
verbose_stream() << "cycle\n";
for (auto e : diseqs)
verbose_stream() << mk_pp(e, m) << "\n";);
ctx.add_constraint(m.mk_or(diseqs));
return true;
}
color[id] = black;
todo.pop_back();
break;
case white:
color.setx(id, grey, white); color.setx(id, grey, white);
dfsnum.setx(id, depth, UINT_MAX);
con = get_constructor(n); con = get_constructor(n);
idx = todo.size() - 1; idx = todo.size() - 1;
if (con) if (con) {
for (auto child : euf::enode_args(con)) for (auto child : euf::enode_args(con)) {
if (color.get(child->get_root_id(), black) != black && dt.is_datatype(child->get_expr())) auto c2 = color.get(child->get_root_id(), white);
todo.push_back({ depth + 1, child, idx }); switch (c2) {
case black:
break;
case grey:
set_conflict(child, idx);
return true;
case white:
todo.push_back({ child, idx });
new_child = true;
break;
}
}
}
if (!new_child) {
color[id] = black;
todo.pop_back();
}
break; break;
} }
}
} }
} }