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...
 
SolverId solver_id () const override
 Returns the identifier of this solver. 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 SolverId id ()
 
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

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

Member Enumeration Documentation

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 ( const DrealSolver )
delete
DrealSolver ( DrealSolver &&  )
delete
DrealSolver ( )
default
~DrealSolver ( )
overridedefault

Member Function Documentation

bool available ( ) const
overridevirtual

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

Implements MathematicalProgramSolverInterface.

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.
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.
DrealSolver& operator= ( DrealSolver &&  )
delete
DrealSolver& operator= ( const DrealSolver )
delete
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.

SolverId solver_id ( ) const
overridevirtual

Returns the identifier of this solver.

Implements MathematicalProgramSolverInterface.


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