diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-05-12 23:33:00 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-13 06:33:00 +0000 |
| commit | 31242de4b423d7225174dd1672edb2dacb68f5b8 (patch) | |
| tree | 657a453475affc67628b1391909af92f3346b411 /src/theory/quantifiers/sygus_inst.h | |
| parent | ffd7bb2069df08c31fd9d8a03d786f1e9fc7147c (diff) | |
Add std::hash overloads for Node, TNode and TypeNode. (#6534)
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
Diffstat (limited to 'src/theory/quantifiers/sygus_inst.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_inst.h | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 05c62d883..80c7e809f 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -110,40 +110,35 @@ class SygusInst : public QuantifiersModule bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas); /* Maps quantifiers to a vector of instantiation constants. */ - std::unordered_map<Node, std::vector<Node>, NodeHashFunction> - d_inst_constants; + std::unordered_map<Node, std::vector<Node>> d_inst_constants; /* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */ - std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_var_eval; + std::unordered_map<Node, std::vector<Node>> d_var_eval; /* Maps quantified formulas to registered counterexample literals. */ - std::unordered_map<Node, Node, NodeHashFunction> d_ce_lits; + std::unordered_map<Node, Node> d_ce_lits; /* Decision strategies registered for quantified formulas. */ - std::unordered_map<Node, std::unique_ptr<DecisionStrategy>, NodeHashFunction> - d_dstrat; + std::unordered_map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat; /* Currently active quantifiers. */ - std::unordered_set<Node, NodeHashFunction> d_active_quant; + std::unordered_set<Node> d_active_quant; /* Currently inactive quantifiers. */ - std::unordered_set<Node, NodeHashFunction> d_inactive_quant; + std::unordered_set<Node> d_inactive_quant; /* Registered counterexample lemma cache. */ - std::unordered_map<Node, Node, NodeHashFunction> d_ce_lemmas; + std::unordered_map<Node, Node> d_ce_lemmas; /* Indicates whether a counterexample lemma was added for a quantified * formula in the current context. */ - context::CDHashSet<Node, NodeHashFunction> d_ce_lemma_added; + context::CDHashSet<Node> d_ce_lemma_added; /* Set of global ground terms in assertions (outside of quantifiers). */ - context::CDHashMap<TypeNode, - std::unordered_set<Node, NodeHashFunction>, - TypeNodeHashFunction> - d_global_terms; + context::CDHashMap<TypeNode, std::unordered_set<Node>> d_global_terms; /* Assertions sent by ppNotifyAssertions. */ - context::CDHashSet<Node, NodeHashFunction> d_notified_assertions; + context::CDHashSet<Node> d_notified_assertions; }; } // namespace quantifiers |