symbolic_formula.h

 
#pragma once
 
#include <functional>
#include <ostream>
#include <set>
#include <string>
#include <utility>
 
#include "dlinear/symbolic/hash.h"
#include "dlinear/symbolic/symbolic_environment.h"
#include "dlinear/symbolic/symbolic_expression.h"
#include "dlinear/symbolic/symbolic_variable.h"
#include "dlinear/symbolic/symbolic_variables.h"
 
namespace dlinear::drake {
namespace symbolic {
 
enum class FormulaKind {
  False,   
  True,    
  Var,     
  Eq,      
  Neq,     
  Gt,      
  Geq,     
  Lt,      
  Leq,     
  And,     
  Or,      
  Not,     
  Forall,  
};
 
// Total ordering between FormulaKinds
bool operator<(FormulaKind k1, FormulaKind k2);
 
class FormulaCell;            // In symbolic/symbolic_formula_cell.h
class FormulaFalse;           // In symbolic/symbolic_formula_cell.h
class FormulaTrue;            // In symbolic/symbolic_formula_cell.h
class FormulaVar;             // In symbolic/symbolic_formula_cell.h
class RelationalFormulaCell;  // In symbolic/symbolic_formula_cell.h
class FormulaEq;              // In symbolic/symbolic_formula_cell.h
class FormulaNeq;             // In symbolic/symbolic_formula_cell.h
class FormulaGt;              // In symbolic/symbolic_formula_cell.h
class FormulaGeq;             // In symbolic/symbolic_formula_cell.h
class FormulaLt;              // In symbolic/symbolic_formula_cell.h
class FormulaLeq;             // In symbolic/symbolic_formula_cell.h
class NaryFormulaCell;        // In symbolic/symbolic_formula_cell.h
class FormulaNot;             // In symbolic/symbolic_formula_cell.h
class FormulaAnd;             // In symbolic/symbolic_formula_cell.h
class FormulaOr;              // In symbolic/symbolic_formula_cell.h
class FormulaForall;          // In symbolic/symbolic_formula_cell.h
 
class Formula {
 public:
  Formula();
  Formula(const Formula &);
  Formula &operator=(const Formula &);
  Formula(Formula &&) noexcept;
  Formula &operator=(Formula &&) noexcept;
  ~Formula();
 
  explicit Formula(const Variable &var);
 
  FormulaKind get_kind() const;
  size_t get_hash() const;
 
  const Variables &GetFreeVariables() const;
 
  bool EqualTo(const Formula &f) const;
 
  bool IsFlattened() const;
 
  bool Less(const Formula &f) const;
 
  bool Evaluate(const Environment &env = Environment{}) const;
 
  Formula Substitute(const Variable &var, const Expression &e) const;
 
  Formula Substitute(const Variable &var, const Formula &f) const;
 
  Formula Substitute(const ExpressionSubstitution &expr_subst,
                     const FormulaSubstitution &formula_subst) const;
 
  Formula Substitute(const ExpressionSubstitution &expr_subst) const;
 
  Formula Substitute(const FormulaSubstitution &formula_subst) const;
 
  std::string to_string() const;
 
  std::string to_smt2_string() const;
 
  static Formula True();
  static Formula False();
 
  explicit operator bool() const { return Evaluate(); }
 
  friend std::ostream &operator<<(std::ostream &os, const Formula &f);
  friend void swap(Formula &a, Formula &b) { std::swap(a.ptr_, b.ptr_); }
 
  friend bool is_false(const Formula &f);
  friend bool is_true(const Formula &f);
  friend bool is_variable(const Formula &f);
  friend bool is_equal_to(const Formula &f);
  friend bool is_not_equal_to(const Formula &f);
  friend bool is_greater_than(const Formula &f);
  friend bool is_greater_than_or_equal_to(const Formula &f);
  friend bool is_less_than(const Formula &f);
  friend bool is_less_than_or_equal_to(const Formula &f);
  friend bool is_relational(const Formula &f);
  friend bool is_conjunction(const Formula &f);
  friend bool is_disjunction(const Formula &f);
  friend bool is_negation(const Formula &f);
  friend bool is_forall(const Formula &f);
 
  // Note that the following cast functions are only for low-level operations
  // and not exposed to the user of symbolic_formula.h. These functions are
  // declared in symbolic_formula_cell.h header.
  friend const FormulaFalse *to_false(const Formula &f);
  friend const FormulaTrue *to_true(const Formula &f);
  friend const FormulaVar *to_variable(const Formula &f);
  friend const RelationalFormulaCell *to_relational(const Formula &f);
  friend const FormulaEq *to_equal_to(const Formula &f);
  friend const FormulaNeq *to_not_equal_to(const Formula &f);
  friend const FormulaGt *to_greater_than(const Formula &f);
  friend const FormulaGeq *to_greater_than_or_equal_to(const Formula &f);
  friend const FormulaLt *to_less_than(const Formula &f);
  friend const FormulaLeq *to_less_than_or_equal_to(const Formula &f);
  friend const NaryFormulaCell *to_nary(const Formula &f);
  friend NaryFormulaCell *to_nary(Formula &f);
  friend const FormulaAnd *to_conjunction(const Formula &f);
  friend const FormulaOr *to_disjunction(const Formula &f);
  friend const FormulaNot *to_negation(const Formula &f);
  friend const FormulaForall *to_forall(const Formula &f);
 
