Z3
Public Member Functions
expr::iterator Class Reference

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 ( expr e,
unsigned  i 
)
inline

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

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

Member Function Documentation

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

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

1696  {
1697  return i != other.i;
1698  }
expr operator* ( ) const
inline

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

1699 { 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:1274
iterator& operator++ ( )
inline

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

1700 { ++i; return *this; }
iterator operator++ ( int  )
inline

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

1701 { assert(false); return *this; }
bool operator== ( iterator const &  other) const
inlinenoexcept

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

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