mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

unsat core dbg

Browse source
This commit is contained in:
Jakob Rath 2023-03-23 13:42:52 +01:00
parent f364ba8c8a
commit df82d9b0f9
2 changed files with 27 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -249,6 +249,8 @@ namespace polysat {
void conflict::init(clause& cl) { void conflict::init(clause& cl) {
LOG("Conflict: clause " << cl); LOG("Conflict: clause " << cl);
for (sat::literal lit : cl)
LOG(" " << lit_pp(s, lit));
SASSERT(empty()); SASSERT(empty());
m_level = s.m_level; m_level = s.m_level;
for (auto lit : cl) { for (auto lit : cl) {
@ -382,6 +384,7 @@ namespace polysat {
} }
void conflict::restore_lemma(clause_ref lemma) { void conflict::restore_lemma(clause_ref lemma) {
SASSERT(!empty());
LOG_H3("Restore Lemma: " << ": " << show_deref(lemma)); LOG_H3("Restore Lemma: " << ": " << show_deref(lemma));
m_lemmas.push_back(std::move(lemma)); m_lemmas.push_back(std::move(lemma));
} }
@ -557,7 +560,12 @@ namespace polysat {
uint_set done_vars; uint_set done_vars;
indexed_uint_set deps; indexed_uint_set deps;
LOG("Conflict: " << *this); LOG_V(11, "State:\n" << s);
LOG_V(11, "Conflict: " << *this);
// LOG_V(11, "Viable:\n" << s.m_viable);
// for (pvar v : m_vars) {
// s.m_viable.log(v);
// }
SASSERT(s.at_base_level()); SASSERT(s.at_base_level());
auto const enqueue_lit = [&](sat::literal lit) { auto const enqueue_lit = [&](sat::literal lit) {
@ -565,7 +573,7 @@ namespace polysat {
return; return;
if (!s.m_bvars.is_assigned(lit)) if (!s.m_bvars.is_assigned(lit))
return; return;
// verbose_stream() << "enqueue " << lit_pp(s, lit) << "\n"; IF_VERBOSE(11, verbose_stream() << " enqueue " << lit_pp(s, lit) << "\n";);
todo_lits.push_back(lit); todo_lits.push_back(lit);
done_lits.insert(lit.var()); done_lits.insert(lit.var());
}; };
@ -577,7 +585,12 @@ namespace polysat {
auto const enqueue_var = [&](pvar v) { auto const enqueue_var = [&](pvar v) {
if (done_vars.contains(v)) if (done_vars.contains(v))
return; return;
// verbose_stream() << "enqueue v" << v << "\n"; IF_VERBOSE(11, {
verbose_stream() << " enqueue v" << v << "\n";
if (signed_constraint c = s.m_constraints.find_op_by_result_var(v))
verbose_stream() << " defined by op_constraint: " << lit_pp(s, c) << "\n";
});
SASSERT(s.is_assigned(v));
todo_vars.push_back(v); todo_vars.push_back(v);
done_vars.insert(v); done_vars.insert(v);
}; };
@ -592,6 +605,7 @@ namespace polysat {
while (!todo_vars.empty()) { while (!todo_vars.empty()) {
pvar const v = todo_vars.back(); pvar const v = todo_vars.back();
todo_vars.pop_back(); todo_vars.pop_back();
IF_VERBOSE(11, verbose_stream() << "Handling v" << v << "\n";);
SASSERT(s.m_justification[v].is_propagation()); // no decisions at base level SASSERT(s.m_justification[v].is_propagation()); // no decisions at base level
@ -605,6 +619,7 @@ namespace polysat {
while (!todo_lits.empty()) { while (!todo_lits.empty()) {
sat::literal const lit = todo_lits.back(); sat::literal const lit = todo_lits.back();
todo_lits.pop_back(); todo_lits.pop_back();
IF_VERBOSE(11, verbose_stream() << "Handling " << lit_pp(s, lit) << "\n";);
if (s.m_bvars.is_assumption(lit)) { if (s.m_bvars.is_assumption(lit)) {
// only assumptions have external dependencies // only assumptions have external dependencies
@ -613,6 +628,7 @@ namespace polysat {
deps.insert(d.val()); deps.insert(d.val());
} }
else if (s.m_bvars.is_bool_propagation(lit)) { else if (s.m_bvars.is_bool_propagation(lit)) {
IF_VERBOSE(11, verbose_stream() << " reason " << *s.m_bvars.reason(lit) << "\n";);
for (sat::literal other : *s.m_bvars.reason(lit)) for (sat::literal other : *s.m_bvars.reason(lit))
enqueue_lit(other); enqueue_lit(other);
} }

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

@ -1497,11 +1497,11 @@ namespace polysat {
VERIFY(at_base_level()); VERIFY(at_base_level());
deps.reset(); deps.reset();
m_conflict.find_deps(deps); m_conflict.find_deps(deps);
IF_VERBOSE(10, IF_VERBOSE(10, {
verbose_stream() << "\nviable:\n" << m_viable << "\n";
verbose_stream() << "polysat unsat_core " << deps << "\n"; verbose_stream() << "polysat unsat_core " << deps << "\n";
// Print constraints involved in the unsat core for debugging. // 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). // NOTE: the output may look confusing since relevant op_constraints are not printed (does not affect correctness of the core).
uint_set vars;
for (auto d : deps) { for (auto d : deps) {
for (sat::bool_var b = 0; b < m_bvars.size(); ++b) { for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
if (m_bvars.dep(b) != d) if (m_bvars.dep(b) != d)
@ -1509,9 +1509,14 @@ namespace polysat {
sat::literal lit(b, m_bvars.value(b) == l_false); sat::literal lit(b, m_bvars.value(b) == l_false);
SASSERT(m_bvars.is_true(lit)); SASSERT(m_bvars.is_true(lit));
verbose_stream() << " " << d << ": " << lit_pp(*this, lit) << "\n"; verbose_stream() << " " << d << ": " << lit_pp(*this, lit) << "\n";
for (pvar v : lit2cnstr(lit).vars())
vars.insert(v);
} }
} }
); for (pvar v : vars)
if (signed_constraint c = m_constraints.find_op_by_result_var(v))
verbose_stream() << " op: " << lit_pp(*this, c) << "\n";
});
#if ENABLE_LEMMA_VALIDITY_CHECK #if ENABLE_LEMMA_VALIDITY_CHECK
clause_builder cb(*this, "unsat core check"); clause_builder cb(*this, "unsat core check");
for (auto d : deps) { for (auto d : deps) {