From fde8808a40df3d88d560cb0c9ec0885e42296633 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Aug 2021 16:59:46 -0700
Subject: [PATCH] #5454
---
src/ast/euf/euf_egraph.cpp | 30 ++++++++++++++++++------------
1 file changed, 18 insertions(+), 12 deletions(-)
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 2a0159265..0af855baf 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -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))