Depth first search iterator base - iterates over supplied expression and all its operands recursively. More...
#include <expr_iterator.h>
Inheritance diagram for depth_iterator_baset< depth_iterator_t >: Collaboration diagram for depth_iterator_baset< depth_iterator_t >:Public Types | |
| typedef void | difference_type |
| typedef exprt | value_type |
| typedef const exprt * | pointer |
| typedef const exprt & | reference |
| typedef std::forward_iterator_tag | iterator_category |
Public Member Functions | |
| template<typename other_depth_iterator_t > | |
| bool | operator== (const depth_iterator_baset< other_depth_iterator_t > &other) const |
| template<typename other_depth_iterator_t > | |
| bool | operator!= (const depth_iterator_baset< other_depth_iterator_t > &other) const |
| depth_iterator_t & | operator++ () |
| Preincrement operator Do not call on the end() iterator. | |
| depth_iterator_t & | next_sibling_or_parent () |
| depth_iterator_t | operator++ (int) |
| Post-increment operator Expensive copy. | |
| const exprt & | operator* () const |
| Dereference operator Dereferencing end() iterator is undefined behaviour. | |
| const exprt * | operator-> () const |
| Dereference operator (member access) Dereferencing end() iterator is undefined behaviour. | |
Protected Member Functions | |
| depth_iterator_baset ()=default | |
| Create end iterator. | |
| depth_iterator_baset (const exprt &root) | |
| Create begin iterator, starting at the supplied node. | |
| ~depth_iterator_baset ()=default | |
| Destructor Protected to discourage upcasting. | |
| depth_iterator_baset (const depth_iterator_baset &)=default | |
| depth_iterator_baset (depth_iterator_baset &&other) | |
| depth_iterator_baset & | operator= (const depth_iterator_baset &)=default |
| depth_iterator_baset & | operator= (depth_iterator_baset &&other) |
| const exprt & | get_root () |
| exprt & | mutate () |
| Obtain non-const exprt reference. | |
| bool | push_expr (const exprt &expr) |
| Pushes expression onto the stack If overridden, this function should be called from the inheriting class by the override function. | |
Private Member Functions | |
| depth_iterator_t & | downcast () |
Private Attributes | |
| std::deque< depth_iterator_expr_statet > | m_stack |
Friends | |
| template<typename other_depth_iterator_t > | |
| class | depth_iterator_baset |
Detailed Description
Depth first search iterator base - iterates over supplied expression and all its operands recursively.
Base class using CRTP Do override .push_expr method of this class, but when doing so make this class a friend so it has access to that overridden .push_expr method in the child class
Definition at line 66 of file expr_iterator.h.
Member Typedef Documentation
◆ difference_type
| typedef void depth_iterator_baset< depth_iterator_t >::difference_type |
Definition at line 69 of file expr_iterator.h.
◆ iterator_category
| typedef std::forward_iterator_tag depth_iterator_baset< depth_iterator_t >::iterator_category |
Definition at line 73 of file expr_iterator.h.
◆ pointer
| typedef const exprt* depth_iterator_baset< depth_iterator_t >::pointer |
Definition at line 71 of file expr_iterator.h.
◆ reference
| typedef const exprt& depth_iterator_baset< depth_iterator_t >::reference |
Definition at line 72 of file expr_iterator.h.
◆ value_type
| typedef exprt depth_iterator_baset< depth_iterator_t >::value_type |
Definition at line 70 of file expr_iterator.h.
Constructor & Destructor Documentation
◆ depth_iterator_baset() [1/4]
|
protecteddefault |
Create end iterator.
◆ depth_iterator_baset() [2/4]
|
inlineexplicitprotected |
Create begin iterator, starting at the supplied node.
Definition at line 155 of file expr_iterator.h.
◆ ~depth_iterator_baset()
|
protecteddefault |
Destructor Protected to discourage upcasting.
◆ depth_iterator_baset() [3/4]
|
protecteddefault |
◆ depth_iterator_baset() [4/4]
|
inlineprotected |
Definition at line 163 of file expr_iterator.h.
Member Function Documentation
◆ downcast()
|
inlineprivate |
Definition at line 213 of file expr_iterator.h.
◆ get_root()
|
inlineprotected |
Definition at line 172 of file expr_iterator.h.
◆ mutate()
|
inlineprotected |
Obtain non-const exprt reference.
Performs a copy-on-write on the root node as a side effect.
- Remarks
- To be called only if a the root is a non-const exprt. Do not call on the end() iterator
Definition at line 182 of file expr_iterator.h.
◆ next_sibling_or_parent()
|
inline |
Definition at line 116 of file expr_iterator.h.
◆ operator!=()
|
inline |
Definition at line 86 of file expr_iterator.h.
◆ operator*()
|
inline |
Dereference operator Dereferencing end() iterator is undefined behaviour.
Definition at line 139 of file expr_iterator.h.
◆ operator++() [1/2]
|
inline |
Preincrement operator Do not call on the end() iterator.
Definition at line 94 of file expr_iterator.h.
◆ operator++() [2/2]
|
inline |
Post-increment operator Expensive copy.
Avoid if possible
Definition at line 130 of file expr_iterator.h.
◆ operator->()
|
inline |
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
Definition at line 147 of file expr_iterator.h.
◆ operator=() [1/2]
|
protecteddefault |
◆ operator=() [2/2]
|
inlineprotected |
Definition at line 166 of file expr_iterator.h.
◆ operator==()
|
inline |
Definition at line 79 of file expr_iterator.h.
◆ push_expr()
|
inlineprotected |
Pushes expression onto the stack If overridden, this function should be called from the inheriting class by the override function.
- Returns
- true if element was successfully pushed onto the stack, false otherwise. If returning false, child will not be iterated over.
Definition at line 204 of file expr_iterator.h.
Friends And Related Symbol Documentation
◆ depth_iterator_baset
|
friend |
Definition at line 76 of file expr_iterator.h.
Member Data Documentation
◆ m_stack
|
private |
Definition at line 211 of file expr_iterator.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/util/expr_iterator.h
