mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

Fix checking of lemma invariant

Browse source
This commit is contained in:
Jakob Rath 2022-10-07 16:20:44 +02:00
parent 8333664433
commit 74b53c3323
2 changed files with 15 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -777,7 +777,7 @@ namespace polysat {
void solver::backjump_lemma() { void solver::backjump_lemma() {
clause_ref lemma = m_conflict.build_lemma(); clause_ref lemma = m_conflict.build_lemma();
LOG_H2("backjump_lemma: " << show_deref(lemma)); LOG_H2("backjump_lemma: " << show_deref(lemma));
SASSERT(lemma_invariant(lemma.get())); SASSERT(lemma);
// find second-highest level of the literals in the lemma // find second-highest level of the literals in the lemma
unsigned max_level = 0; unsigned max_level = 0;
@ -894,7 +894,7 @@ namespace polysat {
SASSERT(m_justification[v].is_decision()); SASSERT(m_justification[v].is_decision());
clause_ref lemma = m_conflict.build_lemma(); clause_ref lemma = m_conflict.build_lemma();
SASSERT(lemma_invariant(lemma.get())); SASSERT(lemma);
if (lemma->empty()) { if (lemma->empty()) {
report_unsat(); report_unsat();
@ -920,7 +920,6 @@ namespace polysat {
clause_ref lemma_ref = m_conflict.build_lemma(); clause_ref lemma_ref = m_conflict.build_lemma();
SASSERT(lemma_ref); SASSERT(lemma_ref);
clause& lemma = *lemma_ref; clause& lemma = *lemma_ref;
SASSERT(lemma_invariant(&lemma));
SASSERT(!lemma.empty()); SASSERT(!lemma.empty());
SASSERT(count(lemma, ~lit) > 0); SASSERT(count(lemma, ~lit) > 0);
@ -945,20 +944,27 @@ namespace polysat {
} }
void solver::backjump_and_learn(unsigned jump_level, clause& lemma) { void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
#ifndef NDEBUG
assignment_t const old_assignment = assignment();
#endif
clause_ref_vector side_lemmas = m_conflict.take_side_lemmas(); clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
m_conflict.reset(); m_conflict.reset();
backjump(jump_level); backjump(jump_level);
for (auto cl : side_lemmas) for (auto cl : side_lemmas)
add_clause(*cl); add_clause(*cl);
SASSERT(lemma_invariant(lemma, old_assignment));
learn_lemma(lemma); learn_lemma(lemma);
} }
bool solver::lemma_invariant(clause const* lemma) { bool solver::lemma_invariant(clause const& lemma, assignment_t const& assignment) {
SASSERT(lemma); LOG("Lemma: " << lemma);
LOG("Lemma: " << *lemma); for (sat::literal lit : lemma) {
for (sat::literal lit : *lemma) {
LOG(" " << lit_pp(*this, lit)); LOG(" " << lit_pp(*this, lit));
SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this)); // TODO: constraints derived by side lemmas are l_undef at this point!
// they will be false after backjumping and when the side lemmas are propagated.
// but at that point, we cannot check is_currently_false anymore, because the assignment was already reset.
// solution: make a copy of assignment and test invariant after propagating side lemmas (inside learn_lemma?)
SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this, assignment));
} }
return true; return true;
} }

2
src/math/polysat/solver.h
View file

@ -236,7 +236,7 @@ namespace polysat {
bool invariant(); bool invariant();
static bool invariant(signed_constraints const& cs); static bool invariant(signed_constraints const& cs);
bool lemma_invariant(clause const* lemma); bool lemma_invariant(clause const& lemma, assignment_t const& assignment);
bool wlist_invariant(); bool wlist_invariant();
bool assignment_invariant(); bool assignment_invariant();
bool verify_sat(); bool verify_sat();