From 1e9381c2f67b278d80d3233dec81c482cf632ee0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Mar 2024 11:48:09 -0700 Subject: [PATCH] update slice/offset claim structures to allow for equal variable. Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/monomials.cpp | 12 ++++++------ src/sat/smt/polysat/types.h | 32 +++++++++++++++++-------------- src/sat/smt/polysat/viable.cpp | 12 ++++++------ src/sat/smt/polysat_egraph.cpp | 12 +++++++++++- src/sat/smt/polysat_solver.cpp | 4 ++-- 5 files changed, 43 insertions(+), 29 deletions(-) diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index 1a5ad68bf..6f4f9c18c 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -324,27 +324,27 @@ namespace polysat { c.get_bitvector_suffixes(x, x_suffixes); rational x_val, y_val; for (auto const& xslice : x_suffixes) { - if (c.size(xslice.v) == mon.num_bits()) + if (c.size(xslice.child) == mon.num_bits()) continue; - auto const& xmax_value = c.var(xslice.v).manager().max_value(); + auto const& xmax_value = c.var(xslice.child).manager().max_value(); if (mon.val <= xmax_value) continue; - if (!c.try_eval(c.var(xslice.v), x_val) || x_val != mon.arg_vals[0]) + if (!c.try_eval(c.var(xslice.child), x_val) || x_val != mon.arg_vals[0]) continue; if (!y_computed) c.get_bitvector_suffixes(y, y_suffixes); y_computed = true; for (auto const& yslice : y_suffixes) { - if (c.size(yslice.v) != c.size(xslice.v)) + if (c.size(yslice.child) != c.size(xslice.child)) continue; - if (!c.try_eval(c.var(yslice.v), y_val) || y_val != mon.arg_vals[1]) + if (!c.try_eval(c.var(yslice.child), y_val) || y_val != mon.arg_vals[1]) continue; bool added = c.add_axiom("0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k", { dependency({x, xslice}), dependency({y, yslice}), ~C.ule(mon.args[0], xmax_value), ~C.ule(mon.args[1], xmax_value), ~C.ugt(mon.var, xmax_value), - C.umul_ovfl(c.var(xslice.v), c.var(yslice.v)) }, + C.umul_ovfl(c.var(xslice.child), c.var(yslice.child)) }, true); if (added) return true; diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 6a5be5834..b749045e5 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -36,34 +36,37 @@ namespace polysat { class signed_constraint; struct fixed_slice { + pvar child; unsigned offset = 0; unsigned length = 0; rational value; fixed_slice() = default; - fixed_slice(rational value, unsigned offset, unsigned length) : offset(offset), length(length), value(std::move(value)) {} + fixed_slice(pvar child, rational value, unsigned offset, unsigned length) : + child(child), offset(offset), length(length), value(std::move(value)) {} unsigned end() const { return offset + length; } }; struct fixed_claim : public fixed_slice { - pvar v; + pvar parent; fixed_claim() = default; - fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(std::move(value), offset, length), v(v) {} - fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), v(v) {} + fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(child, std::move(value), offset, length), parent(v) {} + fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), parent(v) {} }; struct offset_slice { - pvar v; + pvar child; unsigned offset; offset_slice() = default; - offset_slice(pvar v, unsigned offset) : v(v), offset(offset) {} + offset_slice(pvar v, unsigned offset) : child(v), offset(offset) {} }; struct offset_claim : public offset_slice { - pvar w; + pvar parent; offset_claim() = default; - offset_claim(pvar w, offset_slice const& s) : offset_slice(s), w(w) {} + offset_claim(pvar w, offset_slice const& s) : offset_slice(s), parent(w) {} }; + class dependency { struct axiom_t {}; std::variant m_data; @@ -99,11 +102,11 @@ namespace polysat { return out << "tv" << d.eq().first << " == tv" << d.eq().second; else if (d.is_offset_claim()) { auto offs = d.offset(); - return out << "v" << offs.v << " == v" << offs.w << " offset " << offs.offset; + return out << "v" << offs.child << " == v" << offs.parent << " offset " << offs.offset; } else if (d.is_fixed_claim()) { auto fixed = d.fixed(); - return out << fixed.value << " == v" << fixed.v << " [" << fixed.length << "]@" << fixed.offset; + return out << fixed.value << " == v" << fixed.parent << " [" << fixed.length << "]@" << fixed.offset; } else { UNREACHABLE(); @@ -115,8 +118,8 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) { if (js.offset == 0) - return out << "v" << js.v; - return out << "v" << js.v << " at offset " << js.offset; + return out << "v" << js.child; + return out << "v" << js.child << " at offset " << js.offset; } using fixed_bits_vector = vector; @@ -125,8 +128,8 @@ namespace polysat { unsigned level = 0; // level when sub-slice was fixed to value dependency dep = null_dependency; fixed_slice_extra() = default; - fixed_slice_extra(rational value, unsigned offset, unsigned length, unsigned level, dependency dep): - fixed_slice(std::move(value), offset, length), level(level), dep(std::move(dep)) {} + fixed_slice_extra(rational value, unsigned offset, unsigned length, unsigned level, dependency dep) : + fixed_slice(child, std::move(value), offset, length), level(level), dep(std::move(dep)) {} }; using fixed_slice_extra_vector = vector; @@ -137,6 +140,7 @@ namespace polysat { }; using offset_slice_extra_vector = vector; + using dependency_vector = vector; using constraint_or_dependency = std::variant; using constraint_id_or_constraint = std::variant; diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 178b35238..b21a203a2 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -154,7 +154,7 @@ namespace polysat { void viable::init_overlaps(pvar v) { m_overlaps.reset(); c.get_bitvector_suffixes(v, m_overlaps); - std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) < c.size(y.v); }); + std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.child) < c.size(y.child); }); } @@ -683,7 +683,7 @@ namespace polysat { // e.g., prefers constant 'c' if we have pvars for both 'c' and 'concat(c,...)' std::sort(subslices.begin(), subslices.end(), [&](auto const& a, auto const& b) -> bool { return a.level > b.level - || (a.level == b.level && c.size(a.v) < c.size(b.v)); + || (a.level == b.level && c.size(a.child) < c.size(b.child)); }); for (auto const& slice : subslices) @@ -693,7 +693,7 @@ namespace polysat { } dependency viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_slice_extra_vector const& fixed, offset_slice_extra const& slice) { - pvar w = slice.v; + pvar w = slice.child; unsigned offset = slice.offset; unsigned w_level = slice.level; // level where value of w was fixed if (w == m_var) @@ -1496,9 +1496,9 @@ namespace polysat { std::ostream& viable::display_state(std::ostream& out) const { out << "v" << m_var << ":"; for (auto const& slice : m_overlaps) { - out << " v" << slice.v << ":" << c.size(slice.v) << "@" << slice.offset; - if (c.is_assigned(slice.v)) - out << " value=" << c.get_assignment().value(slice.v); + out << " v" << slice.child << ":" << c.size(slice.child) << "@" << slice.offset; + if (c.is_assigned(slice.child)) + out << " value=" << c.get_assignment().value(slice.child); } out << "\n"; return out; diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index 9fe1eb410..e1489bef2 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -115,7 +115,7 @@ namespace polysat { unsigned length = bv.get_bv_size(r->get_expr()); rational value; VERIFY(bv.is_numeral(r->get_expr(), value)); - out.push_back({ fixed_slice(value, offset, length) }); + out.push_back({ fixed_slice(null_var, value, offset, length) }); return false; }; @@ -186,6 +186,10 @@ namespace polysat { m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq); } + // + // explain that pv contains a fixed sub-slice at offset/length + // in addition, if slice.child is not null_var, then explain that + // void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function const& consume_eq) { euf::theory_var v = m_pddvar2var[pv]; expr_ref val(bv.mk_numeral(slice.value, slice.length), m); @@ -197,6 +201,12 @@ namespace polysat { SASSERT(b); m_bv_plugin->explain_slice(var2enode(v), slice.offset, b, consume_eq); + + if (slice.child != null_var) { + auto c = var2enode(m_pddvar2var[slice.child]); + if (b != c) + m_bv_plugin->explain_slice(b, 0, c, consume_eq); + } } } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 5a20737d0..3798be21a 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -148,11 +148,11 @@ namespace polysat { } else if (d.is_fixed_claim()) { auto const& o = d.fixed(); - explain_fixed(o.v, o, consume); + explain_fixed(o.parent, o, consume); } else if (d.is_offset_claim()) { auto const& offs = d.offset(); - explain_slice(offs.v, offs.w, offs.offset, consume); + explain_slice(offs.child, offs.parent, offs.offset, consume); } else { auto const [v1, v2] = d.eq();