  // Returns f1 = f1 && f2.
  static Formula make_conjunction(Formula &f1, const Formula &f2);
  // Returns f1 = f1 || f2.
  static Formula make_disjunction(Formula &f1, const Formula &f2);
 
  friend FormulaCell;
  friend Formula forall(const Variables &vars, const Formula &f);
  friend Formula make_conjunction(const std::set<Formula> &formulas);
  friend Formula make_disjunction(const std::set<Formula> &formulas);
  friend Formula operator!(const Formula &f);
  friend Formula operator==(const Expression &e1, const Expression &e2);
  friend Formula operator!=(const Expression &e1, const Expression &e2);
  friend Formula operator<(const Expression &e1, const Expression &e2);
  friend Formula operator<=(const Expression &e1, const Expression &e2);
  friend Formula operator>(const Expression &e1, const Expression &e2);
  friend Formula operator>=(const Expression &e1, const Expression &e2);
  Formula &operator&=(const Formula &f2);
 
  bool include_ite() const;
 
 private:
  explicit Formula(FormulaCell *ptr);
 
  FormulaCell *ptr_;
};
 
Formula forall(const Variables &vars, const Formula &f);
 
Formula make_conjunction(const std::set<Formula> &formulas);
Formula operator&&(const Formula &f1, const Formula &f2);
Formula operator&&(const Formula &f1, Formula &&f2);
Formula operator&&(Formula &&f1, const Formula &f2);
Formula operator&&(Formula &&f1, Formula &&f2);
 
Formula operator&&(const Variable &v, const Formula &f);
Formula operator&&(const Variable &v, Formula &&f);
Formula operator&&(const Formula &f, const Variable &v);
Formula operator&&(Formula &&f, const Variable &v);
Formula operator&&(const Variable &v1, const Variable &v2);
 
Formula make_disjunction(const std::set<Formula> &formulas);
Formula operator||(const Formula &f1, const Formula &f2);
Formula operator||(const Formula &f1, Formula &&f2);
Formula operator||(Formula &&f1, const Formula &f2);
Formula operator||(Formula &&f1, Formula &&f2);
 
Formula operator||(const Variable &v, const Formula &f);
Formula operator||(const Variable &v, Formula &&f);
Formula operator||(const Formula &f, const Variable &v);
Formula operator||(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 Variable &v1, const Variable &v2);
 
Formula operator==(const Expression &e1, const Expression &e2);
 
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 Expression &e1, const Expression &e2);
 
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 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);
 
std::ostream &operator<<(std::ostream &os, const Formula &f);
 
bool is_false(const Formula &f);
bool is_true(const Formula &f);
bool is_variable(const Formula &f);
bool is_equal_to(const Formula &f);
bool is_not_equal_to(const Formula &f);
bool is_greater_than(const Formula &f);
bool is_greater_than_or_equal_to(const Formula &f);
bool is_less_than(const Formula &f);
bool is_less_than_or_equal_to(const Formula &f);
bool is_relational(const Formula &f);
bool is_conjunction(const Formula &f);
bool is_disjunction(const Formula &f);
bool is_nary(const Formula &f);
bool is_negation(const Formula &f);
bool is_forall(const Formula &f);
 
const Variable &get_variable(const Formula &f);
 
const Expression &get_lhs_expression(const Formula &f);
 
const Expression &get_rhs_expression(const Formula &f);
 
const std::set<Formula> &get_operands(const Formula &f);
 
const Formula &get_operand(const Formula &f);
 
const Variables &get_quantified_variables(const Formula &f);
 
const Formula &get_quantified_formula(const Formula &f);
 
namespace detail {
inline Formula logic_and(const Formula &f1, const Formula &f2) {
  return f1 && f2;
}
}  // namespace detail
}  // namespace symbolic
 
} // namespace dlinear::drake
 
 
namespace std {
/* Provides std::less<dlinear::drake::symbolic::Formula>. */
template<>
struct less<dlinear::drake::symbolic::Formula> {
  bool operator()(const dlinear::drake::symbolic::Formula &lhs,
                  const dlinear::drake::symbolic::Formula &rhs) const {
    return lhs.Less(rhs);
  }
};
 
/* Provides std::equal_to<dlinear::drake::symbolic::Formula>. */
template<>
struct equal_to<dlinear::drake::symbolic::Formula> {
  bool operator()(const dlinear::drake::symbolic::Formula &lhs,
                  const dlinear::drake::symbolic::Formula &rhs) const {
    return lhs.EqualTo(rhs);
  }
};
 
template<>
struct hash<dlinear::drake::symbolic::Formula> {
  size_t operator()(const dlinear::drake::symbolic::Formula &f) const {
    return f.get_hash();
  }
};
 
}  // namespace std