CBMC
depth_iterator_baset< depth_iterator_t > Class Template Reference

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 exprtpointer
 
typedef const exprtreference
 
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. More...
 
depth_iterator_t & next_sibling_or_parent ()
 
depth_iterator_t operator++ (int)
 Post-increment operator Expensive copy. More...
 
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...
 

Protected Member Functions

 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 ()=default
 Destructor Protected to discourage upcasting. More...
 
 depth_iterator_baset (const depth_iterator_baset &)=default
 
 depth_iterator_baset (depth_iterator_baset &&other)
 
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...
 

Private Member Functions

depth_iterator_t & downcast ()
 

Private Attributes

std::deque< depth_iterator_expr_statetm_stack
 

Friends

template<typename other_depth_iterator_t >
class depth_iterator_baset
 

Detailed Description

template<typename depth_iterator_t>
class depth_iterator_baset< depth_iterator_t >

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

template<typename depth_iterator_t >
typedef void depth_iterator_baset< depth_iterator_t >::difference_type

Definition at line 69 of file expr_iterator.h.

◆ iterator_category

template<typename depth_iterator_t >
typedef std::forward_iterator_tag depth_iterator_baset< depth_iterator_t >::iterator_category

Definition at line 73 of file expr_iterator.h.

◆ pointer

template<typename depth_iterator_t >
typedef const exprt* depth_iterator_baset< depth_iterator_t >::pointer

Definition at line 71 of file expr_iterator.h.

◆ reference

template<typename depth_iterator_t >
typedef const exprt& depth_iterator_baset< depth_iterator_t >::reference

Definition at line 72 of file expr_iterator.h.

◆ value_type

template<typename depth_iterator_t >
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]

template<typename depth_iterator_t >
depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( )
protecteddefault

Create end iterator.

◆ depth_iterator_baset() [2/4]

template<typename depth_iterator_t >
depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( const exprt root)
inlineexplicitprotected

Create begin iterator, starting at the supplied node.

Definition at line 155 of file expr_iterator.h.

◆ ~depth_iterator_baset()

template<typename depth_iterator_t >
depth_iterator_baset< depth_iterator_t >::~depth_iterator_baset ( )
protecteddefault

Destructor Protected to discourage upcasting.

◆ depth_iterator_baset() [3/4]

template<typename depth_iterator_t >
depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( const depth_iterator_baset< depth_iterator_t > &  )
protecteddefault

◆ depth_iterator_baset() [4/4]

template<typename depth_iterator_t >
depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( depth_iterator_baset< depth_iterator_t > &&  other)
inlineprotected

Definition at line 163 of file expr_iterator.h.

Member Function Documentation

◆ downcast()

template<typename depth_iterator_t >
depth_iterator_t& depth_iterator_baset< depth_iterator_t >::downcast ( )
inlineprivate

Definition at line 213 of file expr_iterator.h.

◆ get_root()

template<typename depth_iterator_t >
const exprt& depth_iterator_baset< depth_iterator_t >::get_root ( )
inlineprotected

Definition at line 172 of file expr_iterator.h.

◆ mutate()

template<typename depth_iterator_t >
exprt& depth_iterator_baset< depth_iterator_t >::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()

template<typename depth_iterator_t >
depth_iterator_t& depth_iterator_baset< depth_iterator_t >::next_sibling_or_parent ( )
inline

Definition at line 116 of file expr_iterator.h.

◆ operator!=()

template<typename depth_iterator_t >
template<typename other_depth_iterator_t >
bool depth_iterator_baset< depth_iterator_t >::operator!= ( const depth_iterator_baset< other_depth_iterator_t > &  other) const
inline

Definition at line 86 of file expr_iterator.h.

◆ operator*()

template<typename depth_iterator_t >
const exprt& depth_iterator_baset< depth_iterator_t >::operator* ( ) const
inline

Dereference operator Dereferencing end() iterator is undefined behaviour.

Definition at line 139 of file expr_iterator.h.

◆ operator++() [1/2]

template<typename depth_iterator_t >
depth_iterator_t& depth_iterator_baset< depth_iterator_t >::operator++ ( )
inline

Preincrement operator Do not call on the end() iterator.

Definition at line 94 of file expr_iterator.h.

◆ operator++() [2/2]

template<typename depth_iterator_t >
depth_iterator_t depth_iterator_baset< depth_iterator_t >::operator++ ( int  )
inline

Post-increment operator Expensive copy.

Avoid if possible

Definition at line 130 of file expr_iterator.h.

◆ operator->()

template<typename depth_iterator_t >
const exprt* depth_iterator_baset< depth_iterator_t >::operator-> ( ) const
inline

Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.

Definition at line 147 of file expr_iterator.h.

◆ operator=() [1/2]

template<typename depth_iterator_t >
depth_iterator_baset& depth_iterator_baset< depth_iterator_t >::operator= ( const depth_iterator_baset< depth_iterator_t > &  )
protecteddefault

◆ operator=() [2/2]

template<typename depth_iterator_t >
depth_iterator_baset& depth_iterator_baset< depth_iterator_t >::operator= ( depth_iterator_baset< depth_iterator_t > &&  other)
inlineprotected

Definition at line 166 of file expr_iterator.h.

◆ operator==()

template<typename depth_iterator_t >
template<typename other_depth_iterator_t >
bool depth_iterator_baset< depth_iterator_t >::operator== ( const depth_iterator_baset< other_depth_iterator_t > &  other) const
inline

Definition at line 79 of file expr_iterator.h.

◆ push_expr()

template<typename depth_iterator_t >
bool depth_iterator_baset< depth_iterator_t >::push_expr ( const exprt 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 Function Documentation

◆ depth_iterator_baset

template<typename depth_iterator_t >
template<typename other_depth_iterator_t >
friend class depth_iterator_baset
friend

Definition at line 76 of file expr_iterator.h.

Member Data Documentation

◆ m_stack

template<typename depth_iterator_t >
std::deque<depth_iterator_expr_statet> depth_iterator_baset< depth_iterator_t >::m_stack
private

Definition at line 211 of file expr_iterator.h.


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