From c78d5405d1593d03c5b5fb1b2f1cd845bb2197fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jan 2026 11:33:15 -0800 Subject: [PATCH] update iterator pattern Signed-off-by: Nikolaj Bjorner --- src/smt/theory_datatype.cpp | 51 ++++++-------------- src/smt/theory_datatype.h | 95 +++++++++++++++++-------------------- 2 files changed, 57 insertions(+), 89 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 00dae2233..ed2c0249c 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -657,68 +657,45 @@ namespace smt { } } - void subterm_iterator::next() { + void theory_datatype::subterm_iterator::next() { m_current = nullptr; - if (!m_manager) - return; while (!m_todo.empty()) { enode *curr = m_todo.back(); m_todo.pop_back(); enode *root = curr->get_root(); - if (root->is_marked()) continue; root->set_mark(); - m_marked.push_back(root); - + f.m_marked.push_back(root); enode *ctor = nullptr; enode *iter = root; do { - if (m_util->is_constructor(iter->get_expr())) { + if (f.th.m_util.is_constructor(iter->get_expr())) { ctor = iter; break; } iter = iter->get_next(); - } while (iter != root); + } + while (iter != root); if (ctor) { m_current = ctor; - for (enode *child : enode::args(ctor)) { - m_todo.push_back(child); - } - return; - } - else { - m_current = root; - return; + for (enode *child : enode::args(ctor)) + m_todo.push_back(child); } + 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 theory_datatype::list_subterms(enode* arg) { ptr_vector result; - for (enode* n : iterate_subterms(get_manager(), m_util, arg)) { - result.push_back(n); - } + auto f = iterate_subterms(arg); + for (enode* n : f) + result.push_back(n); + f.reset(); return result; } diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index b52cae1b3..7287b7da3 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -153,6 +153,49 @@ namespace smt { void restart_eh() override { m_util.reset(); } bool is_shared(theory_var v) const override; theory_datatype_params const& params() const; + struct iterator_factory; + struct subterm_iterator { + iterator_factory &f; + ptr_vector 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 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: theory_datatype(context& ctx); ~theory_datatype() override; @@ -169,58 +212,6 @@ namespace smt { 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 m_todo; - ptr_vector 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); - } };