diff options
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 40 |
1 files changed, 15 insertions, 25 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index a61944433..e56774d7e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -159,6 +159,14 @@ namespace kind { }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ +// for hash_maps, hash_sets.. +struct NodeHashFunction { + inline size_t operator()(Node node) const; +};/* struct NodeHashFunction */ +struct TNodeHashFunction { + inline size_t operator()(TNode node) const; +};/* struct TNodeHashFunction */ + /** * Encapsulation of an NodeValue pointer. The reference count is * maintained in the NodeValue if ref_count is true. @@ -166,17 +174,6 @@ namespace kind { */ template <bool ref_count> class NodeTemplate { - - // for hash_maps, hash_sets.. - template <bool ref_count1> - struct HashFunction { - size_t operator()(CVC4::NodeTemplate<ref_count1> node) const { - return (size_t) node.getId(); - } - };/* struct HashFunction */ - - typedef HashFunction<false> TNodeHashFunction; - /** * The NodeValue has access to the private constructors, so that the * iterators can can create new nodes. @@ -233,7 +230,7 @@ class NodeTemplate { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } } - +public: /** * Cache-aware, recursive version of substitute() used by the public * member function with a similar signature. @@ -904,19 +901,12 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) { namespace CVC4 { -// for hash_maps, hash_sets.. -struct NodeHashFunction { - size_t operator()(CVC4::Node node) const { - return (size_t) node.getId(); - } -};/* struct NodeHashFunction */ - -// for hash_maps, hash_sets.. -struct TNodeHashFunction { - size_t operator()(CVC4::TNode node) const { - return (size_t) node.getId(); - } -};/* struct TNodeHashFunction */ +inline size_t NodeHashFunction::operator()(Node node) const { + return node.getId(); +} +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 { |