diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_inst.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 47 |
1 files changed, 20 insertions, 27 deletions
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 1c6256c24..286d5f42b 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -47,8 +47,8 @@ namespace { */ void getMaxGroundTerms(TNode n, TypeNode tn, - std::unordered_set<Node, NodeHashFunction>& terms, - std::unordered_set<TNode, TNodeHashFunction>& cache, + std::unordered_set<Node>& terms, + std::unordered_set<TNode>& cache, bool skip_quant = false) { if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX @@ -100,12 +100,11 @@ void getMaxGroundTerms(TNode n, * term was already found in a subterm. * @param skip_quant: Do not traverse quantified formulas (skip quantifiers). */ -void getMinGroundTerms( - TNode n, - TypeNode tn, - std::unordered_set<Node, NodeHashFunction>& terms, - std::unordered_map<TNode, std::pair<bool, bool>, TNodeHashFunction>& cache, - bool skip_quant = false) +void getMinGroundTerms(TNode n, + TypeNode tn, + std::unordered_set<Node>& terms, + std::unordered_map<TNode, std::pair<bool, bool>>& cache, + bool skip_quant = false) { if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH) @@ -169,9 +168,8 @@ void getMinGroundTerms( * @param extra_cons: A map of TypeNode to constants, which are added in * addition to the default grammar. */ -void addSpecialValues( - const TypeNode& tn, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons) +void addSpecialValues(const TypeNode& tn, + std::map<TypeNode, std::unordered_set<Node>>& extra_cons) { if (tn.isBitVector()) { @@ -331,19 +329,16 @@ void SygusInst::registerQuantifier(Node q) Trace("sygus-inst") << "Register " << q << std::endl; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons; - std::unordered_set<Node, NodeHashFunction> term_irrelevant; + std::map<TypeNode, std::unordered_set<Node>> extra_cons; + std::map<TypeNode, std::unordered_set<Node>> exclude_cons; + std::map<TypeNode, std::unordered_set<Node>> include_cons; + std::unordered_set<Node> term_irrelevant; /* Collect relevant local ground terms for each variable type. */ if (options::sygusInstScope() == options::SygusInstScope::IN || options::sygusInstScope() == options::SygusInstScope::BOTH) { - std::unordered_map<TypeNode, - std::unordered_set<Node, NodeHashFunction>, - TypeNodeHashFunction> - relevant_terms; + std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms; for (const Node& var : q[0]) { TypeNode tn = var.getType(); @@ -351,10 +346,9 @@ void SygusInst::registerQuantifier(Node q) /* Collect relevant ground terms for type tn. */ if (relevant_terms.find(tn) == relevant_terms.end()) { - std::unordered_set<Node, NodeHashFunction> terms; - std::unordered_set<TNode, TNodeHashFunction> cache_max; - std::unordered_map<TNode, std::pair<bool, bool>, TNodeHashFunction> - cache_min; + std::unordered_set<Node> terms; + std::unordered_set<TNode> cache_max; + std::unordered_map<TNode, std::pair<bool, bool>> cache_min; getMinGroundTerms(q, tn, terms, cache_min); getMaxGroundTerms(q, tn, terms, cache_max); @@ -383,10 +377,9 @@ void SygusInst::registerQuantifier(Node q) /* Collect relevant ground terms for type tn. */ if (d_global_terms.find(tn) == d_global_terms.end()) { - std::unordered_set<Node, NodeHashFunction> terms; - std::unordered_set<TNode, TNodeHashFunction> cache_max; - std::unordered_map<TNode, std::pair<bool, bool>, TNodeHashFunction> - cache_min; + std::unordered_set<Node> terms; + std::unordered_set<TNode> cache_max; + std::unordered_map<TNode, std::pair<bool, bool>> cache_min; for (const Node& a : d_notified_assertions) { |