Detailed Description

Represents a symbolic form of a first-order logic formula.

It has the following grammar:

    F := ⊥ | ⊤ | Var | E = E | E ≠ E | E > E | E ≥ E | E < E | E ≤ E
       | E ∧ ... ∧ E | E ∨ ... ∨ E | ¬F | ∀ x₁, ..., xn. F

In the implementation, Formula is a simple wrapper including a shared pointer to FormulaCell class which is a super-class of different kinds of symbolic formulas (i.e. FormulaAnd, FormulaOr, FormulaEq). Note that it includes a shared pointer, not a unique pointer, to allow sharing sub-expressions.

Note: The sharing of sub-expressions is not yet implemented.

The following simple simplifications are implemented:

    E1 = E2        ->  True    (if E1 and E2 are structurally equal)
    E1 ≠ E2        ->  False   (if E1 and E2 are structurally equal)
    E1 > E2        ->  False   (if E1 and E2 are structurally equal)
    E1 ≥ E2        ->  True    (if E1 and E2 are structurally equal)
    E1 < E2        ->  False   (if E1 and E2 are structurally equal)
    E1 ≤ E2        ->  True    (if E1 and E2 are structurally equal)
    F1 ∧ F2        ->  False   (if either F1 or F2 is False)
    F1 ∨ F2        ->  True    (if either F1 or F2 is True)
    ¬(¬(F))        ->  F

We flatten nested conjunctions (or disjunctions) at the construction. A conjunction (resp. disjunction) takes a set of conjuncts (resp. disjuncts). Note that any duplicated conjunct/disjunct is removed. For example, both of f1 && (f2 && f1) and (f1 && f2) && f1 are flattened to f1 && f2 && f1 and simplified into f1 && f2. As a result, the two are identified as the same formula.

Note: Formula class has an explicit conversion operator to bool. It evaluates a symbolic formula under an empty environment. If a symbolic formula includes variables, the conversion operator throws an exception. This operator is only intended for third-party code doing things like (imag(SymbolicExpression(0)) == SymbolicExpression(0)) { ... }; that we found in Eigen3 codebase. In general, a user of this class should explicitly call Evaluate from within Drake for readability.

#include <drake/common/symbolic/expression/formula.h>

Public Member Functions
	Formula ()
	Default constructor. More...

	Formula (bool value)
	Constructs from a `bool`. More...

	Formula (std::shared_ptr< const FormulaCell > ptr)

	Formula (const Variable &var)
	Constructs a formula from `var`. More...

	~Formula ()=default

FormulaKind	get_kind () const

Variables	GetFreeVariables () const
	Gets free variables (unquantified variables). More...

bool	EqualTo (const Formula &f) const
	Checks structural equality. More...

bool	Less (const Formula &f) const
	Checks lexicographical ordering between this and `e`. More...

bool	Evaluate (const Environment &env=Environment{}, RandomGenerator *random_generator=nullptr) const
	Evaluates using a given environment (by default, an empty environment) and a random number generator. More...

bool	Evaluate (RandomGenerator *random_generator) const
	Evaluates using an empty environment and a random number generator. More...

Formula	Substitute (const Variable &var, const Expression &e) const
	Returns a copy of this formula replacing all occurrences of `var` with `e`. More...

Formula	Substitute (const Substitution &s) const
	Returns a copy of this formula replacing all occurrences of the variables in `s` with corresponding expressions in `s`. More...

std::string	to_string () const
	Returns string representation of Formula. More...

	operator bool () const
	Conversion to bool. More...

Implements CopyConstructible, CopyAssignable, MoveConstructible, MoveAssignable
	Formula (const Formula &)=default

Formula &	operator= (const Formula &)=default

	Formula (Formula &&)=default

Formula &	operator= (Formula &&)=default

Static Public Member Functions
static Formula	True ()

static Formula	False ()

Friends
template<class HashAlgorithm >
void	hash_append (HashAlgorithm &hasher, const Formula &item) noexcept
	Implements the hash_append generic hashing concept. More...

std::ostream &	operator<< (std::ostream &os, const Formula &f)

void	swap (Formula &a, Formula &b)

bool	is_false (const Formula &f)
	Checks if `f` is structurally equal to False formula. More...

bool	is_true (const Formula &f)
	Checks if `f` is structurally equal to True formula. More...

