cvc4-1.4
uninterpreted_constant.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #pragma once
20 
21 #include "expr/type.h"
22 #include <iostream>
23 
24 namespace CVC4 {
25 
27  const Type d_type;
28  const Integer d_index;
29 
30 public:
31 
33  d_type(type),
34  d_index(index) {
35  CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
36  CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
37  }
38 
40  }
41 
42  Type getType() const throw() {
43  return d_type;
44  }
45  const Integer& getIndex() const throw() {
46  return d_index;
47  }
48 
49  bool operator==(const UninterpretedConstant& uc) const throw() {
50  return d_type == uc.d_type && d_index == uc.d_index;
51  }
52  bool operator!=(const UninterpretedConstant& uc) const throw() {
53  return !(*this == uc);
54  }
55 
56  bool operator<(const UninterpretedConstant& uc) const throw() {
57  return d_type < uc.d_type ||
58  (d_type == uc.d_type && d_index < uc.d_index);
59  }
60  bool operator<=(const UninterpretedConstant& uc) const throw() {
61  return d_type < uc.d_type ||
62  (d_type == uc.d_type && d_index <= uc.d_index);
63  }
64  bool operator>(const UninterpretedConstant& uc) const throw() {
65  return !(*this <= uc);
66  }
67  bool operator>=(const UninterpretedConstant& uc) const throw() {
68  return !(*this < uc);
69  }
70 
71 };/* class UninterpretedConstant */
72 
73 std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC;
74 
79  inline size_t operator()(const UninterpretedConstant& uc) const {
80  return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex());
81  }
82 };/* struct UninterpretedConstantHashFunction */
83 
84 }/* CVC4 namespace */
Hash function for the BitVector constants.
Definition: kind.h:57
Hash function for Types.
Definition: type.h:69
bool operator>(const UninterpretedConstant &uc) const
Class encapsulating CVC4 expression types.
Definition: type.h:89
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
bool operator!=(const UninterpretedConstant &uc) const
UninterpretedConstant(Type type, Integer index)
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator>=(const UninterpretedConstant &uc) const
size_t operator()(const UninterpretedConstant &uc) const
bool operator<=(const UninterpretedConstant &uc) const
struct CVC4::options::out__option_t out
const Integer & getIndex() const
bool operator==(const UninterpretedConstant &uc) const
bool operator<(const UninterpretedConstant &uc) const
Interface for expression types.