cvc4-1.4
emptyset.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #pragma once
21 
22 namespace CVC4 {
23  // messy; Expr needs EmptySet (because it's the payload of a
24  // CONSTANT-kinded expression), and EmptySet needs Expr.
25  class CVC4_PUBLIC EmptySet;
26 }/* CVC4 namespace */
27 
28 #include "expr/expr.h"
29 #include "expr/type.h"
30 #include <iostream>
31 
32 namespace CVC4 {
33 
35 
36  const SetType d_type;
37 
38  EmptySet() { }
39 public:
40 
45  EmptySet(SetType setType):d_type(setType) { }
46 
47 
48  ~EmptySet() throw() {
49  }
50 
51  SetType getType() const { return d_type; }
52 
53  bool operator==(const EmptySet& es) const throw() {
54  return d_type == es.d_type;
55  }
56  bool operator!=(const EmptySet& es) const throw() {
57  return !(*this == es);
58  }
59 
60  bool operator<(const EmptySet& es) const throw() {
61  return d_type < es.d_type;
62  }
63  bool operator<=(const EmptySet& es) const throw() {
64  return d_type <= es.d_type;
65  }
66  bool operator>(const EmptySet& es) const throw() {
67  return !(*this <= es);
68  }
69  bool operator>=(const EmptySet& es) const throw() {
70  return !(*this < es);
71  }
72 
73 };/* class EmptySet */
74 
75 std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC;
76 
77 struct CVC4_PUBLIC EmptySetHashFunction {
78  inline size_t operator()(const EmptySet& es) const {
79  return TypeHashFunction()(es.getType());
80  }
81 };/* struct EmptySetHashFunction */
82 
83 }/* CVC4 namespace */
bool operator==(const EmptySet &es) const
Definition: emptyset.h:53
SetType getType() const
Definition: emptyset.h:51
bool operator>=(const EmptySet &es) const
Definition: emptyset.h:69
EmptySet(SetType setType)
Constructs an emptyset of the specified type.
Definition: emptyset.h:45
Class encapsulating an set type.
Definition: type.h:501
Definition: modes.h:25
Hash function for Types.
Definition: type.h:69
bool operator>(const EmptySet &es) const
Definition: emptyset.h:66
bool operator<(const EmptySet &es) const
Definition: emptyset.h:60
size_t operator()(const EmptySet &es) const
Definition: emptyset.h:78
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
bool operator<=(const EmptySet &es) const
Definition: emptyset.h:63
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator!=(const EmptySet &es) const
Definition: emptyset.h:56
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
struct CVC4::options::out__option_t out
expr.h
Interface for expression types.