Drake
symbolic_formula.h File Reference
#include <functional>
#include <memory>
#include <ostream>
#include <set>
#include <string>
#include <utility>
#include <Eigen/Core>
#include "drake/common/drake_assert.h"
#include "drake/common/drake_copyable.h"
#include "drake/common/eigen_types.h"
#include "drake/common/hash.h"
#include "drake/common/symbolic.h"
Include dependency graph for symbolic_formula.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  Formula
 Represents a symbolic form of a first-order logic formula. More...
 
struct  RelationalOpTraits< DerivedA, DerivedB, typename >
 Provides a return type of relational operations (=, ≠, ≤, <, ≥, >) between Eigen::Arrays. More...
 
struct  hash_value< symbolic::Formula >
 Computes the hash value of a symbolic formula. More...
 
struct  ConditionTraits< symbolic::Formula >
 
struct  less< drake::symbolic::Formula >
 
struct  equal_to< drake::symbolic::Formula >
 

Namespaces

 drake
 
 drake::symbolic
 
 drake::symbolic::detail
 
 drake::assert
 

Enumerations

enum  FormulaKind {
  False, True, Var, Eq,
  Neq, Gt, Geq, Lt,
  Leq, And, Or, Not,
  Forall, Isnan, PositiveSemidefinite
}
 Kinds of symbolic formulas. More...
 

Functions

bool operator< (FormulaKind k1, FormulaKind k2)
 
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 operator&& (const Formula &f1, const Formula &f2)
 
Formula operator&& (const Variable &v, const Formula &f)
 
Formula operator&& (const Formula &f, const Variable &v)
 
Formula operator&& (const Variable &v1, const Variable &v2)
 
Formula make_disjunction (const std::set< Formula > &formulas)
 Returns a disjunction of formulas. More...
 
Formula operator|| (const Formula &f1, const Formula &f2)
 
Formula operator|| (const Variable &v, const Formula &f)
 
Formula operator|| (const Formula &f, const Variable &v)
 
Formula operator|| (const Variable &v1, const Variable &v2)
 
Formula operator! (const Formula &f)
 
Formula operator! (const Variable &v)
 
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)
 
Formula operator> (const Expression &e1, const Expression &e2)
 
Formula operator>= (const Expression &e1, const Expression &e2)
 
Formula isnan (const Expression &e)
 Returns a Formula for the predicate isnan(e) to the given expression. More...
 
Formula positive_semidefinite (const Eigen::Ref< const MatrixX< Expression >> &m)
 Returns a symbolic formula constraining m to be a positive-semidefinite matrix. More...
 
Formula positive_semidefinite (const MatrixX< Expression > &m, Eigen::UpLoType mode)
 Constructs and returns a symbolic positive-semidefinite formula from m. More...
 
template<typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Derived::Scalar, Expression >::value, Formula >::type positive_semidefinite (const Eigen::TriangularView< Derived, Eigen::Lower > &l)
 Constructs and returns a symbolic positive-semidefinite formula from a lower triangular-view l. More...
 
template<typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Derived::Scalar, Expression >::value, Formula >::type positive_semidefinite (const Eigen::TriangularView< Derived, Eigen::Upper > &u)
 Constructs and returns a symbolic positive-semidefinite formula from an upper triangular-view u. More...
 
ostream & operator<< (ostream &os, const Formula &f)
 
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_nary (const Formula &f)
 Checks if f is a n-ary formula ({∧, ∨}). 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...
 
const Variable & get_variable (const Formula &f)
 Returns the embedded variable in the variable formula f. More...
 
const Expression & get_lhs_expression (const Formula &f)
 Returns the lhs-argument of a relational formula f. More...
 
const Expression & get_rhs_expression (const Formula &f)
 Returns the rhs-argument of a relational formula f. More...
 
const set< Formula > & get_operands (const Formula &f)
 Returns the set of formulas in a n-ary formula f. More...
 
const Formula & get_operand (const Formula &f)
 Returns the formula in a negation formula f. More...
 
const Variables & get_quantified_variables (const Formula &f)
 Returns the quantified variables in a forall formula f. More...
 
const Formula & get_quantified_formula (const Formula &f)
 Returns the quantified formula in a forall formula f. More...
 
const MatrixX< Expression > & get_matrix_in_positive_semidefinite (const Formula &f)
 Returns the matrix in a positive-semidefinite formula f. More...
 
Formula logic_and (const Formula &f1, const Formula &f2)
 Returns f1f2. More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()==typename DerivedB::Scalar()), Formula >::value, typename detail::RelationalOpTraits< DerivedA, DerivedB >::ReturnType >::type operator== (const DerivedA &a1, const DerivedB &a2)
 Returns an Eigen array of symbolic formulas where each element includes element-wise symbolic-equality of two arrays m1 and m2. More...
 
template<typename Derived , typename ScalarType >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename Derived::Scalar()==ScalarType()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator== (const Derived &a, const ScalarType &v)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between an array a and a scalar v using equal-to operator (==). More...
 
template<typename ScalarType , typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(ScalarType()==typename Derived::Scalar()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator== (const ScalarType &v, const Derived &a)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between a scalar v and an array using equal-to operator (==). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()<=typename DerivedB::Scalar()), Formula >::value, typename detail::RelationalOpTraits< DerivedA, DerivedB >::ReturnType >::type operator<= (const DerivedA &a1, const DerivedB &a2)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison of two arrays a1 and a2 using less-than-or-equal operator (<=). More...
 
