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_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 2681 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ cube_iterator()

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

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

2702 :
2703 m_solver(s),
2704 m_cutoff(cutoff),
2705 m_vars(vars),
2706 m_cube(s.ctx()),
2707 m_end(end),
2708 m_empty(false) {
2709 if (!m_end) {
2710 inc();
2711 }
2712 }

## Member Function Documentation

## ◆ operator!=()

bool operator!= | ( | cube_iterator const & | other | ) |
| inline noexcept

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

2731 {
2732 return other.m_end != m_end;
2733 };

## ◆ operator*()

expr_vector const & operator* | ( |  | ) | const
| inline noexcept

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

2726{ return m_cube; }

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

## ◆ operator++() [1/2]

cube_iterator & operator++ | ( |  | ) |
| inline

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

2714 {
2715 assert(!m_end);
2716 if (m_empty) {
2717 m_end = true;
2718 }
2719 else {
2720 inc();
2721 }
2722 return *this;
2723 }

## ◆ operator++() [2/2]

cube_iterator operator++ | ( | int |  | ) |
| inline

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

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

## ◆ operator->()

expr_vector const * operator-> | ( |  | ) | const
| inline

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

2725{ return &(operator*()); }
z3::solver::cube_iterator::operator*
expr_vector const & operator*() const noexcept
Definition: z3++.h:2726

## ◆ operator==()

bool operator== | ( | cube_iterator const & | other | ) |
| inline noexcept

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

2728 {
2729 return other.m_end == m_end;
2730 };