diff options
Diffstat (limited to 'src/theory')
228 files changed, 990 insertions, 1108 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 4d181b39f..ed7f54182 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -48,7 +48,7 @@ class ArithIteUtils { SubstitutionMap* d_subs; TheoryModel* d_model; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node> NodeMap; // cache for reduce vars NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n @@ -58,13 +58,13 @@ class ArithIteUtils { NodeMap d_reduceGcd; - typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap; + typedef std::unordered_map<Node, Integer> NodeIntegerMap; NodeIntegerMap d_gcds; Integer d_one; context::CDO<unsigned> d_subcount; - typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> CDNodeMap; + typedef context::CDInsertHashMap<Node, Node> CDNodeMap; CDNodeMap d_skolems; typedef std::map<Node, std::set<Node> > ImpMap; diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index d5533de24..6ab399348 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -39,8 +39,7 @@ TrustNode ArithPreprocess::eliminate(TNode n, bool ArithPreprocess::reduceAssertion(TNode atom) { - context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it = - d_reduced.find(atom); + context::CDHashMap<Node, bool>::const_iterator it = d_reduced.find(atom); if (it != d_reduced.end()) { // already computed @@ -70,8 +69,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom) bool ArithPreprocess::isReduced(TNode atom) const { - context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it = - d_reduced.find(atom); + context::CDHashMap<Node, bool>::const_iterator it = d_reduced.find(atom); if (it == d_reduced.end()) { return false; diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index 63b4515e7..a537c33c7 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -83,7 +83,7 @@ class ArithPreprocess /** The operator elimination utility */ OperatorElim& d_opElim; /** The set of assertions that were reduced */ - context::CDHashMap<Node, bool, NodeHashFunction> d_reduced; + context::CDHashMap<Node, bool> d_reduced; }; } // namespace arith diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 7ff674b25..7c6bfc47b 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -39,9 +39,9 @@ private: /** * Map from a node to it's minimum and maximum. */ - typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap; - CDNodeToMinMaxMap d_minMap; - CDNodeToMinMaxMap d_maxMap; + typedef context::CDHashMap<Node, DeltaRational> CDNodeToMinMaxMap; + CDNodeToMinMaxMap d_minMap; + CDNodeToMinMaxMap d_maxMap; public: ArithStaticLearner(context::Context* userContext); diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 81968fc13..75edc49f5 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -207,8 +207,8 @@ Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs) { Assert(vars.size() == subs.size()); 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<Node>::iterator itv; std::vector<TNode> visit; TNode cur; diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 0c6378bc2..6617fccb0 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -34,12 +34,12 @@ namespace theory { namespace arith { //Sets of Nodes -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; -typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; -typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; +typedef std::unordered_set<Node> NodeSet; +typedef std::unordered_set<TNode> TNodeSet; +typedef context::CDHashSet<Node> CDNodeSet; //Maps from Nodes -> ArithVars, and vice versa -typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap; +typedef std::unordered_map<Node, ArithVar> NodeToArithVarMap; typedef DenseMap<Node> ArithVarToNodeMap; inline Node mkRationalNode(const Rational& q){ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 6032adcc8..e45b7bf29 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -101,7 +101,7 @@ private: * This is node is potentially both the propagation or * Rewriter::rewrite(propagation). */ - typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap; + typedef context::CDHashMap<Node, size_t> ExplainMap; ExplainMap d_explanationMap; ConstraintDatabase& d_constraintDatabase; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index ecd5b10fb..0d3c96f89 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -156,7 +156,7 @@ enum ConstraintType {LowerBound, Equality, UpperBound, Disequality}; typedef context::CDList<ConstraintCP> CDConstraintList; -typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap; +typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap; typedef size_t ConstraintRuleID; static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max(); diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 1cd092abc..19bd2f2bf 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -294,7 +294,7 @@ bool DioSolver::queueEmpty() const{ } Node DioSolver::columnGcdIsOne() const{ - std::unordered_map<Node, Integer, NodeHashFunction> gcdMap; + std::unordered_map<Node, Integer> gcdMap; std::deque<TrailIndex>::const_iterator iter, end; for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 0fac563bb..8f2411036 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -68,7 +68,8 @@ private: * We maintain a map from the variables associated with proofs to an input constraint. * These variables can then be used in polynomial manipulations. */ - typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap; + typedef std::unordered_map<Node, InputConstraintIndex> + NodeToInputConstraintIndexMap; NodeToInputConstraintIndexMap d_varToInputConstraintMap; Node proofVariableToReason(const Variable& v) const{ diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 287b89851..7e103797e 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -43,7 +43,7 @@ class TheoryArith; */ class InferenceManager : public InferenceManagerBuffered { - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + using NodeSet = context::CDHashSet<Node>; public: InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm); diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index b2279344d..b0a4fd859 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -86,7 +86,7 @@ struct ExtState // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors std::map<Node, std::map<Node, Node> > d_mono_diff; /** the set of monomials we should apply tangent planes to */ - std::unordered_set<Node, NodeHashFunction> d_tplane_refine; + std::unordered_set<Node> d_tplane_refine; }; } // namespace nl diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 6df35c71d..404916453 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -238,7 +238,7 @@ void MonomialCheck::checkMagnitude(unsigned c) Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size() << " lemmas." << std::endl; // naive - std::unordered_set<Node, NodeHashFunction> r_lemmas; + std::unordered_set<Node> r_lemmas; for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb = cmp_infers.begin(); itb != cmp_infers.end(); diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index b42c7932d..c50737d51 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -40,7 +40,7 @@ class SplitZeroCheck void check(); private: - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + using NodeSet = context::CDHashSet<Node>; /** Basic data that is shared with other checks */ ExtState* d_data; diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 676390478..c80edbeb3 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -39,7 +39,7 @@ class NlModel; */ class IAndSolver { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: IAndSolver(InferenceManager& im, ArithState& state, NlModel& model); diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 6e96cfe7b..9cd74883b 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -67,7 +67,7 @@ inline std::ostream& operator<<(std::ostream& os, const IAWrapper& iaw) std::vector<Node> ICPSolver::collectVariables(const Node& n) const { - std::unordered_set<TNode, TNodeHashFunction> tmp; + std::unordered_set<TNode> tmp; expr::getVariables(n, tmp); std::vector<Node> res; for (const auto& t : tmp) @@ -93,7 +93,7 @@ std::vector<Candidate> ICPSolver::constructCandidates(const Node& n) auto poly = std::get<0>(comp); std::vector<Candidate> result; - std::unordered_set<TNode, TNodeHashFunction> vars; + std::unordered_set<TNode> vars; expr::getVariables(n, vars); for (const auto& v : vars) { diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 9b1246f67..ed4a5318f 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -242,7 +242,7 @@ bool NlModel::checkModel(const std::vector<Node>& assertions, // all remaining variables are constrained to their exact model values Trace("nl-ext-cm-debug") << " set exact bounds for remaining variables..." << std::endl; - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; std::vector<TNode> visit; TNode cur; for (const Node& a : assertions) @@ -479,10 +479,10 @@ bool NlModel::solveEqualitySimple(Node eq, NodeManager* nm = NodeManager::currentNM(); // the list of variables that occur as a monomial in msum, and whose value // is so far unconstrained in the model. - std::unordered_set<Node, NodeHashFunction> unc_vars; + std::unordered_set<Node> unc_vars; // the list of variables that occur as a factor in a monomial, and whose // value is so far unconstrained in the model. - std::unordered_set<Node, NodeHashFunction> unc_vars_factor; + std::unordered_set<Node> unc_vars_factor; for (std::pair<const Node, Node>& m : msum) { Node v = m.first; @@ -797,7 +797,7 @@ bool NlModel::simpleCheckModelLit(Node lit) Trace("nl-ext-cms-debug") << "* Try univariate quadratic analysis..." << std::endl; std::vector<Node> vs_invalid; - std::unordered_set<Node, NodeHashFunction> vs; + std::unordered_set<Node> vs; std::map<Node, Node> v_a; std::map<Node, Node> v_b; // get coefficients... diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 600dbd02c..acf5ee7f5 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -322,7 +322,7 @@ class NlModel * These literals are exempt from check-model, since they are satisfied by * definition of our model construction. */ - std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved; + std::unordered_map<Node, Node> d_check_model_solved; /** did we use an approximation on this call to last-call effort? */ bool d_used_approx; }; /* class NlModel */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index a3b32c6e9..8221e18d5 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -123,7 +123,7 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions) BoundInference bounds; - std::unordered_set<Node, NodeHashFunction> init_assertions; + std::unordered_set<Node> init_assertions; for (Theory::assertions_iterator it = d_containing.facts_begin(); it != d_containing.facts_end(); diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index e39f97402..4e029be7c 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -80,7 +80,7 @@ class NlLemma; */ class NonlinearExtension { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: NonlinearExtension(TheoryArith& containing, diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 62d101686..0d5e5ad04 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -291,8 +291,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) // compute the concavity int region = -1; - std::unordered_map<Node, int, NodeHashFunction>::iterator itr = - d_tstate.d_tf_region.find(tf); + std::unordered_map<Node, int>::iterator itr = d_tstate.d_tf_region.find(tf); if (itr != d_tstate.d_tf_region.end()) { region = itr->second; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index f98986fad..74f005294 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -201,7 +201,7 @@ struct TranscendentalState * arguments that contain transcendental functions. */ std::map<Node, Node> d_trMaster; - std::map<Node, std::unordered_set<Node, NodeHashFunction>> d_trSlaves; + std::map<Node, std::unordered_set<Node>> d_trSlaves; /** concavity region for transcendental functions * @@ -223,7 +223,7 @@ struct TranscendentalState * of transcendental functions whose arguments have model * values that reside in valid regions. */ - std::unordered_map<Node, int, NodeHashFunction> d_tf_region; + std::unordered_map<Node, int> d_tf_region; /** * Maps representives of a congruence class to the members of that class. * @@ -253,9 +253,7 @@ struct TranscendentalState * each transcendental function application. We store this set for each * Taylor degree. */ - std::unordered_map<Node, - std::map<unsigned, std::vector<Node>>, - NodeHashFunction> + std::unordered_map<Node, std::map<unsigned, std::vector<Node>>> d_secant_points; /** PI diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ce8e2393b..508362158 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3975,7 +3975,7 @@ void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet, // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); - std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms(); + std::unordered_set<TNode> shared = d_containing.currentlySharedTerms(); // TODO: // This is not very good for user push/pop.... @@ -4446,7 +4446,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b Node flattenImplication(Node imp){ NodeBuilder nb(kind::OR); - std::unordered_set<Node, NodeHashFunction> included; + std::unordered_set<Node> included; Node left = imp[0]; Node right = imp[1]; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e23451167..e029e3c41 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -193,8 +193,8 @@ private: * A superset of all of the assertions that currently are not the literal for * their constraint do not match constraint literals. Not just the witnesses. */ - context::CDInsertHashMap<Node, ConstraintP, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals; - + context::CDInsertHashMap<Node, ConstraintP> + d_assertionsThatDoNotMatchTheirLiterals; /** Returns true if x is of type Integer. */ inline bool isInteger(ArithVar x) const { @@ -267,8 +267,7 @@ private: /** * Contains all nodes that have been preregistered */ - context::CDHashSet<Node, NodeHashFunction> d_preregisteredNodes; - + context::CDHashSet<Node> d_preregisteredNodes; /** * Manages information about the assignment and upper and lower bounds on diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 15f27eb96..42c6e7387 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -86,8 +86,7 @@ public: } };/* class Info */ - -typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap; +typedef std::unordered_map<Node, Info*> CNodeInfoMap; /** * Class keeping track of the following information for canonical diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index e887feccb..9b5676d65 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -551,7 +551,7 @@ void TheoryArrays::weakEquivMakeRepIndex(TNode node) { } void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) { - std::unordered_set<TNode, TNodeHashFunction> marked; + std::unordered_set<TNode> marked; vector<TNode> index_trail; vector<TNode>::iterator it, iend; Node equivalence_trail = reason; @@ -1043,7 +1043,8 @@ bool TheoryArrays::collectModelValues(TheoryModel* m, std::vector<Node> arrays; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); - for (; !eqcs_i.isFinished(); ++eqcs_i) { + for (; !eqcs_i.isFinished(); ++eqcs_i) + { Node eqc = (*eqcs_i); if (!eqc.getType().isArray()) { @@ -1051,9 +1052,11 @@ bool TheoryArrays::collectModelValues(TheoryModel* m, continue; } eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine); - for (; !eqc_i.isFinished(); ++eqc_i) { + for (; !eqc_i.isFinished(); ++eqc_i) + { Node n = *eqc_i; - // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly + // If this EC is an array type and it contains something other than STORE + // nodes, we have to compute a representative explicitly if (termSet.find(n) != termSet.end()) { if (n.getKind() != kind::STORE) @@ -1068,10 +1071,13 @@ bool TheoryArrays::collectModelValues(TheoryModel* m, // Build a list of all the relevant reads, indexed by the store representative std::map<Node, std::vector<Node> > selects; set<Node>::iterator set_it = termSet.begin(), set_it_end = termSet.end(); - for (; set_it != set_it_end; ++set_it) { + for (; set_it != set_it_end; ++set_it) + { Node n = *set_it; - // If this term is a select, record that the EC rep of its store parameter is being read from using this term - if (n.getKind() == kind::SELECT) { + // If this term is a select, record that the EC rep of its store parameter + // is being read from using this term + if (n.getKind() == kind::SELECT) + { selects[d_equalityEngine->getRepresentative(n[0])].push_back(n); } } @@ -1081,71 +1087,82 @@ bool TheoryArrays::collectModelValues(TheoryModel* m, TypeSet defaultValuesSet; // Compute all default values already in use - //if (fullModel) { - for (size_t i=0; i<arrays.size(); ++i) { - TNode nrep = d_equalityEngine->getRepresentative(arrays[i]); - d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already - TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep); - it = d_defValues.find(mayRep); - if (it != d_defValues.end()) { - defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second); - } + // if (fullModel) { + for (size_t i = 0; i < arrays.size(); ++i) + { + TNode nrep = d_equalityEngine->getRepresentative(arrays[i]); + d_mayEqualEqualityEngine.addTerm( + nrep); // add the term in case it isn't there already + TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep); + it = d_defValues.find(mayRep); + if (it != d_defValues.end()) + { + defaultValuesSet.add(nrep.getType().getArrayConstituentType(), + (*it).second); } + } //} - // Loop through all array equivalence classes that need a representative computed - for (size_t i = 0; i < arrays.size(); ++i) + // Loop through all array equivalence classes that need a representative + // computed + for (size_t i = 0; i < arrays.size(); ++i) + { + TNode n = arrays[i]; + TNode nrep = d_equalityEngine->getRepresentative(n); + + // if (fullModel) { + // Compute default value for this array - there is one default value for + // every mayEqual equivalence class + TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep); + it = d_defValues.find(mayRep); + // If this mayEqual EC doesn't have a default value associated, get the next + // available default value for the associated array element type + if (it == d_defValues.end()) { - TNode n = arrays[i]; - TNode nrep = d_equalityEngine->getRepresentative(n); - - // if (fullModel) { - // Compute default value for this array - there is one default value for - // every mayEqual equivalence class - TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep); - it = d_defValues.find(mayRep); - // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type - if (it == d_defValues.end()) { - TypeNode valueType = nrep.getType().getArrayConstituentType(); - rep = defaultValuesSet.nextTypeEnum(valueType); - if (rep.isNull()) { - Assert(defaultValuesSet.getSet(valueType)->begin() - != defaultValuesSet.getSet(valueType)->end()); - rep = *(defaultValuesSet.getSet(valueType)->begin()); - } - Trace("arrays-models") << "New default value = " << rep << endl; - d_defValues[mayRep] = rep; - } - else { - rep = (*it).second; + TypeNode valueType = nrep.getType().getArrayConstituentType(); + rep = defaultValuesSet.nextTypeEnum(valueType); + if (rep.isNull()) + { + Assert(defaultValuesSet.getSet(valueType)->begin() + != defaultValuesSet.getSet(valueType)->end()); + rep = *(defaultValuesSet.getSet(valueType)->begin()); } + Trace("arrays-models") << "New default value = " << rep << endl; + d_defValues[mayRep] = rep; + } + else + { + rep = (*it).second; + } - // Build the STORE_ALL term with the default value - rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep)); - /* + // Build the STORE_ALL term with the default value + rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep)); + /* + } + else { + std::unordered_map<Node, Node>::iterator it = d_skolemCache.find(n); + if (it == d_skolemCache.end()) { + rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model + variable for array collectModelInfo"); d_skolemCache[n] = rep; } else { - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); - if (it == d_skolemCache.end()) { - rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo"); - d_skolemCache[n] = rep; - } - else { - rep = (*it).second; - } + rep = (*it).second; } + } */ // For each read, require that the rep stores the right value vector<Node>& reads = selects[nrep]; - for (unsigned j = 0; j < reads.size(); ++j) { + for (unsigned j = 0; j < reads.size(); ++j) + { rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]); } if (!m->assertEquality(n, rep, true)) { return false; } - if (!n.isConst()) { + if (!n.isConst()) + { m->assertSkeleton(rep); } } @@ -1181,7 +1198,7 @@ Node TheoryArrays::getSkolem(TNode ref) // the call to SkolemCache::getExtIndexSkolem should be deterministic, but use // cache anyways for now Node skolem; - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); + std::unordered_map<Node, Node>::iterator it = d_skolemCache.find(ref); if (it == d_skolemCache.end()) { Assert(ref.getKind() == kind::NOT && ref[0].getKind() == kind::EQUAL); // make the skolem using the skolem cache utility diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index f9813cd3f..c85b382e4 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -215,7 +215,7 @@ class TheoryArrays : public Theory { void explain(TNode literal, Node& exp); /** For debugging only- checks invariants about when things are preregistered*/ - context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered; + context::CDHashSet<Node> d_isPreRegistered; /** Helper for preRegisterTerm, also used internally */ void preRegisterTermInternal(TNode n); @@ -374,7 +374,7 @@ class TheoryArrays : public Theory { context::CDQueue<RowLemmaType> d_RowQueue; context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded; - typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; + typedef context::CDHashSet<Node> CDNodeSet; CDNodeSet d_sharedArrays; CDNodeSet d_sharedOther; @@ -384,7 +384,7 @@ class TheoryArrays : public Theory { // When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList) // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time. // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time. - typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap; + typedef std::unordered_map<Node, CTNodeList*> CNodeNListMap; CNodeNListMap d_constReads; context::CDList<TNode> d_reads; context::CDList<TNode> d_constReadsList; @@ -410,7 +410,7 @@ class TheoryArrays : public Theory { };/* class ContextPopper */ ContextPopper d_contextPopper; - std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache; + std::unordered_map<Node, Node> d_skolemCache; context::CDO<unsigned> d_skolemIndex; std::vector<Node> d_skolemAssertions; @@ -420,11 +420,11 @@ class TheoryArrays : public Theory { // List of nodes that need permanent references in this context context::CDList<Node> d_permRef; context::CDList<Node> d_modelConstraints; - context::CDHashSet<Node, NodeHashFunction > d_lemmasSaved; + context::CDHashSet<Node> d_lemmasSaved; std::vector<Node> d_lemmas; // Default values for each mayEqual equivalence class - typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap; + typedef context::CDHashMap<Node, Node> DefValMap; DefValMap d_defValues; typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 6269cb5dd..8ad7a5f95 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -177,9 +177,9 @@ Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard) // Bad case: have to recompute value counts and/or possibly switch out // default value store = n; - std::unordered_set<TNode, TNodeHashFunction> indexSet; - std::unordered_map<TNode, uint32_t, TNodeHashFunction> elementsMap; - std::unordered_map<TNode, uint32_t, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> indexSet; + std::unordered_map<TNode, uint32_t> elementsMap; + std::unordered_map<TNode, uint32_t>::iterator it; uint32_t count; uint32_t max = 0; TNode maxValue; diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index 19ae573d8..5abc752d6 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -45,9 +45,9 @@ void UnionFind<NodeType, NodeHash>::notify() { // The following declarations allow us to put functions in the .cpp file // instead of the header, since we know which instantiations are needed. -template void UnionFind<Node, NodeHashFunction>::notify(); +template void UnionFind<Node, std::hash<Node>>::notify(); -template void UnionFind<TNode, TNodeHashFunction>::notify(); +template void UnionFind<TNode, std::hash<TNode>>::notify(); } // namespace arrays } // namespace theory diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index 0d2bf0bb4..63d66f200 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -105,7 +105,7 @@ private: /** We index the requests in this vector, it's a list */ context::CDList<Element> d_requests; - typedef context::CDHashMap<Node, element_index, NodeHashFunction> trigger_to_list_map; + typedef context::CDHashMap<Node, element_index> trigger_to_list_map; /** Map from triggers, to the list of elements they trigger */ trigger_to_list_map d_triggerToRequestMap; diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index a74515d37..5ce05baba 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -35,7 +35,7 @@ class SolverState; */ class InferenceManager : public InferenceManagerBuffered { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp index ed3d4cf26..c03b21236 100644 --- a/src/theory/bags/make_bag_op.cpp +++ b/src/theory/bags/make_bag_op.cpp @@ -28,7 +28,7 @@ std::ostream& operator<<(std::ostream& out, const MakeBagOp& op) size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const { - return TypeNodeHashFunction()(op.getType()); + return std::hash<TypeNode>()(op.getType()); } MakeBagOp::MakeBagOp(const TypeNode& elementType) diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index 6255f3b00..2b0218fdf 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -36,7 +36,7 @@ class SolverState; */ class TermRegistry { - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDHashMap<Node, Node> NodeMap; public: TermRegistry(SolverState& state, InferenceManager& im); diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 443be0ec7..1d4f6e9ee 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -63,8 +63,7 @@ class CircuitPropagator ASSIGNED_TO_FALSE, }; - typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> - BackEdgesMap; + typedef std::unordered_map<Node, std::vector<Node>> BackEdgesMap; /** * Construct a new CircuitPropagator. @@ -172,8 +171,7 @@ class CircuitPropagator /** * Assignment status of each node. */ - typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> - AssignmentMap; + typedef context::CDHashMap<TNode, AssignmentStatus> AssignmentMap; /** * Assign Node in circuit with the value and add it to the queue; note @@ -245,7 +243,7 @@ class CircuitPropagator /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - context::CDHashSet<Node, NodeHashFunction> d_seen; + context::CDHashSet<Node> d_seen; AssignmentMap d_state; diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 8b2967fe6..2d2155f44 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -140,7 +140,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return Node::null(); } // remove duplicates while keeping the order of children - std::unordered_set<TNode, TNodeHashFunction> clauseSet; + std::unordered_set<TNode> clauseSet; std::vector<Node> disjuncts; unsigned size = children[0].getNumChildren(); for (unsigned i = 0; i < size; ++i) @@ -166,7 +166,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, { Assert(children.size() == 1); Assert(args.size() == 1); - std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2; + std::unordered_set<Node> clauseSet1, clauseSet2; if (children[0].getKind() == kind::OR) { clauseSet1.insert(children[0].begin(), children[0].end()); @@ -201,7 +201,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, Node falseNode = nm->mkConst(false); std::vector<Node> clauseNodes; // literals to be removed from the virtual lhs clause of the resolution - std::unordered_map<Node, unsigned, NodeHashFunction> lhsElim; + std::unordered_map<Node, unsigned> lhsElim; for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2) { // whether pivot should occur as is or negated depends on the polarity of @@ -320,7 +320,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; ++i) { - std::unordered_set<Node, NodeHashFunction> elim; + std::unordered_set<Node> elim; // literals to be removed from "first" clause if (i < childrenSize - 1) { @@ -387,8 +387,8 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, } Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n"; // check that set representation is the same as of the given conclusion - std::unordered_set<Node, NodeHashFunction> clauseComputed{ - clauseNodes.begin(), clauseNodes.end()}; + std::unordered_set<Node> clauseComputed{clauseNodes.begin(), + clauseNodes.end()}; Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop; if (clauseComputed.empty()) { @@ -415,8 +415,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } - std::unordered_set<Node, NodeHashFunction> clauseGiven{args[0].begin(), - args[0].end()}; + std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()}; return clauseComputed == clauseGiven ? args[0] : Node::null(); } if (id == PfRule::SPLIT) diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 0d7431a8e..44d337c28 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -45,7 +45,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { */ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) { - typedef std::unordered_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode> node_set; node_set visited; visited.insert(skipNode); diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index e22f5f20f..68d6e1ad1 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -144,9 +144,13 @@ TypeNode TheoryBuiltinRewriter::getArrayTypeForFunctionType(TypeNode ftn) return ret; } -Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, - std::unordered_map< TNode, Node, TNodeHashFunction >& visited ){ - std::unordered_map< TNode, Node, TNodeHashFunction >::iterator it = visited.find( a ); +Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec( + TNode a, + TNode bvl, + unsigned bvlIndex, + std::unordered_map<TNode, Node>& visited) +{ + std::unordered_map<TNode, Node>::iterator it = visited.find(a); if( it==visited.end() ){ Node ret; if( bvlIndex<bvl.getNumChildren() ){ @@ -185,7 +189,7 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec( TNode a, TNode b Node TheoryBuiltinRewriter::getLambdaForArrayRepresentation( TNode a, TNode bvl ){ Assert(a.getType().isArray()); - std::unordered_map< TNode, Node, TNodeHashFunction > visited; + std::unordered_map<TNode, Node> visited; Trace("builtin-rewrite-debug") << "Get lambda for : " << a << ", with variables " << bvl << std::endl; Node body = getLambdaForArrayRepresentationRec( a, bvl, 0, visited ); if( !body.isNull() ){ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 7d5cde3c2..f528ed43c 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -40,8 +40,11 @@ class TheoryBuiltinRewriter : public TheoryRewriter // conversions between lambdas and arrays private: /** recursive helper for getLambdaForArrayRepresentation */ - static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, - std::unordered_map< TNode, Node, TNodeHashFunction >& visited ); + static Node getLambdaForArrayRepresentationRec( + TNode a, + TNode bvl, + unsigned bvlIndex, + std::unordered_map<TNode, Node>& visited); /** recursive helper for getArrayRepresentationForLambda */ static Node getArrayRepresentationForLambdaRec(TNode n, TypeNode retType); diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 67a04bfea..7eea90cdc 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -32,17 +32,16 @@ namespace bv { typedef std::vector<TNode> ArgsVec; class AbstractionModule { - using NodeVecMap = - std::unordered_map<Node, std::vector<Node>, NodeHashFunction>; - using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>; - using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>; - using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>; - using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>; - using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; + using NodeVecMap = std::unordered_map<Node, std::vector<Node>>; + using NodeTNodeMap = std::unordered_map<Node, TNode>; + using TNodeTNodeMap = std::unordered_map<TNode, TNode>; + using NodeNodeMap = std::unordered_map<Node, Node>; + using TNodeNodeMap = std::unordered_map<Node, TNode>; + using TNodeSet = std::unordered_set<TNode>; using IntNodeMap = std::unordered_map<unsigned, Node>; using IndexMap = std::unordered_map<unsigned, unsigned>; using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >; - using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>; + using SignatureMap = std::unordered_map<TNode, unsigned>; struct Statistics { SizeStat<NodeNodeMap> d_numFunctionsAbstracted; @@ -77,15 +76,15 @@ class AbstractionModule { }; class ArgsTable { - std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; + std::unordered_map<TNode, ArgsTableEntry> d_data; bool hasEntry(TNode signature) const; public: - typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; - ArgsTable() {} - void addEntry(TNode signature, const ArgsVec& args); - ArgsTableEntry& getEntry(TNode signature); - iterator begin() { return d_data.begin(); } - iterator end() { return d_data.end(); } + typedef std::unordered_map<TNode, ArgsTableEntry>::iterator iterator; + ArgsTable() {} + void addEntry(TNode signature, const ArgsVec& args); + ArgsTableEntry& getEntry(TNode signature); + iterator begin() { return d_data.begin(); } + iterator end() { return d_data.end(); } }; /** diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index a7dfb00e5..39ecbc12c 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -56,8 +56,8 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> static Abc_Ntk_t* currentAigNtk(); private: - typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap; - typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap; + typedef std::unordered_map<TNode, Abc_Obj_t*> TNodeAigMap; + typedef std::unordered_map<Node, Abc_Obj_t*> NodeAigMap; static thread_local Abc_Ntk_t* s_abcAigNetwork; std::unique_ptr<context::Context> d_nullContext; diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 2a7931aa0..a669e4a86 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -38,8 +38,8 @@ namespace cvc5 { namespace theory { namespace bv { -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; -typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node> NodeSet; +typedef std::unordered_set<TNode> TNodeSet; /** * The Bitblaster that manages the mapping between Nodes @@ -52,9 +52,9 @@ class TBitblaster { protected: typedef std::vector<T> Bits; - typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache; + typedef std::unordered_map<Node, Bits> TermDefMap; + typedef std::unordered_set<TNode> TNodeSet; + typedef std::unordered_map<Node, Node> ModelCache; typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*); typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*); diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 765f3051e..9e5ace9d8 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -56,7 +56,7 @@ class EagerBitblaster : public TBitblaster<Node> private: context::Context* d_context; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode> TNodeSet; std::unique_ptr<prop::SatSolver> d_satSolver; std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar; diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 09448da8a..4d6501673 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -81,7 +81,7 @@ void BBProof::bbAtom(TNode node) { std::vector<TNode> visit; visit.push_back(node); - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; bool fproofs = options::proofGranularityMode() != options::ProofGranularityMode::OFF; diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index 6cd4960fb..ef23c05c0 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -60,7 +60,7 @@ class BBProof /** The associated term conversion proof generator. */ TConvProofGenerator* d_tcpg; /** Map bit-vector nodes to bit-blasted nodes. */ - std::unordered_map<Node, Node, NodeHashFunction> d_bbMap; + std::unordered_map<Node, Node> d_bbMap; }; } // namespace bv diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h index 04a35bc4f..ebbb2891f 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -68,7 +68,7 @@ class BBSimple : public TBitblaster<Node> /** Caches variables for which we already created bits. */ TNodeSet d_variables; /** Stores bit-blasted atoms. */ - std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms; + std::unordered_map<Node, Node> d_bbAtoms; /** Theory state. */ TheoryState* d_state; }; diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 4b6c4fc5b..ab51ea844 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -45,8 +45,8 @@ class EagerBitblastSolver { bool collectModelInfo(theory::TheoryModel* m, bool fullModel); private: - context::CDHashSet<Node, NodeHashFunction> d_assertionSet; - context::CDHashSet<Node, NodeHashFunction> d_assumptionSet; + context::CDHashSet<Node> d_assertionSet; + context::CDHashSet<Node> d_assumptionSet; context::Context* d_context; /** Bitblasters */ diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 0fa96e619..32b6dbd7a 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -99,17 +99,18 @@ class InequalityGraph : public context::ContextNotifyObj{ return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; } - }; + }; - typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; - typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap; + typedef std::unordered_map<TNode, TermId> TermNodeToIdMap; typedef std::vector<InequalityEdge> Edges; typedef std::unordered_set<TermId> TermIdSet; - typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> + BFSQueue; + typedef std::unordered_set<TNode> TNodeSet; + typedef std::unordered_set<Node> NodeSet; std::vector<InequalityNode> d_ineqNodes; std::vector< Edges > d_ineqEdges; @@ -206,7 +207,7 @@ class InequalityGraph : public context::ContextNotifyObj{ /*** The currently asserted disequalities */ context::CDQueue<TNode> d_disequalities; - typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; + typedef context::CDHashSet<Node> CDNodeSet; CDNodeSet d_disequalitiesAlreadySplit; Node makeDiseqSplitLemma(TNode diseq); /** Backtracking mechanisms **/ diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index f22f298ac..d1411d784 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -100,8 +100,7 @@ class BVQuickCheck bool collectModelValues(theory::TheoryModel* model, const std::set<Node>& termSet); - typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator - vars_iterator; + typedef std::unordered_set<TNode>::const_iterator vars_iterator; vars_iterator beginVars(); vars_iterator endVars(); diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index a9d46f068..ecf2bafb6 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -261,7 +261,7 @@ Node BVSolverBitblast::getValue(TNode node) nb << cur.getOperator(); } - std::unordered_map<Node, Node, NodeHashFunction>::iterator iit; + std::unordered_map<Node, Node>::iterator iit; for (const TNode& child : cur) { iit = d_modelCache.find(child); diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 384017f5f..36c06209a 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -87,7 +87,7 @@ class BVSolverBitblast : public BVSolver * Is cleared at the beginning of a getValue() call if the * `d_invalidateModelCache` flag is set to true. */ - std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; + std::unordered_map<Node, Node> d_modelCache; /** Bit-blaster used to bit-blast atoms/terms. */ std::unique_ptr<BBSimple> d_bitblaster; @@ -123,8 +123,7 @@ class BVSolverBitblast : public BVSolver BVProofRuleChecker d_bvProofChecker; /** Stores the SatLiteral for a given fact. */ - context::CDHashMap<Node, prop::SatLiteral, NodeHashFunction> - d_factLiteralCache; + context::CDHashMap<Node, prop::SatLiteral> d_factLiteralCache; /** Reverse map of `d_factLiteralCache`. */ context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction> diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 57b3e0a08..9b3a2f1fa 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -49,8 +49,8 @@ class BVSolverLazy : public BVSolver context::Context* d_context; /** Context dependent set of atoms we already propagated */ - context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; - context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; + context::CDHashSet<Node> d_alreadyPropagatedSet; + context::CDHashSet<Node> d_sharedTermsSet; std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories; std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>> @@ -122,11 +122,11 @@ class BVSolverLazy : public BVSolver void check(Theory::Effort e); void spendResource(Resource r); - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<TNode> TNodeSet; + typedef std::unordered_set<Node> NodeSet; NodeSet d_staticLearnCache; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; + typedef std::unordered_map<Node, Node> NodeToNode; context::CDO<bool> d_lemmasAdded; @@ -149,7 +149,7 @@ class BVSolverLazy : public BVSolver * Keeps a map from nodes to the subtheory that propagated it so that we can * explain it properly. */ - typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; + typedef context::CDHashMap<Node, SubTheory> PropagatedMap; PropagatedMap d_propagatedBy; std::unique_ptr<EagerBitblastSolver> d_eagerSolver; diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index 52f5d52ac..3faad29a9 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -38,10 +38,10 @@ bool isBVAtom(TNode n) } /* Traverse Boolean nodes and collect BV atoms. */ -void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms) +void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms) { std::vector<TNode> visit; - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; visit.push_back(n); @@ -138,7 +138,7 @@ bool BVSolverSimple::preNotifyFact( d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA); } - std::unordered_set<Node, NodeHashFunction> bv_atoms; + std::unordered_set<Node> bv_atoms; collectBVAtoms(n, bv_atoms); for (const Node& nn : bv_atoms) { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 90276f8b1..3a9e460fe 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -47,7 +47,7 @@ namespace { void collectVariables(TNode node, utils::NodeSet& vars) { std::vector<TNode> stack; - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; stack.push_back(node); while (!stack.empty()) diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 670adafa3..b93ff235f 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -58,10 +58,8 @@ class SubstitutionEx } }; - typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> - Substitutions; - typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> - SubstitutionsCache; + typedef std::unordered_map<Node, SubstitutionElement> Substitutions; + typedef std::unordered_map<Node, SubstitutionElement> SubstitutionsCache; Substitutions d_substitutions; SubstitutionsCache d_cache; @@ -103,9 +101,9 @@ struct WorklistElement WorklistElement() : node(), id(-1) {} }; -typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; -typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap; -typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_map<Node, Node> NodeNodeMap; +typedef std::unordered_map<Node, unsigned> NodeIdMap; +typedef std::unordered_set<TNode> TNodeSet; class ExtractSkolemizer { @@ -124,7 +122,7 @@ class ExtractSkolemizer ExtractList() : base(1), extracts() {} void addExtract(Extract& e); }; - typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap; + typedef std::unordered_map<Node, ExtractList> VarExtractMap; context::Context d_emptyContext; VarExtractMap d_varToExtract; theory::SubstitutionMap* d_modelMap; diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 903a5136e..439bd33ed 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -49,7 +49,7 @@ class BitblastSolver : public SubtheorySolver context::CDQueue<TNode> d_bitblastQueue; Statistics d_statistics; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node> NodeMap; NodeMap d_modelCache; context::CDO<bool> d_validModelCache; diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 52d9e739a..0dfcfdde4 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -50,10 +50,9 @@ class CoreSolverExtTheoryCallback : public ExtTheoryCallback * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { - typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue; - typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - + typedef std::unordered_map<TNode, Node> ModelValue; + typedef std::unordered_map<TNode, bool> TNodeBoolMap; + typedef std::unordered_set<TNode> TNodeSet; struct Statistics { IntStat d_numCallstoCheck; @@ -103,7 +102,7 @@ class CoreSolver : public SubtheorySolver { std::unique_ptr<ExtTheory> d_extTheory; /** To make sure we keep the explanations */ - context::CDHashSet<Node, NodeHashFunction> d_reasons; + context::CDHashSet<Node> d_reasons; ModelValue d_modelValues; void buildModel(); bool assertFactToEqualityEngine(TNode fact, TNode reason); @@ -113,8 +112,8 @@ class CoreSolver : public SubtheorySolver { /** Whether we need a last call effort check */ bool d_needsLastCallCheck; /** For extended functions */ - context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer; - context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer; + context::CDHashSet<Node> d_extf_range_infer; + context::CDHashSet<Node> d_extf_collapse_infer; /** do extended function inferences * diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 65eee95e1..f8a7bf113 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -51,11 +51,11 @@ class InequalitySolver : public SubtheorySolver Statistics(); }; - context::CDHashSet<Node, NodeHashFunction> d_assertionSet; + context::CDHashSet<Node> d_assertionSet; InequalityGraph d_inequalityGraph; - context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; + context::CDHashMap<Node, TNode> d_explanations; context::CDO<bool> d_isComplete; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node> NodeSet; NodeSet d_ineqTerms; bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index 7fb463721..f8717e045 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -87,7 +87,7 @@ namespace cvc5 { **/ class IntBlaster { - using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>; + using CDNodeMap = context::CDHashMap<Node, Node>; public: /** @@ -319,13 +319,13 @@ class IntBlaster * Range constraints of the form 0 <= x < 2^k * These are added for every new integer variable that we introduce. */ - context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions; + context::CDHashSet<Node> d_rangeAssertions; /** * A set of "bitwise" equalities over integers for BITVECTOR_AND * used in for options::SolveBVAsIntMode::BITWISE */ - context::CDHashSet<Node, NodeHashFunction> d_bitwiseAssertions; + context::CDHashSet<Node> d_bitwiseAssertions; /** Useful constants */ Node d_zero; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 63d618da2..4a2d2943d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1047,7 +1047,10 @@ struct Count { {} }; -inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { +inline static void insert(std::unordered_map<TNode, Count>& map, + TNode node, + bool neg) +{ if(map.find(node) == map.end()) { Count c = neg? Count(0,1) : Count(1, 0); map[node] = c; @@ -1073,7 +1076,7 @@ inline Node RewriteRule<AndSimplify>::apply(TNode node) NodeManager *nm = NodeManager::currentNM(); // this will remove duplicates - std::unordered_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count> subterms; unsigned size = utils::getSize(node); BitVector constant = BitVector::mkOnes(size); for (unsigned i = 0; i < node.getNumChildren(); ++i) @@ -1110,8 +1113,7 @@ inline Node RewriteRule<AndSimplify>::apply(TNode node) children.push_back(utils::mkConst(constant)); } - std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = - subterms.begin(); + std::unordered_map<TNode, Count>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { @@ -1163,7 +1165,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; std::vector<Node> processingStack; processingStack.push_back(node); - std::unordered_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode> processed; std::vector<Node> children; Kind kind = node.getKind(); @@ -1200,7 +1202,7 @@ inline Node RewriteRule<OrSimplify>::apply(TNode node) NodeManager *nm = NodeManager::currentNM(); // this will remove duplicates - std::unordered_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count> subterms; unsigned size = utils::getSize(node); BitVector constant(size, (unsigned)0); @@ -1238,8 +1240,7 @@ inline Node RewriteRule<OrSimplify>::apply(TNode node) children.push_back(utils::mkConst(constant)); } - std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = - subterms.begin(); + std::unordered_map<TNode, Count>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { @@ -1283,7 +1284,7 @@ inline Node RewriteRule<XorSimplify>::apply(TNode node) << std::endl; NodeManager *nm = NodeManager::currentNM(); - std::unordered_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count> subterms; unsigned size = utils::getSize(node); BitVector constant; bool const_set = false; @@ -1321,8 +1322,7 @@ inline Node RewriteRule<XorSimplify>::apply(TNode node) std::vector<Node> children; - std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = - subterms.begin(); + std::unordered_map<TNode, Count>::const_iterator it = subterms.begin(); unsigned true_count = 0; bool seen_false = false; for (; it != subterms.end(); ++it) diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index eb2fd6527..1549df639 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -140,7 +140,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache) TNode t = term.getKind() == kind::NOT ? term[0] : term; std::vector<TNode> stack; - std::unordered_map<TNode, bool, TNodeHashFunction> visited; + std::unordered_map<TNode, bool> visited; stack.push_back(t); while (!stack.empty()) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 4844c1a93..8e916e975 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -28,13 +28,13 @@ namespace cvc5 { namespace theory { namespace bv { -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; -typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node> NodeSet; +typedef std::unordered_set<TNode> TNodeSet; namespace utils { -typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_map<TNode, bool> TNodeBoolMap; +typedef std::unordered_set<Node> NodeSet; /* Get the bit-width of given node. */ unsigned getSize(TNode node); diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index 9e6b6d339..f8e7eea09 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -42,9 +42,8 @@ namespace datatypes { */ class InferProofCons : public ProofGenerator { - typedef context:: - CDHashMap<Node, std::shared_ptr<DatatypesInference>, NodeHashFunction> - NodeDatatypesInferenceMap; + typedef context::CDHashMap<Node, std::shared_ptr<DatatypesInference>> + NodeDatatypesInferenceMap; public: InferProofCons(context::Context* c, ProofNodeManager* pnm); diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 4b0c17bee..7e5099d55 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -60,7 +60,7 @@ Node applySygusArgs(const DType& dt, TNode val; if (!op.hasAttribute(SygusVarFreeAttribute())) { - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; if (expr::getFreeVariables(op, fvs)) { if (fvs.size() == 1) @@ -294,8 +294,8 @@ typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node> Node sygusToBuiltin(Node n, bool isExternal) { - 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; unsigned index; @@ -410,8 +410,8 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args) std::vector<Node> eargs; bool svarsInit = false; std::vector<Node> svars; - 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; unsigned index; @@ -521,8 +521,7 @@ Node builtinVarToSygus(Node v) return Node::null(); } -void getFreeSymbolsSygusType(TypeNode sdt, - std::unordered_set<Node, NodeHashFunction>& syms) +void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms) { // datatype types we need to process std::vector<TypeNode> typeToProcess; diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 63e8a057a..6f3791a4d 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -197,8 +197,7 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args); * We have that { a, b, c, e } are added to syms. Notice that expr::getSymbols * excludes variables whose kind is BOUND_VARIABLE. */ -void getFreeSymbolsSygusType(TypeNode sdt, - std::unordered_set<Node, NodeHashFunction>& syms); +void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms); /** Substitute and generalize a sygus datatype type * diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index d4dbdf82d..45d996b55 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -156,8 +156,7 @@ void SygusExtension::registerTerm(Node n) bool success = false; if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ registerTerm(n[0]); - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = - d_term_to_anchor.find(n[0]); + std::unordered_map<Node, Node>::iterator it = d_term_to_anchor.find(n[0]); if( it!=d_term_to_anchor.end() ) { d_term_to_anchor[n] = it->second; unsigned sel_weight = @@ -333,7 +332,7 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp) } // add the above symmetry breaking predicates to lemmas - std::unordered_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode> cache; Node rlv = getRelevancyCondition(n); for (std::pair<Node, InferenceId>& sbl : sbLemmas) { @@ -450,8 +449,8 @@ Node SygusExtension::eliminateTraversalPredicates(Node n) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - 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>::iterator ittb; std::vector<TNode> visit; TNode cur; @@ -948,8 +947,7 @@ void SygusExtension::registerSearchTerm(TypeNode tn, bool topLevel) { //register this term - std::unordered_map<Node, Node, NodeHashFunction>::iterator ita = - d_term_to_anchor.find(n); + std::unordered_map<Node, Node>::iterator ita = d_term_to_anchor.find(n); Assert(ita != d_term_to_anchor.end()); Node a = ita->second; Assert(!a.isNull()); @@ -1050,12 +1048,9 @@ Node SygusExtension::registerSearchValue(Node a, registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), var_count); return Node::null(); }else{ - std::unordered_map<Node, Node, NodeHashFunction>& scasv = - sca.d_search_val[tn]; - std::unordered_map<Node, unsigned, NodeHashFunction>& scasvs = - sca.d_search_val_sz[tn]; - std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv = - scasv.find(bvr); + std::unordered_map<Node, Node>& scasv = sca.d_search_val[tn]; + std::unordered_map<Node, unsigned>& scasvs = sca.d_search_val_sz[tn]; + std::unordered_map<Node, Node>::iterator itsv = scasv.find(bvr); Node bad_val_bvr; bool by_examples = false; if (itsv == scasv.end()) @@ -1264,7 +1259,7 @@ void SygusExtension::addSymBreakLemmasFor(TypeNode tn, Trace("sygus-sb-debug2") << "add lemmas up to size " << max_sz << ", which is (search_size) " << csz << " - (depth) " << d << std::endl; - std::unordered_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode> cache; for (std::pair<const uint64_t, std::vector<Node>>& sbls : its->second) { if (sbls.first <= max_sz) @@ -1443,8 +1438,7 @@ void SygusExtension::notifySearchSize(TNode m, uint64_t s, Node exp) unsigned SygusExtension::getSearchSizeFor( Node n ) { Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl; - std::unordered_map<Node, Node, NodeHashFunction>::iterator ita = - d_term_to_anchor.find(n); + std::unordered_map<Node, Node>::iterator ita = d_term_to_anchor.find(n); Assert(ita != d_term_to_anchor.end()); return getSearchSizeForAnchor( ita->second ); } @@ -1497,7 +1491,7 @@ void SygusExtension::incrementCurrentSearchSize(TNode m) && !s.second.empty())) { Node rlv = getRelevancyCondition(t); - std::unordered_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode> cache; for (const Node& lem : s.second) { Node slem = lem.substitute(x, t, cache); diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h index 25f56b334..3c7607eaf 100644 --- a/src/theory/datatypes/sygus_extension.h +++ b/src/theory/datatypes/sygus_extension.h @@ -64,10 +64,10 @@ class InferenceManager; */ class SygusExtension { - typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; - typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, int> IntMap; + typedef context::CDHashMap<Node, Node> NodeMap; + typedef context::CDHashMap<Node, bool> BoolMap; + typedef context::CDHashSet<Node> NodeSet; public: SygusExtension(TheoryState& s, @@ -149,7 +149,7 @@ class SygusExtension * Map from terms (selector chains) to their anchors. The anchor of a * selector chain S1( ... Sn( x ) ... ) is x. */ - std::unordered_map<Node, Node, NodeHashFunction> d_term_to_anchor; + std::unordered_map<Node, Node> d_term_to_anchor; /** * Map from anchors to the conjecture they are associated with. */ @@ -161,7 +161,7 @@ class SygusExtension * where weight is the selector weight of Si * (see SygusTermDatabase::getSelectorWeight). */ - std::unordered_map<Node, unsigned, NodeHashFunction> d_term_to_depth; + std::unordered_map<Node, unsigned> d_term_to_depth; /** * Map from terms (selector chains) to whether they are the topmost term * of their type. For example, if: @@ -172,7 +172,7 @@ class SygusExtension * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms, * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. */ - std::unordered_map<Node, bool, NodeHashFunction> d_is_top_level; + std::unordered_map<Node, bool> d_is_top_level; /** * Returns true if the selector chain n is top-level based on the above * definition, when tn is the type of n. @@ -198,13 +198,11 @@ private: * term. The range of this map can be updated if we later encounter a sygus * term that also rewrites to the builtin value but has a smaller term size. */ - std::map<TypeNode, std::unordered_map<Node, Node, NodeHashFunction>> - d_search_val; + std::map<TypeNode, std::unordered_map<Node, Node>> d_search_val; /** the size of terms in the range of d_search val. */ - std::map<TypeNode, std::unordered_map<Node, unsigned, NodeHashFunction>> - d_search_val_sz; + std::map<TypeNode, std::unordered_map<Node, unsigned>> d_search_val_sz; /** For each term, whether this cache has processed that term */ - std::unordered_set<Node, NodeHashFunction> d_search_val_proc; + std::unordered_set<Node> d_search_val_proc; }; /** An instance of the above cache, for each anchor */ std::map< Node, SearchCache > d_cache; @@ -513,7 +511,7 @@ private: * This should be user context-dependent if sygus is updated to work in * incremental mode. */ - std::unordered_map<Node, unsigned, NodeHashFunction> d_simple_proc; + std::unordered_map<Node, unsigned> d_simple_proc; //------------------------end static symmetry breaking /** Get the canonical free variable for type tn */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 1ae122f5e..951aea804 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -42,9 +42,9 @@ class TheoryDatatypes : public Theory { private: typedef context::CDList<Node> NodeList; /** maps nodes to an index in a vector */ - typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap; - typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDHashMap<Node, size_t> NodeUIntMap; + typedef context::CDHashMap<Node, bool> BoolMap; + typedef context::CDHashMap<Node, Node> NodeMap; private: //notification class for equality engine diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index c9bfd98df..df644e9b2 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -420,7 +420,7 @@ TypeNode MatchTypeRule::computeType(NodeManager* nodeManager, if (check) { Kind nck = nc.getKind(); - std::unordered_set<Node, NodeHashFunction> bvs; + std::unordered_set<Node> bvs; if (nck == kind::MATCH_BIND_CASE) { for (const Node& v : nc[0]) diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 3a9ddd9d6..1606fbb50 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -87,8 +87,7 @@ namespace theory { */ class EagerProofGenerator : public ProofGenerator { - typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction> - NodeProofNodeMap; + typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap; public: EagerProofGenerator(ProofNodeManager* pnm, diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 90ab5c4f0..c0a3a2a2f 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -132,21 +132,20 @@ Node Evaluator::eval(TNode n, const std::vector<Node>& vals, bool useRewriter) const { - std::unordered_map<Node, Node, NodeHashFunction> visited; + std::unordered_map<Node, Node> visited; return eval(n, args, vals, visited, useRewriter); } -Node Evaluator::eval( - TNode n, - const std::vector<Node>& args, - const std::vector<Node>& vals, - const std::unordered_map<Node, Node, NodeHashFunction>& visited, - bool useRewriter) const +Node Evaluator::eval(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals, + const std::unordered_map<Node, Node>& visited, + bool useRewriter) const { Trace("evaluator") << "Evaluating " << n << " under substitution " << args << " " << vals << " with visited size = " << visited.size() << std::endl; - std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode; - std::unordered_map<TNode, EvalResult, TNodeHashFunction> results; + std::unordered_map<TNode, Node> evalAsNode; + std::unordered_map<TNode, EvalResult> results; // add visited to results for (const std::pair<const Node, Node>& p : visited) { @@ -155,8 +154,7 @@ Node Evaluator::eval( if (results[p.first].d_tag == EvalResult::INVALID) { // could not evaluate, use the evalAsNode map - std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn = - evalAsNode.find(p.second); + std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(p.second); Assert(itn != evalAsNode.end()); Node val = itn->second; if (useRewriter) @@ -172,8 +170,7 @@ Node Evaluator::eval( if (ret.isNull() && useRewriter) { // should be stored in the evaluation-as-node map - std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn = - evalAsNode.find(n); + std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n); Assert(itn != evalAsNode.end()); ret = Rewriter::rewrite(itn->second); } @@ -190,13 +187,13 @@ EvalResult Evaluator::evalInternal( TNode n, const std::vector<Node>& args, const std::vector<Node>& vals, - std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode, - std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results, + std::unordered_map<TNode, Node>& evalAsNode, + std::unordered_map<TNode, EvalResult>& results, bool useRewriter) const { std::vector<TNode> queue; queue.emplace_back(n); - std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr; + std::unordered_map<TNode, EvalResult>::iterator itr; while (queue.size() != 0) { @@ -361,8 +358,8 @@ EvalResult Evaluator::evalInternal( // since the evaluation of op[1] is under a new substitution and thus // should not be cached. We could alternatively copy evalAsNode to // evalAsNodeC but favor avoiding this copy for performance reasons. - std::unordered_map<TNode, Node, NodeHashFunction> evalAsNodeC; - std::unordered_map<TNode, EvalResult, TNodeHashFunction> resultsC; + std::unordered_map<TNode, Node> evalAsNodeC; + std::unordered_map<TNode, EvalResult> resultsC; results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals, @@ -885,10 +882,9 @@ EvalResult Evaluator::evalInternal( return results[n]; } -Node Evaluator::reconstruct( - TNode n, - std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults, - std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const +Node Evaluator::reconstruct(TNode n, + std::unordered_map<TNode, EvalResult>& eresults, + std::unordered_map<TNode, Node>& evalAsNode) const { if (n.getNumChildren() == 0) { @@ -896,8 +892,8 @@ Node Evaluator::reconstruct( } Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); - std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr; - std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn; + std::unordered_map<TNode, EvalResult>::iterator itr; + std::unordered_map<TNode, Node>::iterator itn; std::vector<Node> echildren; if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 211b3060d..42cc34749 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -117,7 +117,7 @@ class Evaluator Node eval(TNode n, const std::vector<Node>& args, const std::vector<Node>& vals, - const std::unordered_map<Node, Node, NodeHashFunction>& visited, + const std::unordered_map<Node, Node>& visited, bool useRewriter = true) const; private: @@ -137,13 +137,12 @@ class Evaluator * `args` to `vals` and rewriting. Notice that this map contains an entry * for n in the case that it cannot be evaluated. */ - EvalResult evalInternal( - TNode n, - const std::vector<Node>& args, - const std::vector<Node>& vals, - std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode, - std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results, - bool useRewriter) const; + EvalResult evalInternal(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals, + std::unordered_map<TNode, Node>& evalAsNode, + std::unordered_map<TNode, EvalResult>& results, + bool useRewriter) const; /** reconstruct * * This function reconstructs the result of evaluating n using a combination @@ -153,10 +152,9 @@ class Evaluator * above method for some args and vals. This method ensures that the return * value is equivalent to the rewritten form of n * { args -> vals }. */ - Node reconstruct( - TNode n, - std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults, - std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const; + Node reconstruct(TNode n, + std::unordered_map<TNode, EvalResult>& eresults, + std::unordered_map<TNode, Node>& evalAsNode) const; }; } // namespace theory diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index 425c6fe6c..f5e08e2f5 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -164,10 +164,9 @@ class ExtTheoryCallback */ class ExtTheory { - using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>; - using NodeExtReducedIdMap = - context::CDHashMap<Node, ExtReducedId, NodeHashFunction>; - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + using NodeBoolMap = context::CDHashMap<Node, bool>; + using NodeExtReducedIdMap = context::CDHashMap<Node, ExtReducedId>; + using NodeSet = context::CDHashSet<Node>; public: /** constructor diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 1db635cda..f1b7c8a83 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -323,11 +323,11 @@ class FpConverter typedef symfpuSymbolic::traits::ubv ubv; typedef symfpuSymbolic::traits::sbv sbv; - typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap; - typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap; - typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap; - typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap; - typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap; + typedef context::CDHashMap<Node, uf> fpMap; + typedef context::CDHashMap<Node, rm> rmMap; + typedef context::CDHashMap<Node, prop> boolMap; + typedef context::CDHashMap<Node, ubv> ubvMap; + typedef context::CDHashMap<Node, sbv> sbvMap; fpMap d_fpMap; rmMap d_rmMap; diff --git a/src/theory/fp/fp_expand_defs.h b/src/theory/fp/fp_expand_defs.h index 674d79331..a9edc8b02 100644 --- a/src/theory/fp/fp_expand_defs.h +++ b/src/theory/fp/fp_expand_defs.h @@ -33,11 +33,10 @@ class FpExpandDefs { using PairTypeNodeHashFunction = PairHashFunction<TypeNode, TypeNode, - TypeNodeHashFunction, - TypeNodeHashFunction>; + std::hash<TypeNode>, + std::hash<TypeNode>>; /** Uninterpreted functions for undefined cases of non-total operators. */ - using ComparisonUFMap = - context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>; + using ComparisonUFMap = context::CDHashMap<TypeNode, Node>; /** Uninterpreted functions for lazy handling of conversions. */ using ConversionUFMap = context:: CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 01dace411..21f2975a8 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -804,7 +804,7 @@ bool TheoryFp::collectModelValues(TheoryModel* m, } } - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; std::stack<TNode> working; std::set<TNode> relevantVariables; for (std::set<Node>::const_iterator i(relevantTerms.begin()); diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 8cf4c4cc5..a41bf342c 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -92,9 +92,8 @@ class TheoryFp : public Theory TrustNode explain(TNode n) override; protected: - using ConversionAbstractionMap = - context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>; - using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>; + using ConversionAbstractionMap = context::CDHashMap<TypeNode, Node>; + using AbstractionMap = context::CDHashMap<Node, Node>; /** Equality engine. */ class NotifyClass : public eq::EqualityEngineNotify { @@ -121,7 +120,7 @@ class TheoryFp : public Theory void registerTerm(TNode node); bool isRegistered(TNode node); - context::CDHashSet<Node, NodeHashFunction> d_registeredTerms; + context::CDHashSet<Node> d_registeredTerms; /** The word-blaster. Translates FP -> BV. */ std::unique_ptr<FpConverter> d_conv; 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); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 631f7bec1..fc29ab8e8 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -54,8 +54,8 @@ class TermRegistry; // TODO: organize this more/review this, github issue #1163 class QuantifiersEngine { friend class ::cvc5::TheoryEngine; - typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, bool> BoolMap; + typedef context::CDHashSet<Node> NodeSet; public: QuantifiersEngine(quantifiers::QuantifiersState& qstate, diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index 68ec573c3..9746f4a22 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -92,7 +92,7 @@ void RelevanceManager::computeRelevance() d_computed = true; d_rset.clear(); Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl; - std::unordered_map<TNode, int, TNodeHashFunction> cache; + std::unordered_map<TNode, int> cache; for (const Node& node: d_input) { TNode n = node; @@ -123,7 +123,7 @@ bool RelevanceManager::isBooleanConnective(TNode cur) bool RelevanceManager::updateJustifyLastChild( TNode cur, std::vector<int>& childrenJustify, - std::unordered_map<TNode, int, TNodeHashFunction>& cache) + std::unordered_map<TNode, int>& cache) { // This method is run when we are informed that child index of cur // has justify status lastChildJustify. We return true if we would like to @@ -226,13 +226,12 @@ bool RelevanceManager::updateJustifyLastChild( return false; } -int RelevanceManager::justify( - TNode n, std::unordered_map<TNode, int, TNodeHashFunction>& cache) +int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache) { // the vector of values of children - std::unordered_map<TNode, std::vector<int>, TNodeHashFunction> childJustify; - std::unordered_map<TNode, int, TNodeHashFunction>::iterator it; - std::unordered_map<TNode, std::vector<int>, TNodeHashFunction>::iterator itc; + std::unordered_map<TNode, std::vector<int>> childJustify; + std::unordered_map<TNode, int>::iterator it; + std::unordered_map<TNode, std::vector<int>>::iterator itc; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -315,8 +314,8 @@ bool RelevanceManager::isRelevant(Node lit) return d_rset.find(lit) != d_rset.end(); } -const std::unordered_set<TNode, TNodeHashFunction>& -RelevanceManager::getRelevantAssertions(bool& success) +const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions( + bool& success) { if (!d_computed) { diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index dc717157b..6c69861fd 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -104,8 +104,7 @@ class RelevanceManager * * The value of this return is only valid if success was not updated to false. */ - const std::unordered_set<TNode, TNodeHashFunction>& getRelevantAssertions( - bool& success); + const std::unordered_set<TNode>& getRelevantAssertions(bool& success); private: /** @@ -124,8 +123,7 @@ class RelevanceManager * This method returns 1 if we justified n to be true, -1 means * justified n to be false, 0 means n could not be justified. */ - int justify(TNode n, - std::unordered_map<TNode, int, TNodeHashFunction>& cache); + int justify(TNode n, std::unordered_map<TNode, int>& cache); /** Is the top symbol of cur a Boolean connective? */ bool isBooleanConnective(TNode cur); /** @@ -140,16 +138,15 @@ class RelevanceManager * @return True if we wish to visit the next child. If this is the case, then * the justify value of the current child is added to childrenJustify. */ - bool updateJustifyLastChild( - TNode cur, - std::vector<int>& childrenJustify, - std::unordered_map<TNode, int, TNodeHashFunction>& cache); + bool updateJustifyLastChild(TNode cur, + std::vector<int>& childrenJustify, + std::unordered_map<TNode, int>& cache); /** The valuation object, used to query current value of theory literals */ Valuation d_val; /** The input assertions */ NodeList d_input; /** The current relevant selection. */ - std::unordered_set<TNode, TNodeHashFunction> d_rset; + std::unordered_set<TNode> d_rset; /** Have we computed the relevant selection this round? */ bool d_computed; /** diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index f44b269cf..d0eee1886 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -69,7 +69,7 @@ const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const namespace { -bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache) +bool containsStoreAll(Node n, std::unordered_set<Node>& cache) { if( std::find( cache.begin(), cache.end(), n )==cache.end() ){ cache.insert(n); @@ -91,7 +91,7 @@ bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache) void RepSet::add( TypeNode tn, Node n ){ //for now, do not add array constants FIXME if( tn.isArray() ){ - std::unordered_set<Node, NodeHashFunction> cache; + std::unordered_set<Node> cache; if( containsStoreAll( n, cache ) ){ return; } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 2b2604593..1094d5920 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -199,7 +199,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, if (d_rewriteStack == nullptr) { - d_rewriteStack.reset(new std::unordered_set<Node, NodeHashFunction>()); + d_rewriteStack.reset(new std::unordered_set<Node>()); } #endif diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index b3ea3b542..1fc685992 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -228,8 +228,7 @@ class Rewriter { /** The proof generator */ std::unique_ptr<TConvProofGenerator> d_tpg; #ifdef CVC5_ASSERTIONS - std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack = - nullptr; + std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr; #endif /* CVC5_ASSERTIONS */ };/* class Rewriter */ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 3b8ec8b6b..b028f0686 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -39,8 +39,8 @@ namespace sep { class TheorySep : public Theory { typedef context::CDList<Node> NodeList; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashMap<Node, Node> NodeNodeMap; ///////////////////////////////////////////////////////////////////////////// // MISC diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index cd4ba5de0..ce2f29bd5 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -62,7 +62,7 @@ namespace sets { */ class CardinalityExtension { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: /** diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index bcb38ff5c..7a64b10c7 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -36,7 +36,7 @@ class TheorySetsPrivate; */ class InferenceManager : public InferenceManagerBuffered { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp index 993457fe8..06d144f72 100644 --- a/src/theory/sets/singleton_op.cpp +++ b/src/theory/sets/singleton_op.cpp @@ -28,7 +28,7 @@ std::ostream& operator<<(std::ostream& out, const SingletonOp& op) size_t SingletonOpHashFunction::operator()(const SingletonOp& op) const { - return TypeNodeHashFunction()(op.getType()); + return std::hash<TypeNode>()(op.getType()); } SingletonOp::SingletonOp(const TypeNode& elementType) diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h index a41886f9d..62547a66e 100644 --- a/src/theory/sets/skolem_cache.h +++ b/src/theory/sets/skolem_cache.h @@ -74,7 +74,7 @@ class SkolemCache /** map from node pairs and identifiers to skolems */ std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; /** the set of all skolems we have generated */ - std::unordered_set<Node, NodeHashFunction> d_allSkolems; + std::unordered_set<Node> d_allSkolems; }; } // namespace sets diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 94e06971c..63039eddd 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -43,7 +43,7 @@ class TheorySetsPrivate; */ class SolverState : public TheoryState { - typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, size_t> NodeIntMap; public: SolverState(context::Context* c, diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index f98f204e0..87f25341e 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -37,7 +37,7 @@ namespace sets { */ class TermRegistry { - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDHashMap<Node, Node> NodeMap; public: TermRegistry(SolverState& state, diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 952bfd83b..3b5ee2390 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -38,8 +38,8 @@ namespace sets { class TheorySets; class TheorySetsPrivate { - typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, bool> NodeBoolMap; + typedef context::CDHashSet<Node> NodeSet; public: void eqNotifyNewClass(TNode t); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 0e14a6c34..74dfc01ba 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -28,9 +28,10 @@ namespace sets { typedef std::map< Node, std::vector< Node > >::iterator MEM_IT; typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT; -typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; +typedef std::map<Node, std::unordered_set<Node> >::iterator TC_GRAPH_IT; typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; -typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; +typedef std::map<Node, std::map<Node, std::unordered_set<Node> > >::iterator + TC_IT; TheorySetsRels::TheorySetsRels(SolverState& s, InferenceManager& im, @@ -281,7 +282,7 @@ void TheorySetsRels::check(Theory::Effort level) NodeManager* nm = NodeManager::currentNM(); Node join_image_rel = join_image_term[0]; - std::unordered_set< Node, NodeHashFunction > hasChecked; + std::unordered_set<Node> hasChecked; Node join_image_rel_rep = getRepresentative( join_image_rel ); std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin(); MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep ); @@ -544,14 +545,14 @@ void TheorySetsRels::check(Theory::Effort level) if( tc_graph_it != (tc_it->second).end() ) { (tc_graph_it->second).insert( mem_rep_snd ); } else { - std::unordered_set< Node, NodeHashFunction > sets; + std::unordered_set<Node> sets; sets.insert( mem_rep_snd ); (tc_it->second)[mem_rep_fst] = sets; } } else { std::map< Node, Node > exp_map; - std::unordered_set< Node, NodeHashFunction > sets; - std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map; + std::unordered_set<Node> sets; + std::map<Node, std::unordered_set<Node> > element_map; sets.insert( mem_rep_snd ); element_map[mem_rep_fst] = sets; d_tcr_tcGraph[tc_rel] = element_map; @@ -609,7 +610,7 @@ void TheorySetsRels::check(Theory::Effort level) TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) ); if( tc_it != d_rRep_tcGraph.end() ) { bool isReachable = false; - std::unordered_set<Node, NodeHashFunction> seen; + std::unordered_set<Node> seen; isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ), getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable ); return isReachable; @@ -617,8 +618,13 @@ void TheorySetsRels::check(Theory::Effort level) return false; } - void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { + void TheorySetsRels::isTCReachable( + Node start, + Node dest, + std::unordered_set<Node>& hasSeen, + std::map<Node, std::unordered_set<Node> >& tc_graph, + bool& isReachable) + { if(hasSeen.find(start) == hasSeen.end()) { hasSeen.insert(start); } @@ -630,7 +636,7 @@ void TheorySetsRels::check(Theory::Effort level) isReachable = true; return; } else { - std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + std::unordered_set<Node>::iterator set_it = pair_set_it->second.begin(); while( set_it != pair_set_it->second.end() ) { // need to check if *set_it has been looked already @@ -645,7 +651,7 @@ void TheorySetsRels::check(Theory::Effort level) void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) { std::map< Node, Node > rel_tc_graph_exps; - std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph; + std::map<Node, std::unordered_set<Node> > rel_tc_graph; Node rel_rep = getRepresentative( tc_rel[0] ); Node tc_rel_rep = getRepresentative( tc_rel ); @@ -656,10 +662,11 @@ void TheorySetsRels::check(Theory::Effort level) Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 )); Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 )); Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep ); - std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); + std::map<Node, std::unordered_set<Node> >::iterator rel_tc_graph_it = + rel_tc_graph.find(fst_element_rep); if( rel_tc_graph_it == rel_tc_graph.end() ) { - std::unordered_set< Node, NodeHashFunction > snd_elements; + std::unordered_set<Node> snd_elements; snd_elements.insert( snd_element_rep ); rel_tc_graph[fst_element_rep] = snd_elements; rel_tc_graph_exps[tuple_rep] = exps[i]; @@ -676,19 +683,23 @@ void TheorySetsRels::check(Theory::Effort level) } } - void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { + void TheorySetsRels::doTCInference( + std::map<Node, std::unordered_set<Node> > rel_tc_graph, + std::map<Node, Node> rel_tc_graph_exps, + Node tc_rel) + { Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl; for (TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); ++tc_graph_it) { - for (std::unordered_set<Node, NodeHashFunction>::iterator - snd_elements_it = tc_graph_it->second.begin(); + for (std::unordered_set<Node>::iterator snd_elements_it = + tc_graph_it->second.begin(); snd_elements_it != tc_graph_it->second.end(); ++snd_elements_it) { std::vector< Node > reasons; - std::unordered_set<Node, NodeHashFunction> seen; + std::unordered_set<Node> seen; Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) ); Assert(rel_tc_graph_exps.find(tuple) != rel_tc_graph_exps.end()); Node exp = rel_tc_graph_exps.find( tuple )->second; @@ -701,8 +712,15 @@ void TheorySetsRels::check(Theory::Effort level) Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl; } - void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) { + void TheorySetsRels::doTCInference( + Node tc_rel, + std::vector<Node> reasons, + std::map<Node, std::unordered_set<Node> >& tc_graph, + std::map<Node, Node>& rel_tc_graph_exps, + Node start_node_rep, + Node cur_node_rep, + std::unordered_set<Node>& seen) + { NodeManager* nm = NodeManager::currentNM(); Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) ); std::vector< Node > all_reasons( reasons ); @@ -737,8 +755,7 @@ void TheorySetsRels::check(Theory::Effort level) seen.insert( cur_node_rep ); TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep ); if( cur_set != tc_graph.end() ) { - for (std::unordered_set<Node, NodeHashFunction>::iterator set_it = - cur_set->second.begin(); + for (std::unordered_set<Node>::iterator set_it = cur_set->second.begin(); set_it != cur_set->second.end(); ++set_it) { diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 2ca8696b0..c30322d07 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -61,27 +61,27 @@ public: */ class TheorySetsRels { typedef context::CDList<Node> NodeList; - typedef context::CDHashSet< Node, NodeHashFunction > NodeSet; - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashMap<Node, Node> NodeMap; -public: - TheorySetsRels(SolverState& s, - InferenceManager& im, - SkolemCache& skc, - TermRegistry& treg); - - ~TheorySetsRels(); - /** - * Invoke the check method with effort level e. At a high level, this class - * will make calls to TheorySetsPrivate::processInference to assert facts, - * lemmas, and conflicts. If this class makes no such call, then the current - * set of assertions is satisfiable with respect to relations. - */ - void check(Theory::Effort e); - /** Is kind k a kind that belongs to the relation theory? */ - static bool isRelationKind(Kind k); - -private: + public: + TheorySetsRels(SolverState& s, + InferenceManager& im, + SkolemCache& skc, + TermRegistry& treg); + + ~TheorySetsRels(); + /** + * Invoke the check method with effort level e. At a high level, this class + * will make calls to TheorySetsPrivate::processInference to assert facts, + * lemmas, and conflicts. If this class makes no such call, then the current + * set of assertions is satisfiable with respect to relations. + */ + void check(Theory::Effort e); + /** Is kind k a kind that belongs to the relation theory? */ + static bool isRelationKind(Kind k); + + private: /** True and false constant nodes */ Node d_trueNode; Node d_falseNode; @@ -98,13 +98,12 @@ private: std::vector<Node> d_pending; NodeSet d_shared_terms; - - std::unordered_set< Node, NodeHashFunction > d_rel_nodes; + std::unordered_set<Node> d_rel_nodes; std::map< Node, std::vector<Node> > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; /** Symbolic tuple variables that has been reduced to concrete ones */ - std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples; + std::unordered_set<Node> d_symbolic_tuples; /** Mapping between relation and its member representatives */ std::map< Node, std::vector< Node > > d_rReps_memberReps_cache; @@ -116,8 +115,8 @@ private: std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph; - std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph; + std::map<Node, std::map<Node, std::unordered_set<Node> > > d_rRep_tcGraph; + std::map<Node, std::map<Node, std::unordered_set<Node> > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; private: @@ -154,9 +153,16 @@ private: void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); void buildTCGraphForRel( Node tc_rel ); void doTCInference(); - void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); - void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ); + void doTCInference(std::map<Node, std::unordered_set<Node> > rel_tc_graph, + std::map<Node, Node> rel_tc_graph_exps, + Node tc_rel); + void doTCInference(Node tc_rel, + std::vector<Node> reasons, + std::map<Node, std::unordered_set<Node> >& tc_graph, + std::map<Node, Node>& rel_tc_graph_exps, + Node start_node_rep, + Node cur_node_rep, + std::unordered_set<Node>& seen); void composeMembersForRels( Node ); void computeMembersForBinOpRel( Node ); @@ -165,8 +171,11 @@ private: void computeMembersForJoinImageTerm( Node ); bool isTCReachable( Node mem_rep, Node tc_rel ); - void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); + void isTCReachable(Node start, + Node dest, + std::unordered_set<Node>& hasSeen, + std::map<Node, std::unordered_set<Node> >& tc_graph, + bool& isReachable); /** Helper functions */ bool hasTerm( Node a ); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 655c2aa88..40f6080e5 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -47,7 +47,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj { IntStat d_statSharedTerms; // Needs to be a map from Nodes as after a backtrack they might not exist - typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; + typedef std::unordered_map<Node, shared_terms_list> SharedTermsMap; /** A map from atoms to a list of shared terms */ SharedTermsMap d_atomsToTerms; @@ -66,12 +66,11 @@ class SharedTermsDatabase : public context::ContextNotifyObj { SharedTermsTheoriesMap d_termsToTheories; /** Map from term to theories that have already been notified about the shared term */ - typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction> - AlreadyNotifiedMap; + typedef context::CDHashMap<TNode, theory::TheoryIdSet> AlreadyNotifiedMap; AlreadyNotifiedMap d_alreadyNotifiedMap; /** The registered equalities for propagation */ - typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet; + typedef context::CDHashSet<Node> RegisteredEqualitiesSet; RegisteredEqualitiesSet d_registeredEqualities; private: diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 9c9adf99e..4c3b2f17e 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -131,7 +131,7 @@ bool ArithEntail::checkApprox(Node ar) // c.isNull() means c = 1 bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1; std::vector<Node>& approx = mApprox[v]; - std::unordered_set<Node, NodeHashFunction> visited; + std::unordered_set<Node> visited; std::vector<Node> toProcess; toProcess.push_back(v); do @@ -561,7 +561,7 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict) << ", strict=" << strict << std::endl; // Find candidates variables to compute substitutions for - std::unordered_set<Node, NodeHashFunction> candVars; + std::unordered_set<Node> candVars; std::vector<Node> toVisit = {assumption}; while (!toVisit.empty()) { diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 41cb3e608..6c423e3b8 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -39,7 +39,7 @@ namespace strings { */ class BaseSolver { - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + using NodeSet = context::CDHashSet<Node>; public: BaseSolver(SolverState& s, InferenceManager& im); diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index ed220c1eb..a6e4ce698 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1078,7 +1078,7 @@ void CoreSolver::processNEqc(Node eqc, // the possible inferences std::vector<CoreInferInfo> pinfer; // compute normal forms that are effectively unique - std::unordered_map<Node, size_t, NodeHashFunction> nfCache; + std::unordered_map<Node, size_t> nfCache; std::vector<size_t> nfIndices; bool hasConstIndex = false; for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++) diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index 143155f55..4e8a0a96b 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -79,7 +79,7 @@ class CoreInferInfo class CoreSolver { friend class InferenceManager; - using NodeIntMap = context::CDHashMap<Node, int, NodeHashFunction>; + using NodeIntMap = context::CDHashMap<Node, int>; public: CoreSolver(SolverState& s, diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index e00668997..a1de5e295 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -251,7 +251,7 @@ void ExtfSolver::checkExtfEval(int effort) bool has_nreduce = false; std::vector<Node> terms = d_extt.getActive(); // the set of terms we have done extf inferences for - std::unordered_set<Node, NodeHashFunction> inferProcessed; + std::unordered_set<Node> inferProcessed; for (const Node& n : terms) { // Setup information about n, including if it is equal to a constant. diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index bfcf244d7..82b4f61ee 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -81,7 +81,7 @@ class ExtfInfoTmp */ class ExtfSolver { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: ExtfSolver(SolverState& s, diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 6b2c4dfc4..af905cbad 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -45,8 +45,7 @@ namespace strings { */ class InferProofCons : public ProofGenerator { - typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>, NodeHashFunction> - NodeInferInfoMap; + typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>> NodeInferInfoMap; public: InferProofCons(context::Context* c, diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index b18c64319..cf9c64bb1 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -72,8 +72,8 @@ namespace strings { */ class InferenceManager : public InferenceManagerBuffered { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashMap<Node, Node> NodeNodeMap; friend class InferInfo; public: diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index ace2756c1..bf4c20f85 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -63,7 +63,7 @@ bool RegExpOpr::checkConstRegExp( Node r ) { RegExpConstType RegExpOpr::getRegExpConstType(Node r) { Assert(r.getType().isRegExp()); - std::unordered_map<Node, RegExpConstType, NodeHashFunction>::iterator it; + std::unordered_map<Node, RegExpConstType>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(r); @@ -1345,8 +1345,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > Node RegExpOpr::removeIntersection(Node r) { Assert(checkConstRegExp(r)); 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(r); diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index d0ed07308..a20e9a0a9 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -78,7 +78,7 @@ class RegExpOpr { std::map<PairNodeStr, Node> d_dv_cache; std::map<PairNodeStr, std::pair<Node, int> > d_deriv_cache; /** cache mapping regular expressions to whether they contain constants */ - std::unordered_map<Node, RegExpConstType, NodeHashFunction> d_constCache; + std::unordered_map<Node, RegExpConstType> d_constCache; std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_fset_cache; std::map<PairNodes, Node> d_inter_cache; std::map<Node, std::vector<PairNodes> > d_split_cache; diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 38fc6fc8f..167ce9570 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -137,7 +137,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) NodeManager* nm = NodeManager::currentNM(); // representatives of strings that are the LHS of positive memberships that // we unfolded - std::unordered_set<Node, NodeHashFunction> repUnfold; + std::unordered_set<Node> repUnfold; // check positive (e=0), then negative (e=1) memberships for (unsigned e = 0; e < 2; e++) { @@ -329,7 +329,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems) { - std::unordered_set<Node, NodeHashFunction> remove; + std::unordered_set<Node> remove; for (const Node& m1 : mems) { diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index bf148a071..98e2449c5 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -38,11 +38,11 @@ namespace strings { class RegExpSolver { typedef context::CDList<Node> NodeList; - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; - typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; - typedef context::CDHashMap<Node, unsigned, NodeHashFunction> NodeUIntMap; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, bool> NodeBoolMap; + typedef context::CDHashMap<Node, int> NodeIntMap; + typedef context::CDHashMap<Node, unsigned> NodeUIntMap; + typedef context::CDHashMap<Node, Node> NodeNodeMap; + typedef context::CDHashSet<Node> NodeSet; public: RegExpSolver(SolverState& s, diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index b3ffa784f..126ee313d 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -207,7 +207,7 @@ class SkolemCache /** map from node pairs and identifiers to skolems */ std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; /** the set of all skolems we have generated */ - std::unordered_set<Node, NodeHashFunction> d_allSkolems; + std::unordered_set<Node> d_allSkolems; }; } // namespace strings diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h index ba9f0f4e1..39ba6168a 100644 --- a/src/theory/strings/strings_fmf.h +++ b/src/theory/strings/strings_fmf.h @@ -37,7 +37,7 @@ namespace strings { */ class StringsFmf { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: StringsFmf(context::Context* c, diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 4460e1ff3..d7a0a0554 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -437,8 +437,7 @@ const context::CDList<TNode>& TermRegistry::getFunctionTerms() const return d_functionsTerms; } -const context::CDHashSet<Node, NodeHashFunction>& TermRegistry::getInputVars() - const +const context::CDHashSet<Node>& TermRegistry::getInputVars() const { return d_inputVars; } diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index f0543c282..7c399759b 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -46,9 +46,9 @@ class InferenceManager; */ class TermRegistry { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet; + typedef context::CDHashMap<Node, Node> NodeNodeMap; public: TermRegistry(SolverState& s, @@ -147,7 +147,7 @@ class TermRegistry * Get the "input variables", corresponding to the set of leaf nodes of * string-like type that have been preregistered as terms to this object. */ - const context::CDHashSet<Node, NodeHashFunction>& getInputVars() const; + const context::CDHashSet<Node>& getInputVars() const; /** Returns true if any str.code terms have been preregistered */ bool hasStringCode() const; //---------------------------- end queries diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 02c0c3130..06a39ec64 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -210,7 +210,7 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl; } Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet; + std::map<TypeNode, std::unordered_set<Node> > repSet; // Generate model // get the relevant string equivalence classes for (const Node& s : termSet) @@ -222,9 +222,7 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, repSet[tn].insert(r); } } - for (const std::pair<const TypeNode, - std::unordered_set<Node, NodeHashFunction> >& rst : - repSet) + for (const std::pair<const TypeNode, std::unordered_set<Node> >& rst : repSet) { // get partition of strings of equal lengths, per type std::map<TypeNode, std::vector<std::vector<Node> > > colT; @@ -241,12 +239,11 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, return true; } -bool TheoryStrings::collectModelInfoType( - TypeNode tn, - const std::unordered_set<Node, NodeHashFunction>& repSet, - std::vector<std::vector<Node> >& col, - std::vector<Node>& lts, - TheoryModel* m) +bool TheoryStrings::collectModelInfoType(TypeNode tn, + const std::unordered_set<Node>& repSet, + std::vector<std::vector<Node> >& col, + std::vector<Node>& lts, + TheoryModel* m) { NodeManager* nm = NodeManager::currentNM(); std::map< Node, Node > processed; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 01111880d..a671129d4 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -60,8 +60,9 @@ namespace strings { */ class TheoryStrings : public Theory { friend class InferenceManager; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet; + public: TheoryStrings(context::Context* c, context::UserContext* u, @@ -195,12 +196,11 @@ class TheoryStrings : public Theory { * * Returns false if a conflict is discovered while doing this assignment. */ - bool collectModelInfoType( - TypeNode tn, - const std::unordered_set<Node, NodeHashFunction>& repSet, - std::vector<std::vector<Node> >& col, - std::vector<Node>& lts, - TheoryModel* m); + bool collectModelInfoType(TypeNode tn, + const std::unordered_set<Node>& repSet, + std::vector<std::vector<Node>>& col, + std::vector<Node>& lts, + TheoryModel* m); /** assert pending fact * diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index c3c444fc7..5a4a25e88 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -70,8 +70,8 @@ void flattenOp(Kind k, Node n, std::vector<Node>& conj) return; } // otherwise, traverse - 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/subs_minimize.cpp b/src/theory/subs_minimize.cpp index b58ffad33..e2a81f54a 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -73,9 +73,9 @@ bool SubstitutionMinimize::findWithImplied(Node t, std::vector<Node> tconj; getConjuncts(t, tconj); // map from conjuncts to their free symbols - std::map<Node, std::unordered_set<Node, NodeHashFunction> > tcFv; + std::map<Node, std::unordered_set<Node> > tcFv; - std::unordered_set<Node, NodeHashFunction> reqSet; + std::unordered_set<Node> reqSet; std::vector<Node> reqSubs; std::map<Node, unsigned> reqVarToIndex; for (const Node& v : reqVars) @@ -104,8 +104,7 @@ bool SubstitutionMinimize::findWithImplied(Node t, for (const Node& tc : tconj) { // ensure we've computed its free symbols - std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator - itf = tcFv.find(tc); + std::map<Node, std::unordered_set<Node> >::iterator itf = tcFv.find(tc); if (itf == tcFv.end()) { expr::getSymbols(tc, tcFv[tc]); @@ -181,8 +180,8 @@ bool SubstitutionMinimize::findInternal(Node n, Trace("subs-min") << "--- Compute values for subterms..." << std::endl; // the value of each subterm in n under the substitution - std::unordered_map<TNode, Node, TNodeHashFunction> value; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> value; + std::unordered_map<TNode, Node>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -262,12 +261,12 @@ bool SubstitutionMinimize::findInternal(Node n, } Trace("subs-min") << "--- Compute relevant variables..." << std::endl; - std::unordered_set<Node, NodeHashFunction> rlvFv; + std::unordered_set<Node> rlvFv; // only variables that occur in assertions are relevant visit.push_back(n); - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator itv; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator itv; do { cur = visit.back(); diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index e1d75d957..08936e3b6 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -40,18 +40,16 @@ namespace theory { * * This map is context-dependent. */ -class SubstitutionMap { - -public: - - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; +class SubstitutionMap +{ + public: + typedef context::CDHashMap<Node, Node> NodeMap; typedef NodeMap::iterator iterator; typedef NodeMap::const_iterator const_iterator; -private: - - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache; + private: + typedef std::unordered_map<Node, Node> NodeCache; /** A dummy context used by this class if none is provided */ context::Context d_context; @@ -68,18 +66,21 @@ private: Node internalSubstitute(TNode t, NodeCache& cache); /** Helper class to invalidate cache on user pop */ - class CacheInvalidator : public context::ContextNotifyObj { + class CacheInvalidator : public context::ContextNotifyObj + { bool& d_cacheInvalidated; - protected: - void contextNotifyPop() override { d_cacheInvalidated = true; } - public: - CacheInvalidator(context::Context* context, bool& cacheInvalidated) : - context::ContextNotifyObj(context), - d_cacheInvalidated(cacheInvalidated) { + protected: + void contextNotifyPop() override { d_cacheInvalidated = true; } + + public: + CacheInvalidator(context::Context* context, bool& cacheInvalidated) + : context::ContextNotifyObj(context), + d_cacheInvalidated(cacheInvalidated) + { } - };/* class SubstitutionMap::CacheInvalidator */ + }; /* class SubstitutionMap::CacheInvalidator */ /** * This object is notified on user pop and marks the SubstitutionMap's @@ -103,7 +104,8 @@ private: /** * Returns true iff x is in the substitution map */ - bool hasSubstitution(TNode x) const { + bool hasSubstitution(TNode x) const + { return d_substitutions.find(x) != d_substitutions.end(); } @@ -115,8 +117,10 @@ private: * is mainly intended for constructing assertions about what has * already been put in the map. */ - TNode getSubstitution(TNode x) const { - AssertArgument(hasSubstitution(x), x, "element not in this substitution map"); + TNode getSubstitution(TNode x) const + { + AssertArgument( + hasSubstitution(x), x, "element not in this substitution map"); return (*d_substitutions.find(x)).second; } @@ -128,29 +132,20 @@ private: /** * Apply the substitutions to the node. */ - Node apply(TNode t, bool doRewrite = false) const { + Node apply(TNode t, bool doRewrite = false) const + { return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite); } - iterator begin() { - return d_substitutions.begin(); - } + iterator begin() { return d_substitutions.begin(); } - iterator end() { - return d_substitutions.end(); - } + iterator end() { return d_substitutions.end(); } - const_iterator begin() const { - return d_substitutions.begin(); - } + const_iterator begin() const { return d_substitutions.begin(); } - const_iterator end() const { - return d_substitutions.end(); - } + const_iterator end() const { return d_substitutions.end(); } - bool empty() const { - return d_substitutions.empty(); - } + bool empty() const { return d_substitutions.empty(); } /** * Print to the output stream @@ -158,7 +153,7 @@ private: void print(std::ostream& out) const; void debugPrint() const; -};/* class SubstitutionMap */ +}; /* class SubstitutionMap */ inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) { subst.print(out); diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 04200ed70..86ab160d8 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -43,8 +43,7 @@ class PreRegisterVisitor { /** The engine */ TheoryEngine* d_engine; - typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction> - TNodeToTheorySetMap; + typedef context::CDHashMap<TNode, theory::TheoryIdSet> TNodeToTheorySetMap; /** * Map from terms to the theories that have already had this term pre-registered. @@ -129,10 +128,8 @@ class PreRegisterVisitor { * been visited already, we need to visit it again, since we need to associate it with both atoms. */ class SharedTermsVisitor { - using TNodeVisitedMap = - std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>; - using TNodeToTheorySetMap = - context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>; + using TNodeVisitedMap = std::unordered_map<TNode, theory::TheoryIdSet>; + using TNodeToTheorySetMap = context::CDHashMap<TNode, theory::TheoryIdSet>; /** * String representation of the visited map, for debugging purposes. */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 5d2128c54..d6ad4cd41 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -341,8 +341,9 @@ bool Theory::isLegalElimination(TNode x, TNode val) return tm->isLegalElimination(x, val); } -std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ - std::unordered_set<TNode, TNodeHashFunction> currentlyShared; +std::unordered_set<TNode> Theory::currentlySharedTerms() const +{ + std::unordered_set<TNode> currentlyShared; for (shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i) { currentlyShared.insert (*i); diff --git a/src/theory/theory.h b/src/theory/theory.h index 9cf663a4f..8f69d4cb2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -828,7 +828,7 @@ class Theory { * This is a utility function for constructing a copy of the currently shared terms * in a queriable form. As this is */ - std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const; + std::unordered_set<TNode> currentlySharedTerms() const; /** * This allows the theory to be queried for whether a literal, lit, is diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1acaca34f..abbca451a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1119,8 +1119,8 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return d_sharedSolver->getEqualityStatus(a, b); } -const std::unordered_set<TNode, TNodeHashFunction>& -TheoryEngine::getRelevantAssertions(bool& success) +const std::unordered_set<TNode>& TheoryEngine::getRelevantAssertions( + bool& success) { // if we are not in SAT mode, or there is no relevance manager, we fail if (!d_inSatMode || d_relManager == nullptr) @@ -1203,10 +1203,9 @@ TrustNode TheoryEngine::getExplanation(TNode node) struct AtomsCollect { std::vector<TNode> d_atoms; - std::unordered_set<TNode, TNodeHashFunction> d_visited; - -public: + std::unordered_set<TNode> d_visited; + public: typedef void return_type; bool alreadyVisited(TNode current, TNode parent) { @@ -1508,7 +1507,7 @@ theory::TrustNode TheoryEngine::getExplanation( // vector of trust nodes to explain at the end std::vector<std::pair<TheoryId, TrustNode>> texplains; // cache of nodes we have already explained by some theory - std::unordered_map<Node, size_t, NodeHashFunction> cache; + std::unordered_map<Node, size_t> cache; while (i < explanationVector.size()) { // Get the current literal to explain diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4c097a262..6887959ed 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -68,10 +68,10 @@ struct NodeTheoryPair { };/* struct NodeTheoryPair */ struct NodeTheoryPairHashFunction { - NodeHashFunction hashFunction; + std::hash<Node> hashFunction; // Hash doesn't take into account the timestamp size_t operator()(const NodeTheoryPair& pair) const { - uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node)); + uint64_t hash = fnv1a::fnv1a_64(std::hash<Node>()(pair.d_node)); return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash)); } };/* struct NodeTheoryPairHashFunction */ @@ -162,7 +162,7 @@ class TheoryEngine { * An empty set of relevant assertions, which is returned as a dummy value for * getRelevantAssertions when relevance is disabled. */ - std::unordered_set<TNode, TNodeHashFunction> d_emptyRelevantSet; + std::unordered_set<TNode> d_emptyRelevantSet; /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; @@ -637,8 +637,7 @@ class TheoryEngine { * relevance manager failed to compute relevant assertions due to an internal * error. */ - const std::unordered_set<TNode, TNodeHashFunction>& getRelevantAssertions( - bool& success); + const std::unordered_set<TNode>& getRelevantAssertions(bool& success); /** * Forwards an entailment check according to the given theoryOfMode. diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 167216226..48969aa21 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -38,9 +38,8 @@ namespace cvc5 { */ class TheoryEngineProofGenerator : public ProofGenerator { - typedef context:: - CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction> - NodeLazyCDProofMap; + typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>> + NodeLazyCDProofMap; public: TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u); diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index a785af186..2cb7d9d30 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -68,7 +68,7 @@ class ProofEqEngine; */ class TheoryInferenceManager { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashSet<Node> NodeSet; public: /** diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a95546cf5..dd1e0b883 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -184,7 +184,7 @@ Cardinality TheoryModel::getCardinality(TypeNode tn) const Node TheoryModel::getModelValue(TNode n) const { - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); + std::unordered_map<Node, Node>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { return (*it).second; } diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index ab66e8fe7..951a62cae 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -398,7 +398,7 @@ class TheoryModel /** are we using model cores? */ bool d_using_model_core; /** symbols that are in the model core */ - std::unordered_set<Node, NodeHashFunction> d_model_core; + std::unordered_set<Node> d_model_core; /** Get model value function. * * This function is a helper function for getValue. @@ -414,7 +414,7 @@ class TheoryModel virtual void addTermInternal(TNode n); private: /** cache for getModelValue */ - mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; + mutable std::unordered_map<Node, Node> d_modelCache; //---------------------------- separation logic /** the value of the heap */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 2103c3997..0a038845c 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -340,7 +340,7 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( void TheoryEngineModelBuilder::addToTypeList( TypeNode tn, std::vector<TypeNode>& type_list, - std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting) + std::unordered_set<TypeNode>& visiting) { if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end()) { @@ -427,11 +427,11 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // the set of equivalence classes that are "assignable", i.e. those that have // an assignable expression in them (see isAssignable), and have not already // been assigned a constant. - std::unordered_set<Node, NodeHashFunction> assignableEqc; + std::unordered_set<Node> assignableEqc; // The set of equivalence classes that are "evaluable", i.e. those that have // an expression in them that is not assignable, and have not already been // assigned a constant. - std::unordered_set<Node, NodeHashFunction> evaluableEqc; + std::unordered_set<Node> evaluableEqc; // Assigner objects for relevant equivalence classes that require special // ways of assigning values, e.g. those that take into account assignment // exclusion sets. @@ -449,7 +449,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // should we compute assigner objects? bool computeAssigners = tm->hasAssignmentExclusionSets(); // the set of exclusion sets we have processed - std::unordered_set<Node, NodeHashFunction> processedExcSet; + std::unordered_set<Node> processedExcSet; for (; !eqcs_i.isFinished(); ++eqcs_i) { Node eqc = *eqcs_i; @@ -591,13 +591,13 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) { assertedReps[eqc] = rep; typeRepSet.add(eqct.getBaseType(), eqc); - std::unordered_set<TypeNode, TypeNodeHashFunction> visiting; + std::unordered_set<TypeNode> visiting; addToTypeList(eqct.getBaseType(), type_list, visiting); } else { typeNoRepSet.add(eqct, eqc); - std::unordered_set<TypeNode, TypeNodeHashFunction> visiting; + std::unordered_set<TypeNode> visiting; addToTypeList(eqct, type_list, visiting); } diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index af3f30fb0..195ba9e0f 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -44,8 +44,8 @@ namespace theory { */ class TheoryEngineModelBuilder { - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_map<Node, Node> NodeMap; + typedef std::unordered_set<Node> NodeSet; public: TheoryEngineModelBuilder(); @@ -164,10 +164,9 @@ class TheoryEngineModelBuilder * For example, if tn is (Array Int Bool) and type_list is empty, * then we append ( Int, Bool, (Array Int Bool) ) to type_list. */ - void addToTypeList( - TypeNode tn, - std::vector<TypeNode>& type_list, - std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting); + void addToTypeList(TypeNode tn, + std::vector<TypeNode>& type_list, + std::unordered_set<TypeNode>& visiting); /** assign function f based on the model m. * This construction is based on "table form". For example: * (f 0 1) = 1 diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 79b5dbe01..58dd763e0 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -72,7 +72,7 @@ namespace theory { */ class TheoryPreprocessor { - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDHashMap<Node, Node> NodeMap; public: /** Constructs a theory preprocessor */ diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp index 70f35afb8..667c8d114 100644 --- a/src/theory/theory_proof_step_buffer.cpp +++ b/src/theory/theory_proof_step_buffer.cpp @@ -186,7 +186,7 @@ Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n) } children.clear(); // remove duplicates while keeping the order of children - std::unordered_set<TNode, TNodeHashFunction> clauseSet; + std::unordered_set<TNode> clauseSet; unsigned size = n.getNumChildren(); for (unsigned i = 0; i < size; ++i) { diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index b7b526205..136992fbe 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -38,7 +38,7 @@ namespace theory { */ class TrustSubstitutionMap : public ProofGenerator { - using NodeUIntMap = context::CDHashMap<Node, size_t, NodeHashFunction>; + using NodeUIntMap = context::CDHashMap<Node, size_t>; public: TrustSubstitutionMap(context::Context* c, diff --git a/src/theory/type_set.cpp b/src/theory/type_set.cpp index 00a3d77fd..12bb2bae6 100644 --- a/src/theory/type_set.cpp +++ b/src/theory/type_set.cpp @@ -113,14 +113,14 @@ Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType) // this is necessary for parametric types whose values are constructed from // other types to ensure that we do not enumerate subterms of other // previously enumerated values - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; addSubTerms(n, visited); ++(*te); return n; } void TypeSet::addSubTerms(TNode n, - std::unordered_set<TNode, TNodeHashFunction>& visited, + std::unordered_set<TNode>& visited, bool topLevel) { if (visited.find(n) == visited.end()) diff --git a/src/theory/type_set.h b/src/theory/type_set.h index 229ec2001..fb4859602 100644 --- a/src/theory/type_set.h +++ b/src/theory/type_set.h @@ -33,10 +33,8 @@ namespace theory { class TypeSet { public: - typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> - TypeSetMap; - typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> - TypeToTypeEnumMap; + typedef std::unordered_map<TypeNode, std::set<Node>*> TypeSetMap; + typedef std::unordered_map<TypeNode, TypeEnumerator*> TypeToTypeEnumMap; typedef TypeSetMap::iterator iterator; typedef TypeSetMap::const_iterator const_iterator; @@ -81,7 +79,7 @@ class TypeSet * (very low expression depth). */ void addSubTerms(TNode n, - std::unordered_set<TNode, TNodeHashFunction>& visited, + std::unordered_set<TNode>& visited, bool topLevel = true); }; /* class TypeSet */ diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 70db9257f..1809a30bd 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -39,8 +39,8 @@ class TheoryUF; class CardinalityExtension { protected: - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; - typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, bool> NodeBoolMap; + typedef context::CDHashMap<Node, int> NodeIntMap; public: /** diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 8e5e0f659..c63f8b51d 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -106,7 +106,7 @@ bool EqProof::expandTransitivityForDisequalities( Node conclusion, std::vector<Node>& premises, CDProof* p, - std::unordered_set<Node, NodeHashFunction>& assumptions) const + std::unordered_set<Node>& assumptions) const { Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: check if need " @@ -684,8 +684,8 @@ void EqProof::reduceNestedCongruence( Node conclusion, std::vector<std::vector<Node>>& transitivityMatrix, CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited, - std::unordered_set<Node, NodeHashFunction>& assumptions, + std::unordered_map<Node, Node>& visited, + std::unordered_set<Node>& assumptions, bool isNary) const { Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i @@ -785,8 +785,8 @@ void EqProof::reduceNestedCongruence( Node EqProof::addToProof(CDProof* p) const { - std::unordered_map<Node, Node, NodeHashFunction> cache; - std::unordered_set<Node, NodeHashFunction> assumptions; + std::unordered_map<Node, Node> cache; + std::unordered_set<Node> assumptions; Node conclusion = addToProof(p, cache, assumptions); Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion << "\n"; @@ -840,13 +840,11 @@ Node EqProof::addToProof(CDProof* p) const return newConclusion; } -Node EqProof::addToProof( - CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited, - std::unordered_set<Node, NodeHashFunction>& assumptions) const +Node EqProof::addToProof(CDProof* p, + std::unordered_map<Node, Node>& visited, + std::unordered_set<Node>& assumptions) const { - std::unordered_map<Node, Node, NodeHashFunction>::const_iterator it = - visited.find(d_node); + std::unordered_map<Node, Node>::const_iterator it = visited.find(d_node); if (it != visited.end()) { Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index c938c8d9d..3179da592 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -88,10 +88,9 @@ class EqProof * equalities) * @return the node that is the conclusion of the proof as added to p. */ - Node addToProof( - CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited, - std::unordered_set<Node, NodeHashFunction>& assumptions) const; + Node addToProof(CDProof* p, + std::unordered_map<Node, Node>& visited, + std::unordered_set<Node>& assumptions) const; /** Removes all reflexivity steps, i.e. (= t t), from premises. */ void cleanReflPremises(std::vector<Node>& premises) const; @@ -173,7 +172,7 @@ class EqProof Node conclusion, std::vector<Node>& premises, CDProof* p, - std::unordered_set<Node, NodeHashFunction>& assumptions) const; + std::unordered_set<Node>& assumptions) const; /** Expand coarse-grained transitivity steps for theory disequalities * @@ -347,8 +346,8 @@ class EqProof Node conclusion, std::vector<std::vector<Node>>& transitivityMatrix, CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited, - std::unordered_set<Node, NodeHashFunction>& assumptions, + std::unordered_map<Node, Node>& visited, + std::unordered_set<Node>& assumptions, bool isNary) const; }; /* class EqProof */ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 8676e446e..024774593 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -136,7 +136,7 @@ private: KindMap d_congruenceKindsExtOperators; /** Map from nodes to their ids */ - std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; + std::unordered_map<TNode, EqualityNodeId> d_nodeIds; /** Map from function applications to their ids */ typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 13709c2ab..853ae719b 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -128,7 +128,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f); if (itus == d_uf_std_skolem.end()) { - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(f, fvs); Node lem; if (!fvs.empty()) diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index 58320d07b..af8f727fd 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -49,8 +49,8 @@ class TheoryUF; */ class HoExtension { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashMap<Node, Node> NodeNodeMap; public: HoExtension(TheoryState& state, TheoryInferenceManager& im); diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index aed662c4c..4ca13d93f 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -80,9 +80,8 @@ class EqualityEngine; */ class ProofEqEngine : public EagerProofGenerator { - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; - typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction> - NodeProofMap; + typedef context::CDHashSet<Node> NodeSet; + typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofMap; public: ProofEqEngine(context::Context* c, diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 65ed4d542..aa5d9d953 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -59,7 +59,7 @@ SymmetryBreaker::Template::Template() : } TNode SymmetryBreaker::Template::find(TNode n) { - unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); + unordered_map<TNode, TNode>::iterator i = d_reps.find(n); if(i == d_reps.end()) { return n; } else { @@ -396,7 +396,7 @@ void SymmetryBreaker::assertFormula(TNode phi) { break; } } - unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); + unordered_map<TNode, set<TNode>>& ps = t.partitions(); for (auto& kv : ps) { Debug("ufsymm") << "UFSYMM partition*: " << kv.first; @@ -416,11 +416,12 @@ void SymmetryBreaker::assertFormula(TNode phi) { } if(!d_template.match(phi)) { // we hit a bad match, extract the partitions and reset the template - unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); + unordered_map<TNode, set<TNode>>& ps = d_template.partitions(); Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; - for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); - i != ps.end(); - ++i) { + for (unordered_map<TNode, set<TNode>>::iterator i = ps.begin(); + i != ps.end(); + ++i) + { Debug("ufsymm") << "UFSYMM partition: " << (*i).first; set<TNode>& p = (*i).second; if(Debug.isOn("ufsymm")) { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index b5d0fbdf9..67eabb6ba 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -63,8 +63,8 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; NodeBuilder d_assertions; - std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; - std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; + std::unordered_map<TNode, std::set<TNode>> d_sets; + std::unordered_map<TNode, TNode> d_reps; TNode find(TNode n); bool matchRecursive(TNode t, TNode n); @@ -72,7 +72,7 @@ class SymmetryBreaker : public context::ContextNotifyObj { public: Template(); bool match(TNode n); - std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } + std::unordered_map<TNode, std::set<TNode>>& partitions() { return d_sets; } Node assertions() { switch(d_assertions.getNumChildren()) { case 0: return Node::null(); @@ -90,10 +90,9 @@ public: typedef TNode Term; typedef std::list<Term> Terms; typedef std::set<Term> TermEq; - typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs; - -private: + typedef std::unordered_map<Term, TermEq> TermEqs; + private: /** * This class wasn't initially built to be incremental. It should * be attached to a UserContext so that it clears everything when @@ -112,7 +111,7 @@ private: Permutations d_permutations; Terms d_terms; Template d_template; - std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache; + std::unordered_map<Node, Node> d_normalizationCache; TermEqs d_termEqs; TermEqs d_termEqsOnly; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 5d91faa87..9cf47bab3 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -349,7 +349,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder& learned) vector<TNode> workList; workList.push_back(n); - std::unordered_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode> processed; while(!workList.empty()) { n = workList.back(); |