diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-30 09:41:12 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-30 09:41:12 -0600 |
commit | 9d52110430b63500d96a15b0a2e0d16517233f91 (patch) | |
tree | c218487154ba30c168f82e09f0e263ff8486c733 /src/theory/evaluator.h | |
parent | 13ef9140d1ba6740ccb2c1f29bd2d243de6872c2 (diff) |
External cache argument for evaluator (#3672)
Diffstat (limited to 'src/theory/evaluator.h')
-rw-r--r-- | src/theory/evaluator.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 533a03657..58e179fbe 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -95,6 +95,14 @@ class Evaluator Node eval(TNode n, const std::vector<Node>& args, const std::vector<Node>& vals) const; + /** + * Same as above, but with a precomputed visited map. + */ + Node eval( + TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals, + const std::unordered_map<Node, Node, NodeHashFunction>& visited) const; private: /** @@ -117,7 +125,8 @@ class Evaluator TNode n, const std::vector<Node>& args, const std::vector<Node>& vals, - std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const; + std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode, + std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results) const; /** reconstruct * * This function reconstructs the result of evaluating n using a combination |