src/expr/ascription_type.cpp

   1 /*********************                                                        */
   2 /*! \file ascription_type.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A class representing a type ascription
  13  **/
  14
  15 #include "expr/ascription_type.h"
  16
  17 #include <iostream>
  18
  19 #include "expr/type_node.h"
  20
  21 namespace CVC4 {
  22
  23 AscriptionType::AscriptionType(TypeNode t) : d_type(new TypeNode(t)) {}
  24
  25 AscriptionType::AscriptionType(const AscriptionType& at)
  26     : d_type(new TypeNode(at.getType()))
  27 {
  28 }
  29
  30 AscriptionType& AscriptionType::operator=(const AscriptionType& at)
  31 {
  32   (*d_type) = at.getType();
  33   return *this;
  34 }
  35
  36 AscriptionType::~AscriptionType() {}
  37 TypeNode AscriptionType::getType() const { return *d_type.get(); }
  38 bool AscriptionType::operator==(const AscriptionType& other) const
  39 {
  40   return getType() == other.getType();
  41 }
  42 bool AscriptionType::operator!=(const AscriptionType& other) const
  43 {
  44   return getType() != other.getType();
  45 }
  46
  47 size_t AscriptionTypeHashFunction::operator()(const AscriptionType& at) const
  48 {
  49   return TypeNodeHashFunction()(at.getType());
  50 }
  51
  52 std::ostream& operator<<(std::ostream& out, AscriptionType at)
  53 {
  54   out << at.getType();
  55   return out;
  56 }
  57
  58 }  // namespace CVC4