bool	is_variable (const Formula &f)
	Checks if `f` is a variable formula. More...

bool	is_equal_to (const Formula &f)
	Checks if `f` is a formula representing equality (==). More...

bool	is_not_equal_to (const Formula &f)
	Checks if `f` is a formula representing disequality (!=). More...

bool	is_greater_than (const Formula &f)
	Checks if `f` is a formula representing greater-than (>). More...

bool	is_greater_than_or_equal_to (const Formula &f)
	Checks if `f` is a formula representing greater-than-or-equal-to (>=). More...

bool	is_less_than (const Formula &f)
	Checks if `f` is a formula representing less-than (<). More...

bool	is_less_than_or_equal_to (const Formula &f)
	Checks if `f` is a formula representing less-than-or-equal-to (<=). More...

bool	is_relational (const Formula &f)
	Checks if `f` is a relational formula ({==, !=, >, >=, <, <=}). More...

bool	is_conjunction (const Formula &f)
	Checks if `f` is a conjunction (∧). More...

bool	is_disjunction (const Formula &f)
	Checks if `f` is a disjunction (∨). More...

bool	is_negation (const Formula &f)
	Checks if `f` is a negation (¬). More...

bool	is_forall (const Formula &f)
	Checks if `f` is a Forall formula (∀). More...

bool	is_isnan (const Formula &f)
	Checks if `f` is an isnan formula. More...

bool	is_positive_semidefinite (const Formula &f)
	Checks if `f` is a positive-semidefinite formula. More...

std::shared_ptr< const FormulaFalse >	to_false (const Formula &f)

std::shared_ptr< const FormulaTrue >	to_true (const Formula &f)

std::shared_ptr< const FormulaVar >	to_variable (const Formula &f)

std::shared_ptr< const RelationalFormulaCell >	to_relational (const Formula &f)

std::shared_ptr< const FormulaEq >	to_equal_to (const Formula &f)

std::shared_ptr< const FormulaNeq >	to_not_equal_to (const Formula &f)

std::shared_ptr< const FormulaGt >	to_greater_than (const Formula &f)

std::shared_ptr< const FormulaGeq >	to_greater_than_or_equal_to (const Formula &f)

std::shared_ptr< const FormulaLt >	to_less_than (const Formula &f)

std::shared_ptr< const FormulaLeq >	to_less_than_or_equal_to (const Formula &f)

std::shared_ptr< const NaryFormulaCell >	to_nary (const Formula &f)

std::shared_ptr< const FormulaAnd >	to_conjunction (const Formula &f)

std::shared_ptr< const FormulaOr >	to_disjunction (const Formula &f)

std::shared_ptr< const FormulaNot >	to_negation (const Formula &f)

std::shared_ptr< const FormulaForall >	to_forall (const Formula &f)

std::shared_ptr< const FormulaIsnan >	to_isnan (const Formula &f)

std::shared_ptr< const FormulaPositiveSemidefinite >	to_positive_semidefinite (const Formula &f)

Constructor & Destructor Documentation

◆ Formula() [1/6]

Formula ( const Formula & )

default

◆ Formula() [2/6]

Formula ( Formula && )

default

◆ Formula() [3/6]

Formula ( )

Default constructor.

Sets the value to Formula::False, to be consistent with value-initialized bools.

◆ Formula() [4/6]

Formula ( bool value )

explicit

Constructs from a bool.

This overload is also used by Eigen when EIGEN_INITIALIZE_MATRICES_BY_ZERO is enabled.

◆ Formula() [5/6]

Formula ( std::shared_ptr< const FormulaCell > ptr )

explicit

◆ Formula() [6/6]

Formula ( const Variable & var )

explicit

Constructs a formula from var.

Precondition: var is of BOOLEAN type.

◆ ~Formula()

~Formula ( )

default

Member Function Documentation

◆ EqualTo()

bool EqualTo ( const Formula & f ) const

Checks structural equality.

◆ Evaluate() [1/2]

bool Evaluate	(	const Environment &	env = `Environment{}`,
		RandomGenerator *	random_generator = `nullptr`
	)		const

Evaluates using a given environment (by default, an empty environment) and a random number generator.

If there is a random variable in this formula which is unassigned in env, it uses random_generator to sample a value and use it to substitute all occurrences of the random variable in this formula.

Exceptions

std::exception	if a variable `v` is needed for an evaluation but not provided by `env`.
std::exception	if an unassigned random variable is detected while `random_generator` is `nullptr`.

◆ Evaluate() [2/2]

bool Evaluate ( RandomGenerator * random_generator ) const

Evaluates using an empty environment and a random number generator.

See the above overload for the exceptions that it might throw.

◆ False()

static Formula False ( )

static

◆ get_kind()

FormulaKind get_kind ( ) const

◆ GetFreeVariables()

Variables GetFreeVariables ( ) const

Gets free variables (unquantified variables).

◆ Less()

bool Less ( const Formula & f ) const

Checks lexicographical ordering between this and e.

If the two formulas f1 and f2 have different kinds k1 and k2 respectively, f1.Less(f2) is equal to k1 < k2. If f1 and f2 are expressions of the same kind, we check the ordering between f1 and f2 by comparing their elements lexicographically.

For example, in case of And, let f1 and f2 be

f1 = f_1,1 ∧ ... ∧ f_1,n
f2 = f_2,1 ∧ ... ∧ f_2,m

f1.Less(f2) is true if there exists an index i (<= n, m) such that for all j < i, we have

¬(f_1_j.Less(f_2_j)) ∧ ¬(f_2_j.Less(f_1_j))

and f_1_i.Less(f_2_i) holds.

This function is used as a compare function in std::map<symbolic::Formula> and std::set<symbolic::Formula> via std::less<symbolic::Formula>.

◆ operator bool()

operator bool ( ) const

explicit

Conversion to bool.

◆ operator=() [1/2]

Formula& operator= ( const Formula & )

default

◆ operator=() [2/2]

Formula& operator= ( Formula && )

default

◆ Substitute() [1/2]

Formula Substitute	(	const Variable &	var,
		const Expression &	e
	)		const

Returns a copy of this formula replacing all occurrences of var with e.

Exceptions

std::exception if NaN is detected during substitution.

◆ Substitute() [2/2]

Formula Substitute ( const Substitution & s ) const

Returns a copy of this formula replacing all occurrences of the variables in s with corresponding expressions in s.

Note that the substitutions occur simultaneously. For example, (x / y > 0).Substitute({{x, y}, {y, x}}) gets (y / x > 0).

Exceptions

std::exception if NaN is detected during substitution.

◆ to_string()

std::string to_string ( ) const

Returns string representation of Formula.

◆ True()

static Formula True ( )

static

Friends And Related Function Documentation

◆ hash_append

void hash_append	(	HashAlgorithm &	hasher,
		const Formula &	item
	)

friend

Implements the hash_append generic hashing concept.

◆ is_conjunction

bool is_conjunction ( const Formula & f )

friend

Checks if f is a conjunction (∧).

◆ is_disjunction

bool is_disjunction ( const Formula & f )

friend

Checks if f is a disjunction (∨).

◆ is_equal_to

bool is_equal_to ( const Formula & f )

friend

Checks if f is a formula representing equality (==).

◆ is_false

bool is_false ( const Formula & f )

friend

Checks if f is structurally equal to False formula.

◆ is_forall

bool is_forall ( const Formula & f )

friend

Checks if f is a Forall formula (∀).

◆ is_greater_than

bool is_greater_than ( const Formula & f )

friend

Checks if f is a formula representing greater-than (>).

◆ is_greater_than_or_equal_to

bool is_greater_than_or_equal_to ( const Formula & f )

friend

Checks if f is a formula representing greater-than-or-equal-to (>=).

◆ is_isnan

bool is_isnan ( const Formula & f )

friend

Checks if f is an isnan formula.

◆ is_less_than

bool is_less_than ( const Formula & f )

friend

Checks if f is a formula representing less-than (<).

◆ is_less_than_or_equal_to

bool is_less_than_or_equal_to ( const Formula & f )

friend

Checks if f is a formula representing less-than-or-equal-to (<=).

◆ is_negation

bool is_negation ( const Formula & f )

friend

Checks if f is a negation (¬).

◆ is_not_equal_to

bool is_not_equal_to ( const Formula & f )

friend

Checks if f is a formula representing disequality (!=).

◆ is_positive_semidefinite

bool is_positive_semidefinite ( const Formula & f )

friend

Checks if f is a positive-semidefinite formula.

◆ is_relational

bool is_relational ( const Formula & f )

friend

Checks if f is a relational formula ({==, !=, >, >=, <, <=}).

◆ is_true

bool is_true ( const Formula & f )

friend

Checks if f is structurally equal to True formula.

◆ is_variable

bool is_variable ( const Formula & f )

friend

Checks if f is a variable formula.

◆ operator<<

std::ostream& operator<<	(	std::ostream &	os,
		const Formula &	f
	)

friend

◆ swap

void swap	(	Formula &	a,
		Formula &	b
	)

friend

◆ to_conjunction

std::shared_ptr<const FormulaAnd> to_conjunction ( const Formula & f )

friend

◆ to_disjunction

std::shared_ptr<const FormulaOr> to_disjunction ( const Formula & f )

friend

◆ to_equal_to

std::shared_ptr<const FormulaEq> to_equal_to ( const Formula & f )

friend

◆ to_false

std::shared_ptr<const FormulaFalse> to_false ( const Formula & f )

friend

◆ to_forall

std::shared_ptr<const FormulaForall> to_forall ( const Formula & f )

friend

◆ to_greater_than

std::shared_ptr<const FormulaGt> to_greater_than ( const Formula & f )

friend

◆ to_greater_than_or_equal_to

std::shared_ptr<const FormulaGeq> to_greater_than_or_equal_to ( const Formula & f )

friend

◆ to_isnan

std::shared_ptr<const FormulaIsnan> to_isnan ( const Formula & f )

friend

◆ to_less_than

std::shared_ptr<const FormulaLt> to_less_than ( const Formula & f )

friend

◆ to_less_than_or_equal_to

std::shared_ptr<const FormulaLeq> to_less_than_or_equal_to ( const Formula & f )

friend

◆ to_nary

std::shared_ptr<const NaryFormulaCell> to_nary ( const Formula & f )

friend

◆ to_negation

std::shared_ptr<const FormulaNot> to_negation ( const Formula & f )

friend

◆ to_not_equal_to

std::shared_ptr<const FormulaNeq> to_not_equal_to ( const Formula & f )

friend

◆ to_positive_semidefinite

std::shared_ptr<const FormulaPositiveSemidefinite> to_positive_semidefinite ( const Formula & f )

friend

◆ to_relational

std::shared_ptr<const RelationalFormulaCell> to_relational ( const Formula & f )

friend

◆ to_true

std::shared_ptr<const FormulaTrue> to_true ( const Formula & f )

friend

◆ to_variable

std::shared_ptr<const FormulaVar> to_variable ( const Formula & f )

friend

The documentation for this class was generated from the following file:

drake/common/symbolic/expression/formula.h

Detailed Description

Public Member Functions

Static Public Member Functions

Friends

Constructor & Destructor Documentation

◆ Formula() [1/6]

◆ Formula() [2/6]

◆ Formula() [3/6]

◆ Formula() [4/6]

◆ Formula() [5/6]

◆ Formula() [6/6]

◆ ~Formula()

Member Function Documentation

◆ EqualTo()

◆ Evaluate() [1/2]

◆ Evaluate() [2/2]

◆ False()

◆ get_kind()

◆ GetFreeVariables()

◆ Less()

◆ operator bool()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ Substitute() [1/2]

◆ Substitute() [2/2]

◆ to_string()

◆ True()

Friends And Related Function Documentation

◆ hash_append

◆ is_conjunction

◆ is_disjunction

◆ is_equal_to

◆ is_false

◆ is_forall

◆ is_greater_than

◆ is_greater_than_or_equal_to

◆ is_isnan

◆ is_less_than

◆ is_less_than_or_equal_to

◆ is_negation

◆ is_not_equal_to

◆ is_positive_semidefinite

◆ is_relational

◆ is_true

◆ is_variable

◆ operator<<

◆ swap

◆ to_conjunction

◆ to_disjunction

◆ to_equal_to

◆ to_false

◆ to_forall

◆ to_greater_than

◆ to_greater_than_or_equal_to

◆ to_isnan

◆ to_less_than

◆ to_less_than_or_equal_to

◆ to_nary

◆ to_negation

◆ to_not_equal_to

◆ to_positive_semidefinite

◆ to_relational

◆ to_true

◆ to_variable