cprover
depth_iteratort Class Referencefinal

#include <expr_iterator.h>

+ Inheritance diagram for depth_iteratort:
+ Collaboration diagram for depth_iteratort:

Public Member Functions

 depth_iteratort ()=default
 Create an end iterator. More...
 
 depth_iteratort (exprt &expr)
 Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflected on this node. More...
 
 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 then the passed mutate_root function will be called to get a non-const copy of the same root on which the mutations will be done. More...
 
exprtmutate ()
 Obtain non-const reference to the exprt instance currently pointed to by the iterator. More...
 
- Public Member Functions inherited from depth_iterator_baset< depth_iteratort >
bool operator== (const depth_iterator_baset< other_depth_iterator_t > &other) const
 
bool operator!= (const depth_iterator_baset< other_depth_iterator_t > &other) const
 
depth_iteratortoperator++ ()
 Preincrement operator Do not call on the end() iterator. More...
 
depth_iteratort operator++ (int)
 Post-increment operator Expensive copy. More...
 
depth_iteratortnext_sibling_or_parent ()
 
const exprtoperator* () const
 Dereference operator Dereferencing end() iterator is undefined behaviour. More...
 
const exprtoperator-> () const
 Dereference operator (member access) Dereferencing end() iterator is undefined behaviour. More...
 

Private Attributes

std::function< exprt &()> mutate_root
 If this is non-empty then the root is currently const and this function must be called before any mutations occur. More...
 

Additional Inherited Members

- Public Types inherited from depth_iterator_baset< depth_iteratort >
typedef void difference_type
 
typedef exprt value_type
 
typedef const exprtpointer
 
typedef const exprtreference
 
typedef std::forward_iterator_tag iterator_category
 
- Protected Member Functions inherited from depth_iterator_baset< depth_iteratort >
 depth_iterator_baset ()=default
 Create end iterator. More...
 
 depth_iterator_baset (const exprt &root)
 Create begin iterator, starting at the supplied node. More...
 
 depth_iterator_baset (const depth_iterator_baset &)=default
 
 depth_iterator_baset (depth_iterator_baset &&other)
 
 ~depth_iterator_baset ()=default
 Destructor Protected to discourage upcasting. More...
 
depth_iterator_basetoperator= (const depth_iterator_baset &)=default
 
depth_iterator_basetoperator= (depth_iterator_baset &&other)
 
const exprtget_root ()
 
exprtmutate ()
 Obtain non-const exprt reference. More...
 
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. More...
 

Detailed Description

Definition at line 235 of file expr_iterator.h.

Constructor & Destructor Documentation

◆ depth_iteratort() [1/3]

depth_iteratort::depth_iteratort ( )
default

Create an end iterator.

◆ depth_iteratort() [2/3]

depth_iteratort::depth_iteratort ( exprt expr)
inlineexplicit

Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflected on this node.

Parameters
exprThe root node to begin iteration at

Definition at line 250 of file expr_iterator.h.

◆ depth_iteratort() [3/3]

depth_iteratort::depth_iteratort ( const exprt expr,
std::function< exprt &()>  mutate_root 
)
inlineexplicit

Create iterator starting at the supplied node (root) If mutations of the child nodes are required then the passed mutate_root function will be called to get a non-const copy of the same root on which the mutations will be done.

Parameters
exprThe root node to begin iteration at
mutate_rootThe function to call to get a non-const copy of the same root expression passed in the expr parameter

Definition at line 261 of file expr_iterator.h.

Member Function Documentation

◆ mutate()

exprt& depth_iteratort::mutate ( )
inline

Obtain non-const reference to the exprt instance currently pointed to by the iterator.

If the iterator is currently using a const root exprt then calls mutate_root to get a non-const root and copies it if it is shared

Returns
A non-const reference to the element this iterator is currently pointing to

Definition at line 277 of file expr_iterator.h.

Member Data Documentation

◆ mutate_root

std::function<exprt &()> depth_iteratort::mutate_root
private

If this is non-empty then the root is currently const and this function must be called before any mutations occur.

Definition at line 241 of file expr_iterator.h.


The documentation for this class was generated from the following file: