From 78f32401ac58bb945b41da47da5841e5768b65c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Dec 2023 18:11:40 -0800 Subject: [PATCH] bugfixes --- src/sat/smt/polysat/core.cpp | 67 +++++++++++++---------------- src/sat/smt/polysat/core.h | 3 +- src/sat/smt/polysat/viable.cpp | 24 +++++++---- src/sat/smt/polysat_internalize.cpp | 15 ++++--- src/sat/smt/polysat_solver.cpp | 13 ++++-- src/sat/smt/polysat_solver.h | 2 +- 6 files changed, 66 insertions(+), 58 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index bd6a3a6c2..d557fa789 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -62,11 +62,6 @@ namespace polysat { auto& [sc, lit, val] = c.m_constraint_index.back(); auto& vars = sc.vars(); auto idx = c.m_constraint_index.size() - 1; - IF_VERBOSE(10, - verbose_stream() << "undo add watch " << sc << " "; - if (vars.size() > 0) verbose_stream() << "(" << idx << ": " << c.m_watch[vars[0]] << ") "; - if (vars.size() > 1) verbose_stream() << "(" << idx << ": " << c.m_watch[vars[1]] << ") "; - verbose_stream() << "\n"); unsigned n = sc.num_watch(); SASSERT(n <= vars.size()); auto del_watch = [&](unsigned i) { @@ -147,10 +142,6 @@ namespace polysat { add_watch(idx, vars[0]); if (j > 1) add_watch(idx, vars[1]); - IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << " "; - if (j > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") "; - if (j > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") "; - verbose_stream() << "\n"); s.trail().push(mk_add_watch(*this)); return { idx }; } @@ -166,38 +157,36 @@ namespace polysat { 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)) { + auto& var_value = m_values[m_var]; + switch (m_viable.find_viable(m_var, var_value)) { case find_t::empty: viable_conflict(m_var); return sat::check_result::CR_CONTINUE; case find_t::singleton: { auto p = var2pdd(m_var).mk_var(m_var); - auto sc = m_constraints.eq(p, m_value); - TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << " " << sc << "\n"); + auto sc = m_constraints.eq(p, var_value); + TRACE("bv", tout << "check-propagate v" << m_var << " := " << var_value << " " << sc << "\n"); auto d = s.propagate(sc, m_viable.explain(), "viable-propagate"); - propagate_assignment(m_var, m_value, d); + propagate_assignment(m_var, var_value, d); return sat::check_result::CR_CONTINUE; } case find_t::multiple: { - 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: - // add m_var != m_value to m_viable but need a constraint index for that. - m_value = mod(m_value + 1, rational::power_of_two(size(m_var))); - goto try_again; - default: - // let core assign equality. - break; - } - } - while (false); + dependency d = null_dependency; + lbool value = s.add_eq_literal(m_var, var_value, d); + TRACE("bv", tout << "check-multiple v" << m_var << " := " << var_value << " " << value << "\n"); + switch (value) { + case l_true: + propagate_assignment(m_var, var_value, d); + break; + case l_false: + // disequality is forced into propagation queue. + var_value = mod(var_value + 1, rational::power_of_two(size(m_var))); + propagate(); + break; + default: + // let core assign equality. + break; + } return sat::check_result::CR_CONTINUE; } case find_t::resource_out: @@ -211,14 +200,17 @@ namespace polysat { sat::check_result core::final_check() { unsigned n = 0; constraint_id conflict_idx = { UINT_MAX }; + // verbose_stream() << "final-check\n"; for (auto idx : m_prop_queue) { auto [sc, d, value] = m_constraint_index[idx.id]; SASSERT(value != l_undef); + // verbose_stream() << "constraint " << (value == l_true ? sc : ~sc) << "\n"; lbool eval_value = eval(sc); CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"; display(tout);); SASSERT(eval_value != l_undef); if (eval_value == value) continue; + // verbose_stream() << "violated " << sc << " " << d << " " << eval_value << "\n"; if (0 == (m_rand() % (++n))) conflict_idx = idx; @@ -288,8 +280,9 @@ namespace polysat { s.set_conflict({dep}, "infeasible assignment"); return; } - if (sc.is_eq(m_var, m_value)) - propagate_assignment(m_var, m_value, dep); + rational var_value; + if (sc.is_eq(m_var, var_value)) + propagate_assignment(m_var, var_value, dep); else propagate_activation(idx, sc, dep); } @@ -424,7 +417,7 @@ namespace polysat { return s.inconsistent(); } - void core::assign_eh(constraint_id index, bool sign, unsigned level) { + void core::assign_eh(constraint_id index, bool sign) { struct unassign : public trail { core& c; unsigned m_index; @@ -434,6 +427,8 @@ namespace polysat { c.m_prop_queue.pop_back(); } }; + if (m_constraint_index[index.id].value != l_undef) + return; m_prop_queue.push_back(index); m_constraint_index[index.id].value = to_lbool(!sign); s.trail().push(unassign(*this, index.id)); @@ -494,7 +489,7 @@ namespace polysat { void core::add_axiom(signed_constraint sc) { auto idx = register_constraint(sc, dependency::axiom()); - assign_eh(idx, false, 0); + assign_eh(idx, false); } signed_constraint core::get_constraint(constraint_id idx) { diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index bbb4d587b..d14748aa9 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -69,7 +69,6 @@ namespace polysat { vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur // values to split on - rational m_value; pvar m_var = 0; dd::pdd_manager& sz2pdd(unsigned sz) const; @@ -99,7 +98,7 @@ namespace polysat { sat::check_result check(); constraint_id register_constraint(signed_constraint& sc, dependency d); bool propagate(); - void assign_eh(constraint_id idx, bool sign, unsigned level); + void assign_eh(constraint_id idx, bool sign); pvar next_var() { return m_var_queue.next_var(); } pdd value(rational const& v, unsigned sz); diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 70f785d89..bc2f11b22 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -107,20 +107,28 @@ namespace polysat { m_num_bits = c.size(v); m_fixed_bits.reset(v); init_overlaps(v); - - rational const& max_value = c.var2pdd(v).max_value(); - - val1 = 0; + bool start_at0 = val1 == 0; + + lbool r = next_viable(val1); TRACE("bv", display_state(tout); display(tout << "next viable v" << v << " " << val1 << " " << r << "\n")); + if (r == l_false && !start_at0) { + val1 = 0; + r = next_viable(val1); + } if (r != l_true) return r; - if (val1 == max_value) { - val2 = val1; - return l_true; + if (val1 == c.var2pdd(v).max_value()) { + if (start_at0) { + val2 = val1; + return l_true; + } + else + val2 = 0; } - val2 = val1 + 1; + else + val2 = val1 + 1; r = next_viable(val2); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index c32de72f8..9f9fc95f5 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -178,13 +178,15 @@ namespace polysat { } }; - void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) { - if (get_bv2a(bv)) - return; + solver::atom* solver::mk_atom(sat::bool_var bv, signed_constraint& sc) { + auto a = get_bv2a(bv); + if (a) + return a; auto index = m_core.register_constraint(sc, dependency(bv)); - auto a = new (get_region()) atom(bv, index); + a = new (get_region()) atom(bv, index); insert_bv2a(bv, a); ctx.push(mk_atom_trail(bv, *this)); + return a; } void solver::internalize_binary_predicate(app* e, std::function const& fn) { @@ -759,6 +761,7 @@ namespace polysat { public: undo_add_eq(solver& s, unsigned i) : s(s), index(i) {} void undo() override { + SASSERT(index == s.m_eqs.back().index()); s.m_eq2constraint.remove(index); s.m_eqs.pop_back(); } @@ -769,10 +772,8 @@ namespace polysat { constraint_id idx; if (m_eq2constraint.find(r.index(), idx)) return idx; - auto sc = m_core.eq(p, q); - TRACE("bv", tout << "new eq " << sc << "\n"); + auto sc = m_core.eq(p, q); idx = m_core.register_constraint(sc, d); - m_eq2constraint.insert(r.index(), idx); m_eqs.push_back(r); ctx.push(undo_add_eq(*this, r.index())); diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 9fde5b084..9b7184c98 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -114,7 +114,7 @@ namespace polysat { if (!a) return; force_push(); - m_core.assign_eh(a->m_index, l.sign(), s().lvl(l)); + m_core.assign_eh(a->m_index, l.sign()); } void solver::set_conflict(dependency_vector const& deps, char const* hint_info) { @@ -193,10 +193,15 @@ namespace polysat { pdd p = m_core.var(pvar); pdd q = m_core.value(val, m_core.size(pvar)); auto sc = m_core.eq(p, q); - mk_atom(eq.var(), sc); s().set_phase(eq); ctx.mark_relevant(eq); d = dependency(eq.var()); + auto value = s().value(eq); + if (!get_bv2a(eq.var())) { + auto a = mk_atom(eq.var(), sc); + if (value == l_false) + m_core.assign_eh(a->m_index, true); + } return s().value(eq); } @@ -213,7 +218,7 @@ namespace polysat { pdd q = var2pdd(v2); auto d = dependency(v1, v2); constraint_id id = eq_constraint(p, q, d); - m_core.assign_eh(id, false, s().scope_lvl()); + m_core.assign_eh(id, false); } @@ -228,7 +233,7 @@ namespace polysat { auto d = dependency(eq.var()); auto id = eq_constraint(p, q, d); TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n"); - m_core.assign_eh(id, true, s().lvl(eq)); + m_core.assign_eh(id, true); } // Core uses the propagate callback to add unit propagations to the trail. diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index f4e0edf6e..e8f85e41c 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -103,7 +103,7 @@ namespace polysat { void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = nullptr; } atom* get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, nullptr); } class mk_atom_trail; - void mk_atom(sat::bool_var bv, signed_constraint& sc); + atom* mk_atom(sat::bool_var bv, signed_constraint& sc); void set_bit_eh(theory_var v, literal l, unsigned idx); void init_bits(expr* e, expr_ref_vector const & bits); void mk_bits(theory_var v);