mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

lemma_invariant

Browse source
This commit is contained in:
Jakob Rath 2022-09-30 13:12:47 +02:00
parent 5e54cd3e44
commit 05442e8788
2 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -718,12 +718,7 @@ namespace polysat {
void solver::backjump_lemma() {
clause_ref lemma = m_conflict.build_lemma();
LOG_H2("backjump_lemma: " << show_deref(lemma));
SASSERT(lemma);
LOG("Lemma: " << *lemma);
for (sat::literal lit : *lemma) {
LOG(" " << lit_pp(*this, lit));
SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this));
}
SASSERT(lemma && lemma_invariant(*lemma));
// find second-highest level of the literals in the lemma
unsigned max_level = 0;
@ -821,6 +816,8 @@ namespace polysat {
SASSERT(m_justification[v].is_decision());
clause_ref lemma = m_conflict.build_lemma();
SASSERT(lemma && lemma_invariant(*lemma));
if (lemma->empty())
report_unsat();
else {
@ -830,6 +827,15 @@ namespace polysat {
}
}
bool solver::lemma_invariant(clause const& lemma) {
LOG("Lemma: " << lemma);
for (sat::literal lit : lemma) {
LOG(" " << lit_pp(*this, lit));
SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this));
}
return true;
}
unsigned solver::level(sat::literal lit0, clause const& cl) {
unsigned lvl = 0;
for (auto lit : cl) {

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

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