summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/array_store_all.h8
-rw-r--r--src/util/ascription_type.h6
-rw-r--r--src/util/bitvector.h28
-rw-r--r--src/util/bool.h6
-rw-r--r--src/util/datatype.h11
-rw-r--r--src/util/hash.h6
-rw-r--r--src/util/integer_cln_imp.h6
-rw-r--r--src/util/integer_gmp_imp.h6
-rw-r--r--src/util/predicate.cpp2
-rw-r--r--src/util/predicate.h8
-rw-r--r--src/util/rational_cln_imp.h6
-rw-r--r--src/util/rational_gmp_imp.h6
-rw-r--r--src/util/subrange_bound.h6
-rw-r--r--src/util/uninterpreted_constant.h8
14 files changed, 46 insertions, 67 deletions
diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index 834eec2c3..277422ecf 100644
--- a/src/util/array_store_all.h
+++ b/src/util/array_store_all.h
@@ -88,12 +88,12 @@ public:
std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
/**
- * Hash function for the BitVector constants.
+ * Hash function for the ArrayStoreAll constants.
*/
-struct CVC4_PUBLIC ArrayStoreAllHashStrategy {
- static inline size_t hash(const ArrayStoreAll& asa) {
+struct CVC4_PUBLIC ArrayStoreAllHashFunction {
+ inline size_t operator()(const ArrayStoreAll& asa) const {
return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
}
-};/* struct ArrayStoreAllHashStrategy */
+};/* struct ArrayStoreAllHashFunction */
}/* CVC4 namespace */
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
index 81289572c..579746332 100644
--- a/src/util/ascription_type.h
+++ b/src/util/ascription_type.h
@@ -48,11 +48,11 @@ public:
/**
* A hash strategy for type ascription operators.
*/
-struct CVC4_PUBLIC AscriptionTypeHashStrategy {
- static inline size_t hash(const AscriptionType& at) {
+struct CVC4_PUBLIC AscriptionTypeHashFunction {
+ inline size_t operator()(const AscriptionType& at) const {
return TypeHashFunction()(at.getType());
}
-};/* struct AscriptionTypeHashStrategy */
+};/* struct AscriptionTypeHashFunction */
/** An output routine for AscriptionTypes */
inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 5d0c301d4..185bb55d9 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -375,11 +375,11 @@ inline BitVector::BitVector(const std::string& num, unsigned base) {
/**
* Hash function for the BitVector constants.
*/
-struct CVC4_PUBLIC BitVectorHashStrategy {
- static inline size_t hash(const BitVector& bv) {
+struct CVC4_PUBLIC BitVectorHashFunction {
+ inline size_t operator()(const BitVector& bv) const {
return bv.hash();
}
-};/* struct BitVectorHashStrategy */
+};/* struct BitVectorHashFunction */
/**
* The structure representing the extraction operation for bit-vectors. The
@@ -403,14 +403,13 @@ struct CVC4_PUBLIC BitVectorExtract {
/**
* Hash function for the BitVectorExtract objects.
*/
-class CVC4_PUBLIC BitVectorExtractHashStrategy {
-public:
- static size_t hash(const BitVectorExtract& extract) {
+struct CVC4_PUBLIC BitVectorExtractHashFunction {
+ size_t operator()(const BitVectorExtract& extract) const {
size_t hash = extract.low;
hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
return hash;
}
-};/* class BitVectorExtractHashStrategy */
+};/* struct BitVectorExtractHashFunction */
/**
@@ -430,12 +429,11 @@ struct CVC4_PUBLIC BitVectorBitOf {
/**
* Hash function for the BitVectorBitOf objects.
*/
-class CVC4_PUBLIC BitVectorBitOfHashStrategy {
-public:
- static size_t hash(const BitVectorBitOf& b) {
+struct CVC4_PUBLIC BitVectorBitOfHashFunction {
+ size_t operator()(const BitVectorBitOf& b) const {
return b.bitIndex;
}
-};/* class BitVectorBitOfHashStrategy */
+};/* struct BitVectorBitOfHashFunction */
@@ -482,11 +480,11 @@ struct CVC4_PUBLIC BitVectorRotateRight {
};/* struct BitVectorRotateRight */
template <typename T>
-struct CVC4_PUBLIC UnsignedHashStrategy {
- static inline size_t hash(const T& x) {
+struct CVC4_PUBLIC UnsignedHashFunction {
+ inline size_t operator()(const T& x) const {
return (size_t)x;
}
-};/* struct UnsignedHashStrategy */
+};/* struct UnsignedHashFunction */
inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
@@ -503,8 +501,6 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
return os << "[" << bv.bitIndex << "]";
}
-
-
}/* CVC4 namespace */
#endif /* __CVC4__BITVECTOR_H */
diff --git a/src/util/bool.h b/src/util/bool.h
index a4d33ca61..9985395e3 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -29,11 +29,11 @@
namespace CVC4 {
-struct BoolHashStrategy {
- static inline size_t hash(bool b) {
+struct BoolHashFunction {
+ inline size_t operator()(bool b) const {
return b;
}
-};/* struct BoolHashStrategy */
+};/* struct BoolHashFunction */
}/* CVC4 namespace */
diff --git a/src/util/datatype.h b/src/util/datatype.h
index b701073c7..c7631ae7b 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -560,17 +560,6 @@ public:
};/* class Datatype */
/**
- * A hash strategy for Datatypes. Needed because Datatypes are used
- * as the constant payload in CONSTANT-kinded TypeNodes (for
- * DATATYPE_TYPE expressions).
- */
-struct CVC4_PUBLIC DatatypeHashStrategy {
- static inline size_t hash(const Datatype& dt) {
- return StringHashFunction()(dt.getName());
- }
-};/* struct DatatypeHashStrategy */
-
-/**
* A hash function for Datatypes. Needed to store them in hash sets
* and hash maps.
*/
diff --git a/src/util/hash.h b/src/util/hash.h
index 6fb20dab0..2420b7acd 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -54,12 +54,6 @@ struct StringHashFunction {
}
};/* struct StringHashFunction */
-struct StringHashStrategy {
- static size_t hash(const std::string& str) {
- return std::hash<const char*>()(str.c_str());
- }
-};/* struct StringHashStrategy */
-
}/* CVC4 namespace */
#endif /* __CVC4__HASH_H */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 43b77df6a..71d6d5b6d 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -460,11 +460,11 @@ public:
friend class CVC4::Rational;
};/* class Integer */
-struct IntegerHashStrategy {
- static inline size_t hash(const CVC4::Integer& i) {
+struct IntegerHashFunction {
+ inline size_t operator()(const CVC4::Integer& i) const {
return i.hash();
}
-};/* struct IntegerHashStrategy */
+};/* struct IntegerHashFunction */
inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
return os << n.toString();
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index dfd6c0599..ea7967023 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -418,11 +418,11 @@ public:
friend class CVC4::Rational;
};/* class Integer */
-struct IntegerHashStrategy {
- static inline size_t hash(const CVC4::Integer& i) {
+struct IntegerHashFunction {
+ inline size_t operator()(const CVC4::Integer& i) const {
return i.hash();
}
-};/* struct IntegerHashStrategy */
+};/* struct IntegerHashFunction */
inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
return os << n.toString();
diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp
index 1868f557d..748e818c3 100644
--- a/src/util/predicate.cpp
+++ b/src/util/predicate.cpp
@@ -49,7 +49,7 @@ operator<<(std::ostream& out, const Predicate& p) {
return out;
}
-size_t PredicateHashStrategy::hash(const Predicate& p) {
+size_t PredicateHashFunction::operator()(const Predicate& p) const {
ExprHashFunction h;
return h(p.d_witness) * 5039 + h(p.d_predicate);
}
diff --git a/src/util/predicate.h b/src/util/predicate.h
index 94a685177..18e0b8b70 100644
--- a/src/util/predicate.h
+++ b/src/util/predicate.h
@@ -31,9 +31,9 @@ class Predicate;
std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
-struct CVC4_PUBLIC PredicateHashStrategy {
- static size_t hash(const Predicate& p);
-};/* class PredicateHashStrategy */
+struct CVC4_PUBLIC PredicateHashFunction {
+ size_t operator()(const Predicate& p) const;
+};/* class PredicateHashFunction */
}/* CVC4 namespace */
@@ -55,7 +55,7 @@ public:
bool operator==(const Predicate& p) const;
friend std::ostream& operator<<(std::ostream& out, const Predicate& p);
- friend size_t PredicateHashStrategy::hash(const Predicate& p);
+ friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
};/* class Predicate */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index ea9f7d055..258060e02 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -314,11 +314,11 @@ public:
};/* class Rational */
-struct RationalHashStrategy {
- static inline size_t hash(const CVC4::Rational& r) {
+struct RationalHashFunction {
+ inline size_t operator()(const CVC4::Rational& r) const {
return r.hash();
}
-};/* struct RationalHashStrategy */
+};/* struct RationalHashFunction */
CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index ed9c57a80..22f1e91b2 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -296,11 +296,11 @@ public:
};/* class Rational */
-struct RationalHashStrategy {
- static inline size_t hash(const CVC4::Rational& r) {
+struct RationalHashFunction {
+ inline size_t operator()(const CVC4::Rational& r) const {
return r.hash();
}
-};/* struct RationalHashStrategy */
+};/* struct RationalHashFunction */
CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 063e59a0f..5de17106d 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -230,15 +230,15 @@ public:
};/* class SubrangeBounds */
-struct CVC4_PUBLIC SubrangeBoundsHashStrategy {
- static inline size_t hash(const SubrangeBounds& bounds) {
+struct CVC4_PUBLIC SubrangeBoundsHashFunction {
+ inline size_t operator()(const SubrangeBounds& bounds) const {
// We use Integer::hash() rather than Integer::getUnsignedLong()
// because the latter might overflow and throw an exception
size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max();
size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max();
return l + 0x9e3779b9 + (u << 6) + (u >> 2);
}
-};/* struct SubrangeBoundsHashStrategy */
+};/* struct SubrangeBoundsHashFunction */
inline std::ostream&
operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h
index 418b8d333..792da178e 100644
--- a/src/util/uninterpreted_constant.h
+++ b/src/util/uninterpreted_constant.h
@@ -77,10 +77,10 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC
/**
* Hash function for the BitVector constants.
*/
-struct CVC4_PUBLIC UninterpretedConstantHashStrategy {
- static inline size_t hash(const UninterpretedConstant& uc) {
- return TypeHashFunction()(uc.getType()) * IntegerHashStrategy::hash(uc.getIndex());
+struct CVC4_PUBLIC UninterpretedConstantHashFunction {
+ inline size_t operator()(const UninterpretedConstant& uc) const {
+ return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex());
}
-};/* struct UninterpretedConstantHashStrategy */
+};/* struct UninterpretedConstantHashFunction */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback