dReal4
|
Multi-thread version of ContractorIbexFwdbwd contractor. More...
#include </home/soonhokong/work/dreal4/dreal/contractor/contractor_ibex_fwdbwd_mt.h>
Public Member Functions | |
ContractorIbexFwdbwdMt ()=delete | |
Deleted default constructor. | |
ContractorIbexFwdbwdMt (Formula f, const Box &box, const Config &config) | |
Constructs IbexFwdbwdMt contractor using f and box . | |
ContractorIbexFwdbwdMt (const ContractorIbexFwdbwdMt &)=delete | |
Deleted copy constructor. | |
ContractorIbexFwdbwdMt (ContractorIbexFwdbwdMt &&)=delete | |
Deleted move constructor. | |
ContractorIbexFwdbwdMt & | operator= (const ContractorIbexFwdbwdMt &)=delete |
Deleted copy assign operator. | |
ContractorIbexFwdbwdMt & | operator= (ContractorIbexFwdbwdMt &&)=delete |
Deleted move assign operator. | |
void | Prune (ContractorStatus *cs) const override |
Performs pruning on cs . | |
std::ostream & | display (std::ostream &os) const override |
Outputs this contractor to os . | |
bool | is_dummy () const |
Returns true if it has no internal ibex contractor. | |
![]() | |
ContractorCell (Contractor::Kind kind, DynamicBitset input, Config config) | |
Constructs a cell with kind and input . | |
ContractorCell ()=delete | |
Deleted default constructor. | |
ContractorCell (const ContractorCell &)=delete | |
Deleted copy constructor. | |
ContractorCell (ContractorCell &&)=delete | |
Deleted move constructor. | |
void | operator= (const ContractorCell &)=delete |
Deleted copy assign operator. | |
void | operator= (ContractorCell &&)=delete |
Deleted move assign operator. | |
virtual | ~ContractorCell ()=default |
Default destructor. | |
Contractor::Kind | kind () const |
Returns its kind. | |
const DynamicBitset & | input () const |
Returns its input. | |
DynamicBitset & | mutable_input () |
Returns its input. | |
const Config & | config () const |
Returns config. | |
bool | include_forall () const |
Returns true if this contractor includes a forall contractor. | |
void | set_include_forall () |
Sets include_forall true. | |
Multi-thread version of ContractorIbexFwdbwd contractor.
The base ContractorIbexFwdbwd is not thread-safe. When there are N jobs, it creates N ContractorIbexFwdbwd instances internally and make sure that each thread calls a designated instance.