From 776f270b64a52fd85fe6c3f9c0c733d34722f27c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Jul 2021 09:08:51 -0700 Subject: [PATCH] #5417 normalize clause --- src/sat/smt/q_clause.h | 4 +++- src/sat/smt/q_ematch.cpp | 10 ++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 8eca0df76..2107b2172 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -29,7 +29,9 @@ namespace q { expr_ref 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; }; diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 7de922f40..6040c4b4b 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -419,6 +419,16 @@ namespace q { r = sign ? m.mk_false() : m.mk_true(); 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)); } if (q->get_num_patterns() == 0) {