summaryrefslogtreecommitdiff
path: root/src/theory/evaluator.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/evaluator.h')
-rw-r--r--src/theory/evaluator.h11
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback