solver::cube_iterator Class Reference

Public Member Functions
	cube_iterator (solver &s, expr_vector &vars, unsigned &cutoff, bool end)
cube_iterator &	operator++ ()
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 2812 of file z3++.h.

Constructor & Destructor Documentation

cube_iterator()

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

inline

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

                                                                                   :
                m_solver(s),
                m_cutoff(cutoff),
                m_vars(vars),
                m_cube(s.ctx()),
                m_end(end),
                m_empty(false) {
                if (!m_end) {
                    inc();
                }
            }

Member Function Documentation

operator!=()

bool operator!= ( cube_iterator const &  other )

inlinenoexcept

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

                                                                 {
                return other.m_end != m_end;
            };

operator*()

expr_vector const& operator* ( ) const

inlinenoexcept

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

{ return m_cube; }

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

operator++() [1/2]

cube_iterator& operator++ ( )

inline

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

                                        {
                assert(!m_end);
                if (m_empty) {
                    m_end = true;
                }
                else {
                    inc();
                }
                return *this;
            }

operator++() [2/2]

cube_iterator operator++ ( int  )

inline

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

{ assert(false); return *this; }

operator->()

expr_vector const* operator-> ( ) const

inline

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

{ return &(operator*()); }

operator==()

bool operator== ( cube_iterator const &  other )

inlinenoexcept

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

                                                                 {
                return other.m_end == m_end;
            };