mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
self-contained function for merge_tf
This commit is contained in:
parent
0949ad26c2
commit
0b8939d86e
|
@ -161,6 +161,7 @@ namespace euf {
|
|||
bool commutative() const { return m_commutative; }
|
||||
void mark_interpreted() { SASSERT(num_args() == 0); m_interpreted = true; }
|
||||
bool merge_enabled() const { return m_merge_enabled; }
|
||||
bool merge_tf() const { return merge_enabled() && (class_size() > 1 || num_parents() > 0 || num_args() > 0); }
|
||||
|
||||
enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; }
|
||||
unsigned hash() const { return m_expr->hash(); }
|
||||
|
|
|
@ -308,7 +308,7 @@ namespace euf {
|
|||
euf::enode* nb = n->get_arg(1);
|
||||
m_egraph.merge(na, nb, c);
|
||||
}
|
||||
else if (n->merge_enabled() && (n->num_parents() > 0 || n->num_args() > 0)) {
|
||||
else if (n->merge_tf()) {
|
||||
euf::enode* nb = sign ? mk_false() : mk_true();
|
||||
m_egraph.merge(n, nb, c);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue