symbolic_expression.h

#pragma once
 
#include <algorithm>  // for cpplint only
#include <cstddef>
#include <functional>
#include <limits>
#include <map>
#include <ostream>
#include <string>
#include <type_traits>
#include <unordered_map>
#include <utility>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/symbolic/hash.h"
#include "dlinear/symbolic/symbolic_environment.h"
#include "dlinear/symbolic/symbolic_variable.h"
#include "dlinear/symbolic/symbolic_variables.h"
 
namespace dlinear::drake {
namespace symbolic {
 
enum class ExpressionKind {
  Constant,               
  Var,                    
  Add,                    
  Mul,                    
  Div,                    
  Log,                    
  Abs,                    
  Exp,                    
  Sqrt,                   
  Pow,                    
  Sin,                    
  Cos,                    
  Tan,                    
  Asin,                   
  Acos,                   
  Atan,                   
  Atan2,                  
  Sinh,                   
  Cosh,                   
  Tanh,                   
  Min,                    
  Max,                    
  IfThenElse,             
  NaN,                    
  Infty,                  
  UninterpretedFunction,  
  // TODO(soonho): add Integral
};
 
bool operator<(ExpressionKind k1, ExpressionKind k2);
 
class ExpressionCell;                   // In symbolic_expression_cell.h
class ExpressionConstant;               // In symbolic_expression_cell.h
class ExpressionInfty;                  // In symbolic_expression_cell.h
class ExpressionVar;                    // In symbolic_expression_cell.h
class UnaryExpressionCell;              // In symbolic_expression_cell.h
class BinaryExpressionCell;             // In symbolic_expression_cell.h
class ExpressionAdd;                    // In symbolic_expression_cell.h
class ExpressionMul;                    // In symbolic_expression_cell.h
class ExpressionDiv;                    // In symbolic_expression_cell.h
class ExpressionLog;                    // In symbolic_expression_cell.h
class ExpressionAbs;                    // In symbolic_expression_cell.h
class ExpressionExp;                    // In symbolic_expression_cell.h
class ExpressionSqrt;                   // In symbolic_expression_cell.h
class ExpressionPow;                    // In symbolic_expression_cell.h
class ExpressionSin;                    // In symbolic_expression_cell.h
class ExpressionCos;                    // In symbolic_expression_cell.h
class ExpressionTan;                    // In symbolic_expression_cell.h
class ExpressionAsin;                   // In symbolic_expression_cell.h
class ExpressionAcos;                   // In symbolic_expression_cell.h
class ExpressionAtan;                   // In symbolic_expression_cell.h
class ExpressionAtan2;                  // In symbolic_expression_cell.h
class ExpressionSinh;                   // In symbolic_expression_cell.h
class ExpressionCosh;                   // In symbolic_expression_cell.h
class ExpressionTanh;                   // In symbolic_expression_cell.h
class ExpressionMin;                    // In symbolic_expression_cell.h
class ExpressionMax;                    // In symbolic_expression_cell.h
class ExpressionIfThenElse;             // In symbolic_expression_cell.h
class ExpressionUninterpretedFunction;  // In symbolic_expression_cell.h
class Formula;                          // In symbolic_formula.h
class Expression;
 
// ExpressionSubstitution is a map from a Variable to a symbolic expression. It
// is used in Expression::Substitute and Formula::Substitute methods as an
// argument.
using ExpressionSubstitution = std::unordered_map<Variable, Expression, hash_value<Variable>>;
 
// FormulaSubstitution is a map from a Variable to a symbolic formula. It
// is used in Expression::Substitute and Formula::Substitute methods as an
// argument.
using FormulaSubstitution = std::unordered_map<Variable, Formula, hash_value<Variable>>;
 
class Expression {
 public:
  Expression(const Expression &);
  Expression &operator=(const Expression &);
  Expression(Expression &&) noexcept;
  Expression &operator=(Expression &&) noexcept;
  ~Expression();
 
  Expression();
 
  // NOLINTNEXTLINE(runtime/explicit): This conversion is desirable.
  Expression(const mpq_class &d);
  // NOLINTNEXTLINE(runtime/explicit): This conversion is desirable.
  Expression(const double d);
  Expression(int d);
  Expression(long d);
  Expression(uint32_t d);
  Expression(uint64_t d);
  // NOLINTNEXTLINE(runtime/explicit): This conversion is desirable.
  Expression(const Variable &var);
  ExpressionKind get_kind() const;
  size_t get_hash() const;
  const Variables &GetVariables() const;
 
  void Swap(Expression &e);
 
  bool EqualTo(const Expression &e) const;
 
  bool Less(const Expression &e) const;
 
  bool is_polynomial() const;
 
  bool include_ite() const;
 
  mpq_class Evaluate(const Environment &env = Environment{}) const;
 
  Expression EvaluatePartial(const Environment &env) const;
 
  Expression Expand() const;
 
  Expression Substitute(const Variable &var, const Expression &e) const;
 
  Expression Substitute(const ExpressionSubstitution &expr_subst,
                        const FormulaSubstitution &formula_subst) const;
 
  Expression Substitute(const ExpressionSubstitution &expr_subst) const;
 
  Expression Substitute(const FormulaSubstitution &formula_subst) const;
 
  Expression Differentiate(const Variable &x) const;
 
  std::string to_string() const;
  std::string to_smt2_string() const;
 
  static Expression Zero();
  static Expression One();
  static Expression Pi();
  static Expression E();
  static Expression NaN();
  static Expression Infty();
  static Expression NInfty();
 
  friend Expression operator+(const Expression &lhs, const Expression &rhs);
  friend Expression operator+(const Expression &lhs, Expression &&rhs);
  friend Expression operator+(Expression &&lhs, const Expression &rhs);
  friend Expression operator+(Expression &&lhs, Expression &&rhs);
  // NOLINTNEXTLINE(runtime/references) per C++ standard signature.
  friend Expression &operator+=(Expression &lhs, const Expression &rhs);
 
  Expression &operator++();
  Expression operator++(int);
 
  friend Expression operator-(const Expression &lhs, const Expression &rhs);
  friend Expression operator-(const Expression &lhs, Expression &&rhs);
  friend Expression operator-(Expression &&lhs, const Expression &rhs);
  friend Expression operator-(Expression &&lhs, Expression &&rhs);
  // NOLINTNEXTLINE(runtime/references) per C++ standard signature.
  friend Expression &operator-=(Expression &lhs, const Expression &rhs);
 
  friend Expression operator+(const Expression &e);
 
  friend Expression operator-(const Expression &e);
  friend Expression operator-(Expression &&e);
 
  Expression &operator--();
  Expression operator--(int);
 
  friend Expression operator*(const Expression &lhs, const Expression &rhs);
  friend Expression operator*(const Expression &lhs, Expression &&rhs);
  friend Expression operator*(Expression &&lhs, const Expression &rhs);
  friend Expression operator*(Expression &&lhs, Expression &&rhs);
  // NOLINTNEXTLINE(runtime/references) per C++ standard signature.
  friend Expression &operator*=(Expression &lhs, const Expression &rhs);
 
  friend Expression operator/(Expression lhs, const Expression &rhs);
  // NOLINTNEXTLINE(runtime/references) per C++ standard signature.
  friend Expression &operator/=(Expression &lhs, const Expression &rhs);
 
  friend Expression log(const Expression &e);
  friend Expression abs(const Expression &e);
  friend Expression exp(const Expression &e);
  friend Expression sqrt(const Expression &e);
  friend Expression pow(const Expression &e1, const Expression &e2);
  friend Expression sin(const Expression &e);
  friend Expression cos(const Expression &e);
  friend Expression tan(const Expression &e);
  friend Expression asin(const Expression &e);
  friend Expression acos(const Expression &e);
  friend Expression atan(const Expression &e);
  friend Expression atan2(const Expression &e1, const Expression &e2);
  friend Expression sinh(const Expression &e);
  friend Expression cosh(const Expression &e);
  friend Expression tanh(const Expression &e);
  friend Expression min(const Expression &e1, const Expression &e2);
  friend Expression max(const Expression &e1, const Expression &e2);
 
  friend Expression if_then_else(const Formula &f_cond,
                                 const Expression &e_then,
                                 const Expression &e_else);
  friend Expression uninterpreted_function(const std::string &name,
                                           const Variables &vars);
 
  friend std::ostream &operator<<(std::ostream &os, const Expression &e);
  friend void swap(Expression &a, Expression &b) { std::swap(a.ptr_, b.ptr_); }
 
  friend bool is_constant(const Expression &e);
  friend bool is_variable(const Expression &e);
  friend bool is_addition(const Expression &e);
  friend bool is_multiplication(const Expression &e);
  friend bool is_division(const Expression &e);
  friend bool is_log(const Expression &e);
  friend bool is_abs(const Expression &e);
  friend bool is_exp(const Expression &e);
  friend bool is_sqrt(const Expression &e);
  friend bool is_pow(const Expression &e);
  friend bool is_sin(const Expression &e);
  friend bool is_cos(const Expression &e);
  friend bool is_tan(const Expression &e);
  friend bool is_asin(const Expression &e);
  friend bool is_acos(const Expression &e);
  friend bool is_atan(const Expression &e);
  friend bool is_atan2(const Expression &e);
  friend bool is_sinh(const Expression &e);
  friend bool is_cosh(const Expression &e);
  friend bool is_tanh(const Expression &e);
  friend bool is_min(const Expression &e);
  friend bool is_max(const Expression &e);
  friend bool is_if_then_else(const Expression &e);
  friend bool is_uninterpreted_function(const Expression &e);
 
