Z3
Public Member Functions
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)
 

Detailed Description

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

Constructor & Destructor Documentation

◆ cube_generator() [1/2]

cube_generator ( solver s)
inline

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

2553  :
2554  m_solver(s),
2555  m_cutoff(0xFFFFFFFF),
2556  m_default_vars(s.ctx()),
2557  m_vars(m_default_vars)
2558  {}

◆ cube_generator() [2/2]

cube_generator ( solver s,
expr_vector vars 
)
inline

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

2560  :
2561  m_solver(s),
2562  m_cutoff(0xFFFFFFFF),
2563  m_default_vars(s.ctx()),
2564  m_vars(vars)
2565  {}

Member Function Documentation

◆ begin()

cube_iterator begin ( )
inline

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

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

◆ end()

cube_iterator end ( )
inline

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

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

◆ set_cutoff()

void set_cutoff ( unsigned  c)
inline

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

2569 { m_cutoff = c; }