mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

Refactor handling of term registration and enhance distinct handling in sls_euf_plugin

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-08 19:26:51 -07:00
parent 633ea63a62
commit c9bd8d59ac
2 changed files with 30 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/sls/sls_context.cpp
View file

@ -446,6 +446,7 @@ namespace sls {
auto visit = [&](expr* e) { auto visit = [&](expr* e) {
m_allterms.setx(e->get_id(), e); m_allterms.setx(e->get_id(), e);
ensure_plugin(e); ensure_plugin(e);
register_term(e);
}; };
if (is_visited(e)) if (is_visited(e))
return; return;
@ -468,7 +469,6 @@ namespace sls {
} }
if (m.is_bool(e)) if (m.is_bool(e))
mk_literal(e); mk_literal(e);
register_term(e);
visit(e); visit(e);
} }
else { else {
@ -479,7 +479,6 @@ namespace sls {
else { else {
expr_ref _e(e, m); expr_ref _e(e, m);
m_todo.pop_back(); m_todo.pop_back();
register_term(e);
visit(e); visit(e);
} }
} }

29
src/ast/sls/sls_euf_plugin.cpp
View file

@ -227,8 +227,37 @@ namespace sls {
} }
else else
m_values.insert(t); m_values.insert(t);
}
}
for (auto lit : ctx.root_literals()) {
if (!ctx.is_true(lit))
lit.neg();
auto e = ctx.atom(lit.var());
if (lit.sign() && e && m.is_distinct(e)) {
auto n = to_app(e)->get_num_args();
expr_ref_vector eqs(m);
for (unsigned i = 0; i < n; ++i) {
auto arg = to_app(e)->get_arg(i);
auto a = ctx.get_value(arg);
for (unsigned j = i + 1; j < n; ++j) {
auto argb = to_app(e)->get_arg(j);
auto b = ctx.get_value(argb);
if (a == b)
goto done_distinct;
eqs.push_back(m.mk_eq(arg, argb));
}
}
// distinct(a, b, c) or a = b or a = c or b = c
eqs.push_back(e);
ctx.add_constraint(m.mk_or(eqs));
new_constraint = true;
done_distinct:
;
} }
} }
return new_constraint; return new_constraint;
} }