Z3
 
Loading...
Searching...
No Matches
Public Member Functions
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
 
iterator & operator++ ()
 
iterator operator++ (int)
 

Detailed Description

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

Constructor & Destructor Documentation

◆ iterator()

iterator ( expr &  e,
unsigned  i 
)
inline

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

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

Member Function Documentation

◆ operator!=()

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

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

1833 {
1834 return i != other.i;
1835 }

◆ operator*()

expr operator* ( ) const
inline

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

1836{ return e.arg(i); }
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition z3++.h:1403

◆ operator++() [1/2]

iterator & operator++ ( )
inline

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

1837{ ++i; return *this; }

◆ operator++() [2/2]

iterator operator++ ( int  )
inline

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

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

◆ operator==()

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

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

1830 {
1831 return i == other.i;
1832 }