diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index d68d3236e..8116283df 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -584,7 +584,7 @@ namespace polysat { } } } - + for (unsigned d : deps) out_deps.push_back(dependency(d)); if (!m_dep.is_null() && !deps.contains(m_dep.val())) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 41bbbb34b..f682fae09 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -812,22 +812,31 @@ namespace polysat { bool saturation::try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y) { set_rule("[x] 2^k*x = 2^k*y & x < 2^N-k => y = x or y >= 2^{N-k}"); auto& m = s.var2pdd(x); - unsigned N = m.power_of_2(); + unsigned const N = m.power_of_2(); pdd y = m.zero(); pdd a = y, b = y, a2 = y; - pdd X = s.var(x); + pdd const X = s.var(x); + // Match ax + b <= y with eval(y) = 0 if (!is_AxB_eq_0(x, axb_l_y, a, b, y)) return false; if (!a.is_val()) return false; if (!a.val().is_power_of_two()) return false; - unsigned k = a.val().trailing_zeros(); + unsigned const k = a.val().trailing_zeros(); if (k == 0) return false; + // x*2^k = b, x <= a2 < 2^{N-k} + rational const bound = rational::power_of_two(N - k); b = -b; if (b.leading_coefficient() != a.val()) return false; + pdd Y = m.zero(); + if (!b.try_div(b.leading_coefficient(), Y)) + return false; + rational Y_val; + if (!s.try_eval(Y, Y_val) || Y_val >= bound) + return false; for (auto c : core) { if (!c->is_ule()) continue; @@ -836,15 +845,9 @@ namespace polysat { continue; if (!a2.is_val()) continue; - // x*2^k = b, x <= a2 < 2^{N-k} - rational bound = rational::power_of_two(N - k); if (i.is_strict() && a2.val() >= bound) continue; if (!i.is_strict() && a2.val() > bound) - continue; - pdd Y = b.div(b.leading_coefficient()); - rational Y_val; - if (!s.try_eval(Y, Y_val) || Y_val >= bound) continue; signed_constraint le = s.ule(Y, bound - 1); m_lemma.reset(); @@ -854,7 +857,6 @@ namespace polysat { if (propagate(x, core, axb_l_y, s.eq(X, Y))) return true; } - return false; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index dfaa718a1..615c679b3 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -180,7 +180,7 @@ namespace polysat { // Input literal contradicts current boolean state (e.g., opposite literals in the input) // => conflict only flags the inconsistency set_conflict_at_base_level(dep); - m_conflict.insert(~c); // ~c is true in the solver, need to track its original dependencies + m_conflict.insert(~c); return; } m_bvars.assumption(lit, m_level, dep); diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index d7a2012e2..a5375f7dc 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -205,6 +205,7 @@ namespace bv { polysat::signed_constraint sc = a->m_sc; if (!sc) return; + force_push(); SASSERT(s().value(a->m_bv) != l_undef); bool sign = l_false == s().value(a->m_bv); sat::literal lit(a->m_bv, sign); @@ -216,6 +217,7 @@ namespace bv { bool solver::polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { if (!use_polysat()) return false; + force_push(); pdd p = var2pdd(r1); pdd q = var2pdd(r2); auto sc = m_polysat.eq(p, q); @@ -229,11 +231,13 @@ namespace bv { bool solver::polysat_diseq_eh(euf::th_eq const& ne) { if (!use_polysat()) return false; + force_push(); euf::theory_var v1 = ne.v1(), v2 = ne.v2(); pdd p = var2pdd(v1); pdd q = var2pdd(v2); auto sc = ~m_polysat.eq(p, q); sat::literal neq = ~expr2literal(ne.eq()); + TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n"); m_polysat.assign_eh(sc, polysat::dependency(1 + 2 * neq.index())); return true; } @@ -241,6 +245,7 @@ namespace bv { void solver::polysat_propagate() { if (!use_polysat()) return; + force_push(); lbool r = m_polysat.unit_propagate(); if (r == l_false) polysat_core(); @@ -249,6 +254,7 @@ namespace bv { lbool solver::polysat_final() { if (!use_polysat()) return l_true; + force_push(); lbool r = m_polysat.check_sat(); if (r == l_false) polysat_core(); @@ -268,6 +274,9 @@ namespace bv { eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2))); } } + for (auto lit : core) { + VERIFY(s().value(lit) == l_true); + } auto ex = mk_bv2ext_justification(core, eqs); ctx.set_conflict(ex); } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 9a177c0cc..c5795de0c 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -247,10 +247,10 @@ namespace bv { return; if (s().is_probing()) return; + TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";); if (polysat_diseq_eh(ne)) return; - TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";); unsigned sz = m_bits[v1].size(); if (sz == 1) return; @@ -801,6 +801,13 @@ namespace bv { return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx; case bv_justification::kind_t::bv2int: return out << "bv <- v" << v1 << " == v" << v2 << " <== " << ctx.bpp(c.a) << " == " << ctx.bpp(c.b) << " == " << ctx.bpp(c.c); + case bv_justification::kind_t::bvext: { + for (unsigned i = 0; i < c.m_num_literals; ++i) + out << c.m_literals[i] << " "; + for (unsigned i = 0; i < c.m_num_eqs; ++i) + out << ctx.bpp(c.m_eqs[i].first) << " == " << ctx.bpp(c.m_eqs[i].second) << " "; + return out << "\n"; + } default: UNREACHABLE(); break;