diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-05-12 23:33:00 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-13 06:33:00 +0000 |
commit | 31242de4b423d7225174dd1672edb2dacb68f5b8 (patch) | |
tree | 657a453475affc67628b1391909af92f3346b411 /src/theory/bv/abstraction.h | |
parent | ffd7bb2069df08c31fd9d8a03d786f1e9fc7147c (diff) |
Add std::hash overloads for Node, TNode and TypeNode. (#6534)
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
Diffstat (limited to 'src/theory/bv/abstraction.h')
-rw-r--r-- | src/theory/bv/abstraction.h | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 67a04bfea..7eea90cdc 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -32,17 +32,16 @@ namespace bv { typedef std::vector<TNode> ArgsVec; class AbstractionModule { - using NodeVecMap = - std::unordered_map<Node, std::vector<Node>, NodeHashFunction>; - using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>; - using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>; - using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>; - using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>; - using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; + using NodeVecMap = std::unordered_map<Node, std::vector<Node>>; + using NodeTNodeMap = std::unordered_map<Node, TNode>; + using TNodeTNodeMap = std::unordered_map<TNode, TNode>; + using NodeNodeMap = std::unordered_map<Node, Node>; + using TNodeNodeMap = std::unordered_map<Node, TNode>; + using TNodeSet = std::unordered_set<TNode>; using IntNodeMap = std::unordered_map<unsigned, Node>; using IndexMap = std::unordered_map<unsigned, unsigned>; using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >; - using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>; + using SignatureMap = std::unordered_map<TNode, unsigned>; struct Statistics { SizeStat<NodeNodeMap> d_numFunctionsAbstracted; @@ -77,15 +76,15 @@ class AbstractionModule { }; class ArgsTable { - std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; + std::unordered_map<TNode, ArgsTableEntry> d_data; bool hasEntry(TNode signature) const; public: - typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; - ArgsTable() {} - void addEntry(TNode signature, const ArgsVec& args); - ArgsTableEntry& getEntry(TNode signature); - iterator begin() { return d_data.begin(); } - iterator end() { return d_data.end(); } + typedef std::unordered_map<TNode, ArgsTableEntry>::iterator iterator; + ArgsTable() {} + void addEntry(TNode signature, const ArgsVec& args); + ArgsTableEntry& getEntry(TNode signature); + iterator begin() { return d_data.begin(); } + iterator end() { return d_data.end(); } }; /** |