diff options
author | Tim King <taking@google.com> | 2017-07-20 18:00:11 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-07-20 18:00:11 -0700 |
commit | 26a2fcf1413a02788dc25745fac87eb610b5a55d (patch) | |
tree | 21e7db3d7707a5be944124cb5959656ba9e2ee36 /src/theory/bv/bv_inequality_graph.h | |
parent | 8cf852387cb3a6ec17e77e61956030ca0c4c3837 (diff) | |
parent | 8b0659e6cd342ae40b676781b5e819d5fd2b3af7 (diff) |
Merge branch 'master' into cleanup-regexp
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index f85d8a835..30270b3c3 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Algebraic solver. + ** \brief Algebraic solver. ** ** Algebraic solver. **/ @@ -19,23 +19,25 @@ #ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H #define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H -#include "context/context.h" +#include <list> +#include <queue> +#include <unordered_map> +#include <unordered_set> + #include "context/cdqueue.h" -#include "theory/uf/equality_engine.h" +#include "context/context.h" #include "theory/theory.h" -#include <queue> -#include <list> +#include "theory/uf/equality_engine.h" + namespace CVC4 { namespace theory { - - namespace bv { -typedef unsigned TermId; +typedef unsigned TermId; typedef unsigned ReasonId; extern const TermId UndefinedTermId; extern const ReasonId UndefinedReasonId; -extern const ReasonId AxiomReasonId; +extern const ReasonId AxiomReasonId; class InequalityGraph : public context::ContextNotifyObj{ @@ -100,15 +102,15 @@ class InequalityGraph : public context::ContextNotifyObj{ } }; - typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; - typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; + typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; typedef std::vector<InequalityEdge> Edges; - typedef __gnu_cxx::hash_set<TermId> TermIdSet; + typedef std::unordered_set<TermId> TermIdSet; typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; std::vector<InequalityNode> d_ineqNodes; std::vector< Edges > d_ineqEdges; |