Drake
DrealSolver Class Referencefinal

#include <drake/solvers/dreal_solver.h>

Classes

class  Interval
 Class representing an interval of doubles. More...
 

Public Types

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

Public Member Functions

 DrealSolver ()
 
 ~DrealSolver () final
 
MathematicalProgramResult Solve (const MathematicalProgram &prog, const std::optional< Eigen::VectorXd > &initial_guess=std::nullopt, const std::optional< SolverOptions > &solver_options=std::nullopt) const
 Like SolverInterface::Solve(), but the result is a return value instead of an output argument. More...
 
void Solve (const MathematicalProgram &, const std::optional< Eigen::VectorXd > &, const std::optional< SolverOptions > &, MathematicalProgramResult *) const override
 
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 SolverBase
 ~SolverBase () override
 
MathematicalProgramResult Solve (const MathematicalProgram &prog, const std::optional< Eigen::VectorXd > &initial_guess=std::nullopt, const std::optional< SolverOptions > &solver_options=std::nullopt) const
 Like SolverInterface::Solve(), but the result is a return value instead of an output argument. More...
 
void Solve (const MathematicalProgram &, const std::optional< Eigen::VectorXd > &, const std::optional< SolverOptions > &, MathematicalProgramResult *) const override
 Solves an optimization program with optional initial guess and solver options. More...
 
bool available () const override
 Returns true iff support for this solver has been compiled into Drake. More...
 
bool enabled () const override
 Returns true iff this solver is properly configured for use at runtime. More...
 
SolverId solver_id () const override
 Returns the identifier of this solver. More...
 
bool AreProgramAttributesSatisfied (const MathematicalProgram &) const override
 Returns true iff the program's attributes are compatible with this solver's capabilities. More...
 
std::string ExplainUnsatisfiedProgramAttributes (const MathematicalProgram &) const override
 Describes the reasons (if any) why the program is incompatible with this solver's capabilities. More...
 
 SolverBase (const SolverBase &)=delete
 
SolverBaseoperator= (const SolverBase &)=delete
 
 SolverBase (SolverBase &&)=delete
 
SolverBaseoperator= (SolverBase &&)=delete
 
- Public Member Functions inherited from SolverInterface
virtual ~SolverInterface ()
 
 SolverInterface (const SolverInterface &)=delete
 
SolverInterfaceoperator= (const SolverInterface &)=delete
 
 SolverInterface (SolverInterface &&)=delete
 
SolverInterfaceoperator= (SolverInterface &&)=delete
 

Static Public Member Functions

static std::optional< IntervalBoxCheckSatisfiability (const symbolic::Formula &f, double delta)
 Checks the satisfiability of a given formula f with a given precision delta. More...
 
static std::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...
 
Static versions of the instance methods with similar names.
static SolverId id ()
 
static bool is_available ()
 
static bool is_enabled ()
 
static bool ProgramAttributesSatisfied (const MathematicalProgram &)
 

Additional Inherited Members

- Protected Member Functions inherited from SolverBase
 SolverBase (std::function< SolverId()> id, std::function< bool()> available, std::function< bool()> enabled, std::function< bool(const MathematicalProgram &)> are_satisfied, std::function< std::string(const MathematicalProgram &)> explain_unsatisfied=nullptr)
 Constructs a SolverBase with the given default implementations of the solver_id(), available(), enabled(), AreProgramAttributesSatisfied(), and ExplainUnsatisfiedProgramAttributes() methods. More...
 
- Protected Member Functions inherited from SolverInterface
 SolverInterface ()
 

Member Typedef Documentation

◆ 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()

~DrealSolver ( )
final

Member Function Documentation

◆ CheckSatisfiability()

static std::optional<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()

static SolverId id ( )
static

◆ is_available()

static bool is_available ( )
static

◆ is_enabled()

static bool is_enabled ( )
static

◆ Minimize()

static std::optional<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()

static bool ProgramAttributesSatisfied ( const MathematicalProgram )
static

◆ Solve() [1/2]

void Solve
override

◆ Solve() [2/2]

Like SolverInterface::Solve(), but the result is a return value instead of an output argument.


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