cvc4-1.4
abstract_value.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 Integer d_index;
28 
29 public:
30 
32  d_index(index) {
33  CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
34  }
35 
36  ~AbstractValue() throw() {
37  }
38 
39  const Integer& getIndex() const throw() {
40  return d_index;
41  }
42 
43  bool operator==(const AbstractValue& val) const throw() {
44  return d_index == val.d_index;
45  }
46  bool operator!=(const AbstractValue& val) const throw() {
47  return !(*this == val);
48  }
49 
50  bool operator<(const AbstractValue& val) const throw() {
51  return d_index < val.d_index;
52  }
53  bool operator<=(const AbstractValue& val) const throw() {
54  return d_index <= val.d_index;
55  }
56  bool operator>(const AbstractValue& val) const throw() {
57  return !(*this <= val);
58  }
59  bool operator>=(const AbstractValue& val) const throw() {
60  return !(*this < val);
61  }
62 
63 };/* class AbstractValue */
64 
65 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
66 
70 struct CVC4_PUBLIC AbstractValueHashFunction {
71  inline size_t operator()(const AbstractValue& val) const {
72  return IntegerHashFunction()(val.getIndex());
73  }
74 };/* struct AbstractValueHashFunction */
75 
76 }/* CVC4 namespace */
Hash function for the BitVector constants.
bool operator!=(const AbstractValue &val) const
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
bool operator==(const AbstractValue &val) const
const Integer & getIndex() const
bool operator>(const AbstractValue &val) const
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
AbstractValue(Integer index)
bool operator<=(const AbstractValue &val) const
std::ostream & operator<<(std::ostream &out, const SubrangeBound &bound)
bool operator<(const AbstractValue &val) const
bool operator>=(const AbstractValue &val) const
struct CVC4::options::out__option_t out
size_t operator()(const AbstractValue &val) const
Interface for expression types.