Drake
DrealSolver Class Reference

#include <drake/solvers/dreal_solver.h>

Public Types

enum  LocalOptimization { kUse, kNotUse }
 Indicates whether to use dReal's –local-optimization option or not. More...
 
using Interval = dreal::Box::Interval
 
using IntervalBox = std::unordered_map< symbolic::Variable, Interval >
 

Public Member Functions

 DrealSolver ()=default
 
 ~DrealSolver () override=default
 
bool available () const override
 Returns true iff this solver was enabled at compile-time. More...
 
SolutionResult Solve (MathematicalProgram &prog) const override
 Sets values for the decision variables on the given MathematicalProgram prog, or: More...
 
void Solve (const MathematicalProgram &prog, const optional< Eigen::VectorXd > &initial_guess, const optional< SolverOptions > &solver_options, MathematicalProgramResult *result) const override
 Solves an optimization program with optional initial guess and solver options. More...
 
SolverId solver_id () const override
 Returns the identifier of this solver. More...
 
bool AreProgramAttributesSatisfied (const MathematicalProgram &prog) const override
 Returns true if the program attributes are satisfied by the solver's capability. More...
 
Does not allow copy, move, or assignment
 DrealSolver (const DrealSolver &)=delete
 
DrealSolveroperator= (const DrealSolver &)=delete
 
 DrealSolver (DrealSolver &&)=delete
 
DrealSolveroperator= (DrealSolver &&)=delete
 
- Public Member Functions inherited from MathematicalProgramSolverInterface
 MathematicalProgramSolverInterface ()=default
 
virtual ~MathematicalProgramSolverInterface ()=default
 
 MathematicalProgramSolverInterface (const MathematicalProgramSolverInterface &)=delete
 
MathematicalProgramSolverInterfaceoperator= (const MathematicalProgramSolverInterface &)=delete
 
 MathematicalProgramSolverInterface (MathematicalProgramSolverInterface &&)=delete
 
MathematicalProgramSolverInterfaceoperator= (MathematicalProgramSolverInterface &&)=delete
 

Static Public Member Functions

static bool is_available ()
 
static SolverId id ()
 
static bool ProgramAttributesSatisfied (const MathematicalProgram &prog)
 
static optional< IntervalBoxCheckSatisfiability (const symbolic::Formula &f, double delta)
 Checks the satisfiability of a given formula f with a given precision delta. More...
 
static optional< IntervalBoxMinimize (const symbolic::Expression &objective, const symbolic::Formula &constraint, double delta, LocalOptimization local_optimization)
 Finds a solution to minimize objective function while satisfying a given constraint using delta. More...
 

Member Typedef Documentation

◆ Interval

using Interval = dreal::Box::Interval

◆ IntervalBox

using IntervalBox = std::unordered_map<symbolic::Variable, Interval>

Member Enumeration Documentation

◆ LocalOptimization

enum LocalOptimization
strong

Indicates whether to use dReal's –local-optimization option or not.

Enumerator
kUse 

Use "--local-optimization" option.

kNotUse 

Do not use "--local-optimization" option.

Constructor & Destructor Documentation

◆ DrealSolver() [1/3]

DrealSolver ( const DrealSolver )
delete

◆ DrealSolver() [2/3]

DrealSolver ( DrealSolver &&  )
delete

◆ DrealSolver() [3/3]

DrealSolver ( )
default

◆ ~DrealSolver()

~DrealSolver ( )
overridedefault

Member Function Documentation

◆ AreProgramAttributesSatisfied()

bool AreProgramAttributesSatisfied ( const MathematicalProgram prog) const
overridevirtual

Returns true if the program attributes are satisfied by the solver's capability.

Implements MathematicalProgramSolverInterface.

◆ available()

bool available ( ) const
inlineoverridevirtual

Returns true iff this solver was enabled at compile-time.

Implements MathematicalProgramSolverInterface.

◆ CheckSatisfiability()

optional< DrealSolver::IntervalBox > CheckSatisfiability ( const symbolic::Formula f,
double  delta 
)
static

Checks the satisfiability of a given formula f with a given precision delta.

Returns
a model, a mapping from a variable to an interval, if f is δ-satisfiable.
a nullopt, if is unsatisfiable.

◆ id()

◆ is_available()

bool is_available ( )
static

◆ Minimize()

optional< DrealSolver::IntervalBox > Minimize ( const symbolic::Expression objective,
const symbolic::Formula constraint,
double  delta,
LocalOptimization  local_optimization 
)
static

Finds a solution to minimize objective function while satisfying a given constraint using delta.

When local_optimization is Localoptimization::kUse, enable "--local-optimization" dReal option which uses NLopt's local-optimization algorithms to refine counterexamples in the process of global optimization.

Returns
a model, a mapping from a variable to an interval, if a solution exists.
nullopt, if there is no solution.

◆ operator=() [1/2]

DrealSolver& operator= ( DrealSolver &&  )
delete

◆ operator=() [2/2]

DrealSolver& operator= ( const DrealSolver )
delete

◆ ProgramAttributesSatisfied()

bool ProgramAttributesSatisfied ( const MathematicalProgram prog)
static

◆ Solve() [1/2]

SolutionResult Solve ( MathematicalProgram prog) const
overridevirtual

Sets values for the decision variables on the given MathematicalProgram prog, or:

  • If no solver is available, throws std::runtime_error
  • If the solver returns an error, returns a nonzero SolutionResult.

Implements MathematicalProgramSolverInterface.

◆ Solve() [2/2]

void Solve ( const MathematicalProgram prog,
const optional< Eigen::VectorXd > &  initial_guess,
const optional< SolverOptions > &  solver_options,
MathematicalProgramResult result 
) const
overridevirtual

Solves an optimization program with optional initial guess and solver options.

Note that these initial guess and solver options are not written to prog. If the prog has set an option for a solver, and solver_options contains a different value for the same option on the same solver, then solver_options takes priority.

Implements MathematicalProgramSolverInterface.

◆ solver_id()

SolverId solver_id ( ) const
overridevirtual

Returns the identifier of this solver.

Implements MathematicalProgramSolverInterface.


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