mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-26 05:43:33 +00:00
Code Activity

update iterator pattern

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-01-13 11:33:15 -08:00
parent 9ca6580e38
commit b3c1de6643
2 changed files with 57 additions and 89 deletions
Download patch file Download diff file Expand all files Collapse all files

51
src/smt/theory_datatype.cpp
View file

@ -665,68 +665,45 @@ namespace smt {
} }
} }
void subterm_iterator::next() { void theory_datatype::subterm_iterator::next() {
m_current = nullptr; m_current = nullptr;
if (!m_manager)
return;
while (!m_todo.empty()) { while (!m_todo.empty()) {
enode *curr = m_todo.back(); enode *curr = m_todo.back();
m_todo.pop_back(); m_todo.pop_back();
enode *root = curr->get_root(); enode *root = curr->get_root();
if (root->is_marked()) if (root->is_marked())
continue; continue;
root->set_mark(); root->set_mark();
m_marked.push_back(root); f.m_marked.push_back(root);
enode *ctor = nullptr; enode *ctor = nullptr;
enode *iter = root; enode *iter = root;
do { do {
if (m_util->is_constructor(iter->get_expr())) { if (f.th.m_util.is_constructor(iter->get_expr())) {
ctor = iter; ctor = iter;
break; break;
} }
iter = iter->get_next(); iter = iter->get_next();
} while (iter != root); }
while (iter != root);
if (ctor) { if (ctor) {
m_current = ctor; m_current = ctor;
for (enode *child : enode::args(ctor)) { for (enode *child : enode::args(ctor))
m_todo.push_back(child); m_todo.push_back(child);
}
return;
}
else {
m_current = root;
return;
} }
else
m_current = root;
return;
} }
} }
subterm_iterator::subterm_iterator(ast_manager &m, datatype_util& m_util, enode *start) : m_manager(&m), m_current(nullptr), m_util(&m_util) {
m_todo.push_back(start);
next();
}
subterm_iterator::subterm_iterator(subterm_iterator &&other) : m_manager(nullptr), m_current(nullptr), m_util(nullptr) {
m_todo.swap(other.m_todo);
m_marked.swap(other.m_marked);
std::swap(m_manager, other.m_manager);
std::swap(m_current, other.m_current);
std::swap(m_util, other.m_util);
}
subterm_iterator::~subterm_iterator() {
for (enode *n : m_marked)
n->unset_mark();
}
ptr_vector<enode> theory_datatype::list_subterms(enode* arg) { ptr_vector<enode> theory_datatype::list_subterms(enode* arg) {
ptr_vector<enode> result; ptr_vector<enode> result;
for (enode* n : iterate_subterms(get_manager(), m_util, arg)) { auto f = iterate_subterms(arg);
result.push_back(n); for (enode* n : f)
} result.push_back(n);
f.reset();
return result; return result;
} }

95
src/smt/theory_datatype.h
View file

@ -156,6 +156,49 @@ namespace smt {
void restart_eh() override { m_util.reset(); } void restart_eh() override { m_util.reset(); }
bool is_shared(theory_var v) const override; bool is_shared(theory_var v) const override;
theory_datatype_params const& params() const; theory_datatype_params const& params() const;
struct iterator_factory;
struct subterm_iterator {
iterator_factory &f;
ptr_vector<enode> m_todo;
enode *m_current = nullptr;
void next();
bool operator!=(const subterm_iterator &other) const { return m_current != other.m_current; }
enode *operator*() const { return m_current; }
void operator++() { next(); }
subterm_iterator(iterator_factory &f, enode *start) : f(f) {
if (start) {
m_todo.push_back(start);
next();
}
}
};
struct iterator_factory {
theory_datatype &th;
ptr_vector<enode> m_marked;
enode *start;
iterator_factory(theory_datatype &th, enode* start) : th(th), start(start) {}
subterm_iterator begin() {
return subterm_iterator(*this, start);
}
subterm_iterator end() {
return subterm_iterator(*this, nullptr);
}
void reset() {
for (enode* n : m_marked)
n->unset_mark();
m_marked.reset();
}
};
iterator_factory iterate_subterms(enode *arg) {
return iterator_factory(*this, arg);
}
public: public:
theory_datatype(context& ctx); theory_datatype(context& ctx);
~theory_datatype() override; ~theory_datatype() override;
@ -172,58 +215,6 @@ namespace smt {
bool include_func_interp(func_decl* f) override; bool include_func_interp(func_decl* f) override;
}; };
/**
* Iterator over the subterms of an enode.
*
* It only takes into account datatype terms when looking for subterms.
*
* It uses the `mark` field of the `enode` struct to mark the node visited.
* It will clean afterwards. *Implementation invariant*: the destructor
* *must* be run *exactly* once otherwise the marks might not be clean or
* might be clean more than once and mid search
*/
class subterm_iterator {
ptr_vector<enode> m_todo;
ptr_vector<enode> m_marked;
ast_manager* m_manager;
enode* m_current;
datatype_util* m_util;
void next();
subterm_iterator() : m_manager(nullptr), m_current(nullptr), m_util(nullptr) {}
public:
// subterm_iterator();
subterm_iterator(ast_manager& m, datatype_util& m_util, enode *start);
~subterm_iterator();
subterm_iterator(subterm_iterator &&other);
// need to delete this function otherwise the destructor could be ran
// more than once, invalidating the marks used in the dfs.
subterm_iterator(const subterm_iterator& other) = delete;
subterm_iterator begin() {
return std::move(*this);
}
subterm_iterator end() {
return subterm_iterator();
}
bool operator!=(const subterm_iterator &other) const {
return m_current != other.m_current;
}
enode *operator*() const {
return m_current;
}
void operator++() { next(); }
subterm_iterator& operator=(const subterm_iterator&) = delete;
};
inline subterm_iterator iterate_subterms(ast_manager& m, datatype_util& m_util, enode *arg) {
return subterm_iterator(m, m_util, arg);
}
}; };