mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

extend invariant check

Browse source
This commit is contained in:
Jakob Rath 2023-01-09 17:16:47 +01:00
parent c55d316c6a
commit 181995a4fb
2 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -210,7 +210,7 @@ namespace polysat {
linear_propagate();
SASSERT(wlist_invariant());
SASSERT(bool_watch_invariant());
SASSERT(assignment_invariant());
SASSERT(eval_invariant());
}
/**
@ -1486,7 +1486,7 @@ namespace polysat {
}
/** Check that boolean assignment and constraint evaluation are consistent */
bool solver::assignment_invariant() const {
bool solver::eval_invariant() const {
if (is_conflict())
return true;
bool ok = true;
@ -1510,11 +1510,16 @@ namespace polysat {
if (is_conflict())
return true;
uint_set active;
bool ok = true;
for (pvar v : m_free_pvars)
active.insert(v);
for (auto const& [v, val] : assignment())
for (auto const& [v, val] : get_assignment()) {
if (active.contains(v)) {
ok = false;
LOG("Variable v" << v << " is in free var queue despite already assigned " << assignment_pp(*this, v, val));
}
active.insert(v);
bool ok = true;
}
for (pvar v = 0; v < num_vars(); ++v) {
if (!active.contains(v)) {
ok = false;

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

@ -314,7 +314,7 @@ namespace polysat {
static bool invariant(signed_constraints const& cs);
bool wlist_invariant() const;
bool bool_watch_invariant() const;
bool assignment_invariant() const;
bool eval_invariant() const;
bool var_queue_invariant() const;
bool verify_sat();