diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute_internals.h | 8 | ||||
-rw-r--r-- | src/expr/datatype.h | 9 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_template.h | 4 | ||||
-rw-r--r-- | src/expr/node.h | 42 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 14 | ||||
-rw-r--r-- | src/expr/record.h | 6 | ||||
-rw-r--r-- | src/expr/symbol_table.cpp | 6 | ||||
-rw-r--r-- | src/expr/symbol_table.h | 6 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 4 | ||||
-rw-r--r-- | src/expr/type_node.h | 22 | ||||
-rw-r--r-- | src/expr/variable_type_map.h | 9 |
13 files changed, 68 insertions, 68 deletions
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 28c618cb0..37c7b6a0b 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -23,7 +23,7 @@ #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#include <ext/hash_map> +#include <unordered_map> namespace CVC4 { namespace expr { @@ -150,7 +150,7 @@ namespace attr { */ template <class value_type> class AttrHash : - public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, + public std::unordered_map<std::pair<uint64_t, NodeValue*>, value_type, AttrHashFunction> { };/* class AttrHash<> */ @@ -161,12 +161,12 @@ class AttrHash : */ template <> class AttrHash<bool> : - protected __gnu_cxx::hash_map<NodeValue*, + protected std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> { /** A "super" type, like in Java, for easy reference below. */ - typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super; + typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super; /** * BitAccessor allows us to return a bit "by reference." Of course, diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 84588fef0..27057ca99 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -20,6 +20,7 @@ #ifndef __CVC4__DATATYPE_H #define __CVC4__DATATYPE_H +#include <functional> #include <iostream> #include <string> #include <vector> @@ -788,16 +789,16 @@ public: */ struct CVC4_PUBLIC DatatypeHashFunction { inline size_t operator()(const Datatype& dt) const { - return StringHashFunction()(dt.getName()); + return std::hash<std::string>()(dt.getName()); } inline size_t operator()(const Datatype* dt) const { - return StringHashFunction()(dt->getName()); + return std::hash<std::string>()(dt->getName()); } inline size_t operator()(const DatatypeConstructor& dtc) const { - return StringHashFunction()(dtc.getName()); + return std::hash<std::string>()(dtc.getName()); } inline size_t operator()(const DatatypeConstructor* dtc) const { - return StringHashFunction()(dtc->getName()); + return std::hash<std::string>()(dtc->getName()); } };/* struct DatatypeHashFunction */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index cee154743..b0611ccbb 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -115,7 +115,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v class ExportPrivate { private: - typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; + typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; ExprManager* from; ExprManager* to; ExprManagerMapCollection& vmap; @@ -393,7 +393,7 @@ static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterat return NodePairIteratorAdaptor<Iterator>(i); } -Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const { +Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const { ExprManagerScope ems(*this); return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 57b4ff93a..d2ad45dee 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -29,8 +29,8 @@ ${includes} #include <stdint.h> #include <iostream> #include <iterator> - #include <string> +#include <unordered_map> #include "base/exception.h" #include "options/language.h" @@ -433,7 +433,7 @@ public: /** * Substitute pairs of (ex,replacement) from the given map. */ - Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const; + Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const; /** * Returns the string representation of the expression. diff --git a/src/expr/node.h b/src/expr/node.h index 69bb98f95..7a8bafe38 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -22,13 +22,16 @@ #ifndef __CVC4__NODE_H #define __CVC4__NODE_H -#include <vector> -#include <string> -#include <iostream> -#include <utility> +#include <stdint.h> + #include <algorithm> #include <functional> -#include <stdint.h> +#include <iostream> +#include <string> +#include <unordered_map> +#include <unordered_set> +#include <utility> +#include <vector> #include "base/configuration.h" #include "base/cvc4_assert.h" @@ -42,7 +45,6 @@ #include "options/language.h" #include "options/set_language.h" #include "util/utility.h" -#include "util/hash.h" namespace CVC4 { @@ -243,7 +245,7 @@ public: * member function with a similar signature. */ Node substitute(TNode node, TNode replacement, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -252,7 +254,7 @@ public: template <class Iterator1, class Iterator2> Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -260,7 +262,7 @@ public: */ template <class Iterator> Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** Default constructor, makes a null expression. */ NodeTemplate() : d_nv(&expr::NodeValue::null()) { } @@ -943,8 +945,6 @@ inline std::ostream& operator<<(std::ostream& out, }/* CVC4 namespace */ -#include <ext/hash_map> - //#include "expr/attribute.h" #include "expr/node_manager.h" #include "expr/type_checker.h" @@ -1296,14 +1296,14 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { if (node == *this) { return replacement; } - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(node, replacement, cache); } template <bool ref_count> Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { Assert(node != *this); if (getNumChildren() == 0) { @@ -1311,7 +1311,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, } // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1351,7 +1351,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache); } @@ -1363,9 +1363,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1410,7 +1410,7 @@ template <class Iterator> inline Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd) const { - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(substitutionsBegin, substitutionsEnd, cache); } @@ -1419,9 +1419,9 @@ template <class Iterator> Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1468,7 +1468,7 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) { template<bool ref_count> bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const { - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; if (!strict && *this == t) { return true; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index f7a1d98d6..e440261cb 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -18,7 +18,6 @@ #include "expr/node_manager.h" #include <algorithm> -#include <ext/hash_set> #include <stack> #include <utility> @@ -36,7 +35,6 @@ using namespace std; using namespace CVC4::expr; -using __gnu_cxx::hash_set; namespace CVC4 { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 44c116558..f112381d8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,7 +30,7 @@ #include <vector> #include <string> -#include <ext/hash_set> +#include <unordered_set> #include "base/tls.h" #include "expr/kind.h" @@ -95,12 +95,12 @@ class NodeManager { bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } }; - typedef __gnu_cxx::hash_set<expr::NodeValue*, - expr::NodeValuePoolHashFunction, - expr::NodeValuePoolEq> NodeValuePool; - typedef __gnu_cxx::hash_set<expr::NodeValue*, - expr::NodeValueIDHashFunction, - expr::NodeValueIDEquality> NodeValueIDSet; + typedef std::unordered_set<expr::NodeValue*, + expr::NodeValuePoolHashFunction, + expr::NodeValuePoolEq> NodeValuePool; + typedef std::unordered_set<expr::NodeValue*, + expr::NodeValueIDHashFunction, + expr::NodeValueIDEquality> NodeValueIDSet; static CVC4_THREADLOCAL(NodeManager*) s_current; diff --git a/src/expr/record.h b/src/expr/record.h index 685756112..7c5854db2 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -19,11 +19,11 @@ #ifndef __CVC4__RECORD_H #define __CVC4__RECORD_H +#include <functional> #include <iostream> #include <string> #include <vector> #include <utility> -#include "util/hash.h" // Forward Declarations namespace CVC4 { @@ -56,13 +56,13 @@ public: struct CVC4_PUBLIC RecordSelectHashFunction { inline size_t operator()(const RecordSelect& t) const { - return StringHashFunction()(t.getField()); + return std::hash<std::string>()(t.getField()); } };/* struct RecordSelectHashFunction */ struct CVC4_PUBLIC RecordUpdateHashFunction { inline size_t operator()(const RecordUpdate& t) const { - return StringHashFunction()(t.getField()); + return std::hash<std::string>()(t.getField()); } };/* struct RecordUpdateHashFunction */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 864ade423..7fd938a9b 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -36,8 +36,8 @@ namespace CVC4 { SymbolTable::SymbolTable() : d_context(new Context()), - d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)), - d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)), + d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)), + d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)), d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) { } @@ -74,7 +74,7 @@ bool SymbolTable::isBound(const std::string& name) const throw() { } bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() { - CDHashMap<std::string, Expr, StringHashFunction>::iterator found = + CDHashMap<std::string, Expr>::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index cefa65d0a..7c3b13003 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -21,7 +21,6 @@ #include <vector> #include <utility> -#include <ext/hash_map> #include "expr/expr.h" #include "util/hash.h" @@ -50,10 +49,11 @@ class CVC4_PUBLIC SymbolTable { context::Context* d_context; /** A map for expressions. */ - context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap; + context::CDHashMap<std::string, Expr>* d_exprMap; /** A map for types. */ - context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >* + d_typeMap; /** A set of defined functions. */ context::CDHashSet<Expr, ExprHashFunction> *d_functions; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 383a31dd0..a4ab2f3b7 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -31,9 +31,9 @@ TypeNode TypeNode::s_null( &expr::NodeValue::null() ); TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const { // in cache? - std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 8dd80bc37..65b422a53 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -22,11 +22,13 @@ #ifndef __CVC4__TYPE_NODE_H #define __CVC4__TYPE_NODE_H -#include <vector> -#include <string> -#include <iostream> #include <stdint.h> +#include <iostream> +#include <string> +#include <unordered_map> +#include <vector> + #include "base/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" @@ -93,7 +95,7 @@ private: * member function with a similar signature. */ TypeNode substitute(const TypeNode& type, const TypeNode& replacement, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -102,7 +104,7 @@ private: template <class Iterator1, class Iterator2> TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const; public: @@ -670,8 +672,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; }/* CVC4 namespace */ -#include <ext/hash_map> - #include "expr/node_manager.h" namespace CVC4 { @@ -687,7 +687,7 @@ inline TypeNode TypeNode::fromType(const Type& t) { inline TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement) const { - std::hash_map<TypeNode, TypeNode, HashFunction> cache; + std::unordered_map<TypeNode, TypeNode, HashFunction> cache; return substitute(type, replacement, cache); } @@ -697,7 +697,7 @@ TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map<TypeNode, TypeNode, HashFunction> cache; + std::unordered_map<TypeNode, TypeNode, HashFunction> cache; return substitute(typesBegin, typesEnd, replacementsBegin, replacementsEnd, cache); } @@ -707,9 +707,9 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const { // in cache? - std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index 739a8d425..94d9c2f67 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -20,8 +20,9 @@ #ifndef __CVC4__VARIABLE_TYPE_MAP_H #define __CVC4__VARIABLE_TYPE_MAP_H +#include <unordered_map> + #include "expr/expr.h" -#include "util/hash.h" namespace CVC4 { @@ -35,13 +36,13 @@ class CVC4_PUBLIC VariableTypeMap { * A map Expr -> Expr, intended to be used for a mapping of variables * between two ExprManagers. */ - std::hash_map<Expr, Expr, ExprHashFunction> d_variables; + std::unordered_map<Expr, Expr, ExprHashFunction> d_variables; /** * A map Type -> Type, intended to be used for a mapping of types * between two ExprManagers. */ - std::hash_map<Type, Type, TypeHashFunction> d_types; + std::unordered_map<Type, Type, TypeHashFunction> d_types; public: Expr& operator[](Expr e) { return d_variables[e]; } @@ -49,7 +50,7 @@ public: };/* class VariableTypeMap */ -typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap; +typedef std::unordered_map<uint64_t, uint64_t> VarMap; struct CVC4_PUBLIC ExprManagerMapCollection { VariableTypeMap d_typeMap; |