solver::cube_generator Class Reference

Public Member Functions
	cube_generator (solver &s)
	cube_generator (solver &s, expr_vector &vars)
cube_iterator	begin ()
cube_iterator	end ()
void	set_cutoff (unsigned c) noexcept

Detailed Description

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

Constructor & Destructor Documentation

cube_generator ( solver &  s )

inline

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

                                     :
                m_solver(s),
                m_cutoff(0xFFFFFFFF),
                m_default_vars(s.ctx()),
                m_vars(m_default_vars)
            {}

cube_generator ( solver &  s, expr_vector &  vars  )

inline

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

                                                        :
                m_solver(s),
                m_cutoff(0xFFFFFFFF),
                m_default_vars(s.ctx()),
                m_vars(vars)
            {}

Member Function Documentation

cube_iterator begin ( )

inline

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

{ return cube_iterator(m_solver, m_vars, m_cutoff, false); }

cube_iterator end ( )

inline

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

{ return cube_iterator(m_solver, m_vars, m_cutoff, true); }

void set_cutoff ( unsigned  c )

inlinenoexcept

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

{ m_cutoff = c; }