From 658f079efd2c82b2fa8d7b10b3530a8de39bf29f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Dec 2023 09:39:51 -0800 Subject: [PATCH] remove literal polarity from dependencies --- src/sat/smt/polysat/core.cpp | 3 +-- src/sat/smt/polysat/saturation.cpp | 4 +-- src/sat/smt/polysat/types.h | 19 +++++++-------- src/sat/smt/polysat_internalize.cpp | 3 +-- src/sat/smt/polysat_solver.cpp | 38 ++++++++++++++++------------- 5 files changed, 34 insertions(+), 33 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 8208a1b57..0f6ab75f8 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -348,8 +348,7 @@ namespace polysat { dependency core::get_dependency(constraint_id idx) const { auto [sc, d, value] = m_constraint_index[idx.id]; - SASSERT(value != l_undef); - return value == l_false ? ~d : d; + return d; } dependency_vector core::get_dependencies(constraint_id_vector const& ids) const { diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index 8af356e1a..828cbccdc 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -68,14 +68,14 @@ namespace polysat { for (auto const& e : cs) { if (std::holds_alternative(e)) { auto d = *std::get_if(&e); - lemma.push_back(~d); + lemma.push_back(d); } else if (std::holds_alternative(e)) { auto sc = *std::get_if(&e); if (c.eval(sc) != l_false) return; auto d = c.propagate(~sc, c.explain_eval(sc)); - lemma.push_back(~d); + lemma.push_back(d); } else UNREACHABLE(); diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 017a4c854..603db7e8f 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -37,33 +37,32 @@ namespace polysat { class dependency { struct axiom_t {}; - std::variant m_data; + std::variant m_data; dependency(): m_data(axiom_t()) {} public: - dependency(sat::literal lit) : m_data(lit){} + dependency(sat::bool_var v) : m_data(v){} dependency(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {} dependency(offset_claim const& c) : m_data(c) {} static dependency axiom() { return dependency(); } - bool is_null() const { return is_literal() && *std::get_if(&m_data) == sat::null_literal; } + 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_literal() 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); } - sat::literal literal() const { SASSERT(is_literal()); return *std::get_if(&m_data); } - theory_var_pair eq() const { SASSERT(!is_literal()); return *std::get_if(&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); } offset_claim offset() const { return *std::get_if(&m_data); } - dependency operator~() const { SASSERT(is_literal()); return dependency(~literal()); } }; - inline const dependency null_dependency = dependency(sat::null_literal); + inline const dependency null_dependency = dependency(sat::null_bool_var); inline std::ostream& operator<<(std::ostream& out, dependency d) { if (d.is_null()) return out << "null"; else if (d.is_axiom()) return out << "axiom"; - else if (d.is_literal()) - return out << d.literal(); + else if (d.is_bool_var()) + return out << d.bool_var(); else if (d.is_eq()) return out << "v" << d.eq().first << " == v" << d.eq().second; else { diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 0441edf4e..942538334 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -181,8 +181,7 @@ namespace polysat { void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) { if (get_bv2a(bv)) return; - sat::literal lit(bv, false); - auto index = m_core.register_constraint(sc, dependency(lit)); + auto index = m_core.register_constraint(sc, dependency(bv)); auto a = new (get_region()) atom(bv, index); insert_bv2a(bv, a); ctx.push(mk_atom_trail(bv, *this)); diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index b96a1a803..4aae1cd0e 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -115,8 +115,10 @@ namespace polysat { sat::literal_vector core; euf::enode_pair_vector eqs; for (auto d : deps) { - if (d.is_literal()) { - core.push_back(d.literal()); + 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 { auto const [v1, v2] = d.eq(); @@ -175,12 +177,12 @@ namespace polysat { return; pdd p = var2pdd(v1); pdd q = var2pdd(v2); - auto sc = ~m_core.eq(p, q); - sat::literal neq = ~expr2literal(ne.eq()); - auto d = dependency(neq); + auto sc = m_core.eq(p, q); + sat::literal eq = expr2literal(ne.eq()); + auto d = dependency(eq.var()); auto id = m_core.register_constraint(sc, d); - TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n"); - m_core.assign_eh(id, false, s().lvl(neq)); + TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n"); + m_core.assign_eh(id, false, s().lvl(eq)); } // Core uses the propagate callback to add unit propagations to the trail. @@ -190,16 +192,16 @@ namespace polysat { dependency solver::propagate(signed_constraint sc, dependency_vector const& deps) { sat::literal lit = ctx.mk_literal(constraint2expr(sc)); if (s().value(lit) == l_true) - return dependency(lit); + return dependency(lit.var()); auto [core, eqs] = explain_deps(deps); auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr); ctx.propagate(lit, ex); - return dependency(lit); + return dependency(lit.var()); } unsigned solver::level(dependency const& d) { - if (d.is_literal()) - return s().lvl(d.literal()); + 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; @@ -229,10 +231,9 @@ namespace polysat { void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) { auto [core, eqs] = explain_deps(deps); - if (d.is_literal()) { - auto lit = d.literal(); - if (sign) - lit.neg(); + if (d.is_bool_var()) { + auto bv = d.bool_var(); + auto lit = sat::literal(bv, sign); if (s().value(lit) == l_true) return; auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr); @@ -264,8 +265,11 @@ namespace polysat { if (std::holds_alternative(e)) { auto d = *std::get_if(&e); SASSERT(!d.is_null()); - if (d.is_literal()) - lits.push_back(~d.literal()); + 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)));