mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

fix tmp_eq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-28 14:27:46 -07:00
parent da124e4275
commit 67ae75bac7
1 changed files with 14 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/ast/euf/euf_egraph.cpp
View file

@ -600,15 +600,6 @@ namespace euf {
return true; return true;
if (ra->get_sort() != rb->get_sort()) if (ra->get_sort() != rb->get_sort())
return true; return true;
if (ra->num_parents() > rb->num_parents())
std::swap(ra, rb);
if (ra->num_parents() <= 3) {
for (enode* p : enode_parents(ra))
if (p->is_equality() && p->get_root()->value() == l_false &&
(rb == p->get_arg(0)->get_root() || rb == p->get_arg(1)->get_root()))
return true;
return false;
}
enode* r = tmp_eq(ra, rb); enode* r = tmp_eq(ra, rb);
if (r && r->get_root()->value() == l_false) if (r && r->get_root()->value() == l_false)
return true; return true;
@ -622,21 +613,15 @@ namespace euf {
} }
enode* egraph::tmp_eq(enode* a, enode* b) { enode* egraph::tmp_eq(enode* a, enode* b) {
func_decl* f = nullptr; SASSERT(a->is_root());
for (unsigned i = m_eq_decls.size(); i-- > 0; ) { SASSERT(b->is_root());
auto e = m_eq_decls.get(i); if (a->num_parents() > b->num_parents())
if (e->get_domain(0) == a->get_sort()) { std::swap(a, b);
f = e; for (enode* p : enode_parents(a))
break; if (p->is_equality() &&
} (b == p->get_arg(0)->get_root() || b == p->get_arg(1)->get_root()))
} return p;
if (!f) { return nullptr;
app_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
m_eq_decls.push_back(eq->get_decl());
f = eq->get_decl();
}
enode* args[2] = { a, b };
return get_enode_eq_to(f, 2, args);
} }
/** /**
@ -736,7 +721,11 @@ namespace euf {
explain_eq(justifications, b, rb); explain_eq(justifications, b, rb);
return sat::null_bool_var; return sat::null_bool_var;
} }
enode* r = tmp_eq(a, b); enode* r = tmp_eq(ra, rb);
if (!r) {
std::cout << bpp(a) << " " << bpp(b) << "\n";
display(std::cout);
}
SASSERT(r && r->get_root()->value() == l_false); SASSERT(r && r->get_root()->value() == l_false);
explain_eq(justifications, r, r->get_root()); explain_eq(justifications, r, r->get_root());
return r->get_root()->bool_var(); return r->get_root()->bool_var();