cvc4-1.4
ascription_type.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #ifndef __CVC4__ASCRIPTION_TYPE_H
20 #define __CVC4__ASCRIPTION_TYPE_H
21 
22 #include "expr/type.h"
23 
24 namespace CVC4 {
25 
34  Type d_type;
35 public:
36  AscriptionType(Type t) throw() : d_type(t) {}
37  Type getType() const throw() { return d_type; }
38  bool operator==(const AscriptionType& other) const throw() {
39  return d_type == other.d_type;
40  }
41  bool operator!=(const AscriptionType& other) const throw() {
42  return d_type != other.d_type;
43  }
44 };/* class AscriptionType */
45 
50  inline size_t operator()(const AscriptionType& at) const {
51  return TypeHashFunction()(at.getType());
52  }
53 };/* struct AscriptionTypeHashFunction */
54 
56 inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
57  out << at.getType();
58  return out;
59 }
60 
61 }/* CVC4 namespace */
62 
63 #endif /* __CVC4__ASCRIPTION_TYPE_H */
A hash function for type ascription operators.
Definition: kind.h:57
Hash function for Types.
Definition: type.h:69
Class encapsulating CVC4 expression types.
Definition: type.h:89
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
size_t operator()(const AscriptionType &at) const
bool operator==(const AscriptionType &other) const
Macros that should be defined everywhere during the building of the libraries and driver binary...
A class used to parameterize a type ascription.
struct CVC4::options::out__option_t out
bool operator!=(const AscriptionType &other) const
Interface for expression types.