diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp index b351ff8e1..7c3cb1344 100644 --- a/src/sat/smt/polysat/constraints.cpp +++ b/src/sat/smt/polysat/constraints.cpp @@ -69,26 +69,33 @@ namespace polysat { return signed_constraint(ckind_t::op_t, cnstr); } - // parity p >= k if low order k bits of p are 0 + // parity(p) >= k if low order k bits of p are 0. + // Requires 0 <= k <= N. signed_constraint constraints::parity_at_least(pdd const& p, unsigned k) { + auto& m = p.manager(); + unsigned N = m.power_of_2(); + // NOTE: it is ambiguous at this point what we want for k > N: + // - as a condition, parity(p) > N is never true + // - as an implied constraint, we usually want p == 0 instead + VERIFY(k <= N); if (k == 0) - return uge(p, 0); - unsigned N = p.manager().power_of_2(); + // parity(p) >= 0 is a tautology + return eq(m.zero()); + if (k == N) + return eq(p); // parity(p) >= k // <=> p * 2^(N - k) == 0 - if (k > N) - // parity(p) > N is never true - return ~eq(p.manager().zero()); - else if (k == 0) - // parity(p) >= 0 is a tautology - return eq(p.manager().zero()); - else if (k == N) - return eq(p); - else - return eq(p * rational::power_of_two(N - k)); + return eq(p * rational::power_of_two(N - k)); } + // parity(p) <= k. + // Requires 0 <= k <= N. signed_constraint constraints::parity_at_most(pdd const& p, unsigned k) { + auto& m = p.manager(); + unsigned N = m.power_of_2(); + if (k == N) + // parity(p) <= N is a tautology + return eq(m.zero()); return ~parity_at_least(p, k + 1); } diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index 96d9e1cae..f6ad6b053 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -64,6 +64,7 @@ namespace polysat { signed_constraint() {} signed_constraint(ckind_t c, constraint* p) : m_op(c), m_constraint(p) {} signed_constraint operator~() const { signed_constraint r(*this); r.m_sign = !r.m_sign; return r; } + bool is_null() const { return m_constraint == nullptr; } bool sign() const { return m_sign; } bool is_positive() const { return !m_sign; } bool is_negative() const { return m_sign; } diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index 860b9be40..74886ba2b 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -102,7 +102,7 @@ namespace polysat { } bool monomials::eval_to_false(unsigned i) { - rational rhs, lhs; + rational rhs; auto& mon = m_monomials[i]; if (!c.try_eval(mon.var, mon.val)) return false; @@ -198,12 +198,12 @@ namespace polysat { } // parity p * q = min(N, parity(p) + parity(q)) - bool monomials::parity(monomial const& mon) { - unsigned parity_val = get_parity(mon.val, mon.num_bits()); + bool monomials::parity(monomial const& mon) { + unsigned N = mon.num_bits(); + unsigned parity_val = get_parity(mon.val, N); unsigned sum_parities = 0; - unsigned N = mon.var.manager().power_of_2(); for (unsigned j = 0; j < mon.args.size(); ++j) { - unsigned k = get_parity(mon.arg_vals[j], mon.num_bits()); + unsigned k = get_parity(mon.arg_vals[j], N); if (k > parity_val) { auto const& p = mon.args[j]; if (c.add_axiom("parity p >= i => parity p * q >= i", { ~C.parity_at_least(p, k), C.parity_at_least(mon.var, k) }, true)) @@ -218,16 +218,18 @@ namespace polysat { if (sum_parities > parity_val) { constraint_or_dependency_vector clause; for (unsigned j = 0; j < mon.args.size(); ++j) - clause.push_back(~C.parity_at_least(mon.args[j], get_parity(mon.arg_vals[j], mon.num_bits()))); - clause.push_back(C.parity_at_least(mon.var, sum_parities)); + clause.push_back(~C.parity_at_least(mon.args[j], get_parity(mon.arg_vals[j], N))); + unsigned min_var_parity = std::min(N, sum_parities); + clause.push_back(C.parity_at_least(mon.var, min_var_parity)); return c.add_axiom("N >= pp + qp, pp >= parity(p), qq >= parity(q) => parity p * q >= pp + qp)", clause, true); } // sum_parities < parity_val + SASSERT(sum_parities < N); constraint_or_dependency_vector clause; - clause.push_back(~C.parity_at_least(mon.var, sum_parities)); + clause.push_back(~C.parity_at_least(mon.var, 1 + sum_parities)); for (unsigned j = 0; j < mon.args.size(); ++j) - clause.push_back(C.parity_at_least(mon.args[j], 1 + get_parity(mon.arg_vals[j], mon.num_bits()))); - return c.add_axiom("parity(p * q) > pp + qp => pp < parity(p) or qp < parity(q))", clause, true); + clause.push_back(C.parity_at_least(mon.args[j], 1 + get_parity(mon.arg_vals[j], N))); + return c.add_axiom("parity(p * q) > pp + qp => parity(p) > pp or parity(q) > qp", clause, true); } // ~ovfl*(p,q) & q != 0 => p <= p*q @@ -374,13 +376,15 @@ namespace polysat { out << sep << p, sep = " * "; else out << sep << "(" << p << ")", sep = " * "; - out << "\n"; + // out << " arg_vals " << arg_vals; + // out << " def " << def; + // out << " val " << val; return out; } std::ostream& monomials::display(std::ostream& out) const { for (auto const& mon : m_monomials) - mon.display(out); + mon.display(out) << "\n"; return out; } } diff --git a/src/sat/smt/polysat/monomials.h b/src/sat/smt/polysat/monomials.h index 15f326c99..e4f6e4329 100644 --- a/src/sat/smt/polysat/monomials.h +++ b/src/sat/smt/polysat/monomials.h @@ -29,18 +29,19 @@ namespace polysat { constraints& C; struct monomial { - pdd_vector args; - pdd var; - pdd def; - rational_vector arg_vals; - rational val; + pdd_vector args; + pdd var; + pdd def; + rational_vector arg_vals; // values of 'args' + rational val; // value of 'var' unsigned size() const { return args.size(); } - unsigned num_bits() const { return args[0].manager().power_of_2(); } + unsigned num_bits() const { return var.manager().power_of_2(); } std::ostream& display(std::ostream& out) const; }; vector m_monomials; pdd_vector m_tmp; - + + friend std::ostream& operator<<(std::ostream& out, monomials::monomial const& mon) { return mon.display(out); } unsigned_vector m_to_refine; void init_to_refine();