Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 2405 of file z3++.h.

Constructor & Destructor Documentation

cube_generator ( solver s)
inline

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

2411  :
2412  m_solver(s),
2413  m_cutoff(0xFFFFFFFF),
2414  m_default_vars(s.ctx()),
2415  m_vars(m_default_vars)
2416  {}
cube_generator ( solver s,
expr_vector vars 
)
inline

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

2418  :
2419  m_solver(s),
2420  m_cutoff(0xFFFFFFFF),
2421  m_default_vars(s.ctx()),
2422  m_vars(vars)
2423  {}

Member Function Documentation

cube_iterator begin ( )
inline

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

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

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

2426 { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
void set_cutoff ( unsigned  c)
inline

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

2427 { m_cutoff = c; }