mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

bool_watch_invariant

Browse source
This commit is contained in:
Jakob Rath 2022-12-13 11:47:21 +01:00
parent 6f1e4283bb
commit a3c7a869cd
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1404,7 +1404,9 @@ namespace polysat {
bool solver::bool_watch_invariant() const {
if (is_conflict()) // propagation may be unfinished if a conflict was discovered
return true;
// Check for missed boolean propagations: no clause should have exactly one unassigned literal, unless it is already true.
// Check for missed boolean propagations:
// - no clause should have exactly one unassigned literal, unless it is already true.
// - no clause should be false
for (auto const& cls : m_constraints.clauses()) {
for (auto const& clref : cls) {
clause const& cl = *clref;
@ -1419,6 +1421,8 @@ namespace polysat {
}
}
SASSERT(undefs != 1);
bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); });
SASSERT(!is_false);
}
}
return true;