dReal4
Public Types | Public Member Functions | Static Public Attributes | List of all members
Config Class Reference

Public Types

using Brancher = std::function< int(const Box &box, const DynamicBitset &bitset, Box *left, Box *right)>
 

Public Member Functions

 Config (const Config &)=default
 
 Config (Config &&)=default
 
Config & operator= (const Config &)=default
 
Config & operator= (Config &&)=default
 
double precision () const
 Returns the precision option.
 
OptionValue< double > & mutable_precision ()
 Returns a mutable OptionValue for 'precision'.
 
bool produce_models () const
 Returns the produce_models option.
 
OptionValue< bool > & mutable_produce_models ()
 Returns a mutable OptionValue for 'produce_models'.
 
bool use_polytope () const
 Returns whether it uses polytope contractors or not.
 
OptionValue< bool > & mutable_use_polytope ()
 Returns a mutable OptionValue for 'use_polytope'.
 
bool use_polytope_in_forall () const
 Returns whether it uses polytope contractors inside forall contractors.
 
OptionValue< bool > & mutable_use_polytope_in_forall ()
 Returns a mutable OptionValue for 'use_polytope_in_forall'.
 
bool use_worklist_fixpoint () const
 Returns whether it uses worklist-fixpoint algorithm.
 
OptionValue< bool > & mutable_use_worklist_fixpoint ()
 Returns a mutable OptionValue for 'use_worklist_fixpoint'.
 
bool use_local_optimization () const
 Returns whether it uses local optimization algorithm in exist-forall problems. More...
 
OptionValue< bool > & mutable_use_local_optimization ()
 Returns a mutable OptionValue for 'use_local_optimization'.
 
int number_of_jobs () const
 Returns the number of parallel jobs.
 
OptionValue< int > & mutable_number_of_jobs ()
 Returns a mutable OptionValue for 'number_of_jobs'.
 
bool stack_left_box_first () const
 Returns whether the ICP algorithm stacks the left box first after branching. More...
 
OptionValue< bool > & mutable_stack_left_box_first ()
 Returns a mutable OptionValue for 'stack_left_box_first'.
 
const Brancher & brancher () const
 Returns the brancher.
 
OptionValue< Brancher > & mutable_brancher ()
 Returns a mutable OptionValue for brancher.
 

Static Public Attributes

static constexpr double kDefaultPrecision {0.001}
 
static constexpr double kDefaultNloptFtolRel {1e-6}
 
static constexpr double kDefaultNloptFtolAbs {1e-6}
 
static constexpr int kDefaultNloptMaxEval {100}
 
static constexpr double kDefaultNloptMaxTime {0.01}
 

NLopt Options

Specifies stopping criteria of NLopt.

See https://nlopt.readthedocs.io/en/latest/NLopt_Reference/#stopping-criteria for more information.

enum  SatDefaultPhase { False = 0, True = 1, JeroslowWang = 2, RandomInitialPhase = 3 }
 
double nlopt_ftol_rel () const
 Returns relative tolerance on function value in NLopt.
 
OptionValue< double > & mutable_nlopt_ftol_rel ()
 Returns a mutable OptionValue for nlopt_ftol_rel.
 
double nlopt_ftol_abs () const
 Returns absolute tolerance on function value in NLopt.
 
OptionValue< double > & mutable_nlopt_ftol_abs ()
 Returns a mutable OptionValue for nlopt_ftol_abs.
 
int nlopt_maxeval () const
 
OptionValue< int > & mutable_nlopt_maxeval ()
 Returns a mutable OptionValue for nlopt_maxeval.
 
double nlopt_maxtime () const
 Returns the maxtime in NLopt.
 
OptionValue< double > & mutable_nlopt_maxtime ()
 Returns a mutable OptionValue for nlopt_maxtime.
 
SatDefaultPhase sat_default_phase () const
 Returns the default phase for SAT solver.
 
OptionValue< SatDefaultPhase > & mutable_sat_default_phase ()
 Returns a mutable OptionValue for sat_default_phase.
 
uint32_t random_seed () const
 Returns the random seed.
 
OptionValue< uint32_t > & mutable_random_seed ()
 Returns a mutable OptionValue for random_seed.
 
bool smtlib2_compliant () const
 Returns if it's smtlib2_compliant mode.
 
OptionValue< bool > & mutable_smtlib2_compliant ()
 Returns a mutable OptionValue for smtlib2_compliant.
 

Member Function Documentation

◆ stack_left_box_first()

bool stack_left_box_first ( ) const

Returns whether the ICP algorithm stacks the left box first after branching.

◆ use_local_optimization()

bool use_local_optimization ( ) const

Returns whether it uses local optimization algorithm in exist-forall problems.

The documentation for this class was generated from the following files: