Z3
 
Loading...
Searching...
No Matches
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 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.

2975 :
2976 m_solver(s),
2977 m_cutoff(0xFFFFFFFF),
2978 m_default_vars(s.ctx()),
2979 m_vars(m_default_vars)
2980 {}

◆ cube_generator() [2/2]

cube_generator ( solver & s,
expr_vector & vars )
inline

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

2982 :
2983 m_solver(s),
2984 m_cutoff(0xFFFFFFFF),
2985 m_default_vars(s.ctx()),
2986 m_vars(vars)
2987 {}

Member Function Documentation

◆ begin()

cube_iterator begin ( )
inline

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

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

◆ end()

cube_iterator end ( )
inline

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

2990{ 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.

2991{ m_cutoff = c; }