|
Drake
|
|
Drake
|
#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_bool.h"#include "drake/common/drake_copyable.h"#include "drake/common/eigen_types.h"#include "drake/common/fmt.h"#include "drake/common/hash.h"#include "drake/common/random.h"Classes | |
| class | Formula |
| Represents a symbolic form of a first-order logic formula. More... | |
| struct | ConditionTraits< symbolic::Formula > |
| struct | hash< drake::symbolic::Formula > |
| struct | less< drake::symbolic::Formula > |
| struct | equal_to< drake::symbolic::Formula > |
Namespaces | |
| drake | |
| drake::symbolic | |
| 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 | isinf (const Expression &e) |
Returns a Formula determining if the given expression e is a positive or negative infinity. More... | |
| Formula | isfinite (const Expression &e) |
Returns a Formula determining if the given expression e has a finite value. 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Derived::Scalar, Expression >, Formula > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Derived::Scalar, Expression >, Formula > | positive_semidefinite (const Eigen::TriangularView< Derived, Eigen::Upper > &u) |
Constructs and returns a symbolic positive-semidefinite formula from an upper triangular-view u. More... | |
| std::ostream & | operator<< (std::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 Expression & | get_unary_expression (const Formula &f) |
Returns the expression in a unary expression formula f. More... | |
| const std::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... | |
| template<typename DerivedA , typename DerivedB > | |
| std::enable_if_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar()==typename DerivedB::Scalar()), Formula >, typename internal::RelationalOpTraits< DerivedA, DerivedB >::ReturnType > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename Derived::Scalar()==ScalarType()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(ScalarType()==typename Derived::Scalar()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar()<=typename DerivedB::Scalar()), Formula >, typename internal::RelationalOpTraits< DerivedA, DerivedB >::ReturnType > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename Derived::Scalar()<=ScalarType()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(ScalarType()<=typename Derived::Scalar()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar()< typename DerivedB::Scalar()), Formula >, typename internal::RelationalOpTraits< DerivedA, DerivedB >::ReturnType > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename Derived::Scalar()< ScalarType()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(ScalarType()< typename Derived::Scalar()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar() >=typename DerivedB::Scalar()), Formula >, typename internal::RelationalOpTraits< DerivedA, DerivedB >::ReturnType > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename Derived::Scalar() >=ScalarType()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(ScalarType() >=typename Derived::Scalar()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar() > typename DerivedB::Scalar()), Formula >, typename internal::RelationalOpTraits< DerivedA, DerivedB >::ReturnType > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename Derived::Scalar() > ScalarType()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(ScalarType() > typename Derived::Scalar()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar() !=typename DerivedB::Scalar()), Formula >, typename internal::RelationalOpTraits< DerivedA, DerivedB >::ReturnType > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(typename Derived::Scalar() !=ScalarType()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< Derived >::XprKind, Eigen::ArrayXpr > &&std::is_same_v< decltype(ScalarType() !=typename Derived::Scalar()), Formula >, Eigen::Array< Formula, Derived::RowsAtCompileTime, Derived::ColsAtCompileTime > > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar()==typename DerivedB::Scalar()), Formula >, Formula > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar() !=typename DerivedB::Scalar()), Formula >, Formula > | operator!= (const DerivedA &m1, const DerivedB &m2) |
Returns a symbolic formula representing the condition whether m1 and m2 are not the same. More... | |
| template<typename DerivedA , typename DerivedB > | |
| std::enable_if_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar()< typename DerivedB::Scalar()), Formula >, Formula > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar()<=typename DerivedB::Scalar()), Formula >, Formula > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar() > typename DerivedB::Scalar()), Formula >, Formula > | 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_t< std::is_same_v< typename Eigen::internal::traits< DerivedA >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< typename Eigen::internal::traits< DerivedB >::XprKind, Eigen::MatrixXpr > &&std::is_same_v< decltype(typename DerivedA::Scalar() >=typename DerivedB::Scalar()), Formula >, Formula > | 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... | |