cvc4-1.4
chain.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__CHAIN_H
21 #define __CVC4__CHAIN_H
22 
23 #include "expr/kind.h"
24 #include <iostream>
25 
26 namespace CVC4 {
27 
30  Kind d_kind;
31 public:
32  explicit Chain(Kind k) : d_kind(k) { }
33  bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; }
34  bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; }
35  Kind getOperator() const { return d_kind; }
36 };/* class Chain */
37 
38 inline std::ostream& operator<<(std::ostream& out, const Chain& ch) CVC4_PUBLIC;
39 inline std::ostream& operator<<(std::ostream& out, const Chain& ch) {
40  return out << ch.getOperator();
41 }
42 
43 struct CVC4_PUBLIC ChainHashFunction {
44  size_t operator()(const Chain& ch) const {
45  return kind::KindHashFunction()(ch.getOperator());
46  }
47 };/* struct ChainHashFunction */
48 
49 }/* CVC4 namespace */
50 
51 #endif /* __CVC4__CHAIN_H */
A class to represent a chained, built-in operator.
Definition: chain.h:29
bool operator==(const Chain &ch) const
Definition: chain.h:33
bool operator!=(const Chain &ch) const
Definition: chain.h:34
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
Macros that should be defined everywhere during the building of the libraries and driver binary...
size_t operator()(const Chain &ch) const
Definition: chain.h:44
Kind getOperator() const
Definition: chain.h:35
kind.h
struct CVC4::options::out__option_t out
Kind_t
Definition: kind.h:60
Chain(Kind k)
Definition: chain.h:32