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.
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.
(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... | |
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) |
Formula | ( | ) |
Default constructor.
Sets the value to Formula::False, to be consistent with value-initialized bool
s.
|
explicit |
Constructs from a bool
.
This overload is also used by Eigen when EIGEN_INITIALIZE_MATRICES_BY_ZERO is enabled.
|
explicit |
Constructs a formula from var
.
var
is of BOOLEAN type. bool EqualTo | ( | const Formula & | f | ) | const |
Checks structural equality.
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.
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 . |
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.
|
static |
FormulaKind get_kind | ( | ) | const |
Variables GetFreeVariables | ( | ) | const |
Gets free variables (unquantified variables).
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>.
|
explicit |
Conversion to bool.
Formula Substitute | ( | const Variable & | var, |
const Expression & | e | ||
) | const |
Returns a copy of this formula replacing all occurrences of var
with e
.
std::exception | if NaN is detected during substitution. |
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).
std::exception | if NaN is detected during substitution. |
std::string to_string | ( | ) | const |
Returns string representation of Formula.
|
static |
|
friend |
Implements the hash_append generic hashing concept.
|
friend |
Checks if f
is a conjunction (∧).
|
friend |
Checks if f
is a disjunction (∨).
|
friend |
Checks if f
is a formula representing equality (==).
|
friend |
Checks if f
is structurally equal to False formula.
|
friend |
Checks if f
is a Forall formula (∀).
|
friend |
Checks if f
is a formula representing greater-than (>).
|
friend |
Checks if f
is a formula representing greater-than-or-equal-to (>=).
|
friend |
Checks if f
is an isnan formula.
|
friend |
Checks if f
is a formula representing less-than (<).
|
friend |
Checks if f
is a formula representing less-than-or-equal-to (<=).
|
friend |
Checks if f
is a negation (¬).
|
friend |
Checks if f
is a formula representing disequality (!=).
|
friend |
Checks if f
is a positive-semidefinite formula.
|
friend |
Checks if f
is a relational formula ({==, !=, >, >=, <, <=}).
|
friend |
Checks if f
is structurally equal to True formula.
|
friend |
Checks if f
is a variable formula.
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |