diff options
Diffstat (limited to 'src/theory/bv/bv_solver_lazy.h')
| -rw-r--r-- | src/theory/bv/bv_solver_lazy.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 57b3e0a08..9b3a2f1fa 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -49,8 +49,8 @@ class BVSolverLazy : public BVSolver context::Context* d_context; /** Context dependent set of atoms we already propagated */ - context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; - context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; + context::CDHashSet<Node> d_alreadyPropagatedSet; + context::CDHashSet<Node> d_sharedTermsSet; std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories; std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>> @@ -122,11 +122,11 @@ class BVSolverLazy : public BVSolver void check(Theory::Effort e); void spendResource(Resource r); - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<TNode> TNodeSet; + typedef std::unordered_set<Node> NodeSet; NodeSet d_staticLearnCache; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; + typedef std::unordered_map<Node, Node> NodeToNode; context::CDO<bool> d_lemmasAdded; @@ -149,7 +149,7 @@ class BVSolverLazy : public BVSolver * Keeps a map from nodes to the subtheory that propagated it so that we can * explain it properly. */ - typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; + typedef context::CDHashMap<Node, SubTheory> PropagatedMap; PropagatedMap d_propagatedBy; std::unique_ptr<EagerBitblastSolver> d_eagerSolver; |