diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-10 17:42:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-10 17:42:31 -0600 |
commit | e87746af7e0d9c838064304b89f0ae55f483bd5a (patch) | |
tree | 10f038e6f85902a713f3fca6d9cd2c49c783d764 /src/theory/evaluator.h | |
parent | d19c52821bb911413ff3dd4494c08a42a1db1e22 (diff) |
Incorporate rewriting on demand in the evaluator (#3549)
Diffstat (limited to 'src/theory/evaluator.h')
-rw-r--r-- | src/theory/evaluator.h | 30 |
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 |