From c467f093d03b64daddb2a6f8795b3675b84b9640 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jan 2024 08:23:28 -0800 Subject: [PATCH] bugfixes Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/core.cpp | 18 ++++++++++-- src/sat/smt/polysat/monomials.cpp | 45 +++++++---------------------- src/sat/smt/polysat/monomials.h | 25 ---------------- src/sat/smt/polysat_internalize.cpp | 19 ++++++++---- src/sat/smt/polysat_solver.cpp | 5 ++-- src/sat/smt/polysat_solver.h | 4 +-- 6 files changed, 45 insertions(+), 71 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 74b9f8711..c552facb3 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -201,6 +201,9 @@ namespace polysat { sat::check_result core::check() { lbool r = l_true; + if (propagate()) + return sat::check_result::CR_CONTINUE; + switch (assign_variable()) { case l_true: break; @@ -462,10 +465,21 @@ namespace polysat { c.m_prop_queue.pop_back(); } }; - if (m_constraint_index[index.id].value != l_undef) + + auto& value = m_constraint_index[index.id].value; + TRACE("bv", tout << "assignment " << index.id << " " << m_constraint_index[index.id].sc << " := " << value << " sign: " << sign << "\n"); + + if (value != l_undef && + ((value == l_false && !sign) || (value == l_true && sign))) { + TRACE("bv", display(tout << "index " << m_constraint_index[index.id].d << " " << m_constraint_index[index.id].sc << "\n")); + } + + SASSERT(value == l_undef || (value == l_false && sign) || (value == l_true && !sign)); + + if (value != l_undef) return; m_prop_queue.push_back(index); - m_constraint_index[index.id].value = to_lbool(!sign); + value = to_lbool(!sign); s.trail().push(unassign(*this, index.id)); } diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index a3974e9b1..fba1cc0ff 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -20,10 +20,7 @@ namespace polysat { monomials::monomials(core& c): c(c), - C(c.cs()), - m_hash(*this), - m_eq(*this), - m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq) + C(c.cs()) {} pvar monomials::mk(unsigned n, pdd const* args) { @@ -31,40 +28,20 @@ namespace polysat { auto& m = args[0].manager(); unsigned sz = m.power_of_2(); m_tmp.reset(); - for (unsigned i = 0; i < n; ++i) + pdd def = c.value(rational(1), sz); + for (unsigned i = 0; i < n; ++i) { m_tmp.push_back(args[i]); - std::stable_sort(m_tmp.begin(), m_tmp.end(), - [&](pdd const& a, pdd const& b) { return a.index() < b.index(); }); - - pdd offset = c.value(rational(0), sz); - unsigned index = m_monomials.size(); - - m_monomials.push_back({m_tmp, offset, offset, {}, rational(0) }); - unsigned j; - if (m_table.find(index, j)) { - m_monomials.pop_back(); - return m_monomials[j].var.var(); + def *= args[i]; } - struct del_monomial : public trail { - monomials& m; - del_monomial(monomials& m):m(m) {} - void undo() override { - unsigned index = m.m_monomials.size()-1; - m.m_table.erase(index); - m.m_monomials.pop_back(); - } - }; - + pdd var = c.var(c.add_var(sz)); + m_monomials.push_back({m_tmp, var, def, {}, rational(0) }); auto & mon = m_monomials.back(); - mon.var = c.var(c.add_var(sz)); - mon.def = c.value(rational(1), sz); - for (auto p : m_tmp) { + + for (auto p : m_tmp) mon.arg_vals.push_back(rational(0)); - mon.def *= p; - } - m_table.insert(index); - c.trail().push(del_monomial(*this)); + + c.trail().push(push_back_vector(m_monomials)); return mon.var.var(); } @@ -175,7 +152,7 @@ namespace polysat { free_index = j; } constraint_or_dependency_vector cs; - pdd offset = c.value(rational(1), m.power_of_2()); + pdd offset = c.value(rational(1), mon.num_bits()); for (unsigned j = mon.size(); j-- > 0; ) { if (j != free_index) { cs.push_back(~C.eq(mon.args[j], mon.arg_vals[j])); diff --git a/src/sat/smt/polysat/monomials.h b/src/sat/smt/polysat/monomials.h index f2599cdda..e45e0a10f 100644 --- a/src/sat/smt/polysat/monomials.h +++ b/src/sat/smt/polysat/monomials.h @@ -40,31 +40,6 @@ namespace polysat { vector m_monomials; pdd_vector m_tmp; - struct mon_eq { - monomials& m; - mon_eq(monomials& m):m(m) {} - bool operator()(unsigned i, unsigned j) const { - auto const& a = m.m_monomials[i].args; - auto const& b = m.m_monomials[j].args; - return a == b; - }; - }; - - struct pdd_hash { - typedef pdd data_t; - unsigned operator()(pdd const& p) const { return p.hash(); } - }; - struct mon_hash { - monomials& m; - mon_hash(monomials& m):m(m) {} - unsigned operator()(unsigned i) const { - auto const& a = m.m_monomials[i].args; - return vector_hash()(a); - } - }; - mon_hash m_hash; - mon_eq m_eq; - hashtable m_table; unsigned_vector m_to_refine; void init_to_refine(); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 3720c04f2..b9de1762e 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -803,16 +803,23 @@ namespace polysat { } }; - constraint_id solver::eq_constraint(pdd p, pdd q, dependency d) { + constraint_id solver::eq_constraint(pdd p, pdd q, bool sign, dependency d) { pdd r = p - q; constraint_id idx; - if (m_eq2constraint.find(r.index(), idx)) - return idx; + std::pair elem; + bool is_new = true; + if (m_eq2constraint.find(r.index(), elem)) { + if (elem.second == sign) + return elem.first; + is_new = false; + } 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())); + if (is_new) { + m_eq2constraint.insert(r.index(), { idx, sign }); + m_eqs.push_back(r); + ctx.push(undo_add_eq(*this, r.index())); + } return idx; } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 09c116b3c..b2744da90 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -217,8 +217,9 @@ namespace polysat { m_var_eqs_head++; pdd p = var2pdd(v1); pdd q = var2pdd(v2); + TRACE("bv", tout << ctx.bpp(n) << " == " << ctx.bpp(var2enode(v2)) << "\n"); auto d = dependency(v1, v2); - constraint_id id = eq_constraint(p, q, d); + constraint_id id = eq_constraint(p, q, false, d); m_core.assign_eh(id, false); } @@ -232,7 +233,7 @@ namespace polysat { pdd q = var2pdd(v2); sat::literal eq = expr2literal(ne.eq()); auto d = dependency(eq.var()); - auto id = eq_constraint(p, q, d); + auto id = eq_constraint(p, q, true, d); TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n"); m_core.assign_eh(id, true); } diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 4b6be64c0..a81571733 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -199,9 +199,9 @@ namespace polysat { void quot_rem(expr* quot, expr* rem, expr* x, expr* y); vector m_eqs; - u_map m_eq2constraint; + u_map> m_eq2constraint; struct undo_add_eq; - constraint_id eq_constraint(pdd p, pdd q, dependency d); + constraint_id eq_constraint(pdd p, pdd q, bool sign, dependency d); // callbacks from core lbool add_eq_literal(pvar v, rational const& val, dependency& d) override;