mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

clarify unsat_core

Browse source
This commit is contained in:
Jakob Rath 2023-02-06 16:33:27 +01:00
parent c79a16db2a
commit a37536e0ae
4 changed files with 27 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/boolean.h
View file

@ -67,6 +67,7 @@ namespace polysat {
unsigned level(sat::literal lit) const { return level(lit.var()); }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; }
clause* reason(sat::literal lit) const { return reason(lit.var()); }
dependency dep(sat::bool_var var) const { return var == sat::null_bool_var ? null_dependency : m_deps[var]; }
dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }

20
src/math/polysat/conflict.cpp
View file

@ -509,6 +509,7 @@ namespace polysat {
indexed_uint_set deps;
LOG("Conflict: " << *this);
SASSERT(s.at_base_level());
auto const enqueue_lit = [&](sat::literal lit) {
if (done_lits.contains(lit))
@ -543,9 +544,7 @@ namespace polysat {
pvar const v = todo_vars.back();
todo_vars.pop_back();
if (s.m_justification[v].is_decision())
continue;
SASSERT(s.m_justification[v].is_propagation());
SASSERT(s.m_justification[v].is_propagation()); // no decisions at base level
for (signed_constraint c : s.m_viable.get_constraints(v))
enqueue_constraint(c);
@ -558,14 +557,12 @@ namespace polysat {
sat::literal const lit = todo_lits.back();
todo_lits.pop_back();
dependency const d = s.m_bvars.dep(lit);
if (!d.is_null())
deps.insert(d.val());
if (s.m_bvars.is_decision(lit))
continue;
else if (s.m_bvars.is_assumption(lit))
continue;
if (s.m_bvars.is_assumption(lit)) {
// only assumptions have external dependencies
dependency const d = s.m_bvars.dep(lit);
if (!d.is_null())
deps.insert(d.val());
}
else if (s.m_bvars.is_bool_propagation(lit)) {
for (sat::literal other : *s.m_bvars.reason(lit))
enqueue_lit(other);
@ -581,6 +578,7 @@ namespace polysat {
}
}
else {
// no decisions at base level
UNREACHABLE();
}
}

4
src/math/polysat/conflict.h
View file

@ -193,6 +193,10 @@ namespace polysat {
/** Move the literals to be narrowed out of the conflict */
sat::literal_vector take_narrow_queue();
/**
* Collect external dependencies of the current conflict.
* This only makes sense for base-level conflicts.
*/
void find_deps(dependency_vector& out_deps) const;
std::ostream& display(std::ostream& out) const;

17
src/math/polysat/solver.cpp
View file

@ -1302,13 +1302,22 @@ namespace polysat {
void solver::unsat_core(dependency_vector& deps) {
VERIFY(is_conflict());
VERIFY(at_base_level());
deps.reset();
m_conflict.find_deps(deps);
IF_VERBOSE(10,
verbose_stream() << "polysat unsat_core";
for (auto d : deps)
verbose_stream() << " " << d;
verbose_stream() << "\n";
verbose_stream() << "polysat unsat_core " << deps << "\n";
// Print constraints involved in the unsat core for debugging.
// NOTE: the output may look confusing since relevant op_constraints are not printed (does not affect correctness of the core).
for (auto d : deps) {
for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
if (m_bvars.dep(b) != d)
continue;
sat::literal lit(b, m_bvars.value(b) == l_false);
SASSERT(m_bvars.is_true(lit));
verbose_stream() << " " << d << ": " << lit_pp(*this, lit) << "\n";
}
}
);
}