diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-05-12 23:33:00 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-13 06:33:00 +0000 |
| commit | 31242de4b423d7225174dd1672edb2dacb68f5b8 (patch) | |
| tree | 657a453475affc67628b1391909af92f3346b411 /src/theory/evaluator.h | |
| parent | ffd7bb2069df08c31fd9d8a03d786f1e9fc7147c (diff) | |
Add std::hash overloads for Node, TNode and TypeNode. (#6534)
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
Diffstat (limited to 'src/theory/evaluator.h')
| -rw-r--r-- | src/theory/evaluator.h | 22 |
1 files changed, 10 insertions, 12 deletions
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 |