  // Note that the following cast functions are only for low-level operations
  // and not exposed to the user of symbolic/symbolic_expression.h
  // header. These functions are declared in
  // symbolic/symbolic_expression_cell.h header.
  friend const ExpressionConstant *to_constant(const Expression &e);
  friend const ExpressionInfty *to_infty(const Expression &e);
  friend const ExpressionVar *to_variable(const Expression &e);
  friend const UnaryExpressionCell *to_unary(const Expression &e);
  friend const BinaryExpressionCell *to_binary(const Expression &e);
  friend const ExpressionAdd *to_addition(const Expression &e);
  friend ExpressionAdd *to_addition(Expression &e);
  friend const ExpressionMul *to_multiplication(const Expression &e);
  friend ExpressionMul *to_multiplication(Expression &e);
  friend const ExpressionDiv *to_division(const Expression &e);
  friend const ExpressionLog *to_log(const Expression &e);
  friend const ExpressionAbs *to_abs(const Expression &e);
  friend const ExpressionExp *to_exp(const Expression &e);
  friend const ExpressionSqrt *to_sqrt(const Expression &e);
  friend const ExpressionPow *to_pow(const Expression &e);
  friend const ExpressionSin *to_sin(const Expression &e);
  friend const ExpressionCos *to_cos(const Expression &e);
  friend const ExpressionTan *to_tan(const Expression &e);
  friend const ExpressionAsin *to_asin(const Expression &e);
  friend const ExpressionAcos *to_acos(const Expression &e);
  friend const ExpressionAtan *to_atan(const Expression &e);
  friend const ExpressionAtan2 *to_atan2(const Expression &e);
  friend const ExpressionSinh *to_sinh(const Expression &e);
  friend const ExpressionCosh *to_cosh(const Expression &e);
  friend const ExpressionTanh *to_tanh(const Expression &e);
  friend const ExpressionMin *to_min(const Expression &e);
  friend const ExpressionMax *to_max(const Expression &e);
  friend const ExpressionIfThenElse *to_if_then_else(const Expression &e);
  friend const ExpressionUninterpretedFunction *to_uninterpreted_function(
      const Expression &e);
 
  friend class ExpressionAddFactory;
  friend class ExpressionMulFactory;
  friend class ExpressionCell;
 
 private:
  static ExpressionCell *make_cell(const mpq_class &d);
  static ExpressionCell *make_cell(const double d);
 
  explicit Expression(ExpressionCell *ptr);
 
