CBMC
const_unique_depth_iteratort Class Referencefinal

#include <expr_iterator.h>

+ Inheritance diagram for const_unique_depth_iteratort:
+ Collaboration diagram for const_unique_depth_iteratort:

Public Member Functions

 const_unique_depth_iteratort (const exprt &expr)
 Create iterator starting at the supplied node (root) More...
 
 const_unique_depth_iteratort ()=default
 Create an end iterator. More...
 
- Public Member Functions inherited from depth_iterator_baset< const_unique_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
 
const_unique_depth_iteratortoperator++ ()
 Preincrement operator Do not call on the end() iterator. More...
 
const_unique_depth_iteratort operator++ (int)
 Post-increment operator Expensive copy. More...
 
const_unique_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 Member Functions

bool push_expr (const exprt &expr)
 Push expression onto the stack and add to the set of traversed exprts. More...
 

Private Attributes

friend depth_iterator_baset
 
std::set< exprtm_traversed
 

Additional Inherited Members

- Public Types inherited from depth_iterator_baset< const_unique_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< const_unique_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 285 of file expr_iterator.h.

Constructor & Destructor Documentation

◆ const_unique_depth_iteratort() [1/2]

const_unique_depth_iteratort::const_unique_depth_iteratort ( const exprt expr)
inlineexplicit

Create iterator starting at the supplied node (root)

Definition at line 291 of file expr_iterator.h.

◆ const_unique_depth_iteratort() [2/2]

const_unique_depth_iteratort::const_unique_depth_iteratort ( )
default

Create an end iterator.

Member Function Documentation

◆ push_expr()

bool const_unique_depth_iteratort::push_expr ( const exprt expr)
inlineprivate

Push expression onto the stack and add to the set of traversed exprts.

Definition at line 298 of file expr_iterator.h.

Member Data Documentation

◆ depth_iterator_baset

friend const_unique_depth_iteratort::depth_iterator_baset
private

Definition at line 288 of file expr_iterator.h.

◆ m_traversed

std::set<exprt> const_unique_depth_iteratort::m_traversed
private

Definition at line 305 of file expr_iterator.h.


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