summaryrefslogtreecommitdiff
path: root/src/theory/theory_model_builder.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model_builder.h')
-rw-r--r--src/theory/theory_model_builder.h11
1 files changed, 5 insertions, 6 deletions
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index af3f30fb0..195ba9e0f 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -44,8 +44,8 @@ namespace theory {
*/
class TheoryEngineModelBuilder
{
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_map<Node, Node> NodeMap;
+ typedef std::unordered_set<Node> NodeSet;
public:
TheoryEngineModelBuilder();
@@ -164,10 +164,9 @@ class TheoryEngineModelBuilder
* For example, if tn is (Array Int Bool) and type_list is empty,
* then we append ( Int, Bool, (Array Int Bool) ) to type_list.
*/
- void addToTypeList(
- TypeNode tn,
- std::vector<TypeNode>& type_list,
- std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting);
+ void addToTypeList(TypeNode tn,
+ std::vector<TypeNode>& type_list,
+ std::unordered_set<TypeNode>& visiting);
/** assign function f based on the model m.
* This construction is based on "table form". For example:
* (f 0 1) = 1
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback