Term.h

 
#pragma once
 
#include <iosfwd>
#include <variant>
 
#include "dlinear/parser/smt2/Sort.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
 
namespace dlinear::smt2 {
 
class Term {
 public:
  enum class Type { EXPRESSION, FORMULA };
 
  Term();
  ~Term() = default;
  explicit Term(Expression e);
  explicit Term(Formula f);
  Term(const Term &) = default;
  Term(Term &&) = default;
  Term &operator=(const Term &) = default;
  Term &operator=(const Formula &);
  Term &operator=(const Expression &);
  Term &operator=(Term &&) = default;
  Term &operator=(Formula &&);
  Term &operator=(Expression &&);
 
  [[nodiscard]] Type type() const;
  [[nodiscard]] const Expression &expression() const;
  Expression &m_expression();
  [[nodiscard]] const Formula &formula() const;
  Formula &m_formula();
 
  Term Substitute(const Variable &v, const Term &t);
 
  void Check(Sort s) const;
 
  void Check(Variable::Type t) const;
 
 private:
  std::variant<Expression, Formula> term_;  
};
 
std::ostream &operator<<(std::ostream &os, const Term &t);
 
}  // namespace dlinear::smt2
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::smt2::Term)
 
#endif