dReal4
|
This is the header file that we consolidate Drake's symbolic classes and expose them inside of dreal namespace. More...
#include <functional>
#include <ostream>
#include <set>
#include <string>
#include <vector>
#include "dreal/symbolic/symbolic_environment.h"
#include "dreal/symbolic/symbolic_expression.h"
#include "dreal/symbolic/symbolic_expression_visitor.h"
#include "dreal/symbolic/symbolic_formula.h"
#include "dreal/symbolic/symbolic_formula_visitor.h"
#include "dreal/symbolic/symbolic_variable.h"
#include "dreal/symbolic/symbolic_variables.h"
Go to the source code of this file.
Namespaces | |
dreal | |
Sum type of symbolic::Expression and symbolic::Formula. | |
Enumerations | |
enum | RelationalOperator { EQ, NEQ, GT, GEQ, LT, LEQ } |
Represents relational operators. More... | |
Functions | |
Formula | imply (const Formula &f1, const Formula &f2) |
Returns a formula f1 ⇒ f2 . | |
Formula | imply (const Variable &v, const Formula &f) |
Returns a formula v ⇒ f . | |
Formula | imply (const Formula &f, const Variable &v) |
Returns a formula f ⇒ v . | |
Formula | imply (const Variable &v1, const Variable &v2) |
Returns a formula v1 ⇒ v2 . | |
Formula | iff (const Formula &f1, const Formula &f2) |
Returns a formula f1 ⇔ f2 . | |
Formula | iff (const Variable &v, const Formula &f) |
Returns a formula v ⇔ f . | |
Formula | iff (const Formula &f, const Variable &v) |
Returns a formula f ⇔ v . | |
Formula | iff (const Variable &v1, const Variable &v2) |
Returns a formula v1 ⇔ v2 . | |
std::set< Formula > | map (const std::set< Formula > &formulas, const std::function< Formula(const Formula &)> &func) |
bool | is_atomic (const Formula &f) |
Checks if f is atomic. | |
bool | is_clause (const Formula &f) |
Checks if f is a clause. | |
set< Formula > | get_clauses (const Formula &f) |
Returns the set of clauses in f. More... | |
bool | is_cnf (const Formula &f) |
Checks if is in CNF form. | |
bool | HaveIntersection (const Variables &variables1, const Variables &variables2) |
Formula | DeltaStrengthen (const Formula &f, const double delta) |
Strengthen the input formula $p f by delta . More... | |
Formula | DeltaWeaken (const Formula &f, const double delta) |
Weaken the input formula $p f by delta . More... | |
bool | IsDifferentiable (const Formula &f) |
Returns true if the formula f is symbolic-differentiable. | |
bool | IsDifferentiable (const Expression &e) |
Returns true if the expression f is symbolic-differentiable. | |
Formula | make_conjunction (const std::vector< Formula > &formulas) |
Make conjunction of formulas . More... | |
Formula | make_disjunction (const vector< Formula > &formulas) |
vector< Variable > | CreateVector (const std::string &prefix, int size, Variable::Type type=Variable::Type::CONTINUOUS) |
Creates a vector of variables of type whose size is size . More... | |
RelationalOperator | operator! (RelationalOperator op) |
Negates op . | |
ostream & | operator<< (std::ostream &os, RelationalOperator op) |
Outputs op to os . | |
This is the header file that we consolidate Drake's symbolic classes and expose them inside of dreal namespace.
Other files in dreal should include this file and should NOT include files in drake/common directory. Similarly, BUILD files should only have a dependency "//dreal/symbolic:symbolic", not "@drake_symbolic//:symbolic".
Test cases which need predicates defined in "drake/common/test/symbolic_test_util.h" file should include "dreal/symbolic/symbolic_test_util.h" file and include "//dreal/symbolic:symbolic_test_util" in BUILD file.