mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 20:58:54 +00:00
Code Activity

more fixes

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 16:01:22 +02:00
parent b6c478c2ca
commit a4c3a8c640
2 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/conflict_core.cpp
View file

@ -136,6 +136,7 @@ namespace polysat {
} }
void conflict_core::remove_var(pvar v) { void conflict_core::remove_var(pvar v) {
LOG("Removing v" << v << " from core");
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < m_constraints.size(); ++i) for (unsigned i = 0; i < m_constraints.size(); ++i)
if (m_constraints[i]->contains_var(v)) if (m_constraints[i]->contains_var(v))
@ -146,8 +147,10 @@ namespace polysat {
indexed_uint_set literals_copy = m_literals; // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set) indexed_uint_set literals_copy = m_literals; // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set)
for (unsigned lit_idx : literals_copy) { for (unsigned lit_idx : literals_copy) {
signed_constraint c = cm().lookup(sat::to_literal(lit_idx)); signed_constraint c = cm().lookup(sat::to_literal(lit_idx));
if (c->contains_var(v)) if (c->contains_var(v)) {
unset_mark(c); unset_mark(c);
m_literals.remove(lit_idx);
}
} }
m_vars.remove(v); m_vars.remove(v);
} }
@ -188,9 +191,9 @@ namespace polysat {
/** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */ /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
void conflict_core::keep(signed_constraint c) { void conflict_core::keep(signed_constraint c) {
if (!c->has_bvar()) { if (!c->has_bvar()) {
m_constraints.erase(c); remove(c);
cm().ensure_bvar(c.get()); cm().ensure_bvar(c.get());
insert_literal(c.blit()); insert(c);
} }
LOG_H3("keeping: " << c); LOG_H3("keeping: " << c);
// NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c? // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?

8
src/math/polysat/search_state.h
View file

@ -92,7 +92,7 @@ namespace polysat {
void init() { void init() {
first = m_search->size(); first = m_search->size();
current = first - 1; current = first; // we start one before the beginning
} }
void try_push_block() { void try_push_block() {
@ -104,7 +104,8 @@ namespace polysat {
void pop_block() { void pop_block() {
current = m_index_stack.back().current; current = m_index_stack.back().current;
first = m_index_stack.back().first; // We don't restore 'first', otherwise 'next()' will immediately push a new block again.
// Instead, the current block is merged with the popped one.
m_index_stack.pop_back(); m_index_stack.pop_back();
} }
@ -116,7 +117,6 @@ namespace polysat {
search_iterator(search_state& search): search_iterator(search_state& search):
m_search(&search) { m_search(&search) {
init(); init();
current++; // we start one before the beginning, then it also works for empty m_search
} }
search_item const& operator*() const { search_item const& operator*() const {
@ -134,7 +134,7 @@ namespace polysat {
if (m_index_stack.empty()) if (m_index_stack.empty())
return false; return false;
pop_block(); pop_block();
return true; return next();
} }
} }
}; };