From 3e7f7ef605249bbf88e7bb6db4fe820c048a5a30 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 17 Aug 2023 17:57:42 +0200 Subject: [PATCH] egraph comment, remove unneeded check --- src/ast/euf/euf_egraph.cpp | 3 ++- src/ast/euf/euf_egraph.h | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 16d1fde81..8ab44d8cd 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -793,7 +793,8 @@ namespace euf { CTRACE("euf_verbose", m_display_justification, n->m_justification.display(tout << n->get_expr_id() << " = " << n->m_target->get_expr_id() << " ", m_display_justification) << "\n";); explain_eq(justifications, cc, n, n->m_target, n->m_justification); } - else if (!n->is_marked1() && n->value() != l_undef) { + else if (n->value() != l_undef) { + SASSERT(!n->is_marked1()); n->mark1(); if (m.is_true(n->get_expr()) || m.is_false(n->get_expr())) continue; diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 7c34184e8..5158f2fc9 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -249,7 +249,8 @@ namespace euf { void pop(unsigned num_scopes); /** - \brief merge nodes, all effects are deferred to the propagation step. + * \brief Merge nodes, all effects are deferred to the propagation step. (TODO: is that comment outdated? at least in polysat::slicing it seems we almost never need to call propagate() separately.) + * The root of the merged class will be root(n2), unless there is a specific reason to prefer root(n1). */ void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); } void new_diseq(enode* n);