formula_cell.h File Reference

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 ∧ ... ∧ fn). More...
class	FormulaOr
	Symbolic formula representing disjunctions (f1 ∨ ... ∨ fn). 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
namespace	drake
namespace	drake::symbolic

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