dReal4
symbolic.h File Reference

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 f1f2.
 
Formula imply (const Variable &v, const Formula &f)
 Returns a formula vf.
 
Formula imply (const Formula &f, const Variable &v)
 Returns a formula fv.
 
Formula imply (const Variable &v1, const Variable &v2)
 Returns a formula v1v2.
 
Formula iff (const Formula &f1, const Formula &f2)
 Returns a formula f1f2.
 
Formula iff (const Variable &v, const Formula &f)
 Returns a formula vf.
 
Formula iff (const Formula &f, const Variable &v)
 Returns a formula fv.
 
Formula iff (const Variable &v1, const Variable &v2)
 Returns a formula v1v2.
 
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.
 

Detailed Description

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.