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/preprocessing/util | |
parent | ffd7bb2069df08c31fd9d8a03d786f1e9fc7147c (diff) |
Add std::hash overloads for Node, TNode and TypeNode. (#6534)
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
Diffstat (limited to 'src/preprocessing/util')
-rw-r--r-- | src/preprocessing/util/ite_utilities.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/util/ite_utilities.h | 21 |
2 files changed, 13 insertions, 14 deletions
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 833fa59b9..3e1b3659a 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -1264,7 +1264,7 @@ bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid) return true; } - unordered_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool>::iterator it; it = d_leavesConstCache.find(e); if (it != d_leavesConstCache.end()) { @@ -1358,7 +1358,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, Node ITESimplifier::getSimpVar(TypeNode t) { - std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; + std::unordered_map<TypeNode, Node>::iterator it; it = d_simpVars.find(t); if (it != d_simpVars.end()) { @@ -1424,7 +1424,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) d_simpContextCache[c] = result; return result; } -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node> NodeSet; void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached) { if (visited.find(x) != visited.end()) diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index 95eaf8a84..3ab655767 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -61,7 +61,7 @@ class ContainsTermITEVisitor size_t cache_size() const { return d_cache.size(); } private: - typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap; + typedef std::unordered_map<Node, bool> NodeBoolMap; NodeBoolMap d_cache; }; @@ -121,7 +121,7 @@ class IncomingArcCounter void clear(); private: - typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t> NodeCountMap; NodeCountMap d_reachCount; bool d_skipVariables; @@ -154,7 +154,7 @@ class TermITEHeightCounter size_t cache_size() const; private: - typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t> NodeCountMap; NodeCountMap d_termITEHeight; }; /* class TermITEHeightCounter */ @@ -181,7 +181,7 @@ class ITECompressor AssertionPipeline* d_assertions; IncomingArcCounter d_incoming; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node> NodeMap; NodeMap d_compressed; void reset(); @@ -232,8 +232,7 @@ class ITESimplifier // constant // or termITE(cnd, ConstantIte, ConstantIte) typedef std::vector<Node> NodeVec; - typedef std::unordered_map<Node, NodeVec*, NodeHashFunction> - ConstantLeavesMap; + typedef std::unordered_map<Node, NodeVec*> ConstantLeavesMap; ConstantLeavesMap d_constantLeaves; // d_constantLeaves satisfies the following invariants: @@ -269,7 +268,7 @@ class ITESimplifier typedef std::pair<Node, Node> NodePair; using NodePairHashFunction = - PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>; + PairHashFunction<Node, Node, std::hash<Node>, std::hash<Node>>; typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap; NodePairMap d_constantIteEqualsConstantCache; NodePairMap d_replaceOverCache; @@ -277,16 +276,16 @@ class ITESimplifier Node replaceOver(Node n, Node replaceWith, Node simpVar); Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); - std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache; + std::unordered_map<Node, bool> d_leavesConstCache; bool leavesAreConst(TNode e, theory::TheoryId tid); bool leavesAreConst(TNode e); NodePairMap d_simpConstCache; Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); - std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + std::unordered_map<TypeNode, Node> d_simpVars; Node getSimpVar(TypeNode t); - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node> NodeMap; NodeMap d_simpContextCache; Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); @@ -335,7 +334,7 @@ class ITECareSimplifier Node d_true; Node d_false; - typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<TNode, Node> TNodeMap; class CareSetPtr; class CareSetPtrVal |