mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5417 normalize clause

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-19 09:08:51 -07:00
parent 7d915eb295
commit 776f270b64
2 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/q_clause.h
View file

@ -29,7 +29,9 @@ namespace q {
expr_ref rhs; expr_ref rhs;
bool sign; bool sign;
lit(expr_ref const& lhs, expr_ref const& rhs, bool sign): lit(expr_ref const& lhs, expr_ref const& rhs, bool sign):
lhs(lhs), rhs(rhs), sign(sign) {} lhs(lhs), rhs(rhs), sign(sign) {
SASSERT(!rhs.m().is_false(rhs) || !sign);
}
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };

10
src/sat/smt/q_ematch.cpp
View file

@ -419,6 +419,16 @@ namespace q {
r = sign ? m.mk_false() : m.mk_true(); r = sign ? m.mk_false() : m.mk_true();
sign = false; sign = false;
} }
if (m.is_true(l) || m.is_false(l))
std::swap(l, r);
if (sign && m.is_false(r)) {
r = m.mk_true();
sign = false;
}
else if (sign && m.is_true(r)) {
r = m.mk_false();
sign = false;
}
cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign)); cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
} }
if (q->get_num_patterns() == 0) { if (q->get_num_patterns() == 0) {