mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

verify_sat should perform a semantic check

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 14:49:20 +02:00
parent 66a41383e8
commit a8e68ebf86
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -749,6 +749,7 @@ namespace polysat {
// Check that fully evaluated constraints are on the stack // Check that fully evaluated constraints are on the stack
SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this)); SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this));
SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_true(*this)); SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_true(*this));
// TODO: work out invariant for the lemma. It should be impossible to extend the model in a way that makes the lemma true.
} }
SASSERT(lemma->size() > 0); SASSERT(lemma->size() > 0);
clause* cl = m_constraints.store(std::move(lemma)); clause* cl = m_constraints.store(std::move(lemma));
@ -901,14 +902,14 @@ namespace polysat {
return true; return true;
} }
/// Check that all original constraints are satisfied by the current model. /// Check that all constraints on the stack are satisfied by the current model.
bool solver::verify_sat() { bool solver::verify_sat() {
LOG_H1("Checking current model..."); LOG_H1("Checking current model...");
LOG("Assignment: " << assignments_pp(*this)); LOG("Assignment: " << assignments_pp(*this));
bool all_ok = true; bool all_ok = true;
for (auto s : m_search) { for (auto s : m_search) {
if (s.is_boolean()) { if (s.is_boolean()) {
bool ok = m_bvars.value(s.lit()) == l_true; bool ok = m_constraints.lookup(s.lit()).is_currently_true(*this);
LOG((ok ? "PASS" : "FAIL") << ": " << s.lit()); LOG((ok ? "PASS" : "FAIL") << ": " << s.lit());
all_ok = all_ok && ok; all_ok = all_ok && ok;
} }