9 #ifndef CPROVER_UTIL_EXPR_ITERATOR_H 10 #define CPROVER_UTIL_EXPR_ITERATOR_H 50 std::reference_wrapper<const exprt>
expr;
59 return distance(left.
it, left.
end) == distance(right.
it, right.
end) &&
69 template<
typename depth_iterator_t>
79 template <
typename other_depth_iterator_t>
82 template <
typename other_depth_iterator_t>
89 template <
typename other_depth_iterator_t>
93 return !(*
this == other);
133 depth_iterator_t tmp(this->
downcast());
143 return m_stack.back().expr.get();
165 {
m_stack=std::move(other.m_stack); }
168 {
m_stack=std::move(other.m_stack); }
172 return m_stack.front().expr.get();
188 auto &operands = expr->operands();
191 const auto i=operands.size()-(state.end-state.it);
192 const auto it=operands.begin()+i;
195 state.end=operands.end();
218 std::deque<depth_iterator_expr_statet>
m_stack;
221 {
return static_cast<depth_iterator_t &>(*
this); }
284 "mutate_root must return the same root node that depth_iteratort was " 307 const bool inserted=this->
m_traversed.insert(expr).second;
const_unique_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
exprt & mutate()
Obtain non-const exprt reference.
depth_iterator_t & downcast()
bool operator==(const depth_iterator_baset< other_depth_iterator_t > &other) const
std::deque< depth_iterator_expr_statet > m_stack
depth_iteratort(exprt &expr)
Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflect...
std::set< exprt > m_traversed
bool push_expr(const exprt &expr)
Pushes expression onto the stack If overridden, this function should be called from the inheriting cl...
std::reference_wrapper< const exprt > expr
depth_iteratort()=default
Create an end iterator.
exprt & mutate()
Obtain non-const reference to the exprt instance currently pointed to by the iterator.
depth_iterator_baset(const exprt &root)
Create begin iterator, starting at the supplied node.
depth_iterator_baset & operator=(depth_iterator_baset &&other)
exprt::operandst::const_iterator operands_iteratort
friend depth_iterator_baset
const exprt * operator->() const
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
bool operator!=(const depth_iterator_baset< other_depth_iterator_t > &other) const
depth_iterator_expr_statet(const exprt &expr, operands_iteratort it, operands_iteratort end)
#define PRECONDITION(CONDITION)
std::forward_iterator_tag iterator_category
const_depth_iteratort()=default
Create an end iterator.
depth_iterator_baset()=default
Create end iterator.
depth_iterator_t operator++(int)
Post-increment operator Expensive copy.
const_unique_depth_iteratort()=default
Create an end iterator.
depth_iterator_t & next_sibling_or_parent()
bool operator==(const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right)
Depth first search iterator base - iterates over supplied expression and all its operands recursively...
depth_iterator_t & operator++()
Preincrement operator Do not call on the end() iterator.
bool push_expr(const exprt &expr)
Push expression onto the stack and add to the set of traversed exprts.
~depth_iterator_baset()=default
Destructor Protected to discourage upcasting.
Base class for all expressions.
depth_iterator_baset & operator=(const depth_iterator_baset &)=default
depth_iteratort(const exprt &expr, std::function< exprt &()> mutate_root)
Create iterator starting at the supplied node (root) If mutations of the child nodes are required the...
const exprt & operator*() const
Dereference operator Dereferencing end() iterator is undefined behaviour.
std::function< exprt &()> mutate_root
If this is non-empty then the root is currently const and this function must be called before any mut...
Helper class for depth_iterator_baset.
depth_iterator_baset(depth_iterator_baset &&other)
const_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)