diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f8d3e6509..c20df35d5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -19,6 +19,9 @@ #ifndef __CVC4__THEORY__BV__THEORY_BV_H #define __CVC4__THEORY__BV__THEORY_BV_H +#include <unordered_map> +#include <unordered_set> + #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" @@ -51,7 +54,7 @@ class TheoryBV : public Theory { context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; std::vector<SubtheorySolver*> d_subtheories; - __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; + std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: @@ -129,22 +132,22 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_staticLearnCache; /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. */ - __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero; - __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero; + std::unordered_map<unsigned, Node> d_BVDivByZero; + std::unordered_map<unsigned, Node> d_BVRemByZero; - typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode; + typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; // for ackermanization FunctionToArgs d_funcToArgs; CVC4::theory::SubstitutionMap d_funcToSkolem; |