mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

port remaining egraph update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-03 15:38:05 -08:00
parent a5a819c291
commit 9425c419ad
1 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -69,7 +69,7 @@ namespace euf {
} }
enode_bool_pair egraph::insert_table(enode* p) { enode_bool_pair egraph::insert_table(enode* p) {
TRACE("euf", tout << "insert_table " << bpp(p) << "\n"); TRACE("euf_verbose", tout << "insert_table " << bpp(p) << "\n");
//SASSERT(!m_table.contains_ptr(p)); //SASSERT(!m_table.contains_ptr(p));
auto rc = m_table.insert(p); auto rc = m_table.insert(p);
p->m_cg = rc.first; p->m_cg = rc.first;
@ -522,7 +522,7 @@ namespace euf {
} }
void egraph::remove_parents(enode* r) { void egraph::remove_parents(enode* r) {
TRACE("euf", tout << bpp(r) << "\n"); TRACE("euf_verbose", tout << bpp(r) << "\n");
SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); })); SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
for (enode* p : enode_parents(r)) { for (enode* p : enode_parents(r)) {
if (p->is_marked1()) if (p->is_marked1())
@ -533,7 +533,7 @@ namespace euf {
SASSERT(m_table.contains_ptr(p)); SASSERT(m_table.contains_ptr(p));
p->mark1(); p->mark1();
erase_from_table(p); erase_from_table(p);
CTRACE("euf", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout)); CTRACE("euf_verbose", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
SASSERT(!m_table.contains_ptr(p)); SASSERT(!m_table.contains_ptr(p));
} }
else if (p->is_equality()) else if (p->is_equality())
@ -546,11 +546,11 @@ namespace euf {
if (!p->is_marked1()) if (!p->is_marked1())
continue; continue;
p->unmark1(); p->unmark1();
TRACE("euf", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";); TRACE("euf_verbose", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
if (p->cgc_enabled()) { if (p->cgc_enabled()) {
auto [p_other, comm] = insert_table(p); auto [p_other, comm] = insert_table(p);
SASSERT(m_table.contains_ptr(p) == (p_other == p)); SASSERT(m_table.contains_ptr(p) == (p_other == p));
CTRACE("euf", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n"); CTRACE("euf_verbose", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
if (p_other != p) if (p_other != p)
m_to_merge.push_back(to_merge(p_other, p, comm)); m_to_merge.push_back(to_merge(p_other, p, comm));
else else
@ -584,14 +584,14 @@ namespace euf {
void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) { void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
enode* r2 = r1->get_root(); enode* r2 = r1->get_root();
TRACE("euf", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";); TRACE("euf_verbose", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
r2->dec_class_size(r1->class_size()); r2->dec_class_size(r1->class_size());
r2->set_is_shared(l_undef); r2->set_is_shared(l_undef);
std::swap(r1->m_next, r2->m_next); std::swap(r1->m_next, r2->m_next);
auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents(); auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents();
for (auto it = begin; it != end; ++it) { for (auto it = begin; it != end; ++it) {
enode* p = *it; enode* p = *it;
TRACE("euf", tout << "erase " << bpp(p) << "\n";); TRACE("euf_verbose", tout << "erase " << bpp(p) << "\n";);
SASSERT(!p->cgc_enabled() || m_table.contains_ptr(p)); SASSERT(!p->cgc_enabled() || m_table.contains_ptr(p));
SASSERT(!p->cgc_enabled() || p->is_cgr()); SASSERT(!p->cgc_enabled() || p->is_cgr());
if (p->cgc_enabled()) if (p->cgc_enabled())
@ -673,7 +673,7 @@ namespace euf {
SASSERT(n1->get_root()->reaches(n1)); SASSERT(n1->get_root()->reaches(n1));
SASSERT(n1->m_target); SASSERT(n1->m_target);
n1->m_target = nullptr; n1->m_target = nullptr;
n1->m_justification = justification::axiom(); n1->m_justification = justification::axiom(null_theory_id);
n1->get_root()->reverse_justification(); n1->get_root()->reverse_justification();
// --------------- // ---------------
// n1 -> ... -> r1 // n1 -> ... -> r1
@ -804,7 +804,10 @@ namespace euf {
explain_eq(justifications, cc, a, b, j2); explain_eq(justifications, cc, a, b, j2);
} }
else if (j.is_equality()) else if (j.is_equality())
explain_eq(justifications, cc, j.lhs(), j.rhs()); explain_eq(justifications, cc, j.lhs(), j.rhs());
else if (j.is_axiom() && j.get_theory_id() != null_theory_id) {
IF_VERBOSE(20, verbose_stream() << "TODO add theory axiom to justification\n");
}
if (cc && j.is_congruence()) if (cc && j.is_congruence())
cc->push_back(std::tuple(a->get_app(), b->get_app(), j.timestamp(), j.is_commutative())); cc->push_back(std::tuple(a->get_app(), b->get_app(), j.timestamp(), j.is_commutative()));
} }