diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 630d92d35..857ddff04 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -203,7 +203,11 @@ namespace polysat { } signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) { - return { dedup(alloc(ule_constraint, *this, a, b)), true }; + bool is_positive = true; + pdd lhs = a; + pdd rhs = b; + ule_constraint::simplify(is_positive, lhs, rhs); + return { dedup(alloc(ule_constraint, *this, lhs, rhs)), is_positive }; } signed_constraint constraint_manager::eq(pdd const& p) { @@ -215,18 +219,12 @@ namespace polysat { } bool signed_constraint::is_eq() const { - if (is_positive()) - return m_constraint->is_eq(); - else - return m_constraint->is_diseq(); + return is_positive() && m_constraint->is_eq(); } pdd const& signed_constraint::eq() const { SASSERT(is_eq()); - if (is_positive()) - return m_constraint->to_ule().lhs(); - else - return m_constraint->to_ule().rhs(); + return m_constraint->to_ule().lhs(); } /** diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 3b63bbdcf..fbc0c8a26 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -106,8 +106,8 @@ namespace polysat { signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r); signed_constraint band(pdd const& p, pdd const& q, pdd const& r); - constraint *const* begin() const { return m_constraints.data(); } - constraint *const* end() const { return m_constraints.data() + m_constraints.size(); } + constraint* const* begin() const { return m_constraints.data(); } + constraint* const* end() const { return m_constraints.data() + m_constraints.size(); } using clause_iterator = decltype(m_clauses)::const_iterator; clause_iterator clauses_begin() const { return m_clauses.begin(); } @@ -167,7 +167,6 @@ namespace polysat { bool operator!=(constraint const& other) const { return !operator==(other); } virtual bool is_eq() const { return false; } - virtual bool is_diseq() const { return false; } bool is_ule() const { return m_kind == ckind_t::ule_t; } bool is_umul_ovfl() const { return m_kind == ckind_t::umul_ovfl_t; } bool is_smul_fl() const { return m_kind == ckind_t::smul_fl_t; } diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index a0024c9ec..07651d459 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -12,15 +12,30 @@ Author: Notes: + Canonical representation of equation p == 0 is the constraint p <= 0. + The alternatives p < 1, -1 <= q, q > -2 are eliminated. + Rewrite rules to simplify expressions. In the following let k, k1, k2 be values. - - k1 <= k2 ==> 0 <= 0 if k1 <= k2 - - k1 <= k2 ==> 1 <= 0 if k1 > k2 - - 0 <= p ==> 0 <= 0 - - p <= -1 ==> 0 <= 0 - - k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2. - - k <= p ==> p - k <= - k - 1 + - k1 <= k2 ==> 0 <= 0 if k1 <= k2 + - k1 <= k2 ==> 1 <= 0 if k1 > k2 + - 0 <= p ==> 0 <= 0 + - p <= 0 ==> 1 <= 0 if p is never zero due to parity + - p <= -1 ==> 0 <= 0 + - k <= p ==> p - k <= - k - 1 + - k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2. + + Note: the rules will rewrite alternative formulations of equations: + - -1 <= p ==> p + 1 <= 0 + - 1 <= p ==> p - 1 <= -2 + + Rewrite rules on signed constraints: + + - p > -2 ==> p + 1 <= 0 + - p <= -2 ==> p + 1 > 0 + + At this point, all equations are in canonical form. TODO: clause simplifications: @@ -44,72 +59,97 @@ Note: #include "math/polysat/solver.h" #include "math/polysat/log.h" +namespace { + using namespace polysat; + + // Simplify lhs <= rhs + void simplify_impl(bool& is_positive, pdd& lhs, pdd& rhs) { + // 0 <= p --> 0 <= 0 + if (lhs.is_zero()) { + rhs = 0; + return; + } + // p <= -1 --> 0 <= 0 + if (rhs.is_val() && rhs.val() == rhs.manager().max_value()) { + lhs = 0, rhs = 0; + return; + } + // p <= p --> 0 <= 0 + if (lhs == rhs) { + lhs = 0, rhs = 0; + return; + } + // Evaluate constants + if (lhs.is_val() && rhs.is_val()) { + if (lhs.val() <= rhs.val()) + lhs = 0, rhs = 0; + else + lhs = 1, rhs = 0; + return; + } + // k <= p --> p - k <= - k - 1 + if (lhs.is_val()) { + pdd k = lhs; + lhs = rhs - k; + rhs = - k - 1; + } + // p > -2 --> p + 1 <= 0 + // p <= -2 --> p + 1 > 0 + if (rhs.is_val() && (rhs + 2).is_zero()) { + lhs = lhs + 1; + rhs = 0; + is_positive = !is_positive; + } + // 2p + 1 <= 0 --> 1 <= 0 + if (rhs.is_zero() && lhs.is_never_zero()) { + lhs = 1; + return; + } + // a*p + q <= 0 --> p + a^-1*q <= 0 for a odd + if (rhs.is_zero() && !lhs.leading_coefficient().is_power_of_two()) { + rational lc = lhs.leading_coefficient(); + rational x, y; + gcd(lc, lhs.manager().two_to_N(), x, y); + if (x.is_neg()) + x = mod(x, lhs.manager().two_to_N()); + lhs *= x; + SASSERT(lhs.leading_coefficient().is_power_of_two()); + } + } // simplify_impl +} + + namespace polysat { ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) : constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) { -#ifndef NDEBUG - pdd const old_lhs = m_lhs; - pdd const old_rhs = m_rhs; -#endif - simplify(); -#ifndef NDEBUG - if (old_lhs != m_lhs || old_rhs != m_rhs) - LOG("Simplify: " << ule_pp(l_true, old_lhs, old_rhs) << " --> " << ule_pp(l_true, m_lhs, m_rhs)); -#endif - m_vars.append(m_lhs.free_vars()); for (auto v : m_rhs.free_vars()) if (!m_vars.contains(v)) m_vars.push_back(v); - } - void ule_constraint::simplify() { - if (m_lhs.is_zero()) { - m_rhs = 0; - return; - } - if (m_rhs.is_val() && m_rhs.val() == m_rhs.manager().max_value()) { - m_lhs = 0, m_rhs = 0; - return; - } - if (m_lhs == m_rhs) { - m_lhs = m_rhs = 0; - return; - } - if (m_lhs.is_val() && m_rhs.is_val()) { - if (m_lhs.val() <= m_rhs.val()) - m_lhs = m_rhs = 0; - else - m_lhs = 1, m_rhs = 0; - return; - } - // k <= p --> p - k <= - k - 1 - if (m_lhs.is_val()) { - pdd k = m_lhs; - m_lhs = m_rhs - k; - m_rhs = - k - 1; - } - // a*p + q <= 0 <=> p + a^-1*q <= 0 for a odd - if (m_rhs.is_zero() && !m_lhs.leading_coefficient().is_power_of_two()) { - rational lc = m_lhs.leading_coefficient(); - rational x, y; - gcd(lc, m_lhs.manager().two_to_N(), x, y); - if (x.is_neg()) - x = mod(x, m_lhs.manager().two_to_N()); - m_lhs *= x; - SASSERT(m_lhs.leading_coefficient().is_power_of_two()); + void ule_constraint::simplify(bool& is_positive, pdd& lhs, pdd& rhs) { +#ifndef NDEBUG + bool const old_is_positive = is_positive; + pdd const old_lhs = lhs; + pdd const old_rhs = rhs; +#endif + simplify_impl(is_positive, lhs, rhs); +#ifndef NDEBUG + if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) { + ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs); + ule_pp const new_ule(to_lbool(is_positive), lhs, rhs); + LOG("Simplify: " << old_ule << " --> " << new_ule); } +#endif } std::ostream& ule_constraint::display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs) { out << lhs; if (rhs.is_zero() && status == l_true) out << " == "; else if (rhs.is_zero() && status == l_false) out << " != "; - // else if (lhs.is_one() && status == l_true) out << " != "; - // else if (lhs.is_one() && status == l_false) out << " == "; else if (status == l_true) out << " <= "; else if (status == l_false) out << " > "; else out << " <=/> "; @@ -149,6 +189,7 @@ namespace polysat { } bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { + // NOTE: don't assume simplifications here because we also call this on partially substituted constraints if (is_positive) { // lhs <= rhs if (rhs.is_zero()) @@ -199,7 +240,6 @@ namespace polysat { return p.is_val() && q.is_val() && p.val() > q.val(); } - inequality ule_constraint::as_inequality(bool is_positive) const { if (is_positive) return inequality(lhs(), rhs(), false, this); diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 4fb518efb..71cf98f4e 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -26,7 +26,7 @@ namespace polysat { pdd m_rhs; ule_constraint(constraint_manager& m, pdd const& l, pdd const& r); - void simplify(); + static void simplify(bool& is_positive, pdd& lhs, pdd& rhs); public: ~ule_constraint() override {} @@ -46,7 +46,6 @@ namespace polysat { unsigned hash() const override; bool operator==(constraint const& other) const override; bool is_eq() const override { return m_rhs.is_zero(); } - bool is_diseq() const override { return m_lhs.is_one(); } void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; };