mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
f3f83d0445
commit
31267e6ab8
|
@ -417,14 +417,7 @@ namespace euf {
|
|||
std::swap(r1, r2);
|
||||
std::swap(n1, n2);
|
||||
}
|
||||
if (m.is_false(r2->get_expr()) && r1->value() == l_true) {
|
||||
set_conflict(n1, n2, j);
|
||||
return;
|
||||
}
|
||||
if (m.is_true(r2->get_expr()) && r1->value() == l_false) {
|
||||
set_conflict(n1, n2, j);
|
||||
return;
|
||||
}
|
||||
|
||||
if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
|
||||
add_literal(n1, false);
|
||||
if (n1->is_equality() && n1->value() == l_false)
|
||||
|
|
|
@ -214,14 +214,6 @@ namespace euf {
|
|||
TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";);
|
||||
DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
|
||||
|
||||
#if 0
|
||||
if (r.size() == 5 && r[0] == literal(401, true) && r[1] == literal(259, false) && r[2] == literal(250, false) &&
|
||||
r[3] == literal(631, false) && r[4] == literal(639, false)) {
|
||||
TRACE("euf", s().display(tout););
|
||||
exit(0);
|
||||
}
|
||||
#endif
|
||||
|
||||
if (!probing)
|
||||
log_antecedents(l, r);
|
||||
}
|
||||
|
@ -311,19 +303,20 @@ namespace euf {
|
|||
if (n->value_conflict()) {
|
||||
euf::enode* nb = sign ? mk_false() : mk_true();
|
||||
m_egraph.merge(n, nb, c);
|
||||
return;
|
||||
}
|
||||
else if (!sign && n->is_equality()) {
|
||||
if (n->merge_tf()) {
|
||||
euf::enode* nb = sign ? mk_false() : mk_true();
|
||||
m_egraph.merge(n, nb, c);
|
||||
}
|
||||
if (!sign && n->is_equality()) {
|
||||
SASSERT(!m.is_iff(e));
|
||||
euf::enode* na = n->get_arg(0);
|
||||
euf::enode* nb = n->get_arg(1);
|
||||
m_egraph.merge(na, nb, c);
|
||||
}
|
||||
else if (n->merge_tf()) {
|
||||
euf::enode* nb = sign ? mk_false() : mk_true();
|
||||
m_egraph.merge(n, nb, c);
|
||||
}
|
||||
else if (sign && n->is_equality())
|
||||
m_egraph.new_diseq(n);
|
||||
else if (sign && n->is_equality())
|
||||
m_egraph.new_diseq(n);
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue