Drake
Formula Class Reference

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

#include <drake/common/symbolic_formula.h>

Public Member Functions

 Formula ()
 Default constructor. More...
 
 Formula (std::shared_ptr< FormulaCell > ptr)
 
 Formula (const Variable &var)
 Constructs a formula from var. More...
 
FormulaKind get_kind () const
 
size_t get_hash () 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{}) const
 Evaluates under a given environment (by default, an empty environment). 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
 
Formulaoperator= (const Formula &)=default
 
 Formula (Formula &&)=default
 
Formulaoperator= (Formula &&)=default
 

Static Public Member Functions

static Formula True ()
 
static Formula False ()
 

Friends

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< FormulaFalseto_false (const Formula &f)
 Casts f to shared_ptr<FormulaFalse>. More...
 
std::shared_ptr< FormulaTrueto_true (const Formula &f)
 Casts f to shared_ptr<FormulaTrue>. More...
 
std::shared_ptr< FormulaVarto_variable (const Formula &f)
 Casts f to shared_ptr<FormulaVar>. More...
 
std::shared_ptr< RelationalFormulaCellto_relational (const Formula &f)
 Casts f to shared_ptr<RelationalFormulaCell>. More...
 
std::shared_ptr< FormulaEqto_equal_to (const Formula &f)
 Casts f to shared_ptr<FormulaEq>. More...
 
std::shared_ptr< FormulaNeqto_not_equal_to (const Formula &f)
 Casts f to shared_ptr<FormulaNeq>. More...
 
std::shared_ptr< FormulaGtto_greater_than (const Formula &f)
 Casts f to shared_ptr<FormulaGt>. More...
 
std::shared_ptr< FormulaGeqto_greater_than_or_equal_to (const Formula &f)
 Casts f to shared_ptr<FormulaGeq>. More...
 
std::shared_ptr< FormulaLtto_less_than (const Formula &f)
 Casts f to shared_ptr<FormulaLt>. More...
 
std::shared_ptr< FormulaLeqto_less_than_or_equal_to (const Formula &f)
 Casts f to shared_ptr<FormulaLeq>. More...
 
std::shared_ptr< NaryFormulaCellto_nary (const Formula &f)
 Casts f to shared_ptr<NaryFormulaCell>. More...
 
std::shared_ptr< FormulaAndto_conjunction (const Formula &f)
 Casts f to shared_ptr<FormulaAnd>. More...
 
std::shared_ptr< FormulaOrto_disjunction (const Formula &f)
 Casts f to shared_ptr<FormulaOr>. More...
 
std::shared_ptr< FormulaNotto_negation (const Formula &f)
 Casts f to shared_ptr<FormulaNot>. More...
 
std::shared_ptr< FormulaForallto_forall (const Formula &f)
 Casts f to shared_ptr<FormulaForall>. More...
 
std::shared_ptr< FormulaIsnanto_isnan (const Formula &f)
 Casts f to shared_ptr<FormulaIsnan>. More...
 
std::shared_ptr< FormulaPositiveSemidefiniteto_positive_semidefinite (const Formula &f)
 Casts f to shared_ptr<FormulaPositiveSemidefinite>. More...
 

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.

Constructor & Destructor Documentation

Formula ( const Formula )
default
Formula ( Formula &&  )
default
Formula ( )
inline

Default constructor.

Here is the call graph for this function:

Here is the caller graph for this function:

Formula ( std::shared_ptr< FormulaCell ptr)
explicit
Formula ( const Variable var)
explicit

Constructs a formula from var.

Precondition
var is of BOOLEAN type and not a dummy variable.

Member Function Documentation

bool EqualTo ( const Formula f) const

Checks structural equality.

Here is the call graph for this function:

Here is the caller graph for this function:

bool Evaluate ( const Environment env = Environment{}) const

Evaluates under a given environment (by default, an empty environment).

Exceptions
runtime_errorif a variable v is needed for an evaluation but not provided by env.

Note that for an equality e₁ = e₂ and an inequality e₁ ≠ e₂, this method partially evaluates e₁ and e₂ and checks the structural equality of the two results if env does not provide complete information to call Evaluate on e₁ and e₂.

Here is the caller graph for this function:

Formula False ( )
static

Here is the caller graph for this function:

size_t get_hash ( ) const

Here is the caller graph for this function:

FormulaKind get_kind ( ) const

Here is the caller graph for this function:

Variables GetFreeVariables ( ) const

Gets free variables (unquantified variables).

Here is the caller graph for this function:

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>.

Here is the call graph for this function:

Here is the caller graph for this function:

operator bool ( ) const
inlineexplicit

Conversion to bool.

Here is the call graph for this function:

Formula& operator= ( Formula &&  )
default
Formula& operator= ( const Formula )
default
Formula Substitute ( const Variable var,
const Expression e 
) const

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

Exceptions
std::runtime_errorif NaN is detected during substitution.

Here is the caller graph for this function:

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::runtime_errorif NaN is detected during substitution.
string to_string ( ) const

Returns string representation of Formula.

Formula True ( )
static

Here is the caller graph for this function:

Friends And Related Function Documentation

bool is_conjunction ( const Formula f)
friend

Checks if f is a conjunction (∧).

bool is_disjunction ( const Formula f)
friend

Checks if f is a disjunction (∨).

bool is_equal_to ( const Formula f)
friend

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

bool is_false ( const Formula f)
friend

Checks if f is structurally equal to False formula.

bool is_forall ( const Formula f)
friend

Checks if f is a Forall formula (∀).

bool is_greater_than ( const Formula f)
friend

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

bool is_greater_than_or_equal_to ( const Formula f)
friend

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

bool is_isnan ( const Formula f)
friend

Checks if f is an isnan formula.

bool is_less_than ( const Formula f)
friend

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

bool is_less_than_or_equal_to ( const Formula f)
friend

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

bool is_negation ( const Formula f)
friend

Checks if f is a negation (¬).

bool is_not_equal_to ( const Formula f)
friend

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

bool is_positive_semidefinite ( const Formula f)
friend

Checks if f is a positive-semidefinite formula.

bool is_relational ( const Formula f)
friend

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

bool is_true ( const Formula f)
friend

Checks if f is structurally equal to True formula.

bool is_variable ( const Formula f)
friend

Checks if f is a variable formula.

std::ostream& operator<< ( std::ostream &  os,
const Formula f 
)
friend
void swap ( Formula a,
Formula b 
)
friend
std::shared_ptr<FormulaAnd> to_conjunction ( const Formula f)
friend

Casts f to shared_ptr<FormulaAnd>.

Precondition
is_conjunction(f) is true.
std::shared_ptr<FormulaOr> to_disjunction ( const Formula f)
friend

Casts f to shared_ptr<FormulaOr>.

Precondition
is_disjunction(f) is true.
std::shared_ptr<FormulaEq> to_equal_to ( const Formula f)
friend

Casts f to shared_ptr<FormulaEq>.

Precondition
is_equal_to(f) is true.
std::shared_ptr<FormulaFalse> to_false ( const Formula f)
friend

Casts f to shared_ptr<FormulaFalse>.

Precondition
is_false(f) is true.
std::shared_ptr<FormulaForall> to_forall ( const Formula f)
friend

Casts f to shared_ptr<FormulaForall>.

Precondition
is_forall(f) is true.
std::shared_ptr<FormulaGt> to_greater_than ( const Formula f)
friend

Casts f to shared_ptr<FormulaGt>.

Precondition
is_greater_than(f) is true.
std::shared_ptr<FormulaGeq> to_greater_than_or_equal_to ( const Formula f)
friend

Casts f to shared_ptr<FormulaGeq>.

Precondition
is_greater_than_or_equal_to(f) is true.
std::shared_ptr<FormulaIsnan> to_isnan ( const Formula f)
friend

Casts f to shared_ptr<FormulaIsnan>.

Precondition
is_isnan(f) is true.
std::shared_ptr<FormulaLt> to_less_than ( const Formula f)
friend

Casts f to shared_ptr<FormulaLt>.

Precondition
is_less_than(f) is true.
std::shared_ptr<FormulaLeq> to_less_than_or_equal_to ( const Formula f)
friend

Casts f to shared_ptr<FormulaLeq>.

Precondition
is_less_than_or_equal_to(f) is true.
std::shared_ptr<NaryFormulaCell> to_nary ( const Formula f)
friend

Casts f to shared_ptr<NaryFormulaCell>.

Precondition
is_nary(f) is true.
std::shared_ptr<FormulaNot> to_negation ( const Formula f)
friend

Casts f to shared_ptr<FormulaNot>.

Precondition
is_negation(f) is true.
std::shared_ptr<FormulaNeq> to_not_equal_to ( const Formula f)
friend

Casts f to shared_ptr<FormulaNeq>.

Precondition
is_not_equal_to(f) is true.
std::shared_ptr<FormulaPositiveSemidefinite> to_positive_semidefinite ( const Formula f)
friend

Casts f to shared_ptr<FormulaPositiveSemidefinite>.

Precondition
is_positive_semidefinite(f) is true.
std::shared_ptr<RelationalFormulaCell> to_relational ( const Formula f)
friend

Casts f to shared_ptr<RelationalFormulaCell>.

Precondition
is_relational(f) is true.
std::shared_ptr<FormulaTrue> to_true ( const Formula f)
friend

Casts f to shared_ptr<FormulaTrue>.

Precondition
is_true(f) is true.
std::shared_ptr<FormulaVar> to_variable ( const Formula f)
friend

Casts f to shared_ptr<FormulaVar>.

Precondition
is_variable(f) is true.

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