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

#include <symbolic_formula.h>

Public Member Functions
	Formula ()
	Default constructor.

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

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

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

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

bool	Evaluate (const Environment &env=Environment{}) const
	Evaluates under a given environment (by default, an empty environment).

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

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

Formula	Substitute (const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) const
	Returns a copy of this formula replacing all occurrences of the variables in `expr_subst` with corresponding expressions in `expr_subst` and all occurrences of the variables in `formula_subst` with corresponding formulas in `formula_subst`.

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

Formula	Substitute (const FormulaSubstitution &formula_subst) const
	Returns a copy of this formula replacing all occurrences of the variables in `formula_subst` with corresponding formulas in `formula_subst`.

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

	operator bool () const
	Conversion to bool.

bool	include_ite () const
	Returns true if this symbolic formula includes an ITE (If-Then-Else) expression.

Friends
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 (∀).

Formula	forall (const Variables &vars, const Formula &f)
	Returns a formula `f`, universally quantified by variables `vars`.

Formula	make_conjunction (const std::set< Formula > &formulas)
	Returns a conjunction of `formulas`.

Formula	make_disjunction (const std::set< Formula > &formulas)
	Returns a disjunction of `formulas`.

Formula	operator== (const Expression &e1, const Expression &e2)
	Returns a formula representing (e1 = e2).

Formula	operator!= (const Expression &e1, const Expression &e2)
	Returns a formula representing e1 ≠ e2.

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 raw pointer to FormulaCell class which is a super-class of different kinds of symbolic formulas (i.e. FormulaAnd, FormulaOr, FormulaEq).

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.

Definition at line 100 of file symbolic_formula.h.

Constructor & Destructor Documentation

◆ Formula()

dlinear::drake::symbolic::Formula::Formula ( const Variable & var )

explicit

Constructs a formula from var.

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

Member Function Documentation

◆ Evaluate()

bool dlinear::drake::symbolic::Formula::Evaluate ( const Environment & env = Environment{} ) const

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

Exceptions

runtime_error if 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₂.

◆ Less()

bool dlinear::drake::symbolic::Formula::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>.

◆ Substitute() [1/5]

Formula dlinear::drake::symbolic::Formula::Substitute ( const ExpressionSubstitution & expr_subst ) const

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

Note: This is equivalent to Substitute(expr_subst, {}).

Exceptions