From 3f7f9df5f0c419b7f7dd39e32852161f406a441f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 23 May 2011 21:58:12 +0000
Subject: Merge from arrays2 branch.

---
 src/expr/node.h | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src/expr')

diff --git a/src/expr/node.h b/src/expr/node.h
index 9351293f8..372eec8c0 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -27,6 +27,7 @@
 #include <vector>
 #include <string>
 #include <iostream>
+#include <utility>
 #include <stdint.h>
 
 #include "expr/type.h"
@@ -877,6 +878,15 @@ struct TNodeHashFunction {
   }
 };/* struct TNodeHashFunction */
 
+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 */
+
 template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
   assertTNodeNotExpired();
-- 
cgit v1.2.3