mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 19:00:25 +00:00
Code Activity

Active lemmas need to be queued for repropagation after resetting conflict

Browse source
This commit is contained in:
Jakob Rath 2023-03-22 17:44:02 +01:00
parent 2804453039
commit e433951e27
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1437,8 +1437,14 @@ namespace polysat {
unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes]; unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
LOG_H3("Pop " << num_scopes << " user scopes"); LOG_H3("Pop " << num_scopes << " user scopes");
pop_levels(m_level - base_level + 1); pop_levels(m_level - base_level + 1);
if (m_level < m_conflict.level()) if (m_level < m_conflict.level()) {
clause_ref_vector lemmas = m_conflict.take_lemmas();
m_conflict.reset(); m_conflict.reset();
// TODO: currently we forget all new lemmas at this point.
for (clause* lemma : lemmas)
if (lemma->is_active())
propagate_clause(*lemma);
}
m_base_levels.shrink(m_base_levels.size() - num_scopes); m_base_levels.shrink(m_base_levels.size() - num_scopes);
m_base_index.shrink(m_base_index.size() - num_scopes); m_base_index.shrink(m_base_index.size() - num_scopes);
} }