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

unsat core validity check works only if m_conflict.m_dep.is_null()

Browse source
This commit is contained in:
Jakob Rath 2023-03-23 14:15:17 +01:00
parent df82d9b0f9
commit 73b97f3a32
2 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -194,7 +194,7 @@ namespace polysat {
unsigned conflict::effective_level() const { unsigned conflict::effective_level() const {
SASSERT(!empty()); SASSERT(!empty());
// If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier. // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
if (m_dep != null_dependency) if (!m_dep.is_null())
return m_level; return m_level;
// In other cases, m_level just tracks the level at which the conflict appeared. // In other cases, m_level just tracks the level at which the conflict appeared.
// Find the minimal level at which the conflict is still valid. // Find the minimal level at which the conflict is still valid.
@ -211,7 +211,7 @@ namespace polysat {
bool conflict::is_valid() const { bool conflict::is_valid() const {
SASSERT(!empty()); SASSERT(!empty());
// If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier. // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
if (m_dep != null_dependency) if (!m_dep.is_null())
return m_level <= s.m_level; return m_level <= s.m_level;
// All conflict constraints must be bool-assigned. // All conflict constraints must be bool-assigned.
for (unsigned lit_idx : m_literals) for (unsigned lit_idx : m_literals)
@ -657,6 +657,8 @@ namespace polysat {
std::ostream& conflict::display(std::ostream& out) const { std::ostream& conflict::display(std::ostream& out) const {
out << "lvl " << m_level; out << "lvl " << m_level;
if (!m_dep.is_null())
out << "dep " << m_dep;
char const* sep = " "; char const* sep = " ";
for (auto c : *this) for (auto c : *this)
out << sep << c->bvar2string() << " " << c, sep = " ; "; out << sep << c->bvar2string() << " " << c, sep = " ; ";

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

@ -1503,15 +1503,19 @@ namespace polysat {
// NOTE: the output may look confusing since relevant op_constraints are not printed (does not affect correctness of the core). // NOTE: the output may look confusing since relevant op_constraints are not printed (does not affect correctness of the core).
uint_set vars; uint_set vars;
for (auto d : deps) { for (auto d : deps) {
bool found = false;
for (sat::bool_var b = 0; b < m_bvars.size(); ++b) { for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
if (m_bvars.dep(b) != d) if (m_bvars.dep(b) != d)
continue; continue;
found = true;
sat::literal lit(b, m_bvars.value(b) == l_false); sat::literal lit(b, m_bvars.value(b) == l_false);
SASSERT(m_bvars.is_true(lit)); SASSERT(m_bvars.is_true(lit));
verbose_stream() << " " << d << ": " << lit_pp(*this, lit) << "\n"; verbose_stream() << " " << d << ": " << lit_pp(*this, lit) << "\n";
for (pvar v : lit2cnstr(lit).vars()) for (pvar v : lit2cnstr(lit).vars())
vars.insert(v); vars.insert(v);
} }
if (!found)
verbose_stream() << " " << d << ": <no constraint in polysat>\n";
} }
for (pvar v : vars) for (pvar v : vars)
if (signed_constraint c = m_constraints.find_op_by_result_var(v)) if (signed_constraint c = m_constraints.find_op_by_result_var(v))
@ -1519,16 +1523,24 @@ namespace polysat {
}); });
#if ENABLE_LEMMA_VALIDITY_CHECK #if ENABLE_LEMMA_VALIDITY_CHECK
clause_builder cb(*this, "unsat core check"); clause_builder cb(*this, "unsat core check");
bool ok = true;
for (auto d : deps) { for (auto d : deps) {
bool found = false;
for (sat::bool_var b = 0; b < m_bvars.size(); ++b) { for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
if (m_bvars.dep(b) != d) if (m_bvars.dep(b) != d)
continue; continue;
found = true;
sat::literal lit(b, m_bvars.value(b) == l_false); sat::literal lit(b, m_bvars.value(b) == l_false);
VERIFY(m_bvars.is_true(lit)); VERIFY(m_bvars.is_true(lit));
cb.insert(~lit); cb.insert(~lit);
} }
if (!found) {
ok = false;
// VERIFY_EQ(d, m_conflict.m_dep);
}
} }
log_lemma_smt2(*cb.build()); // check the unsat core if (ok)
log_lemma_smt2(*cb.build()); // check the unsat core
#endif #endif
} }