mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

wip - tuning and fixes to euf-completion

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-16 03:47:38 -08:00
parent 98fc8c99db
commit 2c7799939e
2 changed files with 14 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/ast/simplifiers/euf_completion.cpp
View file

@ -74,8 +74,11 @@ namespace euf {
for (unsigned i = m_qhead; i < sz; ++i) { for (unsigned i = m_qhead; i < sz; ++i) {
auto [f,d] = m_fmls[i](); auto [f,d] = m_fmls[i]();
auto* n = mk_enode(f); auto* n = mk_enode(f);
if (m.is_eq(f)) if (m.is_eq(f)) {
m_egraph.merge(n->get_arg(0), n->get_arg(1), d); m_egraph.merge(n->get_arg(0), n->get_arg(1), d);
m_nodes.push_back(n->get_arg(0));
m_nodes.push_back(n->get_arg(1));
}
if (m.is_not(f)) if (m.is_not(f))
m_egraph.merge(n->get_arg(0), m_ff, d); m_egraph.merge(n->get_arg(0), m_ff, d);
else else
@ -97,8 +100,6 @@ namespace euf {
for (unsigned i = m_qhead; i < sz; ++i) { for (unsigned i = m_qhead; i < sz; ++i) {
auto [f, d] = m_fmls[i](); auto [f, d] = m_fmls[i]();
if (m.is_and(f))
IF_VERBOSE(0, verbose_stream() << "is-and " << mk_bounded_pp(f, m) << "\n");
expr_dependency_ref dep(d, m); expr_dependency_ref dep(d, m);
expr_ref g = canonize_fml(f, dep); expr_ref g = canonize_fml(f, dep);
if (g != f) { if (g != f) {
@ -106,30 +107,25 @@ namespace euf {
m_stats.m_num_rewrites++; m_stats.m_num_rewrites++;
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n"); IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
expr* x, * y; expr* x, * y;
if (m.is_eq(g, x, y) && find(x) != find(y)) if (m.is_eq(g, x, y) && new_eq(x, y))
m_has_new_eq = true; m_has_new_eq = true;
if (m.is_and(g) && !m_has_new_eq) if (m.is_and(g) && !m_has_new_eq)
for (expr* arg : *to_app(g)) for (expr* arg : *to_app(g))
if (m.is_eq(arg, x, y)) if (m.is_eq(arg, x, y))
m_has_new_eq |= find(x) != find(y); m_has_new_eq |= new_eq(x, y);
else else if (!m.is_true(arg))
m_has_new_eq = true; m_has_new_eq = true;
if (m.is_and(g))
IF_VERBOSE(0, verbose_stream() << mk_bounded_pp(g, m, 3) << "\n");
} }
CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n"); CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
} }
if (m_has_new_eq)
IF_VERBOSE(0, verbose_stream() << "new round\n");
if (!m_has_new_eq) if (!m_has_new_eq)
advance_qhead(m_fmls.size()); advance_qhead(m_fmls.size());
} }
enode* completion::find(expr* e) { bool completion::new_eq(expr* a, expr* b) {
enode* r = m_egraph.find(e); enode* na = m_egraph.find(a);
if (r) enode* nb = m_egraph.find(b);
return r; return !na || !nb || na->get_root() != nb->get_root();
return mk_enode(e);
} }
enode* completion::mk_enode(expr* e) { enode* completion::mk_enode(expr* e) {
@ -254,8 +250,6 @@ namespace euf {
enode* r = n->get_root(); enode* r = n->get_root();
d = m.mk_join(d, explain_eq(n, r)); d = m.mk_join(d, explain_eq(n, r));
d = m.mk_join(d, m_deps.get(r->get_id(), nullptr)); d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));
if (!m_canonical.get(r->get_id()))
IF_VERBOSE(0, verbose_stream() << r->get_id() << " " << m_egraph.bpp(n) << " " << m_egraph.bpp(r) << "\n");
SASSERT(m_canonical.get(r->get_id())); SASSERT(m_canonical.get(r->get_id()));
return m_canonical.get(r->get_id()); return m_canonical.get(r->get_id());
} }
@ -320,6 +314,8 @@ namespace euf {
void completion::map_canonical() { void completion::map_canonical() {
m_todo.reset(); m_todo.reset();
enode_vector roots; enode_vector roots;
if (m_nodes.empty())
return;
for (unsigned i = 0; i < m_nodes.size(); ++i) { for (unsigned i = 0; i < m_nodes.size(); ++i) {
enode* n = m_nodes[i]->get_root(); enode* n = m_nodes[i]->get_root();
if (n->is_marked1()) if (n->is_marked1())
@ -332,8 +328,6 @@ namespace euf {
rep = k; rep = k;
m_reps.setx(n->get_id(), rep, nullptr); m_reps.setx(n->get_id(), rep, nullptr);
if (n->get_id() == 87507)
IF_VERBOSE(0, verbose_stream() << "set-canon " << n->get_id() << "\n");
TRACE("euf_completion", tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n"; TRACE("euf_completion", tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n";
for (enode* k : enode_class(n)) tout << m_egraph.bpp(k) << "\n";); for (enode* k : enode_class(n)) tout << m_egraph.bpp(k) << "\n";);
m_todo.push_back(n->get_expr()); m_todo.push_back(n->get_expr());

2
src/ast/simplifiers/euf_completion.h
View file

@ -43,7 +43,7 @@ namespace euf {
bool m_has_new_eq = false; bool m_has_new_eq = false;
enode* mk_enode(expr* e); enode* mk_enode(expr* e);
enode* find(expr* e); bool new_eq(expr* a, expr* b);
expr_ref mk_and(expr* a, expr* b); expr_ref mk_and(expr* a, expr* b);
void add_egraph(); void add_egraph();
void map_canonical(); void map_canonical();