cprover
Loading...
Searching...
No Matches
const_post_depth_iteratort Class Referencefinal

Post-order depth-first-search iterator. More...

#include <expr_iterator.h>

Collaboration diagram for const_post_depth_iteratort:

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

 const_post_depth_iteratort (const exprt &expr)
 Create iterator starting at the supplied node (root).
 const_post_depth_iteratort ()=default
 Create an end iterator.
bool operator== (const const_post_depth_iteratort &other) const
bool operator!= (const const_post_depth_iteratort &other) const
const_post_depth_iteratortoperator++ ()
 Preincrement operator Do not call on the end() iterator.
const_post_depth_iteratort operator++ (int)
 Post-increment operator Expensive copy.
const exprtoperator* () const
 Dereference operator Dereferencing end() iterator is undefined behaviour.
const exprtoperator-> () const
 Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.

Private Member Functions

void descend_to_leftmost_leaf (const exprt &expr)
 Descend from the given expression to its leftmost leaf, pushing all nodes along the path onto the stack.

Private Attributes

std::deque< depth_iterator_expr_statetm_stack

Detailed Description

Post-order depth-first-search iterator.

Visits all children before visiting the parent node. For expression (a + (b * c)), visits: a, b, c, *, +

Definition at line 342 of file expr_iterator.h.

Member Typedef Documentation

◆ difference_type

Definition at line 345 of file expr_iterator.h.

◆ iterator_category

typedef std::forward_iterator_tag const_post_depth_iteratort::iterator_category

Definition at line 349 of file expr_iterator.h.

◆ pointer

Definition at line 347 of file expr_iterator.h.

◆ reference

Definition at line 348 of file expr_iterator.h.

◆ value_type

Definition at line 346 of file expr_iterator.h.

Constructor & Destructor Documentation

◆ const_post_depth_iteratort() [1/2]

const_post_depth_iteratort::const_post_depth_iteratort ( const exprt & expr)
inlineexplicit

Create iterator starting at the supplied node (root).

Immediately descends to the leftmost leaf.

Definition at line 353 of file expr_iterator.h.

◆ const_post_depth_iteratort() [2/2]

const_post_depth_iteratort::const_post_depth_iteratort ( )
default

Create an end iterator.

Member Function Documentation

◆ descend_to_leftmost_leaf()

void const_post_depth_iteratort::descend_to_leftmost_leaf ( const exprt & expr)
inlineprivate

Descend from the given expression to its leftmost leaf, pushing all nodes along the path onto the stack.

Definition at line 424 of file expr_iterator.h.

◆ operator!=()

bool const_post_depth_iteratort::operator!= ( const const_post_depth_iteratort & other) const
inline

Definition at line 366 of file expr_iterator.h.

◆ operator*()

const exprt & const_post_depth_iteratort::operator* ( ) const
inline

Dereference operator Dereferencing end() iterator is undefined behaviour.

Definition at line 408 of file expr_iterator.h.

◆ operator++() [1/2]

const_post_depth_iteratort & const_post_depth_iteratort::operator++ ( )
inline

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

Definition at line 373 of file expr_iterator.h.

◆ operator++() [2/2]

const_post_depth_iteratort const_post_depth_iteratort::operator++ ( int )
inline

Post-increment operator Expensive copy.

Avoid if possible

Definition at line 399 of file expr_iterator.h.

◆ operator->()

const exprt * const_post_depth_iteratort::operator-> ( ) const
inline

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

Definition at line 416 of file expr_iterator.h.

◆ operator==()

bool const_post_depth_iteratort::operator== ( const const_post_depth_iteratort & other) const
inline

Definition at line 361 of file expr_iterator.h.

Member Data Documentation

◆ m_stack

std::deque<depth_iterator_expr_statet> const_post_depth_iteratort::m_stack
private

Definition at line 436 of file expr_iterator.h.


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