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

Constructor & Destructor Documentation

cube_generator() [1/2]

cube_generator ( solver &  s )

inline

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

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

cube_generator() [2/2]

cube_generator ( solver &  s, expr_vector &  vars  )

inline

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

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

Member Function Documentation

begin()

cube_iterator begin ( )

inline

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

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

end()

cube_iterator end ( )

inline

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

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

set_cutoff()

void set_cutoff ( unsigned  c )

inlinenoexcept

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

{ m_cutoff = c; }