mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Try to fix lemma_invariant

Browse source
This commit is contained in:
Jakob Rath 2022-10-07 17:48:22 +02:00
parent 05f1b4dd1a
commit 714c71ab88
2 changed files with 46 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -853,14 +853,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 #ifndef NDEBUG
assignment_t const old_assignment = assignment(); assignment_t old_assignment;
// We can't use solver::assignment() here because we already used search_sate::pop_assignment().
// TODO: fix search_state design; it should show a consistent state.
search_iterator search_it(m_search);
while (search_it.next()) {
auto& item = *search_it;
if (item.is_assignment()) {
pvar v = item.var();
old_assignment.push_back({v, get_value(v)});
}
}
sat::literal_vector lemma_invariant_todo;
SASSERT(lemma_invariant_part1(lemma, old_assignment, lemma_invariant_todo));
// SASSERT(lemma_invariant(lemma, old_assignment));
#endif #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)); SASSERT(lemma_invariant_part2(lemma_invariant_todo));
learn_lemma(lemma); learn_lemma(lemma);
} }
@ -887,11 +900,37 @@ namespace polysat {
} }
} }
bool solver::lemma_invariant(clause const& lemma, assignment_t const& assignment) { bool solver::lemma_invariant_part1(clause const& lemma, assignment_t const& assignment, sat::literal_vector& out_todo) {
SASSERT(out_todo.empty());
LOG("Lemma: " << lemma); LOG("Lemma: " << lemma);
// LOG("assignment: " << assignment);
for (sat::literal lit : lemma) { for (sat::literal lit : lemma) {
LOG(" " << lit_pp(*this, lit)); auto const c = lit2cnstr(lit);
SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this, assignment)); bool const currently_false = c.is_currently_false(*this, assignment);
LOG(" " << lit_pp(*this, lit) << " currently_false? " << currently_false);
if (!currently_false && m_bvars.value(lit) == l_undef)
out_todo.push_back(lit); // undefs might only be set false after the side lemmas are propagated, so check them later.
else
SASSERT(m_bvars.value(lit) == l_false || currently_false);
}
return true;
}
bool solver::lemma_invariant_part2(sat::literal_vector const& todo) {
// Check that undef literals are now propagated by the side lemmas.
for (sat::literal lit : todo)
SASSERT(m_bvars.value(lit) == l_false);
return true;
}
bool solver::lemma_invariant(clause const& lemma, assignment_t const& old_assignment) {
LOG("Lemma: " << lemma);
// LOG("old_assignment: " << old_assignment);
for (sat::literal lit : lemma) {
auto const c = lit2cnstr(lit);
bool const currently_false = c.is_currently_false(*this, old_assignment);
LOG(" " << lit_pp(*this, lit) << " currently_false? " << currently_false);
SASSERT(m_bvars.value(lit) == l_false || currently_false);
} }
return true; return true;
} }

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

@ -237,6 +237,8 @@ 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, assignment_t const& assignment); bool lemma_invariant(clause const& lemma, assignment_t const& assignment);
bool lemma_invariant_part1(clause const& lemma, assignment_t const& assignment, sat::literal_vector& out_todo);
bool lemma_invariant_part2(sat::literal_vector const& todo);
bool wlist_invariant(); bool wlist_invariant();
bool assignment_invariant(); bool assignment_invariant();
bool verify_sat(); bool verify_sat();