summaryrefslogtreecommitdiff
path: root/src/expr/node.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-10-02 22:48:00 -0700
committerGitHub <noreply@github.com>2017-10-02 22:48:00 -0700
commitd0faa2b676130119c5d01e00851427fa97f44464 (patch)
tree76e25b4558e6752d75230c7ac297af97f870ea24 /src/expr/node.h
parent6861f66d2e2b54fc31d9151b4dbeb2964ea07f94 (diff)
Unify hash functions for pairs (#1161)
CVC4 was implementing multiple, slightly different hash functions for pairs. With pull request #1157, we have a decent generic hash function for pairs. This commit replaces the existing hash function implementations with a typedef of the generic hash function.
Diffstat (limited to 'src/expr/node.h')
-rw-r--r--src/expr/node.h11
1 files changed, 3 insertions, 8 deletions
diff --git a/src/expr/node.h b/src/expr/node.h
index 9b2ea1935..66f8b0a47 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -44,6 +44,7 @@
#include "expr/expr_iomanip.h"
#include "options/language.h"
#include "options/set_language.h"
+#include "util/hash.h"
#include "util/utility.h"
namespace CVC4 {
@@ -959,14 +960,8 @@ inline size_t TNodeHashFunction::operator()(TNode node) const {
return node.getId();
}
-struct TNodePairHashFunction {
- size_t operator()(const std::pair<CVC4::TNode, CVC4::TNode>& pair ) const {
- TNode n1 = pair.first;
- TNode n2 = pair.second;
-
- return (size_t) (n1.getId() * 0x9e3779b9 + n2.getId());
- }
-};/* struct TNodePairHashFunction */
+using TNodePairHashFunction =
+ PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction>;
template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback