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 | |
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')
62 files changed, 287 insertions, 251 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 47f1caf9e..e2d0d2baf 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -15,11 +15,6 @@ ** \todo document this file **/ - - - - - // Pass 1: label the ite as (constant) or (+ constant variable) #include "cvc4_private.h" @@ -27,9 +22,9 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H #define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H +#include <unordered_map> + #include "expr/node.h" -#include <ext/hash_map> -#include <ext/hash_set> #include "context/cdo.h" #include "context/cdtrail_hashmap.h" @@ -46,7 +41,7 @@ class ArithIteUtils { SubstitutionMap* d_subs; TheoryModel* d_model; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; // cache for reduce vars NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n @@ -56,7 +51,7 @@ class ArithIteUtils { NodeMap d_reduceGcd; - typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap; + typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap; NodeIntegerMap d_gcds; Integer d_one; diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 68d4d8f1a..4a9539d49 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -19,7 +19,8 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <vector> #include "context/cdhashset.h" @@ -35,12 +36,12 @@ namespace theory { namespace arith { //Sets of Nodes -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; typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; //Maps from Nodes -> ArithVars, and vice versa -typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap; +typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap; typedef DenseMap<Node> ArithVarToNodeMap; inline Node mkRationalNode(const Rational& q){ diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 9ba4074c1..3427edbd3 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -16,8 +16,9 @@ **/ #include "theory/arith/constraint.h" -#include <ostream> #include <algorithm> +#include <ostream> +#include <unordered_set> #include "base/output.h" #include "proof/proof.h" @@ -1333,7 +1334,7 @@ struct ConstraintCPHash { }; void Constraint::assertionFringe(ConstraintCPVec& v){ - hash_set<ConstraintCP, ConstraintCPHash> visited; + unordered_set<ConstraintCP, ConstraintCPHash> visited; size_t writePos = 0; if(!v.empty()){ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 662327301..25f838567 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -75,7 +75,7 @@ #ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H #define __CVC4__THEORY__ARITH__CONSTRAINT_H -#include <ext/hash_map> +#include <unordered_map> #include <list> #include <set> #include <vector> @@ -145,7 +145,7 @@ enum ConstraintType {LowerBound, Equality, UpperBound, Disequality}; typedef context::CDList<ConstraintCP> CDConstraintList; -typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap; +typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap; typedef size_t ConstraintRuleID; static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max(); diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 77273f609..7d41666e7 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -20,7 +20,7 @@ #pragma once -#include <ext/hash_map> +#include <unordered_map> #include <map> #include <set> #include <vector> @@ -179,7 +179,7 @@ private: int d_upId; public: - typedef __gnu_cxx::hash_map<int, ArithVar> RowIdMap; + typedef std::unordered_map<int, ArithVar> RowIdMap; private: RowIdMap d_rowId2ArithVar; diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index d862dabbd..5b61385f3 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -304,7 +304,7 @@ bool DioSolver::queueEmpty() const{ } Node DioSolver::columnGcdIsOne() const{ - std::hash_map<Node, Integer, NodeHashFunction> gcdMap; + std::unordered_map<Node, Integer, NodeHashFunction> gcdMap; std::deque<TrailIndex>::const_iterator iter, end; for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 2b8b64e75..292f2b856 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -20,6 +20,7 @@ #ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H #define __CVC4__THEORY__ARITH__DIO_SOLVER_H +#include <unordered_map> #include <utility> #include <vector> @@ -68,7 +69,7 @@ private: * We maintain a map from the variables associated with proofs to an input constraint. * These variables can then be used in polynomial manipulations. */ - typedef std::hash_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap; + typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap; NodeToInputConstraintIndexMap d_varToInputConstraintMap; Node proofVariableToReason(const Variable& v) const{ diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h index 471e37fa1..0b91ed074 100644 --- a/src/theory/arith/pseudoboolean_proc.h +++ b/src/theory/arith/pseudoboolean_proc.h @@ -19,7 +19,7 @@ #pragma once -#include <ext/hash_set> +#include <unordered_set> #include <vector> #include "context/cdhashmap.h" @@ -43,7 +43,7 @@ private: CDNode2PairMap d_pbBounds; SubstitutionMap d_subCache; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_learningCache; context::CDO<unsigned> d_pbs; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 13fba2c77..bd983e0bf 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -53,6 +53,8 @@ #pragma once +#include <unordered_map> + #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "theory/arith/error_set.h" @@ -199,7 +201,7 @@ protected: } }; - typedef std::hash_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table; + typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table; static inline int determinizeSgn(int sgn){ return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 5fb31e93f..ab5a19858 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4268,7 +4268,7 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){ // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); - std::hash_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms(); + std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms(); // TODO: // This is not very good for user push/pop.... diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index cc5fddf25..5955fb4e4 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -18,10 +18,9 @@ #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H -#include <ext/hash_set> -#include <ext/hash_map> #include <iostream> #include <map> +#include <unordered_map> #include "context/backtrackable.h" #include "context/cdlist.h" @@ -92,7 +91,7 @@ public: };/* class Info */ -typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap; +typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap; /** * Class keeping track of the following information for canonical diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index 53d935813..4a08838fe 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -23,7 +23,7 @@ #include <utility> #include <vector> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" @@ -33,7 +33,7 @@ namespace arrays { class StaticFactManager { /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> MapType; + typedef std::unordered_map<Node, Node, NodeHashFunction> MapType; /** * Our map of Nodes to their canonical representatives. diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index bde88abab..2f5a9a14f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -551,7 +551,7 @@ void TheoryArrays::weakEquivMakeRepIndex(TNode node) { } void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) { - std::hash_set<TNode, TNodeHashFunction> marked; + std::unordered_set<TNode, TNodeHashFunction> marked; vector<TNode> index_trail; vector<TNode>::iterator it, iend; Node equivalence_trail = reason; @@ -1198,7 +1198,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) /* } else { - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); if (it == d_skolemCache.end()) { rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo"); d_skolemCache[n] = rep; @@ -1240,7 +1240,7 @@ void TheoryArrays::presolve() Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual) { Node skolem; - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); if (it == d_skolemCache.end()) { NodeManager* nm = NodeManager::currentNM(); skolem = nm->mkSkolem(name, type, comment); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 7e8831733..3ef9578ef 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H +#include <unordered_map> + #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdqueue.h" @@ -384,7 +386,7 @@ class TheoryArrays : public Theory { // When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList) // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time. // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time. - typedef std::hash_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap; + typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap; CNodeNListMap d_constReads; context::CDList<TNode> d_reads; context::CDList<TNode> d_constReadsList; @@ -408,7 +410,7 @@ class TheoryArrays : public Theory { };/* class ContextPopper */ ContextPopper d_contextPopper; - std::hash_map<Node, Node, NodeHashFunction> d_skolemCache; + std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache; context::CDO<unsigned> d_skolemIndex; std::vector<Node> d_skolemAssertions; @@ -425,7 +427,7 @@ class TheoryArrays : public Theory { typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap; DefValMap d_defValues; - typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; + typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; ReadBucketMap d_readBucketTable; context::Context* d_readTableContext; context::CDList<Node> d_arrayMerges; diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 4a05f3789..04d199971 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -20,6 +20,9 @@ #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H +#include <unordered_map> +#include <unordered_set> + #include "theory/rewriter.h" #include "theory/type_enumerator.h" @@ -150,9 +153,9 @@ public: // Bad case: have to recompute value counts and/or possibly switch out // default value store = n; - std::hash_set<TNode, TNodeHashFunction> indexSet; - std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap; - std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it; + std::unordered_set<TNode, TNodeHashFunction> indexSet; + std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap; + std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it; unsigned count; unsigned max = 0; TNode maxValue; diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index e896784ef..eb60f339b 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -23,7 +23,7 @@ #include <utility> #include <vector> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" #include "context/cdo.h" @@ -41,7 +41,7 @@ namespace arrays { template <class NodeType, class NodeHash> class UnionFind : context::ContextNotifyObj { /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; + typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType; /** * Our map of Nodes to their canonical representatives. diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 03c811eee..78e01f690 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -19,8 +19,9 @@ #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H -#include <vector> #include <functional> +#include <unordered_map> +#include <vector> #include "theory/theory.h" #include "context/context.h" @@ -64,7 +65,7 @@ public: else return ASSIGNED_TO_TRUE; } - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; private: diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index b5f7e37d4..8373f636b 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -16,6 +16,8 @@ **/ #include <algorithm> +#include <unordered_set> + #include "theory/booleans/theory_bool_rewriter.h" namespace CVC4 { @@ -41,7 +43,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { */ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) { - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; node_set visited; visited.insert(skipNode); 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); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index fd79e3fdc..a0333ed8b 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -19,7 +19,6 @@ #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H -#include <ext/hash_set> #include <iostream> #include <map> diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index e32fa1e71..6d81dbab0 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -1092,7 +1092,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) return true; } - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = d_leavesConstCache.find(e); if (it != d_leavesConstCache.end()) { return (*it).second; @@ -1173,7 +1173,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa Node ITESimplifier::getSimpVar(TypeNode t) { - std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; + std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; it = d_simpVars.find(t); if (it != d_simpVars.end()) { return (*it).second; @@ -1231,7 +1231,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) d_simpContextCache[c] = result; return result; } -typedef std::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){ if(visited.find(x) != visited.end()){ return; diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 29f4f7f1f..4aad9a3f0 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -22,8 +22,7 @@ #ifndef __CVC4__ITE_UTILITIES_H #define __CVC4__ITE_UTILITIES_H -#include <ext/hash_map> -#include <ext/hash_set> +#include <unordered_map> #include <vector> #include "expr/node.h" @@ -80,7 +79,7 @@ public: size_t cache_size() const { return d_cache.size(); } private: - typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap; + typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap; NodeBoolMap d_cache; }; @@ -100,7 +99,7 @@ public: } void clear(); private: - typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; NodeCountMap d_reachCount; bool d_skipVariables; @@ -131,7 +130,7 @@ public: size_t cache_size() const; private: - typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; NodeCountMap d_termITEHeight; }; /* class TermITEHeightCounter */ @@ -158,7 +157,7 @@ private: std::vector<Node>* d_assertions; IncomingArcCounter d_incoming; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_compressed; void reset(); @@ -206,7 +205,7 @@ private: // constant // or termITE(cnd, ConstantIte, ConstantIte) typedef std::vector<Node> NodeVec; - typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; + typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; ConstantLeavesMap d_constantLeaves; // d_constantLeaves satisfies the following invariants: @@ -249,23 +248,23 @@ private: return hash; } };/* struct ITESimplifier::NodePairHashFunction */ - typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap; + typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap; NodePairMap d_constantIteEqualsConstantCache; NodePairMap d_replaceOverCache; NodePairMap d_replaceOverTermIteCache; Node replaceOver(Node n, Node replaceWith, Node simpVar); Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); - std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache; + std::unordered_map<Node, bool, NodeHashFunction> 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::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; Node getSimpVar(TypeNode t); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_simpContextCache; Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); @@ -314,7 +313,7 @@ private: Node d_true; Node d_false; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; class CareSetPtr; class CareSetPtrVal { diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 4c1c93c17..5b714c2d3 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -17,7 +17,6 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H -#include <ext/hash_set> #include <iostream> #include <map> #include <vector> diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8d41c75d8..8597755c9 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -17,13 +17,10 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#include "util/hash.h" -#include "context/cdo.h" - -#include <ext/hash_set> #include <map> #include "context/cdlist.h" +#include "context/cdo.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 40a5b5849..f46b73b1c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -17,13 +17,12 @@ #ifndef __CVC4__THEORY__QUANT_UTIL_H #define __CVC4__THEORY__QUANT_UTIL_H -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" - -#include <ext/hash_set> #include <iostream> #include <map> +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 93390facb..ec5fc633d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -720,7 +720,7 @@ bool TermDb::reset( Theory::Effort effort ){ } } //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed - for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ + for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ Node n = *it; if( !ee->hasTerm( n ) ){ ee->addTerm( n ); @@ -2288,4 +2288,3 @@ Node TermDb::getQAttrQuantIdNumNode( Node q ) { }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f187e5989..4650cc5d4 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -17,12 +17,14 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#include <map> +#include <unordered_set> + #include "expr/attribute.h" #include "theory/theory.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/quant_util.h" -#include <map> namespace CVC4 { namespace theory { @@ -194,9 +196,9 @@ private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; /** terms processed */ - std::hash_set< Node, NodeHashFunction > d_processed; + std::unordered_set< Node, NodeHashFunction > d_processed; /** terms processed */ - std::hash_set< Node, NodeHashFunction > d_iclosure_processed; + std::unordered_set< Node, NodeHashFunction > d_iclosure_processed; /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index d1412500e..9c621dbd6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,25 +19,19 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include <ext/hash_set> -#include <iostream> -#include <map> - #include "context/cdhashmap.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/output_channel.h" #include "theory/theory.h" -#include "util/hash.h" +#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "util/statistics_registry.h" namespace CVC4 { -class TheoryEngine; - namespace theory { - namespace quantifiers { -class ModelEngine; -class InstantiationEngine; - class TheoryQuantifiers : public Theory { private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index faf14e0c7..fa1394f39 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1882,7 +1882,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r_best = r; } //now, make sure that no other member of the class is an instance - std::hash_map<TNode, Node, TNodeHashFunction> cache; + std::unordered_map<TNode, Node, TNodeHashFunction> cache; r_best = getInstance( r_best, eqc, cache ); //store that this representative was chosen at this point if( d_rep_score.find( r_best )==d_rep_score.end() ){ @@ -2001,7 +2001,7 @@ TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNo //helper functions -Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){ +Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){ if(cache.find(n) != cache.end()) { return cache[n]; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 92dfcdae5..7d8f5354b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -17,9 +17,9 @@ #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H -#include <ext/hash_set> #include <iostream> #include <map> +#include <unordered_map> #include "context/cdchunk_list.h" #include "context/cdhashset.h" @@ -449,7 +449,7 @@ private: /** processInferences : will merge equivalence classes in master equality engine, if possible */ bool processInferences( Theory::Effort e ); /** node contains */ - Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); + Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ int getRepScore( Node n, Node f, int index, TypeNode v_tn ); /** flatten representatives */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 27ab7615c..0c20c48a4 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) { } #ifdef CVC4_ASSERTIONS -static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; +static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ class RewriterInitializer { @@ -94,7 +94,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); if(s_rewriteStack == NULL) { - s_rewriteStack = new std::hash_set<Node, NodeHashFunction>(); + s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>(); } #endif diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 34c17a34c..beb5e946c 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -27,9 +27,9 @@ namespace sets { typedef std::map< Node, std::vector< Node > >::iterator MEM_IT; typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT; -typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; +typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; -typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator TC_IT; +typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; void TheorySetsRels::check(Theory::Effort level) { Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl; @@ -240,7 +240,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } Node join_image_rel = join_image_term[0]; - std::hash_set< Node, NodeHashFunction > hasChecked; + std::unordered_set< Node, NodeHashFunction > hasChecked; Node join_image_rel_rep = getRepresentative( join_image_rel ); std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin(); MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep ); @@ -480,14 +480,14 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > if( tc_graph_it != (tc_it->second).end() ) { (tc_graph_it->second).insert( mem_rep_snd ); } else { - std::hash_set< Node, NodeHashFunction > sets; + std::unordered_set< Node, NodeHashFunction > sets; sets.insert( mem_rep_snd ); (tc_it->second)[mem_rep_fst] = sets; } } else { std::map< Node, Node > exp_map; - std::hash_set< Node, NodeHashFunction > sets; - std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map; + std::unordered_set< Node, NodeHashFunction > sets; + std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map; sets.insert( mem_rep_snd ); element_map[mem_rep_fst] = sets; d_tcr_tcGraph[tc_rel] = element_map; @@ -529,7 +529,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) ); if( tc_it != d_rRep_tcGraph.end() ) { bool isReachable = false; - std::hash_set<Node, NodeHashFunction> seen; + std::unordered_set<Node, NodeHashFunction> seen; isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ), getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable ); return isReachable; @@ -537,8 +537,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > return false; } - void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { + void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { if(hasSeen.find(start) == hasSeen.end()) { hasSeen.insert(start); } @@ -550,7 +550,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > isReachable = true; return; } else { - std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); while( set_it != pair_set_it->second.end() ) { // need to check if *set_it has been looked already @@ -565,7 +565,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) { std::map< Node, Node > rel_tc_graph_exps; - std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph; + std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph; Node rel_rep = getRepresentative( tc_rel[0] ); Node tc_rel_rep = getRepresentative( tc_rel ); @@ -576,10 +576,10 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 )); Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 )); Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep ); - std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); + std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); if( rel_tc_graph_it == rel_tc_graph.end() ) { - std::hash_set< Node, NodeHashFunction > snd_elements; + std::unordered_set< Node, NodeHashFunction > snd_elements; snd_elements.insert( snd_element_rep ); rel_tc_graph[fst_element_rep] = snd_elements; rel_tc_graph_exps[tuple_rep] = exps[i]; @@ -596,13 +596,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } } - void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { + void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl; for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) { - for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); + for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) { std::vector< Node > reasons; - std::hash_set<Node, NodeHashFunction> seen; + std::unordered_set<Node, NodeHashFunction> seen; Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) ); Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() ); Node exp = rel_tc_graph_exps.find( tuple )->second; @@ -615,8 +615,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl; } - void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) { + void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) { Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) ); std::vector< Node > all_reasons( reasons ); @@ -646,7 +646,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > seen.insert( cur_node_rep ); TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep ); if( cur_set != tc_graph.end() ) { - for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); + for( std::unordered_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); set_it != cur_set->second.end(); set_it++ ) { Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it ); std::vector< Node > new_reasons( reasons ); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 16770671a..eb97405dc 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -17,11 +17,13 @@ #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" -#include "context/cdhashset.h" +#include <unordered_set> + #include "context/cdchunk_list.h" +#include "context/cdhashset.h" #include "theory/sets/rels_utils.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { @@ -103,12 +105,12 @@ private: std::map< Node, Node > d_pending_facts; - std::hash_set< Node, NodeHashFunction > d_rel_nodes; + std::unordered_set< Node, NodeHashFunction > d_rel_nodes; std::map< Node, std::vector<Node> > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; /** Symbolic tuple variables that has been reduced to concrete ones */ - std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; + std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples; /** Mapping between relation and its member representatives */ std::map< Node, std::vector< Node > > d_rReps_memberReps_cache; @@ -120,8 +122,8 @@ private: std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_rRep_tcGraph; - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tcr_tcGraph; + std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph; + std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; std::map< Node, std::vector< Node > > d_tc_lemmas_last; @@ -154,9 +156,9 @@ private: void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); void buildTCGraphForRel( Node tc_rel ); void doTCInference(); - void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); - void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ); + void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); + void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ); void composeMembersForRels( Node ); void computeMembersForBinOpRel( Node ); @@ -165,8 +167,8 @@ private: void computeMembersForJoinImageTerm( Node ); bool isTCReachable( Node mem_rep, Node tc_rel ); - void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); + void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); void addSharedTerm( TNode n ); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3cce08398..8c3fe67d3 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -25,7 +25,7 @@ namespace theory { namespace sets { typedef std::set<TNode> Elements; -typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; +typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; struct FlattenedNodeTag {}; typedef expr::Attribute<FlattenedNodeTag, bool> flattened; @@ -50,7 +50,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) return RewriteResponse(REWRITE_DONE, n); } - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; node_set visited; visited.insert(skipNode); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 6b78a1698..5ca625751 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -17,6 +17,8 @@ #pragma once +#include <unordered_map> + #include "context/cdhashset.h" #include "expr/node.h" #include "theory/theory.h" @@ -43,7 +45,7 @@ private: IntStat d_statSharedTerms; // Needs to be a map from Nodes as after a backtrack they might not exist - typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; + typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; /** A map from atoms to a list of shared terms */ SharedTermsMap d_atomsToTerms; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a6618175..cca39a62e 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -19,9 +19,10 @@ #ifndef __CVC4__THEORY__SUBSTITUTIONS_H #define __CVC4__THEORY__SUBSTITUTIONS_H +//#include <algorithm> #include <utility> #include <vector> -#include <algorithm> +#include <unordered_map> #include "expr/node.h" #include "context/context.h" @@ -51,7 +52,7 @@ public: private: - typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache; /** The variables, in order of addition */ NodeMap d_substitutions; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 39cce27f9..2a84a7995 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -20,7 +20,7 @@ #include "context/context.h" #include "theory/shared_terms_database.h" -#include <ext/hash_map> +#include <unordered_map> namespace CVC4 { @@ -105,7 +105,7 @@ class SharedTermsVisitor { /** * Cache from preprocessing of atoms. */ - typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; TNodeVisitedMap d_visited; /** diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f010798cd..8509e84ab 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -220,8 +220,8 @@ void Theory::debugPrintFacts() const{ printFacts(DebugChannel.getStream()); } -std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ - std::hash_set<TNode, TNodeHashFunction> currentlyShared; +std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ + std::unordered_set<TNode, TNodeHashFunction> currentlyShared; for (shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i) { currentlyShared.insert (*i); diff --git a/src/theory/theory.h b/src/theory/theory.h index 82607a165..73102a6e2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -19,11 +19,11 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include <ext/hash_set> #include <iosfwd> #include <map> #include <set> #include <string> +#include <unordered_set> #include "context/cdlist.h" #include "context/cdhashset.h" @@ -760,7 +760,7 @@ public: * This is a utility function for constructing a copy of the currently shared terms * in a queriable form. As this is */ - std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const; + std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const; /** * This allows the theory to be queried for whether a literal, lit, is diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7369b7c1f..1023071dc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1645,7 +1645,7 @@ Node TheoryEngine::getExplanation(TNode node) { struct AtomsCollect { std::vector<TNode> d_atoms; - std::hash_set<TNode, TNodeHashFunction> d_visited; + std::unordered_set<TNode, TNodeHashFunction> d_visited; public: diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 82283ef7b..408bff228 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -21,6 +21,7 @@ #include <deque> #include <set> +#include <unordered_map> #include <vector> #include <utility> @@ -189,8 +190,8 @@ class TheoryEngine { theory::TheoryEngineModelBuilder* d_curr_model_builder; bool d_aloc_curr_model_builder; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; /** * Cache for theory-preprocessing of assertions diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index b9a08e3ac..0f92f976e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -132,7 +132,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const { - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { return (*it).second; } diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 126de1e46..c1c57795b 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -17,6 +17,9 @@ #ifndef __CVC4__THEORY__THEORY_MODEL_H #define __CVC4__THEORY__THEORY_MODEL_H +#include <unordered_map> +#include <unordered_set> + #include "smt/model.h" #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" @@ -52,7 +55,7 @@ public: /** true/false nodes */ Node d_true; Node d_false; - mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache; + mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; public: /** comment stream to include in printing */ std::stringstream d_comment_str; @@ -140,8 +143,8 @@ public: */ class TypeSet { public: - typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; - typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; + typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; + typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; typedef TypeSetMap::iterator iterator; typedef TypeSetMap::const_iterator const_iterator; private: @@ -265,9 +268,9 @@ class TheoryEngineModelBuilder : public ModelBuilder protected: /** pointer to theory engine */ TheoryEngine* d_te; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_normalizedCache; - typedef std::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; std::map< Node, Node > d_constantReps; /** process build model */ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7c8e27575..5be32ab90 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -20,8 +20,8 @@ #pragma once #include <deque> -#include <ext/hash_map> #include <queue> +#include <unordered_map> #include <vector> #include "base/output.h" @@ -234,10 +234,10 @@ private: std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; /** Map from nodes to their ids */ - __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; + std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; /** Map from function applications to their ids */ - typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; + typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; /** * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives @@ -611,7 +611,7 @@ private: */ std::vector<TriggerTermSetRef> d_nodeIndividualTrigger; - typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; + typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; /** * A map from pairs of disequal terms, to the reason why we deduced they are disequal. diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index cffa367cf..8a1c30ba6 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -61,7 +61,7 @@ SymmetryBreaker::Template::Template() : } TNode SymmetryBreaker::Template::find(TNode n) { - hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); + unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); if(i == d_reps.end()) { return n; } else { @@ -400,8 +400,8 @@ void SymmetryBreaker::assertFormula(TNode phi) { break; } } - hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); - for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); + for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); i != ps.end(); ++i) { Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; @@ -421,9 +421,9 @@ void SymmetryBreaker::assertFormula(TNode phi) { } if(!d_template.match(phi)) { // we hit a bad match, extract the partitions and reset the template - hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); + unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; - for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); i != ps.end(); ++i) { Debug("ufsymm") << "UFSYMM partition: " << (*i).first; diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index a814c670b..64ca41df2 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -46,6 +46,7 @@ #include <iostream> #include <list> +#include <unordered_map> #include <vector> #include "context/cdlist.h" @@ -64,8 +65,8 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; NodeBuilder<> d_assertions; - std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; - std::hash_map<TNode, TNode, TNodeHashFunction> d_reps; + std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; + std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; TNode find(TNode n); bool matchRecursive(TNode t, TNode n); @@ -73,7 +74,7 @@ class SymmetryBreaker : public context::ContextNotifyObj { public: Template(); bool match(TNode n); - std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } + std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } Node assertions() { switch(d_assertions.getNumChildren()) { case 0: return Node::null(); @@ -91,7 +92,7 @@ public: typedef TNode Term; typedef std::list<Term> Terms; typedef std::set<Term> TermEq; - typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs; + typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs; private: @@ -113,7 +114,7 @@ private: Permutations d_permutations; Terms d_terms; Template d_template; - std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache; + std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache; TermEqs d_termEqs; TermEqs d_termEqsOnly; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 783585f8f..6d4d96a87 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -300,7 +300,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { vector<TNode> workList; workList.push_back(n); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode, TNodeHashFunction> processed; while(!workList.empty()) { n = workList.back(); diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index a32dd076e..04c32f408 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -20,8 +20,10 @@ #ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H #define __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#include <vector> +#include <unordered_map> +#include <unordered_set> #include <utility> +#include <vector> #include "expr/node.h" #include "theory/substitutions.h" @@ -37,9 +39,9 @@ class UnconstrainedSimplifier { /** number of expressions eliminated due to unconstrained simplification */ IntStat d_numUnconstrainedElim; - typedef std::hash_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; - typedef std::hash_map<TNode, TNode, TNodeHashFunction> TNodeMap; - typedef std::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; + typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; TNodeCountMap d_visited; TNodeMap d_visitedOnce; |