cprover
Loading...
Searching...
No Matches
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)
 const_unique_depth_iteratort ()=default
 Create an end iterator.
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.
const_unique_depth_iteratortnext_sibling_or_parent ()
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

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

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

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: