diff options
author | Tim King <taking@cs.nyu.edu> | 2017-07-20 17:04:30 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-20 17:04:30 -0700 |
commit | 8b0659e6cd342ae40b676781b5e819d5fd2b3af7 (patch) | |
tree | 5ac55f64d115b3e8865ce8f691f38da65fc82a94 /src/theory/bv | |
parent | 6d82ee2d1f84065ff4a86f688a3b671b85728f80 (diff) |
Moving from the gnu extensions for hash maps to the c++11 hash maps
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.h | 28 | ||||
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 19 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 13 | ||||
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 30 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.h | 20 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 14 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bvintropow2.h | 4 | ||||
-rw-r--r-- | src/theory/bv/slicer.h | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 17 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 15 |
15 files changed, 119 insertions, 90 deletions
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index ed4b8aeb6..0d7e0ff2a 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -19,8 +19,8 @@ #ifndef __CVC4__THEORY__BV__ABSTRACTION_H #define __CVC4__THEORY__BV__ABSTRACTION_H -#include <ext/hash_map> -#include <ext/hash_set> +#include <unordered_map> +#include <unordered_set> #include "expr/node.h" #include "theory/substitutions.h" @@ -64,10 +64,10 @@ class AbstractionModule { }; class ArgsTable { - __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; + std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; bool hasEntry(TNode signature) const; public: - typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; + typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; ArgsTable() {} void addEntry(TNode signature, const ArgsVec& args); ArgsTableEntry& getEntry(TNode signature); @@ -122,16 +122,16 @@ class AbstractionModule { }; - typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; - typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap; - typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; - typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; - typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap; - typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap; - typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap; + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; + typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap; + typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; + typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<unsigned, Node> IntNodeMap; + typedef std::unordered_map<unsigned, unsigned> IndexMap; + typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap; + typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap; ArgsTable d_argsTable; diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index b6b2e2926..565c454e3 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -19,7 +19,8 @@ #ifndef __CVC4__BITBLASTER_TEMPLATE_H #define __CVC4__BITBLASTER_TEMPLATE_H -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <vector> #include "bitblast_strategies_template.h" @@ -58,8 +59,8 @@ namespace bv { class BitblastingRegistrar; -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; class AbstractionModule; @@ -73,9 +74,9 @@ template <class T> class TBitblaster { protected: typedef std::vector<T> Bits; - typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> ModelCache; + typedef std::unordered_map <Node, Bits, NodeHashFunction> TermDefMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*); typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*); @@ -258,7 +259,7 @@ public: class EagerBitblaster : public TBitblaster<Node> { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; // sat solver used for bitblasting and associated CnfStream prop::SatSolver* d_satSolver; BitblastingRegistrar* d_bitblastingRegistrar; @@ -305,8 +306,8 @@ public: }; /* class Registrar */ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { - typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; - typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; + typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; + typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 380d06349..ec6cbad09 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -9,18 +9,21 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Eager bit-blasting solver. + ** \brief Eager bit-blasting solver. ** ** Eager bit-blasting solver. **/ #include "cvc4_private.h" + +#pragma once + +#include <unordered_set> +#include <vector> + #include "expr/node.h" #include "theory/theory_model.h" #include "theory/bv/theory_bv.h" -#include <vector> -#pragma once - namespace CVC4 { namespace theory { @@ -33,7 +36,7 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; + typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; AssertionSet d_assertionSet; /** Bitblasters */ EagerBitblaster* d_bitblaster; 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; diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index dcd3f1062..c5fe63ad6 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -20,7 +20,7 @@ #define __CVC4__BV_QUICK_CHECK_H #include <vector> -#include <ext/hash_map> +#include <unordered_set> #include "context/cdo.h" #include "expr/node.h" @@ -99,7 +99,7 @@ public: uint64_t computeAtomWeight(TNode atom, NodeSet& seen); void collectModelInfo(theory::TheoryModel* model, bool fullModel); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; + typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; vars_iterator beginVars(); vars_iterator endVars(); diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 3730ebc90..4b4103e44 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -14,12 +14,16 @@ ** Algebraic solver. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" +#include <unordered_map> +#include <unordered_set> + #include "theory/bv/bv_subtheory.h" -#include "theory/substitutions.h" #include "theory/bv/slicer.h" +#include "theory/substitutions.h" namespace CVC4 { namespace theory { @@ -60,8 +64,8 @@ class SubstitutionEx { {} }; - typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; - typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; + typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; + typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; Substitutions d_substitutions; SubstitutionsCache d_cache; @@ -104,9 +108,9 @@ struct WorklistElement { }; -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; -typedef __gnu_cxx::hash_map<Node, unsigned, NodeHashFunction> NodeIdMap; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; class ExtractSkolemizer { @@ -123,7 +127,7 @@ class ExtractSkolemizer { ExtractList() : base(1), extracts() {} void addExtract(Extract& e); }; - typedef __gnu_cxx::hash_map<Node, ExtractList, NodeHashFunction> VarExtractMap; + typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap; context::Context d_emptyContext; VarExtractMap d_varToExtract; theory::SubstitutionMap* d_modelMap; diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index c9fb81195..4bbe4327e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -18,6 +18,8 @@ #pragma once +#include <unordered_map> + #include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_subtheory.h" @@ -47,7 +49,7 @@ class BitblastSolver : public SubtheorySolver { context::CDQueue<TNode> d_bitblastQueue; Statistics d_statistics; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_modelCache; context::CDO<bool> d_validModelCache; diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 662f8835e..b416e019d 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -14,12 +14,16 @@ ** Algebraic solver. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" -#include "theory/bv/bv_subtheory.h" +#include <unordered_map> +#include <unordered_set> + #include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -31,9 +35,9 @@ class Base; * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { - typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; - typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue; + typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; struct Statistics { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 37d3723ac..1123d15ae 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -19,10 +19,12 @@ #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H -#include "theory/bv/bv_subtheory.h" -#include "theory/bv/bv_inequality_graph.h" +#include <unordered_set> + #include "context/cdhashset.h" #include "expr/attribute.h" +#include "theory/bv/bv_inequality_graph.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -47,7 +49,7 @@ class InequalitySolver: public SubtheorySolver { InequalityGraph d_inequalityGraph; context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; context::CDO<bool> d_isComplete; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_ineqTerms; bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index a934cf045..93a83626e 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H +#include <unordered_map> + #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" @@ -26,7 +28,7 @@ namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; class BvToBoolPreprocessor { diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h index 935cbb7ed..e335c1339 100644 --- a/src/theory/bv/bvintropow2.h +++ b/src/theory/bv/bvintropow2.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include <vector> -#include <ext/hash_map> +#include <unordered_map> #ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H #define __CVC4__THEORY__BV__BV_INTRO_POW_H @@ -36,7 +36,7 @@ public: static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess); private: - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache); }; diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index b594d5fec..dc8d333c4 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -20,7 +20,7 @@ #include <vector> #include <list> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" #include "theory/bv/theory_bv_utils.h" @@ -79,7 +79,7 @@ public: * UnionFind * */ -typedef __gnu_cxx::hash_set<TermId> TermSet; +typedef std::unordered_set<TermId> TermSet; typedef std::vector<TermId> Decomposition; struct ExtractTerm { @@ -226,9 +226,9 @@ public: }; class Slicer { - __gnu_cxx::hash_map<TermId, TNode> d_idToNode; - __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId; - __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; + std::unordered_map<TermId, TNode> d_idToNode; + std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId; + std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache; UnionFind d_unionFind; ExtractTerm registerTerm(TNode node); public: 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; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 46297cb68..61f072643 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -19,6 +19,9 @@ #pragma once +#include <unordered_map> +#include <unordered_set> + #include "theory/rewriter.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" @@ -922,7 +925,7 @@ struct Count { {} }; -inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { +inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { if(map.find(node) == map.end()) { Count c = neg? Count(0,1) : Count(1, 0); map[node] = c; @@ -945,7 +948,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant = utils::mkBitVectorOnes(size); @@ -974,7 +977,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { if (it->second.pos > 0 && it->second.neg > 0) { @@ -1018,7 +1021,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; std::vector<Node> processingStack; processingStack.push_back(node); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode, TNodeHashFunction> processed; std::vector<Node> children; Kind kind = node.getKind(); @@ -1053,7 +1056,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant(size, (unsigned)0); @@ -1082,7 +1085,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { if (it->second.pos > 0 && it->second.neg > 0) { @@ -1116,7 +1119,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl; - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant; bool const_set = false; @@ -1144,7 +1147,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { std::vector<Node> children; - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); unsigned true_count = 0; bool seen_false = false; for (; it != subterms.end(); ++it) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5bae1af4f..8b8d5e003 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -17,19 +17,22 @@ #include "cvc4_private.h" -#pragma once +#pragma once #include <set> -#include <vector> #include <sstream> +#include <unordered_map> +#include <unordered_set> +#include <vector> + #include "expr/node_manager.h" namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; namespace utils { @@ -505,11 +508,11 @@ inline T gcd(T a, T b) { return a; } -typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; +typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; bool isCoreTerm(TNode term, TNodeBoolMap& cache); bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; uint64_t numNodes(TNode node, NodeSet& seen); |