mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

deal with literals in conflict_core

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 14:41:13 +02:00
parent 1a810cc696
commit 8edcb9e268
1 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/math/polysat/conflict_core.cpp
View file

@ -50,12 +50,12 @@ namespace polysat {
std::ostream& conflict_core::display(std::ostream& out) const { std::ostream& conflict_core::display(std::ostream& out) const {
char const* sep = ""; char const* sep = "";
for (auto c : m_constraints) for (auto c : *this)
out << sep << c, sep = " ; "; out << sep << c, sep = " ; ";
if (!m_vars.empty()) if (!m_vars.empty())
out << " vars"; out << " vars";
for (auto v : m_vars) for (auto v : m_vars)
out << " " << v; out << " v" << v;
return out; return out;
} }
@ -141,9 +141,14 @@ namespace polysat {
if (m_constraints[i]->contains_var(v)) if (m_constraints[i]->contains_var(v))
unset_mark(m_constraints[i]); unset_mark(m_constraints[i]);
else else
m_constraints[j++] = m_constraints[i]; m_constraints[j++] = m_constraints[i];
m_constraints.shrink(j); m_constraints.shrink(j);
indexed_uint_set literals_copy = m_literals; // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set)
for (unsigned lit_idx : literals_copy) {
signed_constraint c = cm().lookup(sat::to_literal(lit_idx));
if (c->contains_var(v))
unset_mark(c);
}
} }
void conflict_core::set_bailout() { void conflict_core::set_bailout() {
@ -158,9 +163,10 @@ namespace polysat {
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v // resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
SASSERT(var != sat::null_bool_var); SASSERT(var != sat::null_bool_var);
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
bool core_has_pos = contains_literal(sat::literal(var));
bool core_has_neg = contains_literal(~sat::literal(var));
DEBUG_CODE({ DEBUG_CODE({
bool core_has_pos = std::count_if(begin(), end(), [var](auto c){ return c.blit() == sat::literal(var); }) > 0;
bool core_has_neg = std::count_if(begin(), end(), [var](auto c){ return c.blit() == ~sat::literal(var); }) > 0;
bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0; bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0;
bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0; bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0;
SASSERT(!core_has_pos || !core_has_neg); // otherwise core is tautology SASSERT(!core_has_pos || !core_has_neg); // otherwise core is tautology
@ -168,14 +174,10 @@ namespace polysat {
SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg)); SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
}); });
int j = 0; if (core_has_pos)
for (auto c : m_constraints) { remove_literal(sat::literal(var));
if (c->bvar() != var) if (core_has_neg)
m_constraints[j++] = c; remove_literal(~sat::literal(var));
else
unset_mark(c);
}
m_constraints.shrink(j);
for (sat::literal lit : cl) for (sat::literal lit : cl)
if (lit.var() != var) if (lit.var() != var)