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

Update eval_invariant

Browse source
This commit is contained in:
Jakob Rath 2023-03-05 07:55:06 +01:00
parent 2285ed90fb
commit 0433f81f78
1 changed files with 13 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1663,20 +1663,23 @@ namespace polysat {
bool solver::eval_invariant() const { bool solver::eval_invariant() const {
if (is_conflict()) if (is_conflict())
return true; return true;
bool ok = true;
for (sat::bool_var v = m_bvars.size(); v-- > 0; ) { for (sat::bool_var v = m_bvars.size(); v-- > 0; ) {
sat::literal lit(v); sat::literal const lit(v);
auto c = lit2cnstr(lit); signed_constraint const c = lit2cnstr(lit);
if (!all_of(c->vars(), [this](auto w) { return is_assigned(w); })) if (!all_of(c->vars(), [this](pvar w) { return is_assigned(w); }))
continue; continue;
ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this); lbool const bvalue = m_bvars.value(lit);
ok &= (m_bvars.value(lit) != l_false) || !c.is_currently_true(*this); lbool const pvalue = c.eval(*this);
if (!ok) { if (bvalue != l_undef && pvalue != l_undef && bvalue != pvalue) {
LOG("assignment invariant is broken " << v << "\n" << *this); verbose_stream() << "missed bool/eval conflict: " << lit_pp(*this, lit) << "\n";
break; return false;
}
if (bvalue == l_undef && pvalue != l_undef) {
verbose_stream() << "missed evaluation: " << lit_pp(*this, lit) << "\n";
return false;
} }
} }
return ok; return true;
} }
/** Check that each variable is either assigned or queued for decisions */ /** Check that each variable is either assigned or queued for decisions */