Z3
Public Member Functions
solver::cube_iterator Class Reference

#include <z3++.h>

Public Member Functions

 cube_iterator (solver &s, expr_vector &vars, unsigned &cutoff, bool end)
 
cube_iteratoroperator++ ()
 
cube_iterator operator++ (int)
 
expr_vector const * operator-> () const
 
expr_vector const & operator* () const noexcept
 
bool operator== (cube_iterator const &other) noexcept
 
bool operator!= (cube_iterator const &other) noexcept
 

Detailed Description

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

Constructor & Destructor Documentation

◆ cube_iterator()

cube_iterator ( solver s,
expr_vector vars,
unsigned &  cutoff,
bool  end 
)
inline

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

2814 :
2815 m_solver(s),
2816 m_cutoff(cutoff),
2817 m_vars(vars),
2818 m_cube(s.ctx()),
2819 m_end(end),
2820 m_empty(false) {
2821 if (!m_end) {
2822 inc();
2823 }
2824 }

Member Function Documentation

◆ operator!=()

bool operator!= ( cube_iterator const &  other)
inlinenoexcept

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

2843 {
2844 return other.m_end != m_end;
2845 };

◆ operator*()

expr_vector const & operator* ( ) const
inlinenoexcept

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

2838{ return m_cube; }

Referenced by solver::cube_iterator::operator->().

◆ operator++() [1/2]

cube_iterator & operator++ ( )
inline

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

2826 {
2827 assert(!m_end);
2828 if (m_empty) {
2829 m_end = true;
2830 }
2831 else {
2832 inc();
2833 }
2834 return *this;
2835 }

◆ operator++() [2/2]

cube_iterator operator++ ( int  )
inline

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

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

◆ operator->()

expr_vector const * operator-> ( ) const
inline

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

2837{ return &(operator*()); }
expr_vector const & operator*() const noexcept
Definition: z3++.h:2838

◆ operator==()

bool operator== ( cube_iterator const &  other)
inlinenoexcept

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

2840 {
2841 return other.m_end == m_end;
2842 };