summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/attribute_internals.h8
-rw-r--r--src/expr/datatype.h9
-rw-r--r--src/expr/expr_template.cpp4
-rw-r--r--src/expr/expr_template.h4
-rw-r--r--src/expr/node.h42
-rw-r--r--src/expr/node_manager.cpp2
-rw-r--r--src/expr/node_manager.h14
-rw-r--r--src/expr/record.h6
-rw-r--r--src/expr/symbol_table.cpp6
-rw-r--r--src/expr/symbol_table.h6
-rw-r--r--src/expr/type_node.cpp4
-rw-r--r--src/expr/type_node.h22
-rw-r--r--src/expr/variable_type_map.h9
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback