solver::cube_generator Class Reference

#include <z3++.h>

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

Constructor & Destructor Documentation

cube_generator() [1/2]

cube_generator ( solver & s )

inline

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

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

Referenced by solver::cubes(), and solver::cubes().

cube_generator() [2/2]

cube_generator ( solver & s, expr_vector & vars )

inline

Definition at line 3367 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 3374 of file z3++.h.

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

end()

cube_iterator end ( )

inline

Definition at line 3375 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 3376 of file z3++.h.

{ m_cutoff = c; }