Z3
 
Loading...
Searching...
No Matches
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) const noexcept
 
bool operator!= (cube_iterator const &other) const noexcept
 

Detailed Description

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

Constructor & Destructor Documentation

◆ cube_iterator()

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

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

2934 :
2935 m_solver(s),
2936 m_cutoff(cutoff),
2937 m_vars(vars),
2938 m_cube(s.ctx()),
2939 m_end(end),
2940 m_empty(false) {
2941 if (!m_end) {
2942 inc();
2943 }
2944 }

Member Function Documentation

◆ operator!=()

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

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

2963 {
2964 return other.m_end != m_end;
2965 };

◆ operator*()

expr_vector const & operator* ( ) const
inlinenoexcept

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

2958{ return m_cube; }

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

◆ operator++() [1/2]

cube_iterator & operator++ ( )
inline

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

2946 {
2947 assert(!m_end);
2948 if (m_empty) {
2949 m_end = true;
2950 }
2951 else {
2952 inc();
2953 }
2954 return *this;
2955 }

◆ operator++() [2/2]

cube_iterator operator++ ( int )
inline

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

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

◆ operator->()

expr_vector const * operator-> ( ) const
inline

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

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

◆ operator==()

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

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

2960 {
2961 return other.m_end == m_end;
2962 };