  ExpressionCell *ptr_{nullptr};
};
 
Expression operator+(const Expression &lhs, const Expression &rhs);
Expression operator+(const Expression &lhs, Expression &&rhs);
Expression operator+(Expression &&lhs, const Expression &rhs);
Expression operator+(Expression &&lhs, Expression &&rhs);
// NOLINTNEXTLINE(runtime/references) per C++ standard signature.
Expression &operator+=(Expression &lhs, const Expression &rhs);
 
Expression operator-(const Expression &lhs, const Expression &rhs);
Expression operator-(const Expression &lhs, Expression &&rhs);
Expression operator-(Expression &&lhs, const Expression &rhs);
Expression operator-(Expression &&lhs, Expression &&rhs);
// NOLINTNEXTLINE(runtime/references) per C++ standard signature.
Expression &operator-=(Expression &lhs, const Expression &rhs);
 
Expression operator+(const Expression &e);
 
Expression operator-(const Expression &e);
Expression operator-(Expression &&e);
 
Expression operator*(const Expression &lhs, const Expression &rhs);
Expression operator*(const Expression &lhs, Expression &&rhs);
Expression operator*(Expression &&lhs, const Expression &rhs);
Expression operator*(Expression &&lhs, Expression &&rhs);
// NOLINTNEXTLINE(runtime/references) per C++ standard signature.
Expression &operator*=(Expression &lhs, const Expression &rhs);
 
Expression operator/(Expression lhs, const Expression &rhs);
// NOLINTNEXTLINE(runtime/references) per C++ standard signature.
Expression &operator/=(Expression &lhs, const Expression &rhs);
 
Expression Sum(const std::vector<Expression> &expressions);
 
Expression Prod(const std::vector<Expression> &expressions);
 
Expression log(const Expression &e);
Expression abs(const Expression &e);
Expression exp(const Expression &e);
Expression sqrt(const Expression &e);
Expression pow(const Expression &e1, const Expression &e2);
Expression sin(const Expression &e);
Expression cos(const Expression &e);
Expression tan(const Expression &e);
Expression asin(const Expression &e);
Expression acos(const Expression &e);
Expression atan(const Expression &e);
Expression atan2(const Expression &e1, const Expression &e2);
Expression sinh(const Expression &e);
Expression cosh(const Expression &e);
Expression tanh(const Expression &e);
Expression min(const Expression &e1, const Expression &e2);
Expression max(const Expression &e1, const Expression &e2);
Expression if_then_else(const Formula &f_cond, const Expression &e_then,
                        const Expression &e_else);
 
Expression uninterpreted_function(const std::string &name, const Variables &vars);
void swap(Expression &a, Expression &b);
 
std::ostream &operator<<(std::ostream &os, const Expression &e);
 
bool is_constant(const Expression &e);
bool is_constant(const Expression &e, const mpq_class &v);
bool is_zero(const Expression &e);
bool is_one(const Expression &e);
bool is_neg_one(const Expression &e);
bool is_two(const Expression &e);
bool is_nan(const Expression &e);
bool is_infinite(const Expression &e);
bool is_infinity(const Expression &e);
bool is_negative_infinity(const Expression &e);
bool is_variable(const Expression &e);
bool is_addition(const Expression &e);
bool is_multiplication(const Expression &e);
bool is_division(const Expression &e);
bool is_log(const Expression &e);
bool is_abs(const Expression &e);
bool is_exp(const Expression &e);
bool is_sqrt(const Expression &e);
bool is_pow(const Expression &e);
bool is_sin(const Expression &e);
bool is_cos(const Expression &e);
bool is_tan(const Expression &e);
bool is_asin(const Expression &e);
bool is_acos(const Expression &e);
bool is_atan(const Expression &e);
bool is_atan2(const Expression &e);
bool is_sinh(const Expression &e);
bool is_cosh(const Expression &e);
bool is_tanh(const Expression &e);
bool is_min(const Expression &e);
bool is_max(const Expression &e);
bool is_if_then_else(const Expression &e);
bool is_uninterpreted_function(const Expression &e);
 
const mpq_class& get_constant_value(const Expression &e);
const Variable &get_variable(const Expression &e);
const Expression &get_argument(const Expression &e);
const Expression &get_first_argument(const Expression &e);
const Expression &get_second_argument(const Expression &e);
const mpq_class& get_constant_in_addition(const Expression &e);
const std::map<Expression, mpq_class> &get_expr_to_coeff_map_in_addition(
    const Expression &e);
const mpq_class& get_constant_in_multiplication(const Expression &e);
const std::map<Expression, Expression> &
get_base_to_exponent_map_in_multiplication(const Expression &e);
 
const Formula &get_conditional_formula(const Expression &e);
 
const Expression &get_then_expression(const Expression &e);
 
const Expression &get_else_expression(const Expression &e);
 
const std::string &get_uninterpreted_function_name(const Expression &e);
 
Expression operator+(const Variable &var);
Expression operator-(const Variable &var);
 
}  // namespace symbolic
 
} // namespace dlinear::drake
 
 
namespace std {
/* Provides std::less<dlinear::drake::symbolic::Expression>. */
template<>
struct less<dlinear::drake::symbolic::Expression> {
  bool operator()(const dlinear::drake::symbolic::Expression &lhs,
                  const dlinear::drake::symbolic::Expression &rhs) const {
    return lhs.Less(rhs);
  }
};
 
/* Provides std::equal_to<dlinear::drake::symbolic::Expression>. */
template<>
struct equal_to<dlinear::drake::symbolic::Expression> {
  bool operator()(const dlinear::drake::symbolic::Expression &lhs,
                  const dlinear::drake::symbolic::Expression &rhs) const {
    return lhs.EqualTo(rhs);
  }
};
 
template<>
struct hash<dlinear::drake::symbolic::Expression> {
  size_t operator()(const dlinear::drake::symbolic::Expression &e) const {
    return e.get_hash();
  }
};
 
/* Provides std::numeric_limits<dlinear::drake::symbolic::Expression>. */
template<>
struct numeric_limits<dlinear::drake::symbolic::Expression>
    : public numeric_limits<mpq_class> {
  static const bool has_infinity = true;
  static mpq_class infinity();
};
 
}  // namespace std