dReal4
Public Member Functions | Static Public Member Functions | Public Attributes | Friends | List of all members
Formula Class Reference

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

#include </home/soonhokong/work/dreal4/third_party/com_github_robotlocomotion_drake/dreal/symbolic/symbolic_formula.h>

Public Member Functions

 Formula ()
 Default constructor. More...
 
 Formula (const Formula &)
 
Formula & operator= (const Formula &)
 
 Formula (Formula &&) noexcept
 
Formula & operator= (Formula &&) noexcept
 
 Formula (const Variable &var)
 Constructs a formula from var. More...
 
FormulaKind get_kind () const
 
size_t get_hash () const
 
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. 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 Variable &var, const Formula &f) const
 Returns a copy of this formula replacing all occurrences of var with f. More...
 
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. More...
 
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. More...
 
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. More...
 
std::string to_string () const
 Returns string representation of Formula. More...
 
 operator bool () const
 Conversion to bool. More...
 
bool include_ite () const
 Returns true if this symbolic formula includes an ITE (If-Then-Else) expression. More...
 

Static Public Member Functions

static Formula True ()
 
static Formula False ()
 
static Formula make_conjunction (Formula &f1, const Formula &f2)
 
static Formula make_disjunction (Formula &f1, const Formula &f2)
 

Public Attributes

friend FormulaCell
 

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...
 
const FormulaFalse * to_false (const Formula &f)
 Casts f to const FormulaFalse*. More...
 
const FormulaTrue * to_true (const Formula &f)
 Casts f to const FormulaTrue*. More...
 
const FormulaVar * to_variable (const Formula &f)
 Casts f to const FormulaVar*. More...
 
const RelationalFormulaCell * to_relational (const Formula &f)
 Casts f to const RelationalFormulaCell*. More...
 
const FormulaEq * to_equal_to (const Formula &f)
 Casts f to const FormulaEq*. More...
 
const FormulaNeq * to_not_equal_to (const Formula &f)
 Casts f to const FormulaNeq*. More...
 
const FormulaGt * to_greater_than (const Formula &f)
 Casts f to const FormulaGt*. More...
 
const FormulaGeq * to_greater_than_or_equal_to (const Formula &f)
 Casts f to const FormulaGeq*. More...
 
const FormulaLt * to_less_than (const Formula &f)
 Casts f to const FormulaLt*. More...
 
const FormulaLeq * to_less_than_or_equal_to (const Formula &f)
 Casts f to const FormulaLeq*. More...
 
const NaryFormulaCell * to_nary (const Formula &f)
 Casts f to const NaryFormulaCell*. More...
 
NaryFormulaCell * to_nary (Formula &f)
 Casts f to NaryFormulaCell*. More...
 
const FormulaAnd * to_conjunction (const Formula &f)
 Casts f to const FormulaAnd*. More...
 
const FormulaOr * to_disjunction (const Formula &f)
 Casts f to const FormulaOr*. More...
 
const FormulaNot * to_negation (const Formula &f)
 Casts f to const FormulaNot*. More...
 
const FormulaForall * to_forall (const Formula &f)
 Casts f to const FormulaForall*. More...
 
Formula forall (const Variables &vars, const Formula &f)
 Returns a formula f, universally quantified by variables vars. More...
 
Formula make_conjunction (const std::set< Formula > &formulas)
 Returns a conjunction of formulas. More...
 
Formula make_disjunction (const std::set< Formula > &formulas)
 Returns a disjunction of formulas. More...
 
Formula operator! (const Formula &f)
 
Formula operator== (const Expression &e1, const Expression &e2)
 Returns a formula representing (e1 = e2). More...
 
Formula operator!= (const Expression &e1, const Expression &e2)
 Returns a formula representing e1 ≠ e2. More...
 
Formula operator< (const Expression &e1, const Expression &e2)
 
Formula operator<= (const Expression &e1, const Expression &e2)
 
Formula operator> (const Expression &e1, const Expression &e2)
 
