diff options
Diffstat (limited to 'src/theory/evaluator.cpp')
| -rw-r--r-- | src/theory/evaluator.cpp | 44 |
1 files changed, 20 insertions, 24 deletions
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) { |