Incorporate rewriting on demand in the evaluator (#3549)

1 files changed, 20 insertions, 10 deletions

diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index ce19a1f67..a65ffdf19 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -85,9 +85,9 @@ class Evaluator
  public:
   /**
    * Evaluates node `n` under the substitution described by the variable names
-   * `args` and the corresponding values `vals`. The function returns a null
-   * node if there is a subterm that is not constant under the substitution or
-   * if an operator is not supported by the evaluator.
+   * `args` and the corresponding values `vals`. This method uses evaluation
+   * for subterms that evaluate to constants supported in the EvalResult
+   * class and substitution with rewriting for the others.
    *
    * The nodes in the vals must be constant values, that is, they must return
    * true for isConst().
@@ -100,14 +100,24 @@ class Evaluator
   /**
    * Evaluates node `n` under the substitution described by the variable names
    * `args` and the corresponding values `vals`. The internal version returns
-   * an EvalResult which has slightly less overhead for recursive calls. The
-   * function returns an invalid result if there is a subterm that is not
-   * constant under the substitution or if an operator is not supported by the
-   * evaluator.
+   * an EvalResult which has slightly less overhead for recursive calls.
+   *
+   * The method returns an invalid EvalResult if the result of the substitution
+   * on n does not result in a constant value that is one of those supported in
+   * the EvalResult class. Notice that e.g. datatype constants are not supported
+   * in this class.
+   *
+   * This method additionally adds subterms of n that could not be evaluated
+   * (in the above sense) to the map evalAsNode. For each such subterm n', we
+   * store the node corresponding to the result of applying the substitution
+   * `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);
+  EvalResult evalInternal(
+      TNode n,
+      const std::vector<Node>& args,
+      const std::vector<Node>& vals,
+      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode);
 };
 
 }  // namespace theory