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/bv_inequality_graph.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/bv_inequality_graph.h')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 0fa96e619..32b6dbd7a 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -99,17 +99,18 @@ class InequalityGraph : public context::ContextNotifyObj{ return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; } - }; + }; - typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; - typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap; + typedef std::unordered_map<TNode, TermId> TermNodeToIdMap; typedef std::vector<InequalityEdge> Edges; typedef std::unordered_set<TermId> TermIdSet; - typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> + BFSQueue; + typedef std::unordered_set<TNode> TNodeSet; + typedef std::unordered_set<Node> NodeSet; std::vector<InequalityNode> d_ineqNodes; std::vector< Edges > d_ineqEdges; @@ -206,7 +207,7 @@ class InequalityGraph : public context::ContextNotifyObj{ /*** The currently asserted disequalities */ context::CDQueue<TNode> d_disequalities; - typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; + typedef context::CDHashSet<Node> CDNodeSet; CDNodeSet d_disequalitiesAlreadySplit; Node makeDiseqSplitLemma(TNode diseq); /** Backtracking mechanisms **/ |