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

Try to keep conflict alive for longer

Browse source
This commit is contained in:
Jakob Rath 2023-03-23 07:18:36 +01:00
parent e433951e27
commit 5b3f500900
3 changed files with 35 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -171,6 +171,7 @@ namespace polysat {
}
void conflict::reset() {
LOG("Reset conflict");
m_literals.reset();
m_vars.reset();
m_var_occurrences.reset();
@ -190,6 +191,22 @@ namespace polysat {
return contains(lit) || contains(~lit);
}
unsigned conflict::effective_level() const {
// If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
if (m_dep != null_dependency)
return m_level;
// 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.
unsigned lvl = 0;
for (unsigned lit_idx : m_literals) {
sat::literal const lit = sat::to_literal(lit_idx);
lvl = std::max(lvl, s.m_bvars.level(lit));
}
for (pvar v : m_vars)
lvl = std::max(lvl, s.get_level(v));
return lvl;
}
void conflict::init_at_base_level(dependency dep) {
SASSERT(empty());
SASSERT(s.at_base_level());
@ -396,7 +413,6 @@ namespace polysat {
SASSERT(contains(lit));
SASSERT(!contains(~lit));
unsigned const lvl = s.m_bvars.level(lit);
signed_constraint c = s.lit2cnstr(lit);
unsigned const eval_idx = s.m_search.get_bool_index(lit);

1
src/math/polysat/conflict.h
View file

@ -122,6 +122,7 @@ namespace polysat {
uint_set const& vars() const { return m_vars; }
unsigned level() const { return m_level; }
unsigned effective_level() const;
bool is_relevant_pvar(pvar v) const;
bool is_relevant(sat::literal lit) const;

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

@ -1434,17 +1434,26 @@ namespace polysat {
void solver::pop(unsigned num_scopes) {
VERIFY(m_base_levels.size() >= num_scopes);
SASSERT_EQ(m_base_index.size(), m_base_levels.size());
unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
LOG_H3("Pop " << num_scopes << " user scopes");
pop_levels(m_level - base_level + 1);
if (m_level < m_conflict.level()) {
clause_ref_vector lemmas = m_conflict.take_lemmas();
unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
unsigned const target_level = base_level - 1;
clause_ref_vector lemmas;
if (is_conflict() && target_level < m_conflict.effective_level()) {
lemmas = m_conflict.take_lemmas();
m_conflict.reset();
// TODO: currently we forget all new lemmas at this point.
for (clause* lemma : lemmas)
if (lemma->is_active())
propagate_clause(*lemma);
}
pop_levels(m_level - base_level + 1);
SASSERT_EQ(m_level, target_level);
// TODO: currently we forget all new lemmas at this point.
// (but anything that uses popped assumptions cannot be used anymore.)
for (clause* lemma : lemmas)
if (lemma->is_active())
propagate_clause(*lemma);
m_base_levels.shrink(m_base_levels.size() - num_scopes);
m_base_index.shrink(m_base_index.size() - num_scopes);
}