template<typename Derived , typename ScalarType >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename Derived::Scalar()<=ScalarType()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator<= (const Derived &a, const ScalarType &v)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between an array a and a scalar v using less-than-or-equal operator (<=). More...
 
template<typename ScalarType , typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(ScalarType()<=typename Derived::Scalar()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator<= (const ScalarType &v, const Derived &a)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between a scalar v and an array using less-than-or-equal operator (<=). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()< typename DerivedB::Scalar()), Formula >::value, typename detail::RelationalOpTraits< DerivedA, DerivedB >::ReturnType >::type operator< (const DerivedA &a1, const DerivedB &a2)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison of two arrays a1 and a2 using less-than operator (<). More...
 
template<typename Derived , typename ScalarType >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename Derived::Scalar()< ScalarType()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator< (const Derived &a, const ScalarType &v)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between an array a and a scalar v using less-than operator (<). More...
 
template<typename ScalarType , typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(ScalarType()< typename Derived::Scalar()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator< (const ScalarType &v, const Derived &a)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between a scalar v and an array using less-than operator (<). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar() >=typename DerivedB::Scalar()), Formula >::value, typename detail::RelationalOpTraits< DerivedA, DerivedB >::ReturnType >::type operator>= (const DerivedA &a1, const DerivedB &a2)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison of two arrays a1 and a2 using greater-than-or-equal operator (>=). More...
 
template<typename Derived , typename ScalarType >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename Derived::Scalar() >=ScalarType()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator>= (const Derived &a, const ScalarType &v)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between an array a and a scalar v using greater-than-or-equal operator (>=). More...
 
template<typename ScalarType , typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(ScalarType() >=typename Derived::Scalar()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator>= (const ScalarType &v, const Derived &a)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between a scalar v and an array using less-than-or-equal operator (<=) instead of greater-than-or-equal operator (>=). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar() > typename DerivedB::Scalar()), Formula >::value, typename detail::RelationalOpTraits< DerivedA, DerivedB >::ReturnType >::type operator> (const DerivedA &a1, const DerivedB &a2)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison of two arrays a1 and a2 using greater-than operator (>). More...
 
template<typename Derived , typename ScalarType >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename Derived::Scalar() > ScalarType()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator> (const Derived &a, const ScalarType &v)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between an array a and a scalar v using greater-than operator (>). More...
 
template<typename ScalarType , typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(ScalarType() > typename Derived::Scalar()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator> (const ScalarType &v, const Derived &a)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between a scalar v and an array using less-than operator (<) instead of greater-than operator (>). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()!=typename DerivedB::Scalar()), Formula >::value, typename detail::RelationalOpTraits< DerivedA, DerivedB >::ReturnType >::type operator!= (const DerivedA &a1, const DerivedB &a2)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison of two arrays a1 and a2 using not-equal operator (!=). More...
 
template<typename Derived , typename ScalarType >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(typename Derived::Scalar()!=ScalarType()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator!= (const Derived &a, const ScalarType &v)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between an array a and a scalar v using not-equal operator (!=). More...
 
template<typename ScalarType , typename Derived >
std::enable_if< std::is_same< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr >::value &&std::is_same< decltype(ScalarType()!=typename Derived::Scalar()), Formula >::value, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > >::type operator!= (const ScalarType &v, const Derived &a)
 Returns an Eigen array of symbolic formulas where each element includes element-wise comparison between a scalar v and an array using not-equal operator (!=). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()==typename DerivedB::Scalar()), Formula >::value, Formula >::type operator== (const DerivedA &m1, const DerivedB &m2)
 Returns a symbolic formula checking if two matrices m1 and m2 are equal. More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()!=typename DerivedB::Scalar()), Formula >::value, Formula >::type operator!= (const DerivedA &m1, const DerivedB &m2)
 Returns a symbolic formula representing element-wise comparison between two matrices m1 and m2 using not-equal (!=) operator. More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()< typename DerivedB::Scalar()), Formula >::value, Formula >::type operator< (const DerivedA &m1, const DerivedB &m2)
 Returns a symbolic formula representing element-wise comparison between two matrices m1 and m2 using less-than (<) operator. More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar()<=typename DerivedB::Scalar()), Formula >::value, Formula >::type operator<= (const DerivedA &m1, const DerivedB &m2)
 Returns a symbolic formula representing element-wise comparison between two matrices m1 and m2 using less-than-or-equal operator (<=). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar() > typename DerivedB::Scalar()), Formula >::value, Formula >::type operator> (const DerivedA &m1, const DerivedB &m2)
 Returns a symbolic formula representing element-wise comparison between two matrices m1 and m2 using greater-than operator (>). More...
 
template<typename DerivedA , typename DerivedB >
std::enable_if< std::is_same< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr >::value &&std::is_same< decltype(typename DerivedA::Scalar() >=typename DerivedB::Scalar()), Formula >::value, Formula >::type operator>= (const DerivedA &m1, const DerivedB &m2)
 Returns a symbolic formula representing element-wise comparison between two matrices m1 and m2 using greater-than-or-equal operator (>=). More...