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

egraph comment, remove unneeded check

Browse source
This commit is contained in:
Jakob Rath 2023-08-17 17:57:42 +02:00
parent f8c9ed1d90
commit 3e7f7ef605
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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;

3
src/ast/euf/euf_egraph.h
View file

@ -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);