Z3
Loading...
Searching...
No Matches
expr::iterator Class Reference

#include <z3++.h>

Public Member Functions

 iterator (expr &e, unsigned i)
bool operator== (iterator const &other) const noexcept
bool operator!= (iterator const &other) const noexcept
expr operator* () const
iteratoroperator++ ()
iterator operator++ (int)

Detailed Description

Definition at line 1688 of file z3++.h.

Constructor & Destructor Documentation

◆ iterator()

iterator ( expr & e,
unsigned i )
inline

Definition at line 1692 of file z3++.h.

1692: e(e), i(i) {}

Referenced by operator!=(), operator++(), operator++(), and operator==().

Member Function Documentation

◆ operator!=()

bool operator!= ( iterator const & other) const
inlinenoexcept

Definition at line 1696 of file z3++.h.

1696 {
1697 return i != other.i;
1698 }

◆ operator*()

expr operator* ( ) const
inline

Definition at line 1699 of file z3++.h.

1699{ return e.arg(i); }

◆ operator++() [1/2]

iterator & operator++ ( )
inline

Definition at line 1700 of file z3++.h.

1700{ ++i; return *this; }

◆ operator++() [2/2]

iterator operator++ ( int )
inline

Definition at line 1701 of file z3++.h.

1701{ assert(false); return *this; }

◆ operator==()

bool operator== ( iterator const & other) const
inlinenoexcept

Definition at line 1693 of file z3++.h.

1693 {
1694 return i == other.i;
1695 }