diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 090398ce8..0abd86130 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -17,11 +17,21 @@ #define __CVC4__NODE_MANAGER_H #include <vector> -#include <map> +#include <ext/hash_set> #include "node.h" #include "kind.h" +namespace __gnu_cxx { +template<> + struct hash<CVC4::NodeValue*> { + size_t operator()(const CVC4::NodeValue* nv) const { + return (size_t)nv->hash(); + } + }; +} /* __gnu_cxx namespace */ + + namespace CVC4 { class NodeManager { @@ -29,16 +39,18 @@ class NodeManager { template <unsigned> friend class CVC4::NodeBuilder; - typedef std::map<uint64_t, std::vector<Node> > hash_t; - hash_t d_hash; + typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet; + NodeValueSet d_nodeValueSet; - Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); } - Node lookup(uint64_t hash, NodeValue* e); - NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e); + NodeValue* poolLookup(NodeValue* nv) const; + void poolInsert(NodeValue* nv); friend class NodeManagerScope; public: + + NodeManager(); + static NodeManager* currentNM() { return s_current; } // general expression-builders |