summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r--src/theory/theory_model.h13
1 files changed, 8 insertions, 5 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback