symbolic_expression_cell.h

#pragma once
 
#include <algorithm>  // for cpplint only
#include <atomic>
#include <cstddef>
#include <map>
#include <ostream>
#include <string>
#include <optional>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/symbolic/symbolic_environment.h"
#include "dlinear/symbolic/symbolic_expression.h"
#include "dlinear/symbolic/symbolic_formula.h"
#include "dlinear/symbolic/symbolic_variable.h"
#include "dlinear/symbolic/symbolic_variables.h"
 
namespace dlinear::drake::symbolic {
 
class ExpressionCell {
 public:
  ExpressionKind get_kind() const { return kind_; }
 
  size_t get_hash() const;
 
  const Variables &GetVariables() const;
 
  virtual bool EqualTo(const ExpressionCell &c) const = 0;
 
  virtual bool Less(const ExpressionCell &c) const = 0;
 
  bool is_polynomial() const;
 
  bool include_ite() const;
 
  virtual mpq_class Evaluate(const Environment &env) const = 0;
 
  virtual Expression Expand() = 0;
 
  virtual Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) = 0;
 
  virtual Expression Differentiate(const Variable &x) const = 0;
 
  virtual std::ostream &Display(std::ostream &os) const = 0;
 
  virtual std::string to_smt2_string() const = 0;
 
#ifdef DLINEAR_ENABLED_THREADS
  unsigned use_count() const { return atomic_load_explicit(&rc_, std::memory_order_acquire); }
#else
  unsigned use_count() const { return rc_; }
#endif
 
  ExpressionCell(const ExpressionCell &e) = delete;
 
  ExpressionCell(ExpressionCell &&e) = delete;
 
  ExpressionCell &operator=(ExpressionCell &&e) = delete;
 
  ExpressionCell &operator=(const ExpressionCell &e) = delete;
 
  virtual void UpdateHash();
 
 protected:
  explicit ExpressionCell(ExpressionKind k);
  ExpressionCell(ExpressionKind k, bool is_poly);
  ExpressionCell(ExpressionKind k, bool is_poly, bool include_ite);
  ExpressionCell(ExpressionKind k, bool is_poly, bool include_ite, Variables variables);
  ExpressionCell(ExpressionKind k, bool is_poly, bool include_ite, Variables variables, size_t hash);
  virtual ~ExpressionCell() = default;
  Expression GetExpression();
 
  virtual void ComputeVariables(std::optional<Variables>& variables) const;
  virtual void ComputeHash(std::optional<size_t>& hash) const;
  virtual void ComputeIsPolynomial(std::optional<bool>& is_polynomial) const;
  virtual void ComputeIncludeIte(std::optional<bool>& include_ite) const;
 
  void UpdateHash(size_t hash);
 
 private:
  const ExpressionKind kind_{};
  mutable std::optional<Variables> variables_; 
  mutable std::optional<size_t> hash_{};
  mutable std::optional<bool> is_polynomial_{false};
  mutable std::optional<bool> include_ite_{false};
 
  // Reference counter.
#ifdef DLINEAR_ENABLED_THREADS
  mutable std::atomic<unsigned> rc_{0};
  void increase_rc() const { atomic_fetch_add_explicit(&rc_, 1U, std::memory_order_relaxed); }
  void decrease_rc() const {
    if (atomic_fetch_sub_explicit(&rc_, 1U, std::memory_order_acq_rel) == 1U) {
      delete this;
    }
  }
#else
  mutable unsigned rc_{0};
  void increase_rc() const { ++rc_; }
  void decrease_rc() const {
    if (--rc_ == 0) {
      delete this;
    }
  }
#endif
 
  // So that Expression can call {increase,decrease}_rc.
  friend Expression;
};
 
class UnaryExpressionCell : public ExpressionCell {
 public:
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  const Expression &get_argument() const { return e_; }
 
  UnaryExpressionCell(const UnaryExpressionCell &e) = delete;
 
  UnaryExpressionCell() = delete;
 
  UnaryExpressionCell &operator=(UnaryExpressionCell &&e) = delete;
 
  UnaryExpressionCell &operator=(const UnaryExpressionCell &e) = delete;
 
  UnaryExpressionCell(UnaryExpressionCell &&e) = delete;
 
  ~UnaryExpressionCell() override = default;
 
 protected:
  UnaryExpressionCell(ExpressionKind k, const Expression &e, bool is_poly);
  virtual mpq_class DoEvaluate(const mpq_class &v) const = 0;
 
 private:
  const Expression e_;
 
  void ComputeHash(std::optional<size_t>& hash) const override;
  void ComputeVariables(std::optional<Variables>& variables) const override;
  void ComputeIncludeIte(std::optional<bool>& include_ite) const override;
};
 
class BinaryExpressionCell : public ExpressionCell {
 public:
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  const Expression &get_first_argument() const { return e1_; }
  const Expression &get_second_argument() const { return e2_; }
 
  BinaryExpressionCell(const BinaryExpressionCell &e) = delete;
 
  BinaryExpressionCell(BinaryExpressionCell &&e) = delete;
 
  BinaryExpressionCell() = delete;
 
  BinaryExpressionCell &operator=(BinaryExpressionCell &&e) = delete;
 
  BinaryExpressionCell &operator=(const BinaryExpressionCell &e) = delete;
 
  ~BinaryExpressionCell() override = default;
 
 protected:
  BinaryExpressionCell(ExpressionKind k, const Expression &e1, const Expression &e2, bool is_poly);
  virtual mpq_class DoEvaluate(const mpq_class &v1, const mpq_class &v2) const = 0;
 
 private:
  const Expression e1_;
  const Expression e2_;
 
  void ComputeHash(std::optional<size_t>& hash) const override;
  void ComputeVariables(std::optional<Variables>& variables) const override;
  void ComputeIncludeIte(std::optional<bool>& include_ite) const override;
};
 
class ExpressionVar : public ExpressionCell {
 public:
  explicit ExpressionVar(const Variable &v);
  const Variable &get_variable() const { return var_; }
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
 
 private:
  const Variable var_;
 
  void ComputeHash(std::optional<size_t>& hash) const override;
  std::string to_smt2_string() const override;
};
 
class ExpressionConstant : public ExpressionCell {
 public:
  explicit ExpressionConstant(const mpq_class &v);
  const mpq_class& get_value() const { return v_; }
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
  void UpdateHash() override;
 
 private:
  const mpq_class v_{};
 
  virtual void ComputeHash(std::optional<size_t>& hash) const;
};
 
class ExpressionNaN : public ExpressionCell {
 public:
  ExpressionNaN();
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
};
 
class ExpressionInfty : public ExpressionCell {
 public:
  ExpressionInfty(int sign);
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
  int GetSign() const { return sign_; }
 
 private:
  int sign_ = 1;
};
 
class ExpressionAdd : public ExpressionCell {
 public:
  ExpressionAdd(const mpq_class &constant, std::map<Expression, mpq_class> expr_to_coeff_map);
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
  const mpq_class& get_constant() const { return constant_; }
  const std::map<Expression, mpq_class> &get_expr_to_coeff_map() const { return expr_to_coeff_map_; }
 
  // TODO(soonho): Make the following private and allow
  // only selected functions/method to use them.
  mpq_class &get_mutable_constant() { return constant_; }
  std::map<Expression, mpq_class> &get_mutable_expr_to_coeff_map() { return expr_to_coeff_map_; }
 
  void UpdateHash() override;
 
 private:
  void ComputeVariables(std::optional<Variables>& variables) const override;
  void ComputeHash(std::optional<size_t>& hash) const override;
  void ComputeIsPolynomial(std::optional<bool>& is_polynomial) const override;
  void ComputeIncludeIte(std::optional<bool>& include_ite) const override;
  std::ostream &DisplayTerm(std::ostream &os, bool print_plus, const mpq_class &coeff, const Expression &term) const;
 
  mpq_class constant_{};
  std::map<Expression, mpq_class> expr_to_coeff_map_;
};
 
class ExpressionAddFactory {
 public:
  ExpressionAddFactory(const ExpressionAddFactory &) = default;
  ExpressionAddFactory &operator=(const ExpressionAddFactory &) = default;
  ExpressionAddFactory(ExpressionAddFactory &&) noexcept = default;
  ExpressionAddFactory &operator=(ExpressionAddFactory &&) = default;
 
  ExpressionAddFactory() = default;
 
  ~ExpressionAddFactory() = default;
 
  ExpressionAddFactory(const mpq_class& constant, const std::map<Expression, mpq_class>& expr_to_coeff_map);
  ExpressionAddFactory(mpq_class&& constant, std::map<Expression, mpq_class>&& expr_to_coeff_map);
 
  explicit ExpressionAddFactory(const ExpressionAdd *ptr);
 
  ExpressionAddFactory &AddExpression(const Expression &e);
  ExpressionAddFactory &Add(const ExpressionAdd *ptr);
  ExpressionAddFactory &operator=(const ExpressionAdd *ptr);
 
  ExpressionAddFactory &Negate();
  Expression GetExpression();
 
 private:
  /* Adds constant to this factory.
   * Adding constant constant into an add factory representing
   *
   *     c0 + c1 * t1 + ... + cn * tn
   *
   * results in (c0 + constant) + c1 * t1 + ... + cn * tn.  */
  ExpressionAddFactory &AddConstant(const mpq_class &constant);
  /* Adds coeff * term to this factory.
   *
   * Adding (coeff * term) into an add factory representing
   *
   *     c0 + c1 * t1 + ... + cn * tn
   *
   * results in c0 + c1 * t1 + ... + (coeff * term) + ... + cn * tn. Note that
   * it also performs simplifications to merge the coefficients of common terms.
   */
  ExpressionAddFactory &AddTerm(const mpq_class &coeff, const Expression &term);
  /* Adds expr_to_coeff_map to this factory. It calls AddConstant and AddTerm
   * methods. */
  ExpressionAddFactory &AddMap(const std::map<Expression, mpq_class> &expr_to_coeff_map);
 
  bool get_expression_is_called_{false};
  mpq_class constant_{0.0};
  std::map<Expression, mpq_class> expr_to_coeff_map_;
};
 
class ExpressionMul : public ExpressionCell {
 public:
  ExpressionMul(const mpq_class &constant, std::map<Expression, Expression> base_to_exponent_map);
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
  const mpq_class& get_constant() const { return constant_; }
  const std::map<Expression, Expression> &get_base_to_exponent_map() const { return base_to_exponent_map_; }
 
  // TODO(soonho): Make the following private and allow
  // only selected functions/method to use them.
  mpq_class &get_mutable_constant() { return constant_; }
  std::map<Expression, Expression> &get_mutable_base_to_exponent_map() { return base_to_exponent_map_; }
 
 private:
  void ComputeVariables(std::optional<Variables>& variables) const override;
  void ComputeHash(std::optional<size_t>& hash) const override;
  void ComputeIsPolynomial(std::optional<bool>& is_polynomial) const override;
  void ComputeIncludeIte(std::optional<bool>& include_ite) const override;
 
  std::ostream &DisplayTerm(std::ostream &os, bool print_mul, const Expression &base, const Expression &exponent) const;
 
  mpq_class constant_{};
  std::map<Expression, Expression> base_to_exponent_map_;
};
 
class ExpressionMulFactory {
 public:
  ExpressionMulFactory(const ExpressionMulFactory &) = default;
  ExpressionMulFactory &operator=(const ExpressionMulFactory &) = default;
  ExpressionMulFactory(ExpressionMulFactory &&) noexcept = default;
  ExpressionMulFactory &operator=(ExpressionMulFactory &&) = default;
 
  ExpressionMulFactory() = default;
 
  ~ExpressionMulFactory() = default;
 
  ExpressionMulFactory(const mpq_class &constant, const std::map<Expression, Expression>& base_to_exponent_map);
  ExpressionMulFactory(mpq_class &&constant, std::map<Expression, Expression>&& base_to_exponent_map);
 
  explicit ExpressionMulFactory(const ExpressionMul *ptr);
 
  ExpressionMulFactory &AddExpression(const Expression &e);
  ExpressionMulFactory &Add(const ExpressionMul *ptr);
  ExpressionMulFactory &operator=(const ExpressionMul *ptr);
  ExpressionMulFactory &Negate();
  Expression GetExpression();
 
 private:
  /* Adds constant to this factory.
     Adding constant into an mul factory representing
 
         c * b1 ^ e1 * ... * bn ^ en
 
     results in (constant * c) * b1 ^ e1 * ... * bn ^ en. */
  ExpressionMulFactory &AddConstant(const mpq_class &constant);
  /* Adds pow(base, exponent) to this factory.
     Adding pow(base, exponent) into an mul factory representing
 
         c * b1 ^ e1 * ... * bn ^ en
 
     results in c * b1 ^ e1 * ... * base^exponent * ... * bn ^ en. Note that
     it also performs simplifications to merge the exponents of common bases.
  */
  ExpressionMulFactory &AddTerm(const Expression &base, const Expression &exponent);
  /* Adds base_to_exponent_map to this factory. It calls AddConstant and AddTerm
   * methods. */
  ExpressionMulFactory &AddMap(const std::map<Expression, Expression> &base_to_exponent_map);
 
  bool get_expression_is_called_{false};
  mpq_class constant_{1.0};
  std::map<Expression, Expression> base_to_exponent_map_;
};
 
class ExpressionDiv : public BinaryExpressionCell {
 public:
  ExpressionDiv(const Expression &e1, const Expression &e2);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v1, const mpq_class &v2) const override;
};
 