Formula operator>= (const Expression &e1, const Expression &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.

Constructor & Destructor Documentation

◆ Formula() [1/2]

Formula ( )

Default constructor.

◆ Formula() [2/2]

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

◆ include_ite()

bool include_ite ( ) const

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

◆ 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
inlineexplicit

Conversion to bool.

◆ Substitute() [1/5]

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.

◆ Substitute() [2/5]

Formula Substitute ( const Variable &  var,
const Formula &  f 
) const

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

Exceptions
std::runtime_errorif NaN is detected during substitution.

◆ Substitute() [3/5]

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.

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.

◆ Substitute() [4/5]

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
std::runtime_errorif NaN is detected during substitution.

◆ Substitute() [5/5]

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.

Note
This is equivalent to Substitute({}, formula_subst).
Exceptions
std::runtime_errorif NaN is detected during substitution.

◆ to_string()

string to_string ( ) const

Returns string representation of Formula.

Friends And Related Function Documentation

◆ forall

Formula forall ( const Variables &  vars,
const Formula &  f 
)
friend

Returns a formula f, universally quantified by variables vars.

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

◆ make_conjunction

Formula make_conjunction ( const std::set< Formula > &  formulas)
friend

Returns a conjunction of formulas.

It performs the following simplification:

  • make_conjunction({}) returns True.
  • make_conjunction({f₁}) returns f₁.
  • If False ∈ formulas, it returns False.
  • If True ∈ formulas, it will not appear in the return value.
  • Nested conjunctions will be flattened. For example, make_conjunction({f₁, f₂ ∧ f₃}) returns f₁ ∧ f₂ ∧ f₃.

◆ make_disjunction

Formula make_disjunction ( const std::set< Formula > &  formulas)
friend

Returns a disjunction of formulas.

It performs the following simplification:

  • make_disjunction({}) returns False.
  • make_disjunction({f₁}) returns f₁.
  • If True ∈ formulas, it returns True.
  • If False ∈ formulas, it will not appear in the return value.
  • Nested disjunctions will be flattened. For example, make_disjunction({f₁, f₂ ∨ f₃}) returns f₁ ∨ f₂ ∨ f₃.

◆ operator!=

Formula operator!= ( const Expression &  e1,
const Expression &  e2 
)
friend

Returns a formula representing e1 ≠ e2.

◆ operator==

Formula operator== ( const Expression &  e1,
const Expression &  e2 
)
friend

Returns a formula representing (e1 = e2).

◆ to_conjunction

const FormulaAnd* to_conjunction ( const Formula &  f)
friend

Casts f to const FormulaAnd*.

Precondition
is_conjunction(f) is true.

◆ to_disjunction

const FormulaOr* to_disjunction ( const Formula &  f)
friend

Casts f to const FormulaOr*.

Precondition
is_disjunction(f) is true.

◆ to_equal_to

const FormulaEq* to_equal_to ( const Formula &  f)
friend

Casts f to const FormulaEq*.

Precondition
is_equal_to(f) is true.

◆ to_false

const FormulaFalse* to_false ( const Formula &  f)
friend

Casts f to const FormulaFalse*.

Precondition
is_false(f) is true.

◆ to_forall

const FormulaForall* to_forall ( const Formula &  f)
friend

Casts f to const FormulaForall*.

Precondition
is_forall(f) is true.

◆ to_greater_than

const FormulaGt* to_greater_than ( const Formula &  f)
friend

Casts f to const FormulaGt*.

Precondition
is_greater_than(f) is true.

◆ to_greater_than_or_equal_to

const FormulaGeq* to_greater_than_or_equal_to ( const Formula &  f)
friend

Casts f to const FormulaGeq*.

Precondition
is_greater_than_or_equal_to(f) is true.

◆ to_less_than

const FormulaLt* to_less_than ( const Formula &  f)
friend

Casts f to const FormulaLt*.

Precondition
is_less_than(f) is true.

◆ to_less_than_or_equal_to

const FormulaLeq* to_less_than_or_equal_to ( const Formula &  f)
friend

Casts f to const FormulaLeq*.

Precondition
is_less_than_or_equal_to(f) is true.

◆ to_nary [1/2]

const NaryFormulaCell* to_nary ( const Formula &  f)
friend

Casts f to const NaryFormulaCell*.

Precondition
is_nary(f) is true.

◆ to_nary [2/2]

NaryFormulaCell* to_nary ( Formula &  f)
friend

Casts f to NaryFormulaCell*.

Precondition
is_nary(f) is true.

◆ to_negation

const FormulaNot* to_negation ( const Formula &  f)
friend

Casts f to const FormulaNot*.

Precondition
is_negation(f) is true.

◆ to_not_equal_to

const FormulaNeq* to_not_equal_to ( const Formula &  f)
friend

Casts f to const FormulaNeq*.

Precondition
is_not_equal_to(f) is true.

◆ to_relational

const RelationalFormulaCell* to_relational ( const Formula &  f)
friend

Casts f to const RelationalFormulaCell*.

Precondition
is_relational(f) is true.

◆ to_true

const FormulaTrue* to_true ( const Formula &  f)
friend

Casts f to const FormulaTrue*.

Precondition
is_true(f) is true.

◆ to_variable

const FormulaVar* to_variable ( const Formula &  f)
friend

Casts f to const FormulaVar*.

Precondition
is_variable(f) is true.
The documentation for this class was generated from the following files: