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

remove overcomplicated search_iterator

Browse source
This commit is contained in:
Jakob Rath 2022-08-17 09:30:21 +02:00
parent 201d841a90
commit 309473edad
2 changed files with 6 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -106,74 +106,4 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); }
// Go backwards over the search_state.
// If new entries are added during processing an item, they will be queued for processing next after the current item.
class search_iterator {
search_state* m_search;
unsigned current;
unsigned first; // highest index + 1
struct idx_range {
unsigned current;
unsigned first; // highest index + 1
};
vector<idx_range> m_index_stack;
void init() {
first = m_search->size();
current = first; // we start one before the beginning
}
void try_push_block() {
if (first != m_search->size()) {
m_index_stack.push_back({current, first});
init();
}
}
void pop_block() {
current = m_index_stack.back().current;
// 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();
}
unsigned last() {
return m_index_stack.empty() ? 0 : m_index_stack.back().first;
}
public:
search_iterator(search_state& search):
m_search(&search) {
init();
}
void set_resolved() {
m_search->set_resolved(current);
}
search_item const& operator*() {
return (*m_search)[current];
}
bool next() {
#if 1 // If you want to resolve over constraints that have been added during conflict resolution, enable this.
try_push_block();
#endif
if (current > last()) {
--current;
return true;
}
else {
SASSERT(current == last());
if (m_index_stack.empty())
return false;
pop_block();
return next();
}
}
};
}

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

@ -624,10 +624,9 @@ namespace polysat {
}
m_conflict.begin_conflict("resolve_conflict");
search_iterator search_it(m_search);
while (search_it.next()) {
auto& item = *search_it;
search_it.set_resolved();
for (unsigned i = m_search.size(); i-- > 0; ) {
auto& item = m_search[i];
m_search.set_resolved(i);
if (item.is_assignment()) {
// Resolve over variable assignment
pvar v = item.var();
@ -722,10 +721,9 @@ namespace polysat {
*/
void solver::backtrack_fi() {
uint_set relevant_vars;
search_iterator search_it(m_search);
while (search_it.next()) {
auto& item = *search_it;
search_it.set_resolved();
for (unsigned i = m_search.size(); i-- > 0; ) {
auto& item = m_search[i];
m_search.set_resolved(i);
if (item.is_assignment()) {
// Resolve over variable assignment
pvar v = item.var();