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
 
bool operator== (cube_iterator const &other)
 
bool operator!= (cube_iterator const &other)
 

Detailed Description

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

Constructor & Destructor Documentation

◆ cube_iterator()

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

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

2515  :
2516  m_solver(s),
2517  m_cutoff(cutoff),
2518  m_vars(vars),
2519  m_cube(s.ctx()),
2520  m_end(end),
2521  m_empty(false) {
2522  if (!m_end) {
2523  inc();
2524  }
2525  }

Member Function Documentation

◆ operator!=()

bool operator!= ( cube_iterator const &  other)
inline

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

2544  {
2545  return other.m_end != m_end;
2546  };

◆ operator*()

expr_vector const& operator* ( ) const
inline

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

2539 { return m_cube; }

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

◆ operator++() [1/2]

cube_iterator& operator++ ( )
inline

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

2527  {
2528  assert(!m_end);
2529  if (m_empty) {
2530  m_end = true;
2531  }
2532  else {
2533  inc();
2534  }
2535  return *this;
2536  }

◆ operator++() [2/2]

cube_iterator operator++ ( int  )
inline

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

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

◆ operator->()

expr_vector const* operator-> ( ) const
inline

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

2538 { return &(operator*()); }

◆ operator==()

bool operator== ( cube_iterator const &  other)
inline

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

2541  {
2542  return other.m_end == m_end;
2543  };
z3::solver::cube_iterator::operator*
expr_vector const & operator*() const
Definition: z3++.h:2539