From 21236dc80ae409393d8a50d85f0b626c20cd2518 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jan 2024 16:20:13 -0800 Subject: [PATCH] working on viable explanations Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 5 +--- src/math/dd/dd_pdd.h | 2 +- src/sat/smt/polysat/viable.cpp | 43 ++++++++++++++++++++++++++++------ src/sat/smt/polysat/viable.h | 9 +++++-- src/sat/smt/polysat_solver.cpp | 17 +++++++------- 5 files changed, 53 insertions(+), 23 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 324cd58f0..34cd6581b 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -1860,14 +1860,11 @@ namespace dd { return (*this) * rational::power_of_two(n); } - bool pdd::has_unit(pdd& x, pdd& rest) const { - if (is_val()) - return false; + bool pdd::has_unit(pdd& x) const { pdd r = *this; while (!r.is_val()) { if (r.hi().is_one()) { x = m->mk_var(r.var()); - rest = *this - x; return true; } r = r.lo(); diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 33567a3c2..60481d272 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -441,7 +441,7 @@ namespace dd { bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); } bool is_binary() const { return m->is_binary(root); } - bool has_unit(pdd& x, pdd& rest) const; + bool has_unit(pdd& x) const; bool is_monomial() const { return m->is_monomial(root); } bool is_univariate() const { return m->is_univariate(root); } bool is_univariate_in(unsigned v) const { return m->is_univariate_in(root, v); } diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 0eff9973d..1bed9fdf7 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -84,6 +84,7 @@ namespace polysat { } find_t viable::find_viable(pvar v, rational& lo) { + verbose_stream() << "find viable v" << v << " starting with " << lo << "\n"; rational hi; switch (find_viable(v, lo, hi)) { case l_true: @@ -103,7 +104,9 @@ namespace polysat { lbool viable::find_viable(pvar v, rational& val1, rational& val2) { m_explain.reset(); + m_ineqs.reset(); m_var = v; + m_value = nullptr; m_num_bits = c.size(v); m_fixed_bits.reset(v); init_overlaps(v); @@ -128,6 +131,9 @@ namespace polysat { } else val2 = val1 + 1; + + // instead of m_value use linked list of entries? + m_value = alloc(pdd, c.value(val2, m_num_bits)); r = next_viable(val2); @@ -231,14 +237,29 @@ namespace polysat { break; // TODO check if admitted: layer.entries = e; m_explain.push_back(e); + if (e->interval.is_full()) - return l_false; - auto hi = e->interval.hi_val(); - if (wrapped && start <= hi) - return l_false; - if (hi < e->interval.lo_val()) + return l_false; + + auto hi_val = e->interval.hi_val(); + auto lo_val = e->interval.lo_val(); + auto hi = e->interval.hi(); + auto lo = e->interval.lo(); + + + if (!m_value) + m_value = alloc(pdd, lo); + + m_ineqs.push_back({ *m_value, lo, hi }); + + if (wrapped && start <= hi_val) { + verbose_stream() << "WRAPPED\n"; + return l_false; + } + if (hi_val < lo_val) wrapped = true; - val1 = hi; + val1 = hi_val; + m_value = alloc(pdd, hi); SASSERT(val1 < p2b); } SASSERT(val1 < p2b); @@ -533,10 +554,17 @@ namespace polysat { result.push_back(offset_claim(m_var, {e->var, 0})); seen.insert(index.id); for (auto const& sc : e->side_cond) - result.push_back(c.propagate(sc, c.explain_eval(sc))); + result.push_back(c.propagate(sc, c.explain_eval(sc))); auto const& [sc, d, value] = c.m_constraint_index[index.id]; result.push_back(d); } + for (auto [t, lo, hi] : m_ineqs) { + auto sc = cs.ult(t - lo, hi - lo); + verbose_stream() << "Overlap " << t << " in [" << lo << ", " << hi << "[: " << sc << "\n"; + if (!sc.is_always_true()) + result.push_back(c.propagate(sc, c.explain_eval(sc))); + } + result.append(m_fixed_bits.explain()); TRACE("bv", tout << "viable-explain v" << m_var << " - " << result.size() << "\n"); return result; @@ -656,6 +684,7 @@ namespace polysat { } if (ne->interval.is_full()) { m_explain.reset(); + m_ineqs.reset(); m_explain.push_back(ne); m_fixed_bits.reset(); m_var = v; diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index e3715b4d5..c988d9111 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -85,11 +85,15 @@ namespace polysat { entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; } }; - + // short for t in [lo,hi[ + struct interval_member { + pdd t, lo, hi; + }; ptr_vector m_alloc; vector m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order ptr_vector m_equal_lin; // entries that have non-unit multipliers, but are equal - ptr_vector m_diseq_lin; // entries that have distinct non-zero multipliers + ptr_vector m_diseq_lin; // entries that have distinct non-zero multipliers + vector m_ineqs; // inequalities to justify that values are not viable. ptr_vector m_explain; // entries that explain the current propagation or conflict bool well_formed(entry* e); @@ -126,6 +130,7 @@ namespace polysat { bool refine_equal_lin(pvar v, rational const& val); pvar m_var = null_var; + scoped_ptr m_value; // the current symbolid value being checked for viability. unsigned m_num_bits = 0; fixed_bits m_fixed_bits; offset_slices m_overlaps; diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 090876ef6..61e6ecd48 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -383,25 +383,24 @@ namespace polysat { expr_ref solver::constraint2expr(signed_constraint const& sc) { expr_ref result(m); switch (sc.op()) { - case ckind_t::ule_t: { - + case ckind_t::ule_t: { auto p = sc.to_ule().lhs(); auto q = sc.to_ule().rhs(); - pdd x = p, r = p; - if (q.is_zero() && p.has_unit(x, r)) { + pdd x = p; + if (q.is_zero() && p.has_unit(x)) { auto l = pdd2expr(x); - auto h = pdd2expr(-r); - result = m.mk_eq(l, h); + auto r = pdd2expr(x - p); + result = m.mk_eq(l, r); } else { auto l = pdd2expr(p); - auto h = pdd2expr(q); + auto r = pdd2expr(q); if (p == q) result = m.mk_true(); else if (q.is_zero()) - result = m.mk_eq(l, h); + result = m.mk_eq(l, r); else - result = bv.mk_ule(l, h); + result = bv.mk_ule(l, r); } if (sc.sign()) result = m.mk_not(result);