class ExpressionLog : public UnaryExpressionCell {
 public:
  explicit ExpressionLog(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  friend Expression log(const Expression &e);
 
 private:
  /* Throws std::domain_error if v ∉ [0, +oo). */
  static void check_domain(const mpq_class &v);
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionAbs : public UnaryExpressionCell {
 public:
  explicit ExpressionAbs(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  friend Expression abs(const Expression &e);
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionExp : public UnaryExpressionCell {
 public:
  explicit ExpressionExp(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionSqrt : public UnaryExpressionCell {
 public:
  explicit ExpressionSqrt(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  friend Expression sqrt(const Expression &e);
 
 private:
  /* Throws std::domain_error if v ∉ [0, +oo). */
  static void check_domain(const mpq_class &v);
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionPow : public BinaryExpressionCell {
 public:
  ExpressionPow(const Expression &e1, const Expression &e2);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  friend Expression pow(const Expression &e1, const Expression &e2);
 
 private:
  /* Throws std::domain_error if v1 is finite negative and v2 is finite
     non-integer. */
  static void check_domain(const mpq_class &v1, const mpq_class &v2);
  mpq_class DoEvaluate(const mpq_class &v1, const mpq_class &v2) const override;
};
 
class ExpressionSin : public UnaryExpressionCell {
 public:
  explicit ExpressionSin(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionCos : public UnaryExpressionCell {
 public:
  explicit ExpressionCos(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionTan : public UnaryExpressionCell {
 public:
  explicit ExpressionTan(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionAsin : public UnaryExpressionCell {
 public:
  explicit ExpressionAsin(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  friend Expression asin(const Expression &e);
 
 private:
  /* Throws std::domain_error if v ∉ [-1.0, +1.0]. */
  static void check_domain(const mpq_class &v);
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionAcos : public UnaryExpressionCell {
 public:
  explicit ExpressionAcos(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  friend Expression acos(const Expression &e);
 
 private:
  /* Throws std::domain_error if v ∉ [-1.0, +1.0]. */
  static void check_domain(const mpq_class &v);
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionAtan : public UnaryExpressionCell {
 public:
  explicit ExpressionAtan(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionAtan2 : public BinaryExpressionCell {
 public:
  ExpressionAtan2(const Expression &e1, const Expression &e2);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v1, const mpq_class &v2) const override;
};
 
class ExpressionSinh : public UnaryExpressionCell {
 public:
  explicit ExpressionSinh(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionCosh : public UnaryExpressionCell {
 public:
  explicit ExpressionCosh(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionTanh : public UnaryExpressionCell {
 public:
  explicit ExpressionTanh(const Expression &e);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v) const override;
};
 
class ExpressionMin : public BinaryExpressionCell {
 public:
  ExpressionMin(const Expression &e1, const Expression &e2);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v1, const mpq_class &v2) const override;
};
 
class ExpressionMax : public BinaryExpressionCell {
 public:
  ExpressionMax(const Expression &e1, const Expression &e2);
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
 private:
  mpq_class DoEvaluate(const mpq_class &v1, const mpq_class &v2) const override;
};
 
class ExpressionIfThenElse : public ExpressionCell {
 public:
  ExpressionIfThenElse(const Formula &f_cond, const Expression &e_then, const Expression &e_else);
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  const Formula &get_conditional_formula() const { return f_cond_; }
  const Expression &get_then_expression() const { return e_then_; }
  const Expression &get_else_expression() const { return e_else_; }
 
 private:
  void ComputeVariables(std::optional<Variables>& variables) const override;
  void ComputeHash(std::optional<size_t>& hash) const override;
 
  const Formula f_cond_;
  const Expression e_then_;
  const Expression e_else_;
};
 
class ExpressionUninterpretedFunction : public ExpressionCell {
 public:
  ExpressionUninterpretedFunction(const std::string &name, const Variables &vars);
  bool EqualTo(const ExpressionCell &e) const override;
  bool Less(const ExpressionCell &e) const override;
  mpq_class Evaluate(const Environment &env) const override;
  Expression Expand() override;
  Expression Substitute(const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override;
  Expression Differentiate(const Variable &x) const override;
  std::ostream &Display(std::ostream &os) const override;
  std::string to_smt2_string() const override;
 
  const std::string &get_name() const { return name_; }
 
 private:
  const std::string name_;
  const Variables variables_;
 
  void ComputeHash(std::optional<size_t>& hash) const override;
};
 
bool is_constant(const ExpressionCell &c);
bool is_infinite(const ExpressionCell &c);
bool is_variable(const ExpressionCell &c);
bool is_addition(const ExpressionCell &c);
bool is_multiplication(const ExpressionCell &c);
bool is_division(const ExpressionCell &c);
bool is_log(const ExpressionCell &c);
bool is_abs(const ExpressionCell &c);
bool is_exp(const ExpressionCell &c);
bool is_sqrt(const ExpressionCell &c);
bool is_pow(const ExpressionCell &c);
bool is_sin(const ExpressionCell &c);
bool is_cos(const ExpressionCell &c);
bool is_tan(const ExpressionCell &c);
bool is_asin(const ExpressionCell &c);
bool is_acos(const ExpressionCell &c);
bool is_atan(const ExpressionCell &c);
bool is_atan2(const ExpressionCell &c);
bool is_sinh(const ExpressionCell &c);
bool is_cosh(const ExpressionCell &c);
bool is_tanh(const ExpressionCell &c);
bool is_min(const ExpressionCell &c);
bool is_max(const ExpressionCell &c);
bool is_if_then_else(const ExpressionCell &c);
bool is_uninterpreted_function(const ExpressionCell &c);
 
const ExpressionConstant *to_constant(const ExpressionCell *expr_ptr);
const ExpressionConstant *to_constant(const Expression &e);
 
const ExpressionInfty *to_infty(const ExpressionCell *expr_ptr);
const ExpressionInfty *to_infty(const Expression &e);
 
const ExpressionVar *to_variable(const ExpressionCell *expr_ptr);
const ExpressionVar *to_variable(const Expression &e);
 
const UnaryExpressionCell *to_unary(const ExpressionCell *expr_ptr);
const UnaryExpressionCell *to_unary(const Expression &e);
 
const BinaryExpressionCell *to_binary(const ExpressionCell *expr_ptr);
const BinaryExpressionCell *to_binary(const Expression &e);
 
const ExpressionAdd *to_addition(const ExpressionCell *expr_ptr);
const ExpressionAdd *to_addition(const Expression &e);
ExpressionAdd *to_addition(ExpressionCell *expr_ptr);
ExpressionAdd *to_addition(Expression &e);
 
const ExpressionMul *to_multiplication(const ExpressionCell *expr_ptr);
const ExpressionMul *to_multiplication(const Expression &e);
ExpressionMul *to_multiplication(ExpressionCell *expr_ptr);
ExpressionMul *to_multiplication(Expression &e);
 
const ExpressionDiv *to_division(const ExpressionCell *expr_ptr);
const ExpressionDiv *to_division(const Expression &e);
 
const ExpressionLog *to_log(const ExpressionCell *expr_ptr);
const ExpressionLog *to_log(const Expression &e);
 
const ExpressionExp *to_exp(const ExpressionCell *expr_ptr);
const ExpressionExp *to_exp(const Expression &e);
 
const ExpressionAbs *to_abs(const ExpressionCell *expr_ptr);
const ExpressionAbs *to_abs(const Expression &e);
 
const ExpressionExp *to_exp(const ExpressionCell *expr_ptr);
const ExpressionExp *to_exp(const Expression &e);
 
const ExpressionSqrt *to_sqrt(const ExpressionCell *expr_ptr);
const ExpressionSqrt *to_sqrt(const Expression &e);
 
const ExpressionPow *to_pow(const ExpressionCell *expr_ptr);
const ExpressionPow *to_pow(const Expression &e);
 
const ExpressionSin *to_sin(const ExpressionCell *expr_ptr);
const ExpressionSin *to_sin(const Expression &e);
 
const ExpressionCos *to_cos(const ExpressionCell *expr_ptr);
const ExpressionCos *to_cos(const Expression &e);
 
const ExpressionTan *to_tan(const ExpressionCell *expr_ptr);
const ExpressionTan *to_tan(const Expression &e);
 
const ExpressionAsin *to_asin(const ExpressionCell *expr_ptr);
const ExpressionAsin *to_asin(const Expression &e);
 
const ExpressionAcos *to_acos(const ExpressionCell *expr_ptr);
const ExpressionAcos *to_acos(const Expression &e);
 
const ExpressionAtan *to_atan(const ExpressionCell *expr_ptr);
const ExpressionAtan *to_atan(const Expression &e);
 
const ExpressionAtan2 *to_atan2(const ExpressionCell *expr_ptr);
const ExpressionAtan2 *to_atan2(const Expression &e);
 
const ExpressionSinh *to_sinh(const ExpressionCell *expr_ptr);
const ExpressionSinh *to_sinh(const Expression &e);
 
const ExpressionCosh *to_cosh(const ExpressionCell *expr_ptr);
const ExpressionCosh *to_cosh(const Expression &e);
 
const ExpressionTanh *to_tanh(const ExpressionCell *expr_ptr);
const ExpressionTanh *to_tanh(const Expression &e);
 
const ExpressionMin *to_min(const ExpressionCell *expr_ptr);
const ExpressionMin *to_min(const Expression &e);
 
const ExpressionMax *to_max(const ExpressionCell *expr_ptr);
const ExpressionMax *to_max(const Expression &e);
 
const ExpressionIfThenElse *to_if_then_else(const ExpressionCell *expr_ptr);
const ExpressionIfThenElse *to_if_then_else(const Expression &e);
 
const ExpressionUninterpretedFunction *to_uninterpreted_function(const ExpressionCell *expr_ptr);
const ExpressionUninterpretedFunction *to_uninterpreted_function(const Expression &e);
 
}  // namespace dlinear::drake::symbolic