From 20afc55b41fcc4918bc608af5ccf7329fbe23195 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Dec 2023 14:24:52 -0800 Subject: [PATCH] misc bugfixes Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_bv_plugin.cpp | 3 +- src/sat/smt/polysat/core.cpp | 65 +++++------ src/sat/smt/polysat/core.h | 1 + src/sat/smt/polysat/fixed_bits.cpp | 14 +++ src/sat/smt/polysat/fixed_bits.h | 5 + src/sat/smt/polysat/ule_constraint.cpp | 14 +-- src/sat/smt/polysat/viable.cpp | 42 +++++--- src/sat/smt/polysat/viable.h | 3 +- src/sat/smt/polysat_egraph.cpp | 1 + src/sat/smt/polysat_model.cpp | 2 +- src/sat/smt/polysat_solver.cpp | 143 +++++++++---------------- src/sat/smt/polysat_solver.h | 3 + 12 files changed, 149 insertions(+), 147 deletions(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 87bd4c434..e6be6e45b 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -485,7 +485,8 @@ namespace euf { if (n->get_root() == b->get_root() && offs == offset) { while (j != UINT_MAX) { auto [x, y, j2] = just[j]; - consumer(x, y); + if (x != y) + consumer(x, y); j = j2; } for (auto const& [n, offset, j] : m_jtodo) { diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 99814e322..6b6dc1acf 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -41,15 +41,6 @@ namespace polysat { void undo() { c.m_justification[m_var] = null_dependency; c.m_assignment.pop(); - } - }; - - class core::mk_dqueue_var : public trail { - pvar m_var; - core& c; - public: - mk_dqueue_var(pvar v, core& c) : m_var(v), c(c) {} - void undo() { c.m_var_queue.unassign_var_eh(m_var); } }; @@ -171,12 +162,13 @@ namespace polysat { sat::check_result core::check() { if (m_var_queue.empty()) return final_check(); - m_var = m_var_queue.next_var(); - s.trail().push(mk_dqueue_var(m_var, *this)); + m_var = m_var_queue.min_var(); + CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n");); + SASSERT(!is_assigned(m_var)); switch (m_viable.find_viable(m_var, m_value)) { case find_t::empty: - TRACE("bv", tout << "check-conflict v" << m_var << "\n"); + TRACE("bv", tout << "viable-conflict v" << m_var << "\n"); s.set_conflict(m_viable.explain(), "viable-conflict"); return sat::check_result::CR_CONTINUE; case find_t::singleton: { @@ -186,20 +178,21 @@ namespace polysat { return sat::check_result::CR_CONTINUE; } case find_t::multiple: { - TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << "\n"); + do { + try_again: dependency d = null_dependency; lbool value = s.add_eq_literal(m_var, m_value, d); + TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << " " << value << "\n"); switch (value) { case l_true: propagate_assignment(m_var, m_value, d); break; case l_false: m_value = mod(m_value + 1, rational::power_of_two(size(m_var))); - continue; + goto try_again; default: - // let core assign equality. - m_var_queue.unassign_var_eh(m_var); + // let core assign equality. break; } } @@ -208,7 +201,6 @@ namespace polysat { } case find_t::resource_out: TRACE("bv", tout << "check-resource out v" << m_var << "\n"); - m_var_queue.unassign_var_eh(m_var); return sat::check_result::CR_GIVEUP; } UNREACHABLE(); @@ -232,7 +224,7 @@ namespace polysat { auto vars = find_conflict_variables(idx); saturation sat(*this); for (auto v : vars) - if (sat.resolve(v, conflict_idx)) + if (sat.resolve(v, idx)) return sat::check_result::CR_CONTINUE; } @@ -287,27 +279,40 @@ namespace polysat { TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n"); if (sc.is_eq(m_var, m_value)) propagate_assignment(m_var, m_value, dep); - else - sc.activate(*this, dep); + else + propagate_activation(idx, sc, dep); } void core::add_watch(unsigned idx, unsigned var) { m_watch[var].push_back(idx); } + void core::propagate_activation(constraint_id idx, signed_constraint& sc, dependency dep) { + sc.activate(*this, dep); + pvar v = null_var; + for (auto w : sc.vars()) { + if (is_assigned(w)) + continue; + if (v != null_var) + return; + v = w; + } + if (v != null_var) + verbose_stream() << "propagate activation " << v << " " << sc << " " << dep << "\n"; + if (v != null_var && !m_viable.add_unitary(v, idx.id)) + s.set_conflict(m_viable.explain(), "viable-conflict"); + } + void core::propagate_assignment(pvar v, rational const& value, dependency dep) { TRACE("bv", tout << "propagate assignment v" << v << " := " << value << " " << is_assigned(v) << "\n"); if (is_assigned(v)) return; - if (m_var_queue.contains(v)) { - m_var_queue.del_var_eh(v); - s.trail().push(mk_dqueue_var(v, *this)); - } m_values[v] = value; m_justification[v] = dep; m_assignment.push(v , value); s.trail().push(mk_assign_var(v, *this)); + m_var_queue.del_var_eh(v); // update the watch lists for pvars // remove constraints from m_watch[v] that have more than 2 free variables. @@ -347,8 +352,8 @@ namespace polysat { if (!is_assigned(v0) || is_assigned(v1)) continue; // detect unitary, add to viable, detect conflict? - if (value != l_undef) - m_viable.add_unitary(v1, idx); + if (value != l_undef && !m_viable.add_unitary(v1, idx)) + s.set_conflict(m_viable.explain(), "viable-conflict"); } SASSERT(m_watch[v].size() == sz && "size of watch list was not changed"); m_watch[v].shrink(j); @@ -459,10 +464,10 @@ namespace polysat { out << "polysat:\n"; for (auto const& [sc, d, value] : m_constraint_index) out << sc << " " << d << " := " << value << "\n"; - for (unsigned i = 0; i < m_vars.size(); ++i) { - out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n"; - } - m_var_queue.display(out << "vars ") << "\n"; + for (unsigned i = 0; i < m_vars.size(); ++i) + out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n"; + m_var_queue.display(out << "var queue: ") << "\n"; + m_viable.display(out); return out; } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 52d3ae445..fa3507804 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -81,6 +81,7 @@ namespace polysat { void propagate_assignment(constraint_id idx); void propagate_eval(constraint_id idx); void propagate_assignment(pvar v, rational const& value, dependency dep); + void propagate_activation(constraint_id idx, signed_constraint& sc, dependency dep); void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d); void add_watch(unsigned idx, unsigned var); diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp index 4aec4740e..52cb71480 100644 --- a/src/sat/smt/polysat/fixed_bits.cpp +++ b/src/sat/smt/polysat/fixed_bits.cpp @@ -17,6 +17,13 @@ Author: namespace polysat { + void fixed_bits::reset() { + m_fixed_slices.reset(); + m_var = null_var; + m_fixed.reset(); + m_bits.reset(); + } + // reset with fixed bits information for variable v void fixed_bits::reset(pvar v) { m_fixed_slices.reset(); @@ -80,6 +87,9 @@ namespace polysat { break; } } + + + CTRACE("bv", i == sz, display(tout << "overflow\n")); // overflow if (i == sz) return false; @@ -98,6 +108,10 @@ namespace polysat { return result; } + std::ostream& fixed_bits::display(std::ostream& out) const { + return out << "fixed bits: v" << m_var << " " << m_fixed << "\n"; + } + /** * 2^k * x = 2^k * b * ==> x[N-k-1:0] = b[N-k-1:0] diff --git a/src/sat/smt/polysat/fixed_bits.h b/src/sat/smt/polysat/fixed_bits.h index 5a30ac039..551557e7e 100644 --- a/src/sat/smt/polysat/fixed_bits.h +++ b/src/sat/smt/polysat/fixed_bits.h @@ -37,6 +37,9 @@ namespace polysat { public: fixed_bits(core& c) : c(c) {} + // reset without variable reference. + void reset(); + // reset with fixed bits information for variable v void reset(pvar v); @@ -45,5 +48,7 @@ namespace polysat { // explain the fixed bits ranges. dependency_vector explain(); + + std::ostream& display(std::ostream& out) const; }; } diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index c39120ec3..60b7dcd61 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -142,33 +142,33 @@ namespace polysat { } if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) { - LOG("-p + k <= k --> p <= k"); + TRACE("bv", tout << "- p + k <= k--> p <= k\n"); lhs = rhs - lhs; } if (lhs.is_val() && !lhs.is_zero() && lhs.val() == rhs.offset()) { - LOG("k <= p + k --> p <= -k-1"); + TRACE("bv", tout << "k <= p + k --> p <= -k-1\n"); pdd k = lhs; lhs = rhs - lhs; rhs = -k - 1; } if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) { - LOG("k <= -p --> p-1 <= -k-1"); + TRACE("bv", tout << "k <= -p--> p - 1 <= -k - 1\n"); pdd k = lhs; lhs = -(rhs + 1); rhs = -k - 1; } if (rhs.is_val() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) { - LOG("-p <= k --> -k-1 <= p-1"); + TRACE("bv", tout << "-p <= k --> -k-1 <= p-1\n"); pdd k = rhs; rhs = -(lhs + 1); lhs = -k - 1; } if (rhs.is_zero() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) { - LOG("-p <= 0 --> p <= 0"); + TRACE("bv", tout << "-p <= 0 --> p <= 0\n"); lhs = -lhs; } // NOTE: do not use pdd operations in conditions when comparing pdd values. @@ -180,7 +180,7 @@ namespace polysat { // TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken. if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) { - LOG("p - k <= -k - 1 --> k <= p"); + TRACE("bv", tout << "p - k <= -k - 1 --> k <= p\n"); pdd k = -(rhs + 1); rhs = lhs + k; lhs = k; @@ -190,7 +190,7 @@ namespace polysat { // k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q if (lhs.is_val() && rhs.leading_coefficient() == rational::power_of_two(N-1) && rhs.offset() == lhs_minus_one.val()) { - LOG("k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q"); + TRACE("bv", tout << "k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q\n"); rhs = (lhs - 1) - rhs; } diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index a7b5111f6..370f2236d 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -112,6 +112,7 @@ namespace polysat { val1 = 0; lbool r = next_viable(val1); + TRACE("bv", display_state(tout); display(tout << "next viable v" << v << " " << val1 << " " << r << "\n")); if (r != l_true) return r; @@ -547,10 +548,10 @@ namespace polysat { /* * Register constraint at index 'idx' as unitary in v. */ - void viable::add_unitary(pvar v, unsigned idx) { + bool viable::add_unitary(pvar v, unsigned idx) { if (c.is_assigned(v)) - return; + return true; auto [sc, d, value] = c.m_constraint_index[idx]; SASSERT(value != l_undef); if (value == l_false) @@ -559,29 +560,27 @@ namespace polysat { entry* ne = alloc_entry(v, idx); if (!m_forbidden_intervals.get_interval(sc, v, *ne)) { m_alloc.push_back(ne); - return; + return true; } + // verbose_stream() << "v" << v << " " << sc << " " << ne->interval << "\n"; + if (ne->interval.is_currently_empty()) { m_alloc.push_back(ne); - return; + return true; } - if (ne->coeff == 1) { - intersect(v, ne); - return; - } - else if (ne->coeff == -1) { - insert(ne, v, m_diseq_lin, entry_kind::diseq_e); - return; - } + if (ne->coeff == 1) + intersect(v, ne); + else if (ne->coeff == -1) + insert(ne, v, m_diseq_lin, entry_kind::diseq_e); else { unsigned const w = c.size(v); unsigned const k = ne->coeff.parity(w); // unsigned const lo_parity = ne->interval.lo_val().parity(w); // unsigned const hi_parity = ne->interval.hi_val().parity(w); - display_one(std::cerr << "try to reduce entry: ", v, ne) << "\n"; + IF_VERBOSE(1, display_one(verbose_stream() << "try to reduce entry: ", v, ne) << "\n"); if (k > 0 && ne->coeff.is_power_of_two()) { // reduction of coeff gives us a unit entry @@ -640,8 +639,15 @@ namespace polysat { // unsigned const shared_parity = std::min(coeff_parity, std::min(lo_parity, hi_parity)); insert(ne, v, m_equal_lin, entry_kind::equal_e); - return; } + if (ne->interval.is_full()) { + m_explain.reset(); + m_explain.push_back(ne); + m_fixed_bits.reset(); + m_var = v; + return false; + } + return true; } void viable::ensure_var(pvar v) { @@ -890,6 +896,14 @@ namespace polysat { return out; } + std::ostream& viable::display_state(std::ostream& out) const { + out << "v" << m_var << ": "; + for (auto const& slice : m_overlaps) + out << slice.v << " "; + out << "\n"; + return out; + } + /* * Lower bounds are strictly ascending. * Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction). diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index 54681c7a5..5ac17e31c 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -132,6 +132,7 @@ namespace polysat { fixed_bits m_fixed_bits; offset_slices m_overlaps; void init_overlaps(pvar v); + std::ostream& display_state(std::ostream& out) const; public: viable(core& c); @@ -151,7 +152,7 @@ namespace polysat { /* * Register constraint at index 'idx' as unitary in v. */ - void add_unitary(pvar v, unsigned idx); + bool add_unitary(pvar v, unsigned idx); /* * Ensure data-structures tracking variable v. diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index 3981b05ad..f67258d81 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -117,6 +117,7 @@ namespace polysat { void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function& consume_eq) { euf::theory_var v = m_pddvar2var[pv]; euf::theory_var w = m_pddvar2var[pw]; + verbose_stream() << "explain " << ctx.bpp(var2enode(v)) << " " << ctx.bpp(var2enode(w)) << "\n"; m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq); } diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp index 028aeed6b..aa0fad885 100644 --- a/src/sat/smt/polysat_model.cpp +++ b/src/sat/smt/polysat_model.cpp @@ -73,10 +73,10 @@ namespace polysat { } std::ostream& solver::display(std::ostream& out) const { - m_core.display(out); for (unsigned v = 0; v < get_num_vars(); ++v) if (m_var2pdd_valid.get(v, false)) out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n"; + m_core.display(out); m_intblast.display(out); return out; } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index da6b0b08e..e96bff32a 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -113,41 +113,46 @@ namespace polysat { if (ctx.use_drat() && hint_info) hint = mk_proof_hint(hint_info); auto ex = euf::th_explain::conflict(*this, lits, eqs, hint); - + TRACE("bv", ex->display(tout << "conflict: ") << "\n"; s().display(tout)); ctx.set_conflict(ex); } + void solver::explain_dep(dependency const& d, euf::enode_pair_vector& eqs, sat::literal_vector& core) { + if (d.is_bool_var()) { + auto bv = d.bool_var(); + auto lit = sat::literal(bv, s().value(bv) == l_false); + core.push_back(lit); + } + else if (d.is_fixed_claim()) { + auto const& o = d.fixed(); + std::function consume = [&](auto* a, auto* b) { + eqs.push_back({ a, b }); + }; + explain_fixed(o.v, o.lo, o.hi, o.value, consume); + } + else if (d.is_offset_claim()) { + auto const& offs = d.offset(); + std::function consume = [&](auto* a, auto* b) { + eqs.push_back({ a, b }); + }; + explain_slice(offs.v, offs.w, offs.offset, consume); + } + else { + auto const [v1, v2] = d.eq(); + euf::enode* const n1 = var2enode(v1); + euf::enode* const n2 = var2enode(v2); + VERIFY(n1->get_root() == n2->get_root()); + eqs.push_back(euf::enode_pair(n1, n2)); + } + } + std::pair solver::explain_deps(dependency_vector const& deps) { sat::literal_vector core; euf::enode_pair_vector eqs; - for (auto d : deps) { - if (d.is_bool_var()) { - auto bv = d.bool_var(); - auto lit = sat::literal(bv, s().value(bv) == l_false); - core.push_back(lit); - } - else if (d.is_fixed_claim()) { - auto const& o = d.fixed(); - std::function consume = [&](auto* a, auto* b) { - eqs.push_back({ a, b }); - }; - explain_fixed(o.v, o.lo, o.hi, o.value, consume); - } - else if (d.is_offset_claim()) { - auto const& offs = d.offset(); - std::function consume = [&](auto* a, auto* b) { - eqs.push_back({ a, b }); - }; - explain_slice(offs.v, offs.w, offs.offset, consume); - } - else { - auto const [v1, v2] = d.eq(); - euf::enode* const n1 = var2enode(v1); - euf::enode* const n2 = var2enode(v2); - VERIFY(n1->get_root() == n2->get_root()); - eqs.push_back(euf::enode_pair(n1, n2)); - } - } + for (auto d : deps) + explain_dep(d, eqs, core); + + IF_VERBOSE(10, for (auto lit : core) verbose_stream() << " " << lit << ": " << mk_ismt2_pp(literal2expr(lit), m) << " " << s().value(lit) << "\n"; @@ -236,43 +241,15 @@ namespace polysat { unsigned solver::level(dependency const& d) { if (d.is_bool_var()) return s().lvl(d.bool_var()); - else if (d.is_eq()) { - auto [v1, v2] = d.eq(); - sat::literal_vector lits; - ctx.get_eq_antecedents(var2enode(v1), var2enode(v2), lits); - unsigned level = 0; - for (auto lit : lits) - level = std::max(level, s().lvl(lit)); - return level; - } - else if (d.is_offset_claim()) { - auto const& offs = d.offset(); - sat::literal_vector lits; - std::function consume = [&](auto* a, auto* b) { - ctx.get_eq_antecedents(a, b, lits); - }; - explain_slice(offs.v, offs.w, offs.offset, consume); - unsigned level = 0; - for (auto lit : lits) - level = std::max(level, s().lvl(lit)); - return level; - } - else if (d.is_fixed_claim()) { - auto const& f = d.fixed(); - sat::literal_vector lits; - std::function consume = [&](auto* a, auto* b) { - ctx.get_eq_antecedents(a, b, lits); - }; - explain_fixed(f.v, f.lo, f.hi, f.value, consume); - unsigned level = 0; - for (auto lit : lits) - level = std::max(level, s().lvl(lit)); - return level; - } - else { - SASSERT(d.is_axiom()); - return 0; - } + sat::literal_vector lits; + euf::enode_pair_vector eqs; + explain_dep(d, eqs, lits); + for (auto [n1, n2] : eqs) + ctx.get_eq_antecedents(n1, n2, lits); + unsigned level = 0; + for (auto lit : lits) + level = std::max(level, s().lvl(lit)); + return level; } void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint_info) { @@ -311,41 +288,21 @@ namespace polysat { bool solver::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) { sat::literal_vector lits; + euf::enode_pair_vector eqs; for (auto it = begin; it != end; ++it) { auto const& e = *it; if (std::holds_alternative(e)) { auto d = *std::get_if(&e); SASSERT(!d.is_null()); - if (d.is_bool_var()) { - auto bv = d.bool_var(); - auto lit = sat::literal(bv, s().value(bv) == l_false); - lits.push_back(~lit); - } - else if (d.is_eq()) { - auto [v1, v2] = d.eq(); - lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2))); - } - else if (d.is_offset_claim()) { - auto const& o = d.offset(); - std::function consume = [&](auto* a, auto* b) { - lits.push_back(~eq_internalize(a, b)); - }; - explain_slice(o.v, o.w, o.offset, consume); - } - else if (d.is_fixed_claim()) { - auto const& f = d.fixed(); - std::function consume = [&](auto* a, auto* b) { - lits.push_back(~eq_internalize(a, b)); - }; - explain_fixed(f.v, f.lo, f.hi, f.value, consume); - } - else { - SASSERT(d.is_axiom()); - } + explain_dep(d, eqs, lits); } else if (std::holds_alternative(e)) - lits.push_back(ctx.mk_literal(constraint2expr(*std::get_if(&e)))); + lits.push_back(~ctx.mk_literal(constraint2expr(*std::get_if(&e)))); } + for (auto [n1, n2] : eqs) + ctx.get_eq_antecedents(n1, n2, lits); + for (auto& lit : lits) + lit.neg(); for (auto lit : lits) if (s().value(lit) == l_true) return false; diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 1bae8294c..724a6e0ae 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -193,6 +193,9 @@ namespace polysat { return add_axiom(name, clause.begin(), clause.end(), redundant); } + + void explain_dep(dependency const& d, euf::enode_pair_vector& eqs, sat::literal_vector& lits); + std::pair explain_deps(dependency_vector const& deps); expr_ref constraint2expr(signed_constraint const& sc);