mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 15:37:58 +00:00
Code Activity

remove literal polarity from dependencies

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-25 09:39:51 -08:00
parent 5398429c21
commit 658f079efd
5 changed files with 34 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/polysat/core.cpp
View file

@ -348,8 +348,7 @@ namespace polysat {
dependency core::get_dependency(constraint_id idx) const { dependency core::get_dependency(constraint_id idx) const {
auto [sc, d, value] = m_constraint_index[idx.id]; auto [sc, d, value] = m_constraint_index[idx.id];
SASSERT(value != l_undef); return d;
return value == l_false ? ~d : d;
} }
dependency_vector core::get_dependencies(constraint_id_vector const& ids) const { dependency_vector core::get_dependencies(constraint_id_vector const& ids) const {

4
src/sat/smt/polysat/saturation.cpp
View file

@ -68,14 +68,14 @@ namespace polysat {
for (auto const& e : cs) { for (auto const& e : cs) {
if (std::holds_alternative<dependency>(e)) { if (std::holds_alternative<dependency>(e)) {
auto d = *std::get_if<dependency>(&e); auto d = *std::get_if<dependency>(&e);
lemma.push_back(~d); lemma.push_back(d);
} }
else if (std::holds_alternative<signed_constraint>(e)) { else if (std::holds_alternative<signed_constraint>(e)) {
auto sc = *std::get_if<signed_constraint>(&e); auto sc = *std::get_if<signed_constraint>(&e);
if (c.eval(sc) != l_false) if (c.eval(sc) != l_false)
return; return;
auto d = c.propagate(~sc, c.explain_eval(sc)); auto d = c.propagate(~sc, c.explain_eval(sc));
lemma.push_back(~d); lemma.push_back(d);
} }
else else
UNREACHABLE(); UNREACHABLE();

19
src/sat/smt/polysat/types.h
View file

@ -37,33 +37,32 @@ namespace polysat {
class dependency { class dependency {
struct axiom_t {}; struct axiom_t {};
std::variant<axiom_t, sat::literal, theory_var_pair, offset_claim> m_data; std::variant<axiom_t, sat::bool_var, theory_var_pair, offset_claim> m_data;
dependency(): m_data(axiom_t()) {} dependency(): m_data(axiom_t()) {}
public: 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(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {}
dependency(offset_claim const& c) : m_data(c) {} dependency(offset_claim const& c) : m_data(c) {}
static dependency axiom() { return dependency(); } static dependency axiom() { return dependency(); }
bool is_null() const { return is_literal() && *std::get_if<sat::literal>(&m_data) == sat::null_literal; } bool is_null() const { return is_bool_var() && *std::get_if<sat::bool_var>(&m_data) == sat::null_bool_var; }
bool is_axiom() const { return std::holds_alternative<axiom_t>(m_data); } bool is_axiom() const { return std::holds_alternative<axiom_t>(m_data); }
bool is_eq() const { return std::holds_alternative<theory_var_pair>(m_data); } bool is_eq() const { return std::holds_alternative<theory_var_pair>(m_data); }
bool is_literal() const { return std::holds_alternative<sat::literal>(m_data); } bool is_bool_var() const { return std::holds_alternative<sat::bool_var>(m_data); }
bool is_offset_claim() const { return std::holds_alternative<offset_claim>(m_data); } bool is_offset_claim() const { return std::holds_alternative<offset_claim>(m_data); }
sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); } sat::bool_var bool_var() const { SASSERT(is_bool_var()); return *std::get_if<sat::bool_var>(&m_data); }
theory_var_pair eq() const { SASSERT(!is_literal()); return *std::get_if<theory_var_pair>(&m_data); } theory_var_pair eq() const { SASSERT(is_eq()); return *std::get_if<theory_var_pair>(&m_data); }
offset_claim offset() const { return *std::get_if<offset_claim>(&m_data); } offset_claim offset() const { return *std::get_if<offset_claim>(&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) { inline std::ostream& operator<<(std::ostream& out, dependency d) {
if (d.is_null()) if (d.is_null())
return out << "null"; return out << "null";
else if (d.is_axiom()) else if (d.is_axiom())
return out << "axiom"; return out << "axiom";
else if (d.is_literal()) else if (d.is_bool_var())
return out << d.literal(); return out << d.bool_var();
else if (d.is_eq()) else if (d.is_eq())
return out << "v" << d.eq().first << " == v" << d.eq().second; return out << "v" << d.eq().first << " == v" << d.eq().second;
else { else {

3
src/sat/smt/polysat_internalize.cpp
View file

@ -181,8 +181,7 @@ namespace polysat {
void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) { void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) {
if (get_bv2a(bv)) if (get_bv2a(bv))
return; return;
sat::literal lit(bv, false); auto index = m_core.register_constraint(sc, dependency(bv));
auto index = m_core.register_constraint(sc, dependency(lit));
auto a = new (get_region()) atom(bv, index); auto a = new (get_region()) atom(bv, index);
insert_bv2a(bv, a); insert_bv2a(bv, a);
ctx.push(mk_atom_trail(bv, *this)); ctx.push(mk_atom_trail(bv, *this));

38
src/sat/smt/polysat_solver.cpp
View file

@ -115,8 +115,10 @@ namespace polysat {
sat::literal_vector core; sat::literal_vector core;
euf::enode_pair_vector eqs; euf::enode_pair_vector eqs;
for (auto d : deps) { for (auto d : deps) {
if (d.is_literal()) { if (d.is_bool_var()) {
core.push_back(d.literal()); auto bv = d.bool_var();
auto lit = sat::literal(bv, s().value(bv) == l_false);
core.push_back(lit);
} }
else { else {
auto const [v1, v2] = d.eq(); auto const [v1, v2] = d.eq();
@ -175,12 +177,12 @@ namespace polysat {
return; return;
pdd p = var2pdd(v1); pdd p = var2pdd(v1);
pdd q = var2pdd(v2); pdd q = var2pdd(v2);
auto sc = ~m_core.eq(p, q); auto sc = m_core.eq(p, q);
sat::literal neq = ~expr2literal(ne.eq()); sat::literal eq = expr2literal(ne.eq());
auto d = dependency(neq); auto d = dependency(eq.var());
auto id = m_core.register_constraint(sc, d); auto id = m_core.register_constraint(sc, d);
TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n"); TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n");
m_core.assign_eh(id, false, s().lvl(neq)); m_core.assign_eh(id, false, s().lvl(eq));
} }
// Core uses the propagate callback to add unit propagations to the trail. // 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) { dependency solver::propagate(signed_constraint sc, dependency_vector const& deps) {
sat::literal lit = ctx.mk_literal(constraint2expr(sc)); sat::literal lit = ctx.mk_literal(constraint2expr(sc));
if (s().value(lit) == l_true) if (s().value(lit) == l_true)
return dependency(lit); return dependency(lit.var());
auto [core, eqs] = explain_deps(deps); auto [core, eqs] = explain_deps(deps);
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr); auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
ctx.propagate(lit, ex); ctx.propagate(lit, ex);
return dependency(lit); return dependency(lit.var());
} }
unsigned solver::level(dependency const& d) { unsigned solver::level(dependency const& d) {
if (d.is_literal()) if (d.is_bool_var())
return s().lvl(d.literal()); return s().lvl(d.bool_var());
else if (d.is_eq()) { else if (d.is_eq()) {
auto [v1, v2] = d.eq(); auto [v1, v2] = d.eq();
sat::literal_vector lits; sat::literal_vector lits;
@ -229,10 +231,9 @@ namespace polysat {
void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) { void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) {
auto [core, eqs] = explain_deps(deps); auto [core, eqs] = explain_deps(deps);
if (d.is_literal()) { if (d.is_bool_var()) {
auto lit = d.literal(); auto bv = d.bool_var();
if (sign) auto lit = sat::literal(bv, sign);
lit.neg();
if (s().value(lit) == l_true) if (s().value(lit) == l_true)
return; return;
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr); auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
@ -264,8 +265,11 @@ namespace polysat {
if (std::holds_alternative<dependency>(e)) { if (std::holds_alternative<dependency>(e)) {
auto d = *std::get_if<dependency>(&e); auto d = *std::get_if<dependency>(&e);
SASSERT(!d.is_null()); SASSERT(!d.is_null());
if (d.is_literal()) if (d.is_bool_var()) {
lits.push_back(~d.literal()); auto bv = d.bool_var();
auto lit = sat::literal(bv, s().value(bv) == l_false);
lits.push_back(~lit);
}
else if (d.is_eq()) { else if (d.is_eq()) {
auto [v1, v2] = d.eq(); auto [v1, v2] = d.eq();
lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2))); lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));