Z3
Public Member Functions
solver::cube_iterator Class Reference

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

Constructor & Destructor Documentation

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

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

2894  :
2895  m_solver(s),
2896  m_cutoff(cutoff),
2897  m_vars(vars),
2898  m_cube(s.ctx()),
2899  m_end(end),
2900  m_empty(false) {
2901  if (!m_end) {
2902  inc();
2903  }
2904  }

Member Function Documentation

bool operator!= ( cube_iterator const &  other)
inlinenoexcept

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

2923  {
2924  return other.m_end != m_end;
2925  };
expr_vector const& operator* ( ) const
inlinenoexcept

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

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

2918 { return m_cube; }
cube_iterator& operator++ ( )
inline

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

2906  {
2907  assert(!m_end);
2908  if (m_empty) {
2909  m_end = true;
2910  }
2911  else {
2912  inc();
2913  }
2914  return *this;
2915  }
cube_iterator operator++ ( int  )
inline

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

2916 { assert(false); return *this; }
expr_vector const* operator-> ( ) const
inline

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

2917 { return &(operator*()); }
expr_vector const & operator*() const noexcept
Definition: z3++.h:2918
bool operator== ( cube_iterator const &  other)
inlinenoexcept

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

2920  {
2921  return other.m_end == m_end;
2922  };