mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

log

Browse source
This commit is contained in:
Jakob Rath 2022-08-22 12:46:47 +02:00
parent 53f276d225
commit 3c093e03cf
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -624,7 +624,7 @@ namespace polysat {
return; return;
} }
m_conflict.begin_conflict("resolve_conflict"); m_conflict.begin_conflict("resolve_conflict");
search_iterator search_it(m_search); search_iterator search_it(m_search);
while (search_it.next()) { while (search_it.next()) {
auto& item = *search_it; auto& item = *search_it;
@ -675,6 +675,7 @@ namespace polysat {
} }
} }
} }
LOG("End of resolve_conflict loop");
m_conflict.end_conflict(); m_conflict.end_conflict();
report_unsat(); report_unsat();
} }
@ -688,6 +689,11 @@ namespace polysat {
clause_ref lemma = m_conflict.build_lemma().build(); clause_ref lemma = m_conflict.build_lemma().build();
LOG_H2("backtrack_lemma: " << show_deref(lemma)); LOG_H2("backtrack_lemma: " << show_deref(lemma));
SASSERT(lemma); SASSERT(lemma);
LOG("Lemma: " << *lemma);
for (sat::literal lit : *lemma) {
LOG(" Literal " << lit << " is: " << lit_pp(*this, lit));
SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this));
}
// find second-highest level of the literals in the lemma // find second-highest level of the literals in the lemma
unsigned max_level = 0; // could be simplified if we're sure that always max_level == m_level unsigned max_level = 0; // could be simplified if we're sure that always max_level == m_level