mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +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 deaced1711
commit c78d5405d1
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

@ -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<enode> theory_datatype::list_subterms(enode* arg) {
ptr_vector<enode> 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;
}

95
src/smt/theory_datatype.h
View file

@ -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<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:
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<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);
}
};