diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-23 21:58:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-23 21:58:12 +0000 |
commit | 3f7f9df5f0c419b7f7dd39e32852161f406a441f (patch) | |
tree | 67ae6454e4496f6370cf8236500946e2c7e926b0 /src/expr | |
parent | 91656937b2188f05cdd9b42955c04e6157349285 (diff) |
Merge from arrays2 branch.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node.h | 10 |
1 files changed, 10 insertions, 0 deletions
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(); |