Detailed Description

Internal use only.

Provides implementation-details of symbolic formulas.

#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/expression/all.h"

Include dependency graph for 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...

Detailed Description

Classes

Namespaces

Functions