diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 61c717fb4..7a68ef13d 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -374,6 +374,11 @@ namespace polysat { } } else if (v == null_var && weak_eval(sc) == l_false) { + saturation sat(*this); + if (sat(idx) == l_false) { + verbose_stream() << "Saturated conflict " << ~sc << "\n"; + return; + } auto ex = explain_weak_eval(sc); ex.push_back(dep); verbose_stream() << "infeasible propagation " << ~sc << " <- " << ex << "\n"; diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index 9b78e6a94..1a5ad68bf 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -61,21 +61,17 @@ namespace polysat { shuffle(m_to_refine.size(), m_to_refine.data(), c.rand()); if (any_of(m_to_refine, [&](auto i) { return prefix_overflow(m_monomials[i]); })) return l_false; - if (any_of(m_to_refine, [&](auto i) { return mul0(m_monomials[i]); })) return l_false; if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); })) return l_false; if (any_of(m_to_refine, [&](auto i) { return mul_parametric_inverse(m_monomials[i]); })) return l_false; - - if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); })) - return l_false; if (any_of(m_to_refine, [&](auto i) { return mul0_inverse(m_monomials[i]); })) return l_false; - if (false && any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); })) + if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); })) return l_false; - if (false && any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); })) + if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); })) return l_false; if (any_of(m_to_refine, [&](auto i) { return non_overflow_monotone(m_monomials[i]); })) return l_false; @@ -172,7 +168,6 @@ namespace polysat { } // p * q = p => parity(q - 1) + parity(p) >= N - // p * q = p & ~Ovfl(p,q) => q = 1 or p = 0 bool monomials::mul_parametric_inverse(monomial const& mon) { for (unsigned j = mon.size(); j-- > 0; ) { auto const& arg_val = mon.arg_vals[j]; @@ -197,16 +192,16 @@ namespace polysat { if (c.add_axiom("p * q = p => parity(q - 1) + parity(p) >= N", { ~C.eq(mon.var, p), ~C.parity_at_most(p, pb), C.parity_at_least(qs - 1, N - pb) }, true)) return true; } - if (c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), ~C.umul_ovfl(p, qs), C.eq(qs, 1), C.eq(p) }, true)) - return true; } } return false; } - // parity p >= i => parity p * q >= i + // 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()); + 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()); if (k > parity_val) { @@ -214,8 +209,25 @@ namespace polysat { 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)) return true; } + sum_parities += k; } - return false; + if (sum_parities == parity_val) + return false; + if (sum_parities >= N && N == parity_val) + return false; + 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)); + return c.add_axiom("N >= pp + qp, pp >= parity(p), qq >= parity(q) => parity p * q >= pp + qp)", clause, true); + } + // sum_parities < parity_val + constraint_or_dependency_vector clause; + clause.push_back(~C.parity_at_least(mon.var, 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); } // ~ovfl*(p,q) & q != 0 => p <= p*q @@ -247,21 +259,8 @@ namespace polysat { return c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true); } - // p * q = 1 => parity(p) = 0 (instance of parity(p*q) >= min(N, parity(p) + parity(q)) // ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1 bool monomials::mul1_inverse(monomial const& mon) { - if (!mon.val.is_odd()) - return false; - - unsigned j = 0; - for (auto const& val : mon.arg_vals) { - if (val.is_even()) { - if (c.add_axiom("odd(p*q) => odd(p)", - {~C.parity_at_most(mon.var, 0), C.parity_at_most(mon.args[j], 0) }, true)) - return true; - } - ++j; - } if (mon.val != 1) return false; rational product(1); @@ -288,43 +287,22 @@ namespace polysat { // p*q = 0 => parity(p) + parity(q) >= N - // TODO: update to use parity instead of overflow - // ~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0 bool monomials::mul0_inverse(monomial const& mon) { if (mon.val != 0) return false; - for (auto const& val : mon.arg_vals) - if (val == 0) - return false; - rational product(1); - for (auto const& val : mon.arg_vals) - product *= val; - if (product > mon.var.manager().max_value()) + + unsigned sum_parities = 0; + unsigned N = mon.var.manager().power_of_2(); + for (unsigned j = 0; j < mon.args.size(); ++j) + sum_parities += get_parity(mon.arg_vals[j], mon.num_bits()); + if (sum_parities >= N) return false; constraint_or_dependency_vector clause; clause.push_back(~C.eq(mon.var)); - pdd p = mon.args[0]; - for (unsigned i = 1; i < mon.args.size(); ++i) { - clause.push_back(C.umul_ovfl(p, mon.args[i])); - p *= mon.args[i]; - } - for (auto const& q : mon.args) - clause.push_back(C.eq(q)); + 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("~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0", clause, true); - } - - // parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0 - bool monomials::parity0(monomial const& mon) { - if (mon.val.is_odd()) - return false; - if (!all_of(mon.arg_vals, [&](auto const& v) { return v.is_odd(); })) - return false; - constraint_or_dependency_vector clause; - clause.push_back(~C.parity_at_least(mon.var, 1)); - for (auto const& p : mon.args) - clause.push_back(C.parity_at_least(p, 1)); - return c.add_axiom("parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0", clause, true); + return c.add_axiom("p*q = 0 & pp + qq < N => parity(p) > pp or parity(q) > qp", clause, true); } // 0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k diff --git a/src/sat/smt/polysat/monomials.h b/src/sat/smt/polysat/monomials.h index d88b80543..15f326c99 100644 --- a/src/sat/smt/polysat/monomials.h +++ b/src/sat/smt/polysat/monomials.h @@ -55,7 +55,6 @@ namespace polysat { bool non_overflow_monotone(monomial const& mon); bool mul1_inverse(monomial const& mon); bool mul0_inverse(monomial const& mon); - bool parity0(monomial const& mon); bool prefix_overflow(monomial const& mon); bool bit_blast(monomial const& mon); diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index a00faf93d..ce81a39aa 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -35,16 +35,23 @@ namespace polysat { TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"); has_conflict = true; - auto vars = c.find_conflict_variables(idx); - for (auto v : vars) - if (resolve(v, idx)) - return l_false; + if (l_false == operator()(idx)) + return l_false; } if (has_conflict) return l_undef; return l_true; } + lbool saturation::operator()(constraint_id idx) { + auto sc = c.get_constraint(idx); + auto vars = c.find_conflict_variables(idx); + for (auto v : vars) + if (resolve(v, idx)) + return l_false; + return l_undef; + } + bool saturation::resolve(pvar v, constraint_id id) { auto sc = c.get_constraint(id); if (!sc.unfold_vars().contains(v)) @@ -209,12 +216,12 @@ namespace polysat { /** * Expand the following axioms: * Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2} - * Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 2 - * Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 2 => 0x * 0y >= 2^N + * Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1 + * Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2^N * * ~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2} - * ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 2 - * ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 2 => 0x * 0y < 2^N + * ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 1 + * ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 1 => 0x * 0y < 2^N */ void saturation::try_umul_blast(umul_ovfl const& sc) { auto x = sc.p(); @@ -245,14 +252,14 @@ namespace polysat { if (sc.sign()) { // Case ~Ovfl(x,y) is asserted by current assignment x * y is overflow SASSERT(bx > 1 && by > 1); - SASSERT(bx + by >= N + 2); + SASSERT(bx + by >= N + 1); if (bx > (N + 1) / 2) { add_clause("~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}", { d, ~C.ule(x, y), C.ult(x, rational::power_of_two((N + 1) / 2)) }, true); } - else if (bx + by > N + 2) - add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k + 2", - {d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 2)}, true); + else if (bx + by > N + 1) + add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k + 1", + {d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 1)}, true); else { auto x1 = c.mk_zero_extend(1, x); auto y1 = c.mk_zero_extend(1, y); @@ -269,16 +276,16 @@ namespace polysat { add_clause("Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}", { d, ~C.ule(x, y), C.uge(x, rational::power_of_two((N + 1) / 2)) }, true); } - else if (bx + by < N + 2) { + else if (bx + by < N + 1) { SASSERT(bx <= by); - add_clause("Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 2", - { d, ~C.msb_le(x, bx), C.msb_ge(y, N - bx + 2) }, true); + add_clause("Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1", + { d, ~C.msb_le(x, bx), C.msb_ge(y, N - bx + 1) }, true); } else { auto x1 = c.mk_zero_extend(1, x); auto y1 = c.mk_zero_extend(1, y); - add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 2 => 0x * 0y >= 2 ^ N", - { d, ~C.msb_le(x, bx), ~C.msb_le(y, N - bx + 2), C.uge(x1 * y1, rational::power_of_two(N)) }, true); + add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2 ^ N", + { d, ~C.msb_le(x, bx), ~C.msb_le(y, N - bx + 1), C.uge(x1 * y1, rational::power_of_two(N)) }, true); } } } diff --git a/src/sat/smt/polysat/saturation.h b/src/sat/smt/polysat/saturation.h index 49af28275..e2d899792 100644 --- a/src/sat/smt/polysat/saturation.h +++ b/src/sat/smt/polysat/saturation.h @@ -80,5 +80,6 @@ namespace polysat { public: saturation(core& c); lbool operator()(); + lbool operator()(constraint_id id); }; }