Formula.h

#pragma once
 
#include <vector>
 
#include "delpi/libs/gmp.h"
#include "delpi/symbolic/Expression.h"
#include "delpi/symbolic/FormulaKind.h"
#include "delpi/util/concepts.h"
 
namespace delpi {

class Formula {
 public:
  Formula(Expression expression, FormulaKind kind, mpq_class rhs);
  Formula(const Formula& o) = default;
  Formula(Formula&& o) noexcept = default;
  Formula& operator=(const Formula& o) = default;
  Formula& operator=(Formula&& o) noexcept = default;

  [[nodiscard]] Formula Substitute(const Expression::SubstitutionMap& s) const;
  template <MapFromTo<Variable, mpq_class> T>
  [[nodiscard]] bool Evaluate(const T& env) const;

  [[nodiscard]] const Expression& expression() const { return expression_; }
  [[nodiscard]] FormulaKind kind() const { return kind_; }
  [[nodiscard]] const mpq_class& rhs() const { return rhs_; }
  [[nodiscard]] std::vector<Variable> variables() const { return expression_.variables(); }

  [[nodiscard]] bool equal_to(const Formula& o) const noexcept;
  [[nodiscard]] bool less(const Formula& o) const noexcept;
  [[nodiscard]] std::size_t hash() const noexcept;
 
  Formula operator-() const;
  Formula operator!() const;
  std::strong_ordering operator<=>(const Formula&) const;
  bool operator==(const Formula& o) const { return equal_to(o); }
 
  Expression expression_;  
  FormulaKind kind_;       
  mpq_class rhs_;          
};
 
Formula operator==(const Variable& lhs, const Variable& rhs);
Formula operator!=(const Variable& lhs, const Variable& rhs);
Formula operator<(const Variable& lhs, const Variable& rhs);
Formula operator<=(const Variable& lhs, const Variable& rhs);
Formula operator>(const Variable& lhs, const Variable& rhs);
Formula operator>=(const Variable& lhs, const Variable& rhs);
 
Formula operator==(const Expression& lhs, const Expression& rhs);
Formula operator!=(const Expression& lhs, const Expression& rhs);
Formula operator<(const Expression& lhs, const Expression& rhs);
Formula operator<=(const Expression& lhs, const Expression& rhs);
Formula operator>(const Expression& lhs, const Expression& rhs);
Formula operator>=(const Expression& lhs, const Expression& rhs);
 
Formula operator==(mpq_class lhs, const Expression& rhs);
Formula operator!=(mpq_class lhs, const Expression& rhs);
Formula operator<(mpq_class lhs, const Expression& rhs);
Formula operator<=(mpq_class lhs, const Expression& rhs);
Formula operator>(mpq_class lhs, const Expression& rhs);
Formula operator>=(mpq_class lhs, const Expression& rhs);
 
Formula operator==(const Expression& lhs, mpq_class rhs);
Formula operator!=(const Expression& lhs, mpq_class rhs);
Formula operator<(const Expression& lhs, mpq_class rhs);
Formula operator<=(const Expression& lhs, mpq_class rhs);
Formula operator>(const Expression& lhs, mpq_class rhs);
Formula operator>=(const Expression& lhs, mpq_class rhs);
 
std::ostream& operator<<(std::ostream& os, const Formula& formula);
 
}  // namespace delpi
 
#ifdef DELPI_INCLUDE_FMT
 
#include "delpi/util/logging.h"
 
OSTREAM_FORMATTER(delpi::Formula);
 
#endif