Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
 
bool operator== (cube_iterator const &other)
 
bool operator!= (cube_iterator const &other)
 

Detailed Description

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

Constructor & Destructor Documentation

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

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

2370  :
2371  m_solver(s),
2372  m_cutoff(cutoff),
2373  m_vars(vars),
2374  m_cube(s.ctx()),
2375  m_end(end),
2376  m_empty(false) {
2377  if (!m_end) {
2378  inc();
2379  }
2380  }

Member Function Documentation

bool operator!= ( cube_iterator const &  other)
inline

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

2399  {
2400  return other.m_end != m_end;
2401  };
expr_vector const& operator* ( ) const
inline

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

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

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

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

2382  {
2383  assert(!m_end);
2384  if (m_empty) {
2385  m_end = true;
2386  }
2387  else {
2388  inc();
2389  }
2390  return *this;
2391  }
cube_iterator operator++ ( int  )
inline

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

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

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

2393 { return &(operator*()); }
expr_vector const & operator*() const
Definition: z3++.h:2394
bool operator== ( cube_iterator const &  other)
inline

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

2396  {
2397  return other.m_end == m_end;
2398  };