From aa1285288eb295ec5a6af3175d2e64fff5724ce6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 15 Mar 2024 15:08:12 +0100 Subject: [PATCH] Fix integration of propagate_from_containing_slice --- src/sat/smt/polysat/core.cpp | 8 +-- src/sat/smt/polysat/types.h | 31 ++++++++-- src/sat/smt/polysat/viable.cpp | 109 ++++++++++++++++++++++++--------- src/sat/smt/polysat/viable.h | 26 ++++---- src/sat/smt/polysat_egraph.cpp | 11 +++- src/sat/smt/polysat_solver.cpp | 8 ++- 6 files changed, 137 insertions(+), 56 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 7a68ef13d..23cdcc24c 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -387,11 +387,11 @@ namespace polysat { } void core::propagate_assignment(pvar v, rational const& value, dependency dep) { - TRACE("bv", tout << "propagate assignment v" << v << " := " << value << "\n"); + TRACE("bv", tout << "propagate assignment v" << v << " := " << value << " justified by " << dep << "\n"); + // verbose_stream() << "propagate assignment v" << v << " := " << value << " justified by " << dep << "\n"; SASSERT(!is_assigned(v)); - if (!m_viable.assign(v, value)) { + if (!m_viable.assign(v, value, dep)) { auto deps = m_viable.explain(); - deps.push_back(dep); verbose_stream() << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n"; s.set_conflict(deps, "non-viable assignment"); return; @@ -532,7 +532,7 @@ namespace polysat { }; auto& value = m_constraint_index[index.id].value; - TRACE("bv", tout << "assignment " << index.id << " " << m_constraint_index[index.id].sc << " := " << value << " sign: " << sign << "\n"); + TRACE("bv", tout << "assignment cid=" << index.id << " " << m_constraint_index[index.id].sc << " := " << value << " sign: " << sign << "\n"); if (value != l_undef && ((value == l_false && !sign) || (value == l_true && sign))) { diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 8f414b13e..126bba541 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -17,11 +17,17 @@ Author: #include "util/trail.h" #include "util/sat_literal.h" +namespace euf { + class enode; +} + namespace polysat { using pdd = dd::pdd; using pvar = unsigned; using theory_var = int; + using enode_pair = std::pair; + struct constraint_id { unsigned id = UINT_MAX; bool is_null() const { return id == UINT_MAX; } @@ -60,6 +66,8 @@ namespace polysat { offset_slice(pvar child, unsigned offset) : child(child), offset(offset) {} }; + // parent[X:offset] = child + // where X = offset + size(child) - 1 struct offset_claim : public offset_slice { pvar parent; offset_claim() = default; @@ -69,22 +77,25 @@ namespace polysat { class dependency { struct axiom_t {}; - std::variant m_data; + std::variant m_data; dependency(): m_data(axiom_t()) {} public: dependency(sat::bool_var v) : m_data(v){} - dependency(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {} + dependency(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {} + dependency(euf::enode* n1, euf::enode* n2) : m_data(std::make_pair(n1, n2)) {} dependency(offset_claim const& c) : m_data(c) {} dependency(fixed_claim const& c): m_data(c) {} static dependency axiom() { return dependency(); } bool is_null() const { return is_bool_var() && *std::get_if(&m_data) == sat::null_bool_var; } bool is_axiom() const { return std::holds_alternative(m_data); } bool is_eq() const { return std::holds_alternative(m_data); } + bool is_enode_eq() const { return std::holds_alternative(m_data); } bool is_bool_var() const { return std::holds_alternative(m_data); } bool is_offset_claim() const { return std::holds_alternative(m_data); } bool is_fixed_claim() const { return std::holds_alternative(m_data); } sat::bool_var bool_var() const { SASSERT(is_bool_var()); return *std::get_if(&m_data); } theory_var_pair eq() const { SASSERT(is_eq()); return *std::get_if(&m_data); } + enode_pair enode_eq() const { SASSERT(is_enode_eq()); return *std::get_if(&m_data); } offset_claim offset() const { return *std::get_if(&m_data); } fixed_claim fixed() const { return *std::get_if(&m_data); } }; @@ -100,6 +111,8 @@ namespace polysat { return out << d.bool_var(); else if (d.is_eq()) return out << "tv" << d.eq().first << " == tv" << d.eq().second; + else if (d.is_enode_eq()) + return out << "enode " << d.enode_eq().first << " == enode " << d.enode_eq().second; else if (d.is_offset_claim()) { auto offs = d.offset(); return out << "v" << offs.child << " == v" << offs.parent << " offset " << offs.offset; @@ -125,6 +138,10 @@ namespace polysat { using fixed_bits_vector = vector; struct fixed_slice_extra : public fixed_slice { + // pvar child; + // unsigned offset = 0; + // unsigned length = 0; + // rational value; unsigned level = 0; // level when sub-slice was fixed to value dependency dep = null_dependency; fixed_slice_extra() = default; @@ -134,9 +151,13 @@ namespace polysat { using fixed_slice_extra_vector = vector; struct offset_slice_extra : public offset_slice { - unsigned level = 0; // level when variable was fixed to value + // pvar child; + // unsigned offset; + unsigned level = 0; // level when child was fixed to value + dependency dep = null_dependency; // justification for fixed value + rational value; // fixed value of child offset_slice_extra() = default; - offset_slice_extra(pvar child, unsigned offset, unsigned level) : offset_slice(child, offset), level(level) {} + offset_slice_extra(pvar child, unsigned offset, unsigned level, dependency dep, rational value) : offset_slice(child, offset), level(level), dep(std::move(dep)), value(std::move(value)) {} }; using offset_slice_extra_vector = vector; @@ -172,7 +193,7 @@ namespace polysat { virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0; virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice) = 0; virtual void get_fixed_sub_slices(pvar v, fixed_slice_extra_vector& fixed_slice, offset_slice_extra_vector& subslices) = 0; - virtual pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) = 0; + virtual pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) = 0; virtual pdd mk_zero_extend(unsigned sz, pdd const& p) = 0; virtual unsigned level(dependency const& d) = 0; }; diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index cd8a5f03b..0b2eb07a5 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -83,12 +83,13 @@ namespace polysat { return e; } - bool viable::assign(pvar v, rational const& value) { + bool viable::assign(pvar v, rational const& value, dependency dep) { m_var = v; m_explain_kind = explain_t::none; m_num_bits = c.size(v); m_fixed_bits.init(v); m_explain.reset(); + m_assign_dep = null_dependency; init_overlaps(v); bool first = true; while (true) { @@ -99,6 +100,7 @@ namespace polysat { continue; m_explain.push_back({ e, value }); m_explain_kind = explain_t::assignment; + m_assign_dep = dep; return false; } } @@ -124,6 +126,7 @@ namespace polysat { m_fixed_bits.init(v); init_overlaps(v); m_explain_kind = explain_t::none; + m_assign_dep = null_dependency; for (unsigned rounds = 0; rounds < 10; ) { entry* n = find_overlap(lo); @@ -558,9 +561,9 @@ namespace polysat { } /* - * Explain why the current variable is not viable or - * or why it can only have a single value. - */ + * Explain why the current variable is not viable or + * or why it can only have a single value. + */ dependency_vector viable::explain() { dependency_vector result; auto last = m_explain.back(); @@ -635,20 +638,32 @@ namespace polysat { if (m_explain_kind == explain_t::assignment) { // there is just one entry SASSERT(m_explain.size() == 1); + SASSERT(!m_assign_dep.is_null()); explain_entry(last.e); // assignment conflict and propagation from containing slice depends on concrete values, // so we also need the evaluations of linear terms + SASSERT(!c.is_assigned(m_var)); // assignment of m_var is justified by m_assign_dep auto index = last.e->constraint_index; if (!index.is_null()) result.append(c.explain_weak_eval(c.get_constraint(index))); - auto exp = propagate_from_containing_slice(last.e, last.value, result); - // verbose_stream() << "exp is " << exp << "\n"; - if (!exp.is_null()) { - result.clear(); - result.push_back(exp); - } + // 'result' so far contains explanation for entry and its weak evaluation + switch (propagate_from_containing_slice(last.e, last.value, result)) { + case l_true: + // propagated interval onto subslice + result = m_containing_slice_deps; + break; + case l_false: + // conflict (projected interval is full) + result = m_containing_slice_deps; + break; + case l_undef: + // unable to propagate interval to containing slice + // fallback explanation uses assignment of m_var + result.push_back(m_assign_dep); + break; + }; } unmark(); if (c.inconsistent()) @@ -656,20 +671,32 @@ namespace polysat { return result; } - dependency viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps) { + /* + * l_true: successfully projected interval onto subslice + * l_false: also successfully projected interval onto subslice, resulted in full interval + * l_undef: failed + * + * In case of l_true/l_false, conflict will be in m_containing_slice_deps. + */ + lbool viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps) { verbose_stream() << "\n\n\n\n\n\nNon-viable assignment for v" << m_var << " size " << c.size(m_var) << "\n"; display_one(verbose_stream() << "entry: ", e) << "\n"; verbose_stream() << "value " << value << "\n"; + // verbose_stream() << "m_overlaps " << m_overlaps << "\n"; m_fixed_bits.display(verbose_stream() << "fixed: ") << "\n"; + // TODO: each of subslices corresponds to one in fixed, but may occur with different pvars + // for each offset/length with pvar we need to do the projection only once. fixed_slice_extra_vector fixed; offset_slice_extra_vector subslices; c.s.get_fixed_sub_slices(m_var, fixed, subslices); // TODO: move into m_fixed bits? + TRACE("bv", c.display(tout)); + // this case occurs if e-graph merges e.g. nodes "x - 2" and "3"; // polysat will see assignment "x = 5" but no fixed bits if (subslices.empty()) - return null_dependency; + return l_undef; unsigned max_level = 0; for (auto const& slice : subslices) @@ -688,19 +715,19 @@ namespace polysat { }); for (auto const& slice : subslices) - if (auto d = propagate_from_containing_slice(e, value, e_deps, fixed, slice); !d.is_null()) - return d; - return null_dependency; + if (auto r = propagate_from_containing_slice(e, value, e_deps, fixed, slice); r != l_undef) + return r; + return l_undef; } - 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) { + lbool 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.child; unsigned offset = slice.offset; unsigned w_level = slice.level; // level where value of w was fixed if (w == m_var) - return null_dependency; + return l_undef; if (w == e->var) - return null_dependency; + return l_undef; // verbose_stream() << "v" << m_var << " size " << c.size(m_var) << ", v" << w << " size " << c.size(w) << " offset " << offset << " level " << w_level << "\n"; @@ -725,7 +752,7 @@ namespace polysat { // wwwwwwwww unsigned const v_sz = e->bit_width; if (offset >= v_sz) - return null_dependency; + return l_undef; unsigned const w_sz = c.size(w); unsigned const z_sz = offset; @@ -744,9 +771,8 @@ namespace polysat { verbose_stream() << "propagate interval " << v_ivl << " from v" << m_var << " to v" << w << "[" << y_sz << "]" << "\n"; }); - dependency_vector deps; - deps.append(e_deps); // explains e - deps.push_back(offset_claim{m_var, slice}); // explains m_var[...] = w + dependency_vector& deps = m_containing_slice_deps; + deps.reset(); r_interval ivl = v_ivl; @@ -756,6 +782,8 @@ namespace polysat { while (remaining_x_sz > 0 && !ivl.is_empty() && !ivl.is_full()) { unsigned remaining_x_end = remaining_x_sz + x_off; // find next fixed slice (prefer lower level) + // sort fixed claims by bound (upper: decreasing, lower: increasing), then by merge-level (prefer lower merge level), ignore merge level higher than var? (or just max?) + // note that we might choose multiple overlapping ones, if they allow to make more progress? fixed_slice_extra best; unsigned best_end = 0; SASSERT(best_end < x_off); // because y_sz != 0 @@ -819,7 +847,7 @@ namespace polysat { } if (ivl.is_empty()) - return null_dependency; + return l_undef; // chop off z-part unsigned remaining_z_sz = z_sz; @@ -886,24 +914,44 @@ namespace polysat { } if (ivl.is_empty()) - return null_dependency; + return l_undef; IF_VERBOSE(3, { verbose_stream() << "=> v" << w << "[" << y_sz << "] not in " << ivl << "\n"; }); + deps.append(e_deps); // explains e + deps.push_back(offset_claim{m_var, slice}); // explains m_var[...] = w + if (ivl.is_full()) { - pdd zero = c.var2pdd(m_var).zero(); - auto sc = cs.ult(zero, zero); // false - return c.propagate(sc, deps, "propagate from containing slice (conflict)"); + // deps is a conflict + return l_false; } else { // proper interval - auto sc = ~cs.ult(w_shift * (c.var(w) - ivl.lo()), w_shift * (ivl.hi() - ivl.lo())); - return c.propagate(sc, deps, "propagate from containing slice"); + SASSERT(ivl.is_proper() && !ivl.is_empty()); + // deps => 2^w_shift w not in ivl + signed_constraint sc = ~cs.ult(w_shift * (c.var(w) - ivl.lo()), w_shift * (ivl.hi() - ivl.lo())); + dependency d = c.propagate(sc, deps, "propagate from containing slice"); + + verbose_stream() << "v" << w << " value " << slice.value << "\n"; + verbose_stream() << "v" << w << " value-dep " << slice.dep << "\n"; + + if (ivl.contains(slice.value)) { + // the conflict is projected interval + fixed value + deps.reset(); + deps.push_back(d); + deps.push_back(slice.dep); + return l_true; + } + else { + // interval propagation worked but it doesn't conflict the currently assigned value + // TODO: also skip propagation of the signed constraint in this case? + return l_undef; + } } - return null_dependency; + return l_undef; } @@ -1120,6 +1168,7 @@ namespace polysat { } // verbose_stream() << "v" << v << " " << sc << " " << ne->interval << "\n"; + TRACE("bv", tout << "v" << v << " " << sc << " " << ne->interval << "\n"; display_one(tout, ne) << "\n"); if (ne->interval.is_currently_empty()) { m_alloc.push_back(ne); diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index a9f054926..4cff7f195 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -115,8 +115,10 @@ namespace polysat { bool intersect(pvar v, entry* e); - dependency propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps); - dependency 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); + lbool propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps); + lbool 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); + dependency_vector m_containing_slice_deps; + static r_interval chop_off_upper(r_interval const& i, unsigned Ny, unsigned Nz, rational const* y_fixed_value = nullptr); static r_interval chop_off_lower(r_interval const& i, unsigned Ny, unsigned Nz, rational const* z_fixed_value = nullptr); @@ -149,6 +151,7 @@ namespace polysat { pvar m_var = null_var; explain_t m_explain_kind = explain_t::none; + dependency m_assign_dep = null_dependency; unsigned m_num_bits = 0; fixed_bits m_fixed_bits; offset_slices m_overlaps; @@ -167,25 +170,24 @@ namespace polysat { find_t find_viable(pvar v, rational& out_val); /* - * Explain the current variable is not viable or signleton. - */ + * Explain the current variable is not viable or singleton. + */ dependency_vector explain(); /* - * Register constraint at index 'idx' as unitary in v. - */ + * Register constraint at index 'idx' as unitary in v. + */ find_t add_unitary(pvar v, constraint_id, rational& value); /* - * Ensure data-structures tracking variable v. - */ + * Ensure data-structures tracking variable v. + */ void ensure_var(pvar v); /* - * Check if assignment is viable. - */ - bool assign(pvar v, rational const& value); - + * Check if assignment is viable. + */ + bool assign(pvar v, rational const& value, dependency dep); std::ostream& display(std::ostream& out) const; diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index 770bc670c..d8e5e2674 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -125,7 +125,7 @@ namespace polysat { // walk the e-graph to retrieve fixed sub-slices along with justifications, // as well as pvars that correspond to these sub-slices. - void solver::get_fixed_sub_slices(pvar pv, fixed_slice_extra_vector& fixed, offset_slice_extra_vector& subslices) { + void solver::get_fixed_sub_slices(pvar pv, fixed_slice_extra_vector& fixed, offset_slice_extra_vector& pvars) { #define GET_FIXED_SUB_SLICES_DISPLAY 1 auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool { euf::enode* r = n->get_root(); @@ -141,7 +141,8 @@ namespace polysat { unsigned level = merge_level(n, r); euf::theory_var u = n->get_th_var(get_id()); - dependency dep = (u == euf::null_theory_var) ? dependency::axiom() : dependency(u, w); // TODO: probably need an enode_pair instead? + // dependency dep = (u == euf::null_theory_var || u == w) ? dependency::axiom() : dependency(u, w); // TODO: probably need an enode_pair instead? + dependency dep = dependency(n, r); #if GET_FIXED_SUB_SLICES_DISPLAY verbose_stream() << " " << value << "[" << length << "]@" << offset; @@ -168,9 +169,13 @@ namespace polysat { verbose_stream() << " node " << ctx.bpp(sib); verbose_stream() << " tv " << s; verbose_stream() << " merge-level " << p_level; + verbose_stream() << " assigned? " << m_core.get_assignment().contains(p.var()); + if (m_core.get_assignment().contains(p.var())) + verbose_stream() << " value " << m_core.get_assignment().value(p.var()); verbose_stream() << "\n"; #endif - subslices.push_back(offset_slice_extra(p.var(), offset, p_level)); + dependency d = dependency(r, sib); + pvars.push_back(offset_slice_extra(p.var(), offset, p_level, d, value)); } return true; diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 3798be21a..3e9d47e72 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -154,6 +154,11 @@ namespace polysat { auto const& offs = d.offset(); explain_slice(offs.child, offs.parent, offs.offset, consume); } + else if (d.is_enode_eq()) { + auto const [n1, n2] = d.enode_eq(); + VERIFY(n1->get_root() == n2->get_root()); + eqs.push_back(euf::enode_pair(n1, n2)); + } else { auto const [v1, v2] = d.eq(); euf::enode* const n1 = var2enode(v1); @@ -169,7 +174,6 @@ namespace polysat { for (auto d : deps) explain_dep(d, eqs, core); - IF_VERBOSE(10, verbose_stream() << "explain\n"; for (auto lit : core) @@ -270,7 +274,7 @@ namespace polysat { } void solver::propagate_eq(pvar pv, rational const& val, dependency const& d) { - auto v = m_pddvar2var[pv]; + theory_var v = m_pddvar2var[pv]; auto a = var2enode(v); auto bval = bv.mk_numeral(val, get_bv_size(v)); ctx.internalize(bval);