Drake
symbolic_formula_cell.h File Reference

Detailed Description

Provides implementation-details of symbolic formulas.

It is strongly discouraged to include and use this header file outside of drake/common/symbolic_* files. To include this file, you need to define DRAKE_COMMON_SYMBOLIC_DETAIL_HEADER before. Without it, you have compile-time errors.

#include <memory>
#include <ostream>
#include <set>
#include <string>
#include "drake/common/drake_assert.h"
#include "drake/common/hash.h"
#include "drake/common/random.h"
#include "drake/common/symbolic.h"
Include dependency graph for symbolic_formula_cell.h:

Classes

class  FormulaCell
 Represents an abstract class which is the base of concrete symbolic-formula classes (i.e. More...
 
class  RelationalFormulaCell
 Represents the base class for relational operators (==, !=, <, <=, >, >=). More...
 
class  NaryFormulaCell
 Represents the base class for N-ary logic operators (∧ and ∨). More...
 
class  FormulaTrue
 Symbolic formula representing true. More...
 
class  FormulaFalse
 Symbolic formula representing false. More...
 
class  FormulaVar
 Symbolic formula representing a Boolean variable. More...
 
class  FormulaEq
 Symbolic formula representing equality (e1 = e2). More...
 
class  FormulaNeq
 Symbolic formula representing disequality (e1 ≠ e2). More...
 
class  FormulaGt
 Symbolic formula representing 'greater-than' (e1 > e2). More...
 
class  FormulaGeq
 Symbolic formula representing 'greater-than-or-equal-to' (e1 ≥ e2). More...
 
class  FormulaLt
 Symbolic formula representing 'less-than' (e1 < e2). More...
 
class  FormulaLeq
 Symbolic formula representing 'less-than-or-equal-to' (e1 ≤ e2). More...
 
class  FormulaAnd
 Symbolic formula representing conjunctions (f1 ∧ ... More...
 
class  FormulaOr
 Symbolic formula representing disjunctions (f1 ∨ ... More...
 
class  FormulaNot
 Symbolic formula representing negations (¬f). More...
 
class  FormulaForall
 Symbolic formula representing universal quantifications (∀ x₁, ..., * xn. More...
 
class  FormulaIsnan
 Symbolic formula representing isnan predicate. More...
 
class  FormulaPositiveSemidefinite
 Symbolic formula representing positive-semidefinite (PSD) constraint. More...
 

Namespaces

 drake
 
 drake::symbolic
 

Functions

bool is_false (const FormulaCell &f)
 Checks if f is structurally equal to False formula. More...
 
bool is_true (const FormulaCell &f)
 Checks if f is structurally equal to True formula. More...
 
bool is_variable (const FormulaCell &f)
 Checks if f is a variable formula. More...
 
bool is_equal_to (const FormulaCell &f)
 Checks if f is a formula representing equality (==). More...
 
bool is_not_equal_to (const FormulaCell &f)
 Checks if f is a formula representing disequality (!=). More...
 
bool is_greater_than (const FormulaCell &f)
 Checks if f is a formula representing greater-than (>). More...
 
bool is_greater_than_or_equal_to (const FormulaCell &f)
 Checks if f is a formula representing greater-than-or-equal-to (>=). More...
 
bool is_less_than (const FormulaCell &f)
 Checks if f is a formula representing less-than (<). More...
 
bool is_less_than_or_equal_to (const FormulaCell &f)
 Checks if f is a formula representing less-than-or-equal-to (<=). More...
 
bool is_relational (const FormulaCell &f)
 Checks if f is a relational formula ({==, !=, >, >=, <, <=}). More...
 
bool is_conjunction (const FormulaCell &f)
 Checks if f is a conjunction (∧). More...
 
bool is_disjunction (const FormulaCell &f)
 Checks if f is a disjunction (∨). More...
 
bool is_negation (const FormulaCell &f)
 Checks if f is a negation (¬). More...
 
bool is_forall (const FormulaCell &f)
 Checks if f is a Forall formula (∀). More...
 
bool is_isnan (const FormulaCell &f)
 Checks if f is an isnan formula. More...
 
bool is_positive_semidefinite (const FormulaCell &f)
 Checks if f is a positive semidefinite formula. More...
 
std::shared_ptr< const FormulaFalse > to_false (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaFalse>. More...
 
std::shared_ptr< const FormulaTrue > to_true (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaTrue>. More...
 
std::shared_ptr< const FormulaVar > to_variable (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaVar>. More...
 
std::shared_ptr< const RelationalFormulaCell > to_relational (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const RelationalFormulaCell>. More...
 
std::shared_ptr< const FormulaEq > to_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaEq>. More...
 
std::shared_ptr< const FormulaNeq > to_not_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaNeq>. More...
 
std::shared_ptr< const FormulaGt > to_greater_than (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaGt>. More...
 
std::shared_ptr< const FormulaGeq > to_greater_than_or_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaGeq>. More...
 
std::shared_ptr< const FormulaLt > to_less_than (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaLt>. More...
 
std::shared_ptr< const FormulaLeq > to_less_than_or_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaLeq>. More...
 
std::shared_ptr< const FormulaAnd > to_conjunction (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaAnd>. More...
 
std::shared_ptr< const FormulaOr > to_disjunction (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaOr>. More...
 
std::shared_ptr< const NaryFormulaCell > to_nary (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const NaryFormulaCell>. More...
 
std::shared_ptr< const FormulaNot > to_negation (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaNot>. More...
 
std::shared_ptr< const FormulaForall > to_forall (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaForall>. More...
 
std::shared_ptr< const FormulaIsnan > to_isnan (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaIsnan>. More...
 
std::shared_ptr< const FormulaPositiveSemidefinite > to_positive_semidefinite (const std::shared_ptr< const FormulaCell > &f_ptr)
 Casts f_ptr to shared_ptr<const FormulaPositiveSemidefinite>. More...