diff options
Diffstat (limited to 'src/theory/quantifiers')
88 files changed, 399 insertions, 503 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 2bde66fe7..86444b8cf 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -114,12 +114,11 @@ static bool isInvertible(Kind k, unsigned index) || k == BITVECTOR_SHL; } -Node BvInverter::getPathToPv( - Node lit, - Node pv, - Node sv, - std::vector<unsigned>& path, - std::unordered_set<TNode, TNodeHashFunction>& visited) +Node BvInverter::getPathToPv(Node lit, + Node pv, + Node sv, + std::vector<unsigned>& path, + std::unordered_set<TNode>& visited) { if (visited.find(lit) == visited.end()) { @@ -169,7 +168,7 @@ Node BvInverter::getPathToPv(Node lit, std::vector<unsigned>& path, bool projectNl) { - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; Node slit = getPathToPv(lit, pv, sv, path, visited); // if we are able to find a (invertible) path to pv if (!slit.isNull() && !pvs.isNull()) diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index bf6c31b1b..e840b53de 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -104,7 +104,7 @@ class BvInverter Node pv, Node sv, std::vector<unsigned>& path, - std::unordered_set<TNode, TNodeHashFunction>& visited); + std::unordered_set<TNode>& visited); /** Helper function for getInv. * diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index dfc5efff7..789a723b9 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -83,8 +83,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol, bool& rew_print) { // have we added this term before? - std::unordered_map<Node, Node, NodeHashFunction>::iterator itac = - d_add_term_cache.find(sol); + std::unordered_map<Node, Node>::iterator itac = d_add_term_cache.find(sol); if (itac != d_add_term_cache.end()) { return itac->second; diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 1a2add6eb..309aaf4b7 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -124,7 +124,7 @@ class CandidateRewriteDatabase : public ExprMiner /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; /** the cache for results of addTerm */ - std::unordered_map<Node, Node, NodeHashFunction> d_add_term_cache; + std::unordered_map<Node, Node> d_add_term_cache; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index a57b74c78..d5f06b6e9 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -227,8 +227,7 @@ bool CandidateRewriteFilter::notify(Node s, Assert(!s.isNull()); n = d_drewrite->toExternal(n); Assert(!n.isNull()); - std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it = - d_pairs.find(n); + std::map<Node, std::unordered_set<Node> >::iterator it = d_pairs.find(n); if (Trace.isOn("crf-match")) { Trace("crf-match") << " " << s << " matches " << n diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index 7d2d9088c..4995dc7c2 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -115,7 +115,7 @@ class CandidateRewriteFilter * Stores all relevant pairs returned by this sampler (see registerTerm). In * detail, if (t,s) is a relevant pair, then t in d_pairs[s]. */ - std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs; + std::map<Node, std::unordered_set<Node> > d_pairs; /** * For each (builtin) type, a match trie storing all terms in the domain of * d_pairs. diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index c76243a46..ec15b926f 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -270,8 +270,8 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, Node pv, CegInstEffort effort) { - std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::iterator - iti = d_var_to_inst_id.find(pv); + std::unordered_map<Node, std::vector<unsigned>>::iterator iti = + d_var_to_inst_id.find(pv); if (iti == d_var_to_inst_id.end()) { // no bounds @@ -317,7 +317,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, // get the slack value introduced for the asserted literal Node curr_slack_val; - std::unordered_map<Node, Node, NodeHashFunction>::iterator itms = + std::unordered_map<Node, Node>::iterator itms = d_alit_to_model_slack.find(alit); if (itms != d_alit_to_model_slack.end()) { @@ -382,12 +382,12 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, Node lit) { // result of rewriting the visited term - std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited; - visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>()); + std::stack<std::unordered_map<TNode, Node>> visited; + visited.push(std::unordered_map<TNode, Node>()); // whether the visited term contains pv - std::unordered_map<Node, bool, NodeHashFunction> visited_contains_pv; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; - std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs; + std::unordered_map<Node, bool> visited_contains_pv; + std::unordered_map<TNode, Node>::iterator it; + std::unordered_map<TNode, Node> curr_subs; std::stack<std::stack<TNode> > visit; TNode cur; visit.push(std::stack<TNode>()); @@ -400,8 +400,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, if (it == visited.top().end()) { - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc = - curr_subs.find(cur); + std::unordered_map<TNode, Node>::iterator itc = curr_subs.find(cur); if (itc != curr_subs.end()) { visited.top()[cur] = itc->second; @@ -422,7 +421,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, // of this witness expression since we are // now in the context { cur[0][0] -> bv }, // hence we push a context here - visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>()); + visited.push(std::unordered_map<TNode, Node>()); visit.push(std::stack<TNode>()); } visited.top()[cur] = Node::null(); @@ -507,7 +506,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, if (Trace.isOn("cegqi-bv-nl")) { std::vector<TNode> trace_visit; - std::unordered_set<TNode, TNodeHashFunction> trace_visited; + std::unordered_set<TNode> trace_visited; trace_visit.push_back(result); do @@ -535,7 +534,7 @@ Node BvInstantiator::rewriteTermForSolvePv( Node pv, Node n, std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv) + std::unordered_map<Node, bool>& contains_pv) { NodeManager* nm = NodeManager::currentNM(); @@ -648,7 +647,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; // map from terms to bitvector extracts applied to that term std::map<Node, std::vector<Node> > extract_map; - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; Trace("cegqi-bv-pp-debug2") << "Register ce lemma " << lem << std::endl; collectExtracts(lem, extract_map, visited); for (std::pair<const Node, std::vector<Node> >& es : extract_map) @@ -728,8 +727,8 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( void BvInstantiatorPreprocess::collectExtracts( Node lem, - std::map<Node, std::vector<Node> >& extract_map, - std::unordered_set<TNode, TNodeHashFunction>& visited) + std::map<Node, std::vector<Node>>& extract_map, + std::unordered_set<TNode>& visited) { std::vector<TNode> visit; TNode cur; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index a1774de1c..cbc73dc2c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -108,16 +108,15 @@ class BvInstantiator : public Instantiator /** identifier counter, used to allocate ids to each solve form */ unsigned d_inst_id_counter; /** map from variables to list of solved form ids */ - std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction> - d_var_to_inst_id; + std::unordered_map<Node, std::vector<unsigned>> d_var_to_inst_id; /** for each solved form id, the term for instantiation */ std::unordered_map<unsigned, Node> d_inst_id_to_term; /** for each solved form id, the corresponding asserted literal */ std::unordered_map<unsigned, Node> d_inst_id_to_alit; /** map from variable to current id we are processing */ - std::unordered_map<Node, unsigned, NodeHashFunction> d_var_to_curr_inst_id; + std::unordered_map<Node, unsigned> d_var_to_curr_inst_id; /** the amount of slack we added for asserted literals */ - std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack; + std::unordered_map<Node, Node> d_alit_to_model_slack; //--------------------------------end solved forms /** rewrite assertion for solve pv * @@ -137,11 +136,10 @@ class BvInstantiator : public Instantiator * where we guarantee that all subterms of terms in children * appear in the domain of contains_pv. */ - Node rewriteTermForSolvePv( - Node pv, - Node n, - std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv); + Node rewriteTermForSolvePv(Node pv, + Node n, + std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv); /** process literal, called from processAssertion * * lit is the literal to solve for pv that has been rewritten according to @@ -204,8 +202,8 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess * visited is the terms we've already visited. */ void collectExtracts(Node lem, - std::map<Node, std::vector<Node> >& extract_map, - std::unordered_set<TNode, TNodeHashFunction>& visited); + std::map<Node, std::vector<Node>>& extract_map, + std::unordered_set<TNode>& visited); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index 768ae73a6..5040125ba 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -59,10 +59,9 @@ Node getPvCoeff(TNode pv, TNode n) return coeff; } -Node normalizePvMult( - TNode pv, - const std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv) +Node normalizePvMult(TNode pv, + const std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv) { bool neg, neg_coeff = false; bool found_pv = false; @@ -139,10 +138,9 @@ Node normalizePvMult( #ifdef CVC5_ASSERTIONS namespace { -bool isLinearPlus( - TNode n, - TNode pv, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv) +bool isLinearPlus(TNode n, + TNode pv, + std::unordered_map<Node, bool>& contains_pv) { Node coeff; Assert(n.getAttribute(BvLinearAttribute())); @@ -163,10 +161,9 @@ bool isLinearPlus( } // namespace #endif -Node normalizePvPlus( - Node pv, - const std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv) +Node normalizePvPlus(Node pv, + const std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv) { NodeManager* nm; NodeBuilder nb_c(BITVECTOR_PLUS); @@ -252,10 +249,9 @@ Node normalizePvPlus( return result; } -Node normalizePvEqual( - Node pv, - const std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv) +Node normalizePvEqual(Node pv, + const std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv) { Assert(children.size() == 2); diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 15b13433a..6be22805d 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -61,10 +61,9 @@ Node getPvCoeff(TNode pv, TNode n); * a null node otherwise. If pv does not occur in children it returns a * multiplication over children. */ -Node normalizePvMult( - TNode pv, - const std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv); +Node normalizePvMult(TNode pv, + const std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv); /** * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks @@ -81,10 +80,9 @@ Node normalizePvMult( * a null node otherwise. If pv does not occur in children it returns an * addition over children. */ -Node normalizePvPlus( - Node pv, - const std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv); +Node normalizePvPlus(Node pv, + const std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv); /** * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv @@ -97,10 +95,9 @@ Node normalizePvPlus( * * pv * (-a - 1) = c - b. */ -Node normalizePvEqual( - Node pv, - const std::vector<Node>& children, - std::unordered_map<Node, bool, NodeHashFunction>& contains_pv); +Node normalizePvEqual(Node pv, + const std::vector<Node>& children, + std::unordered_map<Node, bool>& contains_pv); } // namespace utils } // namespace quantifiers diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 8a3b22a1f..0d85b8946 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -274,7 +274,7 @@ CegHandledStatus CegInstantiator::isCbqiKind(Kind k) CegHandledStatus CegInstantiator::isCbqiTerm(Node n) { CegHandledStatus ret = CEG_HANDLED; - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -846,7 +846,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, } Trace("cegqi-inst-debug") << "[3] try based on assertions." << std::endl; d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION; - std::unordered_set<Node, NodeHashFunction> lits; + std::unordered_set<Node> lits; for (unsigned r = 0; r < 2; r++) { TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF; @@ -1104,8 +1104,7 @@ bool CegInstantiator::isEligibleForInstantiation(Node n) const bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ Assert(d_prog_var.find(n) != d_prog_var.end()); if( !non_basic.empty() ){ - for (std::unordered_set<Node, NodeHashFunction>::iterator it = - d_prog_var[n].begin(); + for (std::unordered_set<Node>::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it) { @@ -1439,7 +1438,7 @@ Node CegInstantiator::getModelValue( Node n ) { Node CegInstantiator::getBoundVariable(TypeNode tn) { unsigned index = 0; - std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb = + std::unordered_map<TypeNode, unsigned>::iterator itb = d_bound_var_index.find(tn); if (itb != d_bound_var_index.end()) { @@ -1529,9 +1528,9 @@ void CegInstantiator::registerCounterexampleLemma(Node lem, } // register variables that were introduced during TheoryEngine preprocessing - std::unordered_set<Node, NodeHashFunction> ceSyms; + std::unordered_set<Node> ceSyms; expr::getSymbols(lem, ceSyms); - std::unordered_set<Node, NodeHashFunction> qSyms; + std::unordered_set<Node> qSyms; expr::getSymbols(d_quant, qSyms); // all variables that are in counterexample lemma but not in quantified // formula diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 0279a72ca..2c228777d 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -359,14 +359,11 @@ class CegInstantiator { /** cache from nodes to the set of variables it contains * (from the quantified formula we are instantiating). */ - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction> - d_prog_var; + std::unordered_map<Node, std::unordered_set<Node>> d_prog_var; /** cache of the set of terms that we have established are * ineligible for instantiation. */ - std::unordered_set<Node, NodeHashFunction> d_inelig; + std::unordered_set<Node> d_inelig; /** ensures n is in d_prog_var and d_inelig. */ void computeProgVars(Node n); //-------------------------------end globally cached @@ -379,7 +376,7 @@ class CegInstantiator { /** map from types to representatives of that type */ std::map<TypeNode, std::vector<Node> > d_curr_type_eqc; /** solved asserts */ - std::unordered_set<Node, NodeHashFunction> d_solved_asserts; + std::unordered_set<Node> d_solved_asserts; /** process assertions * This is called once at the beginning of check to * set up all necessary information for constructing instantiations, @@ -389,16 +386,14 @@ class CegInstantiator { /** cache bound variables for type returned * by getBoundVariable(...). */ - std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> - d_bound_var; + std::unordered_map<TypeNode, std::vector<Node>> d_bound_var; /** current index of bound variables for type. * The next call to getBoundVariable(...) for * type tn returns the d_bound_var_index[tn]^th * element of d_bound_var[tn], or a fresh variable * if not in bounds. */ - std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction> - d_bound_var_index; + std::unordered_map<TypeNode, unsigned> d_bound_var_index; //-------------------------------end cached per round //-------------------------------data per theory @@ -434,7 +429,7 @@ class CegInstantiator { */ std::vector<Node> d_vars; /** set form of d_vars */ - std::unordered_set<Node, NodeHashFunction> d_vars_set; + std::unordered_set<Node> d_vars_set; /** index of variables reported in instantiation */ std::vector<unsigned> d_var_order_index; /** number of input variables diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 5547409de..882f69b85 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -65,8 +65,8 @@ class InstRewriterCegqi : public InstantiationRewriter */ class InstStrategyCegqi : public QuantifiersModule { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashMap<Node, int> NodeIntMap; public: InstStrategyCegqi(QuantifiersState& qs, diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 6ae5cf546..a20c37043 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -55,8 +55,7 @@ bool NestedQe::hasProcessed(Node q) const return d_qnqe.find(q) != d_qnqe.end(); } -bool NestedQe::getNestedQuantification( - Node q, std::unordered_set<Node, NodeHashFunction>& nqs) +bool NestedQe::getNestedQuantification(Node q, std::unordered_set<Node>& nqs) { expr::getKindSubterms(q[1], kind::FORALL, true, nqs); return !nqs.empty(); @@ -64,7 +63,7 @@ bool NestedQe::getNestedQuantification( bool NestedQe::hasNestedQuantification(Node q) { - std::unordered_set<Node, NodeHashFunction> nqs; + std::unordered_set<Node> nqs; return getNestedQuantification(q, nqs); } @@ -79,7 +78,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) inputExists = true; } Assert(q.getKind() == kind::FORALL); - std::unordered_set<Node, NodeHashFunction> nqs; + std::unordered_set<Node> nqs; if (!getNestedQuantification(q, nqs)) { Trace("cegqi-nested-qe-debug") diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index 020d15d3a..f6e15d4c6 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -30,7 +30,7 @@ namespace quantifiers { class NestedQe { - using NodeNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>; + using NodeNodeMap = context::CDHashMap<Node, Node>; public: NestedQe(context::UserContext* u); @@ -53,8 +53,7 @@ class NestedQe * Get nested quantification. Returns true if q has nested quantifiers. * Adds each nested quantifier in the body of q to nqs. */ - static bool getNestedQuantification( - Node q, std::unordered_set<Node, NodeHashFunction>& nqs); + static bool getNestedQuantification(Node q, std::unordered_set<Node>& nqs); /** * Does quantified formula q have nested quantification? */ diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index e8b5e260a..ef60792a6 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -239,10 +239,10 @@ class ConjectureGenerator : public QuantifiersModule friend class SubsEqcIndex; friend class TermGenerator; friend class TermGenEnv; - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; - typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; -//this class maintains a congruence closure for *universal* facts -private: + typedef context::CDHashMap<Node, Node> NodeMap; + typedef context::CDHashMap<Node, bool> BoolMap; + // this class maintains a congruence closure for *universal* facts + private: //notification class for equality engine class NotifyClass : public eq::EqualityEngineNotify { ConjectureGenerator& d_sg; diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 95fae09e8..73a894081 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -90,10 +90,10 @@ void HigherOrderTrigger::collectHoVarApplyTerms( void HigherOrderTrigger::collectHoVarApplyTerms( Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps) { - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; // whether the visited node is a child of a HO_APPLY chain - std::unordered_map<TNode, bool, TNodeHashFunction> withinApply; + std::unordered_map<TNode, bool> withinApply; std::vector<TNode> visit; TNode cur; for (unsigned i = 0, size = ns.size(); i < size; i++) diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 64f03e7fa..78b2e6c84 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -145,7 +145,7 @@ class HigherOrderTrigger : public Trigger std::map<TNode, std::vector<Node> > d_ho_var_bvs; std::map<TNode, Node> d_ho_var_bvl; /** the set of types of ho variables */ - std::unordered_set<TypeNode, TypeNodeHashFunction> d_ho_var_types; + std::unordered_set<TypeNode> d_ho_var_types; /** add higher-order type predicate lemmas * * Adds lemmas of the form P( f ), where P is the predicate diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 4ff77bdbf..d5af43242 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -472,10 +472,10 @@ int PatternTermSelector::isInstanceOf(Node n1, { Assert(n1 != n2); int status = 0; - std::unordered_set<TNode, TNodeHashFunction> subs_vars; + std::unordered_set<TNode> subs_vars; std::unordered_set< std::pair<TNode, TNode>, - PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction> > + PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>> visited; std::vector<std::pair<TNode, TNode> > visit; std::pair<TNode, TNode> cur; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index c63e2c830..3a78819ea 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -163,8 +163,8 @@ Node Trigger::ensureGroundTermPreprocessed(Valuation& val, std::vector<Node>& gts) { NodeManager* nm = NodeManager::currentNM(); - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 0a6ac6a78..f87ec6435 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -115,7 +115,7 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) return Node::null(); } // now, make sure that no other member of the class is an instance - std::unordered_map<TNode, Node, TNodeHashFunction> cache; + std::unordered_map<TNode, Node> cache; r_best = getInstance(r_best, eqc, cache); // store that this representative was chosen at this point if (d_rep_score.find(r_best) == d_rep_score.end()) @@ -142,10 +142,9 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) //helper functions -Node EqualityQuery::getInstance( - Node n, - const std::vector<Node>& eqc, - std::unordered_map<TNode, Node, TNodeHashFunction>& cache) +Node EqualityQuery::getInstance(Node n, + const std::vector<Node>& eqc, + std::unordered_map<TNode, Node>& cache) { if(cache.find(n) != cache.end()) { return cache[n]; diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 4809cc6c2..f39ff86e3 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -84,7 +84,9 @@ class EqualityQuery : public QuantifiersUtil /** processInferences : will merge equivalence classes in master equality engine, if possible */ bool processInferences( Theory::Effort e ); /** node contains */ - Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ); + Node getInstance(Node n, + const std::vector<Node>& eqc, + std::unordered_map<TNode, Node>& cache); /** get score */ int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn); }; /* EqualityQuery */ diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index a8159bef9..e73323e48 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -783,7 +783,7 @@ Node ExtendedRewriter::extendedRewriteBcp( // the processing terms std::vector<Node> clauses; // the terms we have propagated information to - std::unordered_set<Node, NodeHashFunction> prop_clauses; + std::unordered_set<Node> prop_clauses; // the assignment std::map<Node, Node> assign; std::vector<Node> avars; @@ -1531,8 +1531,8 @@ Node ExtendedRewriter::partialSubstitute(Node n, const std::map<Node, Node>& assign, const std::map<Kind, bool>& rkinds) { - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::map<Node, Node>::const_iterator ita; std::vector<TNode> visit; TNode cur; diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 8e3b9f607..d37e71b72 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -47,9 +47,9 @@ namespace quantifiers { class BoundedIntegers : public QuantifiersModule { - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; - typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + typedef context::CDHashMap<Node, bool> NodeBoolMap; + typedef context::CDHashMap<Node, int> NodeIntMap; + typedef context::CDHashMap<Node, Node> NodeNodeMap; typedef context::CDHashMap<int, bool> IntBoolMap; private: //for determining bounds diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index fd91a94ab..808db7aec 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -42,7 +42,7 @@ struct ModelBasisArgSort { std::vector< Node > d_terms; // number of arguments that are model-basis terms - std::unordered_map<Node, unsigned, NodeHashFunction> d_mba_count; + std::unordered_map<Node, unsigned> d_mba_count; bool operator() (int i,int j) { return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]); } diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index fdaf18e81..e33d1db6d 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -96,7 +96,7 @@ protected: std::map<Node, Node > d_quant_cond; /** A set of quantified formulas that cannot be handled by model-based * quantifier instantiation */ - std::unordered_set<Node, NodeHashFunction> d_unhandledQuant; + std::unordered_set<Node> d_unhandledQuant; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; std::map< Node, std::vector< int > > d_star_insts; diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index a249cf2a8..beb2a33cd 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -55,10 +55,10 @@ Node FunDefEvaluator::evaluate(Node n) const Assert(Rewriter::rewrite(n) == n); Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); - std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount; - std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount; - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, unsigned> funDefCount; + std::unordered_map<TNode, unsigned>::iterator itCount; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::map<Node, FunDefInfo>::const_iterator itf; std::vector<TNode> visit; TNode cur; diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 42bff316a..9b410dd08 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -100,8 +100,8 @@ class InstLemmaList */ class Instantiate : public QuantifiersUtil { - using NodeInstListMap = context:: - CDHashMap<Node, std::shared_ptr<InstLemmaList>, NodeHashFunction>; + using NodeInstListMap = + context::CDHashMap<Node, std::shared_ptr<InstLemmaList>>; public: Instantiate(QuantifiersState& qs, @@ -352,7 +352,7 @@ class Instantiate : public QuantifiersUtil * The list of quantified formulas for which the domain of d_c_inst_match_trie * is valid. */ - context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom; + context::CDHashSet<Node> d_c_inst_match_trie_dom; /** * A CDProof storing instantiation steps. */ diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index b2a807197..fae160aa8 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -50,7 +50,7 @@ Node QuantifiersProofRuleChecker::checkInternal( { return Node::null(); } - std::unordered_map<Node, Node, NodeHashFunction> subs; + std::unordered_map<Node, Node> subs; if (!expr::match(exists[1], p, subs)) { return Node::null(); diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index 1fbf53761..a78f66c51 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -34,8 +34,7 @@ void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; } bool QuantifiersBoundInference::mayComplete(TypeNode tn) { - std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it = - d_may_complete.find(tn); + std::unordered_map<TypeNode, bool>::iterator it = d_may_complete.find(tn); if (it == d_may_complete.end()) { // cache diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h index 0bcb5937a..55e7b0766 100644 --- a/src/theory/quantifiers/quant_bound_inference.h +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -116,7 +116,7 @@ class QuantifiersBoundInference /** Whether finite model finding is enabled */ bool d_isFmf; /** may complete */ - std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete; + std::unordered_map<TypeNode, bool> d_may_complete; /** The bounded integers module, which may help infer bounds */ BoundedIntegers* d_bint; }; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index cff9fde0b..8c4d68631 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2309,7 +2309,7 @@ std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) { bool QuantConflictFind::isPropagatingInstance(Node n) const { - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; std::vector<TNode> visit; TNode cur; visit.push_back(n); diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 5a36452fe..de521cd07 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -193,8 +193,9 @@ class QuantConflictFind : public QuantifiersModule { friend class MatchGen; friend class QuantInfo; - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; -private: + typedef context::CDHashMap<Node, bool> NodeBoolMap; + + private: context::CDO< bool > d_conflict; std::map< Kind, Node > d_zero; //for storing nodes created during t-constraint solving (prevents memory leaks) diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 06b9c59f5..18aeec773 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -47,7 +47,7 @@ namespace quantifiers { * one variable per quantified formula at a time. */ class QuantDSplit : public QuantifiersModule { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: QuantDSplit(QuantifiersState& qs, diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp index 43a404ff9..e53b1ed13 100644 --- a/src/theory/quantifiers/quantifiers_macros.cpp +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -107,8 +107,8 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround) bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround) { - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 3df5aa65f..48106b858 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1061,7 +1061,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, { // compute variables in itm->first, these are not eligible for // elimination - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(m.first, fvs); for (const Node& v : fvs) { @@ -1113,8 +1113,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, } // traverse the body, invalidate variables if they occur in places other than // the bounds they occur in - std::unordered_map<TNode, std::unordered_set<int>, TNodeHashFunction> - evisited; + std::unordered_map<TNode, std::unordered_set<int>> evisited; std::vector<TNode> evisit; std::vector<int> evisit_pol; TNode ecur; @@ -1242,13 +1241,12 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computePrenex( - Node q, - Node body, - std::unordered_set<Node, NodeHashFunction>& args, - std::unordered_set<Node, NodeHashFunction>& nargs, - bool pol, - bool prenexAgg) +Node QuantifiersRewriter::computePrenex(Node q, + Node body, + std::unordered_set<Node>& args, + std::unordered_set<Node>& nargs, + bool pol, + bool prenexAgg) { NodeManager* nm = NodeManager::currentNM(); Kind k = body.getKind(); @@ -1382,8 +1380,8 @@ Node QuantifiersRewriter::computePrenexAgg(Node n, } else { - std::unordered_set<Node, NodeHashFunction> argsSet; - std::unordered_set<Node, NodeHashFunction> nargsSet; + std::unordered_set<Node> argsSet; + std::unordered_set<Node> nargsSet; Node q; Node nn = computePrenex(q, n, argsSet, nargsSet, true, true); Assert(n != nn || argsSet.empty()); @@ -1893,7 +1891,7 @@ Node QuantifiersRewriter::computeOperation(Node f, } else { - std::unordered_set<Node, NodeHashFunction> argsSet, nargsSet; + std::unordered_set<Node> argsSet, nargsSet; n = computePrenex(f, n, argsSet, nargsSet, true, false); Assert(nargsSet.empty()); args.insert(args.end(), argsSet.begin(), argsSet.end()); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index c2f60c7f9..cfc4eca2e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -247,8 +247,8 @@ class QuantifiersRewriter : public TheoryRewriter */ static Node computePrenex(Node q, Node body, - std::unordered_set<Node, NodeHashFunction>& args, - std::unordered_set<Node, NodeHashFunction>& nargs, + std::unordered_set<Node>& args, + std::unordered_set<Node>& nargs, bool pol, bool prenexAgg); /** diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 6955245f7..90b30a016 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -70,7 +70,7 @@ class QueryGenerator : public ExprMiner private: /** cache of all terms registered to this generator */ - std::unordered_set<Node, NodeHashFunction> d_terms; + std::unordered_set<Node> d_terms; /** the threshold used by this module for maximum number of sat points */ unsigned d_deqThresh; /** diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index cc11d884c..05492b5b7 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -285,7 +285,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; // now must check if it has other bound variables - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(cr, fvs); // bound variables must be contained in the single invocation variables for (const Node& bv : fvs) @@ -316,7 +316,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Trace("si-prt") << "...not single invocation." << std::endl; singleInvocation = false; // rename bound variables with maximal overlap with si_vars - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(cr, fvs); std::vector<Node> termsNs; std::vector<Node> subsNs; @@ -349,7 +349,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl; d_conjuncts[2].push_back(cr); - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(cr, fvs); d_all_vars.insert(fvs.begin(), fvs.end()); if (singleInvocation) diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 90b8fb3ea..7f8cfc326 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -202,7 +202,7 @@ class SingleInvocationPartition std::vector<Node> d_si_vars; /** every free variable of conjuncts[2] */ - std::unordered_set<Node, NodeHashFunction> d_all_vars; + std::unordered_set<Node> d_all_vars; /** map from functions to first-order variables that anti-skolemized them */ std::map<Node, Node> d_func_fo_var; /** map from first-order variables to the function it anti-skolemized */ diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 90e780c44..c9234db2c 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -102,7 +102,7 @@ TrustNode Skolemize::process(Node q) bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems) { - std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it = + std::unordered_map<Node, std::vector<Node>>::iterator it = d_skolem_constants.find(q); if (it != d_skolem_constants.end()) { @@ -114,7 +114,7 @@ bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems) Node Skolemize::getSkolemConstant(Node q, unsigned i) { - std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it = + std::unordered_map<Node, std::vector<Node>>::iterator it = d_skolem_constants.find(q); if (it != d_skolem_constants.end()) { @@ -326,8 +326,7 @@ Node Skolemize::mkSkolemizedBody(Node f, Node Skolemize::getSkolemizedBody(Node f) { Assert(f.getKind() == FORALL); - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = - d_skolem_body.find(f); + std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f); if (it == d_skolem_body.end()) { std::vector<TypeNode> fvTypes; @@ -381,8 +380,7 @@ bool Skolemize::isInductionTerm(Node n) void Skolemize::getSkolemTermVectors( std::map<Node, std::vector<Node> >& sks) const { - std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator - itk; + std::unordered_map<Node, std::vector<Node>>::const_iterator itk; for (const auto& p : d_skolemized) { Node q = p.first; diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 412f7a069..2a09913a9 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -65,7 +65,7 @@ class TermRegistry; */ class Skolemize { - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + typedef context::CDHashMap<Node, Node> NodeNodeMap; public: Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm); @@ -146,10 +146,9 @@ class Skolemize /** quantified formulas that have been skolemized */ NodeNodeMap d_skolemized; /** map from quantified formulas to the list of skolem constants */ - std::unordered_map<Node, std::vector<Node>, NodeHashFunction> - d_skolem_constants; + std::unordered_map<Node, std::vector<Node>> d_skolem_constants; /** map from quantified formulas to their skolemized body */ - std::unordered_map<Node, Node, NodeHashFunction> d_skolem_body; + std::unordered_map<Node, Node> d_skolem_body; /** Pointer to the proof node manager */ ProofNodeManager* d_pnm; /** Eager proof generator for skolemization lemmas */ diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 6b1369363..a0cebda8e 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -508,7 +508,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, for (unsigned r = 0; r < 2; r++) { - std::unordered_set<Node, NodeHashFunction>& rlemmas = + std::unordered_set<Node>& rlemmas = r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj; for (const Node& lem : rlemmas) { @@ -585,7 +585,7 @@ bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs, // Maybe we already evaluated some terms in refinement lemmas. // In particular, the example eval cache for f may have some evaluations // cached, which we add to evalVisited and pass to the evaluator below. - std::unordered_map<Node, Node, NodeHashFunction> evalVisited; + std::unordered_map<Node, Node> evalVisited; ExampleInfer* ei = d_parent->getExampleInfer(); for (unsigned i = 0, vsize = vs.size(); i < vsize; i++) { @@ -611,7 +611,7 @@ bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs, Evaluator* eval = d_tds->getEvaluator(); for (unsigned r = 0; r < 2; r++) { - std::unordered_set<Node, NodeHashFunction>& rlemmas = + std::unordered_set<Node>& rlemmas = r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj; for (const Node& lem : rlemmas) { diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index db2c44ca9..b9f593b69 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -107,14 +107,14 @@ class Cegis : public SygusModule /** refinement lemmas */ std::vector<Node> d_refinement_lemmas; /** (processed) conjunctions of refinement lemmas that are not unit */ - std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_conj; + std::unordered_set<Node> d_refinement_lemma_conj; /** (processed) conjunctions of refinement lemmas that are unit */ - std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_unit; + std::unordered_set<Node> d_refinement_lemma_unit; /** substitution entailed by d_refinement_lemma_unit */ std::vector<Node> d_rl_eval_hds; std::vector<Node> d_rl_vals; /** all variables appearing in refinement lemmas */ - std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars; + std::unordered_set<Node> d_refinement_lemma_vars; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index f94bc2ab2..9953c5d05 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -330,7 +330,7 @@ bool CegisCoreConnective::constructSolution( { // check refinement points Node etsrn = d == 0 ? etsr : etsr.negate(); - std::unordered_set<Node, NodeHashFunction> visited; + std::unordered_set<Node> visited; std::vector<Node> pt; Node rid = cfilter.getRefinementPt(this, etsrn, visited, pt); if (!rid.isNull()) @@ -447,7 +447,7 @@ void CegisCoreConnective::Component::addFalseCore(Node id, Node CegisCoreConnective::Component::getRefinementPt( CegisCoreConnective* p, Node n, - std::unordered_set<Node, NodeHashFunction>& visited, + std::unordered_set<Node>& visited, std::vector<Node>& ss) { std::vector<Node> ctx; @@ -608,7 +608,7 @@ void CegisCoreConnective::getModel(SmtEngine& smt, bool CegisCoreConnective::getUnsatCore( SmtEngine& smt, - const std::unordered_set<Node, NodeHashFunction>& queryAsserts, + const std::unordered_set<Node>& queryAsserts, std::vector<Node>& uasserts) const { UnsatCore uc = smt.getUnsatCore(); @@ -656,10 +656,10 @@ Node CegisCoreConnective::evaluate(Node n, } return nm->mkConst(!expRes); } - std::unordered_map<Node, Node, NodeHashFunction>& ec = d_eval_cache[n]; + std::unordered_map<Node, Node>& ec = d_eval_cache[n]; if (!id.isNull()) { - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = ec.find(id); + std::unordered_map<Node, Node>::iterator it = ec.find(id); if (it != ec.end()) { return it->second; @@ -691,7 +691,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, ? d_true : (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts)); std::vector<Node> mvs; - std::unordered_set<Node, NodeHashFunction> visited; + std::unordered_set<Node> visited; bool addSuccess = true; // Ensure that the current conjunction evaluates to false on all refinement // points. We get refinement points until we have exhausted. @@ -759,7 +759,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // "Let U be a subset of D such that S ^ U ^ ~B is unsat." // and uasserts is set to U. std::vector<Node> uasserts; - std::unordered_set<Node, NodeHashFunction> queryAsserts; + std::unordered_set<Node> queryAsserts; queryAsserts.insert(ccheck.getFormula()); queryAsserts.insert(d_sc); bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); @@ -796,7 +796,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // "Let W be a subset of D such that S ^ W is unsat." // and uasserts is set to W. uasserts.clear(); - std::unordered_set<Node, NodeHashFunction> queryAsserts2; + std::unordered_set<Node> queryAsserts2; queryAsserts2.insert(d_sc); getUnsatCore(*checkSc, queryAsserts2, uasserts); falseCore = true; diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index d8f6fb203..baff98de3 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -260,7 +260,7 @@ class CegisCoreConnective : public Cegis */ Node getRefinementPt(CegisCoreConnective* p, Node n, - std::unordered_set<Node, NodeHashFunction>& visited, + std::unordered_set<Node>& visited, std::vector<Node>& ss); /** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */ void getTermPool(std::vector<Node>& passerts) const; @@ -349,10 +349,9 @@ class CegisCoreConnective : public Cegis * If one of the formulas in queryAsserts was in the unsat core, then this * method returns true. Otherwise, this method returns false. */ - bool getUnsatCore( - SmtEngine& smt, - const std::unordered_set<Node, NodeHashFunction>& queryAsserts, - std::vector<Node>& uasserts) const; + bool getUnsatCore(SmtEngine& smt, + const std::unordered_set<Node>& queryAsserts, + std::vector<Node>& uasserts) const; /** * Return the result of checking satisfiability of formula n. * If n was satisfiable, then we store the model for d_vars in mvs. @@ -367,10 +366,7 @@ class CegisCoreConnective : public Cegis */ Node evaluate(Node n, Node id, const std::vector<Node>& mvs); /** A cache of the above function */ - std::unordered_map<Node, - std::unordered_map<Node, Node, NodeHashFunction>, - NodeHashFunction> - d_eval_cache; + std::unordered_map<Node, std::unordered_map<Node, Node>> d_eval_cache; /** The evaluator utility used for the above function */ Evaluator d_eval; //-----------------------------------end for evaluation diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 02d9f3185..3ae34d82c 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -74,12 +74,12 @@ void EnumStreamPermutation::reset(Node value) } // collect variables occurring in value std::vector<Node> vars; - std::unordered_set<Node, NodeHashFunction> visited; + std::unordered_set<Node> visited; collectVars(value, vars, visited); // partition permutation variables d_curr_ind = 0; Trace("synth-stream-concrete") << " ..permutting vars :"; - std::unordered_set<Node, NodeHashFunction> seen_vars; + std::unordered_set<Node> seen_vars; for (const Node& v_cons : vars) { Assert(cons_var.find(v_cons) != cons_var.end()); @@ -231,10 +231,9 @@ unsigned EnumStreamPermutation::getVarClassSize(unsigned id) const return it->second.size(); } -void EnumStreamPermutation::collectVars( - Node n, - std::vector<Node>& vars, - std::unordered_set<Node, NodeHashFunction>& visited) +void EnumStreamPermutation::collectVars(Node n, + std::vector<Node>& vars, + std::unordered_set<Node>& visited) { if (visited.find(n) != visited.end()) { diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 3e849e9a7..ea028991b 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -82,11 +82,11 @@ class EnumStreamPermutation /** value to which we are generating permutations */ Node d_value; /** generated permutations (modulo rewriting) */ - std::unordered_set<Node, NodeHashFunction> d_perm_values; + std::unordered_set<Node> d_perm_values; /** retrieves variables occurring in value */ void collectVars(Node n, std::vector<Node>& vars, - std::unordered_set<Node, NodeHashFunction>& visited); + std::unordered_set<Node>& visited); /** Utility for stepwise application of Heap's algorithm for permutation * * see https://en.wikipedia.org/wiki/Heap%27s_algorithm @@ -229,7 +229,7 @@ class EnumStreamSubstitution */ Node d_last; /** generated combinations */ - std::unordered_set<Node, NodeHashFunction> d_comb_values; + std::unordered_set<Node> d_comb_values; /** permutation utility */ EnumStreamPermutation d_stream_permutations; /** Utility for stepwise generation of ordered subsets of size k from n diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp index 12818685e..d701fe6d9 100644 --- a/src/theory/quantifiers/sygus/example_infer.cpp +++ b/src/theory/quantifiers/sygus/example_infer.cpp @@ -41,8 +41,7 @@ bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates) d_examplesOut[v].clear(); d_examplesTerm[v].clear(); } - std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>> - visited; + std::map<std::pair<bool, bool>, std::unordered_set<Node>> visited; // n is negated conjecture if (!collectExamples(n, visited, true, false)) { @@ -86,8 +85,7 @@ bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates) bool ExampleInfer::collectExamples( Node n, - std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>>& - visited, + std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited, bool hasPol, bool pol) { diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 921e52c3c..d34e32b0e 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -107,8 +107,7 @@ class ExampleInfer */ bool collectExamples( Node n, - std::map<std::pair<bool, bool>, - std::unordered_set<Node, NodeHashFunction>>& visited, + std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited, bool hasPol, bool pol); /** Pointer to the sygus term database */ diff --git a/src/theory/quantifiers/sygus/example_min_eval.cpp b/src/theory/quantifiers/sygus/example_min_eval.cpp index 43740708b..8d303b90c 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.cpp +++ b/src/theory/quantifiers/sygus/example_min_eval.cpp @@ -32,7 +32,7 @@ ExampleMinEval::ExampleMinEval(Node n, d_vars.insert(d_vars.end(), vars.begin(), vars.end()); // compute its free variables - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(n, fvs); for (size_t i = 0, vsize = vars.size(); i < vsize; i++) { diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp index 8a8fcf64b..19725e08b 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp @@ -28,8 +28,7 @@ RConsObligationInfo::RConsObligationInfo(Node builtin) : d_builtins({builtin}) { } -const std::unordered_set<Node, NodeHashFunction>& -RConsObligationInfo::getBuiltins() const +const std::unordered_set<Node>& RConsObligationInfo::getBuiltins() const { return d_builtins; } @@ -44,8 +43,8 @@ void RConsObligationInfo::addBuiltin(Node builtin) d_builtins.emplace(builtin); } -const std::unordered_set<Node, NodeHashFunction>& -RConsObligationInfo::getCandidateSolutions() const +const std::unordered_set<Node>& RConsObligationInfo::getCandidateSolutions() + const { return d_candSols; } @@ -55,8 +54,7 @@ void RConsObligationInfo::addCandidateSolutionToWatchSet(Node candSol) d_watchSet.emplace(candSol); } -const std::unordered_set<Node, NodeHashFunction>& -RConsObligationInfo::getWatchSet() const +const std::unordered_set<Node>& RConsObligationInfo::getWatchSet() const { return d_watchSet; } @@ -66,8 +64,7 @@ std::string RConsObligationInfo::obToString(Node k, { std::stringstream ss; ss << "(["; - std::unordered_set<Node, NodeHashFunction>::const_iterator it = - obInfo.getBuiltins().cbegin(); + std::unordered_set<Node>::const_iterator it = obInfo.getBuiltins().cbegin(); ss << *it; ++it; while (it != obInfo.getBuiltins().cend()) @@ -81,10 +78,9 @@ std::string RConsObligationInfo::obToString(Node k, void RConsObligationInfo::printCandSols( const Node& root, - const std::unordered_map<Node, RConsObligationInfo, NodeHashFunction>& - obInfo) + const std::unordered_map<Node, RConsObligationInfo>& obInfo) { - std::unordered_set<Node, NodeHashFunction> visited; + std::unordered_set<Node> visited; std::vector<Node> stack; stack.push_back(root); @@ -103,7 +99,7 @@ void RConsObligationInfo::printCandSols( for (const Node& j : obInfo.at(k).getCandidateSolutions()) { Trace("sygus-rcons") << datatypes::utils::sygusToBuiltin(j) << " "; - std::unordered_set<TNode, TNodeHashFunction> subObs; + std::unordered_set<TNode> subObs; expr::getVariables(j, subObs); for (const TNode& l : subObs) { diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index f1a48d561..2fd23c5fa 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.h +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -57,7 +57,7 @@ class RConsObligationInfo /** * @return equivalent builtin terms to reconstruct for this class' obligation */ - const std::unordered_set<Node, NodeHashFunction>& getBuiltins() const; + const std::unordered_set<Node>& getBuiltins() const; /** * Add candidate solution to the set of candidate solutions for the @@ -70,8 +70,7 @@ class RConsObligationInfo /** * @return set of candidate solutions for this class' obligation */ - const std::unordered_set<Node, NodeHashFunction>& getCandidateSolutions() - const; + const std::unordered_set<Node>& getCandidateSolutions() const; /** * Add candidate solution to the set of candidate solutions waiting for the @@ -85,7 +84,7 @@ class RConsObligationInfo * @return set of candidate solutions waiting for this class' obligation * to be solved */ - const std::unordered_set<Node, NodeHashFunction>& getWatchSet() const; + const std::unordered_set<Node>& getWatchSet() const; /** * Return a string representation of an obligation. @@ -120,8 +119,7 @@ class RConsObligationInfo */ static void printCandSols( const Node& root, - const std::unordered_map<Node, RConsObligationInfo, NodeHashFunction>& - obInfo); + const std::unordered_map<Node, RConsObligationInfo>& obInfo); private: /** Equivalent builtin terms for this class' obligation. @@ -129,7 +127,7 @@ class RConsObligationInfo * To solve the obligation, one of these builtin terms must be reconstructed * in the specified grammar (sygus datatype type) of the obligation. */ - std::unordered_set<Node, NodeHashFunction> d_builtins; + std::unordered_set<Node> d_builtins; /** A set of candidate solutions to this class' obligation. * * Each candidate solution is a sygus datatype term containing skolem subterms @@ -143,7 +141,7 @@ class RConsObligationInfo * where c_z1 and c_z2 are skolems. Notice that `d_candSols` may contain a * pure term that solves the obligation ((c_+ c_x c_y) in this example). */ - std::unordered_set<Node, NodeHashFunction> d_candSols; + std::unordered_set<Node> d_candSols; /** A set of candidate solutions waiting for this class' obligation to * be solved. * @@ -151,7 +149,7 @@ class RConsObligationInfo * the watch-set of c_z2. Similarly, (c_+ c_z1 c_z2) and (c_+ c_z1 c_y) are in * the watch-set of c_z1. */ - std::unordered_set<Node, NodeHashFunction> d_watchSet; + std::unordered_set<Node> d_watchSet; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index d1d38c3f3..89c6444a5 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -93,7 +93,7 @@ class RConsTypeInfo * possible to have multiple obligations to reconstruct the same builtin term * from different sygus datatype types. */ - std::unordered_map<Node, Node, NodeHashFunction> d_ob; + std::unordered_map<Node, Node> d_ob; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 78cb0dbb1..fc7e7a1b9 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -46,7 +46,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - std::unordered_set<Node, NodeHashFunction> symset; + std::unordered_set<Node> symset; for (size_t i = 0, size = asserts.size(); i < size; i++) { expr::getSymbols(asserts[i], symset); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 83a4276ab..0cf92b373 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -1084,8 +1084,8 @@ Node SygusEnumerator::TermEnumMaster::convertShape( Node n, std::map<TypeNode, int>& vcounter) { NodeManager* nm = NodeManager::currentNM(); - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index c7efae3bb..355108957 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -204,7 +204,7 @@ class SygusEnumerator : public EnumValGenerator /** the list of sygus terms we have enumerated */ std::vector<Node> d_terms; /** the set of builtin terms corresponding to the above list */ - std::unordered_set<Node, NodeHashFunction> d_bterms; + std::unordered_set<Node> d_bterms; /** * The index of first term whose size is greater than or equal to that size, * if it exists. @@ -501,7 +501,7 @@ class SygusEnumerator : public EnumValGenerator * lemma that entails ~is-C( d_enum ) was registered to * TermDbSygus::registerSymBreakLemma. */ - std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons; + std::unordered_set<Node> d_sbExcTlCons; //-------------------------------- end externally specified symmetry breaking }; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index 434118af0..bae6f6327 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -61,7 +61,7 @@ class EnumValGeneratorBasic : public EnumValGenerator /** the current term */ Node d_currTerm; /** cache of (enumerated) builtin values we have enumerated so far */ - std::unordered_set<Node, NodeHashFunction> d_cache; + std::unordered_set<Node> d_cache; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index aff145322..0ef1e7f17 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -76,8 +76,7 @@ void SygusEvalUnfold::registerModelValue(Node a, std::vector<Node>& vals, std::vector<Node>& exps) { - std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator its = - d_subterms.find(a); + std::map<Node, std::unordered_set<Node> >::iterator its = d_subterms.find(a); if (its == d_subterms.end()) { return; diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index c9a0b0ba5..bb181996a 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -132,7 +132,7 @@ class SygusEvalUnfold /** sygus term database associated with this utility */ TermDbSygus* d_tds; /** the set of evaluation terms we have already processed */ - std::unordered_set<Node, NodeHashFunction> d_eval_processed; + std::unordered_set<Node> d_eval_processed; /** map from evaluation heads to evaluation function applications */ std::map<Node, std::vector<Node> > d_evals; /** @@ -150,7 +150,7 @@ class SygusEvalUnfold * This maps anchor terms to the set of shared selector chains with * them as an anchor, for example x may map to { x, x.1, x.2, x.1.1 }. */ - std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_subterms; + std::map<Node, std::unordered_set<Node> > d_subterms; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a532e6cad..263b36abf 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -58,11 +58,10 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q) } void CegGrammarConstructor::collectTerms( - Node n, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& consts) + Node n, std::map<TypeNode, std::unordered_set<Node>>& consts) { - std::unordered_map<TNode, bool, TNodeHashFunction> visited; - std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, bool> visited; + std::unordered_map<TNode, bool>::iterator it; std::stack<TNode> visit; TNode cur; visit.push(n); @@ -100,13 +99,13 @@ Node CegGrammarConstructor::process(Node q, // now, construct the grammar Trace("cegqi") << "SynthConjecture : convert to deep embedding..." << std::endl; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons; + std::map<TypeNode, std::unordered_set<Node>> extra_cons; if( options::sygusAddConstGrammar() ){ Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl; collectTerms( q[1], extra_cons ); } - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exc_cons; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> inc_cons; + std::map<TypeNode, std::unordered_set<Node>> exc_cons; + std::map<TypeNode, std::unordered_set<Node>> inc_cons; NodeManager* nm = NodeManager::currentNM(); @@ -148,7 +147,7 @@ Node CegGrammarConstructor::process(Node q, // check which arguments are irrelevant std::unordered_set<unsigned> arg_irrelevant; d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant); - std::unordered_set<Node, NodeHashFunction> term_irlv; + std::unordered_set<Node> term_irlv; // convert to term for (const unsigned& arg : arg_irrelevant) { @@ -279,8 +278,8 @@ Node CegGrammarConstructor::process(Node q, Node CegGrammarConstructor::convertToEmbedding(Node n) { NodeManager* nm = NodeManager::currentNM(); - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::stack<TNode> visit; TNode cur; visit.push(n); @@ -552,12 +551,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& - exclude_cons, - const 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, + const std::map<TypeNode, std::unordered_set<Node>>& include_cons, + std::unordered_set<Node>& term_irrelevant, std::vector<SygusDatatypeGenerator>& sdts, std::set<TypeNode>& unres) { @@ -601,8 +598,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // create placeholders for collected types std::vector<TypeNode> unres_types; std::map<TypeNode, TypeNode> type_to_unres; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::const_iterator - itc; + std::map<TypeNode, std::unordered_set<Node>>::const_iterator itc; // maps types to the index of its "any term" grammar construction std::map<TypeNode, std::pair<unsigned, bool>> typeToGAnyTerm; options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode(); @@ -726,12 +722,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } else { - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator - itec = extra_cons.find(types[i]); + std::map<TypeNode, std::unordered_set<Node>>::iterator itec = + extra_cons.find(types[i]); if (itec != extra_cons.end()) { - for (std::unordered_set<Node, NodeHashFunction>::iterator set_it = - itec->second.begin(); + for (std::unordered_set<Node>::iterator set_it = itec->second.begin(); set_it != itec->second.end(); ++set_it) { @@ -1493,16 +1488,14 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, - 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) { Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl; - for (std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator - it = extra_cons.begin(); + for (std::map<TypeNode, std::unordered_set<Node>>::iterator it = + extra_cons.begin(); it != extra_cons.end(); ++it) { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 8745f7d61..a743bed2f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -111,12 +111,10 @@ public: TypeNode range, Node bvl, const std::string& fun, - 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); /** * Make the default sygus datatype type corresponding to builtin type range. @@ -125,10 +123,10 @@ public: Node bvl, const std::string& fun) { - 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; return mkSygusDefaultType(range, bvl, fun, @@ -183,9 +181,8 @@ public: /** is the syntax restricted? */ bool d_is_syntax_restricted; /** collect terms */ - void collectTerms( - Node n, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& consts); + void collectTerms(Node n, + std::map<TypeNode, std::unordered_set<Node>>& consts); //---------------- grammar construction /** A class for generating sygus datatypes */ class SygusDatatypeGenerator @@ -211,12 +208,12 @@ public: /** Should we include constructor with operator op? */ bool shouldInclude(Node op) const; /** The constructors that should be excluded. */ - std::unordered_set<Node, NodeHashFunction> d_exclude_cons; + std::unordered_set<Node> d_exclude_cons; /** * If this set is non-empty, then only include variables and constructors * from it. */ - std::unordered_set<Node, NodeHashFunction> d_include_cons; + std::unordered_set<Node> d_include_cons; /** The sygus datatype we are generating. */ SygusDatatype d_sdt; }; @@ -236,13 +233,10 @@ public: TypeNode range, Node bvl, const std::string& fun, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& - extra_cons, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& - exclude_cons, - const 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, + const std::map<TypeNode, std::unordered_set<Node>>& include_cons, + std::unordered_set<Node>& term_irrelevant, std::vector<SygusDatatypeGenerator>& sdts, std::set<TypeNode>& unres); diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 3c8320d8c..426ad07ef 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -38,8 +38,8 @@ void SygusInterpol::collectSymbols(const std::vector<Node>& axioms, const Node& conj) { Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl; - std::unordered_set<Node, NodeHashFunction> symSetAxioms; - std::unordered_set<Node, NodeHashFunction> symSetConj; + std::unordered_set<Node> symSetAxioms; + std::unordered_set<Node> symSetConj; for (size_t i = 0, size = axioms.size(); i < size; i++) { expr::getSymbols(axioms[i], symSetAxioms); @@ -96,7 +96,7 @@ void SygusInterpol::createVariables(bool needsShared) void SygusInterpol::getIncludeCons( const std::vector<Node>& axioms, const Node& conj, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result) + std::map<TypeNode, std::unordered_set<Node>>& result) { NodeManager* nm = NodeManager::currentNM(); Assert(options::produceInterpols() != options::ProduceInterpols::NONE); @@ -116,38 +116,35 @@ void SygusInterpol::getIncludeCons( else if (options::produceInterpols() == options::ProduceInterpols::SHARED) { // Get operators from axioms - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> - include_cons_axioms; + std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms; Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); expr::getOperatorsMap(tmpAssumptions, include_cons_axioms); // Get operators from conj - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> - include_cons_conj; + std::map<TypeNode, std::unordered_set<Node>> include_cons_conj; expr::getOperatorsMap(conj, include_cons_conj); // Compute intersection - for (std::map<TypeNode, - std::unordered_set<Node, NodeHashFunction>>::iterator it = + for (std::map<TypeNode, std::unordered_set<Node>>::iterator it = include_cons_axioms.begin(); it != include_cons_axioms.end(); it++) { TypeNode tn = it->first; - std::unordered_set<Node, NodeHashFunction> axiomsOps = it->second; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator - concIter = include_cons_conj.find(tn); + std::unordered_set<Node> axiomsOps = it->second; + std::map<TypeNode, std::unordered_set<Node>>::iterator concIter = + include_cons_conj.find(tn); if (concIter != include_cons_conj.end()) { - std::unordered_set<Node, NodeHashFunction> conjOps = concIter->second; + std::unordered_set<Node> conjOps = concIter->second; for (const Node& n : axiomsOps) { if (conjOps.find(n) != conjOps.end()) { if (result.find(tn) == result.end()) { - result[tn] = std::unordered_set<Node, NodeHashFunction>(); + result[tn] = std::unordered_set<Node>(); } result[tn].insert(n); } @@ -184,11 +181,11 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, else { // set default grammar - 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::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; getIncludeCons(axioms, conj, include_cons); - std::unordered_set<Node, NodeHashFunction> terms_irrelevant; + std::unordered_set<Node> terms_irrelevant; itpGTypeS = CegGrammarConstructor::mkSygusDefaultType( NodeManager::currentNM()->booleanType(), d_ibvlShared, diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index c96f23e00..07f5ed4ad 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -122,10 +122,9 @@ class SygusInterpol * @param conj input argument * @param result the return value */ - void getIncludeCons( - const std::vector<Node>& axioms, - const Node& conj, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result); + void getIncludeCons(const std::vector<Node>& axioms, + const Node& conj, + std::map<TypeNode, std::unordered_set<Node>>& result); /** * Set up the grammar for the interpol-to-synthesis. @@ -180,7 +179,7 @@ class SygusInterpol /** * unordered set for shared symbols between axioms and conjecture. */ - std::unordered_set<Node, NodeHashFunction> d_symSetShared; + std::unordered_set<Node> d_symSetShared; /** * free variables created from d_syms. */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 966d341c1..78f5c49e6 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -57,7 +57,7 @@ Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TNode tnvn = nvn; - std::unordered_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode> cache; for (const Node& c : d_terms) { Node conj_subs = c.substitute(d_var, tnvn, cache); diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 0fc610580..ca5f057b1 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -138,7 +138,7 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest */ bool d_is_conjunctive; /** cache of n -> the simplified form of eval( n ) */ - std::unordered_map<Node, Node, NodeHashFunction> d_visited; + std::unordered_map<Node, Node> d_visited; }; /** EquivSygusInvarianceTest diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 3f802c954..f5cadc607 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -36,8 +36,7 @@ void SynthConjectureProcessFun::init(Node f) Assert(f.getType().isFunction()); // initialize the arguments - std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction> - type_to_init_deq_id; + std::unordered_map<TypeNode, unsigned> type_to_init_deq_id; std::vector<TypeNode> argTypes = f.getType().getArgTypes(); for (unsigned j = 0; j < argTypes.size(); j++) { @@ -77,8 +76,7 @@ bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) { if (n.isVar()) { - std::unordered_map<Node, unsigned, NodeHashFunction>::iterator ita = - d_arg_var_num.find(n); + std::unordered_map<Node, unsigned>::iterator ita = d_arg_var_num.find(n); if (ita != d_arg_var_num.end()) { arg_index = ita->second; @@ -90,13 +88,11 @@ bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) Node SynthConjectureProcessFun::inferDefinition( Node n, - std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry, - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>& free_vars) + std::unordered_map<Node, unsigned>& term_to_arg_carry, + std::unordered_map<Node, std::unordered_set<Node>>& free_vars) { - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::stack<TNode> visit; TNode cur; visit.push(n); @@ -115,7 +111,7 @@ Node SynthConjectureProcessFun::inferDefinition( else { // if it is term used by another argument, use it - std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt = + std::unordered_map<Node, unsigned>::iterator itt = term_to_arg_carry.find(cur); if (itt != term_to_arg_carry.end()) { @@ -185,7 +181,7 @@ unsigned SynthConjectureProcessFun::assignRelevantDef( } unsigned rid = args[id]; // for merging previously equivalent definitions - std::unordered_map<Node, unsigned, NodeHashFunction> prev_defs; + std::unordered_map<Node, unsigned> prev_defs; for (unsigned j = 0; j < args.size(); j++) { unsigned i = args[j]; @@ -199,8 +195,7 @@ unsigned SynthConjectureProcessFun::assignRelevantDef( else { Node t = d_arg_props[i].d_template; - std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt = - prev_defs.find(t); + std::unordered_map<Node, unsigned>::iterator itt = prev_defs.find(t); if (itt != prev_defs.end()) { // merge previously equivalent definitions @@ -254,10 +249,8 @@ void SynthConjectureProcessFun::processTerms( std::vector<Node>& ns, std::vector<Node>& ks, Node nf, - std::unordered_set<Node, NodeHashFunction>& synth_fv, - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>& free_vars) + std::unordered_set<Node>& synth_fv, + std::unordered_map<Node, std::unordered_set<Node>>& free_vars) { Assert(ns.size() == ks.size()); Trace("sygus-process-arg-deps") << "Process " << ns.size() @@ -266,14 +259,14 @@ void SynthConjectureProcessFun::processTerms( // get the relevant variables // relevant variables are those that appear in the body of the conjunction - std::unordered_set<Node, NodeHashFunction> rlv_vars; + std::unordered_set<Node> rlv_vars; Assert(free_vars.find(nf) != free_vars.end()); rlv_vars = free_vars[nf]; // get the single occurrence variables // single occurrence variables are those that appear in only one position, // as an argument to the function-to-synthesize. - std::unordered_map<Node, bool, NodeHashFunction> single_occ_variables; + std::unordered_map<Node, bool> single_occ_variables; for (unsigned index = 0; index < ns.size(); index++) { Node n = ns[index]; @@ -282,7 +275,7 @@ void SynthConjectureProcessFun::processTerms( Node nn = n[i]; if (nn.isVar()) { - std::unordered_map<Node, bool, NodeHashFunction>::iterator its = + std::unordered_map<Node, bool>::iterator its = single_occ_variables.find(nn); if (its == single_occ_variables.end()) { @@ -296,12 +289,10 @@ void SynthConjectureProcessFun::processTerms( } else { - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>::iterator itf = free_vars.find(nn); + std::unordered_map<Node, std::unordered_set<Node>>::iterator itf = + free_vars.find(nn); Assert(itf != free_vars.end()); - for (std::unordered_set<Node, NodeHashFunction>::iterator itfv = - itf->second.begin(); + for (std::unordered_set<Node>::iterator itfv = itf->second.begin(); itfv != itf->second.end(); ++itfv) { @@ -327,10 +318,9 @@ void SynthConjectureProcessFun::processTerms( std::unordered_map<unsigned, Node> n_arg_map; // terms to the argument that is carrying it. // the arguments in the range of this map must be marked as relevant. - std::unordered_map<Node, unsigned, NodeHashFunction> term_to_arg_carry; + std::unordered_map<Node, unsigned> term_to_arg_carry; // map of terms to (unprocessed) arguments where it occurs - std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction> - term_to_args; + std::unordered_map<Node, std::vector<unsigned>> term_to_args; // initialize for (unsigned a = 0; a < n.getNumChildren(); a++) @@ -408,8 +398,8 @@ void SynthConjectureProcessFun::processTerms( // list of all arguments std::vector<Node> arg_list; // now look at the terms for unprocessed arguments - for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>:: - iterator it = term_to_args.begin(); + for (std::unordered_map<Node, std::vector<unsigned>>::iterator it = + term_to_args.begin(); it != term_to_args.end(); ++it) { @@ -454,8 +444,8 @@ void SynthConjectureProcessFun::processTerms( { infer_def_t = Node::null(); // see if we can infer a definition - for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>:: - iterator it = term_to_args.begin(); + for (std::unordered_map<Node, std::vector<unsigned>>::iterator it = + term_to_args.begin(); it != term_to_args.end(); ++it) { @@ -483,8 +473,8 @@ void SynthConjectureProcessFun::processTerms( while (arg_list_counter < arg_list.size() && !success) { Node curr = arg_list[arg_list_counter]; - std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>:: - iterator it = term_to_args.find(curr); + std::unordered_map<Node, std::vector<unsigned>>::iterator it = + term_to_args.find(curr); if (it != term_to_args.end()) { Trace("sygus-process-arg-deps") << " *** Decide relevant " << curr @@ -548,7 +538,7 @@ Node SynthConjectureProcess::postSimplify(Node q) // get the base on the conjecture Node base = q[1]; - std::unordered_set<Node, NodeHashFunction> synth_fv; + std::unordered_set<Node> synth_fv; if (base.getKind() == NOT && base[0].getKind() == FORALL) { for (unsigned j = 0, size = base[0][0].getNumChildren(); j < size; j++) @@ -617,8 +607,9 @@ bool SynthConjectureProcess::getIrrelevantArgs( return false; } -void SynthConjectureProcess::processConjunct( - Node n, Node f, std::unordered_set<Node, NodeHashFunction>& synth_fv) +void SynthConjectureProcess::processConjunct(Node n, + Node f, + std::unordered_set<Node>& synth_fv) { Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl; Trace("sygus-process-arg-deps") << " " << n << " for synth fun " << f @@ -626,24 +617,20 @@ void SynthConjectureProcess::processConjunct( // first, flatten the conjunct // make a copy of free variables since we may add new ones - std::unordered_set<Node, NodeHashFunction> synth_fv_n = synth_fv; - std::unordered_map<Node, Node, NodeHashFunction> defs; + std::unordered_set<Node> synth_fv_n = synth_fv; + std::unordered_map<Node, Node> defs; Node nf = flatten(n, f, synth_fv_n, defs); Trace("sygus-process-arg-deps") << "Flattened to: " << std::endl; Trace("sygus-process-arg-deps") << " " << nf << std::endl; // get free variables in nf - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction> - free_vars; + std::unordered_map<Node, std::unordered_set<Node>> free_vars; getFreeVariables(nf, synth_fv_n, free_vars); // get free variables in each application std::vector<Node> ns; std::vector<Node> ks; - for (std::unordered_map<Node, Node, NodeHashFunction>::iterator it = - defs.begin(); + for (std::unordered_map<Node, Node>::iterator it = defs.begin(); it != defs.end(); ++it) { @@ -666,11 +653,11 @@ void SynthConjectureProcess::processConjunct( Node SynthConjectureProcess::SynthConjectureProcess::flatten( Node n, Node f, - std::unordered_set<Node, NodeHashFunction>& synth_fv, - std::unordered_map<Node, Node, NodeHashFunction>& defs) + std::unordered_set<Node>& synth_fv, + std::unordered_map<Node, Node>& defs) { - std::unordered_map<Node, Node, NodeHashFunction> visited; - std::unordered_map<Node, Node, NodeHashFunction>::iterator it; + std::unordered_map<Node, Node> visited; + std::unordered_map<Node, Node>::iterator it; std::stack<Node> visit; Node cur; visit.push(n); @@ -730,15 +717,13 @@ Node SynthConjectureProcess::SynthConjectureProcess::flatten( void SynthConjectureProcess::getFreeVariables( Node n, - std::unordered_set<Node, NodeHashFunction>& synth_fv, - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>& free_vars) + std::unordered_set<Node>& synth_fv, + std::unordered_map<Node, std::unordered_set<Node>>& free_vars) { // first must compute free variables in each subterm of n, // as well as contains_synth_fun - std::unordered_map<Node, bool, NodeHashFunction> visited; - std::unordered_map<Node, bool, NodeHashFunction>::iterator it; + std::unordered_map<Node, bool> visited; + std::unordered_map<Node, bool>::iterator it; std::stack<Node> visit; Node cur; visit.push(n); diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 3a2c6eb4d..d751e4c9c 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -144,10 +144,8 @@ struct SynthConjectureProcessFun std::vector<Node>& ns, std::vector<Node>& ks, Node nf, - std::unordered_set<Node, NodeHashFunction>& synth_fv, - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>& free_vars); + std::unordered_set<Node>& synth_fv, + std::unordered_map<Node, std::unordered_set<Node>>& free_vars); /** is the i^th argument of the function-to-synthesize of this class relevant? */ bool isArgRelevant(unsigned i); @@ -169,7 +167,7 @@ struct SynthConjectureProcessFun /** map from d_arg_vars to the argument # * they represent. */ - std::unordered_map<Node, unsigned, NodeHashFunction> d_arg_var_num; + std::unordered_map<Node, unsigned> d_arg_var_num; /** check match * This function returns true iff we can infer: * cn * { x -> n_arg_map[d_arg_var_num[x]] | x in d_arg_vars } = n @@ -217,10 +215,8 @@ struct SynthConjectureProcessFun */ Node inferDefinition( Node n, - std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry, - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>& free_vars); + std::unordered_map<Node, unsigned>& term_to_arg_carry, + std::unordered_map<Node, std::unordered_set<Node>>& free_vars); /** Assign relevant definition * * If def is non-null, @@ -322,9 +318,7 @@ class SynthConjectureProcess * is the set of (inner) universal variables in the synthesis * conjecture. */ - void processConjunct(Node n, - Node f, - std::unordered_set<Node, NodeHashFunction>& synth_fv); + void processConjunct(Node n, Node f, std::unordered_set<Node>& synth_fv); /** flatten * * Flattens all applications of f in term n. @@ -337,18 +331,16 @@ class SynthConjectureProcess */ Node flatten(Node n, Node f, - std::unordered_set<Node, NodeHashFunction>& synth_fv, - std::unordered_map<Node, Node, NodeHashFunction>& defs); + std::unordered_set<Node>& synth_fv, + std::unordered_map<Node, Node>& defs); /** get free variables * Constructs a map of all free variables that occur in n * from synth_fv and stores them in the map free_vars. */ void getFreeVariables( Node n, - std::unordered_set<Node, NodeHashFunction>& synth_fv, - std::unordered_map<Node, - std::unordered_set<Node, NodeHashFunction>, - NodeHashFunction>& free_vars); + std::unordered_set<Node>& synth_fv, + std::unordered_map<Node, std::unordered_set<Node>>& free_vars); /** for each synth-fun, information that is specific to this conjecture */ std::map<Node, SynthConjectureProcessFun> d_sf_info; diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 1321ad879..719bb448b 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -70,7 +70,7 @@ Node SygusReconstruct::reconstructSolution(Node sol, // the set of unique (up to rewriting) patterns/shapes in the grammar used by // matching - std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> pool; + std::unordered_map<TypeNode, std::vector<Node>> pool; uint64_t count = 0; @@ -209,7 +209,7 @@ TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz) // obligations generated by match. Note that we might have already seen (and // even solved) those obligations, hence the name "candidate obligations" - std::unordered_map<Node, Node, NodeHashFunction> candObs; + std::unordered_map<Node, Node> candObs; // the builtin terms corresponding to sygus variables in the grammar are bound // variables. However, we want the `match` method to treat them as ground // terms. So, we add redundant substitutions @@ -444,10 +444,10 @@ void SygusReconstruct::removeSolvedObs(TypeObligationSetMap& unsolvedObs) Node SygusReconstruct::mkGround(Node n) const { // get the set of bound variables in n - std::unordered_set<TNode, TNodeHashFunction> vars; + std::unordered_set<TNode> vars; expr::getVariables(n, vars); - std::unordered_map<TNode, TNode, TNodeHashFunction> subs; + std::unordered_map<TNode, TNode> subs; // generate a ground value for each one of those variables for (const TNode& var : vars) @@ -492,8 +492,7 @@ void SygusReconstruct::clear() } void SygusReconstruct::printPool( - const std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>& - pool) const + const std::unordered_map<TypeNode, std::vector<Node>>& pool) const { Trace("sygus-rcons") << "\nPool:\n["; diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index 334b95e71..e3c214bde 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -28,9 +28,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -using ObligationSet = std::unordered_set<Node, NodeHashFunction>; -using TypeObligationSetMap = - std::unordered_map<TypeNode, ObligationSet, TypeNodeHashFunction>; +using ObligationSet = std::unordered_set<Node>; +using TypeObligationSetMap = std::unordered_map<TypeNode, ObligationSet>; /** SygusReconstruct * @@ -288,9 +287,8 @@ class SygusReconstruct : public expr::NotifyMatch * * @param pool a pool of patterns/shapes to print */ - void printPool(const std::unordered_map<TypeNode, - std::vector<Node>, - TypeNodeHashFunction>& pool) const; + void printPool( + const std::unordered_map<TypeNode, std::vector<Node>>& pool) const; /** pointer to the sygus term database */ TermDbSygus* d_tds; @@ -298,20 +296,20 @@ class SygusReconstruct : public expr::NotifyMatch SygusStatistics& d_stats; /** a map from an obligation to its reconstruction info */ - std::unordered_map<Node, RConsObligationInfo, NodeHashFunction> d_obInfo; + std::unordered_map<Node, RConsObligationInfo> d_obInfo; /** a map from a sygus datatype type to its reconstruction info */ - std::unordered_map<TypeNode, RConsTypeInfo, TypeNodeHashFunction> d_stnInfo; + std::unordered_map<TypeNode, RConsTypeInfo> d_stnInfo; /** a map from an obligation to its sygus solution (if it exists) */ - std::unordered_map<TNode, TNode, TNodeHashFunction> d_sol; + std::unordered_map<TNode, TNode> d_sol; /** a map from a candidate solution to its sub-obligations */ - std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_subObs; + std::unordered_map<Node, std::vector<Node>> d_subObs; /** a map from a candidate solution to its parent obligation */ - std::unordered_map<Node, Node, NodeHashFunction> d_parentOb; + std::unordered_map<Node, Node> d_parentOb; /** a cache of sygus variables treated as ground terms by matching */ - std::unordered_map<Node, Node, NodeHashFunction> d_sygusVars; + std::unordered_map<Node, Node> d_sygusVars; /** A trie for filtering out redundant terms from the paterns pool */ expr::MatchTrie d_poolTrie; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 62f362e2b..d45a96d3b 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -286,7 +286,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, bool SygusRepairConst::mustRepair(Node n) { - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -365,8 +365,8 @@ Node SygusRepairConst::getSkeleton(Node n, } NodeManager* nm = NodeManager::currentNM(); // get the most general candidate skeleton of n - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -464,8 +464,8 @@ Node SygusRepairConst::getFoQuery(Node body, // now, we must replace all terms of the form eval( z_i, t1...tn ) with // a fresh first-order variable w_i, where z_i is a variable introduced in // the skeleton inference step (z_i is a variable in sk_vars). - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> visited; + std::unordered_map<TNode, Node>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(body); @@ -577,8 +577,8 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, // should have at least one restriction Assert(restrictLA); - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 1a2159b10..f0452a59c 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -123,7 +123,7 @@ class SygusRepairConst /** reverse map of d_sk_to_fo */ std::map<Node, Node> d_fo_to_sk; /** a cache of satisfiability queries of the form [***] above we have tried */ - std::unordered_set<Node, NodeHashFunction> d_queries; + std::unordered_set<Node> d_queries; /** * Register information for sygus type tn, tprocessed stores the set of * already registered types. diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 7f816a97f..4cf0e6bb4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1128,9 +1128,8 @@ Node SygusUnifIo::constructSol( if (ret_dt.isNull() && !retValMod) { bool firstTime = true; - std::unordered_set<Node, NodeHashFunction> intersection; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator - pit; + std::unordered_set<Node> intersection; + std::map<TypeNode, std::unordered_set<Node>>::iterator pit; for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++) { if (x.d_vals[i].getConst<bool>()) diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index ef6732cd6..fd918c996 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -311,9 +311,7 @@ class SygusUnifIo : public SygusUnif * A -> ite( A, B, C ) | ... * where terms of type B and C can both act as solutions. */ - std::map<size_t, - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>> - d_psolutions; + std::map<size_t, std::map<TypeNode, std::unordered_set<Node>>> d_psolutions; /** * This flag is set to true if the solution construction was * non-deterministic with respect to failure/success. diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 356c908dc..a5c7af161 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -30,10 +30,10 @@ namespace quantifiers { using BoolNodePair = std::pair<bool, Node>; using BoolNodePairHashFunction = - PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>; + PairHashFunction<bool, Node, BoolHashFunction, std::hash<Node>>; using BoolNodePairMap = std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>; -using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>; +using NodePairMap = std::unordered_map<Node, Node>; using NodePair = std::pair<Node, Node>; class SynthConjecture; @@ -120,7 +120,7 @@ class SygusUnifRl : public SygusUnif /** Whether we are additionally using information gain heuristics */ bool d_useCondPoolIGain; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ - std::unordered_set<Node, NodeHashFunction> d_unif_candidates; + std::unordered_set<Node> d_unif_candidates; /** construct sol */ Node constructSol(Node f, Node e, @@ -248,7 +248,7 @@ class SygusUnifRl : public SygusUnif /** gathered evaluation point heads */ std::vector<Node> d_hds; /** all enumerated model values for conditions */ - std::unordered_set<Node, NodeHashFunction> d_cond_mvs; + std::unordered_set<Node> d_cond_mvs; /** get condition enumerator */ Node getConditionEnumerator() const { return d_cond_enum; } /** set conditions */ @@ -262,7 +262,7 @@ class SygusUnifRl : public SygusUnif Node d_false; /** Accumulates solutions built when considering all enumerated condition * values (which may generate repeated solutions) */ - std::unordered_set<Node, NodeHashFunction> d_sols; + std::unordered_set<Node> d_sols; /** * Conditional enumerator variables corresponding to the condition values in * d_conds. These are used for generating separation lemmas during diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index ec4ade86b..df73c4821 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -31,7 +31,7 @@ namespace quantifiers { class SynthEngine : public QuantifiersModule { - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, bool> NodeBoolMap; public: SynthEngine(QuantifiersState& qs, diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index b18a7c796..826563401 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1018,11 +1018,10 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, return rewriteNode(res); } -Node TermDbSygus::evaluateWithUnfolding( - Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited) +Node TermDbSygus::evaluateWithUnfolding(Node n, + std::unordered_map<Node, Node>& visited) { - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = - visited.find(n); + std::unordered_map<Node, Node>::iterator it = visited.find(n); if( it==visited.end() ){ Node ret = n; while (ret.getKind() == DT_SYGUS_EVAL @@ -1068,7 +1067,7 @@ Node TermDbSygus::evaluateWithUnfolding( Node TermDbSygus::evaluateWithUnfolding(Node n) { - std::unordered_map<Node, Node, NodeHashFunction> visited; + std::unordered_map<Node, Node> visited; return evaluateWithUnfolding(n, visited); } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index c8a422a0e..e0a812069 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -285,8 +285,7 @@ class TermDbSygus { */ Node evaluateWithUnfolding(Node n); /** same as above, but with a cache of visited nodes */ - Node evaluateWithUnfolding( - Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited); + Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited); /** is evaluation point? * * Returns true if n is of the form eval( x, c1...cn ) for some variable x 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) { 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 diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index d4720ea7c..36602d3ae 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -323,8 +323,8 @@ bool SygusSampler::isContiguous(Node n) void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs) { - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -359,8 +359,8 @@ bool SygusSampler::checkVariables(Node n, bool checkOrder, bool checkLinear) // compute free variables in n for each type std::map<unsigned, std::vector<Node> > fvs; - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -411,8 +411,8 @@ bool SygusSampler::containsFreeVariables(Node a, Node b, bool strict) computeFreeVariables(a, fvs); std::vector<Node> fv_found; - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(b); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 56a486022..bedab16f1 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -152,8 +152,7 @@ Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar) Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) { - std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it = - d_type_fv.find(tn); + std::unordered_map<TypeNode, Node>::iterator it = d_type_fv.find(tn); if (it == d_type_fv.end()) { SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index a8551a581..01465c7ca 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -65,13 +65,12 @@ class DbList * lazily for performance reasons. */ class TermDb : public QuantifiersUtil { - using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>; + using NodeBoolMap = context::CDHashMap<Node, bool>; using NodeList = context::CDList<Node>; - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; - using TypeNodeDbListMap = context:: - CDHashMap<TypeNode, std::shared_ptr<DbList>, TypeNodeHashFunction>; - using NodeDbListMap = - context::CDHashMap<Node, std::shared_ptr<DbList>, NodeHashFunction>; + using NodeSet = context::CDHashSet<Node>; + using TypeNodeDbListMap = + context::CDHashMap<TypeNode, std::shared_ptr<DbList>>; + using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>; public: TermDb(QuantifiersState& qs, @@ -316,7 +315,7 @@ class TermDb : public QuantifiersUtil { Node d_true; Node d_false; /** map from type nodes to a fresh variable we introduced */ - std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv; + std::unordered_map<TypeNode, Node> d_type_fv; /** inactive map */ NodeBoolMap d_inactive_map; /** count of the number of non-redundant ground terms per operator */ diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index ffade62fb..d6b0d8154 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -29,8 +29,7 @@ Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index) { Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; - std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it = - d_typ_enum_map.find(tn); + std::unordered_map<TypeNode, size_t>::iterator it = d_typ_enum_map.find(tn); size_t teIndex; if (it == d_typ_enum_map.end()) { diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index 50abef744..f23640e07 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -62,10 +62,9 @@ class TermEnumeration */ QuantifiersBoundInference* d_qbi; /** ground terms enumerated for types */ - std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> - d_enum_terms; + std::unordered_map<TypeNode, std::vector<Node>> d_enum_terms; /** map from type to the index of its type enumerator in d_typ_enum. */ - std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map; + std::unordered_map<TypeNode, size_t> d_typ_enum_map; /** type enumerators */ std::vector<TypeEnumerator> d_typ_enum; }; diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp index aa0fbd06d..883161f1a 100644 --- a/src/theory/quantifiers/term_pools.cpp +++ b/src/theory/quantifiers/term_pools.cpp @@ -98,7 +98,7 @@ void TermPools::getTermsForPool(Node p, std::vector<Node>& terms) // if we have yet to compute terms on this round if (dom.d_currTerms.empty()) { - std::unordered_set<Node, NodeHashFunction> reps; + std::unordered_set<Node> reps; // eliminate modulo equality for (const Node& t : dom.d_terms) { diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index cf2ba7a47..c3e4fcf4c 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -39,7 +39,7 @@ class FirstOrderModel; */ class TermRegistry { - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + using NodeSet = context::CDHashSet<Node>; public: TermRegistry(QuantifiersState& qs, diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 9db3dd020..b771db986 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -123,7 +123,7 @@ Node TermUtil::getRemoveQuantifiers( Node n ) { //quantified simplify Node TermUtil::getQuantSimplify( Node n ) { - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(n, fvs); if (fvs.empty()) { @@ -156,8 +156,8 @@ void TermUtil::computeVarContainsInternal(Node n, Kind k, std::vector<Node>& vars) { - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); |