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.
|
| template<class HashAlgorithm> |
| void | hash_append (HashAlgorithm &hasher, const Formula &item) noexcept |
| | Implements the hash_append generic hashing concept.
|
| void | swap (Formula &a, Formula &b) |
| bool | is_false (const Formula &f) |
| | Checks if f is structurally equal to False formula.
|
| bool | is_true (const Formula &f) |
| | Checks if f is structurally equal to True formula.
|
| bool | is_variable (const Formula &f) |
| | Checks if f is a variable formula.
|
| bool | is_equal_to (const Formula &f) |
| | Checks if f is a formula representing equality (==).
|
| bool | is_not_equal_to (const Formula &f) |
| | Checks if f is a formula representing disequality (!=).
|
| bool | is_greater_than (const Formula &f) |
| | Checks if f is a formula representing greater-than (>).
|
| bool | is_greater_than_or_equal_to (const Formula &f) |
| | Checks if f is a formula representing greater-than-or-equal-to (>=).
|
| bool | is_less_than (const Formula &f) |
| | Checks if f is a formula representing less-than (<).
|
| bool | is_less_than_or_equal_to (const Formula &f) |
| | Checks if f is a formula representing less-than-or-equal-to (<=).
|
| bool | is_relational (const Formula &f) |
| | Checks if f is a relational formula ({==, !=, >, >=, <, <=}).
|
| bool | is_conjunction (const Formula &f) |
| | Checks if f is a conjunction (∧).
|
| bool | is_disjunction (const Formula &f) |
| | Checks if f is a disjunction (∨).
|
| bool | is_negation (const Formula &f) |
| | Checks if f is a negation (¬).
|
| bool | is_forall (const Formula &f) |
| | Checks if f is a Forall formula (∀).
|
| bool | is_isnan (const Formula &f) |
| | Checks if f is an isnan formula.
|
| bool | is_positive_semidefinite (const Formula &f) |
| | Checks if f is a positive-semidefinite formula.
|
| 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) |
| bool | operator< (const Formula &, const Formula &) |
| | Provides a strict weak ordering on formulas (see Less), for use as the comparator of an ordered container, e.g., std::set<Formula>.
|
| bool | operator== (const Formula &, const Formula &) |
| | Checks structural equality of formulas (see EqualTo), for use as the key-equality predicate of an unordered container, e.g., std::unordered_set<Formula>.
|
| bool Less |
( |
const Formula & | f | ) |
const |
|
nodiscard |
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>.
