mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

#5454

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-11 16:59:46 -07:00
parent 8faad26c3c
commit fde8808a40
1 changed files with 18 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -118,14 +118,14 @@ namespace euf {
n->set_is_equality();
update_children(n);
reinsert_equality(n);
return n;
}
enode_bool_pair p = insert_table(n);
enode* n2 = p.first;
if (n2 == n)
update_children(n);
else
merge(n, n2, justification::congruence(p.second));
else {
auto [n2, comm] = insert_table(n);
if (n2 == n)
update_children(n);
else
merge(n, n2, justification::congruence(comm));
}
return n;
}
@ -266,6 +266,11 @@ namespace euf {
if (enable_merge != n->merge_enabled()) {
toggle_merge_enabled(n);
m_updates.push_back(update_record(n, update_record::toggle_merge()));
if (enable_merge && n->num_args() > 0) {
auto [n2, comm] = insert_table(n);
if (n2 != n)
merge(n, n2, justification::congruence(comm));
}
}
}
@ -403,7 +408,7 @@ namespace euf {
if (r1 == r2)
return;
TRACE("euf", j.display(tout << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
TRACE("euf", j.display(tout << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n" << bpp(r1) << " " << bpp(r2) << "\n";);
IF_VERBOSE(20, j.display(verbose_stream() << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
force_push();
SASSERT(m_num_scopes == 0);
@ -457,12 +462,13 @@ namespace euf {
if (!p->is_marked1())
continue;
p->unmark1();
TRACE("euf", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->merge_enabled() << "\n";);
if (p->merge_enabled()) {
auto rc = insert_table(p);
enode* p_other = rc.first;
auto [p_other, comm] = insert_table(p);
SASSERT(m_table.contains_ptr(p) == (p_other == p));
TRACE("euf", tout << "other " << bpp(p_other) << "\n";);
if (p_other != p)
m_to_merge.push_back(to_merge(p_other, p, rc.second));
m_to_merge.push_back(to_merge(p_other, p, comm));
else
r2->m_parents.push_back(p);
if (p->is_equality())
@ -752,7 +758,7 @@ namespace euf {
out << "] ";
}
if (n->value() != l_undef)
out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
if (n->has_th_vars()) {
out << "[t";
for (auto v : enode_th_vars(n))